Set Warnings "-notation-overridden,-parsing". Require Import Maps. From Coq Require Import Bool.Bool. From Coq Require Import Arith.Arith. From Coq Require Import Arith.EqNat. From Coq Require Import Arith.PeanoNat. Import Nat. From Coq Require Import omega.Omega. Require Import Imp. Require Import Hoare. Module HoareAssertAssume. Definition assert_implies (P Q : Assertion) : Prop := forall st, P st -> Q st. Notation "P ->> Q" := (assert_implies P Q) (at level 80) : hoare_spec_scope. Open Scope hoare_spec_scope. Notation "P <<->> Q" := (P ->> Q /\ Q ->> P) (at level 80) : hoare_spec_scope. Definition Aexp : Type := state -> nat. Definition assert_of_Prop (P : Prop) : Assertion := fun _ => P. Definition Aexp_of_nat (n : nat) : Aexp := fun _ => n. Definition Aexp_of_aexp (a : aexp) : Aexp := fun st => aeval st a. Coercion assert_of_Prop : Sortclass >-> Assertion. Coercion Aexp_of_nat : nat >-> Aexp. Coercion Aexp_of_aexp : aexp >-> Aexp. Arguments assert_of_Prop /. Arguments Aexp_of_nat /. Arguments Aexp_of_aexp /. Bind Scope assertion_scope with Assertion. Bind Scope assertion_scope with Aexp. Delimit Scope assertion_scope with assertion. Notation assert P := (P%assertion : Assertion). Notation mkAexp a := (a%assertion : Aexp). Notation "~ P" := (fun st => ~ assert P st) : assertion_scope. Notation "P /\ Q" := (fun st => assert P st /\ assert Q st) : assertion_scope. Notation "P \/ Q" := (fun st => assert P st \/ assert Q st) : assertion_scope. Notation "P -> Q" := (fun st => assert P st -> assert Q st) : assertion_scope. Notation "P <-> Q" := (fun st => assert P st <-> assert Q st) : assertion_scope. Notation "a = b" := (fun st => mkAexp a st = mkAexp b st) : assertion_scope. Notation "a <> b" := (fun st => mkAexp a st <> mkAexp b st) : assertion_scope. Notation "a <= b" := (fun st => mkAexp a st <= mkAexp b st) : assertion_scope. Notation "a < b" := (fun st => mkAexp a st < mkAexp b st) : assertion_scope. Notation "a >= b" := (fun st => mkAexp a st >= mkAexp b st) : assertion_scope. Notation "a > b" := (fun st => mkAexp a st > mkAexp b st) : assertion_scope. Notation "a + b" := (fun st => mkAexp a st + mkAexp b st) : assertion_scope. Notation "a - b" := (fun st => mkAexp a st - mkAexp b st) : assertion_scope. Notation "a * b" := (fun st => mkAexp a st * mkAexp b st) : assertion_scope. Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q) (at level 90, c at next level) : hoare_spec_scope. Notation "P [ X |-> a ]" := (assn_sub X a P) (at level 10, X at next level). Definition bassn b : Assertion := fun st => (beval st b = true). Coercion bassn : bexp >-> Assertion. Arguments bassn /. (** In this exercise, we will extend IMP with two commands, [ASSERT] and [ASSUME]. Both commands are ways to indicate that a certain statement should hold any time this part of the program is reached. However they differ as follows: - If an [ASSERT] statement fails, it causes the program to go into an error state and exit. - If an [ASSUME] statement fails, the program fails to evaluate at all. In other words, the program gets stuck and has no final state. The new set of commands is: *) Inductive com : Type := | CSkip : com | CAss : string -> aexp -> com | CSeq : com -> com -> com | CIf : bexp -> com -> com -> com | CWhile : bexp -> com -> com | CAssert : bexp -> com | CAssume : bexp -> com. Notation "'SKIP'" := CSkip. Notation "x '::=' a" := (CAss x a) (at level 60). Notation "c1 ;; c2" := (CSeq c1 c2) (at level 80, right associativity). Notation "'WHILE' b 'DO' c 'END'" := (CWhile b c) (at level 80, right associativity). Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" := (CIf c1 c2 c3) (at level 80, right associativity). Notation "'ASSERT' b" := (CAssert b) (at level 60). Notation "'ASSUME' b" := (CAssume b) (at level 60). (** To define the behavior of [ASSERT] and [ASSUME], we need to add notation for an error, which indicates that an assertion has failed. We modify the [ceval] relation, therefore, so that it relates a start state to either an end state or to [error]. The [result] type indicates the end value of a program, either a state or an error: *) Inductive result : Type := | RNormal : state -> result | RError : result. (** Now we are ready to give you the ceval relation for the new language. *) Inductive ceval : com -> state -> result -> Prop := (* Old rules, several modified *) | E_Skip : forall st, st =[ SKIP ]=> RNormal st | E_Ass : forall st a1 n x, aeval st a1 = n -> st =[ x ::= a1 ]=> RNormal (x !-> n ; st) | E_SeqNormal : forall c1 c2 st st' r, st =[ c1 ]=> RNormal st' -> st' =[ c2 ]=> r -> st =[ c1 ;; c2 ]=> r | E_SeqError : forall c1 c2 st, st =[ c1 ]=> RError -> st =[ c1 ;; c2 ]=> RError | E_IfTrue : forall st r b c1 c2, beval st b = true -> st =[ c1 ]=> r -> st =[ TEST b THEN c1 ELSE c2 FI ]=> r | E_IfFalse : forall st r b c1 c2, beval st b = false -> st =[ c2 ]=> r -> st =[ TEST b THEN c1 ELSE c2 FI ]=> r | E_WhileFalse : forall b st c, beval st b = false -> st =[ WHILE b DO c END ]=> RNormal st | E_WhileTrueNormal : forall st st' r b c, beval st b = true -> st =[ c ]=> RNormal st' -> st' =[ WHILE b DO c END ]=> r -> st =[ WHILE b DO c END ]=> r | E_WhileTrueError : forall st b c, beval st b = true -> st =[ c ]=> RError -> st =[ WHILE b DO c END ]=> RError (* Rules for Assert and Assume *) where "st '=[' c ']=>' r" := (ceval c st r). (** We redefine hoare triples: Now, [{{P}} c {{Q}}] means that, whenever [c] is started in a state satisfying [P], and terminates with result [r], then [r] is not an error and the state of [r] satisfies [Q]. *) Definition hoare_triple (P : Assertion) (c : com) (Q : Assertion) : Prop := forall st r, st =[ c ]=> r -> P st -> (exists st', r = RNormal st' /\ Q st'). Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q) (at level 90, c at next level) : hoare_spec_scope. Theorem assert_assume_differ : exists P b Q, ({{P}} ASSUME b {{Q}}) /\ ~ ({{P}} ASSERT b {{Q}}). Proof. Admitted. Theorem assert_implies_assume : forall P b Q, ({{P}} ASSERT b {{Q}}) -> ({{P}} ASSUME b {{Q}}). Proof. Admitted. Theorem hoare_assert : forall Q (b:bexp), {{Q /\ b}} ASSERT b {{Q}}. Proof. Admitted. Theorem hoare_assume : forall (Q: state -> Prop) (b:bexp), {{b -> Q}} ASSUME b {{Q}}. Proof. Admitted. End HoareAssertAssume.