Pierre Vial (Sep 08 2020 at 12:40): Pierre Vial (Sep 08 2020 at 12:40):Hi,
I'm trying to build myself the reification of the formula "2 = 1" using the reifications of 2, 1, = and nat, but I fail, seemingly because I cannot remove some tEvar which appear in the reification of =. Things work fine if I reify eq nat instead of just eq, but I would like to proceed generically. How should I do to discard tEvar while reifying eq
From MetaCoq Require Import All.
Require Import MetaCoq.Template.All.
Require Import List String.
Import ListNotations MonadNotation.
MetaCoq Quote Definition zero_reif := 0.
MetaCoq Quote Definition one_reif := 1.
MetaCoq Quote Definition two_reif := 2.
MetaCoq Unquote Definition two_unreif := two_reif. (*everything is fine *)
MetaCoq Quote Definition nat_reif := nat.
MetaCoq Quote Definition eq_reif_generic := Eval cbn in eq.
Print eq_reif_generic. (* tEvar appears in the term *)
MetaCoq Quote Definition eq_nat_reif := Eval cbn in (eq nat).
Print eq_nat_reif. (* no tEvar *)
(** Reification of 2 = 1**)
MetaCoq Quote Definition two_equal_one_reif := Eval cbn in (eq 2 1).
Print two_equal_one_reif.
(** trying to build by myselft the reification of "2 = 1" **)
Fail MetaCoq Unquote Definition try2 := (tApp eq_reif_generic [nat_reif; two_reif]).
(* The command has indeed failed with message:
inspect_term: cannot recognize (tEvar 26 []) (maybe you forgot to reduce it?) *)
Fail MetaCoq Unquote Definition try2 := (tApp eq_reif_generic [nat_reif; two_reif ; one_reif ]).
(* same fail*)
Fail MetaCoq Unquote Definition try3 := (tApp eq_reif_generic [two_reif ; one_reif ]).
(* same fail *)
I guess one should call the type checker (type inference actually) on the term in order to infer the evar number 26 must be nat.
Is there an API to call type inference on the unquoted term? Or, is there a type inference algorithm written at the meta level?
(@Pierre Vial I'm not an metacoq expert, I'm just curious)
Pierre Vial (Sep 08 2020 at 13:16):@Enrico Tassi In the end of Section 2.1 of the MetaCoq project file, it is said that tEvar is not handled yet. Although it dates back to an older version of MetaCoq, I was hoping that there would be a hack to avoid having tEvar popping up
Pierre Vial (Sep 08 2020 at 13:17):Well, actually, reifying @eq instead of eq does the job (should have thought of it myself rightaway), but I would still be interested to know if one may call type inference
Théo Winterhalter (Sep 08 2020 at 13:55):Right now, we cannot call the inference algorithm of Coq no. @eq is indeed the _official_ way to go. Generally speaking we do not handle evars yet.
Last updated: May 31 2023 at 11:01 UTC