(* Projet Coq - WP - MPRI 2.7.1 *) (***** Partie 1 : definition de While ****************************************) Require Import ZArith.BinInt. Import Z. Definition Var := nat. Definition Mem := Var -> Z. Definition Expr:= Mem -> Z. Inductive Instr : Type := | skip: Instr | abort: Instr | assign: Var -> Expr -> Instr | seq: Instr -> Instr -> Instr | ifelse: Expr -> Instr -> Instr -> Instr | while: Expr -> Instr -> Instr. Definition ifonly (exp: Expr) (inst: Instr) : Instr := ifelse exp inst skip. (***** CPO *******************************************************************) Fixpoint nat_eq x y := match x, y with | 0, 0 => true | 0, S _ => false | S _, 0 => false | S x0, S y0 => nat_eq x0 y0 end. Definition Sequence (S: Type) := nat -> S. Inductive cpo (T: Type): Type := | CpoError: (cpo T) | CpoElem: T -> (cpo T). Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop := fun T x y => match x, y with | CpoError _, _ => True | CpoElem _ x0, CpoElem _ y0 => x0 = y0 | _, _ => False end. Arguments cpo_leq {T} _ _. Infix "cpo<=" := cpo_leq (at level 100). Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop := fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)). Arguments is_chain {T} _. Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop := fun T chain elt => forall (n: nat), (chain n) cpo<= elt. Arguments is_lub_of {T} _ _. Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T. Arguments find_lub {T} _. Axiom find_lub_correct: forall (T: Type), forall (chain: Sequence (cpo T)), is_chain chain -> is_lub_of chain (find_lub chain). Arguments find_lub_correct {T} {chain} _. (***** Interpretation ********************************************************) Definition subst: Mem -> Var -> Z -> Mem := fun (m: Mem) (v: Var) (z: Z) (v2: Var) => if nat_eq v v2 then z else m v2. Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity). Definition MemCpo := cpo Mem. Definition MemError := CpoError Mem. Definition MemElem := CpoElem Mem. Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo := match mem with | CpoError _ => MemError | CpoElem _ mem0 => match inst with | skip => MemElem mem0 | abort => MemError | assign v e => (MemElem (mem0 [v <- (e mem0)])) | seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0)) | ifelse guard instrIf instrElse => if ((guard mem0) =? 0) % Z then interp instrElse mem else interp instrIf mem | while guard body => let fix while_chain (mem: MemCpo) (n: nat): MemCpo := match n with | 0 => mem | S m => match while_chain (MemElem mem0) m with | CpoError _ => MemError | CpoElem _ submem => if ((guard submem) =? 0) % Z then interp body (MemElem submem) else mem end end in find_lub (fun n => match while_chain (MemElem mem0) n with | CpoError _ => MemError | CpoElem _ submem => if ((guard submem) =? 0) % Z then MemError else MemElem submem end) end end. (***** Validite, prouvabilite pour Hoare *************************************) Definition Assert := Mem -> Prop. Delimit Scope assert with assert. Definition assertTop : Assert := fun _ => True. Definition assertBot : Assert := fun _ => False. Definition assertNot : Assert -> Assert := fun orig mem => ~ (orig mem). Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert. Definition assertAnd : Assert -> Assert -> Assert := fun x1 x2 mem => (x1 mem) /\ (x2 mem). Infix "/\" := assertAnd : assert. Definition assertOr : Assert -> Assert -> Assert := fun x1 x2 mem => (x1 mem) \/ (x2 mem). Infix "\/" := assertOr : assert. Definition assertImpl : Assert -> Assert -> Assert := fun x1 x2 => (~x1 \/ x2) % assert. Infix "->" := assertImpl : assert. Definition assertForall : Var -> Assert -> Assert := fun ident asser mem => forall (z: Z), asser (mem [ident <- z]). Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert. Definition existsForall : Var -> Assert -> Assert := fun ident asser mem => exists (z: Z), asser (mem [ident <- z]). Notation "'exists' x" := (existsForall x) (at level 87, no associativity): assert. Definition assertMemForall : Assert -> Assert := fun asser mem => forall (mem: Mem), asser mem. Notation "'\-/m' x" := (assertMemForall x) (at level 90, no associativity): assert. Definition existsMemForall : Assert -> Assert := fun asser mem => exists (mem: Mem), asser mem. Notation "'exists_m' x" := (existsMemForall x) (at level 87, no associativity): assert. Definition substAssert : Assert -> Var -> Z -> Assert := fun asser ident val mem => asser (mem [ident <- val]). Notation "a [[ x <- z ]]" := (substAssert a x z) (at level 50, left associativity). Definition substAssertExpr : Assert -> Var -> Expr -> Assert := fun asser ident expr mem => asser (mem [ident <- (expr mem)]). Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z) (at level 50, left associativity). Definition assertOfExpr : Expr -> Assert := fun expr mem => (expr mem <> 0)%Z. Definition assertImplLogical (a1 a2: Assert): Prop := forall (m: Mem), (a1 m) -> (a2 m). (***** Hoare provability *****************************************************) Reserved Notation "|- [| x |] y [| z |]" (at level 30). Inductive hoare_provability : Assert -> Instr -> Assert -> Prop := | H_skip: forall pre, hoare_provability pre skip pre | H_abort: forall pre, forall post, hoare_provability pre abort post | H_assign: forall post, forall (x: Var), forall (e: Expr), (|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert | H_conseq: forall pre, forall post, forall pre', forall post', forall s, (|- [| pre' |] s [| post' |]) % assert -> (assertImplLogical pre pre') -> (assertImplLogical post' post) -> (|- [| pre |] s [| post |]) % assert | H_seq: forall pre, forall mid, forall post, forall s1, forall s2, (|- [|pre|] s1 [|mid|]) % assert -> (|- [|mid|] s2 [|post|]) % assert -> (|- [|pre|] (seq s1 s2) [|post|]) % assert | H_if: forall pre, forall post, forall expr, forall sIf, forall sElse, (|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert -> (|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert -> (|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert | H_while: forall inv, forall expr, forall sBody, (|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert -> (|- [| inv |] (while expr sBody) [| inv /\ ~ (assertOfExpr expr) |]) % assert where "|- [| pre |] instr [| post |]" := (hoare_provability pre instr post) : assert. (***** Hoare: provability implies consequence ********************************) Definition conseq_or_bottom (y: Assert) (m: MemCpo) := match m with | CpoError _ => True | CpoElem _ m0 => y m0 end. Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) := forall mem: Mem, (pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))). Notation "|= [| pre |] instr [| post |]" := (hoare_consequence pre instr post) (at level 30): assert. Lemma weaken_in_conseq: forall a1, forall a2, forall m, assertImplLogical a1 a2 -> conseq_or_bottom a1 m -> conseq_or_bottom a2 m. Proof. intros a1 a2 m impl conseq. destruct m. - apply conseq. - simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq. Qed. Theorem hoare_provability_implies_consequence : forall (pre: Assert), forall (s: Instr), forall (post: Assert), ( |- [| pre |] s [| post |] ) % assert -> ( |= [| pre |] s [| post |] ) % assert. Proof. intros pre instr post. intros deduction. induction deduction; intros mem preInMem; simpl. - exact preInMem. - trivial. - exact preInMem. - apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0). apply IHdeduction. apply H. exact preInMem. - destruct (interp s1 (MemElem mem)) eqn:mRel. admit. apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1. specialize IHdeduction1 with mem as IH1_mem. rewrite mRel in IH1_mem. apply IH1_mem. assumption. - destruct (expr mem =? 0)%Z eqn:branchEqn. * apply (IHdeduction2 mem). unfold assertOfExpr. unfold assertAnd. split. + assumption. + unfold assertNot. rewrite <- Z.eqb_eq. congruence. * apply (IHdeduction1 mem). unfold assertOfExpr. unfold assertAnd. split. + assumption. + rewrite <- Z.eqb_eq. congruence.