The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi,

I have an idea. You can take the advantage of the fact that all well-formed terms in Coq must have types, and that will enforce unification.

Ltac unify_by t1 t2 :=

  let t := constr:(eq_refl : t1 = t2) in

  match type of t with

  | _ = ?t => t

  end.

Tactic Notation "my" "change" constr(t1) "with" uconstr(t2) :=

  let t := unify_by t1 t2 in

  change t1 with t.

It at very least handles your example.

Goal @inr bool _ (1 + 1) = inr 2.

Fail change (@inr bool _ (1 + 1)) with (inr 2).

(* The command has indeed failed with message:

Cannot infer the implicit parameter A of inr whose type is "Type". *)

my change (@inr bool _ (1 + 1)) with (inr (2 * 1 + 0)). (* this works *)

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of John M Grosen <jmgrosen AT mit.edu>
Sent: February 27, 2019 6:34 PM
To: coq-club AT inria.fr
Subject: RE: [Coq-Club] change uses inferior type inference

 

Try using Tactic Notation's uconstr for untyped terms:

Tactic Notation "changee" uconstr(a) "with" uconstr(b) :=
  assert (a=b) as XX by reflexivity;
  rewrite XX;
  clear XX.

Goal inr true = inl 5.
  changee (inr true:(nat+bool)) with (inr (negb false)). (* succeeds *)

--
John
________________________________________
From: coq-club-request AT inria.fr [coq-club-request AT inria.fr] on behalf of Abhishek Anand [abhishek.anand.iitg AT gmail.com]
Sent: Wednesday, February 27, 2019 3:26 PM
To: coq-club
Subject: Re: [Coq-Club] change uses inferior type inference

Here is a minimal example to illustrate the problem:

assert (inl 2 = inr true). (* succeeds *)

change (inr true:(nat+bool)) with (inr true). (*  Cannot infer the
implicit parameter A of inr ...*)


-- Abhishek
http://www.cs.cornell.edu/~aa755/


On Wed, Feb 27, 2019 at 3:18 PM Abhishek Anand
<abhishek.anand.iitg AT gmail.com> wrote:
>
> Many times, the following tactic succeeds:
>
> assert (a=b) by reflexivity.
>
> but the following fails with some type inference error suggesting that
> while inferring types, Coq is not exploiting the fact that `a` and `b`
> must have the same types:
>
> change a with b
>
> Can the `change` tactic be made as smart as `assert (_=_)`?
>
> I thought the following Ltac would work, but it suffers from the same
> problem as `change`.
>       Ltac changee a b :=
>         assert (a=b) as XX by reflexivity;
>         rewrite XX;
>         clear XX.
>
> I guess terms are fully typed before being passed to Ltac.
>
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/