I want to write something like the following, but I get Error: Cannot infer the implicit parameter A of eq_refl whose type is "Type".
. It should be possible to infer all of the implicit arguments to eq_refl
because:
my_refl _
is matched against the my_refl x
appearing in the goal.my_refl x
is x = x
.my_refl x
for should have the same type, so we should be trying to elaborate eq_refl : x = x
, which is fine.How can I convey part 3 to Coq (without explicitly writing the type x = x
in my script)?
Definition my_refl {A} (x : A) : x = x := eq_refl.
Parameter A : Type.
Parameter x : A.
Goal my_refl x = eq_refl.
change (my_refl _) with eq_refl.
Here's the best I can come up with:
Definition my_refl {A} (x : A) : x = x := eq_refl.
Parameter A : Type.
Parameter x : A.
Goal my_refl x = eq_refl.
evar (ty : Type).
set (foo := my_refl _ : ty).
subst foo.
change (my_refl _) with (eq_refl : ty).
Or to not subst foo.
and instead change foo with (eq_refl : ty).
. It seems strange that change
doesn't just do this, though, and I also think there must be a way that's a little more direct.
or
set (foo := my_refl _);
let ty := type of foo in
let bar := open_constr:(eq_refl) in
let ty' := type of bar in
unify ty ty';
change foo with bar;
clear foo.
Can I extract this as an Ltac
definition (for arbitrary unelaborated terms instead of my_refl _
and eq_refl
)?
Aha, Tactic Notation
with uconstr(...)
arguments. Thanks!
James Wood has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC