(**
Two objectives here:
- two common linear data structures: lists and natural numbers,
  with their induction principles
- extensions of arithmetic expressions
*)

(** * Lists and natural numbers *)

(** ** Lists *)

(**
The standard type of lists is paramaterized by
the type of elements.
For the sake of simplicity we consider lists of colors.
 *)

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

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

Example l1 := Consc Green (Consc Red Nilc).
Example l2 := Consc Orange (Consc Orange Nilc).

(** The most important function on lists is concatenation,
    It is recursively defined by cases on the *first* argument.
 *)

Fixpoint app u v : listc :=
  match u with
  | Nilc       => v
  | Consc x u' => Consc x (app u' v)
  end.

Compute (app l1 l2).

(** We start with two basic lemmas stated in a very similar way:
    [Nilc] is a neutral element both on the left and the right of [app]
    but the proofs are very different. *)

Theorem app_Nilc_l : forall l, app Nilc l = l.
Proof.
  intro l. cbn [app]. reflexivity.
Qed.

Theorem app_Nilc_r : forall l, app l Nilc = l.
Proof.
  intro l. cbn [app]. (* no progress: why? *)
  (** use induction *)
  (* COMPLETE HERE *)
Admitted.

(** Essential lemma: app is associative *)

Theorem app_assoc : forall u v w, app u (app v w) = app (app u v) w.
Proof.
  intros u v w.
  (** As app performs a case analysis on its firs argument, we try an induction on [u] *)
  induction u as [ | x u' IH_u'].
  (* COMPLETE HERE *)
Admitted.

(* ----------------------------------------------------------------------- *)
(** BEGIN optional exercises (1) *)

Fixpoint rev u : listc :=
  match u with
  | Nilc       => Nilc
  | Consc x u' => app (rev u') (Consc x Nilc)
  end.

(* Previous theorems may be useful... *)
Lemma app_rev : forall u v, rev (app u v) = app (rev v) (rev u).
Proof.
  (* COMPLETE HERE *)
Admitted.

Lemma rev_rev : forall u, rev (rev u) = u.
Proof.
  (* COMPLETE HERE *)
Admitted.

(** END optional exercises (1) *)
(* ----------------------------------------------------------------------- *)

(** ** Natural numbers *)

(** Since the work by Peano and Dedekind at the end of the 19th century,
    natural numbers are no longer primitive but are obtained using
    two basic constructs:
    - zero, denoted by O (capital O);
    - the successor of an already constructed natural number [n], denoted by [S n].
    This corresponds exactly to the following inductive type.
*)

Inductive nat : Set :=
| O : nat
| S : nat -> nat
.

Check (S (S O)). (** represents the number usually written [2] *)

(** Comparing the definitions of [nat] and of [listc], we see that
    natural numbers are similar uncolored lists.
    Scoop: the usual induction principle on natural numbers is nothing
    but a special case of structural induction.!
    The operation correspondong to [app] pn [nat] is just addition.
    The next exercises can be solved by imitating previous exercises
    on lists.
 *)

Fixpoint plus (n m : nat) : nat. Admitted.
(** replece ". Admitted" by " := right definition ." *)

Theorem plus_0_l : forall n, plus O n = n.
  (* COMPLETE HERE *)
Admitted.

Theorem plus_0_r : forall n, plus n O = n.
  (* COMPLETE HERE *)
Admitted.


(** In the following exercises a simple structural induction is enough,
    choose a suitable variable. *)

Theorem plus_assoc : forall n m p, plus n (plus m p) = plus (plus n m) p.
  (* COMPLETE HERE *)
Admitted.

(* ----------------------------------------------------------------------- *)
(** BEGIN optional exercises (2) *)

Theorem plus_Sm_r : forall n m, plus n (S m) = S (plus n m).
  (* COMPLETE HERE *)
Admitted.

(* Reuse previous results  *)
Theorem plus_com : forall n m, plus n m = plus m n.
  (* COMPLETE HERE *)
Admitted.

(** Length of a list:
    it is simpler and better to define it with [S] rather than [plus].
*)
Fixpoint length (l : listc) : nat. Admitted.

Theorem length_app : forall u v, length (app u v) = plus (length u) (length v).
  (* COMPLETE HERE *)
Admitted.

(** END optional exercises (2) *)
(* ----------------------------------------------------------------------- *)

(** Natural numbers of Coq are defined exactly as above. *)

Reset nat.
Print nat.

(** Advantage: we benefit from common notations, for example,
    [S (S O)] is written [2] *)

Fact two : 2 = S (S O).
Proof. (** Coq displays the goal in his way *) reflexivity. Qed.

(** * Useful commands in order to look for information *)

(** What is the function behind "+" ? *)
Locate "+".
Print Nat.add.
(** Entering the naming space [Nat] *)
Import Nat.
Locate "+".
(* Which functions of type [nat -> nat -> nat] are available? *)
Search (nat -> nat -> nat).

