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. ?
reif_forallP_P_implies_P' shouldn't you use
tProd nAnon reif_Prop instead of
tProd nAnon reif_Type_Term ?
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
@Matthieu Sozeau can you confirm this is a bug?
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.
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?
That's pretty weird…
Maybe try in a new file? There may be something weird in the context?
I did it at the very beginning of a new file, but the error was the same :/
Théo Winterhalter said:
Matthieu Sozeau can you confirm this is a bug?
It looks like one
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?
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
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
Ok thanks ! I'll try to install it again
Last updated: May 31 2023 at 04:01 UTC