Library HSem

Author: Xavier Leroy, with significant modifications by Alberto Momigliano to exploit CoqHammer's automation.
Works for Coq 8.14.
Requires Hammer's tactics, version is 1.3.2
opam install coq-hammer,

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".

Require Import List.
Require Import Arith.
Require Import ZArith.
Require Import Zwf.
Require Import Coq.Program.Equality.
Require Import Sequences.
From Coq Require Import Lia.

From Hammer Require Import Tactics.
From Hammer Require Import Hammer.

Ltac inv H := inversion H; clear H; subst.
Ltac liaContradiction := exfalso; lia.

Notation Z_eq_dec := Z.eq_dec.

Open Scope Z_scope.

Part 1. The IMP language and its semantics


Definition ident := nat.

Definition eq_ident: forall (x y: ident), {x=y}+{x<>y} := eq_nat_dec.

Inductive expr : Type :=
  | Evar: ident -> expr
  | Econst: Z -> expr
  | Eadd: expr -> expr -> expr
  | Esub: expr -> expr -> expr.

Coercion Econst : Z >-> expr.
Coercion Evar : ident >-> expr.
Notation "A +! B" := (Eadd A B) (at level 50).
Notation "A -! B" := (Esub A B) (at level 50).

Execution states, associating values to variables.

Definition state := ident -> Z.

Definition initial_state: state := fun (x: ident) => 0.

Definition update (s: state) (x: ident) (n: Z) : state :=
  fun y => if eq_ident x y then n else s y.

Evaluation of expressions.

Fixpoint eval_expr (s: state) (e: expr) {struct e} : Z :=
  match e with
  | Evar x => s x
  | Econst n => n
  | Eadd e1 e2 => eval_expr s e1 + eval_expr s e2
  | Esub e1 e2 => eval_expr s e1 - eval_expr s e2
  end.

Using the semantics of expressions: to evaluate a given expression

Eval compute in (
  let x : ident := O in
  let s : state := update initial_state x 12 in
  eval_expr s (Eadd (Evar x) (Econst 1))).

Using the semantics of expressions: to reason symbolically over a given expression

Remark expr_add_pos:
  forall s x, s x >= 0 -> eval_expr s (x +! 1) > 0.
Proof.
 simpl. lia.
Qed.

Using the semantics of expressions: to show a "meta" property

Fixpoint is_free (x: ident) (e: expr) {struct e} : Prop :=
  match e with
  | Evar y => x = y
  | Econst n => False
  | Eadd e1 e2 => is_free x e1 \/ is_free x e2
  | Esub e1 e2 => is_free x e1 \/ is_free x e2
  end.

Lemma eval_expr_domain:
  forall s1 s2 e,
  (forall x, is_free x e -> s1 x = s2 x) ->
  eval_expr s1 e = eval_expr s2 e.
Proof.
  induction e; hauto q: on.
Qed.

Optimization

A blueprint for correctness-preserving source-to-source transformation. Here just replace 0 + n with n:

Fixpoint optimize_0plus (a:expr) : expr :=
  match a with
  | Evar _ | Econst _ => a
  | Eadd (Econst 0) e2 => optimize_0plus e2
  | Eadd e1 e2 => Eadd (optimize_0plus e1) (optimize_0plus e2)
  | Esub e1 e2 => Esub (optimize_0plus e1) (optimize_0plus e2)
  end.

Example test_optimize_0plus:
  optimize_0plus (2 +! (0 +! (0 +! 1))) = 2 +! 1.
Proof. reflexivity. Qed.

Soundness proof:
Theorem optimize_0plus_sound: forall a s,
  eval_expr s (optimize_0plus a) = eval_expr s a.
Proof.
  induction a;
    hauto lq: on drew: off.
Qed.

Require Coq.extraction.Extraction.
Extraction Language Haskell.
Require Import ExtrHaskellZNum.
Extract Inductive positive => "Prelude.Integer" [
  "(\x -> 2 Prelude.* x Prelude.+ 1)"
  "(\x -> 2 Prelude.* x)"
  "1" ]
  "(\fI fO fH n -> if n Prelude.== 1 then fH () else if Prelude.odd n then fI (n `Prelude.div` 2) else fO (n `Prelude.div` 2))".

Extract Inductive Z => "Prelude.Integer" [ "0" "(\x -> x)" "Prelude.negate" ]
  "(\fO fP fN n -> if n Prelude.== 0 then fO () else if n Prelude.> 0 then fP n else fN (Prelude.negate n))".

