(* week-12_arithmetic-expressions-with-names.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 11 Apr 2025 *)

(* ********** *)

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

Require Import Bool Arith List String.

Definition String_eqb (s1 s2 : string) : bool :=
  match String.string_dec s1 s2 with
    left _ =>
    true
  | right _ =>
    false
  end.

(* ********** *)

(* Names: *)

Definition name : Type :=
  string.

(* ***** *)

(* The abstract data type of environments: *)

Definition environment (denotable : Type) : Type :=
  list (name * denotable).

Definition mt (denotable : Type) : environment denotable :=
  nil.

Definition extend (denotable : Type) (x : name) (d : denotable) (e : environment denotable) : environment denotable :=
  (x , d) :: e.

Fixpoint lookup (denotable : Type) (x : name) (e : environment denotable) : option denotable :=
  match e with
    nil =>
    None
  | (x', d) :: e' =>
    if String_eqb x x'
    then Some d
    else lookup denotable x e'
  end.

Lemma fold_unfold_lookup_nil :
  forall (denotable : Type) (x : name),
    lookup denotable x nil =
    None.
Proof.
  fold_unfold_tactic lookup.
Qed.

Lemma fold_unfold_lookup_cons :
  forall (denotable : Type) (x x' : name) (d : denotable) (e' : environment denotable),
    lookup denotable x ((x', d) :: e') =
    if String_eqb x x'
    then Some d
    else lookup denotable x e'.
Proof.
  fold_unfold_tactic lookup.
Qed.

(* ********** *)

(* Syntax: *)

Inductive arithmetic_expression : Type :=
  Literal : nat -> arithmetic_expression
| Name : name -> arithmetic_expression
| Plus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression
| Times : arithmetic_expression -> arithmetic_expression -> arithmetic_expression.

(* ********** *)

(* Semantics: *)

Inductive msg : Type :=
  Undeclared_name : name -> msg.

Inductive expressible_value : Type :=
  Expressible_nat : nat -> expressible_value
| Expressible_msg : msg -> expressible_value.

(* ********** *)

Definition specification_of_evaluate (evaluate : arithmetic_expression -> environment nat -> expressible_value) :=
  (forall (n : nat)
          (e : environment nat),
      evaluate (Literal n) e = Expressible_nat n)
  /\
  ((forall (x : string)
           (e : environment nat)
           (n : nat),
       lookup nat x e = Some n ->
       evaluate (Name x) e = Expressible_nat n)
   /\
   (forall (x : string)
           (e : environment nat),
       lookup nat x e = None ->
       evaluate (Name x) e = Expressible_msg (Undeclared_name x)))
  /\
  ((forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n1 n2 : nat),
       evaluate ae1 e = Expressible_nat n1 ->
       evaluate ae2 e = Expressible_nat n2 ->
       evaluate (Plus ae1 ae2) e = Expressible_nat (n1 + n2))
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (m1 : msg),
       evaluate ae1 e = Expressible_msg m1 ->
       evaluate (Plus ae1 ae2) e = Expressible_msg m1)
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (m2 : msg),
       evaluate ae2 e = Expressible_msg m2 ->
       evaluate (Plus ae1 ae2) e = Expressible_msg m2))
  /\
  ((forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n1 n2 : nat),
       evaluate ae1 e = Expressible_nat n1 ->
       evaluate ae2 e = Expressible_nat n2 ->
       evaluate (Times ae1 ae2) e = Expressible_nat (n1 * n2))
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (m1 : msg),
       evaluate ae1 e = Expressible_msg m1 ->
       evaluate (Times ae1 ae2) e = Expressible_msg m1)
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (m2 : msg),
       evaluate ae2 e = Expressible_msg m2 ->
       evaluate (Times ae1 ae2) e = Expressible_msg m2)).

(* ***** *)

Theorem specification_of_evaluate_is_ambiguous :
  forall evaluate : arithmetic_expression -> environment nat -> expressible_value,
    specification_of_evaluate evaluate ->
    exists (ae : arithmetic_expression)
           (e : environment nat),
      evaluate ae e <> evaluate ae e.
