Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] cases in leq proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] cases in leq proof


Chronological Thread 
    < Chronological >      < Thread >
  • 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.

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



Archive powered by MHonArc 2.6.19+.

Top of Page