(* Exercise coq_tree_01 *)

(* Let us define binary tree of natural numbers.
   Such a tree is either a leaf, or an internal
   node with some natural number and two subtrees. *)
Inductive nat_tree : Set :=
  | leaf : nat_tree
  | node : nat_tree -> nat -> nat_tree -> nat_tree.

(* Now let us define the 'In n T' predicate that returns
   a proposition indicating whether a tree 'T' contains 
   a natural number 'n' *)
Fixpoint In (n : nat) (T : nat_tree) {struct T} : Prop :=
  match T with
  | leaf => False
  | node l v r => In n l \/ v = n \/ In n r
  end.
  
(* Now let us prove that if an element 'n' belongs to
   this particular tree:
   
       b
      /
     a

   then 'n' either equals 'a' or 'b'. *)

Lemma tree2_In : forall n a b, 
  In n (node (node leaf a leaf) b leaf) ->
  n = a \/ n = b.
  
Proof.
(* Here is the ultar short proof script: [Note that these script are always constructed after
   having first constructed a longer one!] *)
intros n a b [[H1 | [H2 | H3]] | [H4 |H5]]; try contradiction;auto.
(* Some comments:
   - ; composes two tactics  
       T1;T2 means that T2 is applied to _all_ subgoals that are generated by T1
   - try T  tries tactic T1 on the goal and does nothing if T1 fails
     this is different from just "T1", because T1 may fail, but "try T1" never fails
   - auto solves quite a few goals by itself 
   - intros [[H1 | [H2 | H3]] | [H4 |H5]] does an intro _and_ a destruct
     Basically: if the goal is forall h:A, B and A is an inductive type with two constructors, 
     = you can type "intros h; elim h; intro H1 " etc (later: intro H2)
     = you can type "intros h; destruct h as [H1 | H2] " etc
     = you can type "intros [H1 | H2]"
     The latter is what I am doing here, taking full advantage of the unfolded shape of 
     In n (node (node leaf a leaf) b leaf)Qed.
   - The clue of the exercise is a bit hidden in my script, because intros does the unfolding
     of the definition of In (and the computation) by itself
*)
Qed.

Lemma tree2_In' : forall n a b, 
  In n (node (node leaf a leaf) b leaf) ->
  n = a \/ n = b.
  
Proof.
(* Here is the longer proof script that I had first created *)
intros n a b H.
simpl in H.
  (* This unfolds the definition of In and therefore computes the normal of the type of H *)
elim H.
intro H1.
elim H1.
intro H2.
contradiction.
intro H3.
elim H3.
intro H4; left; symmetry; assumption.
intro H5;contradiction.
  (* Now I am glueing things together a bit: *)
intro H6; elim H6; try contradiction; try (right; symmetry; assumption).
Qed.