Proof.
  intro evaluate.
  unfold specification_of_evaluate.
  intros [_ [[_ S_evaluate_Name_m] [[_ [S_evaluate_m1 S_evaluate_m2]] _]]].
  exists (Plus (Name "x"%string) (Name "y"%string)), (mt nat).
  assert (LHS :
            evaluate (Plus (Name "x"%string) (Name "y"%string)) (mt nat) = Expressible_msg (Undeclared_name "x"%string)).
  { Check (S_evaluate_m1 (Name "x"%string) (Name "y"%string) (mt nat) (Undeclared_name "x"%string)).
    apply (S_evaluate_m1 (Name "x"%string) (Name "y"%string) (mt nat) (Undeclared_name "x"%string)).
    Check (S_evaluate_Name_m "x"%string (mt nat) (fold_unfold_lookup_nil nat "x"%string)).
    rewrite -> (S_evaluate_Name_m "x"%string (mt nat) (fold_unfold_lookup_nil nat "x"%string)).
    reflexivity. }
  assert (RHS :
            evaluate (Plus (Name "x"%string) (Name "y"%string)) (mt nat) = Expressible_msg (Undeclared_name "y"%string)).
  { Check (S_evaluate_m2 (Name "x"%string) (Name "y"%string) (mt nat) (Undeclared_name "y"%string)).
    apply (S_evaluate_m2 (Name "x"%string) (Name "y"%string) (mt nat) (Undeclared_name "y"%string)).
    Check (S_evaluate_Name_m "y"%string (mt nat) (fold_unfold_lookup_nil nat "y"%string)).
    rewrite -> (S_evaluate_Name_m "y"%string (mt nat) (fold_unfold_lookup_nil nat "y"%string)).
    reflexivity. }
  rewrite -> LHS at 1.
  rewrite -> RHS.
  unfold not.
  intro H_absurd; discriminate H_absurd.
Qed.

(* ********** *)

Definition specification_of_evaluate_ltr (evaluate : arithmetic_expression -> environment nat -> expressible_value) :=
  (forall (n : nat)
          (e : environment nat),
      evaluate (Literal n) e = Expressible_nat n)
  /\
  ((forall (x : string)
           (e : environment nat)
           (n : nat),
       lookup nat x e = Some n ->
       evaluate (Name x) e = Expressible_nat n)
   /\
   (forall (x : string)
           (e : environment nat),
       lookup nat x e = None ->
       evaluate (Name x) e = Expressible_msg (Undeclared_name x)))
  /\
  ((forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n1 n2 : nat),
       evaluate ae1 e = Expressible_nat n1 ->
       evaluate ae2 e = Expressible_nat n2 ->
       evaluate (Plus ae1 ae2) e = Expressible_nat (n1 + n2))
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n1 : nat)
           (m2 : msg),
       evaluate ae1 e = Expressible_nat n1 ->
       evaluate ae2 e = Expressible_msg m2 ->
       evaluate (Plus ae1 ae2) e = Expressible_msg m2)
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (m1 : msg),
       evaluate ae1 e = Expressible_msg m1 ->
       evaluate (Plus ae1 ae2) e = Expressible_msg m1))
  /\
  ((forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n1 n2 : nat),
       evaluate ae1 e = Expressible_nat n1 ->
       evaluate ae2 e = Expressible_nat n2 ->
       evaluate (Times ae1 ae2) e = Expressible_nat (n1 * n2))
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n1 : nat)
           (m2 : msg),
       evaluate ae1 e = Expressible_nat n1 ->
       evaluate ae2 e = Expressible_msg m2 ->
       evaluate (Times ae1 ae2) e = Expressible_msg m2)
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (m1 : msg),
       evaluate ae1 e = Expressible_msg m1 ->
       evaluate (Times ae1 ae2) e = Expressible_msg m1)).

(* ***** *)

(* Exercise 01 *)

Theorem at_most_one_function_satisfies_specification_of_evaluate_ltr :
  forall evaluate_ltr1 : arithmetic_expression -> environment nat -> expressible_value,
    specification_of_evaluate_ltr evaluate_ltr1 ->
    forall evaluate_ltr2 : arithmetic_expression -> environment nat -> expressible_value,
      specification_of_evaluate_ltr evaluate_ltr2 ->
      forall (ae : arithmetic_expression)
             (e : environment nat),
        evaluate_ltr1 ae e = evaluate_ltr2 ae e.
