coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to use patterns inside proofs?

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] How to use patterns inside proofs?
Date: Wed, 15 Jul 2020 11:48:38 -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:1VzJSRDozburGTbyXaONUyQJP3N1i/DPJgcQr6AfoPdwSPT5pcbcNUDSrc9gkEXOFd2Cra4d1ayN6euxAyQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagYL5+Nhu7oRveusQSn4dpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9R/g6xbrhyvpAFxzZDIb4yOLvVyYrnQcMkGSWZdXMtcUTFKDIOmb4sICuoMJfpVr4b7p1sPthu+BQ6sBObywTJWhn/5x7E60/gmEQHexgMvAtIOsXTOo9T1KawfVvq6zKbOzTXCdPNW2TD96I3Tfx89pPGMXKh8ftDNxkU1FgPFiEydpIr4NDyayuoDqXKU7/Z8Ve2xkW4nrRl8rDaxyssxhYTEmp4ZxF/a+Clkz4g4KsG0RUp7bNOkDpddqj+WO5dqT84mTW9luig3x6EFtJO4YSQHyZYqyhDbZvGBboOG4QrjWf6MLTtmin9pYrOyihio/US+1uHxWNO43EhXoiZbitXAqGwB2hjJ5sWESvZx5Fqt1DeO2gzJ9+1JI045mKzGIJA72LEwjIAcsUHbEy/2hkr2iKiWe10h+uey6uTnZq/qqYOZN491kA3xKLghlta+AeQ+KgQOXm6b9vqg1LD74EH1XrtHguc3n6TXqpzWO9gXq6CjDwNLz4ov9Q6zDzK839QZmXkHIkhFeBWCj4XxIV7OL/b4Dfakg1SslzdrwuvLMaHkApXMNHTMiqvucax8605a0AYz18xQ54pICrEdJ/L+QlP+tNvBDhMgLwO0x/vnB85m24MFWWOPB7eZP7nIvV+J4OIvOeiMa5UPtDbzMfh2r8Lp2HQ+gBoWebSj9ZoRcnGxWPp8cGuDZn+5q9gHEHwKuQ92Z+zjlEGFSTdfZ2e7Tupo7z49CZmmCoLrTYWsxrWKmia9SM4FLltaA0yBRC+7P76PXO0BPXrLc51R1wccXL3kcLcPkBSntQv00b1id7OG8SgZ85voktlztbSKyUMCsAdsBsHY6FmjCnlulzpRFTQz3eZ2qgp8zAXbiPUqs7ljDdVWoshxfEI6OJrblrIoDtnzXkTKe9bPQV3gQ9P0WTw=

Hi;

I want to understand how to use pattern variables to manipulate expressions inside proofs. A google search did not help very much.

Let's say I have an _expression_ 2 + <bigExp> and I want to rewrite it as <bigExp> + 2. I do not want to mention <bigExp> explicitly in my proof. How do I achieve this?

Here is my attempt.

Goal 2 + (3 + 1) = 6.
Proof.
replace (2 + ?t1) with (?t1 + 2).

But it doesn't work.

--Agnishom

[Coq-Club] How to use patterns inside proofs?, Agnishom Chattopadhyay, 07/15/2020
- Re: [Coq-Club] How to use patterns inside proofs?, jonikelee AT gmail.com, 07/15/2020
- Re: [Coq-Club] How to use patterns inside proofs?, Yannick Zakowski, 07/15/2020