Stream: Coq users

Topic: ✔ change with checked type

James Wood (Aug 09 2022 at 10:03):

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:

1. my_refl _ is matched against the my_refl x appearing in the goal.
2. The type of my_refl x is x = x.
3. The thing I'm changing 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.

James Wood (Aug 09 2022 at 10:28):

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).

James Wood (Aug 09 2022 at 10:32):

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.

Gaëtan Gilbert (Aug 09 2022 at 10:41):

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.

James Wood (Aug 09 2022 at 11:05):

Can I extract this as an Ltac definition (for arbitrary unelaborated terms instead of my_refl _ and eq_refl)?

James Wood (Aug 09 2022 at 12:31):

Aha, Tactic Notation with uconstr(...) arguments. Thanks!

Notification Bot (Aug 09 2022 at 12:31):

James Wood has marked this topic as resolved.

Last updated: Apr 19 2024 at 13:02 UTC