Proof.
  intros evaluate_ltr1 S_evaluate_ltr1 evaluate_ltr2 S_evaluate_ltr2 ae e.
  induction ae as [n | x | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2].
  - destruct S_evaluate_ltr1 as [S_evaluate_ltr1_Literal _].
    destruct S_evaluate_ltr2 as [S_evaluate_ltr2_Literal _].
    rewrite -> S_evaluate_ltr1_Literal.
    rewrite -> S_evaluate_ltr2_Literal.
    reflexivity.
  - destruct S_evaluate_ltr1 as [_ [[S_evaluate_ltr1_Name_n S_evaluate_ltr1_Name_m] _]].
    destruct S_evaluate_ltr2 as [_ [[S_evaluate_ltr2_Name_n S_evaluate_ltr2_Name_m] _]].
    case (lookup nat x e) as [n | ] eqn:L_x.
    + rewrite -> (S_evaluate_ltr1_Name_n x e n L_x).
      rewrite -> (S_evaluate_ltr2_Name_n x e n L_x).
      reflexivity.
    + rewrite -> (S_evaluate_ltr1_Name_m x e L_x).
      rewrite -> (S_evaluate_ltr2_Name_m x e L_x).
      reflexivity.
  - destruct S_evaluate_ltr1 as [_ [_ [[S_evaluate_ltr1_Plus_nn [S_evaluate_ltr1_Plus_nm S_evaluate_ltr1_Plus_m]] _]]].
    destruct S_evaluate_ltr2 as [_ [_ [[S_evaluate_ltr2_Plus_nn [S_evaluate_ltr2_Plus_nm S_evaluate_ltr2_Plus_m]] _]]].
    case (evaluate_ltr2 ae1 e) as [n1 | m1] eqn:E2_ae1.
    + case (evaluate_ltr2 ae2 e) as [n2 | m2] eqn:E2_ae2.
      * rewrite -> (S_evaluate_ltr1_Plus_nn ae1 ae2 e n1 n2 IHae1 IHae2).
        rewrite -> (S_evaluate_ltr2_Plus_nn ae1 ae2 e n1 n2 E2_ae1 E2_ae2).
        reflexivity.
      * rewrite -> (S_evaluate_ltr1_Plus_nm ae1 ae2 e n1 m2 IHae1 IHae2).
        rewrite -> (S_evaluate_ltr2_Plus_nm ae1 ae2 e n1 m2 E2_ae1 E2_ae2).
        reflexivity.
    + rewrite -> (S_evaluate_ltr1_Plus_m ae1 ae2 e m1 IHae1).
      rewrite -> (S_evaluate_ltr2_Plus_m ae1 ae2 e m1 E2_ae1).
      reflexivity.
  - destruct S_evaluate_ltr1 as [_ [_ [_ [S_evaluate_ltr1_Times_nn [S_evaluate_ltr1_Times_nm S_evaluate_ltr1_Times_m]]]]].
    destruct S_evaluate_ltr2 as [_ [_ [_ [S_evaluate_ltr2_Times_nn [S_evaluate_ltr2_Times_nm S_evaluate_ltr2_Times_m]]]]].
    case (evaluate_ltr2 ae1 e) as [n1 | m1] eqn:E2_ae1.
    + case (evaluate_ltr2 ae2 e) as [n2 | m2] eqn:E2_ae2.
      * rewrite -> (S_evaluate_ltr1_Times_nn ae1 ae2 e n1 n2 IHae1 IHae2).
        rewrite -> (S_evaluate_ltr2_Times_nn ae1 ae2 e n1 n2 E2_ae1 E2_ae2).
        reflexivity.
      * rewrite -> (S_evaluate_ltr1_Times_nm ae1 ae2 e n1 m2 IHae1 IHae2).
        rewrite -> (S_evaluate_ltr2_Times_nm ae1 ae2 e n1 m2 E2_ae1 E2_ae2).
        reflexivity.
    + rewrite -> (S_evaluate_ltr1_Times_m ae1 ae2 e m1 IHae1).
      rewrite -> (S_evaluate_ltr2_Times_m ae1 ae2 e m1 E2_ae1).
      reflexivity.
Qed.

(* ***** *)

