(** * Binary Trees of natural numbers *)

(** We define the type of binary trees 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.

(** We 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.
  
(* We 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 ultra 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)].
   - 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.


(** Now define the function 'mirror' that return a mirror
   image of a tree. #<br>#
   For instance:
 <<   
               a              a
             /   \          /   \
   mirror(  b     d   ) =  d     b
      	    \    /\       /\    /
	          c   e  f     f e    c
>>
*)

Fixpoint mirror (T : nat_tree) : nat_tree :=
  match T return nat_tree with 
  | leaf => leaf 
  | node l n r => node (mirror r) n (mirror l) 
  end.
  
(** We check this function on the example presented above *)
   
Lemma mirror_ex : forall a b c d e f,
  mirror (node
      (node leaf b (node leaf c leaf)) 
      a
      (node (node leaf e leaf) d (node leaf f leaf))) =
  node
    (node (node leaf f leaf) d (node leaf e leaf))
    a
    (node (node leaf c leaf) b leaf).

Proof.
intros.
unfold mirror.
reflexivity.
Qed.

(** Now prove that taking mirror image of a tree
   twice returs the original tree. *)
    
Lemma mirror_double : forall T, mirror (mirror T) = T.
Proof.
Admitted.

(** Now prove that an element belong to a mirror
   image of a tree if and only if it belongs to the 
   tree itself. *)
   
(** Hint: to see how the iff ([<->] connective is defined 
         in Rocq try [Print iff.] You can also do 
	 [unfold iff] within the proof. *)
   
Lemma mirror_In_l : forall n T, In n T -> In n (mirror T).
Proof.
intro n.
induction T.
- simpl. auto.
- intro H.
  simpl.
  simpl in H.
  repeat destruct H.
(** or  [destruct H as [H0 | [H1 | H2]].] *)
  + right. right.
    apply IHT1; auto.
  + right; left.
    auto.
  + left.
    apply IHT2; auto.
Qed.

Lemma mirror_In_r : forall n T, In n (mirror T) -> In n T.
Proof.
intro n.
induction T.
- intro H. simpl in H ; contradiction.
- simpl. intro H.
  simpl in H.
  destruct H as [H0 | [H1 | H2]].
  + right ; right ; apply IHT2 ; exact H0.
  + right ; left ; exact H1.
  + left ; apply IHT1 ; exact H2.
Qed.

Lemma mirror_In : forall n T, In n T <-> In n (mirror T).
Proof.
(** combine [mirror_In_l] and [mirror_In_r] *)
intros.
unfold iff.
split.
- apply mirror_In_l.
- apply mirror_In_r.
Qed.

(** Now define a function [tree_sum] that given a
   tree returns the sum of all the elements in the tree *)

Fixpoint tree_sum (t: nat_tree) := 
match t with
| leaf => 0
| node t1 n t2 => (tree_sum t1) + (tree_sum t2) + n 
end.

(** Check it on some input *)
Require Import Lia.
Lemma tree_sum_ex : forall a b c d,
  tree_sum (node (node leaf a leaf) b (node (node leaf c leaf) d leaf)) =
  a + b + c + d.  
Proof.
intros.
simpl.
lia.
Qed.

(** Now prove that the sum of the elements in the
   mirrored tree is the same as in the original one *)
   
Lemma mirror_tree_sum : forall T, tree_sum T = tree_sum (mirror T).
Proof.
Admitted.