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