Fixpoint evaluate_ltr (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
  match ae with
    Literal n =>
    Expressible_nat n
  | Name x =>
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end
  | Plus ae1 ae2 =>
    match evaluate_ltr ae1 e with
      Expressible_nat n1 =>
      match evaluate_ltr ae2 e with
        Expressible_nat n2 =>
        Expressible_nat (n1 + n2)
      | Expressible_msg m2 =>
        Expressible_msg m2
      end
    | Expressible_msg m1 =>
      Expressible_msg m1
    end
  | Times ae1 ae2 =>
    match evaluate_ltr ae1 e with
      Expressible_nat n1 =>
      match evaluate_ltr ae2 e with
        Expressible_nat n2 =>
        Expressible_nat (n1 * n2)
      | Expressible_msg m2 =>
        Expressible_msg m2
      end
    | Expressible_msg m1 =>
      Expressible_msg m1
    end
  end.
                                                                                            
Lemma fold_unfold_evaluate_ltr_Literal :
  forall (n : nat)
         (e : environment nat),
    evaluate_ltr (Literal n) e =
    Expressible_nat n.
Proof.
  fold_unfold_tactic evaluate_ltr.
Qed.

Lemma fold_unfold_evaluate_ltr_Name :
  forall (x : name)
         (e : environment nat),
    evaluate_ltr (Name x) e =
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end.
Proof.
  fold_unfold_tactic evaluate_ltr.
Qed.

Lemma fold_unfold_evaluate_ltr_Plus :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_ltr (Plus ae1 ae2) e =
    match evaluate_ltr ae1 e with
      Expressible_nat n1 =>
      match evaluate_ltr ae2 e with
        Expressible_nat n2 =>
        Expressible_nat (n1 + n2)
      | Expressible_msg m2 =>
        Expressible_msg m2
      end
    | Expressible_msg m1 =>
      Expressible_msg m1
    end.
Proof.
  fold_unfold_tactic evaluate_ltr.
Qed.

Lemma fold_unfold_evaluate_ltr_Times :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_ltr (Times ae1 ae2) e =
    match evaluate_ltr ae1 e with
      Expressible_nat n1 =>
      match evaluate_ltr ae2 e with
        Expressible_nat n2 =>
        Expressible_nat (n1 * n2)
      | Expressible_msg m2 =>
        Expressible_msg m2
      end
    | Expressible_msg m1 =>
      Expressible_msg m1
    end.
Proof.
  fold_unfold_tactic evaluate_ltr.
Qed.

(* ***** *)

Theorem evaluate_ltr_satisfies_the_specification_of_evaluate_ltr :
  specification_of_evaluate_ltr evaluate_ltr.
Proof.
  unfold specification_of_evaluate_ltr.
  split; [ | split; [ | split]].
  - exact fold_unfold_evaluate_ltr_Literal.
  - split.
    + intros x e n L_x.
      rewrite -> fold_unfold_evaluate_ltr_Name.
      rewrite -> L_x.
      reflexivity.
    + intros x e L_x.
      rewrite -> fold_unfold_evaluate_ltr_Name.
      rewrite -> L_x.
      reflexivity.
  - split; [ | split].
    + intros ae1 ae2 e n1 n2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_ltr_Plus.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e n1 m2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_ltr_Plus.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e m1 E_ae1.
      rewrite -> fold_unfold_evaluate_ltr_Plus.
      rewrite -> E_ae1.
      reflexivity.
  - split; [ | split].
    + intros ae1 ae2 e n1 n2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_ltr_Times.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e n1 m2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_ltr_Times.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e m1 E_ae1.
      rewrite -> fold_unfold_evaluate_ltr_Times.
      rewrite -> E_ae1.
      reflexivity.
Qed.

(* ***** *)

(* Exercise 02 *)

Theorem at_least_one_function_satisfies_specification_of_evaluate_ltr :
  exists evaluate : arithmetic_expression -> environment nat -> expressible_value,
    specification_of_evaluate_ltr evaluate.
Proof.
  exists evaluate_ltr.
  exact evaluate_ltr_satisfies_the_specification_of_evaluate_ltr.
Qed.

(* ********** *)

Definition specification_of_evaluate_rtl (evaluate : arithmetic_expression -> environment nat -> expressible_value) :=
  (forall (n : nat)
          (e : environment nat),
      evaluate (Literal n) e = Expressible_nat n)
  /\
  ((forall (x : string)
           (e : environment nat)
           (n : nat),
       lookup nat x e = Some n ->
       evaluate (Name x) e = Expressible_nat n)
   /\
   (forall (x : string)
           (e : environment nat),
       lookup nat x e = None ->
       evaluate (Name x) e = Expressible_msg (Undeclared_name x)))
  /\
  ((forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n2 n1 : nat),
       evaluate ae2 e = Expressible_nat n2 ->
       evaluate ae1 e = Expressible_nat n1 ->
       evaluate (Plus ae1 ae2) e = Expressible_nat (n1 + n2))
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n2 : nat)
           (m1 : msg),
       evaluate ae2 e = Expressible_nat n2 ->
       evaluate ae1 e = Expressible_msg m1 ->
       evaluate (Plus ae1 ae2) e = Expressible_msg m1)
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (m2 : msg),
       evaluate ae2 e = Expressible_msg m2 ->
       evaluate (Plus ae1 ae2) e = Expressible_msg m2))
  /\
  ((forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n2 n1 : nat),
       evaluate ae2 e = Expressible_nat n2 ->
       evaluate ae1 e = Expressible_nat n1 ->
       evaluate (Times ae1 ae2) e = Expressible_nat (n1 * n2))
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (n2 : nat)
           (m1 : msg),
       evaluate ae2 e = Expressible_nat n2 ->
       evaluate ae1 e = Expressible_msg m1 ->
       evaluate (Times ae1 ae2) e = Expressible_msg m1)
   /\
   (forall (ae1 ae2 : arithmetic_expression)
           (e : environment nat)
           (m2 : msg),
       evaluate ae2 e = Expressible_msg m2 ->
       evaluate (Times ae1 ae2) e = Expressible_msg m2)).

