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: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <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 21:38:27 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
Ironport-phdr: 9a23:k/niyh1osOwBIZlWsmDT+DRfVm0co7zxezQtwd8Zse0fIvad9pjvdHbS+e9qxAeQG9mCsLQY0KGN7+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVijexe7x/IRu5oQjfucQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LpwRRT2lCkIKSI28GDPisxxkq1bpg6hpwdiyILQeY2ZKeZycr/Ycd4cWGFPXNteVzZZD4yzYYsADeoPM+hboYfguVUBsQCzChOwCO710DJEmmP60K883u88EQ/GxgsgH9cWvXnJstr1KL0dWv22w6nJyTXDbulZ2TH86IPVdR0uuu+DXa5qfsfKzEkvDwLFgkyLqY3rJDOZzOMNs3KU7+d5U++klmApqwZ0oje1x8csjJHEiZ4SylDe8yV23oI1JdmiREFlfNGkDZ1dvDyZOYtuWs4uXm9ltSIgxrEbvZO3ZisHxZU9yxLCa/GLa5aE7g7nWeqLIjp1hGhpdKyiixqu60StxePxW8+p21hQtCVFiMPDtnUV2hzT9MeHTvx981+j2TaSzwDT6/1ELl4ulabBLp4h2r8wmoMQsUTHBS/5g1/6jKqOdkUr4OSn9vrobq3npp+aKYB0lhnzPrkgl8G7G+g0LwwDU3KY9Om9zrHv4E30TK1PjvIsk6nZtJ7aJd4cpq68GwJayZgs6wqlADq91dQYhXgHIEteeBOJlIjlIVbOIOr3DfunmVSjjC9rx+zaPr3mGpjCMn/DkK74cblh705c1RE8wMtE55NUD7EBOOj8VlXwtNzeFB85Mha7z/zpCNVnhcsiXjekBbbRG6fPuxfc7eU2ZuKIeYU9uTDnKvFj6eS43lEjnlpIV6S11NMlaXS5F/JnaxGTbGblqtIZECIRoRF4S/bl3g7RGQVPbmq/CvpvrgowD5irWMKaHtj03e6xmRyjF5gTXVhoT1CBFXCyKteGRu8NdC+IZMp5k3kHUaOrDYo52leiuV2ikus1Hq/v4iQd8Knb+p1w7uzXmws18GUvXcGF0iSWUHoymXkHFWZvgPJP5Hdlw1LG6pBWxuRCHIUItfZRU0IhKoWayPZ1WYj/

The following creates a new variable z that is equal to x and has the new definition you want:

Lemma rw (x := 2) (y:2=1): x = 1.
  assert (x2: x = 2) by reflexivity.
  rewrite y in x2.
  pose (z := 1).
  assert (eqxz: x = z).
    rewrite x2. reflexivity.
  rewrite eqxz.
  reflexivity.
Qed.

On Mon, Sep 30, 2019 at 5: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