(* ========================================================================= *)
(*                                                                           *)
(* * LISTE                                                                   *)
(*                                                                           *)
(* ========================================================================= *)

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

Require Export Nat.  (* Importa le nostre definizioni sui numeri naturali.   *)

Inductive List (X : Set) : Set :=
  | nil : List X
  | cons : X -> List X -> List X.

Check (nil nat).
Check (cons nat O (cons nat (S O) (nil nat))).

(* ------------------------------------------------------------------------- *)
(* Concatenazione di due liste: append l1 l2.                                *)
(*                                                                           *)
(* Notare l'analogia con la funzione plus per i naturali.                    *)
(* ------------------------------------------------------------------------- *)

Fixpoint append (X : Set) (l1 l2 : List X) { struct l1 } : List X :=
  match l1 with
  | nil => l2
  | cons h t => cons X h (append X t l2)
  end.

Definition test_list1 : List nat := (cons nat O (nil nat)).
Definition test_list2 : List nat := (cons nat (S O) (nil nat)).

Eval compute in (append nat test_list1 test_list2).
(* ==> cons nat O (cons nat (S O) (nil nat))  : List nat                     *)

Lemma append_assoc : forall (X : Set) (l1 l2 l3 : List X),
  append X l1 (append X l2 l3) = append X (append X l1 l2) l3.
intros.
induction l1.
simpl.
reflexivity.
simpl.
rewrite IHl1.
reflexivity.
Qed.

(* ------------------------------------------------------------------------- *)
(* Argomenti Impliciti                                                       *)
(*                                                                           *)
(* "cons X h t" e' una funzione di 3 argomenti.  Ma X e' determinato da h e  *)
(* da t.  Quindi chiediamo a Coq di "nascondere" X (di renderlo implicito).  *)
(* ------------------------------------------------------------------------- *)
Implicit Arguments cons [X].

(* ------------------------------------------------------------------------- *)
(* Stessa cosa per "append".                                                 *)
(* ------------------------------------------------------------------------- *)

Implicit Arguments append [X].

Eval compute in (append test_list1 test_list2).
(* ==> cons nat O (cons nat (S O) (nil nat))  : List nat *)

Print cons.
Print append.

(* ------------------------------------------------------------------------- *)
(* E' noioso specificare sempre gli argomenti impliciti.  Chiediamo a Coq di *)
(* dichiarare considerare impliciti gli argomenti in maniera automatica      *)
(* quando questo e' possibile.                                               *)
(* ------------------------------------------------------------------------- *)

Set Implicit Arguments.

Fixpoint rev (X : Set) (l : List X) { struct l } : List X :=
  match l with
  | nil => nil X
  | cons h t => append (rev t) (cons h (nil X))
  end.

(* ------------------------------------------------------------------------- *)
(* Osserviamo che adesso "X" e' un argomento implicito per rev perche' e'    *)
(* deterimato da "l".                                                        *)
(* ------------------------------------------------------------------------- *)

Print rev.

(* ------------------------------------------------------------------------- *)
(* Calcolo: Rev di [0,1] = [1,0].                                            *)
(* ------------------------------------------------------------------------- *)

Eval compute in (rev (cons O (cons (S O) (nil nat)))).

(* ------------------------------------------------------------------------- *)
(* Lunghezza di una lista.                                                   *)
(* ------------------------------------------------------------------------- *)

Fixpoint length (X : Set) (l : List X) { struct l } : nat :=
  match l with
  | nil => O
  | cons h t => S (length t)
  end.

(* ------------------------------------------------------------------------- *)
(* Calcolo: Lunghezza di [0,0,0] = 3.                                        *)
(* ------------------------------------------------------------------------- *)

Eval compute in (length (cons O (cons O (cons O (nil nat))))).

(* ------------------------------------------------------------------------- *)
(* Lunghezza di append di  l1 e l2 = lunghezza di l1 + lunghezza di l2.      *)
(* ------------------------------------------------------------------------- *)

Lemma length_append : forall X (l1 l2 : List X),
  length (append l1 l2) = plus (length l1) (length l2).
intros.
induction l1.
simpl.
reflexivity.
simpl.
rewrite IHl1.
reflexivity.
Qed.

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

Lemma length_rev : forall X (l : List X),
  length (rev l) = length l.

Qed.

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

Lemma append_nil : forall (X : Set) (l : List X),
  append l (nil X) = l.

Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio.                                                                *)
(* ------------------------------------------------------------------------- *)
Lemma rev_append : forall X (l1 l2 : List X),
  rev (append l1 l2) = append (rev l2) (rev l1).

Qed.