The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>]

Here is a simple way without additional equalities or definitions.

Lemma rw (x := 2) (y:2=1): False.
revert x. rewrite y; intro x.

Jean-Francois

On Mon, Sep 30, 2019 at 09:17:06PM -0300, Beta Ziliani wrote:
>    You can always lift the definitional equality into a Leibniz one and
>    perform the rewrite there
>    Assert (eqx2 : x = 2) by reflexivity.
>    Rewrite y in eqxy.
>    If you need get back a definitional equality with the new term, you can
>    Pose (z := x).
>    Assert (eqxz : x = z) by reflexivity.
>    Rewrite eqxz.
>    The last step is to change x with z in the goal.
> 
>    Written from mobile. Excuse my limited communication.
>    On Mon, Sep 30, 2019, 7:51 PM Agnishom Chattopadhyay
>    
> <[1]agnishom AT cmi.ac.in>
>  wrote:
> 
>      I would think that the answer is no. x is not a propositional equality
>      in the above example. It's a definitional equality. So, I don't think
>      rewrite applies here.
>      You can't do "rewrite x in y." either, for similar reasons. The
>      [2]reference says "where eq is the Leibniz equality or a registered
>      setoid equality"
>      Note that you can prove this theorem with "inversion y.".
>      --Agnishom
>      On Mon, Sep 30, 2019 at 3:54 PM Abhishek Anand
>      
> <[3]abhishek.anand.iitg AT gmail.com>
>  wrote:
> 
>        Is there a way to rewrite in the body of a let binding in a proof
>        context:?
>        Lemma rw (x := 2) (y:2=1): False.
>          rewrite y in x. (* Error: Found no subterm matching "2" in x. *)
>        Thanks,
>        -- Abhishek

-- 
Jean-Francois Monin
Verimag
Universite Grenoble Alpes