coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
- To: Xavier Leroy <xavier.leroy AT college-de-france.fr>, "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to organize this tricky proof?
- Date: Fri, 22 Mar 2019 13:49:46 +0000
- Accept-language: en-CA, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-BL2-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:cyY8+RPnsHqVonL90Nwl6mtUPXoX/o7sNwtQ0KIMzox0K/z6psbcNUDSrc9gkEXOFd2Cra4d06yJ6uu9BSQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagfb9+Nhe7oRjeusQWjoZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLzhSwZKzA27n3Yis1ojKJavh2hoQB/w5XJa42RLfZyY7/Rcc8fSWdHWclfSjFBApikb4QRE+UBIehWr474p1QUrBu+AxSnCOfgxzJMg3P727Ax3eY8HgHcxAEuH8wAvmnIrNv7N6kSX+K6w7XHwjjYdfxaxSvx5ZLUfhw9v/2BW697f8rLyUkoEgPIllGeppb+PzOS0OQGrnGX4OlgVeKojW4npBx6rCWvxsgyjInJiZsZwU3G+yVk3Y04ItO4R1N7Yd+lC5tcqT2WO5ZqTs45Q2Fovzo6yrgctp66eCgG0ogoxxnaa/GedYWD/xztVOGUIThihXJlfqqyhxmz8Ui8yu38S9K73ExLripClNTHq3MD1wTL58WIVvdx5EOs1SiV2w3d8O1JLkE5mbLVK5E/wbM8ip8evEHdESPqnEj7jqqbe0Q59uWm6enqZ7brqoGeOoBpjwzzMboiltGxAek+LwMARXKU+f6m273m5UD5QKtFjvkxkqTBqJ7XOcMVqrKnDwNMz4st7QizAy6h0NsDg3YLNlVFeA+bj4fyPFHOPfb4Auqlj1S0ijdrwOzGMaP9DZXRL3jDl7Hhcax6605B1Aozyddf55VXCr0bPP3zXUrxuMTZDh8/LQO03/7qBdph2o8EXW+DHLWVPa3IvVKH5+8jO+yMa5UUuDb5Jfgl/fnujXohlF8TYKap3ZoWaGumEvh6PkmVfWHhgtcGEWcWuwoxVu3qiFmYXTFPYHayWrow5isnB4K+EYfDWoetjaSd0ye8B51af3xJClSREXjzbIiEQPcNaCeKIsB7iDAEVL6hS5Ug1R60rgP6xaBnfaLo/XgovIzi2cI9w+DJkgB6oSx9EcWQySeJQntzj0sDQDsy0a9y5EBwj1mZ2K5zjrpWD4oXr7lCVR5/PprBxcR7DcrzU0TPZJ3BHF2hW5CtBSw7ZtM32d4HJUhnTYaMlBfGigijGLgT3/m5BJsy/ern33X3KIM162uOgKctj0s9GJMWbUWmgbJ6/gnXQYXOlhPKxO6Raa0A0XuVpy+4xm2UsRQdDVcpAPf1GEsHb06TluzXo0bLTrugE7Mia1ATycmeL6JLbpviilAUHa6/auSbWHq4niKLPTjN3qmFNdG4e2IB2SzcDA4PlAVBpS/bZzh7PT+opiflNBIrFV/rZB+zo89XjSvhC2UQlUSNZUAn0Kep8BkIg/DaU+kUwr8PpCYmrXNzAUq52NXVTdGHolg4cQ==
Hi Xavier,
thank you for answering.
this wouldn't work, however, because Q genuinely relies on *smaller T* in one case, where bigger P might appear; while R always relies the *same T* but smaller P (and it goes back to Q with the same T but even smaller P).
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Xavier Leroy <xavier.leroy AT college-de-france.fr>
Sent: March 22, 2019 4:41 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to organize this tricky proof?
Sent: March 22, 2019 4:41 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to organize this tricky proof?
On Thu, Mar 21, 2019 at 9:51 PM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:
Hi,
consider a type `T` and an inductively defined proposition `P : T -> Prop`. theorem `foo : forall (t : T), P t -> Q t` is proved by doing an induction on `t` and then `P t`.
however, inside of `foo`, in each case of `t`, I will need another theorem `bar : forall (t : T), P t -> R t`, which is proved by induction on `P t` and some cases require `foo`.
What about proving
Lemma foobar: forall (t: T), P t -> Q t /\ R t.
with a single induction on "P t" ? Then, "foo" and "bar" are trivial corollaries.
- Xavier Leroy
since `bar` always operate on smaller `P t` instances, so these two theorems are true, but just mutually dependent.
my problem is, I am not sure how to organize this proof to make it shorter. clearly, I can prove `bar` for each particular `t` but it pointlessly adds so much more identical proofs. On the other hand, `foo` and `bar` are not structurally mutually recursive either, because `foo` decreases on `T` while `bar` decreases on `P t`, which stops me from using Fixpoint.
Is there any way to organize the proof, so that I only need to prove `foo` and `bar` once?
- [Coq-Club] How to organize this tricky proof?, Jason -Zhong Sheng- Hu, 03/21/2019
- Re: [Coq-Club] How to organize this tricky proof?, Dominique Larchey-Wendling, 03/21/2019
- Re: [Coq-Club] How to organize this tricky proof?, Jason -Zhong Sheng- Hu, 03/21/2019
- Re: [Coq-Club] How to organize this tricky proof?, Xavier Leroy, 03/22/2019
- Re: [Coq-Club] How to organize this tricky proof?, Jason -Zhong Sheng- Hu, 03/22/2019
- Re: [Coq-Club] How to organize this tricky proof?, Favonia, 03/22/2019
- Re: [Coq-Club] How to organize this tricky proof?, Dominique Larchey-Wendling, 03/21/2019
Archive powered by MHonArc 2.6.18.