Require Import ZArith List String. Require Import Semantics. Open Scope Z_scope. Open Scope list_scope. Open Scope string_scope. (** the expression "x + 2" *) Example exp1 : expr := zplus "x" 2. Goal exp1 = apply Plus (var "x") (num 2). reflexivity. Save toto. (** In Coq, all functions are total *) Compute (4/0). (** in order to have a cleaner semantics, we use option type *) Definition strict_div x y : option Z := if Z.eqb y 0 then None else Some (x/y). Compute strict_div 6 4. Compute strict_div 6 0. (* Definition bind {A B:Type} (v:option A)(f:A->option B) : option B := match v with Some x => f x | None => None end. *) Definition f0 (z:Z) := bind (strict_div 1000 z) (fun r => ret (3 + z)). Compute f0 7. Compute f0 0. (** Evaluation of expressions *) (** let's try to define evaluation of expressions without variables *) Fixpoint vfree_eval (e:expr) : option Z := match e with var _ => None | num z => ret z | apply Plus e1 e2 => bind (vfree_eval e1) (fun v1 => bind (vfree_eval e2) (fun v2 => ret (v1 + v2))) | apply Minus e1 e2 => bind (vfree_eval e1) (fun v1 => bind (vfree_eval e2) (fun v2 => ret (v1 - v2))) | apply Mult e1 e2 => bind (vfree_eval e1) (fun v1 => bind (vfree_eval e2) (fun v2 => ret (v1 * v2))) | apply Div e1 e2 => bind (vfree_eval e2) (fun v2 => if Z.eqb v2 0 then None else bind (vfree_eval e1) (fun v1 => ret (v1/v2))) end. Compute vfree_eval (zplus 5 (zdiv 6 2)). Compute vfree_eval (zmult 0 "x"). (** We can simplify and extend the evaluation to expressions containing variables *) Example e0 : env := (("x",4)::("y",3)::("z",6)::nil). Compute lookup e0 "y". Compute lookup e0 "z". Compute (op2fun Plus 2 3). Compute (op2fun Div 3 0). Compute af e0 (zmult "x" (zplus "y" "z")). Compute af e0 (zmult "t" 8). Compute bf e0 (blt "x" 5). Compute bf e0 (blt "x" (zdiv 5 (zminus "y" "y"))). Compute uf e0 "y" 78. Compute uf e0 "t" 0. Print e0. Definition p1:= sequence (assign "z" "x") (sequence (assign "x" "y") (assign "y" "z")). Compute f_star 3 e0 p1. Compute f_star 6 e0 p1. (** %\begin{verbatim} i := 0; x := 0; d := 1; while i < arg do x := x + d; d := d + 2 ; i := i + 1 done \end{verbatim}% *) (** ** Its abstract syntax *) Example sqr: instr := sequence (assign "i" 0) (sequence (assign "x" 0) (sequence (assign "d" 1) (while (blt "i" "arg") (sequence (assign "x" (zplus "x" "d")) (sequence (assign "d" (zplus "d" 2)) (assign "i" (zplus "i" 1))))))). (** ** a simple environment *) Example rho := (("x",0)::("d",0)::("i",0)::("arg",6)::nil). Compute f_star 23 rho sqr. Compute f_star 83 rho sqr. Example loop := while btrue skip. Compute f_star 567 nil loop. (** projects : 1: add if-then-else construct (quite easy) or 2: add a construct corresponding to the declaration of local variables (initialised to 0) or 3: add a break construct (difficult) For each project, the task is easy to define: the most part of the "Semantics" module must be adapted to your extension. Build also a module of examples for demos *) (* Expressing partial functions with predicates (i.e. relations) *) Check op2rel Plus 2 6 8. Check op2rel Div 6 0 54. Example E2_6 : op2rel Plus 2 6 8. Proof. compute. reflexivity. Qed. Example Div0 : forall x y, ~ op2rel Div x 0 y. Proof. intros x y H. vm_compute in H. discriminate. (* Note : Professionals would have simply written intros x y H;discriminate. *) Qed. (** The relational view of lookup *) Example rho0 : env := ("i",0)::("x",0)::("d",1)::nil. Example mapsTo1 : mapsTo "d" 1 rho0. unfold rho0. right. discriminate. right. discriminate. left. Qed. Example mapsTo2 : forall z, ~ mapsTo "foo" z rho0. (** the bad way *) unfold rho0. intros z Hz. destruct (mapsTo_inv _ _ _ _ _ Hz). destruct H as [H0 _]; discriminate. destruct H as [_ H0]. destruct (mapsTo_inv _ _ _ _ _ H0). destruct H as [H1 _]; discriminate. destruct H as [_ H1]. destruct (mapsTo_inv _ _ _ _ _ H1). destruct H as [H2 _]; discriminate. destruct H as [_ H2]. inversion H2. Qed. (* ugly, isn't it ? *) Example mapsTo1' : mapsTo "d" 1 rho0. rewrite lookup_reflect. reflexivity. Qed. Example mapsTo2' : forall z, ~ mapsTo "foo" z rho0. Proof. intros z;rewrite lookup_reflect. discriminate. Qed. (** evaluation of an expression (propositional view) *) Example expr1 := (zdiv (zplus "x" 3) "d"). Example eval1: aeval rho0 expr1 3. Proof. unfold rho0, expr1. constructor 3 with 3 1. constructor 3 with 0 3. repeat constructor. discriminate. repeat constructor. repeat constructor. repeat (constructor; auto;try discriminate). constructor. Qed. (*** ouf ! *) Example eval1' : aeval rho0 expr1 3. SearchAbout [af aeval]. rewrite <- af_reflect. reflexivity. (* waoh *) Qed. Example E6 : forall v, ~ aeval nil (zplus "x" 6) v. intros v H;inversion H. inversion H4. inversion H10. Qed. Lemma E6' : forall v, ~ aeval nil (zplus "x" 6) v. Proof. intro v. rewrite <- af_reflect. (* simpl. *) discriminate. Qed. (* exercise ? *) Definition undefined (v:string)(r:env) := match lookup r v with Some _ => false | None => true end. Fixpoint occurs (v:string)(e : expr) := match e with num _ => false | var w => if string_dec v w then true else false | apply _ e1 e2 => occurs v e1 || occurs v e2 end. Lemma undefined_None : forall v r e, occurs v e = true -> undefined v r = true -> af r e = None. induction e;simpl. destruct (string_dec v s). unfold undefined. subst s;case_eq (lookup r v);auto. intros;discriminate. discriminate. discriminate. SearchAbout [orb or]. rewrite Bool.orb_true_iff. destruct 1. intro H0; rewrite IHe1;auto. intro H0; rewrite IHe2;auto. simpl. case (af r e1);simpl;auto. Qed. (** Evaluation of boolean expressions : logical view *) Example E7 : beval rho (blt 0 "arg") true. repeat econstructor. discriminate. discriminate. discriminate. Qed. Example E8 : beval rho (beq 0 "arg") false. econstructor. econstructor. econstructor. econstructor. discriminate. right. discriminate. right. discriminate. left;auto. discriminate. Qed. Compute bf rho (beq 0 "arg"). Compute bf nil (beq 0 "arg"). Example E8' : beval rho (beq 0 "arg") false. rewrite <- bf_reflect. reflexivity. Qed. (** big step semantics *) Example E9 : s_update rho "i" 4 (("x",0)::("d",0)::("i",4)::("arg",6)::nil). unfold rho;repeat (right; [|discriminate]). left. Qed. Example E10 : exec (("x",7)::("y",10)::nil) (assign "x" (zplus "x" "y")) (("x",17)::("y",10)::nil). eapply SN2. econstructor. SearchAbout[aeval af]. rewrite <- af_reflect. reflexivity. rewrite <- af_reflect;reflexivity. red. reflexivity. constructor. Qed. Example E11 : exec (("x",7)::("y",10)::("tmp",0)::nil) (sequence (assign "tmp" "x") (sequence (assign "x" "y") (assign "y" "tmp"))) (("x",10)::("y",7)::("tmp",7)::nil). repeat econstructor; try discriminate. Qed. Example prog8 : instr := while (blt 0 "x") (sequence (assign "y" (zmult 2 "y")) (assign "x" (zminus "x" 1))). Example E12 : exec (("x",3)::("y",1)::nil) prog8 (("x",0)::("y",8)::nil). unfold prog8;econstructor. rewrite <- bf_reflect;reflexivity. econstructor. econstructor. repeat econstructor; try discriminate. simpl; repeat econstructor; try discriminate. repeat econstructor; try discriminate. simpl. econstructor. rewrite <- bf_reflect;reflexivity. econstructor. econstructor. repeat econstructor; try discriminate. simpl. eright. eleft. discriminate. econstructor. repeat econstructor; try discriminate. repeat econstructor; try discriminate. simpl. econstructor. rewrite <- bf_reflect;reflexivity. econstructor. econstructor. repeat econstructor; try discriminate. simpl. eright. eleft. discriminate. econstructor. repeat econstructor; try discriminate. repeat econstructor; try discriminate. simpl. apply SN5. rewrite <- bf_reflect;reflexivity. Qed. Example E12' : exec (("x",3)::("y",1)::nil) prog8 (("x",0)::("y",8)::nil). apply f_star_exec with (n:=34%nat). reflexivity. Qed. (* Hi, I'm here *) Compute f_star 10 rho sqr. Compute f_star 200 rho sqr. Compute f_star 200 (("arg",6)::nil) sqr. Example ae1 := apply Plus (var "x") (num 42). Example exp11 : expr := zmult (num 3) (zplus (num 7) (var "x")). Example E3' : op2rel Plus 4 5 9. Proof. reflexivity. Qed. Example E4' : forall z z', ~ op2rel Div z 0 z'. Proof. intros z z' H; vm_compute in H; discriminate. Qed. Example rho1 : env := (("x",4)::("y",8)::nil). Compute lookup rho1 "x". Compute lookup rho1 "foo". Example E5': aeval rho1 exp11 33. unfold exp1;cpp;repeat econstructor. Qed. Example preds : p_env := ("wd",(fun zs => True)):: ("even",(fun zs:list Z => (match zs with z::nil => Z.modulo z 2 = 0 | _ => False end)))::nil. Example as1 : assert := a_b (blt (var "x") (num 10)). Example ins1 := (prec as1) (a_assign "x" (zplus "x" 1)). Compute vcg ins1 (blt "x" 12). (* vcg ( {(*@ x < 8 *); x := x+1} (*@ x < 10 *)) *) Compute vcg (prec (blt "x" 8) (a_assign "x" (zplus "x" 1))) (blt "x" 10). (* (x < 8 ==> (x + 1 < 10)) :: nil *) (* vcg { (*@ y < x *); z:= x ; x := y ; y := z} (*@ x < y *) *) Compute vcg (prec (blt "y" "x") (a_sequence (a_assign "z" "x") (a_sequence (a_assign "x" "y") (a_assign "y" "z")))) (blt "x" "y"). (* = c_imp (blt "y" "x") (blt "y" "x") :: nil : list condition *) Example asqr: a_instr := (a_sequence (a_assign "i" 0) (a_sequence (a_assign "x" 0) (a_sequence (a_assign "d" 1) (a_while (blt "i" "arg") (beq "x" (zmult "i" "i")) (a_sequence (a_assign "x" (zplus "x" "d")) (a_sequence (a_assign "d" (zplus "d" 2)) (a_assign "i" (zplus "i" 1)))))))). Definition vcs1 := vcg asqr (beq "x" (zmult "arg" "arg")). Compute vcs1. (* c_imp (a_conj (a_not (blt "i" "arg")) (beq "x" (zmult "i" "i"))) (beq "x" (zmult "arg" "arg")) :: c_imp (a_conj (blt "i" "arg") (beq "x" (zmult "i" "i"))) (beq (zplus "x" "d") (zmult (zplus "i" 1) (zplus "i" 1))) :: nil *) Goal valid_l nil vcs1 . unfold vcs1, valid_l;simpl. intros g;repeat split. destruct 1. (* g : string -> Z H : ~ g "i" < g "arg" H0 : g "x" = g "i" * g "i" ============================ g "x" = g "arg" * g "arg" *) Abort. (* let us confirm our first impression *) Goal ~ valid_l nil vcs1 . unfold vcs1, valid_l;simpl. intro Habs. SearchAbout (string -> Z). generalize (Habs (e_to_f (("arg",5)::("i",7)::("x",49)::nil) (fun s=> 0))). simpl. intros [H1 [H2 _]]. contradict H1. omega. Qed. (* OK, let us add new assertions *) Example asqr2: a_instr := (a_sequence (a_assign "i" 0) (a_sequence (a_assign "x" 0) (a_sequence (a_assign "d" 1) (a_while (blt "i" "arg") (a_conj (beq "x" (zmult "i" "i")) (a_not (blt "arg" "i"))) (a_sequence (a_assign "x" (zplus "x" "d")) (a_sequence (a_assign "d" (zplus "d" 2)) (a_assign "i" (zplus "i" 1)))))))). Compute vcg asqr2 (beq "x" (zmult "arg" "arg")). (* = c_imp (a_conj (a_not (blt "i" "arg")) (a_conj (beq "x" (zmult "i" "i")) (a_not (blt "arg" "i")))) (beq "x" (zmult "arg" "arg")) :: c_imp (a_conj (blt "i" "arg") (a_conj (beq "x" (zmult "i" "i")) (a_not (blt "arg" "i")))) (a_conj (beq (zplus "x" "d") (zmult (zplus "i" 1) (zplus "i" 1))) (a_not (blt "arg" (zplus "i" 1)))) :: nil : list condition *) Goal valid_l nil (vcg asqr2 (beq "x" (zmult "arg" "arg"))). unfold asqr2, valid_l;simpl. intros g;repeat split. destruct 1 as [H1 [H2 H3]]. assert (g "i" = g "arg") by omega. rewrite <- H;auto. (* ok for this noe, next, please *) (* g : string -> Z H : g "i" < g "arg" /\ g "x" = g "i" * g "i" /\ ~ g "arg" < g "i" ============================ g "x" + g "d" = (g "i" + 1) * (g "i" + 1) *) destruct H as [H1 [H2 H3]]. (* argh, we know nothing about "d" *) Abort. Example asqr3: a_instr := (a_sequence (a_assign "i" 0) (a_sequence (a_assign "x" 0) (a_sequence (a_assign "d" 1) (a_while (blt "i" "arg") (a_conj (beq "x" (zmult "i" "i")) (a_conj (a_not (blt "arg" "i")) (beq "d" (zplus "i" (zplus "i" 1))))) (a_sequence (a_assign "x" (zplus "x" "d")) (a_sequence (a_assign "d" (zplus "d" 2)) (a_assign "i" (zplus "i" 1)))))))). Definition asqr3' := add_precond asqr3 (beq "x" (zmult "arg" "arg")). Compute asqr3'. About i_a. (* About the precondition generated from the program *) Goal forall g, i_a nil g (pc asqr3 (beq "x" (zmult "arg" "arg")) ) <-> (0 <= g "arg" ). intros;simpl. split;omega. Qed. Lemma asq3_v: valid_l nil (vcg asqr3 (beq "x" (zmult "arg" "arg"))). unfold asqr3, valid_l;simpl. intros g;repeat split. destruct 1 as [H1 [H2 [H3 H4]]]. assert (g "i" = g "arg") by omega. rewrite <- H;auto. destruct H as [H1 [H2 [H3 H4]]]. rewrite H2,H4;ring. destruct H as [H1 [H2 [H3 H4]]]. omega. destruct H as [H1 [H2 [H3 H4]]]. rewrite H4. ring. Qed. Theorem Partial_correction : correct nil asqr3 (beq "x" (zmult "arg" "arg")). About OK. apply OK. apply asq3_v. Qed. Print correct. (* correct = fun (ps : p_env) (i : a_instr) (A : assert) => let i' := un_annot i in let pred := pc i A in forall (g : string -> Z) (r1 r2 : env), exec r1 i' r2 -> i_a ps (r1 @ g) pred -> i_a ps (r2 @ g) A : p_env -> a_instr -> assert -> Prop *) (* Note that the precondition generated by pc is quite useful *) Lemma counter_example : ~ ( forall (g : string -> Z) (r1 r2 : env), exec r1 (un_annot asqr3) r2 -> i_a nil (r2 @ g) (beq "x" (zmult "arg" "arg"))). Proof. intros H. generalize (H (fun s => 0) (("x",0)::("i",0)::("d",0)::("arg",-5)::nil) (("x",0)::("i",0)::("d",1)::("arg",-5)::nil)). intro. simpl in H0. assert (0 <> 25) by discriminate. apply H1;apply H0. apply f_star_exec with 45%nat. simpl. trivial. Qed. Lemma sqr_loops : forall n, f_star (7+n) (("d",0)::("x",0)::("i",0) ::("arg",-6)::nil) sqr = Some (("d", 1) :: ("x", 0) :: ("i", 0) :: ("arg", -6) :: nil, skip). Proof. induction n;simpl;auto. Qed. Goal sqr = un_annot asqr3. reflexivity. Qed. (* miscellaneous *) Eval simpl in (pc asqr3 (beq "x" (zmult "arg" "arg"))). Compute pc asqr3 (beq "x" (zmult "arg" "arg")). Compute bf rho1 (beq "y" (zplus "x" "x")). Compute bf rho1 (beq 1 (zdiv 100 (zminus "x" "x"))). Compute bf rho1 (beq 1 (zdiv 100 (zplus "x" "x"))). Compute bf rho1 (beq 1 (zdiv "y" (zplus "x" "x"))). Compute bf rho1 (bor (beq (zdiv 5 0) 33) btrue). Compute bf rho1 (bor btrue (beq (zdiv 5 0) 33)). Compute op2fun Plus 6 7. Compute op2fun Div 8 2. Compute op2fun Div 7 0. Compute f_p preds "even" (Some (4::nil)). Compute f_p preds "even" (Some (5::nil)). Goal f_p preds "even" (Some (4::nil)). reflexivity. Qed. Goal ~ f_p preds "even" (Some (5::nil)). intro;discriminate. Qed. Goal ~ f_p preds "wd" (lf' (fun _ => 0) ((zdiv 3 0)::nil)). simpl. tauto. Qed. Goal f_p preds "wd" (lf' (fun _ => 0) ((zdiv 3 2)::nil)). simpl. trivial. Qed. Goal f_p preds "even" (lf' (fun _ => 0) ((zdiv 8 2)::nil)). simpl. trivial. Qed. Goal ~ f_p preds "even" (lf' (fun _ => 0) ((zdiv 10 2)::nil)). simpl. vm_compute. discriminate. Qed. Compute lf' (fun s => 0) (num 33 ::(zdiv 56 "x"):: (num 18)::nil). Compute lf' (fun s => 1) ((num 33 ::(zdiv 56 "x"):: num 18::nil) : list expr). (* substitution *) Compute subst (zmult "x" "x") "x" (zplus "x" 1) . Compute b_subst (blt "x" 10 ) "x" (zplus "x" 1) .