coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to use patterns inside proofs?
Date: Wed, 15 Jul 2020 13:02:46 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f178.google.com
Ironport-phdr: 9a23:eA/mxh17hIXILlPJsmDT+DRfVm0co7zxezQtwd8ZseMQKfad9pjvdHbS+e9qxAeQG9mCtbQf0aGH6ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhTexe71/IAu5oQjVqMUdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LpwRRT2lCkIKSI28GDPisxxkq1bpg6hpwdiyILQeY2ZKeZycr/Ycd4cWGFPXNteVzZZD42yb4UBEfcPM+VaoInzoFUBogexCwa3CePzyDJFnGP60Lcm3+g/FwzNwQwuH8gJsHTRtNj5OqUSUeezzKnJzjXMcfdW1inj54XTfRAhpOuDXbN0ccbL1UYvEAbFgluNooHiPTOV0eINs2mY7+V+UeKglXAophp+ojiq3Mgsi43JipgJxVDD8CV02YA4LsC3R0Bne9CrCodQtz2EOItsRMMvW31ktSknxrEbp5O2fCsHxZcoyhPBZfKKfIaG7xztWeqPLzp1hG9oda+/iRu87ESt1OPyW9e33VhEqidLktnCu3ML2hfO6caHUuNw8lm91TuLzQze6eFJLVoqmabFNZIt2KM8m5gQvEjbACP7mVn6gLKTe0k5/uWn9+Hqb7rnq5OAK4N5jx/yPb8gmsyxBOk1MQcDUHSV+em52r3j80j0QLtUgfIrkaTUtYzVKdgbq6O5BQJez5wt5AylDzi81dQVhXkHI0xBeBKAl4XpPkvBIPH8DfummlSskypny+nIPrH8AJjALWLPkLjmfbZ65E5czBQ8wcpD6JJTD7ENOPPzWknvu9zEFhI1LRC4zuL9BNh+1o4SQ3yDDrGHPK/IrFOF5OEiL/GJZIAPuTb9L/Yl5+TpjX88gVIdf66p3Z0WaHC7APtmJ1uWbmT3j9cOFGcFpAs+TOjwhFKeVj5TYm6+X7gg6TEjFIKmEYDDS5ixj7yGxSe3B4FZZmRbCl+XCnrobIWFW/IUaC2IOMNhkzoEVaKgS4A7zx2uuhX6mPJbKb/99SsZrpLk0ZBe5+TPiRYq/DB0Hs2MmzWEQGd1hWMPQhc92aE5qEc7y1HVgoZihPkNX95U4fJKXwM3OLbTyuV7D5b5XQeLNoOLT1CnQdiiDDwZQdc4wttIaEF4TYbxxivf1janVudG34eAA4Y5p+eFhyCoepRNjk3e3axktGEIB8tCMWr82Px6/gnXQpfKygCXzvn6M6sb2yHJ+SGIym/c5BgEAj41ar3MWDUkXmWTtc7wvxqQQLqnCLBhOQxEm5bbe/l6L+bxhFADf8/NfdHXYma/gWC1XE/aybaFbY6scGIYjnzQ

On Wed, 15 Jul 2020 11:48:38 -0500
Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

> 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

I do not think patterns work with "replace". They do work with
"change". Secondly, the usage of the pattern on the RHS of "with"
should not have a ?. Try "change (2 + ?t1) with (t1 + 2)."

[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