(* ***** *)

(* Exercise 03 *)

Theorem at_most_one_function_satisfies_specification_of_evaluate_rtl :
  forall evaluate_rtl1 : arithmetic_expression -> environment nat -> expressible_value,
    specification_of_evaluate_rtl evaluate_rtl1 ->
    forall evaluate_rtl2 : arithmetic_expression -> environment nat -> expressible_value,
      specification_of_evaluate_rtl evaluate_rtl2 ->
      forall (ae : arithmetic_expression)
             (e : environment nat),
        evaluate_rtl1 ae e = evaluate_rtl2 ae e.
Proof.
Abort.

(* ***** *)

(* Exercise 04 *)

Theorem at_least_one_function_satisfies_specification_of_evaluate_rtl :
  exists evaluate : arithmetic_expression -> environment nat -> expressible_value,
    specification_of_evaluate_rtl evaluate.
Proof.
Abort.

(* ********** *)

Fixpoint evaluate_ltr2 (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
  match ae with
    Literal n =>
    Expressible_nat n
  | Name x =>
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end
  | Plus ae1 ae2 =>
    match (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) with
      (Expressible_nat n1, Expressible_nat n2) =>
      Expressible_nat (n1 + n2)
    | (Expressible_msg m1, _) =>
      Expressible_msg m1
    | (_, Expressible_msg m2) =>
      Expressible_msg m2
    end
  | Times ae1 ae2 =>
    match (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) with
      (Expressible_nat n1, Expressible_nat n2) =>
      Expressible_nat (n1 * n2)
    | (Expressible_msg m1, _) =>
      Expressible_msg m1
    | (_, Expressible_msg m2) =>
      Expressible_msg m2
    end
  end.
                                                                                            
Lemma fold_unfold_evaluate_ltr2_Literal :
  forall (n : nat)
         (e : environment nat),
    evaluate_ltr2 (Literal n) e =
    Expressible_nat n.
Proof.
  fold_unfold_tactic evaluate_ltr2.
Qed.

Lemma fold_unfold_evaluate_ltr2_Name :
  forall (x : name)
         (e : environment nat),
    evaluate_ltr2 (Name x) e =
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end.
Proof.
  fold_unfold_tactic evaluate_ltr2.
Qed.

Lemma fold_unfold_evaluate_ltr2_Plus :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_ltr2 (Plus ae1 ae2) e =
    match (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) with
      (Expressible_nat n1, Expressible_nat n2) =>
      Expressible_nat (n1 + n2)
    | (Expressible_msg m1, _) =>
      Expressible_msg m1
    | (_, Expressible_msg m2) =>
      Expressible_msg m2
    end.
Proof.
  fold_unfold_tactic evaluate_ltr2.
Qed.

Lemma fold_unfold_evaluate_ltr2_Times :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_ltr2 (Times ae1 ae2) e =
    match (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) with
      (Expressible_nat n1, Expressible_nat n2) =>
      Expressible_nat (n1 * n2)
    | (Expressible_msg m1, _) =>
      Expressible_msg m1
    | (_, Expressible_msg m2) =>
      Expressible_msg m2
    end.
Proof.
  fold_unfold_tactic evaluate_ltr2.
Qed.

(* ***** *)

Theorem evaluate_ltr2_satisfies_the_specification_of_evaluate_ltr :
  specification_of_evaluate_ltr evaluate_ltr2.
Proof.
  unfold specification_of_evaluate_ltr.
  split; [ | split; [ | split]].
  - exact fold_unfold_evaluate_ltr2_Literal.
  - split.
    + intros x e n L_x.
      rewrite -> fold_unfold_evaluate_ltr2_Name.
      rewrite -> L_x.
      reflexivity.
    + intros x e L_x.
      rewrite -> fold_unfold_evaluate_ltr2_Name.
      rewrite -> L_x.
      reflexivity.
  - split; [ | split].
    + intros ae1 ae2 e n1 n2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_ltr2_Plus.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e n1 m2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_ltr2_Plus.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e m1 E_ae1.
      rewrite -> fold_unfold_evaluate_ltr2_Plus.
      rewrite -> E_ae1.
      reflexivity.
  - split; [ | split].
    + intros ae1 ae2 e n1 n2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_ltr2_Times.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e n1 m2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_ltr2_Times.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e m1 E_ae1.
      rewrite -> fold_unfold_evaluate_ltr2_Times.
      rewrite -> E_ae1.
      reflexivity.
Qed.

(* ***** *)

Fixpoint evaluate_rtl2 (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
  match ae with
    Literal n =>
    Expressible_nat n
  | Name x =>
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end
  | Plus ae1 ae2 =>
    match (evaluate_rtl2 ae1 e, evaluate_rtl2 ae2 e) with
      (Expressible_nat n1, Expressible_nat n2) =>
      Expressible_nat (n1 + n2)
    | (_, Expressible_msg m2) =>
      Expressible_msg m2
    | (Expressible_msg m1, _) =>
      Expressible_msg m1
    end
  | Times ae1 ae2 =>
    match (evaluate_rtl2 ae1 e, evaluate_rtl2 ae2 e) with
      (Expressible_nat n1, Expressible_nat n2) =>
      Expressible_nat (n1 * n2)
    | (_, Expressible_msg m2) =>
      Expressible_msg m2
    | (Expressible_msg m1, _) =>
      Expressible_msg m1
    end
  end.

Lemma fold_unfold_evaluate_rtl2_Literal :
  forall (n : nat)
         (e : environment nat),
    evaluate_rtl2 (Literal n) e =
    Expressible_nat n.
Proof.
  fold_unfold_tactic evaluate_rtl2.
Qed.

Lemma fold_unfold_evaluate_rtl2_Name :
  forall (x : name)
         (e : environment nat),
    evaluate_rtl2 (Name x) e =
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end.
Proof.
  fold_unfold_tactic evaluate_rtl2.
Qed.

Lemma fold_unfold_evaluate_rtl2_Plus :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_rtl2 (Plus ae1 ae2) e =
    match (evaluate_rtl2 ae1 e, evaluate_rtl2 ae2 e) with
      (Expressible_nat n1, Expressible_nat n2) =>
      Expressible_nat (n1 + n2)
    | (_, Expressible_msg m2) =>
      Expressible_msg m2
    | (Expressible_msg m1, _) =>
      Expressible_msg m1
    end.
Proof.
  fold_unfold_tactic evaluate_rtl2.
Qed.

Lemma fold_unfold_evaluate_rtl2_Times :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_rtl2 (Times ae1 ae2) e =
    match (evaluate_rtl2 ae1 e, evaluate_rtl2 ae2 e) with
      (Expressible_nat n1, Expressible_nat n2) =>
      Expressible_nat (n1 * n2)
    | (_, Expressible_msg m2) =>
      Expressible_msg m2
    | (Expressible_msg m1, _) =>
      Expressible_msg m1
    end.
Proof.
  fold_unfold_tactic evaluate_rtl2.
Qed.

Theorem evaluate_rtl2_satisfies_the_specification_of_evaluate_rtl :
  specification_of_evaluate_rtl evaluate_rtl2.
Proof.
  unfold specification_of_evaluate_rtl.
  split; [ | split; [ | split]].
  - exact fold_unfold_evaluate_rtl2_Literal.
  - split.
    + intros x e n L_x.
      rewrite -> fold_unfold_evaluate_rtl2_Name.
      rewrite -> L_x.
      reflexivity.
    + intros x e L_x.
      rewrite -> fold_unfold_evaluate_rtl2_Name.
      rewrite -> L_x.
      reflexivity.
  - split; [ | split].
    + intros ae1 ae2 e n1 n2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_rtl2_Plus.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e n2 m1 E_ae2 E_ae1.
      rewrite -> fold_unfold_evaluate_rtl2_Plus.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e m2 E_ae2.
      rewrite -> fold_unfold_evaluate_rtl2_Plus.
      rewrite -> E_ae2.
      case (evaluate_rtl2 ae1 e) as [n1 | m1] eqn:E_ae1.
      * reflexivity.
      * reflexivity.
  - split; [ | split].
    + intros ae1 ae2 e n1 n2 E_ae1 E_ae2.
      rewrite -> fold_unfold_evaluate_rtl2_Times.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e n2 m1 E_ae2 E_ae1.
      rewrite -> fold_unfold_evaluate_rtl2_Times.
      rewrite -> E_ae1.
      rewrite -> E_ae2.
      reflexivity.
    + intros ae1 ae2 e m2 E_ae2.
      rewrite -> fold_unfold_evaluate_rtl2_Times.
      rewrite -> E_ae2.
      case (evaluate_rtl2 ae1 e) as [n1 | m1] eqn:E_ae1.
      * reflexivity.
      * reflexivity.
Qed.

(* ********** *)

Print evaluate_ltr2.

(*
evaluate_ltr2 = 
fix evaluate_ltr2 (ae : arithmetic_expression) (e : environment nat) {struct ae} : expressible_value :=
  match ae with
  | Literal n => Expressible_nat n
  | Name x =>
      match lookup nat x e with
      | Some n => Expressible_nat n
      | None => Expressible_msg (Undeclared_name x)
      end
  | Plus ae1 ae2 =>
      let (e0, e1) := (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) in
      match e0 with
      | Expressible_nat n1 =>
          match e1 with
          | Expressible_nat n2 => Expressible_nat (n1 + n2)
          | Expressible_msg m2 => Expressible_msg m2
          end
      | Expressible_msg m1 => Expressible_msg m1
      end
  | Times ae1 ae2 =>
      let (e0, e1) := (evaluate_ltr2 ae1 e, evaluate_ltr2 ae2 e) in
      match e0 with
      | Expressible_nat n1 =>
          match e1 with
          | Expressible_nat n2 => Expressible_nat (n1 * n2)
          | Expressible_msg m2 => Expressible_msg m2
          end
      | Expressible_msg m1 => Expressible_msg m1
      end
  end
     : arithmetic_expression -> environment nat -> expressible_value
*)

(* ********** *)

(* Exercise 06 *)

Fixpoint evaluate_ltr2_switched (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
  match ae with
    Literal n =>
    Expressible_nat n
  | Name x =>
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end
  | Plus ae1 ae2 =>
    match (evaluate_ltr2_switched ae2 e, evaluate_ltr2_switched ae1 e) with
      (Expressible_nat n2, Expressible_nat n1) =>
      Expressible_nat (n1 + n2)
    | (Expressible_msg m2, _) =>
      Expressible_msg m2
    | (_, Expressible_msg m1) =>
      Expressible_msg m1
    end
  | Times ae1 ae2 =>
    match (evaluate_ltr2_switched ae2 e, evaluate_ltr2_switched ae1 e) with
      (Expressible_nat n2, Expressible_nat n1) =>
      Expressible_nat (n1 * n2)
    | (Expressible_msg m2, _) =>
      Expressible_msg m2
    | (_, Expressible_msg m1) =>
      Expressible_msg m1
    end
  end.

Lemma fold_unfold_evaluate_ltr2_switched_Literal :
  forall (n : nat)
         (e : environment nat),
    evaluate_ltr2_switched (Literal n) e =
    Expressible_nat n.
Proof.
  fold_unfold_tactic evaluate_ltr2_switched.
Qed.

Lemma fold_unfold_evaluate_ltr2_switched_Name :
  forall (x : name)
         (e : environment nat),
    evaluate_ltr2_switched (Name x) e =
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end.
Proof.
  fold_unfold_tactic evaluate_ltr2_switched.
Qed.

Lemma fold_unfold_evaluate_ltr2_switched_Plus :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_ltr2_switched (Plus ae1 ae2) e =
    match (evaluate_ltr2_switched ae2 e, evaluate_ltr2_switched ae1 e) with
      (Expressible_nat n2, Expressible_nat n1) =>
      Expressible_nat (n1 + n2)
    | (Expressible_msg m2, _) =>
      Expressible_msg m2
    | (_, Expressible_msg m1) =>
      Expressible_msg m1
    end.
Proof.
  fold_unfold_tactic evaluate_ltr2_switched.
Qed.

Lemma fold_unfold_evaluate_ltr2_switched_Times :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_ltr2_switched (Times ae1 ae2) e =
    match (evaluate_ltr2_switched ae2 e, evaluate_ltr2_switched ae1 e) with
      (Expressible_nat n2, Expressible_nat n1) =>
      Expressible_nat (n1 * n2)
    | (Expressible_msg m2, _) =>
      Expressible_msg m2
    | (_, Expressible_msg m1) =>
      Expressible_msg m1
    end.
Proof.
  fold_unfold_tactic evaluate_ltr2_switched.
Qed.

(* ***** *)

Fixpoint evaluate_rtl2_switched (ae : arithmetic_expression) (e : environment nat) : expressible_value :=
  match ae with
    Literal n =>
    Expressible_nat n
  | Name x =>
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end
  | Plus ae1 ae2 =>
    match (evaluate_rtl2_switched ae2 e, evaluate_rtl2_switched ae1 e) with
      (Expressible_nat n2, Expressible_nat n1) =>
      Expressible_nat (n1 + n2)
    | (_, Expressible_msg m1) =>
      Expressible_msg m1
    | (Expressible_msg m2, _) =>
      Expressible_msg m2
    end
  | Times ae1 ae2 =>
    match (evaluate_rtl2_switched ae2 e, evaluate_rtl2_switched ae1 e) with
      (Expressible_nat n2, Expressible_nat n1) =>
      Expressible_nat (n1 * n2)
    | (_, Expressible_msg m1) =>
      Expressible_msg m1
    | (Expressible_msg m2, _) =>
      Expressible_msg m2
    end
  end.

Lemma fold_unfold_evaluate_rtl2_switched_Literal :
  forall (n : nat)
         (e : environment nat),
    evaluate_rtl2_switched (Literal n) e =
    Expressible_nat n.
Proof.
  fold_unfold_tactic evaluate_rtl2_switched.
Qed.

Lemma fold_unfold_evaluate_rtl2_switched_Name :
  forall (x : name)
         (e : environment nat),
    evaluate_rtl2_switched (Name x) e =
    match lookup nat x e with
      Some n =>
      Expressible_nat n
    | None =>
      Expressible_msg (Undeclared_name x)
    end.
Proof.
  fold_unfold_tactic evaluate_rtl2_switched.
Qed.

Lemma fold_unfold_evaluate_rtl2_switched_Plus :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_rtl2_switched (Plus ae1 ae2) e =
    match (evaluate_rtl2_switched ae2 e, evaluate_rtl2_switched ae1 e) with
      (Expressible_nat n2, Expressible_nat n1) =>
      Expressible_nat (n1 + n2)
    | (_, Expressible_msg m1) =>
      Expressible_msg m1
    | (Expressible_msg m2, _) =>
      Expressible_msg m2
    end.
Proof.
  fold_unfold_tactic evaluate_rtl2_switched.
Qed.

Lemma fold_unfold_evaluate_rtl2_switched_Times :
  forall (ae1 ae2 : arithmetic_expression)
         (e : environment nat),
    evaluate_rtl2_switched (Times ae1 ae2) e =
    match (evaluate_rtl2_switched ae2 e, evaluate_rtl2_switched ae1 e) with
      (Expressible_nat n2, Expressible_nat n1) =>
      Expressible_nat (n1 * n2)
    | (_, Expressible_msg m1) =>
      Expressible_msg m1
    | (Expressible_msg m2, _) =>
      Expressible_msg m2
    end.
Proof.
  fold_unfold_tactic evaluate_rtl2_switched.
Qed.

(* ********** *)

(* end of week-12_arithmetic-expressions-with-names.v *)