coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewrite in the body of a let binding in a proof context

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] rewrite in the body of a let binding in a proof context
Date: Mon, 30 Sep 2019 17:51:00 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:g1hPnhCX3gfqa07XzjxDUyQJP3N1i/DPJgcQr6AfoPdwSPvyo8bcNUDSrc9gkEXOFd2Cra4d0KyK6Ou5ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+Nhq7oAveusULnIdpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9R/g6JVoh2vpxJxzY3Jbo+LKPVzZbnScc8ASGdbQspdSy5MD4WhZIUPFeoBOuNYopHhqlsBqxu+BBKsBOPoyj9Nm3T7w6063P49EQHa2wwgB8gBv2nUrNT1LqgTUf2+wa7SwjXMafNW2Cz96IjPchAkuvyDQbdwccvLxUY1CwzJlFSQqYr8Mj6Ty+8DvW+b7+96WuKujW4qsx1+oj+1xscqlIbJgoYVxkra+ipk3YY5Pdy4SEhhYd6lCpRcrS+aN5FwT8g/QG9ooD43xqAYtZO1ZiQHyZoqywTBZ/CbfYWE+AzvWPuPLTtgmn5pZLayiwyx/EWg0OHwS8i53VdQoidKjNXBsG0G2QbJ5cidUPR9+1+s2TaR2ADX7eFJOUU0mrDaK54l2LI/ip8TsUXZEiDshEr6lq6WdkM89uip7eTofKnmq4eBO4NqhAzyKKUjl8KlDegmLgQDUXKX9fqh2LH95UH5Ra9FjvwykqnXqpDaIsEbq7ajDA9a1IYj6g2/Dzeh0NQdhnQIMFdFeBOdg4fzJ17COvH4DfGnj1S2jDhr3+zGPqHmApjVMnfDl67hca9h5E5Y1Qo81stS54lUC7EEOPL8QFX9tN3eDh8jMgy72fzrCNtn1tBWZWXaCaiAdajWrFWg5+Q1IuDKapVGliz6Lq0M6Pjvln8+nBc2faC1wZwPYXy4D/13axGQbnztmdcGFE8Buwt4ReesiVvUAm0bXGq7Q69pvmJzM4mhF4qWHtn80ozE5z+yG9htXk4DD1mNFXnycIDdAqUHbSPUK8QnkzpWDOH8Gb9k7gmnsUrB85QiLufQ/XRG55fq1dwz7OjS0xg5sz1yXZzEjzO9Clpsl2ZNfAcYmbhlqBUkmFyG0O5xiLpZE44L6g==

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 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 <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
http://www.cs.cornell.edu/~aa755/

Re: [Coq-Club] rewrite in the body of a let binding in a proof context, Agnishom Chattopadhyay, 10/01/2019
- Re: [Coq-Club] rewrite in the body of a let binding in a proof context, Beta Ziliani, 10/01/2019
  - Re: [Coq-Club] rewrite in the body of a let binding in a proof context, Jean-Francois Monin, 10/01/2019
- <Possible follow-up(s)>
- Re: [Coq-Club] rewrite in the body of a let binding in a proof context, Beta Ziliani, 10/01/2019
  - Re: [Coq-Club] rewrite in the body of a let binding in a proof context, Jason Gross, 10/01/2019