coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] rewrite in the body of a let binding in a proof context
Date: Mon, 30 Sep 2019 13:53:34 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f43.google.com
Ironport-phdr: 9a23:RBMgGRw8XvIu9rLXCy+O+j09IxM/srCxBDY+r6Qd2+oVIJqq85mqBkHD//Il1AaPAdyAra4ewLOK4+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVijexe7x/IAu5oQnMucQbgpZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8N/jKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMMPpDoIn9plsOthu+ChevBOjy1jJIgGX53asn3O88FgzJxhcvH9IPsHTPrNX6KqQSXfqvw6nO1zrDae5Z1S386IjJbhAhruqBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvWac7+plT+2vimgnphltrTio3McsjJfGhoYRylze6yp23Zs1KNulQ0B4ed6pCIVcuz2eOodsQc4vQ3tktDs7x7AHo5K2cyYHxZI6zBDFcfOHaZKH4hf7WeaRPzh4gHVldaq6hxmo8EigzvTwVsiz0FpXtyZFnNbBu34X2xzc7ciHTfR9/kO/1jqVyw/T7eRELVg1lardNZEh3qY9moQPvUnHBCP7m0X7gLWLekgl++Wk8evqb7v+qp+ZLYB0iwX+Mqo0msy4BOQ1KhIBUHOb+eS9z73j/VP2QLZQgvIslKnWqpbaKtkBqq64Ag9Vzokj5g2wDzejytsYnH0HIEhZdxKAiojlI0vOL+zgDfejn1Ssly9myOzBPr34G5nCMnzDkKr6crtm8E5dyA8zzchF6J5OC7EBJujzWk7ru9DCAB85KV/8/+GyA9Jkk4gaRGjHVqSeKebZtUKCzuMpOeiFIoEP7mXTMf8gstfkjX4imVIeNYCv1J0bICSxFPRnOEWUYjzlhN4HHSELvxYxZOPvgVyGFzVUYiDhDOoH+jgnBdf+Xs/4TYe3jenZhXrpLthtfmlDT2u0PzLoeoGDAapebSuTJopglWVBW+T6DYAm0h6quUnxzL81drOFqB1djorq0Z1O38OWkBgz8TJuCMHEijOCSmh1miUDQDpkhfkj83w48U+K1O1Du9IdDcZavqobXQIzNJqaxOt/WYj/

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/

[Coq-Club] rewrite in the body of a let binding in a proof context, Abhishek Anand, 09/30/2019