td6 : solution exos 1 to 4

solutions/td6.v

+(* TD6 *)
+
+Require Import Arith List Bool NArith.
+Import ListNotations.
+
+Set Implicit Arguments.
+
+(* Exercise 1 *)
+
+Inductive expr :=
+| Num  : nat -> expr            (* Numerical constant:  n       *)
+| Plus : expr -> expr -> expr   (* Sum expression:      e1 + e2 *)
+| Mult : expr -> expr -> expr.  (* Product expression:  e1 * e2 *)
+
+Fixpoint eval (e:expr) : nat :=
+ match e with
+ | Num n => n
+ | Plus e e' => eval e + eval e'
+ | Mult e e' => eval e * eval e'
+ end.
+
+Compute eval (Plus (Mult (Num 3) (Num 5)) (Num 7)).  (* 3*5+7 *)
+
+(* Exercise 2 *)
+
+Inductive inst :=
+ | PUSH : nat -> inst
+ | ADD : inst
+ | MUL : inst.
+
+Definition prog := list inst.
+
+Definition stack := list nat.
+
+(* Exercise 3 *)
+
+Fixpoint exec_inst (i:inst) (stk:stack) : stack :=
+ match i with
+ | PUSH n => n::stk
+ | ADD => match stk with
+          | e1::e2::stk' => (e1+e2)::stk'
+          | _ => [] (* or stk or whatever you prefer *)
+          end
+ | MUL => match stk with
+          | e1::e2::stk' => (e1*e2)::stk'
+          | _ => []
+          end
+ end.
+
+Fixpoint exec_prog (p:prog) (stk:stack) : stack :=
+ match p with
+ | [] => stk
+ | i::p' => let stk' := exec_inst i stk in
+            exec_prog p' stk'
+ end.
+
+(* Exercise 4 *)
+
+Fixpoint compile (e:expr) : prog :=
+ match e with
+ | Num n => [PUSH n]
+ | Plus e e' => compile e ++ compile e' ++ [ADD]
+ | Mult e e' => compile e ++ compile e' ++ [MUL]
+ end.
+
+Definition example_expr := Plus (Mult (Num 3) (Num 5)) (Num 7).
+Compute compile example_expr. (* 3*5+7 *)
+Compute exec_prog (compile example_expr) []. (* [22] *)
+
+(* First invariant, the easy one :
+
+   forall e, exec_prog (compile e) [] = [eval e]
+
+   We'll see how to prove it later, but for now let's test it
+   in a boolean way. *)
+
+Definition check_invariant1 e :=
+ match exec_prog (compile e) [] with
+ | [n] => n =? eval e
+ | _ => false
+ end.
+
+Compute check_invariant1 example_expr.
+
+(* A generalized invariant, holding for any initial stack *)
+
+Compute exec_prog (compile example_expr) [1;2;3;4]. (* [22; 1; 2; 3; 4] *)
+
+(* Hence :
+
+   forall e, forall stk, exec_prog (compile e) stk = (eval e)::stk
+
+   It's this version that is actually provable (by induction), and then the
+   previous one is just a consequence.
+
+   Boolean test for the moment :
+*)
+
+Fixpoint eqb_list (l l' : list nat) :=
+ match l, l' with
+ | [], [] => true
+ | x::l, x'::l' => (x =? x') && (eqb_list l l')
+ | _, _ => false
+ end.
+
+Definition check_invariant2 e stk :=
+ eqb_list (exec_prog (compile e) stk) ((eval e)::stk).
+
+Compute check_invariant2 example_expr [].
+Compute check_invariant2 example_expr [1;2;3;4].
+
+(* As a teaser, the actual Coq proof. More on that in January *)
+
+Lemma exec_prog_app p p' stk :
+ exec_prog (p++p') stk = exec_prog p' (exec_prog p stk).
+Proof.
+ revert stk. induction p; simpl; auto.
+Qed.
+
+Lemma compile_ok :
+ forall e stk, exec_prog (compile e) stk = (eval e)::stk.
+Proof.
+ induction e; intros; simpl.
+ - trivial.
+ - rewrite !exec_prog_app, IHe1, IHe2. simpl. f_equal. apply Nat.add_comm.
+ - rewrite !exec_prog_app, IHe1, IHe2. simpl. f_equal. apply Nat.mul_comm.
+Qed.
+
+Lemma compile_okbis :
+ forall e, exec_prog (compile e) [] = [eval e].
+Proof.
+ intros. apply compile_ok.
+Qed.