Initial import

Hoare.v

@@ -0,0 +1,332 @@
+Require Import ImpSimpl.
+Require Import base tactics. (* For typeclasses; obtained from <http://robbertkrebbers.nl/research/ch2o/> *)
+
+(** * Basic definition *)
+
+(** (From ImpSimpl.v) We assume big-step semantics [exec v c v'] representing that [c], if
+executed in a state [v], results in the state [v']. 
+
+In this semantics the state is just a valuation of variables. We
+assume that we can evaluate a boolean expression [be] in a state [v]
+as [beval be v]; we also assume that we can evaluate an arithmetic
+expression [ae] in a state [v] as [eval ae v]. *)
+
+
+(** An assertion in our logic is going to be a predicate on program
+state, i.e. on valuations. *)
+Definition assertion := valuation -> Prop.
+
+
+(** We specify the entailment relation on assertions: [P ==> Q] if [P v]
+ implies [Q v] for all states [v]. *)
+Definition himpl : assertion -> assertion -> Prop := fun P Q =>
+  forall (v : valuation), P v -> Q v.
+Infix "==>" := himpl.
+
+(** It is easily seen that this relation is reflexive and transitive *)
+Instance: Reflexive himpl.
+Proof. intros P v. intuition. Qed.
+
+Instance: Transitive himpl.
+Proof. intros P Q R HPQ HQR v. intuition. Qed.
+
+
+(** Given an assertion [P] (the precondition), an assertion [Q] (the
+postcondition) and a program [c], we write [hoare_interp P c Q v] if,
+supposing the precondition [P] holds at the state [v], and [c]
+evaluates to state [v'] from state [v], we can show that the
+postcondition [Q] holds at the state [v']. 
+
+If this holds for all states [v], we say that the triple (P, Q, c) is
+_valid_, written as [hoare_valid P c Q].
+
+Such a triple (P, Q, c) is called a _Hoare triple_ and is usually
+denoted as [{P} c {Q}]. We will reserve similar notation for Hoare
+triples that are _derivable_ in Hoare logic in the next section
+*)
+Definition hoare_interp (P : assertion) (c : cmd) (Q: assertion) (v : valuation) := forall v', exec v c v' -> P v ->  Q v'.
+
+Definition hoare_valid P c Q := forall v, hoare_interp P c Q v.
+
+(** * Derivable Hoare triples *)
+
+(** The type of deriavable Hoare triples is denoted as [hoare_triple]
+and we use the notation [{{P}} c {{Q}}] as a shorthand for
+[hoare_triple P c Q].*)
+Inductive hoare_triple : assertion -> cmd -> assertion -> Prop :=
+| HtSkip : forall P, hoare_triple P Skip P
+| HtAssign : forall (P : assertion) x e,
+  hoare_triple P (Assign x e) 
+    (fun v => exists v', P v' /\ v = (<[x := eval e v']>v'))
+| HtSeq : forall (P Q R : assertion) c1 c2,
+  hoare_triple P c1 Q
+  -> hoare_triple Q c2 R
+  -> hoare_triple P (Seq c1 c2) R
+| HtIf : forall (P Q1 Q2 : assertion) b c1 c2,
+  hoare_triple (fun v => P v /\ beval b v = true) c1 Q1
+  -> hoare_triple (fun v => P v /\ beval b v = false) c2 Q2
+  -> hoare_triple P (If_ b c1 c2) (fun v => Q1 v \/ Q2 v)
+| HtWhileInv : forall (I : assertion) b c,
+  hoare_triple (fun v => I v /\ beval b v = true) c I
+  -> hoare_triple I (While_ b c) (fun v => I v /\ beval b v = false)
+(**
+<<
+P' ==> P    {P} c {Q}    Q ==> Q'
+----------------------------------
+           {P'} c {Q'}
+>>
+
+*)                  
+| HtConsequence : forall (P Q P' Q' : assertion) c,
+  hoare_triple P c Q
+  -> P' ==> P -> Q ==> Q'
+  -> hoare_triple P' c Q'
+(** 
+<<
+∀a  {P(a)} c {Q}
+-----------------
+ {∃a.P(a)} c {Q}
+>>
+*)                  
+| HtExists : forall A (P : A -> assertion) (Q: assertion) c,
+  (forall (a:A), hoare_triple (P a) c (Q))
+  -> hoare_triple (fun v => exists a, P a v) c Q
+.
+
+(* And here's the classic notation for Hoare triples. *)
+Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).
+
+(* Special case of consequence: keeping the precondition; only changing the
+ * postcondition. *)
+Lemma HtStrengthenPost : forall (P Q Q' : assertion) c,
+  hoare_triple P c Q
+  -> Q ==> Q'
+  -> hoare_triple P c Q'.
+Proof.
+  intros; eapply HtConsequence; eauto using reflexivity.
+  (** TODO : eauto doesn't use [reflexivity]? **)
+Qed.
+
+Lemma HtWeakenPre : forall (P P' Q : assertion) c,
+  hoare_triple P c Q
+  -> P' ==> P
+  -> hoare_triple P' c Q.
+Proof.
+  intros; eapply HtConsequence; eauto using reflexivity.
+  (** TODO : eauto doesn't use [reflexivity]? **)
+Qed.
+
+Ltac ht1 := apply HtSkip || apply HtAssign || eapply HtSeq
+            || eapply HtIf || eapply HtWhileInv
+            || eapply HtStrengthenPost.
+
+(** * Soundness of Hoare logic rules. This is mostly taken from FRAP. *)
+
+Lemma hoare_triple_big_step_while: forall (I : assertion) b c,
+  (forall v v', exec v c v'
+                     -> I v
+                     -> beval b v = true
+                     -> I v')
+  -> forall v v', exec v (While_ b c) v'
+                       -> I v
+                       -> I v' /\ beval b v' = false.
+Proof.
+  intros I b c P v v'.
+  intro. dependent induction H; eauto.
+Qed.
+
+Theorem hoare_triple_sound : forall pre c post,
+    hoare_triple pre c post
+    -> hoare_valid pre c post.
+Proof.
+  unfold hoare_valid, hoare_interp.
+  intros pre c post H.
+  dependent induction H; intros v v' E;
+  try (inversion E; subst; by eauto).
+
+  intro.
+  eapply hoare_triple_big_step_while; eauto. 
+
+  intros [a HP]. eapply H0; eassumption.
+Qed.
+
+
+(** * (Syntactic) Weakest precondition *)
+
+(** Syntactic definition of a weakest precondition *)
+Fixpoint wpl (c : cmd) (Q : assertion) : assertion := 
+  match c with
+    | Skip => Q
+    | Assign x E => fun v => Q (<[ x := eval E v ]>v)
+    | Seq c1 c2 => wpl c1 (wpl c2 Q)
+    | If_ be th el => fun v => if beval be v
+                               then (wpl th Q) v
+                                else (wpl el Q) v
+    | While_ be body =>
+      fun v => exists Inv, Inv v /\
+       (forall x, ((beval be x = true /\ Inv x) -> wpl body Inv x)
+        /\
+        ((beval be x = false /\ Inv x) -> Q x))
+  end.
+
+(** ** Semantic soundness & completeness of [wpl] *)
+
+(** [wpl] is sound w.r.t. valuation semantics, this establishes that
+[wpl s Q] is in fact a precondition *)
+Theorem wpl_sound_sem (s : cmd) (Q : assertion) :
+  hoare_valid (wpl s Q) s Q.
+Proof.
+  generalize dependent Q.
+  induction s; simpl; intuition; intros v v' E; try (inversion E; subst; by intuition).
+
+  inversion E; subst. intro wplHolds. eapply IHs2; eauto. eapply IHs1; eauto.
+
+  inversion E; subst; rewrite H4; intro wplHods.
+  eapply IHs1; eauto.
+  eapply IHs2; eauto. 
+
+  dependent induction E; intros [Inv [L1 L2]]. eapply L2; eauto.
+  assert (Inv v2) as Inv_v2 by (eapply IHs; eauto; eapply L2; eauto). 
+  assert (wpl (While_ be s) Q v2) as RealInv by (simpl;eauto).
+  eapply IHE2; eauto. 
+Qed.
+
+Hint Resolve ExSkip ExAssign ExSeq ExIfTrue ExIfFalse ExWhileFalse ExWhileTrue.
+
+(** An auxiliary definition. This is "the real" weakest precondition,
+or a "semantic" weakest precondition. *)
+Definition WeP (c : cmd) (Q: assertion) : assertion :=
+  fun v => forall v', exec v c v' -> Q v'.
+
+
+(** We can prove that [wpl] is complete in the following sense: *)
+
+Theorem wpl_complete_sem (c : cmd) (P Q : assertion) :
+  forall v, hoare_interp P c Q v
+  -> P v -> wpl c Q v.
+Proof.
+  generalize dependent Q. generalize dependent P.
+  induction c; simpl; intros P Q v HT Pv. intuition; by eauto. unfold hoare_interp in HT.
+  try (intuition; by eauto). 
+
+  (** Case [c = c1;c2]. By the first induction hypothesis, to show that [wpl c1 (wpl c2 Q)] holds it suffices to show that [{P} c1 {wpl c2 Q}] holds. *)
+  eapply IHc1 with (P:=P); eauto.
+  intros v' E _.
+  (** This reduces to showing that [wpl c2 Q] holds after the
+execution of [c1]. This can be obtained by applying the second induction
+hypothesis. *)
+  eapply IHc2; try eassumption.
+  intros v'' E2 Pv'. eapply HT; eauto.
+
+  (** Case [c = if be then c1 else c2]. In this case we reason by case analysis: whether [be] is true in the state [v]. If it evaluates to [true] then we use the first induction hypothesis, otherwise use the second one. *)
+  remember (beval be v) as b; destruct b;
+  unfold hoare_interp in HT.
+  eapply IHc1; eauto. intros ???. eapply HT; eauto.
+  eapply IHc2; eauto. intros ???. eapply HT; eauto.
+
+  (** Case [c = while be do c]. In this case we pick the invariant to be the semantic weakest precondition [WeP]. *)
+  (* TODO: pull this out in a separate lemma *)
+  exists (WeP (While_ be c) Q).
+  split. unfold WeP; intuition.
+  intro e. split. 
+  intros [Cond W]. unfold WeP in W. 
+  eapply IHc with (WeP (While_ be c) Q). intros e' ? ?. intros e'' ?.
+  eapply W. eapply ExWhileTrue with e'; eassumption. 
+  eassumption.
+
+  intros [Cond W]. unfold WeP in W. 
+  eapply W. eapply ExWhileFalse. 
+  eassumption.
+Qed.
+
+Theorem wpl_complete_sem' (c : cmd) (P Q : assertion) :
+  hoare_valid P c Q
+  -> (P ==> wpl c Q).
+Proof.
+  intros H v Pv. eapply wpl_complete_sem; eauto.
+Qed.
+
+Theorem wpl_entailment (c : cmd) (P Q : assertion) :
+  (P ==> wpl c Q) -> (hoare_valid P c Q).
+Proof.
+  intros H v v' E Pv.
+  eapply wpl_sound_sem; eauto.
+Qed.
+
+Theorem wpl_entailment' (c : cmd) (P Q : assertion) :
+  forall v, (P v -> wpl c Q v) -> hoare_interp P c Q v.
+Proof.                                             
+  intros v H v' E Pv.
+  eapply wpl_sound_sem; eauto.
+Qed.
+
+(** An auxiliary lemma: wpl is monotone in the second arg *)
+Theorem wpl_mon (c : cmd) (Q Q' : assertion) :
+  Q ==> Q' ->
+  wpl c Q ==> wpl c Q'.
+Proof. generalize dependent Q. generalize dependent Q'.
+  induction c; simpl; intros Q' Q HQ v; intuition.
+
+  eapply IHc1; eauto. 
+
+  destruct (beval be v); intuition. eapply IHc1; eauto. eapply IHc2; eauto.
+  
+  destruct H as [I [HI HII]].
+  exists I; intuition; eauto. eapply IHc. reflexivity. eapply HII; eauto.
+  eapply HQ. eapply HII; eauto.
+Qed.
+
+(** ** Syntactic soundness of [wpl] and relative completeness of the Hoare logic *)
+  
+(** Finally, we can prove the syntactic soundness of [wpl] *)
+Theorem wpl_soundness_synt (s : cmd) (Q : assertion) :
+  {{ wpl s Q }} s {{Q}}.
+Proof.
+  generalize dependent Q. dependent induction s;
+  try (simpl; intuition; by ht1); intro Q.
+  - simpl. eapply HtStrengthenPost. eapply HtAssign. 
+  intros v [v' [S1 S2]]. rewrite S2; assumption.
+
+  - simpl. eapply HtStrengthenPost. 
+    eapply HtIf; eapply HtWeakenPre. 
+      eapply IHs1. intros v [WP C];
+        rewrite C in *; eassumption.
+      eapply IHs2. intros v [WP C];
+        rewrite C in *; eassumption.
+    intro v. intuition.
+  
+  - simpl. eapply HtExists; intro I. 
+    set (Istrong:=(fun v => I v /\ (∀ x : valuation,
+       ((beval be x = true) ∧ I x → wpl s I x)
+         ∧ ((beval be x = false) ∧ I x → Q x)))).
+
+    eapply HtStrengthenPost.
+    { eapply HtWhileInv with (I:=Istrong).
+      apply HtWeakenPre with (wpl s Istrong).
+      eapply IHs.
+
+      (* this should be (cut (wpl s I)) *)
+      transitivity (fun v =>
+       wpl s I v /\ (∀ x : valuation,
+         ((beval be x = true) ∧ I x → wpl s I x)
+           ∧ ((beval be x = false) ∧ I x → Q x))).
+      unfold Istrong;
+      intros v [[Iv IU] beq]. split. eapply IU; eauto. assumption.
+
+      intros v [HWP IU]. 
+        generalize v HWP; clear v HWP. 
+      eapply wpl_mon. intros v' HI. unfold Istrong; intuition.
+    }
+    {
+      unfold Istrong; intros v [[Iv UI] Heq].
+      apply UI; auto.
+    }
+Qed.
+
+(** The syntactic soundness of [wpl] + consequence rule ==> relative completeness of Hoare rules *)
+Theorem completeness P c Q : hoare_valid P c Q -> hoare_triple P c Q.
+Proof. intro HV.
+       eapply HtWeakenPre.
+       apply wpl_soundness_synt.
+       apply wpl_complete_sem'. assumption.
+Qed.

ImpSimpl.v

@@ -0,0 +1,107 @@
+(** This file is a slight modification of ImpSimpl.v from Adam
+Chilipala's FRAP: <http://adam.chlipala.net/frap/> *)
+
+Require Import String.
+
+(** We use Robbert's prelude from <http://robbertkrebbers.nl/research/ch2o/> *)
+Require Import stringmap natmap.
+
+(** Here's some appropriate syntax for expressions (side-effect-free) of a simple imperative language with a mutable memory. *)
+Inductive exp :=
+| Const (n : nat)
+| Var (x : string)
+| Plus (e1 e2 : exp)
+| Minus (e1 e2 : exp)
+| Mult (e1 e2 : exp).
+
+(** Those were the expressions of numeric type.  Here are the Boolean expressions. *)
+Inductive bexp :=
+| Equal (e1 e2 : exp)
+| Less (e1 e2 : exp).
+
+Definition var := string.
+Definition valuation := stringmap nat.
+
+Inductive cmd :=
+| Skip
+| Assign (x : var) (e : exp)
+| Seq (c1 c2 : cmd)
+| If_ (be : bexp) (then_ else_ : cmd)
+| While_ (be : bexp) (body : cmd).
+
+(** Shorthand notation for looking up in a finite map, returning zero if the key is not found *)
+Notation "m $! k" := (match m !! k with Some n => n | None => O end) (at level 30).
+
+(** Start of expression semantics: meaning of expressions *)
+Fixpoint eval (e : exp) (v : valuation) : nat :=
+  match e with
+  | Const n => n
+  | Var x => v $! x
+  | Plus e1 e2 => eval e1 v + eval e2 v
+  | Minus e1 e2 => eval e1 v - eval e2 v
+  | Mult e1 e2 => eval e1 v * eval e2 v
+  end.
+
+(** Meaning of Boolean expressions *)
+Fixpoint beval (b : bexp) (v : valuation) : bool :=
+  match b with
+  | Equal e1 e2 => beq_nat (eval e1 v) (eval e2 v)
+  | Less e1 e2 => negb (eval e2 v <=? eval e1 v)
+  end.
+
+Inductive exec : valuation -> cmd -> valuation -> Prop :=
+| ExSkip : forall v,
+  exec v Skip v
+| ExAssign : forall v x e,
+  exec v (Assign x e) (<[x := eval e v]>v)
+| ExSeq : forall v1 c1 v2 c2 v3,
+  exec v1 c1 v2
+  -> exec v2 c2 v3
+  -> exec v1 (Seq c1 c2) v3
+| ExIfTrue : forall v1 b c1 c2 v2,
+  beval b v1 = true
+  -> exec v1 c1 v2
+  -> exec v1 (If_ b c1 c2) v2
+| ExIfFalse : forall v1 b c1 c2 v2,
+  beval b v1 = false
+  -> exec v1 c2 v2
+  -> exec v1 (If_ b c1 c2) v2
+| ExWhileFalse : forall v b c,
+  beval b v = false
+  -> exec v (While_ b c) v
+| ExWhileTrue : forall v1 b c v2 v3,
+  beval b v1 = true
+  -> exec v1 c v2
+  -> exec v2 (While_ b c) v3
+  -> exec v1 (While_ b c) v3.
+
+
+Open Scope string_scope.
+(* BEGIN syntax macros that won't be explained *)
+Coercion Const : nat >-> exp.
+Coercion Var : string >-> exp.
+Infix "+" := Plus : cmd_scope.
+Infix "-" := Minus : cmd_scope.
+Infix "*" := Mult : cmd_scope.
+Infix "=" := Equal : cmd_scope.
+Infix "<" := Less : cmd_scope.
+Definition set (dst src : exp) : cmd :=
+  match dst with  
+  | Var dst' => Assign dst' src
+  | _ => Assign "Bad LHS" 0
+  end.
+Infix "<-" := set (no associativity, at level 70) : cmd_scope.
+Infix ";;" := Seq (right associativity, at level 75) : cmd_scope.
+Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at level 75, b at level 0).
+Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ b body) (at level 75).
+Delimit Scope cmd_scope with cmd.
+
+Infix "+" := plus : reset_scope.
+Infix "-" := minus : reset_scope.
+Infix "*" := mult : reset_scope.
+Infix "=" := eq : reset_scope.
+Infix "<" := lt : reset_scope.
+Delimit Scope reset_scope with reset.
+Open Scope reset_scope.
+(* END macros *)
+

Makefile

@@ -0,0 +1,12 @@
+CH2O=/Users/dan/projects/ch2o-new/
+
+ImpSimpl.vo: ImpSimpl.v
+	coqc -R $(CH2O) ch2o ImpSimpl.v
+
+Hoare.vo: Hoare.v ImpSimpl.vo
+	coqc -R $(CH2O) ch2o Hoare.v
+
+all: Hoare.vo
+
+doc: ImpSimpl.vo Hoare.vo
+	coqdoc -R $(CH2O) ch2o ImpSimpl.v Hoare.v