Extraction eval_expr.

Partiality in specs: the division case


Module div.

  Inductive expr : Type :=
  | Evar: ident -> expr
  | Econst: Z -> expr
  | Eadd: expr -> expr -> expr
  | Esub: expr -> expr -> expr
  | Ediv: expr -> expr -> expr.

Now the state is a partial map:

Definition state := ident -> option Z.

Fixpoint eval_expr (s: state) (e: expr) {struct e} : option Z :=
  match e with
  | Evar x => s x
  | Econst n => Some n
  | Eadd e1 e2 => match eval_expr s e1, eval_expr s e2 with
      | Some n1, Some n2 => Some (n1 + n2)
      | _, _ => None
                  end
  | Esub e1 e2 => match eval_expr s e1, eval_expr s e2 with
      | Some n1, Some n2 => Some (n1 - n2)
      | _, _ => None
                  end
   |Ediv e1 e2 => match eval_expr s e1, eval_expr s e2 with
      | Some n1, Some n2 =>
if n2 =? 0 then None else Some (n1 / n2)
      | _, _ => None
                    end
  end.
End div.

IMP:
A limited form of bexp, easy to generalize to negation, conjuction etc.
Inductive bool_expr : Type :=
  | Bequal: expr -> expr -> bool_expr
  | Bless: expr -> expr -> bool_expr.

Notation "A =! B" := (Bequal A B) (at level 55).
Notation "A <! B" := (Bless A B) (at level 54).

Definition eval_bool_expr (s: state) (b: bool_expr) : bool :=
  match b with
  | Bequal e1 e2 =>
      if Z_eq_dec (eval_expr s e1) (eval_expr s e2) then true else false
  | Bless e1 e2 =>
      if Z_lt_dec (eval_expr s e1) (eval_expr s e2) then true else false
  end.

Inductive cmd : Type :=
  | Cskip: cmd
  | Cassign: ident -> expr -> cmd
  | Cseq: cmd -> cmd -> cmd
  | Cifthenelse: bool_expr -> cmd -> cmd -> cmd
  | Cwhile: bool_expr -> cmd -> cmd.

Notation "A <- B" := (Cassign A B) (at level 60).
Notation "A ;; B" := (Cseq A B) (at level 70).
Notation "'If' A 'Then' B 'Else' C" := (Cifthenelse A B C) (at level 65).
Notation "'While' A 'Do' B" := (Cwhile A B) (at level 65).

Reduction semantics


Inductive red : cmd * state -> cmd * state -> Prop :=
    red_assign : forall (x : ident) (e : expr) (s : state),
      red (x <- e, s) (Cskip, update s x (eval_expr s e))
          
  | red_seq_left : forall (c1 c2 : cmd) (s : state) (c1' : cmd) (s' : state),
      red (c1, s) (c1', s') -> red (c1;; c2, s) (c1';; c2, s')
                                   
| red_seq_skip : forall (c : cmd) (s : state), red (Cskip;; c, s) (c, s)
                                                   
  | red_if_true : forall (s : state) (b : bool_expr) (c1 c2 : cmd),
                  eval_bool_expr s b = true ->
                  red (If b Then c1 Else c2, s) (c1, s)
                      
  | red_if_false : forall (s : state) (b : bool_expr) (c1 c2 : cmd),
                   eval_bool_expr s b = false ->
                   red (If b Then c1 Else c2, s) (c2, s)
                       
  | red_while_true : forall (s : state) (b : bool_expr) (c : cmd),
                     eval_bool_expr s b = true ->
                     red (While b Do c, s) (c;; While b Do c, s)
                         
  | red_while_false : forall (b : bool_expr) (c : cmd) (s : state),
                      eval_bool_expr s b = false ->
                      red (While b Do c, s) (Cskip, s).

Note: induction on the derivation (1), using inversion (inv:red) and the constructors (ctrs:red).
If we do not specify ctrs,inv, by default sauto will try to use and invert on any inductive definition in scope and easily gets lost -- not here, though as this is the only relevent def.

Lemma red_deterministic:
  forall cs cs1, red cs cs1 -> forall cs2, red cs cs2 -> cs1 = cs2.
Proof.
  induction 1; sauto inv: red ctrs: red.
Qed.

The three possible outcomes of execution.
star is the reflexive-transitive closure of a relation:

Print star.

