(* ========================================================================= *)
(*                                                                           *)
(* * Trees - Alberi binari                                                   *)
(*                                                                           *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* NOTA IMPORTANTE: Prima di utilizzare questo file, e' necessario compilare *)
(* il file Lists.v nel modo seguente:                                        *)
(* - Aprire il file Lists.v                                                  *)
(* - Usare il menu in alto Compile -> Compile buffer.                        *)
(* - Assicuarsi che non siano segnalati errori e tornare a questo file.      *)
(* ------------------------------------------------------------------------- *)

Require Export Lists.
Set Implicit Arguments.

(* ------------------------------------------------------------------------- *)
(* Un albero binario e' un insieme "induttivo", cioe' e' il piu' piccolo     *)
(* insieme tale che:                                                         *)
(*   - esiste un albero "foglia" Leaf;                                       *)
(*   - dati due alberi t1, t2 e' possibile formare un albero "nodo",         *)
(*     indicato con Node t1 t2                                               *)
(* Cosi' come per i naturali usiamo il comando "Inductive".                  *)
(* ------------------------------------------------------------------------- *)

Inductive tree (X : Set) : Set :=
  | leaf : tree X
  | node : X -> tree X -> tree X -> tree X.

Check tree.
Check leaf.
Check node.
Check tree_ind.
Check tree_rec.

(* ------------------------------------------------------------------------- *)
(* Due alberi di esempio per i test.                                         *)
(* ------------------------------------------------------------------------- *)

Definition test_tree1 : tree nat := node O (leaf nat) (leaf nat).
Definition test_tree2 : tree nat := node (S O) test_tree1 (leaf nat).

(* Numero di foglie di un albero. *)
Fixpoint size X (t : tree X) { struct t } : nat :=
  match t with
  | leaf => O
  | node x t1 t2 => S (plus (size t1) (size t2))
  end.

Eval compute in (size test_tree2).

(* ------------------------------------------------------------------------- *)
(* Appiattimento di un albero in una lista.                                  *)
(* ------------------------------------------------------------------------- *)

Fixpoint tree_to_list (X : Set) (t : tree X) { struct t } : List X :=
  match t with
  | leaf => nil X
  | node x t1 t2 => append (tree_to_list t1) (cons x (tree_to_list t2))
  end.

(* ------------------------------------------------------------------------- *)
(* Esercizio.                                                                *)
(* ------------------------------------------------------------------------- *)
Lemma size_length : forall (X : Set) (t : tree X),
  size t = length (tree_to_list t).

Qed.

(* ------------------------------------------------------------------------- *)
(* reverse, scambia ricorsivamente i sottoalberi sinistri con quelli destri. *)
(* Nota: da non confondere con "rev" che abbiamo definito per le liste:      *)
(*    rev : forall X, List X -> List X                                       *)
(* ------------------------------------------------------------------------- *)

Fixpoint symmetric (X : Set) (t : tree X) { struct t } : tree X :=
  match t with
  | leaf => leaf X
  | node x t1 t2 => node x (symmetric t2) (symmetric t1)
  end.

Eval compute in (symmetric test_tree2).

Remark test_size_symmetric : size (symmetric test_tree2) = size test_tree2.
simpl.
reflexivity.
Qed.

Remark test_symmetric_symmetric :
  symmetric (symmetric test_tree2) = test_tree2.
simpl.
reflexivity.
Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio.                                                                *)
(* ------------------------------------------------------------------------- *)

Lemma symmetric_symmetric : forall (X : Set) (t : tree X),
  symmetric (symmetric t) = t.

Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio.                                                                *)
(* ------------------------------------------------------------------------- *)

Lemma symmetric_rev : forall (X : Set) (t : tree X),
  tree_to_list (symmetric t) = rev (tree_to_list t).

Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio.                                                                *)
(* ------------------------------------------------------------------------- *)

Lemma size_symmetric : forall (X : Set) (t : tree X),
  size (symmetric t) = size t.

Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio. Scrivere due funzioni list_to_tree_left e list_to_tree_right   *)
(* che data una lista costruiscono i corrispondenti alberi sbilanciati a     *)
(* sinistra e a destra.                                                      *)
(* Enunciare e dimostrare i seguenti fatti.                                  *)
(* - il simmetrico di list_to_tree_left e' uguale a list_to_tree_right.      *)
(* - la composizione di list_to_tree_left e tree_to_list e' l'identita'.     *)
(* - qual e' il ristultato della composizione di list_to_tree_right e        *)
(*   tree_to_list ?                                                          *)
(* ------------------------------------------------------------------------- *)