Pierre Vial (Jun 30 2020 at 09:14): Pierre Vial (Jun 30 2020 at 09:14):In a project, I'm trying to define a predicate to characterize first order formulas. For that, I try to some pattern-matching on connectors from Prop.
MetaCoq Quote Definition and_reif := Eval compute in and.
MetaCoq Quote Definition or_reif := Eval compute in or.
MetaCoq Quote Definition not_reif := Eval compute in not.
To perform the actual pattern-matching, I recover the reified terms corresponding to the constructors.
For instance:
Print not_reif.
gives me
not_reif = tLambda (nNamed "A") (tSort (Universe.from_kernel_repr (Level.lProp, false) [])) (tProd nAnon (tRel 0) (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "False"); inductive_ind := 0 |} []))
: term
However, when I write:
Fixpoint is_cons_Prop (t: term) : bool :=
match t with
| tApp ( tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "and"); inductive_ind := 0 |} [] ) u => true
| tApp ( tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "or"); inductive_ind := 0 |} [] ) u => true
| tApp ( tLambda (nNamed "A") (tSort (Universe.from_kernel_repr (Level.lProp, false) [])) (tProd nAnon (tRel 0) (tInd {| inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "False"); inductive_ind := 0 |} [])) ) u => true
| => false
end.
I get the following error:
Error: Unknown constructor: Universe.from_kernel_repr.
Thus, the constructor Universe.from_kernel_repr seems to be unknown by coqtop. Where is the problem exactly ?
Btw, is there an more elegant solution where I directly use and_reif, or_reif, not_reif and so on?
Gaëtan Gilbert (Jun 30 2020 at 09:26):It's a definition not a constructor https://github.com/MetaCoq/metacoq/blob/22c7bf25bb03452dceff77264417fed702552856/template-coq/theories/Universes.v#L349
Matthieu Sozeau (Jun 30 2020 at 09:27):The problem here is that Universe.from_kernel_expr is a function and not a pattern. Maybe you can match with the normal form of the expression. Otherwise you could maybe use a wildcard pattern in this case. To use and_reif or_reif etc. you would have to swich to using (decidable) syntactic equality
Pierre Vial (Jun 30 2020 at 09:33):OK, thanks
Last updated: Oct 13 2024 at 01:02 UTC