Start HoareLogic, with several examples

Frap.v

@@ -71,11 +71,18 @@ Ltac removeDups :=
                  || (apply RdDup; [ simpl; intuition congruence | ]))
   end.
 
+Ltac simpl_maps :=
+  repeat match goal with
+         | [ |- context[add ?m ?k1 ?v $? ?k2] ] =>
+           (rewrite (@lookup_add_ne _ _ m k1 k2 v) by (congruence || omega))
+           || (rewrite (@lookup_add_eq _ _ m k1 k2 v) by (congruence || omega))
+         end.
+
 Ltac simplify := repeat (unifyTails; pose proof I);
                 repeat match goal with
                        | [ H : True |- _ ] => clear H
                        end;
-                repeat progress (simpl in *; intros; try autorewrite with core in *);
+                repeat progress (simpl in *; intros; try autorewrite with core in *; simpl_maps);
                                  repeat (removeDups || doSubtract).
 Ltac propositional := intuition idtac.
 

HoareLogic.v

@@ -0,0 +1,341 @@
+(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
+  * Chapter 10: Hoare Logic: Verifying Imperative Programs
+  * Author: Adam Chlipala
+  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
+
+Require Import Frap.
+
+
+(** * Syntax and semantics of a simple imperative language *)
+
+(* Here's some appropriate syntax for expressions (side-effect-free) of a simple
+ * imperatve language with a mutable memory. *)
+Inductive exp :=
+| Const (n : nat)
+| Var (x : string)
+| Read (e1 : exp)
+| 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 heap := fmap nat nat.
+Definition valuation := fmap var nat.
+Definition assertion := heap -> valuation -> Prop.
+
+(* Here's the syntax of side-effecting commands, where we attach an assertion to
+ * every "while" loop, for reasons that should become clear later.  The
+ * assertion is ignored in the operational semantics! *)
+Inductive cmd :=
+| Skip
+| Assign (x : var) (e : exp)
+| Write (e1 e2 : exp)
+| Seq (c1 c2 : cmd)
+| If_ (be : bexp) (then_ else_ : cmd)
+| While_ (inv : assertion) (be : bexp) (body : cmd)
+
+(* And one more, which we'll use to characterize program correctness more
+ * simply: *)
+| Assert (a : assertion).
+
+Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 30).
+
+(* Start of expression semantics: meaning of expressions, as a function of
+ * state *)
+Fixpoint eval (e : exp) (h : heap) (v : valuation) : nat :=
+  match e with
+  | Const n => n
+  | Var x => v $! x
+  | Read e1 => h $! eval e1 h v
+  | Plus e1 e2 => eval e1 h v + eval e2 h v
+  | Minus e1 e2 => eval e1 h v - eval e2 h v
+  | Mult e1 e2 => eval e1 h v * eval e2 h v
+  end.
+
+(* Meaning of Boolean expressions *)
+Fixpoint beval (b : bexp) (h : heap) (v : valuation) : bool :=
+  match b with
+  | Equal e1 e2 => if eval e1 h v ==n eval e2 h v then true else false
+  | Less e1 e2 => if eval e2 h v <=? eval e1 h v then false else true
+  end.
+
+(* A big-step operational semantics for commands *)
+Inductive exec : heap -> valuation -> cmd -> heap -> valuation -> Prop :=
+| ExSkip : forall h v,
+  exec h v Skip h v
+| ExAssign : forall h v x e,
+  exec h v (Assign x e) h (v $+ (x, eval e h v))
+| ExWrite : forall h v e1 e2,
+  exec h v (Write e1 e2) (h $+ (eval e1 h v, eval e2 h v)) v
+| ExSeq : forall h1 v1 c1 h2 v2 c2 h3 v3,
+  exec h1 v1 c1 h2 v2
+  -> exec h2 v2 c2 h3 v3
+  -> exec h1 v1 (Seq c1 c2) h3 v3
+| ExIfTrue : forall h1 v1 b c1 c2 h2 v2,
+  beval b h1 v1 = true
+  -> exec h1 v1 c1 h2 v2
+  -> exec h1 v1 (If_ b c1 c2) h2 v2
+| ExIfFalse : forall h1 v1 b c1 c2 h2 v2,
+  beval b h1 v1 = false
+  -> exec h1 v1 c2 h2 v2
+  -> exec h1 v1 (If_ b c1 c2) h2 v2
+| ExWhileFalse : forall I h v b c,
+  beval b h v = false
+  -> exec h v (While_ I b c) h v
+| ExWhileTrue : forall I h1 v1 b c h2 v2 h3 v3,
+  beval b h1 v1 = true
+  -> exec h1 v1 c h2 v2
+  -> exec h2 v2 (While_ I b c) h3 v3
+  -> exec h1 v1 (While_ I b c) h3 v3
+
+(* Assertions execute only when they are true. *)
+| ExAssert : forall h v (a : assertion),
+  a h v
+  -> exec h v (Assert a) h v.
+
+
+(** * Hoare logic *)
+
+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 h v => exists v', P h v' /\ v = v' $+ (x, eval e h v'))
+| HtWrite : forall (P : assertion) (e1 e2 : exp),
+  hoare_triple P (Write e1 e2) (fun h v => exists h', P h' v /\ h = h' $+ (eval e1 h' v, eval e2 h' 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 h v => P h v /\ beval b h v = true) c1 Q1
+  -> hoare_triple (fun h v => P h v /\ beval b h v = false) c2 Q2
+  -> hoare_triple P (If_ b c1 c2) (fun h v => Q1 h v \/ Q2 h v)
+| HtWhile : forall (I P : assertion) b c,
+  (forall h v, P h v -> I h v)
+  -> hoare_triple (fun h v => I h v /\ beval b h v = true) c I
+  -> hoare_triple P (While_ I b c) (fun h v => I h v /\ beval b h v = false)
+| HtConsequence : forall (P Q P' Q' : assertion) c,
+  hoare_triple P c Q
+  -> (forall h v, P' h v -> P h v)
+  -> (forall h v, Q h v -> Q' h v)
+  -> hoare_triple P' c Q'.
+
+Lemma hoare_triple_big_step_while: forall I b c,
+  (forall h v h' v', I h v /\ beval b h v = true
+                     -> exec h v c h' v'
+                     -> I h' v')
+  -> (forall h v h' v', exec h v c h' v'
+                        -> I h v
+                        -> beval b h v = true
+                        -> I h' v')
+  -> forall h v h' v', exec h v (While_ I b c) h' v'
+                       -> I h v
+                       -> I h' v' /\ beval b h' v' = false.
+Proof.
+  induct 3; eauto.
+Qed.
+
+Theorem hoare_triple_big_step : forall pre c post,
+    hoare_triple pre c post
+    -> forall h v h' v', exec h v c h' v'
+                         -> pre h v
+                         -> post h' v'.
+Proof.
+  induct 1; eauto; invert 1; eauto.
+
+  simplify.
+  eapply hoare_triple_big_step_while; eauto.
+Qed.
+
+
+(* BEGIN syntax macros that won't be explained *)
+Coercion Const : nat >-> exp.
+Coercion Var : string >-> exp.
+Notation "*[ e ]" := (Read e) : cmd_scope.
+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
+  | Read dst' => Write dst' src
+  | 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, e at level 0).
+Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I 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 *)
+
+(* We should draw some attention to the next notation, which defines special
+ * lambdas for writing assertions. *)
+Notation "h & v ~> e" := (fun h v => e%reset) (at level 85, v at level 0).
+
+Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).
+
+
+
+(** * Some examples of verified programs *)
+
+(** ** Swapping the values in two variables *)
+
+Ltac ht1 := apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
+            || eapply HtIf || eapply HtWhile
+            || match goal with
+               | [ |- hoare_triple ?pre _ _ ] => eapply HtConsequence with (P := pre); [ | tauto | ]
+               end.
+
+Ltac ht := simplify; repeat ht1; cbv beta; propositional; subst;
+           repeat match goal with
+                  | [ H : ex _ |- _ ] => invert H; propositional; subst
+                  end;
+           simplify;
+           repeat match goal with
+                  | [ _ : context[?a <=? ?b] |- _ ] => destruct (a <=? b); try discriminate
+                  | [ H : ?E = ?E |- _ ] => clear H
+                  end; simplify; propositional; auto; try linear_arithmetic.
+
+Theorem swap_ok : forall a b,
+  {{_&v ~> v $! "x" = a /\ v $! "y" = b}}
+    "tmp" <- "x";;
+    "x" <- "y";;
+    "y" <- "tmp"
+  {{_&v ~> v $! "x" = b /\ v $! "y" = a}}.
+Proof.
+  ht.
+Qed.
+
+(** ** Computing the maximum of two variables *)
+
+Theorem max_ok : forall a b,
+  {{_&v ~> v $! "x" = a /\ v $! "y" = b}}
+    when "x" < "y" then
+      "m" <- "y"
+    else
+      "m" <- "x"
+    done
+  {{_&v ~> v $! "m" = max a b}}.
+Proof.
+  ht.
+Qed.
+
+(** ** Iterative factorial *)
+
+(* These two rewrite rules capture the definition of functional [fact], in
+ * exactly the form useful in our Hoare-logic proof. *)
+Lemma fact_base : forall n,
+  n = 0
+  -> fact n = 1.
+Proof.
+  simplify; subst; auto.
+Qed.
+
+Hint Rewrite <- minus_n_O.
+
+Lemma fact_rec : forall n,
+  n > 0
+  -> fact n = n * fact (n - 1).
+Proof.
+  simplify; cases n; simplify; linear_arithmetic.
+Qed.
+
+Hint Rewrite fact_base fact_rec using linear_arithmetic.
+
+(* Note the careful choice of loop invariant below.  It may look familiar from
+ * earlier chapters' proofs! *)
+Theorem fact_ok : forall n,
+  {{_&v ~> v $! "n" = n}}
+    "acc" <- 1;;
+    {{_&v ~> v $! "acc" * fact (v $! "n") = fact n}}
+    while 0 < "n" loop
+      "acc" <- "acc" * "n";;
+      "n" <- "n" - 1
+    done
+  {{_&v ~> v $! "acc" = fact n}}.
+Proof.
+  ht.
+  ring [H0]. (* This variant of [ring] suggests a hypothesis to use in the
+              * proof. *)
+Qed.
+
+(** ** Selection sort *)
+
+(* This is our one example of a program reading/writing memory, which holds the
+ * representation of an array that we want to sort in-place. *)
+
+(** One simple lemma turns out to be helpful to guide [auto] properly. *)
+Lemma leq_f : forall A (m : fmap A nat) x y,
+  x = y
+  -> m $! x <= m $! y.
+Proof.
+  ht.
+Qed.
+
+Hint Resolve leq_f.
+Hint Extern 1 (@eq nat _ _) => linear_arithmetic.
+Hint Extern 1 (_ < _) => linear_arithmetic.
+Hint Extern 1 (_ <= _) => linear_arithmetic.
+(* We also register [linear-arithmetic] as a step to try during proof search. *)
+
+(* These invariants are fairly hairy, but probably the best way to understand
+ * them is just to spend a while reading them.  They generally talk about
+ * sortedness of subsets of the array.  See the final postcondition for how we
+ * interpret a part of memory as an array.  Also note that we only prove here
+ * that the final array is sorted, *not* that it's a permutation of the original
+ * array!  (Exercise for the reader?  I'm not sure how much work it would
+ * take.) *)
+Theorem selectionSort_ok :
+  {{_&_ ~> True}}
+    "i" <- 0;;
+    {{h&v ~> v $! "i" <= v $! "n"
+        /\ (forall i j, i < j < v $! "i" -> h $! (v $! "a" + i) <= h $! (v $! "a" + j))
+        /\ (forall i j, i < v $! "i" -> v $! "i" <= j < v $! "n" -> h $! (v $! "a" + i) <= h $! (v $! "a" + j)) }}
+    while "i" < "n" loop
+      "j" <- "i"+1;;
+      "best" <- "i";;
+      {{h&v ~> v $! "i" < v $! "j" <= v $! "n"
+         /\ v $! "i" <= v $! "best" < v $! "n"
+         /\ (forall k, v $! "i" <= k < v $! "j" -> h $! (v $! "a" + v $! "best") <= h $! (v $! "a" + k))
+         /\ (forall i j, i < j < v $! "i" -> h $! (v $! "a" + i) <= h $! (v $! "a" + j))
+         /\ (forall i j, i < v $! "i" -> v $! "i" <= j < v $! "n" -> h $! (v $! "a" + i) <= h $! (v $! "a" + j)) }}
+      while "j" < "n" loop
+        when *["a" + "j"] < *["a" + "best"] then
+          "best" <- "j"
+        else
+          Skip
+        done;;
+        "j" <- "j" + 1
+      done;;
+      "tmp" <- *["a" + "best"];;
+      *["a" + "best"] <- *["a" + "i"];;
+      *["a" + "i"] <- "tmp";;
+      "i" <- "i" + 1
+    done
+  {{h&v ~> forall i j, i < j < v $! "n" -> h $! (v $! "a" + i) <= h $! (v $! "a" + j)}}.
+Proof.
+  ht; repeat match goal with
+             | [ |- context[_ $+ (?a + ?x, _) $! (?a + ?y)] ] =>
+               cases (x ==n y); ht
+             end.
+
+  cases (k ==n x0 $! "j"); ht.
+  specialize (H k); ht.
+
+  cases (k ==n x $! "j"); ht.
+Qed.