(** A key technique for proving properties of recursive
    functions having an accumulator *)


(** * Introduction *)

(** We don't bother about the type of elements at the moment
    and just take lists of colors *)

Inductive tlcolor : Set :=
  | Green : tlcolor
  | Orange : tlcolor
  | Red : tlcolor
.

Inductive listc : Set  :=
  | Nilc  : listc
  | Consc : tlcolor -> listc -> listc
.

Example lc1 := Consc Green (Consc Red Nilc).
Example lc2 := Consc Orange (Consc Orange Nilc).

Fixpoint lengthc (u : listc) : nat :=
  match u with
  | Nilc => 0
  | Consc x u' => S (lengthc u')
  end.

(** Version with an accumulator *)
(** It can be alternatively (and equivalently) defined as follows: *)
Fixpoint lengthc2 (u : listc) : nat -> nat :=
  fun a =>
    match u with
    | Nilc => a
    | Consc x u' => lengthc2 u' (S a)
    end.

(** Or as follows: *)
Fixpoint lengthc2_alt (u : listc) (a : nat) : nat :=
    match u with
    | Nilc => a
    | Consc x u' => lengthc2_alt u' (S a)
    end.

(** We want to prove Theorem lengthc2_lengthc below.
    A direct attempt by induction in [u] fails:
    the case where the accumulator is 0 depends on the case
    where the accumulator is 1, and so on. *)

Theorem lengthc2_lengthc : forall u, lengthc2 u 0 = lengthc u.
Proof.
  intro u. induction u as [ | x u' IH_u'].
  - cbn. reflexivity.
  - cbn. (* The induction hypothesis is too weak. *)
Abort.

(* We the start by guessing a suitable property that characterizes
   the result of [lengthc2], not only for all lists [u]
   but also for all accumulators [a]. *)
Lemma lengthc2_plus : forall u a, lengthc2 u a = lengthc u + a.
Proof.
  intros u a.
  induction u as [ | x u' IH_u'].
  - reflexivity.
  - cbn.

    (** Here again, the induction hypothesis is too weak.
    The point is that the accumulator was considered as fixed
    to [a], whereas the accumulator changes in the recursive call.
    KEY POINT: the property to be shown by induction has to be
    a property FOR ALL [a]. *)

  (** So we restart the proof. *)
  Restart.

  intros u a.
  (** Using [revert] which has the opposite effect of [intro]. *)
  revert a.

  (** Remark: here it was possible to simply write, at the beginning,
      [intro u]. *)
  Restart.
  intro u.
  induction u as [ | x u' IH_u'].
  (* All subgoals start with a quantification over [a],
     as expected. *)
  - intro a.
    cbn [lengthc lengthc2]. cbn. reflexivity.
  - intro a'.
    cbn [lengthc lengthc2]. cbn.
    Check (IH_u' (S a')).
    rewrite (IH_u' (S a')).
    Check plus_n_Sm.
    Check (plus_n_Sm (lengthc u') a').
    rewrite <- (plus_n_Sm (lengthc u') a').
    reflexivity.
Qed.

(* The desired theorem is a simple corollary of the previous lemma. *)
Theorem lengthc2_lengthc : forall u, lengthc2 u 0 = lengthc u.
Proof.
  intro u.
  rewrite (lengthc2_plus u 0). rewrite <- (plus_n_O (lengthc u)).
  reflexivity.
Qed.

(** Reminder: we provided explicit arguments to equality lemmas
     such as [plus_n_O], etc.
    In common cases, Coq is able to find them, allowing us to
    simply vrite, for instance :
    [rewrite <- plus_n_O].
 *)

(* ---------------------------------------------------------------------- *)
(** * Exercises *)

(** (After an idea from Yuxin Deng).
    Lemma [lengthc2_plus] could also be proved without special care on [a]
    using the following lemma. But be careful in its proof! *)
Lemma lengthc2_S : forall u a, lengthc2 u (S a) = S (lengthc2 u a).
Proof.
Admitted.

(** ** Polymorphic lists *)

(** The above theorems were developed for lists of nats.
    It is intuitively clear that the type of elements is
    irrelevant: we could take lists of colors or whatever as well.
    To this effect, just add an argument for this type.
    Remember that no computation is performed on it, [A] is
    just transfered as is in other functions calls.
 *)

Inductive list (A : Set) : Set :=
| Nil : list A
| Cons : A -> list A -> list A.

Arguments Nil {A}.
Arguments Cons {A}.

Fixpoint length {A : Set} (l : list A) :=
  match l with
  | Nil      => 0
  | Cons x l => S (length l)
  end.

(** Exercise: write functions that translate [listc] to [list tlcolor]
    and conversely.  *)

Fixpoint listc_to_list (l : listc) : list tlcolor. Admitted.

Fixpoint list_to_listc (l : list tlcolor) : listc. Admitted.

(** Exercise: define a polymorphic version of [length2c] *)
Fixpoint length2 {A : Set} (u : list A) : nat -> nat. Admitted.

(** Exercise: prove the expected relationship between [length]
    and [length2], using a suitable additional lemma.*)

Theorem length2_length : forall A (u : list A), length2 u 0 = length u.
Proof.
Admitted.

(** ** Efficient algorithm for reverting lists *)

(** Here is a reference program for reverting a list *)
Fixpoint app {A : Set} (u v : list A) :=
  match u with
  | Nil      => v
  | Cons x u => Cons x (app u v)
  end.

Fixpoint rev {A : Set} (l : list A) :=
  match l with
  | Nil      => Nil
  | Cons x l => app (rev l) (Cons x Nil)
  end.

(*
rev (1 :: 2 :: 3 :: [])
rev (2 :: 3 :: [])  ++  (1 :: [])
(rev [3]  ++  [2])  ++  [1]
((rev ([])  ++ (3 :: []))  ++  (2 :: []))  ++  (1 :: [])
[]  ++ ([3]  ++ ([2]  ++ [1]))
  *)

(** The following properties of [app] were already studied *)
Lemma app_Nil {A} : forall l : list A, app l Nil = l.
Proof.
  induction l as [ | x l Hl]; cbn; [ | rewrite Hl]; reflexivity.
Qed.

Lemma app_assoc {A} :
  forall u v w : list A, app (app u v) w = app u (app v w).
Proof.
  intros u v w.
  induction u as [ | x u Hu]; cbn; [ | rewrite Hu]; reflexivity.
Qed.

(** A linear-time version of rev, using an accumulator. *)
Fixpoint reva {A : Set} (l  : list A) : list A -> list A :=
  fun a =>
    match l with
    | Nil      => a
    | Cons x l => reva l (Cons x a)
    end.

(** Exercise: prove the expected relationship between [rev]
    and [reva], using a suitable additional lemma.*)
Theorem reva_correct :
  forall (A : Set) (l : list A), reva l Nil = rev l.
Proof.
Admitted.