The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Patricia,

Here are some possible low-level proofs for you are asking.

Notice that you can directly proceed by induction on S n <= m,

you have to generalize the result to the case of n <= m instead.

The only result imported from StdLib is plus_comm

which you can also show by two (nested) inductions.

Best,

Dominique

------

Require Import Arith.

Theorem le_plus n m : n <= m -> exists k, k+n = m.

Proof.

  induction 1 as [ | m H IH ].

  + exists 0; trivial.

  + destruct IH as (k & Hk).

    exists (S k).

    rewrite <- Hk; trivial.

Qed.

Theorem S_plus_comm k n : S k + n = k + S n.

Proof.

  do 2 (rewrite (plus_comm k); simpl).

  trivial.

Qed.

Theorem le_to_exist n m : S n <= m -> exists k, S k + n = m.

Proof.

  intros H.

  destruct le_plus with (1 := H) as (k & Hk).

  exists k; rewrite <- Hk.

  apply S_plus_comm.

Qed.

---

De: "Patricia Peratto" <psperatto AT vera.com.uy>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mardi 22 Décembre 2020 22:15:38
Objet: Re: [Coq-Club] cases in leq proof

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:

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