(************************************************************************* * Catherine Dubois - tutorial TOOLS 2011 - july 2011 * This file is a Coq proof of the compiler correctness presented in * Graham Hutton, Joel Wright: Compiling Exceptions Correctly. MPC 2004: 211-227 * Part : simple language with only arithmetic expressions ***************************************************************************) Inductive expr : Set := Val : nat -> expr | Add : expr -> expr -> expr. Fixpoint eval (e : expr) : nat := match e with Val i => i | Add e1 e2 => eval e1 + eval e2 end. Eval compute in eval (Add (Val 5) (Add (Val 4) (Val 3))). Require Import List. Definition stack := (list nat). Inductive Op : Set := PUSH : nat -> Op | ADD : Op. Definition code := list Op. Inductive exec : code -> stack -> stack -> Prop := exnil : forall s, exec nil s s | expush : forall cs i s fs, exec cs (i::s) fs -> exec((PUSH i)::cs) s fs | exadd : forall cs i j s fs, exec cs ((j+i)::s) fs -> exec (ADD::cs) (i :: j :: s) fs . Lemma exec_det : forall ops s s1 s2, exec ops s s1 -> exec ops s s2 -> s1=s2. induction 1 ; intros. (*nil*) inversion_clear H. reflexivity. (*Push _ ::r*) inversion_clear H0. auto. (*Add::r*) inversion_clear H0. auto. Qed. Fixpoint comp (e : expr) := match e with Val i => (PUSH i)::nil | Add e1 e2 => comp e1 ++ comp e2 ++ (ADD::nil) end. Eval compute in comp (Add (Val 5) (Add (Val 4) (Val 3))). Definition my_ex := PUSH 5:: PUSH 4 :: PUSH 3 :: ADD :: ADD :: nil. Lemma exec_my_ex : exec my_ex nil (12::nil). unfold my_ex. repeat constructor. Qed. Lemma distributivity : forall ops1 ops2 s sf1 sf2, exec ops1 s sf1 -> exec ops2 sf1 sf2 -> exec (ops1++ops2) s sf2. induction ops1;intros;inversion_clear H;simpl. assumption. constructor. apply IHops1 with (sf1:=sf1); assumption. constructor. apply IHops1 with (sf1:=sf1); assumption. Qed. Theorem comp_correctness2: forall e s, exec (comp e) s ((eval e)::s). induction e;simpl;intros. (*Val*) constructor. constructor. (*Add*) apply distributivity with (sf1:=eval e1 :: s);auto. apply distributivity with (sf1:=eval e2 :: eval e1 :: s);auto. constructor. constructor. Qed. Theorem correctness : forall e, exec (comp e) nil ((eval e)::nil). intro e;exact (comp_correctness2 e nil). Qed. (* A more general theorem of correctness *) Lemma my_rew_app : forall (A : Set), forall (l1 l2 : list A), forall a, (l1 ++ a::nil)++l2 = l1 ++ a::l2. induction l1. simpl;auto. simpl;intros. rewrite IHl1. reflexivity. Qed. Ltac rew_app H := rewrite <- app_ass in H ; rewrite my_rew_app in H ;rewrite app_ass in H. Theorem gen_comp_correctness: forall e ops s sf, exec ((comp e)++ops) s sf -> exec ops ((eval e)::s) sf. induction e;simpl;intros. (*Val*) inversion_clear H;assumption. (*Add*) assert (exec (ADD::ops) ((eval e2)::(eval e1)::s) sf) as Hyp1. apply IHe2. apply IHe1. rew_app H. assumption. inversion_clear Hyp1. assumption. Qed.