Skip to content

Latest commit

 

History

History
132 lines (119 loc) · 5.82 KB

notes.org

File metadata and controls

132 lines (119 loc) · 5.82 KB

MetaCoq

Inductive definitions

metacoq defintion

type one_inductive_body = { ind_name : ident; ind_type : T.term;
                            ind_kelim : sort_family list;
                            ind_ctors : ((ident * T.term) * nat) list;
                            ind_projs : (ident * T.term) list }

val ind_name : one_inductive_body -> ident

val ind_type : one_inductive_body -> T.term

val ind_kelim : one_inductive_body -> sort_family list

val ind_ctors : one_inductive_body -> ((ident * T.term) * nat) list

val ind_projs : one_inductive_body -> (ident * T.term) list

type mutual_inductive_body = { ind_finite : recursivity_kind;
                               ind_npars : nat;
                               ind_params : context;
                               ind_bodies : one_inductive_body list;
                               ind_universes : universes_decl }

TemplateMonad

metacoq definition

Cumulative Inductive TemplateMonad@{t u} : Type@{t} -> Prop :=
(* Monadic operations *)
| tmReturn : forall {A:Type@{t}}, A -> TemplateMonad A
| tmBind : forall {A B : Type@{t}}, TemplateMonad A -> (A -> TemplateMonad B)
                               -> TemplateMonad B

(* General commands *)
| tmPrint : forall {A:Type@{t}}, A -> TemplateMonad unit
| tmMsg   : string -> TemplateMonad unit
| tmFail : forall {A:Type@{t}}, string -> TemplateMonad A
| tmEval : reductionStrategy -> forall {A:Type@{t}}, A -> TemplateMonad A

(* Return the defined constant *)
| tmLemma : ident -> forall A : Type@{t}, TemplateMonad A
| tmDefinitionRed_ : forall (opaque : bool), ident -> option reductionStrategy -> forall {A:Type@{t}}, A -> TemplateMonad A
| tmAxiomRed : ident -> option reductionStrategy -> forall A : Type@{t}, TemplateMonad A

(* Guaranteed to not cause "... already declared" error *)
| tmFreshName : ident -> TemplateMonad ident

| tmAbout : qualid -> TemplateMonad (option global_reference)
| tmCurrentModPath : unit -> TemplateMonad string

(* Quoting and unquoting commands *)
(* Similar to Quote Definition ... := ... *)
| tmQuote : forall {A:Type@{t}}, A  -> TemplateMonad Ast.term
(* Similar to Quote Recursively Definition ... := ...*)
| tmQuoteRec : forall {A:Type@{t}}, A  -> TemplateMonad program
(* Quote the body of a definition or inductive. Its name need not be fully qualified *)
| tmQuoteInductive : qualid -> TemplateMonad mutual_inductive_body
| tmQuoteUniverses : TemplateMonad constraints
| tmQuoteConstant : qualid -> bool (* bypass opacity? *) -> TemplateMonad constant_entry
(* unquote before making the definition *)
(* FIXME take an optional universe context as well *)
| tmMkInductive : mutual_inductive_entry -> TemplateMonad unit
| tmUnquote : Ast.term  -> TemplateMonad typed_term@{u}
| tmUnquoteTyped : forall A : Type@{t}, Ast.term -> TemplateMonad A

(* Typeclass registration and querying for an instance *)
| tmExistingInstance : qualid -> TemplateMonad unit
| tmInferInstance : option reductionStrategy -> forall A : Type@{t}, TemplateMonad (option A)

AST definition

metacoq definition

Inductive term : Set :=
| tRel (n : nat)
| tVar (id : ident) (* For free variables (e.g. in a goal) *)
| tEvar (ev : nat) (args : list term)
| tSort (s : universe)
| tCast (t : term) (kind : cast_kind) (v : term)
| tProd (na : name) (ty : term) (body : term)
| tLambda (na : name) (ty : term) (body : term)
| tLetIn (na : name) (def : term) (def_ty : term) (body : term)
| tApp (f : term) (args : list term)
| tConst (c : kername) (u : universe_instance)
| tInd (ind : inductive) (u : universe_instance)
| tConstruct (ind : inductive) (idx : nat) (u : universe_instance)
| tCase (ind_and_nbparams: inductive*nat) (type_info:term)
        (discr:term) (branches : list (nat * term))
| tProj (proj : projection) (t : term)
| tFix (mfix : mfixpoint term) (idx : nat)
| tCoFix (mfix : mfixpoint term) (idx : nat).

And inductive in this case stands for

type inductive = { inductive_mind : kername; inductive_ind : nat }

in basicAst.mli

Equations

Subterm relation

equations definition it uses ederive mechanism, as defined in subterm.ml sigma in the definition comes from the following lines:

let sigma = Evd.from_env env in
let sigma, c = Evd.fresh_global ~rigid:Evd.univ_rigid env sigma s

Subterm metacoq

Parameters:

from AgdaTutorial by Diviánszky Péter

“The first index can be turned into a new parameter if each constructor has the same variable on the first index position (in the result type).” Which means that in subterms parameters can be arbitrary, so this is a perfectly valid example of parameterized type:

Inductive nnat (A : Type) : Type :=
  n_zero : nnat A
| n_one : (nat -> nnat (list A)) -> nnat A.

Surprisingly, coq-equations can’t derive subterm relation for this.

The error for the above type is:

Error: Illegal application:
The term "nnat_direct_subterm" of type "forall A : Type, nnat A -> nnat A -> Prop"
cannot be applied to the terms
 "A" : "Type"
 "n n0" : "nnat (list A)"
 "n_one A n" : "nnat A"
The 2nd term has type "nnat (list A)" which should be coercible to
"nnat A".

Question:

It should be possible to generalize this to the “proper” subterms, essentially making it an index.