coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] cases in leq proof

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] cases in leq proof
Date: Tue, 22 Dec 2020 18:15:38 -0300 (UYT)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta04.in.vera.com.uy 1B4DD222EAD
Ironport-phdr: 9a23:hq31wx2Jbeq+BlQasmDT+DRfVm0co7zxezQtwd8ZseIUL/ad9pjvdHbS+e9qxAeQG9mCtLQe07ad6vq9EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oMhm6sQrcusYLjYd8Kqs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpVrhyhuRJxwIzbYI+IOvVxYqzdfM8aSHFbUcpNSyNOGZ+wY5cNAucHIO1Wr5P9p1wLrRamHwejHv/vyiVJhnDq3K01yfkqHxvY0ww6Bd0OrGjUrNLoP6oVSeC117HIwivZb/xMxTf99I/Ifws/of6SR7J/a9DdxlUoFwPAlFmQtIzkMiqT2+8QvGeV8/BuWvizi247tQ5xuD6vy98jh4TGhI8bxVHJ+yVkzIorJdO1SEp2bN+nHZZQsyyUN5d7TM0hTm12pSo3zqELtJy6cSUKyJoqxwLTZvOaf4WV5B/oSeWfIS9giX57ZL6zmwy+/Ee8xuHmWMS4zUxGoyVEn9XUq3wA1QLf5tKZRvZy5Eus1yuD2xrd5+1YJ00/iLDVJIQ7wrEqk5oeqUTDETHymEXxlKKWc18r+ums6+j9fLXpuIWcOJVuhg7iNaQun9azAfk4MwQWXmib//qz1KH78EHnXLlGkuc6n6bFvJzAK8kXu7S1DgBU34o77hawFTam0NAWnXkdK1JFfQqKj5DyO1HWPv/4F+2wg0iwkDds3P3GIKPuAo/XIXTZjLjherN951RByAsz1dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zFQaZOyi2YYdQHG+BPVvZUuDMlT2hdJUKW4WpAs1TeWisFCYWCJPYD7mR7kk6ysyFJ6hJZnOXInri7uEmjqqSM4FLltaA0yBRC+7P76PXO0BPXrLc51R1wccXL3kcLcPkBSntQv00b1id7GG5CACvNTo090z+vyBzEhvpwwxNNyU1iS2d08xnm4MQGZmjqV2oEg71FqZ2O5zhPkeCM0Bv6oVADd/DobVyqlBM/63QhjIJ4zbVlu8S5OtBjR3U8Njm9I=

Thank you by your help. I would like to apply inversion

to know how to manage proofs in Prop.

I get the message:

Inversion would require case analysis on sort
Set which is not allowed for inductive
definition le.

De: "Adam Chlipala" <adamc AT csail.mit.edu>
Para: coq-club AT inria.fr
Enviados: Martes, 22 de Diciembre 2020 17:21:23
Asunto: Re: [Coq-Club] cases in leq proof

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:

997646937.2536423.1608668177032.JavaMail.zimbra AT vera.com.uy">
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