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


Set Warnings "-notation-overridden,-parsing".
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.Arith.PeanoNat. Import Nat.
Require Import Coq.omega.Omega.
From LF Require Import Maps.
From LF Require Import Imp.
From LF 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 *)

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

    X ::= X + 1;; Y ::= X + 1
*)
(* /QUIZ *)

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

    IFB X <= Y
    THEN SKIP
    ELSE
      Z ::= X;; 
      X ::= Y;;
      Y ::= Z
    FI
*)
(* /QUIZ *)

(* 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
*)
(* /QUIZ *)

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

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

    This suggests that 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

   (Note the _parameters_ [m] and [p], which stand for
   fixed-but-arbitrary numbers.  Formally, they are simply Coq
   variables of type [nat].)
*)
(** 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 }}
*)
(** 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 (either a single assertion or possibly
    two assertions separated by an implication). *)

(** 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 is locally consistent if its precondition is the
      appropriate substitution of its postcondition:

          {{ P [X |-> a] }}
          X ::= a
          {{ P }}
*)
(** - A conditional is locally consistent (with respect to assertions
      [P] and [Q]) if the assertions at the top of its "then" and
      "else" branches are exactly [P /\ b] and [P /\ ~b] and 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 }}
          IFB b THEN
            {{ P /\ b }}
            c1
            {{ Q }}
          ELSE
            {{ P /\ ~b }}
            c2
            {{ Q }}
          FI
          {{ 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:

          {{ 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 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 }}
       IFB X <= Y THEN
         Z ::= Y - X
       ELSE
         Z ::= X - Y
       FI
         {{ Z + X = Y \/ Z + Y = X }}

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

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

(** The following Imp program calculates the integer quotient and
    remainder of two numbers [m] and [n] that are arbitrary constants
    in the program.

       X ::= m;;
       Y ::= 0;;
       WHILE n <= X DO
         X ::= X - n;;
         Y ::= Y + 1
       END;

    In we replace [m] and [n] by concrete 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 [I] for the
    loop.  As a first step we can leave [I] 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)      {{ I }}
               WHILE !(X = 0) DO
        (3)        {{ I /\ X <> 0 }}  ->>              (c)
        (4)        {{ I [X |-> X-1] [Y |-> Y-1] }}
                 Y ::= Y - 1;;
        (5)        {{ I [X |-> X-1] }}
                 X ::= X - 1
        (6)        {{ I }}
               END
        (7)      {{ I /\ ~ (X <> 0) }}  ->>            (b)
        (8)      {{ Y = n - m }}

    By examining this skeleton, we can see that any valid [I] 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 one iteration of the loop, 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 (Optional) *)

(** 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 *)

(** The first thing we need to do is to formalize a variant of the
    syntax of commands with embedded assertions.  We call the new
    commands _decorated commands_, or [dcom]s. *)

(** We don't want both preconditions and postconditions on each
    command, because a sequence of two commands would contain
    redundant decorations, the postcondition of the first likely
    being the same as the precondition of the second. Instead,
    decorations are added corresponding to each postcondition.
    A separate type, [decorated], is used to add the precondition
    for the entire program. **)

Inductive dcom : Type :=
  | DCSkip :  Assertion -> dcom
  | DCSeq : dcom -> dcom -> dcom
  | DCAsgn : string -> aexp ->  Assertion -> dcom
  | DCIf : bexp ->  Assertion -> dcom ->  Assertion -> dcom
           -> Assertion-> dcom
  | DCWhile : bexp -> Assertion -> dcom -> Assertion -> dcom
  | DCPre : Assertion -> dcom -> dcom
  | DCPost : dcom -> Assertion -> dcom.

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

Notation "'SKIP' {{ P }}"
      := (DCSkip P)
      (at level 10) : dcom_scope.
Notation "l '::=' a {{ P }}"
      := (DCAsgn l a P)
      (at level 60, a at next level) : dcom_scope.
Notation "'WHILE' b 'DO' {{ Pbody }} d 'END' {{ Ppost }}"
      := (DCWhile b Pbody d Ppost)
      (at level 80, right associativity) : dcom_scope.
Notation "'IFB' b 'THEN' {{ P }} d 'ELSE' {{ P' }} d' 'FI' {{ Q }}"
      := (DCIf b P d P' d' Q)
      (at level 80, right associativity)  : dcom_scope.
Notation "'->>' {{ P }} d"
      := (DCPre P d)
      (at level 90, right associativity)  : dcom_scope.
Notation "d '->>' {{ P }}"
      := (DCPost d P)
      (at level 80, right associativity)  : dcom_scope.
Notation " d ;; d' "
      := (DCSeq d d')
      (at level 80, right associativity)  : dcom_scope.
Notation "{{ P }} d"
      := (Decorated P d)
      (at level 90)  : dcom_scope.

Delimit Scope dcom_scope with dcom.
Open Scope dcom_scope.
(** To avoid clashing with the existing [Notation] definitions for
    ordinary [com]mands, we introduce these notations in a special
    scope called [dcom_scope], and we [Open] this scope for the
    remainder of the file.

    Careful readers will note that we've defined two notations
    for specifying a precondition explicitly, one with and one
    without a [->>].  The "without" version is intended to be
    used to supply the initial precondition at the very top
    of the program. *)
(** Here's how our decorated programs look now: *)

Example dec_while : decorated :=
  {{ fun st => True }}
  WHILE !(X = 0)
  DO
    {{ fun st => True /\ st X <> 0}}
    X ::= X - 1
    {{ fun _ => True }}
  END
  {{ fun st => True /\ st X = 0}} ->>
  {{ fun st => st 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 _           => SKIP
  | DCSeq d1 d2        => (extract d1 ;; extract d2)
  | DCAsgn X a _       => X ::= a
  | DCIf b _ d1 _ d2 _ => IFB b THEN extract d1 ELSE extract d2 FI
  | DCWhile b _ d _    => WHILE b DO extract d END
  | DCPre _ d          => extract d
  | DCPost d _         => extract d
  end.

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


(** The choice of exactly where to put assertions in the definition of
    [dcom] is a bit subtle.  The simplest thing to do would be to
    annotate every [dcom] with a precondition and postcondition.  But
    this would result in very verbose programs with a lot of repeated
    annotations: for example, a program like [SKIP;SKIP] would have to
    be annotated as

        {{P}} ({{P}} SKIP {{P}}) ;; ({{P}} SKIP {{P}}) {{P}},

    with pre- and post-conditions on each [SKIP], plus identical pre-
    and post-conditions on the semicolon!

    Instead, the rule we've followed is this:

       - The _post_-condition expected by each [dcom] [d] is embedded
         in [d].

       - The _pre_-condition is supplied by the context. *)

(** In other words, the invariant of the representation is that a
    [dcom] [d] together with a precondition [P] determines a Hoare
    triple [{{P}} (extract d) {{post d}}], where [post] is defined as
    follows: *)

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.

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

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.

(** We can express what it means for a decorated program to be
    correct as follows: *)

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

(** 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_. *)

(* ================================================================= *)
(** ** 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. *)

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 =>
      ((fun st => P st /\ bassn b st) ->> P1)
      /\ ((fun st => P st /\ ~ (bassn b st)) ->> P2)
      /\ (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)
      /\ ((fun st => post d st /\ bassn b st) ->> Pbody)
      /\ ((fun st => post d st /\ ~(bassn b st)) ->> Ppost)
      /\ 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 P H; simpl in *.
  - (* Skip *)
    eapply hoare_consequence_pre.
      apply hoare_skip.
      assumption.
  - (* Seq *)
    inversion H as [H1 H2]. clear H.
    eapply hoare_seq.
      apply IHd2. apply H2.
      apply IHd1. apply H1.
  - (* Asgn *)
    eapply hoare_consequence_pre.
      apply hoare_asgn.
      assumption.
  - (* If *)
    inversion H as [HPre1 [HPre2 [Hd1 [Hd2 [HThen HElse]]]]].
    clear H.
    apply IHd1 in HThen. clear IHd1.
    apply IHd2 in HElse. clear IHd2.
    apply hoare_if.
      + eapply hoare_consequence_post with (Q':=post d1); eauto.
         eapply hoare_consequence_pre; eauto.
      + eapply hoare_consequence_post with (Q':=post d2); eauto.
         eapply hoare_consequence_pre; eauto.
  - (* While *)
    inversion H as [Hpre [Hbody1 [Hpost1  Hd]]]. clear H.
    eapply hoare_consequence_pre; eauto.
    eapply hoare_consequence_post; eauto.
    apply hoare_while.
    eapply hoare_consequence_pre; eauto.
  - (* Pre *)
    inversion H as [HP Hd]; clear H.
    eapply hoare_consequence_pre. apply IHd. apply Hd. assumption.
  - (* Post *)
    inversion H as [Hd HQ]; clear H.
    eapply hoare_consequence_post. apply IHd. apply Hd. assumption.
Qed.

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

(** 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.

Lemma 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. *)

Eval simpl in (verification_conditions_dec dec_while).
(**

    ==>
    (((fun _ : state => True) ->> (fun _ : state => True)) /\
     ((fun st : state => True /\ bassn (! (X = 0)) st) ->>
      (fun st : state => True /\ st X <> 0)) /\
     ((fun st : state => True /\ ~ bassn (! (X = 0)) st) ->>
      (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)   
*)

(** In principle, we could work with such propositions using just the
    tactics we have so far, but we can make things much smoother with
    a bit of automation.  We first define a custom [verify] tactic
    that uses [split] repeatedly to turn all the conjunctions into
    separate subgoals and then uses [omega] and [eauto] (described in
    chapter [Auto] in _Logical Foundations_) to deal with as many
    of them as possible. *)

Tactic Notation "verify" :=
  apply verification_correct;
  repeat split;
  simpl; unfold assert_implies;
  unfold bassn in *; unfold beval in *; unfold aeval in *;
  unfold assn_sub; intros;
  repeat rewrite t_update_eq;
  repeat (rewrite t_update_neq; [| (intro X; inversion X)]);
  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;
  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 omega.

(** What's left after [verify] does its thing is "just the interesting
    parts" of checking that the decorations are correct. For very
    simple examples [verify] immediately solves the goal (provided
    that the annotations are correct!). *)

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

(** Another example (formalizing a decorated program we've seen
    before): *)

Example subtract_slowly_dec (m:nat) (p:nat) : decorated :=
    {{ fun st => st X = m /\ st Z = p }} ->>
    {{ fun st => st Z - st X = p - m }}
  WHILE ! (X = 0)
  DO   {{ fun st => st Z - st X = p - m /\ st X <> 0 }} ->>
       {{ fun st => (st Z - 1) - (st X - 1) = p - m }}
     Z ::= Z - 1
       {{ fun st => st Z - (st X - 1) = p - m }} ;;
     X ::= X - 1
       {{ fun st => st Z - st X = p - m }}
  END
    {{ fun st => st Z - st X = p - m /\ st X = 0 }} ->>
    {{ fun st => st Z = p - m }}.

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

(* ================================================================= *)
(** ** Examples *)

(** In this section, we use the automation developed above to verify
    formal decorated programs corresponding to most of the informal
    ones we have seen. *)

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

Definition swap : com :=
  X ::= X + Y;;
  Y ::= X - Y;;
  X ::= X - Y.

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

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

(* ----------------------------------------------------------------- *)
(** *** Simple Conditionals *)

Definition if_minus_plus_com :=
  IFB X <= Y
    THEN Z ::= Y - X
    ELSE Y ::= X + Z
  FI.

Definition if_minus_plus_dec :=
  {{fun st => True}}
  IFB X <= Y  THEN
      {{ fun st => True /\ st X <= st Y }} ->>
      {{ fun st => st Y = st X + (st Y - st X) }}
    Z ::= Y - X
      {{ fun st => st Y = st X + st Z }}
  ELSE
      {{ fun st => True /\ ~(st X <= st Y) }} ->>
      {{ fun st => st X + st Z = st X + st Z }}
    Y ::= X + Z
      {{ fun st => st Y = st X + st Z }}
  FI
  {{fun st => st Y = st X + st Z}}.

Theorem if_minus_plus_correct :
  dec_correct if_minus_plus_dec.
Proof. verify. Qed.

Definition if_minus_dec :=
  {{fun st => True}}
  IFB X <= Y THEN
      {{fun st => True /\ st X <= st Y }} ->>
      {{fun st => (st Y - st X) + st X = st Y
               \/ (st Y - st X) + st Y = st X}}
    Z ::= Y - X
      {{fun st => st Z + st X = st Y \/ st Z + st Y = st X}}
  ELSE
      {{fun st => True /\ ~(st X <= st Y) }} ->>
      {{fun st => (st X - st Y) + st X = st Y
               \/ (st X - st Y) + st Y = st X}}
    Z ::= X - Y
      {{fun st => st Z + st X = st Y \/ st Z + st Y = st X}}
  FI
    {{fun st => st Z + st X = st Y \/ st Z + st Y = st X}}.

Theorem if_minus_correct :
  dec_correct if_minus_dec.
Proof. verify. Qed.

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