(* Which properties of addition are available? *)
Search (_ + _ = _).
Search (_ = _ + _).

 (* We can enforce two places to refer to the same thing *)

Search (_ + ?x = ?x ).
Search (?x = ?x + _ ).

(** * Back to AST of arithmetical expressions *)

(** We consider arithmetical expressions including not only
    operations and constants, but also names of variables.
    For the sake of simplicity we consider that those variables would
    be written "x0", "x1", "x2", etc., which allows us to represent them
    by a simple natural numbers.
    Note that constructors [Aco] and [Ava] allow us to distinguish
    between the constant 2 and the variable "x2".
*)

Inductive aexp :=
| Aco : nat -> aexp (* constantes *)
| Ava : nat -> aexp (* variables *)
| Apl : aexp -> aexp -> aexp
| Amu : aexp -> aexp -> aexp
| Asu : aexp -> aexp -> aexp
.

(* Define some [aexp] expressions fot testing purposes, e.g. for
  (1 + x2) * 3 et  (x0 * 2) + x3
 *)

Example aexp_ex1 : aexp. Admitted.
Example aexp_ex2 : aexp. Admitted.


(** In order to evaluate an expression represented by an [aexp],
    we need as *state*, which is an association between
    each variable name and a value in [nat].
    We choose to represent such a state y a list of natural numbers,
    with the following convention:
    - the first element of the list is the value associated to x0
    - the second element ot the list is the value associated to x1
    - and so on;
    - for all other names, the associated value is 0.
 *)

Inductive state :=
  | Nil : state
  | Cons : nat -> state -> state
.

Definition s_ex1 : state := Cons 3 (Cons 0 (Cons 8 Nil)).

(** Define a function [get] that returns the value associated to xi in the state [s] *)

Fixpoint get (i: nat) (s: state) : nat. Admitted.

Example get_ex1 : get 2 s_ex1 = 8.
Proof. Admitted. (* reflexivity. Qed. *)

(** Complete and prove the defining equations of [get] *)

Remark get_def_1: forall (i:nat),
    get i Nil = 42 . (* replace 42 by the right value *)
Proof. Admitted. (* reflexivity. Qed. *)

Remark get_def_2: forall (v:nat) (q:state),
    get 0 (Cons v q) = 42 . (* replace 42 by the right value *)
Proof. Admitted. (* reflexivity. Qed. *)

Remark get_def_3: forall (i:nat) (v:nat) (q:state),
    get (1+i) (Cons v q) = 42 (* get i _ *). (* replace 42 by the right value *)
Proof. Admitted. (* reflexivity. Qed. *)

(** Define a function [eval] that returns the value of an [aexp], in the state [s] *)

Fixpoint eval (a: aexp) (s: state) : nat. Admitted.

Example eval_ex1_ex1 : eval aexp_ex1 s_ex1 = 27.
Proof. Admitted. (* reflexivity. Qed. *)
Example eval_ex2_ex1 : eval aexp_ex2 s_ex1 = 6.
Proof. Admitted. (* reflexivity. Qed. *)

(** Define a function [rename] which takes an aexp [a] and returns [a] where
    variables corresponding to x0, x1, x2... are respectively
    renamed to x1, x2, x3...  *)

Fixpoint rename (a: aexp) : aexp. Admitted.

(** Define a function [shift] that takes as input a state [s] and returns
    the state where the value of x0 is 0, 
    the value of x1 is the value of x0 in [s],
    the value of x2 is the value of x1 in [s], 
    the value of x3 is the value of x2 in [s], etc. 
    Hint: it is NOT a Fixpoint *)

Definition shift (s : state) : state := Cons 0 s.

(** Show that evaluating a renamed expression in a shifted state
    returns the same result as before *)



(** ** Boolean Expressions *)

(** Define a type named [bexp] for ASTs of Boolean expressions,
    including:
    - Boolean constants Btrue and Bfalse
    - a unary Boolean operator Bnot
    - Boolean binary operators Band and Bor
    - a comparison operator representing equality testing
      between two arithmetical expressions.
*)

Inductive bexp :=
  (* COMPLETE HERE *)
.

(* ----------------------------------------------------------------------- *)
(** BEGIN optional exercises (3) *)

(** The initial environment of Coq includes, beyond [nat],
    an enumerated named [bool] with two values names [true] and [false]
    as well as functions such as disjunction between two values
    of type [bool].
    You can discover the details using the command "Print bool"
    and the command [Search] indicated above, but it is instructive to
    program the Boolean functions by yourself using pattern matching
    as for [tlcolor], along the scheme:

      match Boolean_expr with
      | true => ...
      | false => ...
      end

    The comparison operation between two natural numbers has to be encoded as well.

    Define an evaluation function on [bexp] based on those functions.
*)

(** END optional exercises (3) *)
(* ----------------------------------------------------------------------- *)