The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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/