(** * Hoare2: Hoare Logic, Part II *)



Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Strings.String.
From PLF 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 Lia.
From PLF Require Export Imp.
From PLF Require Import Hoare.

(* QUIZ

    On a piece of paper, write down a specification (as
    a Hoare triple) for the following program:

    X := 2;
    Y := X + X

*)

(* QUIZ

    Write down a (useful) specification for the following program:

    X := X + 1; Y := X + 1
*)

(* QUIZ

    Write down a (useful) specification for the following program:

    if X <= Y
    then skip
    else
      Z := X;
      X := Y;
      Y := Z
    end
*)

(* QUIZ

    Write down a (useful) specification for the following program:

    X := m;
    Z := 0;
    while ~(X = 0) do
      X := X - 2;
      Z := Z + 1
    end
*)

(* ################################################################# *)
(** * Decorated Programs *)

(** The beauty of Hoare Logic is that it is _compositional_: the
    structure of proofs exactly follows the structure of programs.

    It follows that, as we saw in [Hoare], we can record the
    essential ideas of a proof (informally, and leaving out some
    low-level calculational details) by "decorating" a program with
    appropriate assertions on each of its commands.

    Such a _decorated program_ carries within it an argument for its
    own correctness. *)

(** For example, consider the program:

    X := m;
    Z := p;
    while ~(X = 0) do
      Z := Z - 1;
      X := X - 1
    end
*)
(** Here is one possible specification for this program:

      {{ True }}
    X := m;
    Z := p;
    while ~(X = 0) do
      Z := Z - 1;
      X := X - 1
    end
      {{ Z = p - m }}

   Note the _parameters_ [m] and [p], which stand for
   fixed-but-arbitrary numbers.  Formally, they are simply Coq
   variables of type [nat].
*)
(** Here is a decorated version of the program, embodying a
    proof of this specification:

      {{ True }} ->>
      {{ m = m }}
    X := m;
      {{ X = m }} ->>
      {{ X = m /\ p = p }}
    Z := p;
      {{ X = m /\ Z = p }} ->>
      {{ Z - X = p - m }}
    while ~(X = 0) do
        {{ Z - X = p - m /\ X <> 0 }} ->>
        {{ (Z - 1) - (X - 1) = p - m }}
      Z := Z - 1;
        {{ Z - (X - 1) = p - m }}
      X := X - 1
        {{ Z - X = p - m }}
    end
      {{ Z - X = p - m /\ ~ (X <> 0) }} ->>
      {{ Z = p - m }}
*)

(** Concretely, a decorated program consists of the program text
    interleaved with assertions (or possibly multiple assertions
    separated by implications). *)

(** To check that a decorated program represents a valid proof, we
    check that each individual command is _locally consistent_ with
    its nearby assertions in the following sense: *)

(** - [skip] is locally consistent if its precondition and
      postcondition are the same:

          {{ P }} skip {{ P }}
*)
(** - The sequential composition of [c1] and [c2] is locally
      consistent (with respect to assertions [P] and [R]) if [c1] is
      locally consistent (with respect to [P] and [Q]) and [c2] is
      locally consistent (with respect to [Q] and [R]):

          {{ P }} c1; {{ Q }} c2 {{ R }}
*)
(** - An assignment [X ::= a] is locally consistent with respect to
      a precondition of the form [P [X |-> a]] and the postcondition [P]:

          {{ P [X |-> a] }}
          X := a
          {{ P }}
*)
(** - A conditional is locally consistent with respect to assertions
      [P] and [Q] if its "then" branch is locally consistent with respect
      to [P /\ b] and [Q]) and its "else" branch is locally consistent
      with respect to [P /\ ~b] and [Q]:

          {{ P }}
          if b then
            {{ P /\ b }}
            c1
            {{ Q }}
          else
            {{ P /\ ~b }}
            c2
            {{ Q }}
          end
          {{ Q }}
*)
(** - A while loop with precondition [P] is locally consistent if its
      postcondition is [P /\ ~b], if the pre- and postconditions of
      its body are exactly [P /\ b] and [P], and if its body is
      locally consistent with respect to assertions [P /\ b] and [P]:

          {{ P }}
          while b do
            {{ P /\ b }}
            c1
            {{ P }}
          end
          {{ P /\ ~b }}
*)
(** - A pair of assertions separated by [->>] is locally consistent if
      the first implies the second:

          {{ P }} ->>
          {{ P' }}

      This corresponds to the application of [hoare_consequence], and it
      is the _only_ place in a decorated program where checking whether
      decorations are correct is not fully mechanical and syntactic,
      but rather may involve logical and/or arithmetic reasoning. *)

(* ================================================================= *)
(** ** Example: Swapping Using Addition and Subtraction *)

(** Here is a program that swaps the values of two variables using
    addition and subtraction (instead of by assigning to a temporary
    variable).

       X := X + Y;
       Y := X - Y;
       X := X - Y

    We can prove (informally) using decorations that this program is
    correct -- i.e., it always swaps the values of variables [X] and [Y]. *)
(* WORK IN CLASS *)

(* ================================================================= *)
(** ** Example: Simple Conditionals *)

(** Here's a simple program using conditionals, with a possible
    specification:

         {{ True }}
       if X <= Y then
         Z := Y - X
       else
         Z := X - Y
       end
         {{ Z + X = Y \/ Z + Y = X }}

    Let's turn it into a decorated program...
*)
(* WORK IN CLASS *)

(* ================================================================= *)
(** ** Example: Reduce to Zero *)

(** Here is a very simple [while] loop with a simple
    specification:

          {{ True }}
        while ~(X = 0) do
          X := X - 1
        end
          {{ X = 0 }}

*)
(* WORK IN CLASS *)

(** From an informal proof in the form of a decorated program, it is
    easy to read off a formal proof using the Coq versions of the
    Hoare rules.  Note that we do _not_ unfold the definition of
    [hoare_triple] anywhere in this proof -- the idea is to use the
    Hoare rules as a self-contained logic for reasoning about
    programs. *)

Definition reduce_to_zero' : com :=
  <{ while ~(X = 0) do
       X := X - 1
     end }>.

Theorem reduce_to_zero_correct' :
  {{True}}
    reduce_to_zero'
  {{X = 0}}.
Proof.
  unfold reduce_to_zero'.
  (* First we need to transform the postcondition so
     that hoare_while will apply. *)
  eapply hoare_consequence_post.
  - apply hoare_while.
    + (* Loop body preserves invariant *)
      (* Need to massage precondition before [hoare_asgn] applies *)
      eapply hoare_consequence_pre.
      * apply hoare_asgn.
      * (* Proving trivial implication (2) ->> (3) *)
        unfold assn_sub, "->>". simpl. intros. exact I.
  - (* Invariant and negated guard imply postcondition *)
    intros st [Inv GuardFalse].
    unfold bassn in GuardFalse. simpl in GuardFalse.
    rewrite not_true_iff_false in GuardFalse.
    rewrite negb_false_iff in GuardFalse.
    apply eqb_eq in GuardFalse.
    apply GuardFalse.
Qed.

(** In [Hoare] we introduced a series of tactics named [assn_auto]
    to automate proofs involving just assertions.  We can try using
    the most advanced of those tactics to streamline the previous proof: *)

Theorem reduce_to_zero_correct'' :
  {{True}}
  reduce_to_zero'
  {{X = 0}}.
Proof.
  unfold reduce_to_zero'.
  eapply hoare_consequence_post.
  - apply hoare_while.
    + eapply hoare_consequence_pre.
      * apply hoare_asgn.
      * assn_auto''.
  - assn_auto''. (* doesn't succeed *)
Abort.

(** Automation to the rescue! *)

Ltac verify_assn :=
  repeat split;
  simpl; unfold assert_implies;
  unfold ap in *; unfold ap2 in *;
  unfold bassn in *; unfold beval in *; unfold aeval in *;
  unfold assn_sub; intros;
  repeat (simpl in *;
          rewrite t_update_eq ||
          (try rewrite t_update_neq; [| (intro X; inversion X; fail)]));
  simpl in *;
  repeat match goal with [H : _ /\ _ |- _] => destruct H end;
  repeat rewrite not_true_iff_false in *;
  repeat rewrite not_false_iff_true in *;
  repeat rewrite negb_true_iff in *;
  repeat rewrite negb_false_iff in *;
  repeat rewrite eqb_eq in *;
  repeat rewrite eqb_neq in *;
  repeat rewrite leb_iff in *;
  repeat rewrite leb_iff_conv in *;
  try subst;
  simpl in *;
  repeat
    match goal with
      [st : state |- _] =>
        match goal with
        | [H : st _ = _ |- _] => rewrite -> H in *; clear H
        | [H : _ = st _ |- _] => rewrite <- H in *; clear H
        end
    end;
  try eauto; try lia.

(** All that automation makes it easy to verify [reduce_to_zero']: *)

Theorem reduce_to_zero_correct''' :
  {{True}}
  reduce_to_zero'
  {{X = 0}}.
Proof.
  unfold reduce_to_zero'.
  eapply hoare_consequence_post.
  - apply hoare_while.
    + eapply hoare_consequence_pre.
      * apply hoare_asgn.
      * verify_assn.
  - verify_assn.
Qed.

(* ================================================================= *)
(** ** Example: Division *)

(** The following Imp program calculates the integer quotient and
    remainder of parameters [m] and [n].

       X := m;
       Y := 0;
       while n <= X do
         X := X - n;
         Y := Y + 1
       end;

    If we replace [m] and [n] by numbers and execute the program, it
    will terminate with the variable [X] set to the remainder when [m]
    is divided by [n] and [Y] set to the quotient.

    Here's a possible specification:

        {{ True }}
      X := m;
      Y := 0;
      while n <= X do
        X := X - n;
        Y := Y + 1
      end
        {{ n * Y + X = m /\ X < n }}
*)
(* WORK IN CLASS *)

(* ################################################################# *)
(** * Finding Loop Invariants *)

(** Once the outer pre- and postcondition are chosen, the only
    creative part in verifying programs using Hoare Logic is finding
    the right loop invariants... *)

(* ================================================================= *)
(** ** Example: Slow Subtraction *)

(** The following program subtracts the value of [X] from the value of
    [Y] by repeatedly decrementing both [X] and [Y].  We want to verify its
    correctness with respect to the pre- and postconditions shown:

             {{ X = m /\ Y = n }}
           while ~(X = 0) do
             Y := Y - 1;
             X := X - 1
           end
             {{ Y = n - m }}
*)

(** To verify this program, we need to find an invariant [Inv] for the
    loop.  As a first step we can leave [Inv] as an unknown and build a
    _skeleton_ for the proof by applying the rules for local
    consistency (working from the end of the program to the beginning,
    as usual, and without any thinking at all yet).

    This leads to the following skeleton:

        (1)      {{ X = m /\ Y = n }}  ->>             (a)
        (2)      {{ Inv }}
               while ~(X = 0) do
        (3)        {{ Inv /\ X <> 0 }}  ->>              (c)
        (4)        {{ Inv [X |-> X-1] [Y |-> Y-1] }}
                 Y := Y - 1;
        (5)        {{ Inv [X |-> X-1] }}
                 X := X - 1
        (6)        {{ Inv }}
               end
        (7)      {{ Inv /\ ~ (X <> 0) }}  ->>            (b)
        (8)      {{ Y = n - m }}

    By examining this skeleton, we can see that any valid [Inv] will
    have to respect three conditions:
    - (a) it must be _weak_ enough to be implied by the loop's
      precondition, i.e., (1) must imply (2);
    - (b) it must be _strong_ enough to imply the program's postcondition,
      i.e., (7) must imply (8);
    - (c) it must be _preserved_ by each iteration of the loop (given
      that the loop guard evaluates to true), i.e., (3) must imply (4). *)

(* WORK IN CLASS *)

(* ================================================================= *)
(** ** Example: Parity *)

(** Here is a cute little program for computing the parity of the
    value initially stored in [X] (due to Daniel Cristofani).

         {{ X = m }}
       while 2 <= X do
         X := X - 2
       end
         {{ X = parity m }}

    The mathematical [parity] function used in the specification is
    defined in Coq as follows: *)

Fixpoint parity x :=
  match x with
  | 0 => 0
  | 1 => 1
  | S (S x') => parity x'
  end.

(* WORK IN CLASS *)

(* ================================================================= *)
(** ** Example: Finding Square Roots *)

(** The following program computes the integer square root of [X]
    by naive iteration:

      {{ X=m }}
    Z := 0;
    while (Z+1)*(Z+1) <= X do
      Z := Z+1
    end
      {{ Z*Z<=m /\ m<(Z+1)*(Z+1) }}
*)

(* WORK IN CLASS *)

(* ================================================================= *)
(** ** Example: Squaring *)

(** Here is a program that squares [X] by repeated addition:

    {{ X = m }}
  Y := 0;
  Z := 0;
  while ~(Y = X)  do
    Z := Z + X;
    Y := Y + 1
  end
    {{ Z = m*m }}
*)

(* WORK IN CLASS *)

(* ################################################################# *)
(** * Formal Decorated Programs (Advanced) *)

(** With a little more work, we can formalize the definition of
    well-formed decorated programs and mostly automate the mechanical
    steps when filling in decorations. *)

(* ================================================================= *)
(** ** Syntax *)

(** _Decorated commands_ contain assertions mostly just as
    postconditions, omitting preconditions where possible and letting
    the context supply them.

    The alternative--decorating every command with both a pre- and
    postcondition--would be too heavyweight. E.g., [skip; skip] would
    become:

        {{P}} ({{P}} skip {{P}}) ; ({{P}} skip {{P}}) {{P}},
*)

(** Specifically, we decorate as follows:

    - Command [skip] is decorated only with its postcondition, as
      [skip {{ Q }}].

    - Sequence [d1 ;; d2] contains no additional decoration.  Inside
      [d2] there will be a postcondition; that serves as the
      postcondition of [d1 ;; d2].  Inside [d1] there will also be a
      postcondition; it additionally serves as the precondition for
      [d2].

    - Assignment [X ::= a] is decorated only with its postcondition,
      as [X ::= a {{ Q }}].

    - If statement [if b then d1 else d2] is decorated with a
      postcondition for the entire statement, as well as preconditions
      for each branch, as
      [if b then {{ P1 }} d1 else {{ P2 }} d2 end {{ Q }}].

    - While loop [while b do d end] is decorated with its
      postcondition and a precondition for the body, as
      [while b do {{ P }} d end {{ Q }}].  The postcondition inside
      [d] serves as the loop invariant.

    - Implications [->>] are added as decorations for a precondition
      as [->> {{ P }} d], or for a postcondition as [d ->> {{ Q }}].
      The former is waiting for another precondition to eventually be
      supplied, e.g., [{{ P'}} ->> {{ P }} d], and the latter relies
      on the postcondition already embedded in [d].
*)

Inductive dcom : Type :=
| DCSkip (Q : Assertion)
  (* skip {{ Q }} *)
| DCSeq (d1 d2 : dcom)
  (* d1 ;; d2 *)
| DCAsgn (X : string) (a : aexp) (Q : Assertion)
  (* X := a {{ Q }} *)
| DCIf (b : bexp) (P1 : Assertion) (d1 : dcom)
       (P2 : Assertion) (d2 : dcom) (Q : Assertion)
  (* if b then {{ P1 }} d1 else {{ P2 }} d2 end {{ Q }} *)
| DCWhile (b : bexp) (P : Assertion) (d : dcom) (Q : Assertion)
  (* while b do {{ P }} d end {{ Q }} *)
| DCPre (P : Assertion) (d : dcom)
  (* ->> {{ P }} d *)
| DCPost (d : dcom) (Q : Assertion)
  (* d ->> {{ Q }} *)
.

(** [DCPre] is used to provide the weakened precondition from
    the rule of consequence. To provide the initial precondition
    at the very top of the program, we use [Decorated]: *)

Inductive decorated : Type :=
  | Decorated : Assertion -> dcom -> decorated.

(** To avoid clashing with the existing [Notation] definitions for
    ordinary [com]mands, we introduce these notations in a custom entry
    notation called [dcom]. *)

Declare Scope dcom_scope.
Notation "'skip' {{ P }}"
      := (DCSkip P)
      (in custom com at level 0, P constr) : dcom_scope.
Notation "l ':=' a {{ P }}"
      := (DCAsgn l a P)
      (in custom com at level 0, l constr at level 0,
          a custom com at level 85, P constr, no associativity) : dcom_scope.
Notation "'while' b 'do' {{ Pbody }} d 'end' {{ Ppost }}"
      := (DCWhile b Pbody d Ppost)
           (in custom com at level 89, b custom com at level 99,
           Pbody constr, Ppost constr) : dcom_scope.
Notation "'if' b 'then' {{ P }} d 'else' {{ P' }} d' 'end' {{ Q }}"
      := (DCIf b P d P' d' Q)
           (in custom com at level 89, b custom com at level 99,
               P constr, P' constr, Q constr) : dcom_scope.
Notation "'->>' {{ P }} d"
      := (DCPre P d)
      (in custom com at level 12, right associativity, P constr) : dcom_scope.
Notation "d '->>' {{ P }}"
      := (DCPost d P)
      (in custom com at level 10, right associativity, P constr) : dcom_scope.
Notation " d ; d' "
      := (DCSeq d d')
      (in custom com at level 90, right associativity) : dcom_scope.
Notation "{{ P }} d"
      := (Decorated P d)
      (in custom com at level 91, P constr) : dcom_scope.

Open Scope dcom_scope.

Example dec0 :=
  <{ skip {{ True }} }>.
Example dec1 :=
  <{ while true do {{ True }} skip {{ True }} end
  {{ True }} }>.

(** An example [decorated] program that decrements [X] to [0]: *)

Example dec_while : decorated :=
  <{
  {{ True }}
  while ~(X = 0)
  do
    {{ True /\ (X <> 0) }}
    X := X - 1
    {{ True }}
  end
  {{ True /\  X = 0}} ->>
  {{ X = 0 }} }>.

(** It is easy to go from a [dcom] to a [com] by erasing all
    annotations. *)

Fixpoint extract (d : dcom) : com :=
  match d with
  | DCSkip _           => CSkip
  | DCSeq d1 d2        => CSeq (extract d1) (extract d2)
  | DCAsgn X a _       => CAss X a
  | DCIf b _ d1 _ d2 _ => CIf b (extract d1) (extract d2)
  | DCWhile b _ d _    => CWhile b (extract d)
  | DCPre _ d          => extract d
  | DCPost d _         => extract d
  end.

Definition extract_dec (dec : decorated) : com :=
  match dec with
  | Decorated P d => extract d
  end.

Example extract_while_ex :
  extract_dec dec_while = <{while ~ X = 0 do X := X - 1 end}>.
Proof.
  unfold dec_while.
  reflexivity.
Qed.

(** It is straightforward to extract the precondition and
    postcondition from a decorated program. *)

Fixpoint post (d : dcom) : Assertion :=
  match d with
  | DCSkip P                => P
  | DCSeq d1 d2             => post d2
  | DCAsgn X a Q            => Q
  | DCIf  _ _ d1 _ d2 Q     => Q
  | DCWhile b Pbody c Ppost => Ppost
  | DCPre _ d               => post d
  | DCPost c Q              => Q
  end.

Definition pre_dec (dec : decorated) : Assertion :=
  match dec with
  | Decorated P d => P
  end.

Definition post_dec (dec : decorated) : Assertion :=
  match dec with
  | Decorated P d => post d
  end.

Example pre_dec_while : pre_dec dec_while = True.
Proof. reflexivity. Qed.

Example post_dec_while : post_dec dec_while = (X = 0)%assertion.
Proof. reflexivity. Qed.

(** When is a decorated program correct? *)

Definition dec_correct (dec : decorated) :=
  {{pre_dec dec}} extract_dec dec {{post_dec dec}}.

Example dec_while_triple_correct :
  dec_correct dec_while
 = {{ True }}
   while ~(X = 0) do X := X - 1 end
   {{ X = 0 }}.
Proof. reflexivity. Qed.

(** To check whether this Hoare triple is _valid_, we need a way to
    extract the "proof obligations" from a decorated program. These
    obligations are often called _verification conditions_, because
    they are the facts that must be verified to see that the
    decorations are logically consistent and thus constitute a proof
    of correctness. *)

(* ================================================================= *)
(** ** Extracting Verification Conditions *)

(** The function [verification_conditions] takes a [dcom] [d] together
    with a precondition [P] and returns a _proposition_ that, if it
    can be proved, implies that the triple [{{P}} (extract d) {{post d}}]
    is valid. It does this by walking over [d] and generating a big
    conjunction that includes

    - all the local consistency checks, plus

    - many uses of [->>] to bridge the gap between (i) assertions
      found inside decorated commands and (ii) assertions used by the
      local consistency checks.  These uses correspond applications of
      the consequence rule. *)

Fixpoint verification_conditions (P : Assertion) (d : dcom) : Prop :=
  match d with
  | DCSkip Q =>
      (P ->> Q)
  | DCSeq d1 d2 =>
      verification_conditions P d1
      /\ verification_conditions (post d1) d2
  | DCAsgn X a Q =>
      (P ->> Q [X |-> a])
  | DCIf b P1 d1 P2 d2 Q =>
      ((P /\ b) ->> P1)%assertion
      /\ ((P /\ ~ b) ->> P2)%assertion
      /\ (post d1 ->> Q) /\ (post d2 ->> Q)
      /\ verification_conditions P1 d1
      /\ verification_conditions P2 d2
  | DCWhile b Pbody d Ppost =>
      (* post d is the loop invariant and the initial
         precondition *)
      (P ->> post d)
      /\ ((post d  /\ b) ->> Pbody)%assertion
      /\ ((post d  /\ ~ b) ->> Ppost)%assertion
      /\ verification_conditions Pbody d
  | DCPre P' d =>
      (P ->> P') /\ verification_conditions P' d
  | DCPost d Q =>
      verification_conditions P d /\ (post d ->> Q)
  end.

(** And now the key theorem, stating that [verification_conditions]
    does its job correctly.  Not surprisingly, we need to use each of
    the Hoare Logic rules at some point in the proof. *)

Theorem verification_correct : forall d P,
  verification_conditions P d -> {{P}} extract d {{post d}}.
Proof.
  induction d; intros; simpl in *.
  - (* Skip *)
    eapply hoare_consequence_pre.
      + apply hoare_skip.
      + assumption.
  - (* Seq *)
    destruct H as [H1 H2].
    eapply hoare_seq.
      + apply IHd2. apply H2.
      + apply IHd1. apply H1.
  - (* Asgn *)
    eapply hoare_consequence_pre.
      + apply hoare_asgn.
      + assumption.
  - (* If *)
    destruct H as [HPre1 [HPre2 [Hd1 [Hd2 [HThen HElse] ] ] ] ].
    apply IHd1 in HThen. clear IHd1.
    apply IHd2 in HElse. clear IHd2.
    apply hoare_if.
      + eapply hoare_consequence; eauto.
      + eapply hoare_consequence; eauto.
  - (* While *)
    destruct H as [Hpre [Hbody1 [Hpost1  Hd] ] ].
    eapply hoare_consequence; eauto.
    apply hoare_while.
    eapply hoare_consequence_pre; eauto.
  - (* Pre *)
    destruct H as [HP Hd].
    eapply hoare_consequence_pre; eauto.
  - (* Post *)
    destruct H as [Hd HQ].
    eapply hoare_consequence_post; eauto.
Qed.

(** Now that all the pieces are in place, we can verify an entire program. *)

Definition verification_conditions_dec (dec : decorated) : Prop :=
  match dec with
  | Decorated P d => verification_conditions P d
  end.

Corollary verification_correct_dec : forall dec,
  verification_conditions_dec dec -> dec_correct dec.
Proof.
  intros [P d]. apply verification_correct.
Qed.

(** The propositions generated by [verification_conditions] are fairly
    big, and they contain many conjuncts that are essentially trivial.
    Our [verify_assn] can often take care of them. *)

Example vc_dec_while :
  verification_conditions_dec dec_while =
    ((((fun _ : state => True) ->> (fun _ : state => True)) /\
    ((fun st : state => True /\ negb (st X =? 0) = true) ->>
     (fun st : state => True /\ st X <> 0)) /\
    ((fun st : state => True /\ negb (st X =? 0) <> true) ->>
     (fun st : state => True /\ st X = 0)) /\
    (fun st : state => True /\ st X <> 0) ->> (fun _ : state => True) [X |-> X - 1]) /\
   (fun st : state => True /\ st X = 0) ->> (fun st : state => st X = 0)).
Proof. verify_assn. Qed.

(* ================================================================= *)
(** ** Automation *)

(** To automate the entire process of verification, we can use
    [verification_correct] to extract the verification conditions,
    then use [verify_assn] to verify them (if it can).  *)
Ltac verify :=
  intros;
  apply verification_correct;
  verify_assn.

Theorem Dec_while_correct :
  dec_correct dec_while.
Proof. verify. Qed.

(** Let's use that automation to verify formal decorated programs
    corresponding to informal ones we have seen. *)

(* ----------------------------------------------------------------- *)
(** *** Slow Subtraction *)

Example subtract_slowly_dec (m : nat) (p : nat) : decorated :=
  <{
    {{ X = m /\  Z = p }} ->>
    {{ Z - X = p - m }}
  while ~(X = 0)
  do   {{ Z - X = p - m /\ X  <>  0 }} ->>
       {{ (Z - 1) - (X - 1) = p - m }}
     Z := Z - 1
       {{ Z - (X - 1) = p - m }} ;
     X := X - 1
       {{ Z - X = p - m }}
  end
    {{ Z - X = p - m /\ X = 0 }} ->>
    {{ Z = p - m }} }>.

Theorem subtract_slowly_dec_correct : forall m p,
  dec_correct (subtract_slowly_dec m p).
Proof. verify. (* this grinds for a bit! *) Qed.

(* ----------------------------------------------------------------- *)
(** *** Swapping Using Addition and Subtraction *)

(* Definition swap : com := *)
(*   <{ X := X + Y; *)
(*      Y := X - Y; *)
(*      X := X - Y }>. *)

Definition swap_dec (m n:nat) : decorated :=
  <{
   {{ X = m /\ Y = n}} ->>
   {{ (X + Y) - ((X + Y) - Y) = n
                /\ (X + Y) - Y = m }}
  X := X + Y
   {{ X - (X - Y) = n /\ X - Y = m }};
  Y := X - Y
   {{ X - Y = n /\ Y = m }};
  X := X - Y
   {{ X = n /\ Y = m}} }>.

Theorem swap_correct : forall m n,
  dec_correct (swap_dec m n).
Proof. verify.   Qed.

(** See the full version of the chapter for the rest... *)