lambdapi 2.4.1 · OCaml Package

Generation of induction principles.

We only consider first-order dependent types (no functional arguments). Polymorphic types can be encoded by using codes. In case of a mutually defined types, we generate an induction for each type. A single induction principle can be defined from those individual induction principles by using a conjunction operator.

In the OCaml code, the prefix "ind" is used for inductive types. The prefix "rec" is used for recursors, aka induction principles.

val log_ind : 'a Lplib.Base.outfmt -> 'a

type inductive = (Core.Term.sym * Core.Term.sym list) list

Type for inductive type definitions.

type config = {

symb_Prop : Core.Term.sym;
(*
: TYPE. Type of propositions.
*)
symb_prf : Core.Term.sym;
(*
: Prop → TYPE. Interpretation of propositions as types.
*)

}

Builtin configuration for induction.

val get_config : Core.Sig_state.t -> Common.Pos.popt -> config

get_config ss pos build the configuration using ss.

val prf_of : 
  config ->
  Core.Term.tvar ->
  Core.Term.tbox list ->
  Core.Term.tbox ->
  Core.Term.tbox

prf_of p c ts t returns the term c.symb_prf (p t1 ... tn t) where ts = ts1;...;tsn.

val gen_safe_prefixes : inductive -> string * string * string

compute safe prefixes for predicate and constructor argument variables.

type data = {

ind_var : Core.Term.tvar;
(*
predicate variable
*)
ind_type : Core.Term.tbox;
(*
predicate variable type
*)
ind_conclu : Core.Term.tbox;
(*
induction principle conclusion
*)

}

Type of maps associating to every inductive type some data useful for generating the induction principles.

type ind_pred_map = (Core.Term.sym * data) list

val ind_typ_with_codom : 
  Common.Pos.popt ->
  Core.Term.sym ->
  Core.Env.t ->
  (Core.Term.tbox list -> Core.Term.tbox) ->
  string ->
  Core.Term.term ->
  Core.Term.tbox

ind_typ_with_codom pos ind_sym env codom x_str a assumes that a is of the form Π(i1:a1),...,Π(in:an), TYPE. It then generates a tbox similar to this type except that TYPE is replaced by codom [i1;...;in]. The string x_str is used as prefix for the variables ik.

val create_ind_pred_map : 
  Common.Pos.popt ->
  config ->
  int ->
  inductive ->
  string ->
  string ->
  string ->
  Core.Term.tvar array * Core.Env.t * ind_pred_map

create_ind_pred_map pos c arity ind_list a_str p_str x_str builds an ind_pred_map from ind_list. The resulting list is in reverse order wrt ind_list. a_str is used as prefix for parameter names, p_str is used as prefix for predicate variable names, and x_str is used as prefix for the names of the variable arguments of predicate variables.

val fold_cons_type : 
  Common.Pos.popt ->
  ind_pred_map ->
  string ->
  Core.Term.sym ->
  Core.Term.tvar array ->
  Core.Term.sym ->
  (int -> Core.Term.tvar -> 'var) ->
  'a ->
  (Core.Env.t ->
    Core.Term.sym ->
    Core.Term.tvar ->
    Core.Term.term list ->
    'var ->
    'aux) ->
  ('a -> 'var -> 'aux -> 'a) ->
  (Core.Term.term -> 'var -> 'aux -> 'c -> 'c) ->
  ('a -> 'var -> 'a) ->
  (Core.Term.term -> 'var -> 'c -> 'c) ->
  ('var list -> 'a -> Core.Term.tvar -> Core.Term.term list -> 'c) ->
  'c

fold_cons_type generates some value of type 'c by traversing the structure of cons_sym.sym_type and accumulating some data of type 'a.

pos is the position of the inductive command.

ind_pred_map is defined above.

x_str is a string used as prefix for generating variable names when deconstructing a product with LibTerm.unbind_name.

ind_sym is an inductive type symbol of ind_pred_map.

cons_sym is a constructor symbol of ind_sym.

inj_var injects traversed bound variables into the type 'var.

init is the initial value of type 'a.

The traversal is made by the function fold : (xs : 'var list) -> (acc : 'a) -> term -> 'c below. It keeps track of the variables xs we went through (the last variable comes first) and some accumulator acc set to init at the beginning.

During the traversal, there are several possible cases:

1) If the argument is a product of the form Π x:t, u with t of the form Π y₁:a₁, …, Π yₙ:aₙ, s ts and s mapped to p in ind_pred_map, then the result is rec_dom t x' v next where x' = inj_var (length xs) x, v = aux env s p ts x', env = y₁:a₁; …; yₙ:aₙ and next = fold (x'::xs) acc' u is the result of the traversal of u with the list of variables extended with x and the accumulator acc' = acc_rec_dom acc x' v.

2) If the type argument is a product Πx:t, u not of the previous form, then the result is nonrec_dom t x' next where next = fold (x'::xs) acc' u and acc' = acc_nonrec_dom acc x'.

3) If the type argument is of the form ind_sym ts, then the result is codom ts xs acc.

4) Any other case is an error.

val gen_rec_types : 
  config ->
  Common.Pos.popt ->
  inductive ->
  Core.Term.tvar array ->
  Core.Env.t ->
  ind_pred_map ->
  string ->
  Core.Term.term list

gen_rec_type c pos ind_list vs env ind_pred_map x_str generates the induction principles for each type in the inductive definition ind_list defined at the position pos whose parameters are vs. x_str is a string used for prefixing variable names that are generated. Remark: in the generated induction principles, each recursive argument is followed by its induction hypothesis. For instance, with inductive T:TYPE := c: T->T->T, we get ind_T: Π p:T -> Prop, (Π x₀:T, π(p x₀)-> Π x₁:T, π(p x₁)-> π(p (c x₀ x₁)) -> Π x:T, π(p x).

val rec_name : Core.Term.sym -> string

rec_name ind_sym returns the name of the induction principle associated to the inductive type symbol ind_sym.

val iter_rec_rules : 
  Common.Pos.popt ->
  inductive ->
  Core.Term.tvar array ->
  ind_pred_map ->
  (Parsing.Syntax.p_rule -> unit) ->
  unit

iter_rec_rules pos ind_list vs rec_sym_list ind_pred_map generates the recursor rules for the inductive type definition ind_list as position pos with parameters vs, recursors are rec_sym_list and ind_pred_map.

For instance, inductive T : Π(i1:A1),..,Π(im:Am), TYPE := c1:T1 | .. | cn:Tn generates a rule for each constructor. If Ti = Π x1:B1,..,Π xk:Bk,T then the rule for ci is ind_T p pc1 .. pcn _ .. _ (ci x1 .. xk) --> pci x1 t1? ... xk tk? with m underscores, tj? = ind_T p pc1 .. pcn _ .. _ xj if Bj = T v1 ... vm, and nothing otherwise.

package lambdapi