(*
Inductive list (A: Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.

Check list_ind.
Print list_ind.
Check list_rect.
Print list_rect.
*)

Require Import List.
Print list_rect.

Print list.


Section sec_lemmas_on_lists.

Variable A: Type.

Fixpoint append (u v: list A) :=
   match u with
  | nil => v
  | a :: u  => a :: (append u v)
  end.

Lemma nil_neutral_right_explicit_proof :
  forall l: list A, append l nil = l.
Proof.
  intro l. pattern l. apply list_ind; simpl. 
    reflexivity.
    clear l. intros a l IHl. rewrite IHl. reflexivity.
Qed.

Lemma nil_neutral_right :  forall l: list A, append l nil = l.
Proof.
  induction l as [ | x l IHl]; simpl. 
    reflexivity.
    rewrite IHl. reflexivity.
Qed.

Lemma append_assoc: forall u v w: list A,
  append u (append v w) = append (append u v) w.
Proof.
intros u v w. induction u as [| x u Hu]; simpl.
  reflexivity.
  rewrite Hu. reflexivity.
Qed.

Fixpoint revert (l: list A) := 
  match l with
  | nil => nil
  | x :: l =>  append  (revert l) (x :: nil)
  end.

Variable a1 a2 a3: A.
Definition l1 := (a1 :: a2 :: a3 :: nil).
Compute revert l1.

Fixpoint make_long (n: nat) : list A :=
  match n with
  | 0 => nil
  | S n => a1 :: (make_long n)
  end.

Compute revert (make_long 1000).
Time Compute revert (make_long 1000).
(*Time Compute revert (make_long 10000).*)

Fixpoint rev_aux (l: list A) (u: list A) := 
  match l with
  | nil => u
  | x :: l => rev_aux l (x :: u)
  end.

Definition rev (l: list A) := rev_aux l nil.

Compute rev l1.
Time Compute rev (make_long 10000).

(*
Theorem rev_is_revert : forall l, rev l = revert l.
Proof.
unfold rev. induction l.
  simpl. reflexivity.
  simpl. rewrite <- IHl. (*FAILURE*)
Abort.
*)

Lemma rev_aux_meaning : forall l u, rev_aux l u = append (revert l) u.
Proof.
intros l u. revert u. induction l as [| x l Hl]; simpl; intro u. 
  reflexivity. rewrite (Hl (x :: u)). rewrite <- append_assoc. reflexivity.
Qed.
  
Theorem rev_is_revert : forall l, rev l = revert l.
Proof.
intro l; unfold rev. rewrite rev_aux_meaning. apply nil_neutral_right.
Qed.