The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

Dear Patricia,

A good way to get familiar with inversion is to prove some simple  properties of le with and without this tactic.

First, with a plain destruct, we prove an « Inversion lemma »:

Lemma le_inv : forall n p,  n <= p -> n = p \/ exists k, p = S k /\ n <= k.

Proof.

  intros n p  H; destruct H.

  - left; trivial.     

  - right; exists m; split; trivial.

Qed.

Then the analysis of some hypotheses like n <= 0, or S.n <= S p can be done using le_inv:

Corollary le_n_0: forall n, n <= 0 -> n = 0.

Proof.

  intros n H; destruct (le_inv n 0 H).

  - assumption.

  - destruct H0 as [k [H1 _]]; discriminate.

Qed.

With inversion :

Lemma  le_n_0': forall n, n <= 0 -> n = 0.

Proof.

  intros n H; inversion H; trivial.

Qed.

As an exercise, you can prove (forall n p,  S n <= S p -> n <= p)  the same ways.

(Note you will probably have to apply the transitivity of le).

On this example, you will notice that inversion often uses discriminate and injection.

With some practice, you will know easily when to use induction or inversion, according to the context.

Pierre

P.S.

  On which goal did you obtain this error message ?

Le 22 déc. 2020 à 22:15, Patricia Peratto <psperatto AT vera.com.uy> a écrit :

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