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: Jason Gross <jasongross9 AT gmail.com>
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:16:54 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f44.google.com
Ironport-phdr: 9a23:7g2QBhDh6PKTXRwLxLveUyQJP3N1i/DPJgcQr6AfoPdwSPv8oMbcNUDSrc9gkEXOFd2Cra4d0KyK6Ou7CSQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+Nhq7oAveusQYgoZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9R/g6JVoh2vpxJxzY3Jbo+LKPVzZbnScc8ASGdbQspdSy5MD4WhZIUPFeoBOuNYopH5qVQUthu+Ag+sD/7uxD9SgX/2xrY62PkmHAHExgMgBNUOsHLbrNXvM6cSSvu1wa3TwDXMavNZwzb96IzSfh89pvGMWKt9fMzMwkchEAPFi0+fqY3jPz6NyusNtHKb7+x+WuKrj24rsR9+rSWyxss0hYnJh54VylDZ9Spi2oo6Odq4SEt9bNW5E5VQrzmXO5VqTs4mWW1luyY3xqcYtZKnfyUG0psqyhHZZveaaYaH+AjjW/yUITpghHJqZra/hxGq/Eil0OL8V8203E9UoSVYj9XAr34N2hPc58SdRft9+UCh2TmL1w/N8O1LPUc0la/DJ54gxL4/iIYTvFzdEiPqnEj6lqybe0U+9uS29+jqYa/qq5CTOoNsjwHxKKUumsixAeQiNQgOWnCW+eam2734+k35RrpKjucxkqnCq5DXId8WpqG8AwBP04Yj7wyzACuh0NQdhXUHNk5KeAqbj4j1PFHDOOz3DfCmg1i1jDhrw+3GMab6D5XWLnnDla/hcqxn505dzgoz19Ff6IhOBrEPOvKgEnP24dffF1oyNxG+i7LsD8w43YcDU0qOBLWYOeXcqwnbyPgoJryubZQSvn7SMf8+/La6j3YinlkSZ66yxso/Z3WxH/AgKEKcNym/yuwdGHsH61JtBNfhj0ePBGYKNiSCGpkk7zR+M7qISILKR4SjmruEhX7pEZhfZ2QAAVeJQy6xK9e0HswUYSfXGfdP1yQeXOH4GYAk3BCq8gT9zug/d7eGymgjrZvmkeNNyajTmBU1r2EmCs2c1ySAQzgxkD9UATAx2697rAp2zVLRiaU=

If you `Rewrite Import ssreflect`, then `rewrite y in x` works and does what you want. So ssr rewrite can handle what you want. Note also that there is a long-standing bug report about this (from 2012): https://github.com/coq/coq/issues/2911

On Mon, Sep 30, 2019 at 8:39 PM Beta Ziliani <beta AT mpi-sws.org> wrote:

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