(* CS3234, Martin Henz and Aquinas Hobor *) (* Homework on Hoare logic soundness in Coq *) (* Some useful tactics *) Tactic Notation "spec" hyp(H) := match type of H with ?a -> _ => let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end. Tactic Notation "spec" hyp(H) constr(a) := (generalize (H a); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) := (generalize (H a b); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) := (generalize (H a b c); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) := (generalize (H a b c d); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) := (generalize (H a b c d e); clear H; intro H). Ltac remembertac2 x a := let x := fresh x in let H := fresh "Heq" x in (set (x:=a) in *; assert (H: a=x) by reflexivity; clearbody x). Tactic Notation "cases" constr(a) := let x := fresh in (remembertac2 x a; destruct x). Require ClassicalFacts. (* no axioms in this line *) Require Export Coq.Logic.ClassicalChoice. (* Axioms dependent_unique_choice, relational_choice *) Tactic Notation "LEM" constr(a) := destruct (classic a). Axiom dep_extensionality: forall (A: Type) (B: A -> Type) (f g : forall x: A, B x), (forall x, f x = g x) -> f = g. Implicit Arguments dep_extensionality. Axiom prop_ext: ClassicalFacts.prop_extensionality. Implicit Arguments prop_ext. Require Import ZArith. Open Local Scope Z_scope. (* The following material is exactly the same as in the homework *) Definition var : Type := nat. Inductive nexp : Type := | neInt : Z -> nexp | neVar : var -> nexp | nePlus : nexp -> nexp -> nexp | neMinus : nexp -> nexp -> nexp | neTimes : nexp -> nexp -> nexp. Inductive bexp : Type := | beLE : nexp -> nexp -> bexp | beOr : bexp -> bexp -> bexp | beNot : bexp -> bexp. Definition beTrue : bexp := beLE (neInt 0) (neInt 0). Definition beFalse : bexp := beNot beTrue. Definition beAnd (b1 b2 : bexp) : bexp := beNot (beOr (beNot b1) (beNot b2)). Definition beEq (n1 n2 : nexp) : bexp := beAnd (beLE n1 n2) (beLE n2 n1). Definition beNeq (n1 n2 : nexp) : bexp := beNot (beEq n1 n2). Definition beLT (n1 n2 : nexp) : bexp := beAnd (beLE n1 n2) (beNeq n1 n2). Definition context : Type := var -> Z. Fixpoint neval (rho : context) (ne : nexp) : Z := match ne with | neInt z => z | neVar x => rho x | nePlus ne1 ne2 => (neval rho ne1) + (neval rho ne2) | neMinus ne1 ne2 => (neval rho ne1) - (neval rho ne2) | neTimes ne1 ne2 => (neval rho ne1) * (neval rho ne2) end. Fixpoint beval (rho : context) (be : bexp) : Prop := match be with | beLE n1 n2 => (neval rho n1) <= (neval rho n2) | beOr b1 b2 => (beval rho b1) \/ (beval rho b2) | beNot b => ~(beval rho b) end. Inductive Command : Type := | Skip : Command | Assign : var -> nexp -> Command | Seq : Command -> Command -> Command | If : bexp -> Command -> Command -> Command | While : bexp -> Command -> Command. Definition assert : Type := context -> Prop. Definition Top : assert := fun _ => True. Definition Bot : assert := fun _ => False. Definition And (P1 P2 : assert) : assert := fun rho => (P1 rho) /\ (P2 rho). Definition Or (P1 P2 : assert) : assert := fun rho => (P1 rho) \/ (P2 rho). Definition Impl (P1 P2 : assert) : assert := fun rho => (P1 rho) -> (P2 rho). Definition Not (P : assert) : assert := Impl P Bot. Definition Univ (A : Type) (P : A -> assert) : assert := fun rho => forall a, P a rho. Definition Exis (A : Type) (P : A -> assert) : assert := fun rho => exists a, P a rho. Definition Lift (P : Prop) : assert := fun rho => P. Definition NEval (ne : nexp) (z : Z) : assert := fun rho => neval rho ne = z. Definition BEval (be : bexp) : assert := fun rho => beval rho be. Definition relation : Type := context -> context -> Prop. Definition Box (R : relation) (P : assert) : assert := fun rho => forall rho', R rho rho' -> P rho'. Definition Diam (R : relation) (P : assert) : assert := fun rho => exists rho', R rho rho' /\ P rho'. Definition upd_ctx (rho : context) (x : var) (z : Z) : context := fun x' => if eq_nat_dec x x' then z else rho x'. Definition U (x : var) (z : Z) : relation := fun rho rho' => rho' = upd_ctx rho x z. Definition UBox (x : var) (z : Z) : assert -> assert := Box (U x z). Definition UEBox (x : var) (ne : nexp) (P : assert) : assert := fun rho => UBox x (neval rho ne) P rho. Inductive BStep : Command -> context -> context -> Prop := | bSkip : forall rho, BStep Skip rho rho | bAssign : forall x ne rho, BStep (Assign x ne) rho (upd_ctx rho x (neval rho ne)) | bSeq : forall rho rho' rho'' c1 c2, BStep c1 rho rho' -> BStep c2 rho' rho'' -> BStep (Seq c1 c2) rho rho'' | bIf1 : forall rho rho' b c1 c2, beval rho b -> BStep c1 rho rho' -> BStep (If b c1 c2) rho rho' | bIf2 : forall rho rho' b c1 c2, ~beval rho b -> BStep c2 rho rho' -> BStep (If b c1 c2) rho rho' | bWhile1 : forall rho rho' rho'' b c, beval rho b -> BStep c rho rho' -> BStep (While b c) rho' rho'' -> BStep (While b c) rho rho'' | bWhile2 : forall rho b c, ~beval rho b -> BStep (While b c) rho rho. Lemma BStep_det: forall rho c rho' rho'', BStep rho c rho' -> BStep rho c rho'' -> rho' = rho''. Proof. intros. revert rho'' H0. induction H; intros. inversion H0. trivial. inversion H0. trivial. inversion H1; subst. generalize (IHBStep1 rho'0 H4); intro. subst rho'0. generalize (IHBStep2 _ H7); intro. subst rho''0. trivial. inversion H1; subst. apply IHBStep in H8. trivial. contradiction. inversion H1; subst. contradiction. apply IHBStep in H8. trivial. inversion H2; subst. apply IHBStep1 in H6. subst rho'0. apply IHBStep2 in H9. trivial. contradiction. inversion H0; subst. contradiction. trivial. Qed. Definition SBox (c : Command) : assert -> assert := Box (BStep c). Definition SDiam (c : Command) : assert -> assert := Diam (BStep c). Definition HTriple (P : assert) (c : Command) (Q : assert) : Prop := forall rho, (Impl P (SBox c Q)) rho. Definition THTriple (P : assert) (c : Command) (Q : assert) : Prop := forall rho, (Impl P (SDiam c Q)) rho. Lemma THTriple_HTriple: forall P c Q, THTriple P c Q -> HTriple P c Q. Proof. repeat intro. generalize (H rho H0). intro. destruct H2 as [rho'' [? ?]]. replace rho' with rho''; trivial. eapply BStep_det; eauto. Qed. (* Here we just assert the truth of the facts proved in the homework *) Axiom HT_Skip: forall P, HTriple P Skip P. Axiom HT_Assign: forall x e P, HTriple (UEBox x e P) (Assign x e) P. Axiom HT_Seq: forall P Q R c1 c2, HTriple P c1 Q -> HTriple Q c2 R -> HTriple P (Seq c1 c2) R. Axiom HT_Cons: forall P c Q P' Q', HTriple P' c Q' -> (forall rho, (Impl P P') rho) -> (forall rho, (Impl Q' Q) rho) -> HTriple P c Q. Axiom HT_If : forall P Q b c1 c2, HTriple (And P (BEval b)) c1 Q -> HTriple (And P (Not (BEval b))) c2 Q -> HTriple P (If b c1 c2) Q. Axiom HT_While : forall P b c, HTriple (And P (BEval b)) c P -> HTriple P (While b c) (And P (Not (BEval b))). (* Your first goal -- 10 marks *) Lemma HT_Conj : forall P1 P2 c Q1 Q2, HTriple P1 c Q1 -> HTriple P2 c Q2 -> HTriple (And P1 P2) c (And Q1 Q2). Proof. admit. Qed. (* Do not delete this line. *) Opaque HTriple. (* READ AND TAKE THE TIME TO UNDERSTAND THIS EXAMPLE *) Definition var_x : var := O. Definition var_y : var := S O. (* A very simple program: x := y + 1 *) Definition Very_Simple_Program : Command := Assign var_x (nePlus (neVar var_y) (neInt 1)). (* We need the following two lemmas about upd_ctx -- don't worry exactly how it is proved *) Lemma upd_ctx_same: forall rho x z, (upd_ctx rho x z) x = z. Proof. intros. unfold upd_ctx. elim (eq_nat_dec x x); auto. intro. contradiction b. trivial. Qed. Lemma upd_ctx_notsame : forall rho x x' z, x <> x' -> (upd_ctx rho x z) x' = rho x'. Proof. intros. unfold upd_ctx. elim (eq_nat_dec x x'); auto. intro. contradiction. Qed. (* A very simple verification: {y = 0} VSP {x = 1} *) Lemma Verify_VSP: HTriple (NEval (neVar var_y) 0) Very_Simple_Program (NEval (neVar var_x) 1). Proof. (* First we use the rule of consequence; we provide the new pre and postconditions using "with" *) apply HT_Cons with (UEBox var_x (nePlus (neVar var_y) (neInt 1)) (NEval (neVar var_x )1)) (NEval (neVar var_x) 1). unfold Very_Simple_Program. (* Now we can just apply the assignment rule *) apply HT_Assign. (* Now we have to prove the other parts of the rule of consequence *) (* precondition *) repeat intro. unfold U in H0. rewrite H0. unfold NEval in *. simpl in *. rewrite upd_ctx_same. rewrite H. auto. (* postcondtion *) repeat intro. trivial. Qed. (* OK, now it is your turn. Here you go: *) Definition x_isEven : assert := fun rho => exists m, rho var_x = m + m. Definition x_isOdd : assert := fun rho => exists m, rho var_x = m + m + 1. (* This is the following program: x := x + 5; x := x + 3 *) Definition Simple_Prog : Command := Seq (Assign var_x (nePlus (neVar var_x) (neInt 5))) (Assign var_x (nePlus (neVar var_x) (neInt 3))). (* 20 marks *) Lemma SP_Verify: HTriple x_isEven Simple_Prog x_isEven. Proof. admit. Qed.