An impredicative définition of <= on nat

Consider the following definition : 
Require Arith.

Definition my_le (n p:nat) :=
  forall P:nat->Prop,
    P n ->
    (forall q:nat, P q -> P (S q)) ->
    P p.
Prove the following theorems : 
Lemma my_le_n : forall n:nat, my_le n n.
Lemma my_le_S : forall n p:nat, my_le n p -> my_le n (S p).
Lemma my_le_inv : forall n p:nat, my_le n p ->n=p \/ my_le (S n) p.
Lemma my_le_inv2 : forall n p:nat, my_le (S n) p ->
                     exists q, p=(S q) /\ my_le n q.
Lemma my_le_n_O : forall n:nat, my_le n (0) -> n=0.
Lemma my_le_le : forall n p:nat, my_le n p -> le n p.
Lemma le_my_le : forall n p:nat, le n p -> my_le n p.

Hints

In order to get comfortable with the definition of my_le, you should try to prove manually some simple inequalities, like (my_le 0 2), (my_le 1 3), etc.
You should also print and look at the proof terms for all the theorems you prove. It will make you understand how my_le works.

Solution

See file le_impred.v

Going home
Pierre Castéran