Pierre Vial (Jun 10 2020 at 15:19): 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. ?
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 ?
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
Théo Winterhalter (Jun 10 2020 at 15:33):@Matthieu Sozeau can you confirm this is a bug?
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.
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?
Théo Winterhalter (Jun 12 2020 at 08:10):That's pretty weird…
Chantal Keller (Jun 12 2020 at 13:27):Maybe try in a new file? There may be something weird in the context?
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 :/
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
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?
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
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
Pierre Vial (Jun 12 2020 at 14:51):Ok thanks ! I'll try to install it again
Last updated: May 31 2023 at 04:01 UTC