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?

It's a definition not a constructor https://github.com/MetaCoq/metacoq/blob/22c7bf25bb03452dceff77264417fed702552856/template-coq/theories/Universes.v#L349

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

OK, thanks

Last updated: Jun 23 2024 at 01:02 UTC