coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] cases in leq proof
- Date: Tue, 22 Dec 2020 15:21:23 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
- Ironport-phdr: 9a23:JkQPPB9GMmZlvv9uRHKM819IXTAuvvDOBiVQ1KB30OocTK2v8tzYMVDF4r011RmVBNqdsaoYwLOM7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhjexe61+IAm5oAneq8Uan4tvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFokaxVvhyhqRx8zYDabo6aO/hxcb/GcNwAWWZMRNxcWzBPD46+aYYEEuoPPfxfr4n4v1YDsQaxChOpBOjy1DJIhnv23awi0+s7FQHJxhErEtUUv3vJttr1MbsdXPupw6nT1zrDbvdW1S346IjJbhAtu++DUq9tccfIz0QkCgzKgEmKp4P/IzOVyvoCs3Kd7+d4V++iiHAqpx9trzSxxskhlorEi5wUx17K9yh03ps4K9K4RkN5btOoDZtdui6aOYZ5Rs4vXn9ktSc4x7MJuZO2cy4Hw4kkyR7Hc/GLbpaE7xH5WOufPTt0nmxpdKihixqv7USs0u/xW8eu3FpUsyZIlsPAu3EN2hDJ98SLVOdx80G80jiVzQ/T8PtLIUUsmKrbNZEhxrkwm4IUsUTeAi/2l0L2jK6QdkUr4+So8Pjnba/6ppCGLYN7lhr+Pb4vmsy7G+g4NwkOX3SB9euiybLj4FX1QLRMjvIojqnUqI3WKdoYq6KjDQJZzpwv5wilAzu4zdgUgWELLFdfdxKGi4jpNUvOIPf9DfqnmVujjS1kx/XaMbD6HprNNWLMkLblfbpn7k5cyRYzwcpB6J1JF7ENOOjzVVPptNzEEh85NBS5zPrgCNVkz48RRWaPArKCP67Jql+J5ucvI/GWa4MPuTb9LeIl5//0gnMjl18dZ/rh4ZxCY3ehW/9iPk+xYHz2g95HH31ZkBA5SbnDhFSHGRVTY3eqVqY1rmUyBIujBq/IXYmshPqE3Tv9E5FLMDMVQmuQGGvlIt3XE8wHbzifd5c4zm40EIO5Qopk7imA8RfgwuM6fOHP8ywc85fiyJ546/CBzUhjpwwxNNyU1iS2d08xm2oJQzEs26Um/B520V6C1e59guAeGNBOtaoQD1UKcKXExuk/MOjcHwLMetDSEAShX8mpBjA3QZcq39YSagB2ANyjilbG3jbsDrMIxeSG
It's certainly a good exercise to learn
how to work with "le" proofs in a more fundamental way, but your
example falls within linear arithmetic, a decidable theory, so
there is a very simple proof.
Require Import Omega.
Theorem le_to_exist : forall n m,
S n <= m
-> exists k, S k + n = m.
Proof.
intros.
exists (m - S n).
omega.
Qed.
Theorem le_to_exist : forall n m,
S n <= m
-> exists k, S k + n = m.
Proof.
intros.
exists (m - S n).
omega.
Qed.
On 12/22/20 3:16 PM, Patricia Peratto
wrote:
I want to prove:
Theorem
le_to_exist (n m:nat)(p:le (S n) m):
exists_prop nat
(fun (k:nat)=>add (S k) n = m).
Patricia
De: "Patricia Peratto" <psperatto AT vera.com.uy>
Para: "coq-club" <coq-club AT inria.fr>
Enviados: Martes, 22 de Diciembre 2020 17:04:08
Asunto: [Coq-Club] cases in leq proof
Is there some way to make a case analisis over a proof
of a leq proposition?
Regards,
Patricia
- [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Robbert Krebbers, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Dominique Larchey-Wendling, 12/23/2020
- Re: [Coq-Club] cases in leq proof, Castéran Pierre, 12/23/2020
- Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
Archive powered by MHonArc 2.6.19+.