Library tree_ex

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.

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.

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.

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

destruct H.
destruct H.
contradiction.
destruct H.
left. symmetry. assumption.
contradiction.

Now I am glueing things together a bit:

destruct H; try contradiction; try (right; symmetry; assumption).
Qed.

Now define the function 'mirror' that return a mirror image of a tree.

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 Coq 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.