Definition terminates (c: cmd) (s s': state) : Prop :=
  star red (c, s) (Cskip, s').

Print infseq.

infseq describes infinite sequences of a relation.
Definition diverges (c: cmd) (s: state) : Prop :=
  infseq red (c, s).

Definition goes_wrong (c: cmd) (s: state) : Prop :=
  exists c', exists s',
  star red (c, s) (c', s') /\ c' <> Cskip /\ forall c'' s'', ~ red (c', s') (c'',s'').

Natural semantics


Inductive exec : state -> cmd -> state -> Prop :=

  exec_skip : forall s : state, exec s Cskip s

| exec_assign : forall (s : state) (x : ident) (e : expr),
                  exec s (x <- e) (update s x (eval_expr s e))

| exec_seq : forall (s : state) (c1 c2 : cmd) (s1 s2 : state),
               exec s c1 s1 -> exec s1 c2 s2 -> exec s (c1;; c2) s2

| exec_if : forall (s : state) (be : bool_expr) (c1 c2 : cmd) (s' : state),
              exec s (if eval_bool_expr s be then c1 else c2) s' ->
              exec s (If be Then c1 Else c2) s'

| exec_while_loop : forall (s : state) (be : bool_expr)
                        (c : cmd) (s1 s2 : state),
                      eval_bool_expr s be = true ->
                      exec s c s1 ->
                      exec s1 (While be Do c) s2 -> exec s (While be Do c) s2

| exec_while_stop : forall (s : state) (be : bool_expr) (c : cmd),
                      eval_bool_expr s be = false -> exec s (While be Do c) s.

Notation "A >> B ==> C" :=
  (exec B A C) (at level 80, no associativity).
Termination in natural semantics implies termination in reduction semantics.

Remark star_red_seq_left:
  forall c s c' s' c2,
    star red (c, s) (c', s') ->
    star red (c;; c2, s) (c';; c2, s').
Proof.
  intros. dependent induction H; sauto lq: on.
Qed.

Lemma exec_terminates:
  forall s c s', exec s c s' -> terminates c s s'.
Proof.
  unfold terminates.
  induction 1;
    try hauto ctrs: red, star
                           use: star_trans , star_red_seq_left.
   time sauto ctrs: red, star brefl: on.
Qed.

If we change the definition of exec so that it does not need reflection, it's faster:
Module noif.
  Inductive exec : state -> cmd -> state -> Prop :=

  exec_skip : forall s : state, exec s Cskip s

| exec_assign : forall (s : state) (x : ident) (e : expr),
                  exec s (x <- e) (update s x (eval_expr s e))

| exec_seq : forall (s : state) (c1 c2 : cmd) (s1 s2 : state),
               exec s c1 s1 -> exec s1 c2 s2 -> exec s (c1;; c2) s2

  | exec_ift : forall (s : state) (be : bool_expr) (c1 c2 : cmd) (s' : state),
          eval_bool_expr s be = true ->
                      exec s c1 s' ->
              exec s (If be Then c1 Else c2) s'


| exec_iff : forall (s : state) (be : bool_expr) (c1 c2 : cmd) (s' : state),
          eval_bool_expr s be = false ->
                      exec s c2 s' ->
              exec s (If be Then c1 Else c2) s'

                   
| exec_while_loop : forall (s : state) (be : bool_expr)
                        (c : cmd) (s1 s2 : state),
                      eval_bool_expr s be = true ->
                      exec s c s1 ->
                      exec s1 (While be Do c) s2 -> exec s (While be Do c) s2

| exec_while_stop : forall (s : state) (be : bool_expr) (c : cmd),
                      eval_bool_expr s be = false -> exec s (While be Do c) s.

End noif.
Lemma exec_terminates':
  forall s c s', noif.exec s c s' -> terminates c s s'.
Proof.
  unfold terminates.
  induction 1;
    hauto ctrs: red, star
                           use: star_trans , star_red_seq_left.
Qed.

Termination in reduction semantics implies termination in natural semantics.

Lemma red_preserves_exec:
  forall c s c' s', red (c, s) (c', s') ->
  forall sfinal, exec s' c' sfinal -> exec s c sfinal.
Proof.
  intros. dependent induction H; sauto lq:on.
Qed.

Lemma terminates_exec:
  forall s c s', terminates c s s' -> exec s c s'.
Proof.
  unfold terminates. intros; dependent induction H;
  hauto l: on use: red_preserves_exec.
Qed.

Definitional interpreter


Inductive result: Type :=
  | Bot: result
  | Res: state -> result.

Definition bind (r: result) (f: state -> result) : result :=
  match r with
  | Res s => f s
  | Bot => Bot
  end.

Fixpoint interp (n: nat) (c: cmd) (s: state) {struct n} : result :=
  match n with
  | O => Bot
  | S n' =>
       match c with
      | Cskip => Res s
      | x <- e => Res (update s x (eval_expr s e))
      | c1;; c2 => bind (interp n' c1 s) (fun s1 : state => interp n' c2 s1)
      | If b Then c1 Else c2 =>
          interp n' (if eval_bool_expr s b then c1 else c2) s
      | While b Do c1 =>
          if eval_bool_expr s b
          then
           bind (interp n' c1 s)
             (fun s1 : state => interp n' (While b Do c1) s1)
          else Res s
      end
  end.

A sample program and its execution. The program computes the quotient and remainder of variables a and b. In concrete syntax: 
       r := a; 
       q := 0;
       while b < r + 1 do 
             r := r - b; q := q + 1 
       done

Open Scope nat_scope.

Definition va : ident := 0.
Definition vb : ident := 1.
Definition vq : ident := 2.
Definition vr : ident := 3.

Open Scope Z_scope.

Definition prog :=
  vr <- va;;
  (vq <- 0;;
   While vb <! vr +! 1 Do
                      (vr <- vr -! vb;; vq <- vq +! 1)).

Compute 13 / 3 and have (4,1)
Definition prog_init_state := update (update initial_state va 13) vb 3.

Definition test_prog fuel:=
  match interp fuel prog prog_init_state with
  | Res s => Some(s vq, s vr)
  | Bot => None
  end.

Eval compute in test_prog 10.

Eval compute in test_prog 5.

The natural ordering over results.

Definition res_le (r1 r2: result) := r1 = Bot \/ r1 = r2.

The interp function is monotone in n with respect to this ordering.

Remark bind_mon:
  forall r1 f1 r2 f2,
  res_le r1 r2 -> (forall s, res_le (f1 s) (f2 s)) ->
  res_le (bind r1 f1) (bind r2 f2).
Proof.
        hauto unfold: res_le, bind. Qed.

Open Scope nat_scope.

Lemma interp_mon:
  forall n n' c s, n <= n' -> res_le (interp n c s) (interp n' c s).
Proof.
  induction n; intros.
  - hauto lq: on .
  - destruct n'.
  + sauto lq: on .
  + assert (n <= n') by lia. simpl.     destruct c; hauto lq:on use: bind_mon brefl:on.
  Qed.

Corollary interp_Res_stable:
  forall n n' c s s',
  n <= n' -> interp n c s = Res s' -> interp n' c s = Res s'.
Proof.
        hauto use: interp_mon unfold: res_le.
Qed.

It follows an equivalence between termination according to the natural semantics and the fact that interp n c s returns Res for a suitably large n.

Remark bind_Res_inversion:
  forall r f s, bind r f = Res s -> exists s1, r = Res s1 /\ f s1 = Res s.
Proof.
sauto lq: on .
Qed.

Lemma interp_exec:
  forall n c s s', interp n c s = Res s' -> exec s c s'.
Proof.
  induction n; intros until s'; simpl.
  + congruence.
  + destruct c;
  time try sauto lq: on rew: off use: bind_Res_inversion.

  -
    destruct (eval_bool_expr s b) eqn: EE;
     sauto brefl:on lq: on rew: off use: bind_Res_inversion.
Qed.

Hint Resolve Max.le_max_l Max.le_max_r : core.

Automation does not work here
Lemma exec_interp:
  forall s c s', exec s c s' -> exists n, interp n c s = Res s'.
Proof.
  induction 1.
-
  exists 1%nat. auto.
-
  exists 1%nat. reflexivity.
-
  destruct IHexec1 as [n1 I1]. destruct IHexec2 as [n2 I2].
    exists (S (max n1 n2)). simpl.
  rewrite (interp_Res_stable n1 (max n1 n2) c1 s s1); auto. simpl.
  rewrite (interp_Res_stable n2 (max n1 n2) c2 s1 s2); auto.
-
  destruct IHexec as [n I]. exists (S n); simpl. auto.
-
  destruct IHexec1 as [n1 I1]. destruct IHexec2 as [n2 I2].
  exists (S (max n1 n2)). simpl. rewrite H.
  rewrite (interp_Res_stable n1 (max n1 n2) c s s1); auto. simpl.
  apply interp_Res_stable with n2; auto.
-
  exists 1%nat. simpl. now rewrite H.
Qed.

Again, proof reconstruction fails
Corollary exec_interp_either:
  forall s c s' n, exec s c s' -> interp n c s = Bot \/ interp n c s = Res s'.
Proof.
    intros.
  destruct (exec_interp _ _ _ H) as [m I].
  destruct (le_ge_dec n m).
    rewrite <- I. change (res_le (interp n c s) (interp m c s)). apply interp_mon; auto.
  right. eapply interp_Res_stable; eauto.
Qed.

Bonus material

Program equivalence

Towards showing correctness of compilation with with programs involving mutable state, we need a notion, called behavioral equivalence:
We do this by defining command equivalence as "if the first one terminates in a particular state then so does the second, and vice versa":

Definition equiv_cmd (c1 c2 : cmd) :=
  forall s s', c1 >> s ==> s' <-> c2 >> s ==> s'.

Notation "A ~~ B" := (equiv_cmd A B) (at level 75, no associativity).

It's an equivalence relation
Lemma lem_sim_refl : forall c, c ~~ c.
Proof.
  sfirstorder.
Qed.

Lemma lem_sim_sym : forall c c', c ~~ c' -> c' ~~ c.
Proof.
  sfirstorder unfold: equiv_cmd.
Qed.

Lemma lem_sim_trans : forall c1 c2 c3, c1 ~~ c2 -> c2 ~~ c3 -> c1 ~~ c3.
Proof.
  sauto unfold: equiv_cmd.
Qed.

Some equivalence properties of commands:
Skip vs sequence.
Lemma skip_left : forall c,
    (Cskip;; c ) ~~ c.
Proof.
  sauto lq: on unfold: equiv_cmd.
Qed.

Lemma skip_right : forall c,
    (c;; Cskip) ~~ c.
Proof.
  sauto lq: on unfold: equiv_cmd.
Qed.

Sequence is associative
Lemma lem_seq_assoc : forall c1 c2 c3, c1;; (c2;; c3) ~~ (c1;; c2);; c3.
Proof.
  sauto l: on unfold: equiv_cmd.
Qed.

Definition Btrue := Bequal (Econst 0) (Econst 0).
Definition Bfalse := Bequal (Econst 0) (Econst 1).

Conditionals
Lemma lem_triv_if_true : forall c1 c2, If Btrue Then c1 Else c2 ~~ c1.
Proof.
    sauto unfold: equiv_cmd.
Qed.

Lemma lem_triv_if_false : forall c1 c2, If Bfalse Then c1 Else c2 ~~ c2.
Proof.
    sauto unfold: equiv_cmd.
Qed.

Lemma lem_triv_if : forall b c, If b Then c Else c ~~ c.
Proof.
    sauto unfold: equiv_cmd.
Qed.

Lemma lem_commute_if :
  forall b1 b2 c1 c2 c3,
    If b1 Then (If b2 Then c1 Else c2) Else c3 ~~
       If b2 Then (If b1 Then c1 Else c3) Else (If b1 Then c2 Else c3).
Proof.
    unfold equiv_cmd.
    intros .
      time (destruct (eval_bool_expr s b1) eqn:?; destruct (eval_bool_expr s b2) eqn:?;
                        sauto qb: on).
Qed.

Unfolding of while
Lemma lem_unfold_while : forall b c,
    While b Do c ~~ If b Then c;; While b Do c Else Cskip.
Proof.
  sauto unfold: equiv_cmd.
  Qed.

We assume some lemmas about updating the state
Print update.
Theorem t_update_same : forall (s : state) x,
    update s x (s x) = s.
Proof.
  Admitted.

Lemma update_other: forall x v s y, x <> y -> (update s x v ) y = s y.
Proof.
  Admitted.

Theorem identity_assignment : forall x,
    x <- x ~~ Cskip.
Proof.
        split.
    - sauto ctrs:exec use:t_update_same.
    - assert (Hx : exec s' ( x <- x) (update s' x (s' x)));
         sauto dep:on depth: 5 ctrs:exec use:t_update_same.
Qed.

Exercise

Define equivalence for arithmentic and boolean expressions and show that these are equivalence relations. Then generalize the above congruence property to account for equivalence of expressions.

Congruence

Lemma lem_while_cong_aux : forall b c c' s s',
  While b Do c >> s ==> s' -> c ~~ c' -> While b Do c' >> s ==> s'.
Proof.
  intros .
  remember (While b Do c).
  induction H; sauto lq: on unfold: equiv_cmd.
Qed.

Lemma lem_while_cong : forall b c c',
  c ~~ c' -> While b Do c ~~ While b Do c'.
Proof.
  hauto use: lem_while_cong_aux unfold: equiv_cmd.
Qed.

Lemma CSeq_congruence : forall c1 c1' c2 c2',
   c1 ~~ c1' -> c2 ~~ c2' ->
  (c1 ;; c2) ~~ ( c1';; c2') .
  Proof.
   sauto lq: on unfold: equiv_cmd.
Qed.

Lemma lem_if_cong : forall b c1 c1' c2 c2',
  c1 ~~ c1' -> c2 ~~ c2' ->
  If b Then c1 Else c2 ~~ If b Then c1' Else c2'.
  Proof.
     sauto use: exec_if unfold: equiv_cmd.
Qed.

Now we can show that two programs are equivalent just by concentrating on the bit they differ, rather than using the operational semantics. This is a big deal.
A trivial example, where we make a non-sensical modification of the quotient program of before.
In fact, this is silly, since by simplification they *are* the same code, but use your imagination.

  Print prog.

Definition prog1 :=
  vr <- va;;
  ( vq <- (Econst ( 1 - 1));;
   While vb <! vr +! (Econst 1) Do
                      (vr <- vr -! vb;; vq <- vq +! (Econst 1))).

Example cong: prog ~~ prog1.
Proof.
  unfold prog, prog1.
  eapply CSeq_congruence.
  - sfirstorder.
  - eapply CSeq_congruence. simpl.
     + sfirstorder.
     + sfirstorder.
Restart.
sfirstorder unfold: prog, prog1.
Qed.

Part 2. Axiomatic semantics and program proof

Assertions over states.

Definition assertion := state -> Prop.

Definition aupdate (P: assertion) (x: ident) (e: expr) : assertion :=
  fun s => P (update s x (eval_expr s e)).

Definition atrue (be: bool_expr) : assertion :=
  fun s => eval_bool_expr s be = true.

Definition afalse (be: bool_expr) : assertion :=
  fun s => eval_bool_expr s be = false.

Definition aand (P Q: assertion) : assertion :=
  fun s => P s /\ Q s.

Definition aor (P Q: assertion) : assertion :=
  fun s => P s \/ Q s.

Definition aimp (P Q: assertion) : Prop :=
  forall s, P s -> Q s.

A few notations to improve legibility.

Notation "P -->> Q" := (aimp P Q) (at level 95, no associativity).
Notation "P //\\ Q" := (aand P Q) (at level 80, right associativity).
Notation "P \\// Q" := (aor P Q) (at level 75, right associativity).

The rules of the axiomatic semantics, defining valid weak Hoare triples {P} c {Q}.

Inductive triple: assertion -> cmd -> assertion -> Prop :=
  | triple_skip: forall P,
      triple P Cskip P

  | triple_assign: forall P x e,
      triple (aupdate P x e) (Cassign x e) P

  | triple_seq: forall c1 c2 P Q R,
      triple P c1 Q -> triple Q c2 R ->
      triple P (Cseq c1 c2) R

  | triple_if: forall be c1 c2 P Q,
      triple (aand (atrue be) P) c1 Q ->
      triple (aand (afalse be) P) c2 Q ->
      triple P (Cifthenelse be c1 c2) Q

  | triple_while: forall be c P,
      triple (aand (atrue be) P) c P ->
      triple P (Cwhile be c) (aand (afalse be) P)

  | triple_consequence: forall c P Q P' Q',
      triple P' c Q' -> aimp P P' -> aimp Q' Q ->
      triple P c Q.

Notation "|- {{ P }} c {{ Q }}" := (triple P c Q).

An example: proving max correct.
Open Scope nat_scope.

Definition X : ident := 0.
Definition Y : ident := 1.

Open Scope Z_scope.

Search max.
Lemma max_correct (a b : Z) :
       |- {{fun s : state => s X = a /\ s Y = b}} If X <! Y Then Cskip Else Y <- X {{fun s : state => s Y = Z.max a b}}.
Proof.
  apply triple_if.
  - eapply triple_consequence with (Q':=fun s : state => s Y = Z.max a b).
    + econstructor.
    + unfold atrue, aimp,aand. sauto.
    + unfold aimp. sauto.
  -
    eapply triple_consequence with (Q':=fun s : state => s Y = Z.max a b).
    + eapply triple_assign.
    + unfold atrue, aimp,aand, aupdate,update. sauto.
    + unfold aimp. sauto.

Restart.
      apply triple_if.
  - eapply triple_consequence with (Q':=fun s : state => s Y = Z.max a b);
      sauto unfold: aimp.
  - eapply triple_consequence with (Q':=fun s : state => s Y = Z.max a b);
     sauto b:on use: triple_assign unfold: aimp, aupdate,update.
Qed.
Close Scope nat_scope.

Semantic interpretation of weak Hoare triples in terms of concrete executions.

CoInductive finally: state -> cmd -> assertion -> Prop :=
  | finally_done: forall s (Q: assertion),
      Q s ->
      finally s Cskip Q

  | finally_step: forall c s c' s' Q,
      red (c, s) (c', s') -> finally s' c' Q ->
      finally s c Q.

Definition sem_triple (P: assertion) (c: cmd) (Q: assertion) :=
  forall s, P s -> finally s c Q.

Notation "|= {{ P }} c {{ Q }}" := (sem_triple P c Q).

Lemma finally_seq:
  forall c1 c2 s Q R,
  finally s c1 Q -> sem_triple Q c2 R -> finally s (Cseq c1 c2) R.
Proof.
  cofix COINDHYP; intros.
  inv H.
  apply finally_step with c2 s.
  - apply red_seq_skip.
    - auto.
- apply finally_step with (Cseq c' c2) s'.
    apply red_seq_left; auto.
    apply COINDHYP with Q. auto. auto.
Qed.

Lemma finally_while:
  forall be c P,
  sem_triple (aand (atrue be) P) c P ->
  sem_triple P (Cwhile be c) (aand (afalse be) P).
Proof.
  cofix COINDHYP1; intros.
  red; intros.
  destruct (eval_bool_expr s be) eqn:BE.
-
  apply finally_step with (Cseq c (Cwhile be c)) s.
  apply red_while_true; auto.
  assert (LOOP: forall c' s',
          finally s' c' P ->
          finally s' (Cseq c' (Cwhile be c)) (aand (afalse be) P)).
  {
    cofix COINDHYP2; intros.
    inv H1.
  + apply finally_step with (Cwhile be c) s'. apply red_seq_skip.
    apply COINDHYP1. auto. auto.
  + apply finally_step with (Cseq c'0 (Cwhile be c)) s'0.
    apply red_seq_left. auto.
    apply COINDHYP2. auto.
  }
  apply LOOP. apply H. split; auto.
-
  apply finally_step with Cskip s.
  apply red_while_false; auto.
  apply finally_done. split; auto.
Qed.

Lemma finally_consequence:
  forall s c Q Q', aimp Q Q' -> finally s c Q -> finally s c Q'.
Proof.
  cofix COINDHYP; intros. inv H0.
  apply finally_done. auto.
  apply finally_step with c' s'. auto. apply COINDHYP with Q; auto.
Qed.

Every derivable Hoare triple is semantically valid.

Lemma triple_correct:
   forall (P : assertion) (c : cmd) (Q : assertion),
       |- {{P}} c {{Q}} -> |= {{P}} c {{Q}}.
Proof.
  induction 1.
  -
    hauto l: on ctrs: finally.
-
   hfcrush l: on ctrs: finally, red.
-
  sauto use: finally_seq unfold: sem_triple.
-
  red. intros. destruct (eval_bool_expr s be) eqn:BE;
  hauto lq: on unfold: sem_triple use: finally_step , red_if_true, red_if_false.

- apply finally_while. auto.
-
  sfirstorder use: finally_consequence unfold: sem_triple.
Qed.

Weakest precondition calculus & verification condition generation

Inductive acmd : Type :=
  | Askip: acmd
  | Aassign: ident -> expr -> acmd
  | Aseq: acmd -> acmd -> acmd
  | Aifthenelse: bool_expr -> acmd -> acmd -> acmd
  | Awhile: bool_expr -> assertion -> acmd -> acmd
  | Aassert: assertion -> acmd.

Notation "A <- B" := (Aassign A B) (at level 60).
Notation "A ;; B" := (Aseq A B) (at level 70).
Notation "'If' A 'Then' B 'Else' C" := (Aifthenelse A B C) (at level 65).
Notation "'While' '{{' Inv '}}' A 'Do' B" := (Awhile A Inv B) (at level 65).

wp a Q computes the weakest precondition for command a with postcondition Q.

Fixpoint wp (a: acmd) (Q: assertion) {struct a} : assertion :=
  match a with
  | Askip => Q
  | Aassign x e => aupdate Q x e
  | Aseq a1 a2 => wp a1 (wp a2 Q)
  | Aifthenelse b a1 a2 => aor (aand (atrue b) (wp a1 Q)) (aand (afalse b) (wp a2 Q))
  | Awhile b P a1 => P
  | Aassert P => P
  end.

vcg a Q computes a logical formula which, if true, implies that the triple {wp a Q} a Q holds.

Fixpoint vcg (a: acmd) (Q: assertion) {struct a} : Prop :=
  match a with
  | Askip => True
  | Aassign x e => True
  | Aseq a1 a2 => vcg a1 (wp a2 Q) /\ vcg a2 Q
  | Aifthenelse b a1 a2 => vcg a1 Q /\ vcg a2 Q
  | Awhile b P a1 =>
      vcg a1 P /\
      aimp (aand (afalse b) P) Q /\
      aimp (aand (atrue b) P) (wp a1 P)
  | Aassert P =>
      aimp P Q
  end.

Definition vcgen (P: assertion) (a: acmd) (Q: assertion) : Prop :=
  aimp P (wp a Q) /\ vcg a Q.

Mapping annotated commands back to regular commands.

Fixpoint erase (a: acmd) {struct a} : cmd :=
  match a with
  | Askip => Cskip
  | Aassign x e => Cassign x e
  | Aseq a1 a2 => Cseq (erase a1) (erase a2)
  | Aifthenelse b a1 a2 => Cifthenelse b (erase a1) (erase a2)
  | Awhile b P a1 => Cwhile b (erase a1)
  | Aassert P => Cskip
  end.

Correctness of wp and vcg.

Lemma vcg_correct:
  forall a Q, vcg a Q -> triple (wp a Q) (erase a) Q.
Proof.
  induction a; simpl; intros.
-
  sfirstorder. -
  sfirstorder. -
  sauto lq: on.
-
  destruct H.
  apply triple_if.
  + apply triple_consequence with (wp a1 Q) Q;
       hauto unfold: aimp, afalse, aor, atrue, aand.
  + apply triple_consequence with (wp a2 Q) Q;
      hauto unfold: aimp, afalse, aor, atrue, aand.
-
  destruct H as [A [B C]].
  apply triple_consequence with a (aand (afalse b) a);
    sauto use: triple_while, triple_consequence unfold: aimp.

   - sfirstorder use: triple_consequence, triple_skip unfold: aimp.
Qed.

Theorem vcgen_correct:
  forall P a Q, vcgen P a Q -> triple P (erase a) Q.
Proof.
        hauto use: triple_consequence, vcg_correct unfold: aimp.
Qed.

Example of verification.

Open Scope Z_scope.

Definition precondition : assertion :=
  fun s => s va >= 0 /\ s vb > 0.

Definition invariant : assertion :=
  fun s => s vr >= 0 /\ s vb > 0 /\ s va = s vb * s vq + s vr.

Definition postcondition : assertion :=
  fun s => s vq = s va / s vb.

The program is the earlier Euclidean division example annotated with a loop invariant. 
       r := a; q := 0;
       while b < r + 1 do {invariant}  r := r - b; q := q + 1 done
Definition aprog :=
  vr <- va;;
(vq <- 0;;
 While {{invariant}} vb <! vr +! 1
                                  Do (vr <- vr -! vb;; vq <- vq +! 1)).

Lemma aprog_correct:
  triple precondition (erase aprog) postcondition.
Proof.
  apply vcgen_correct.
  unfold aprog.
  unfold vcgen. simpl. unfold aimp, aand, afalse, atrue, aupdate; simpl.
  intuition.
  -
1- invariant holds initially (r = a and q = 0)
    hauto drew: off unfold: precondition, invariant, update.

  -
2- invariant and b >= r+1 imply postcondition
   
    unfold invariant in H1. unfold postcondition.
    qauto use: Z.le_gt_cases, Z.le_succ_l, Z.ge_le, Z.div_unique.

  -
3- invariant is preserved by assignment r := r - b; q := q + 1
        destruct (Z_lt_dec (s vb) (s vr + 1)); try congruence.
  unfold invariant in H1. unfold invariant, update; simpl. intuition.
Qed.