The Coq mailing list

[John M Grosen <jmgrosen AT mit.edu>]

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/