(* Various Examples of Programming and Proving in Coq III *)

(** Inversion **)

Section INVERSION.

Lemma inject_nat : forall n m :nat, S n = S m -> n = m.
Proof.
intros n m Heq.
inversion_clear Heq.
reflexivity.
Qed.

Print le.

(* 
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n 
  | le_S : forall m : nat, n <= m -> n <= S m
*)

Check le_ind.
(*
le_ind
     : forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, n <= m -> P m -> P (S m)) ->
       forall n0 : nat, n <= n0 -> P n0 
*)

Lemma basic1 :forall n : nat, le n 0 -> n = 0.
Proof.
induction n.
auto.
intro H.
(* And now what?? *)
inversion H.
(* inversion analyses the possible cases for H; 
   there is none (!), because the types of le_n and le_S don't match on the type of H,
   so the type "S n <= 0" is empty, so we can conclude everything, and we have a proof of S n = 0 *)
Qed.

(* Different proof of the same lemma 
   There is no need to do an induction on n *)
Lemma basic2 :forall n : nat, le n 0 -> n = 0.
Proof.
intros n H.
inversion H.
(* only le_n can be a proof of n <= 0 *)
(* NB inversion_clear H removes all superfluous hypotheses 
   from the context *)
auto.
Qed.

(* Here you see what hypotheses inversion creates *)
Lemma explain_inversion : forall R : nat -> nat -> Prop, forall n m : nat, le n m -> R n m.
Proof.
intros R n m H.
inversion H.
(* inversion has created two goals, one for each case of the constructor of <= 
   To see the second goal: *)
Show 2.
Abort.

Inductive even : nat -> Prop :=
| even_O : even O
| even_S_S : forall n, even n -> even (S (S n)).

Print even.

Lemma base1_even : ~ even 1.
intro H.
inversion H.
Qed.

Lemma base3_even : ~ even 3.
Proof.
intro H.
inversion_clear H.
inversion H0.
(* also try:
   simple inversion H.
   inversion H0.
   inversion H1.
   intros H3.
   inversion H3. *)
(* If you want to really understand what inversion H1 does here:
   - it applies even_ind with 
     P:= fun n:nat => n=1 -> False
   - It then does all kinds of simplifications on the constraints
     to solve the goal
   To see only the first step at work, do
     simple inversion H.
     Show 2. (to see the second goal that "simple inversion H" has created
*)
Qed.


Lemma base2_even : forall n, ~ even n -> ~even (S (S n)).
(* Prove using inversion_clear *)
Admitted.

Inductive odd : nat -> Prop :=
| odd_1 : odd 1
| odd_S_S : forall n, odd n -> odd (S (S n)).

Lemma base1_odd :  ~ odd 0.
Admitted.

Lemma base2_odd : forall n, ~ odd n -> ~odd (S (S n)).
(* Prove using inversion_clear *)
Admitted.

Print option.
Lemma option_eq : forall x y : nat, Some x = Some y -> x =y.
Proof.
intros x y H.
inversion H.
(* This derives x=y from Some x = Some y, 
   which holds because Some is a constructor *)
reflexivity.
Qed.

Lemma option_eq1 : forall x : nat, Some x <> None.
intro x.
intro H.
inversion H.
Qed.

End INVERSION.