(** * 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.
Admitted.

Lemma mirror_In_r : forall n T, In n (mirror T) -> In n T.
Proof.
Admitted.

Lemma mirror_In : forall n T, In n T <-> In n (mirror T).
Proof.
(** combine [mirror_In_l] and [mirror_In_r] *)
Admitted.

(** 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) := 0.

(** Write the body of the function [tree_sum] *)

(** 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.
Admitted.

(** 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.