feat: finish term project

cs3234/labs/term-project.v

@@ -7,6 +7,7 @@
 
 (* Three language processors for arithmetic expressions. *)
 
+
 (*
    group name:
 
@@ -488,7 +489,7 @@ Definition specification_of_decode_execute (decode_execute : byte_code_instructi
   (forall (n1 n2 : nat)
      (ds : data_stack),
       n1 <? n2 = false ->
-      decode_execute SUB (n2 :: n1 :: ds) = OK ((n2 - n1) :: ds))
+      decode_execute SUB (n2 :: n1 :: ds) = OK ((n1 - n2) :: ds))
   /\
  (* if the data stack does not contain at least two nats
    evaluating
@@ -516,7 +517,7 @@ Definition decode_execute (bci : byte_code_instruction) (ds : data_stack) : resu
       | n2 :: n1 :: ds' =>
           if n1 <? n2
           then KO (String.append "numerical underflow: -" (string_of_nat (n2 - n1)))
-          else OK ((n2 - n1) :: ds')
+          else OK ((n1 - n2) :: ds')
       | _ => KO "ADD: stack underflow"
       end
   end.
@@ -725,6 +726,7 @@ Definition specification_of_run (run : target_program -> expressible_value) :=
        run (Target_program bcis) = Expressible_msg s).
 
 
+(* Since this is talking mostly about the data stack, thats where we will work from *)
 Theorem there_is_at_most_one_run_function :
   forall (f g : target_program -> expressible_value),
     specification_of_run f ->
@@ -732,16 +734,93 @@ Theorem there_is_at_most_one_run_function :
     forall (t: target_program),
     f t = g t.
 Proof.
-  intros f g.
+  intros f g S_f S_g [bcis].
-  unfold specification_of_run.
+  (* This was the tricky part in my understanding. We are operating on the result of FDEL. Thus, we
-  intros S_f S_g [bcis].
+   check every case of fdel and work from there *)
-  case (fetch_decode_execute_loop bcis nil) as [ds | s] eqn:H_fdel.
+  case (fetch_decode_execute_loop bcis nil) as [[| n [| n' ds'']] | s] eqn:H_fdel.
-  - destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_f_nil _].
+  - unfold specification_of_run in S_f,S_g.
+    destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_f_nil _].
     destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [S_g_nil _].
-    case ds as [ | n ds' ] eqn:H_ds.
+    rewrite -> (S_g_nil bcis H_fdel).
-    + rewrite -> (S_g_nil bcis H_fdel).
+    exact (S_f_nil bcis H_fdel).
-      exact (S_f_nil bcis H_fdel).
+  - unfold specification_of_run in S_f,S_g.
-    + Check (S_f_nil bcis).
+    destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [S_f_one _]].
+    destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [S_g_one _]].
+    rewrite -> (S_g_one bcis n H_fdel).
+    exact (S_f_one bcis n H_fdel).
+  - unfold specification_of_run in S_f,S_g.
+    destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [S_f_mult _]]].
+    destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [S_g_mult _]]].
+    rewrite -> (S_g_mult bcis n n' ds'' H_fdel).
+    exact (S_f_mult bcis n n' ds'' H_fdel).
+  - unfold specification_of_run in S_f,S_g.
+    destruct (S_f fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [_ S_f_KO]]].
+    destruct (S_g fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification) as [_ [_ [_ S_g_KO]]].
+    rewrite -> (S_g_KO bcis s H_fdel).
+    exact (S_f_KO bcis s H_fdel).
+Qed.
+
+
+Definition run (p : target_program) : expressible_value :=
+  match p with
+    Target_program bcis =>
+      match (fetch_decode_execute_loop bcis nil) with
+      | OK nil => Expressible_msg "no result on the data stack"
+      | OK (n :: nil) => Expressible_nat n
+      | OK (n :: n' :: ds'') => Expressible_msg "too many results on the data stack"
+      | KO s => Expressible_msg s
+      end
+  end.
+
+
+Theorem run_satisfies_the_specification_of_run :
+ specification_of_run run.
+Proof.
+  unfold specification_of_run.
+  intros fdel.
+  intros S_fdel.
+  split.
+  { intros bcis H_fdel.
+    unfold run.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop
+                 fetch_decode_execute_loop fdel
+                 fetch_decode_execute_loop_satifies_the_specification S_fdel
+                 bcis nil
+      ).
+    rewrite -> H_fdel.
+    reflexivity. }
+  split.
+  { intros bcis n H_fdel.
+    unfold run.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop
+                 fetch_decode_execute_loop fdel
+                 fetch_decode_execute_loop_satifies_the_specification S_fdel
+                 bcis nil
+      ).
+    rewrite -> H_fdel.
+    reflexivity.
+  }
+  split.
+  { intros bcis n n' ds'' H_fdel .
+    unfold run.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop
+                 fetch_decode_execute_loop fdel
+                 fetch_decode_execute_loop_satifies_the_specification S_fdel
+                 bcis nil
+      ).
+    rewrite -> H_fdel.
+    reflexivity.
+  }
+  intros bcis s H_fdel .
+  unfold run.
+  rewrite -> (there_is_at_most_one_fetch_decode_execute_loop
+               fetch_decode_execute_loop fdel
+               fetch_decode_execute_loop_satifies_the_specification S_fdel
+               bcis nil
+    ).
+  rewrite -> H_fdel.
+  reflexivity.
+Qed.
 
 
 (* Task 4:
@@ -762,6 +841,71 @@ Definition specification_of_compile_aux (compile_aux : arithmetic_expression ->
   (forall ae1 ae2 : arithmetic_expression,
      compile_aux (Minus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil)).
 
+Theorem there_is_at_most_one_compile_aux_function :
+  forall (f g : arithmetic_expression -> list byte_code_instruction),
+    (specification_of_compile_aux f) ->
+    (specification_of_compile_aux g) ->
+    forall (ae : arithmetic_expression),
+    f ae = g ae.
+Proof.
+  intros f g S_f S_g ae.
+  destruct S_f as [S_f_Literal [S_f_Plus S_f_Minus]].
+  destruct S_g as [S_g_Literal [S_g_Plus S_g_Minus]].
+  induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2 ].
+  - rewrite -> S_g_Literal.
+    exact (S_f_Literal n).
+  - rewrite -> S_g_Plus.
+    rewrite -> S_f_Plus.
+    rewrite -> IHae1.
+    rewrite -> IHae2.
+    reflexivity.
+  - rewrite -> S_g_Minus.
+    rewrite -> S_f_Minus.
+    rewrite -> IHae1.
+    rewrite -> IHae2.
+    reflexivity.
+Qed.
+
+Fixpoint compile_aux (ae : arithmetic_expression) : (list byte_code_instruction) :=
+  match ae with
+  | Literal n => PUSH n :: nil
+  | Plus ae1 ae2 => (compile_aux ae1) ++ (compile_aux ae2) ++ (ADD :: nil)
+  | Minus ae1 ae2 => (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil)
+  end.
+
+Lemma fold_unfold_compile_aux_Literal :
+  forall (n : nat),
+    compile_aux (Literal n) = PUSH n :: nil.
+Proof.
+  fold_unfold_tactic compile_aux.
+Qed.
+
+Lemma fold_unfold_compile_aux_Plus :
+  forall (ae1 ae2 : arithmetic_expression),
+    compile_aux (Plus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (ADD :: nil).
+Proof.
+  fold_unfold_tactic compile_aux.
+Qed.
+
+Lemma fold_unfold_compile_aux_Minus :
+  forall (ae1 ae2 : arithmetic_expression),
+    compile_aux (Minus ae1 ae2) = (compile_aux ae1) ++ (compile_aux ae2) ++ (SUB :: nil).
+Proof.
+  fold_unfold_tactic compile_aux.
+Qed.
+
+Theorem compile_aux_satifies_the_specification_of_compile_aux :
+  specification_of_compile_aux compile_aux.
+Proof.
+  unfold specification_of_compile_aux.
+  split.
+  { exact fold_unfold_compile_aux_Literal.}
+  split.
+  { exact fold_unfold_compile_aux_Plus.}
+  exact fold_unfold_compile_aux_Minus.
+Qed.
+
+
 (* Task 5:
    a. time permitting, prove that the definition above specifies at most one function;
    b. implement this function using list concatenation, i.e., ++; and
@@ -774,6 +918,37 @@ Definition specification_of_compile (compile : source_program -> target_program)
     forall ae : arithmetic_expression,
       compile (Source_program ae) = Target_program (compile_aux ae).
 
+Theorem there_is_at_most_one_compile_function :
+  forall (f g : source_program -> target_program),
+    (specification_of_compile f) ->
+    (specification_of_compile g) ->
+    forall (sp : source_program),
+      f sp = g sp.
+Proof.
+  intros f g.
+  unfold specification_of_compile.
+  intros S_f S_g [ae].
+  rewrite -> (S_g compile_aux compile_aux_satifies_the_specification_of_compile_aux ae).
+  exact (S_f compile_aux compile_aux_satifies_the_specification_of_compile_aux ae).
+Qed.
+
+Definition compile (sp : source_program) : target_program :=
+  match sp with
+  | Source_program ae => Target_program (compile_aux ae)
+  end.
+
+Theorem compile_satifies_the_specification_of_compile :
+  specification_of_compile compile.
+Proof.
+  unfold specification_of_compile, compile.
+  intros compile_aux' S_compile_aux' ae.
+  rewrite -> (there_is_at_most_one_compile_aux_function
+           compile_aux' compile_aux
+           S_compile_aux' compile_aux_satifies_the_specification_of_compile_aux ae).
+  reflexivity.
+Qed.
+
+
 (* Task 6:
    a. time permitting, prove that the definition above specifies at most one function;
    b. implement this function; and
@@ -782,6 +957,120 @@ Definition specification_of_compile (compile : source_program -> target_program)
 
 (* ********** *)
 
+Fixpoint compile_alt_aux_acc (ae : arithmetic_expression) (acc : list byte_code_instruction) : (list byte_code_instruction) :=
+  match ae with
+  | Literal n => PUSH n :: acc
+  | Plus ae1 ae2 => (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (ADD :: acc)))
+  | Minus ae1 ae2 => (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (SUB :: acc)))
+  end.
+
+Lemma fold_unfold_compile_alt_aux_acc_Literal :
+  forall (n : nat)
+    (acc : list byte_code_instruction),
+    compile_alt_aux_acc (Literal n) acc = PUSH n :: acc.
+Proof.
+  fold_unfold_tactic compile_alt_aux_acc.
+Qed.
+
+Lemma fold_unfold_compile_alt_aux_acc_Plus :
+  forall (ae1 ae2 : arithmetic_expression)
+    (acc : list byte_code_instruction),
+    compile_alt_aux_acc (Plus ae1 ae2) acc = (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (ADD :: acc))).
+Proof.
+  fold_unfold_tactic compile_alt_aux_acc.
+Qed.
+
+Lemma fold_unfold_compile_alt_aux_acc_Minus :
+  forall (ae1 ae2 : arithmetic_expression)
+    (acc : list byte_code_instruction),
+    compile_alt_aux_acc (Minus ae1 ae2) acc = (compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 (SUB :: acc))).
+Proof.
+  fold_unfold_tactic compile_alt_aux_acc.
+Qed.
+
+Definition compile_alt_aux (ae : arithmetic_expression) : list byte_code_instruction :=
+  compile_alt_aux_acc ae nil.
+
+Lemma about_compile_alt_aux_acc :
+  forall (ae : arithmetic_expression)
+    (ds : list byte_code_instruction),
+    compile_alt_aux_acc ae ds = compile_alt_aux_acc ae nil ++ ds.
+  Proof.
+    intros ae.
+    induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2].
+    - intro ds.
+      Check (fold_unfold_compile_alt_aux_acc_Literal n ds).
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n ds).
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n nil).
+      rewrite -> fold_unfold_list_append_cons.
+      rewrite -> fold_unfold_list_append_nil.
+      reflexivity.
+    - intro ds.
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2).
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2).
+      rewrite -> (IHae2 (ADD :: ds)).
+      rewrite -> (IHae2 (ADD :: nil)).
+      rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ ADD :: ds)).
+      rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ ADD :: nil)).
+      rewrite <- 2 app_assoc.
+      rewrite -> fold_unfold_list_append_cons.
+      rewrite -> fold_unfold_list_append_nil.
+      reflexivity.
+    - intro ds.
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2).
+      rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2).
+      rewrite -> (IHae2 (SUB :: ds)).
+      rewrite -> (IHae2 (SUB :: nil)).
+      rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ SUB :: ds)).
+      rewrite -> (IHae1 (compile_alt_aux_acc ae2 nil ++ SUB :: nil)).
+      rewrite <- 2 app_assoc.
+      rewrite -> fold_unfold_list_append_cons.
+      rewrite -> fold_unfold_list_append_nil.
+      reflexivity.
+Qed.
+
+Theorem compile_alt_aux_satisifes_the_specification_of_compile_aux :
+  specification_of_compile_aux compile_alt_aux.
+Proof.
+  unfold specification_of_compile_aux, compile_alt_aux.
+  split.
+  { intros n.
+    rewrite -> (fold_unfold_compile_alt_aux_acc_Literal n nil).
+    reflexivity. }
+  split.
+  { intros ae1 ae2.
+    rewrite -> (fold_unfold_compile_alt_aux_acc_Plus ae1 ae2 nil).
+    Check about_compile_alt_aux_acc.
+    rewrite -> (about_compile_alt_aux_acc ae2 (ADD :: nil)).
+    rewrite -> (about_compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 nil ++ ADD :: nil)).
+
+    reflexivity. }
+  intros ae1 ae2.
+  rewrite -> (fold_unfold_compile_alt_aux_acc_Minus ae1 ae2 nil).
+  Check about_compile_alt_aux_acc.
+  rewrite -> (about_compile_alt_aux_acc ae2 (SUB :: nil)).
+  rewrite -> (about_compile_alt_aux_acc ae1 (compile_alt_aux_acc ae2 nil ++ SUB :: nil)).
+  reflexivity.
+Qed.
+
+Definition compile_alt (sp : source_program) : target_program :=
+  match sp with
+  | Source_program ae => Target_program (compile_alt_aux ae)
+  end.
+
+Theorem compile_alt_satisfies_the_specificiation_of_compile :
+  specification_of_compile compile_alt.
+Proof.
+  unfold specification_of_compile, compile_alt.
+  intros compile_aux' S_compile_aux ae.
+  rewrite -> (there_is_at_most_one_compile_aux_function
+               compile_aux' compile_alt_aux
+               S_compile_aux compile_alt_aux_satisifes_the_specification_of_compile_aux
+               ae
+    ).
+  reflexivity.
+Qed.
+
 (* Task 7:
    implement an alternative compiler
    using an auxiliary function with an accumulator
@@ -795,8 +1084,155 @@ Definition specification_of_compile (compile : source_program -> target_program)
 
 (* ********** *)
 
+Theorem the_commuting_diagram_evaluate_nat :
+  forall (ae : arithmetic_expression)
+    (n : nat)
+    (ds : data_stack),
+    evaluate ae = Expressible_nat n ->
+    fetch_decode_execute_loop (compile_aux ae) ds = OK (n :: ds).
+Proof.
+  intro ae.
+  induction ae as [n | ae1 IHae1 ae2 IHae2| ae1 IHae1 ae2 IHae2];
+    intros n' ds H_eval.
+  - rewrite -> fold_unfold_compile_aux_Literal.
+    rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+    unfold decode_execute.
+    rewrite -> fold_unfold_fetch_decode_execute_loop_nil.
+    rewrite -> fold_unfold_evaluate_Literal in H_eval.
+    injection H_eval as n_is_n'.
+    rewrite -> n_is_n'.
+    reflexivity.
+  - rewrite -> fold_unfold_compile_aux_Plus.
+    rewrite -> fold_unfold_evaluate_Plus in H_eval.
+    (* I need the 2 statements evaluate ae1 = Expressible_nat n *)
+    case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1.
+    + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2.
+      * injection H_eval as n1_plus_n2_is_n'.
+        Search fetch_decode_execute_loop.
+        destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [H_fdel_append_ae1 _].
+        rewrite -> (H_fdel_append_ae1
+                     (n1::ds)
+                     (IHae1 n1 ds eq_refl)
+          ).
+        destruct (about_fetch_decode_execute_loop (compile_aux ae2) (ADD :: nil) (n1 :: ds)) as [H_fdel_append_ae2 _].
+        rewrite -> (H_fdel_append_ae2
+                     (n2::n1::ds)
+                     (IHae2 n2 (n1::ds) eq_refl)
+          ).
+        rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+        unfold decode_execute.
+        rewrite -> fold_unfold_fetch_decode_execute_loop_nil.
+        rewrite -> n1_plus_n2_is_n'.
+        reflexivity.
+      * discriminate H_eval.
+    + discriminate H_eval.
+  - rewrite -> fold_unfold_compile_aux_Minus.
+    rewrite -> fold_unfold_evaluate_Minus in H_eval.
+    case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1.
+    + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2.
+      * case (n1 <? n2) eqn:H_n1_lt_n2.
+        ++ discriminate H_eval.
+        ++ injection H_eval as n1_minus_n2_is_n'.
+           destruct (about_fetch_decode_execute_loop
+                       (compile_aux ae1)
+                       (compile_aux ae2 ++ SUB :: nil) ds) as [H_fdel_append_ae1 _].
+           rewrite -> (H_fdel_append_ae1
+                        (n1::ds)
+                        (IHae1 n1 ds eq_refl)
+             ).
+           destruct (about_fetch_decode_execute_loop
+                       (compile_aux ae2)
+                       (SUB :: nil) (n1::ds)) as [H_fdel_append_ae2 _].
+           rewrite -> (H_fdel_append_ae2
+                        (n2::n1::ds)
+                        (IHae2 n2 (n1::ds) eq_refl)
+             ).
+           rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+           unfold decode_execute.
+           rewrite -> H_n1_lt_n2.
+           rewrite -> fold_unfold_fetch_decode_execute_loop_nil.
+           rewrite <- n1_minus_n2_is_n'.
+           reflexivity.
+      * discriminate H_eval.
+  + discriminate H_eval.
+Qed.
+
+Theorem the_commuting_diagram_evaluate_msg :
+  forall (ae : arithmetic_expression)
+    (s : string)
+    (ds : data_stack),
+    evaluate ae = Expressible_msg s ->
+    fetch_decode_execute_loop (compile_aux ae) ds = KO s.
+  Proof.
+    intro ae.
+    induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2]; intros s ds H_eval.
+    - rewrite -> fold_unfold_evaluate_Literal in H_eval.
+      discriminate H_eval.
+    - rewrite -> fold_unfold_evaluate_Plus in H_eval.
+      case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1.
+      + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2.
+        * discriminate H_eval.
+        * rewrite -> fold_unfold_compile_aux_Plus.
+          injection H_eval as s2_is_s.
+          destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [H_fdel_append _].
+          rewrite -> (H_fdel_append (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)).
+          destruct (about_fetch_decode_execute_loop (compile_aux ae2) (ADD::nil) (n1::ds)) as [_ H_fdel_append_KO].
+          rewrite -> (H_fdel_append_KO s2 (IHae2 s2 (n1::ds) eq_refl)).
+          rewrite -> s2_is_s.
+          reflexivity.
+      + injection H_eval as s1_is_s.
+          destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ ADD :: nil) ds) as [_ H_fdel_append_KO].
+          rewrite -> fold_unfold_compile_aux_Plus.
+          rewrite -> (H_fdel_append_KO s1 (IHae1 s1 ds eq_refl)).
+          rewrite -> s1_is_s.
+          reflexivity.
+    - rewrite -> fold_unfold_evaluate_Minus in H_eval.
+      case (evaluate ae1) as [n1 | s1] eqn:H_eval_ae1.
+      + case (evaluate ae2) as [n2 | s2] eqn:H_eval_ae2.
+        * case (n1 <? n2) eqn:H_n1_lt_n2.
+          ++ rewrite -> fold_unfold_compile_aux_Minus.
+             destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [H_fdel_append_ae1 _].
+             rewrite -> (H_fdel_append_ae1 (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)).
+             destruct (about_fetch_decode_execute_loop (compile_aux ae2) (SUB :: nil) (n1::ds)) as [H_fdel_append_ae2 _].
+             rewrite -> (H_fdel_append_ae2 (n2::n1::ds) (the_commuting_diagram_evaluate_nat ae2 n2 (n1::ds) H_eval_ae2)).
+             rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+             unfold decode_execute.
+             rewrite -> H_n1_lt_n2.
+             injection H_eval as n1_lt_n2_msg.
+             simpl (KO ("numerical underflow: -" ++ string_of_nat (n2 - n1))).
+             rewrite -> n1_lt_n2_msg.
+             reflexivity.
+          ++ discriminate H_eval.
+        * injection H_eval as s2_is_s.
+          ++ rewrite -> fold_unfold_compile_aux_Minus.
+             destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [H_fdel_append_ae1 _].
+             rewrite -> (H_fdel_append_ae1 (n1 :: ds) (the_commuting_diagram_evaluate_nat ae1 n1 ds H_eval_ae1)).
+             destruct (about_fetch_decode_execute_loop (compile_aux ae2) (SUB::nil) (n1::ds)) as [_ H_fdel_append_KO].
+             rewrite -> (H_fdel_append_KO s2 (IHae2 s2 (n1::ds) eq_refl)).
+             rewrite -> s2_is_s.
+             reflexivity.
+      + injection H_eval as s1_is_s.
+        rewrite -> fold_unfold_compile_aux_Minus.
+        destruct (about_fetch_decode_execute_loop (compile_aux ae1) (compile_aux ae2 ++ SUB :: nil) ds) as [_ H_fdel_append_KO].
+        rewrite -> (H_fdel_append_KO s1 (IHae1 s1 ds eq_refl)).
+        rewrite -> s1_is_s.
+        reflexivity.
+  Qed.
+
+Theorem the_commuting_diagram :
+  forall (sp : source_program),
+    interpret sp = run (compile sp).
+Proof.
+  intros [ae].
+  unfold interpret, compile,run.
+  case evaluate as [n | s] eqn:H_eval.
+  - rewrite -> (the_commuting_diagram_evaluate_nat ae n nil H_eval).
+    reflexivity.
+  - rewrite -> (the_commuting_diagram_evaluate_msg ae s nil H_eval).
+    reflexivity.
+Qed.
 (* Task 8 (the capstone):
-   Prove that interpreting an arithmetic expression gives the same result
+
    as first compiling it and then executing the compiled program.
 *)
 
