(** * Inversion and Automation *)

(** ** 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 :=] #<br>#
[    le_n : n <= n]  #<br>#
[  | le_S : forall m : nat, n <= m -> n <= S m]
*)

Check le_ind.
(*
[le_ind] #<br>#
[    : forall (n : nat) (P : nat -> Prop),] #<br>#
[       P n ->] #<br>#
[       (forall m : nat, n <= m -> P m -> P (S m)) -> ] #<br>#
[       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.
Proof.
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.
Proof.
Admitted.

Lemma base2_odd : forall n, ~ odd n -> ~odd (S (S n)).
Proof.
(** 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.
Proof.
intro x.
intro H.
inversion H.
Qed.

End Inversion.


(** ** Automation and some goodies **)

(** Automation tactics: #<br>#
   - intuition  general #<br>#
   - firstorder general #<br>#
   - auto       first do Require Import Arith, general, also solves basic arithmetic #<br>#
   - ring       solves equations over rings, basically nat with * + 0 1 #<br>#
   - lia        first do Require Import Lia solves various kinds of equations and inequations over nat#<br>#
   - congruence solves equations between closed terms and knows that constructors are different!#<br>#
              so apply to prove  [None < > Some t]
*)


Require Import Arith.

Require Import Lia.

Lemma test_ring : forall x y z : nat, z * y + x * x *(y + z) =   y * (z + x * x) + z * x * x.
Proof.
intros x y z.
ring.
(** lia can also solve this! *)
Qed.

Lemma test_lia : forall x y z : nat, 2 * (x + y) + z <  z + 2 * x + y * 2 + 1.
Proof.
intros x y z.
lia.
(** ring cannot solve this, as it only solves equations *)
Qed.


Lemma test_intuition : forall A B C: Prop, (A -> B) /\ (B->C) -> A -> C.
Proof.
intros.
intuition.
(** tauto. also solves this; it is a complete proposition logic prover 
   for intuitionistic proposition logic *)
Qed.

Lemma test_intuition' : forall A B C D: Prop, (A -> B) /\ (B->C) -> (A \/ D) -> (C/\D).
Proof.
intros.
intuition.
(** intuition simplifies the statement, leaving the user with the
   work that's still left to do. In this case, the goal is unprovable
   so we are stuck, but in many cases this is very useful, as it does
   all the trivial logical simplifications one has to do by hand otherwise
   NB [tauto.] simply fails here
*)
Abort.



Section FirstOrder.

Variable D:Set.
Variable P Q : D -> D -> Prop.

Lemma test_firstorder: (forall x y :D, P x x -> Q x y ) -> forall x, P x x  -> Q x x.
Proof.
firstorder.
(** firstorder is an experimental extension of tauto to first order logic *)
Qed.

End FirstOrder.


(** *** Defining functions over nat by case distinction *)
Inductive tree : Set :=
  | leaf : tree
  | node : tree -> nat -> tree -> tree.

(** When inserting an element in a tree we need to distinguish#<br>#
    [n < m \/ n = m \/ m < n] #<br>#
   There are various ways (basically 3) to do that
*)

(** 1. [leb : nat -> nat -> bool] *)
Print leb.
Print Nat.leb.
Check leb.
Definition test1 (n:nat):= if leb n 3 then 7 else 0.
(* Or with nice notation *)
Definition test2 (n:nat):= if n <=? 3 then 7 else 0.


(** 2. [le_gt_dec : nat -> nat -> sumbool] *)
Check le_gt_dec.
Print le_gt_dec.
Print sumbool.
Definition test3 (n:nat):= match le_gt_dec n 3 with
| left _ => 7 
| right _ => 0
end.

(** Or in simpler notation: *)
Definition test4 (n:nat):= if le_gt_dec n 3 then 7 else 0.
(** So the if _ then _ else _ notation also works for sumbool instead of bool *)

(** 3. Nat.Compare : nat -> nat -> comparison *)
Print Nat.compare.
Check Nat.compare.
Print comparison.

(** Helper axioms to deal with nat comparisons in Coq. *)
Lemma comp_lt : 
forall n m : nat, (Nat.compare n m) = Lt -> n < m.
Proof.
intros.
(** And now what?? *)
Search Nat.compare.
(** Gives you all the basic lemmas about [Nat.compare] *)
Search "?=".
apply nat_compare_Lt_lt.
assumption.
Qed.

(** Note that [n ?= m] abbreviates [Nat.compare n m] and [n =? m] abbreviates [Nat.eqb n m] *)

(** Case distinction on [Nat.compare n m] *)
Definition ThreeChoices (n m : nat) : nat :=
  match Nat.compare n m with
    | Lt  => 0
    | Eq  => 1
    | Gt => 2
  end.

Lemma simple : forall n m : nat, ThreeChoices n m <= 2.
Proof.
intros n m.
(** And now what ?? #<br># 
   [destruct (Nat.compare n m)] doesn't work #<br>#
   [elim (nat_compare n m)] doesn't work ... *)

(** Solution: use [eqn:] to keep the equation you destruct: #<br>#
   [destruct (Nat.compare n m) eqn:Heqe.] *)

(** Alternative solution: [case_eq (Nat.compare n m).] *)
destruct (Nat.compare n m) eqn:Heqe.
unfold ThreeChoices.
rewrite Heqe.
auto.
unfold ThreeChoices.
rewrite Heqe.
auto.
(** etcetera *)
Admitted.

(** An alernative way that helps in this simple case *)
Lemma simple' : forall n m : nat, ThreeChoices n m <= 2.
Proof.
intros n m.
unfold ThreeChoices.
case (n ?= m).
- auto.
- auto.
- auto.
Qed.