Stream: MetaCoq

Topic: Mismatch about printed name of a constructor


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre Vial (Jun 30 2020 at 09:33):

OK, thanks


Last updated: Aug 11 2022 at 03:02 UTC