@@ -829,6 +1265,33 @@ Fixpoint verify_aux (bcis : list byte_code_instruction) (n : nat) : option nat :
       end
   end.
 
+Definition fold_unfold_verify_aux_nil :
+  forall (n : nat),
+    verify_aux nil n = Some n.
+Proof.
+  fold_unfold_tactic verify_aux.
+Qed.
+
+Definition fold_unfold_verify_aux_cons :
+  forall (bci : byte_code_instruction)
+    (bcis : list byte_code_instruction)
+    (n : nat),
+    verify_aux (bci :: bcis) n =
+      match bci with
+        | PUSH _ =>
+          verify_aux bcis (S n)
+        | _ =>
+          match n with
+            | S (S n') =>
+              verify_aux bcis (S n')
+            | _ =>
+              None
+          end
+      end.
+Proof.
+  fold_unfold_tactic verify_aux.
+Qed.
+
 Definition verify (p : target_program) : bool :=
   match p with
   | Target_program bcis =>
@@ -849,19 +1312,233 @@ Definition verify (p : target_program) : bool :=
    Prove that the compiler emits code
    that is accepted by the verifier.
 *)
-
+Lemma about_verify_aux_some :
-(*
+  forall (bci1s bci2s : list byte_code_instruction)
-Theorem the_compiler_emits_well_behaved_code :
+    (n n' : nat),
-  forall ae : arithmetic_expression,
+    (verify_aux bci1s n) = Some n' ->
-    verify (compile ae) = true.
+    (verify_aux (bci1s ++ bci2s) n) = (verify_aux bci2s n').
 Proof.
-Abort.
+  intros bci1s.
-*)
+  induction bci1s as [ | bci bci1s' IHbci1s' ].
+  - intros bci2s n n' H_verify_aux.
+    rewrite -> fold_unfold_verify_aux_nil in H_verify_aux.
+    injection H_verify_aux as n_is_n'.
+    rewrite -> fold_unfold_list_append_nil.
+    rewrite -> n_is_n'.
+    reflexivity.
+  - intros bci2s n n' H_verify_aux.
+    rewrite -> fold_unfold_list_append_cons.
+    rewrite -> fold_unfold_verify_aux_cons.
+    case bci as [ x |  | ] eqn:H_bci.
+    + rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+      rewrite -> (IHbci1s' bci2s (S n) n' H_verify_aux).
+      reflexivity.
+    + case n as [ | [ | n'' ] ].
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        discriminate H_verify_aux.
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        discriminate H_verify_aux.
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        rewrite -> (IHbci1s' bci2s (S n'') n' H_verify_aux).
+        reflexivity.
+    + case n as [ | [ | n'' ] ].
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        discriminate H_verify_aux.
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        discriminate H_verify_aux.
+      * rewrite -> fold_unfold_verify_aux_cons in H_verify_aux.
+        rewrite -> (IHbci1s' bci2s (S n'') n' H_verify_aux).
+        reflexivity.
+Qed.
+
+Lemma compile_aux_emits_one_value :
+  forall (ae : arithmetic_expression)
+    (n : nat),
+    verify_aux (compile_aux ae) n = Some (S n).
+Proof.
+  intro ae.
+  induction ae as [n | ae1 IHae1 ae2 IHae2 | ae1 IHae1 ae2 IHae2]; intro n'.
+  - rewrite -> fold_unfold_compile_aux_Literal.
+    rewrite -> fold_unfold_verify_aux_cons.
+    rewrite -> fold_unfold_verify_aux_nil.
+    reflexivity.
+  - rewrite -> fold_unfold_compile_aux_Plus.
+    rewrite -> (about_verify_aux_some
+             (compile_aux ae1)
+             (compile_aux ae2 ++ ADD :: nil)
+             n' (S n')
+             (IHae1 n')).
+    rewrite -> (about_verify_aux_some
+             (compile_aux ae2)
+             (ADD :: nil)
+             (S n') (S (S n'))
+             (IHae2 (S n'))).
+    rewrite -> fold_unfold_verify_aux_cons.
+    rewrite -> fold_unfold_verify_aux_nil.
+    reflexivity.
+  - rewrite -> fold_unfold_compile_aux_Minus.
+    rewrite -> (about_verify_aux_some
+                 (compile_aux ae1)
+                 (compile_aux ae2 ++ SUB :: nil)
+                 n' (S n')
+                 (IHae1 n')).
+    rewrite -> (about_verify_aux_some
+             (compile_aux ae2)
+             (SUB :: nil)
+             (S n') (S (S n'))
+             (IHae2 (S n'))).
+    rewrite -> fold_unfold_verify_aux_cons.
+    rewrite -> fold_unfold_verify_aux_nil.
+    reflexivity.
+Qed.
+
+
+
+Theorem the_compiler_emits_well_behaved_code :
+  forall sp : source_program,
+    verify (compile sp) = true.
+Proof.
+  intros [ae].
+  unfold verify, compile.
+rewrite -> (compile_aux_emits_one_value ae 0).
+reflexivity.
+Qed.
+
 
 (* Subsidiary question:
    What is the practical consequence of this theorem?
 *)
 
+Definition alternative_specification_of_run (run : target_program -> expressible_value) :=
+  forall fetch_decode_execute_loop : list byte_code_instruction -> data_stack -> result_of_decoding_and_execution,
+    specification_of_fetch_decode_execute_loop fetch_decode_execute_loop ->
+    forall (bcis : list byte_code_instruction),
+      (fetch_decode_execute_loop bcis nil = OK nil ->
+       run (Target_program bcis) = Expressible_msg "no result on the data stack")
+      /\
+      (forall (n : nat),
+         fetch_decode_execute_loop bcis nil = OK (n :: nil) ->
+         run (Target_program bcis) = Expressible_nat n)
+      /\
+      (forall (n n' : nat)
+              (ds'' : data_stack),
+         fetch_decode_execute_loop bcis nil = OK (n :: n' :: ds'') ->
+         run (Target_program bcis) = Expressible_msg "too many results on the data stack")
+      /\
+      (forall (s : string),
+         fetch_decode_execute_loop bcis nil = KO s ->
+         run (Target_program bcis) = Expressible_msg s).
+
+Theorem run_satisfies_the_alternative_specification_of_run :
+  alternative_specification_of_run run.
+Proof.
+  unfold alternative_specification_of_run.
+  intros fdel' S_fdel' bcis.
+  split.
+  { intros H_fdel_nil.
+    unfold run.
+    rewrite <- (there_is_at_most_one_fetch_decode_execute_loop
+             fdel' fetch_decode_execute_loop
+             S_fdel' fetch_decode_execute_loop_satifies_the_specification
+             bcis nil
+          ).
+    rewrite -> H_fdel_nil.
+    reflexivity. }
+  split.
+  { intros n H_fdel_one.
+    unfold run.
+    rewrite <- (there_is_at_most_one_fetch_decode_execute_loop
+             fdel' fetch_decode_execute_loop
+             S_fdel' fetch_decode_execute_loop_satifies_the_specification
+             bcis nil
+          ).
+    rewrite -> H_fdel_one.
+    reflexivity.
+  }
+  split.
+  { intros n n' ds H_fdel_many.
+    unfold run.
+    rewrite <- (there_is_at_most_one_fetch_decode_execute_loop
+             fdel' fetch_decode_execute_loop
+             S_fdel' fetch_decode_execute_loop_satifies_the_specification
+             bcis nil
+          ).
+    rewrite -> H_fdel_many.
+    reflexivity.
+  }
+  intros s H_fdel_KO.
+  unfold run.
+  rewrite <- (there_is_at_most_one_fetch_decode_execute_loop
+               fdel' fetch_decode_execute_loop
+               S_fdel' fetch_decode_execute_loop_satifies_the_specification
+               bcis nil
+    ).
+  rewrite -> H_fdel_KO.
+  reflexivity.
+Qed.
 (* ********** *)
 
+Theorem there_is_at_most_one_run_function_with_this_alternative :
+  forall run1 run2 : target_program -> expressible_value,
+    alternative_specification_of_run run1 ->
+    alternative_specification_of_run run2 ->
+    forall tp :
+
+ target_program,
+      run1 tp = run2 tp.
+Proof.
+  intros run1 run2 S_run1 S_run2 [bcis].
+
+  case (fetch_decode_execute_loop bcis nil) as [ ds | s] eqn:H_fdel.
+  - case ds as [ | n ds' ] eqn:H_ds.
+    + destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [H_run1_nil _].
+      destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [H_run2_nil _].
+      rewrite -> (H_run1_nil H_fdel).
+      rewrite -> (H_run2_nil H_fdel).
+      reflexivity.
+    + case ds' as [ | n' ds'' ] eqn:H_ds'.
+      * destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [H_run1_one _]].
+        destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [H_run2_one _]].
+        rewrite -> (H_run1_one n H_fdel).
+        rewrite -> (H_run2_one n H_fdel).
+        reflexivity.
+      * destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [H_run1_many _]]].
+        destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [H_run2_many _]]].
+        rewrite -> (H_run1_many n n' ds'' H_fdel).
+        rewrite -> (H_run2_many n n' ds'' H_fdel).
+        reflexivity.
+  - destruct (S_run1 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [_ H_run1_KO]]].
+    destruct (S_run2 fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification bcis) as [_ [_ [_ H_run2_KO]]].
+    rewrite -> (H_run1_KO s H_fdel).
+    rewrite -> (H_run2_KO s H_fdel).
+    reflexivity.
+Qed.
+
+Proposition equivalence_of_the_two_specifications :
+  forall run : target_program -> expressible_value,
+    specification_of_run run <-> alternative_specification_of_run run.
+Proof.
+  intro run'.
+  unfold specification_of_run.
+  unfold alternative_specification_of_run.
+  split.
+  - intro S_run.
+    assert (S_run := S_run fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification).
+    destruct S_run as [S_run_nil [S_run_one [S_run_many S_run_KO]]].
+    intros fdel S_fdel bcis.
+    rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis).
+    split.
+    { intros H_fdel_nil.
+      rewrite -> (S_run_nil bcis H_fdel_nil).
+      reflexivity. }
+    split.
+    { intros n H_fdel_one.
+      rewrite -> (S_run_one bcis n H_fdel_one).
+      reflexivity. }
+    split.
+    { intros n n' H_fdel_many.
+      rewrite -> (S_run_many bcis n n' H_fdel_many).
+      reflexivity. }
+    split.
+
 (* end of term-project.v *)