Stream: MetaCoq

Topic: Unquote and quote does work using Prop


view this post on Zulip Pierre Vial (Jun 10 2020 at 15:19):

Hello again,

I'm meeting a problem while unquoting something that I've just quoted that may be a bug.
I'm using coq.8.11.0 on Vscoq.

Definition mkImpl (A B : term) : term := (* comes from demo.v in the repo*)
   tProd nAnon A B.

Quote Definition reif_forallP_P_implies_P := Eval compute in (forall (P:Prop), P ->P ).
Make Definition uq_reif_forallP_implies_P := reif_forallP_P_implies_P.

The Make Definition outputs the following error:

The term "forall P : Prop, P -> P" has type "Type" while it is expected to have type "Prop".

Likewise, when I try to build the reification of forall (P : Prop), P -> P. :

Quote Definition reif_Prop := Eval compute in Prop.

Definition reif_forallP_P_implies_P' := tProd nAnon reif_Type_Term (mkImpl  (tRel 0) (tRel 0)).

Make Definition uq_reif_forallP_implies_P' := trad_works_Prop.

This time, the Make Definition raises the following (different) error:

Anomaly "Not a sort." Please report at http://coq.inria.fr/bugs/.
Not in proof mode.

When I print reif_Prop, I obtain,

reif_Prop = tSort (Universe.make'' (Level.lProp, false) [])
    : term

So, what is wrong and how should I unquote (the reification of) forall (P : Prop), P -> P. ?

view this post on Zulip Kenji Maillard (Jun 10 2020 at 15:27):

In reif_forallP_P_implies_P' shouldn't you use tProd nAnon reif_Prop instead of tProd nAnon reif_Type_Term ?

view this post on Zulip Pierre Vial (Jun 10 2020 at 15:30):

Huh, yes, sorry, here is the right code:

Definition reif_forallP_P_implies_P' := tProd nAnon reif_Prop (mkImpl  (tRel 0) (tRel 0)).

Make Definition uq_reif_forallP_implies_P' := reif_forallP_P_implies_P'.

but I still get the same error message

view this post on Zulip Théo Winterhalter (Jun 10 2020 at 15:33):

@Matthieu Sozeau can you confirm this is a bug?

view this post on Zulip Théo Winterhalter (Jun 11 2020 at 18:08):

Wait can you try with just

From MetaCoq Require Import All.

Quote Definition reif_forallP_P_implies_P := Eval compute in (forall (P:Prop), P ->P ).
Make Definition uq_reif_forallP_implies_P := reif_forallP_P_implies_P.

For me it works with no errors.

view this post on Zulip Pierre Vial (Jun 11 2020 at 18:19):

I just did. I still get:

The term "forall P : Prop, P -> P" has type "Type" while it is expected to have type "Prop".
Not in proof mode.

but perhaps it is related to opam installation then?

view this post on Zulip Théo Winterhalter (Jun 12 2020 at 08:10):

That's pretty weird…

view this post on Zulip Chantal Keller (Jun 12 2020 at 13:27):

Maybe try in a new file? There may be something weird in the context?

view this post on Zulip Pierre Vial (Jun 12 2020 at 13:48):

I did it at the very beginning of a new file, but the error was the same :/

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 14:09):

Théo Winterhalter said:

Matthieu Sozeau can you confirm this is a bug?

It looks like one

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 14:10):

Maybe we're not talking about the same version of MetaCoq though, if it works for Théo. @Pierre Vial what does your opam list say?

view this post on Zulip Pierre Vial (Jun 12 2020 at 14:12):

It gives me this:

base-bigarray            base
base-threads             base
base-unix                base
camlp5                   7.11          Preprocessor-pretty-printer of OCaml
conf-findutils           1             Virtual package relying on findutils
conf-m4                  1             Virtual package relying on m4
coq                      8.9.1         Formal proof management system
coq-equations            1.2.1+8.9     A function definition package for Coq
coq-metacoq              1.0~alpha+8.9 A meta-programming framework for Coq
coq-metacoq-checker      1.0~alpha+8.9 Specification of Coq's type theory and re
coq-metacoq-erasure      1.0~alpha+8.9 Implementation and verification of an era
coq-metacoq-pcuic        1.0~alpha+8.9 A type system equivalent to Coq's and its
coq-metacoq-safechecker  1.0~alpha+8.9 Implementation and verification of safe c
coq-metacoq-template     1.0~alpha+8.9 A quoting and unquoting library for Coq i
coq-metacoq-translations 1.0~alpha+8.9 Implementation and verification of an era
num                      1.3           The legacy Num library for arbitrary-prec
ocaml                    4.09.0        The OCaml compiler (virtual package)
ocaml-base-compiler      4.09.0        Official release 4.09.0
ocaml-config             1             OCaml Switch Configuration
ocamlfind                1.8.1         A library manager for OCaml

I'm a bit surprised, because opam switch tells me that I'm using my coq.8.11.0 switch

view this post on Zulip Matthieu Sozeau (Jun 12 2020 at 14:23):

Hmm, yep it looks like you coq.8.11.0 switch has coq 8.9. So you might be seeing a bug in an old version of metacoq

view this post on Zulip Pierre Vial (Jun 12 2020 at 14:51):

Ok thanks ! I'll try to install it again


Last updated: Aug 11 2022 at 02:03 UTC