Hoare2: Hoare Logic, Part II
Set Warnings "notationoverridden,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 omega.Omega.
From PLF Require Import Hoare.
From PLF Require Import Imp.
Decorated Programs
 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):
 An assignment is locally consistent if its precondition is the
appropriate substitution of its postcondition:
 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):
 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:
 A pair of assertions separated by >> is locally consistent if
the first implies the second:
Example: Swapping Using Addition and Subtraction
 We begin with the undecorated program (the unnumbered lines).
 We add the specification  i.e., the outer precondition (1) and postcondition (5). In the precondition, we use parameters m and n to remember the initial values of variables X and Y so that we can refer to them in the postcondition (5).
 We work backwards, mechanically, starting from (5) and proceeding until we get to (2). At each step, we obtain the precondition of the assignment from its postcondition by substituting the assigned variable with the righthandside of the assignment. For instance, we obtain (4) by substituting X with X  Y in (5), and we obtain (3) by substituting Y with X  Y in (4).
 Finally, we verify that (1) logically implies (2)  i.e.,
that the step from (1) to (2) is a valid use of the law of
consequence. For this we substitute X by m and Y by n
and calculate as follows:
Example: Simple Conditionals
 We start with the outer precondition (1) and postcondition (8).
 We follow the format dictated by the hoare_if rule and copy the postcondition (8) to (4) and (7). We conjoin the precondition (1) with the guard of the conditional to obtain (2). We conjoin (1) with the negated guard of the conditional to obtain (5).
 In order to use the assignment rule and obtain (3), we substitute Z by Y  X in (4). To obtain (6) we substitute Z by X  Y in (7).
 Finally, we verify that (2) implies (3) and (5) implies (6). Both of these implications crucially depend on the ordering of X and Y obtained from the guard. For instance, knowing that X <= Y ensures that subtracting X from Y and then adding back X produces Y, as required by the first disjunct of (3). Similarly, knowing that ~ (X <= Y) ensures that subtracting Y from X and then adding back Y produces X, as needed by the second disjunct of (6). Note that n  m + m = n does not hold for arbitrary natural numbers n and m (for example, 3  5 + 5 = 5).
Exercise: 2 stars, standard (if_minus_plus_reloaded)
☐
Example: Reduce to Zero
 Start with the outer precondition (1) and postcondition (6).
 Following the format dictated by the hoare_while rule, we copy (1) to (4). We conjoin (1) with the guard to obtain (2) and with the negation of the guard to obtain (5). Note that, because the outer postcondition (6) does not syntactically match (5), we need a trivial use of the consequence rule from (5) to (6).
 Assertion (3) is the same as (4), because X does not appear in 4, so the substitution in the assignment rule is trivial.
 Finally, the implication between (2) and (3) is also trivial.
Definition reduce_to_zero' : com :=
(WHILE ~(X = 0) DO
X ::= X  1
END)%imp.
Theorem reduce_to_zero_correct' :
{{fun st => True}}
reduce_to_zero'
{{fun st => st X = 0}}.
Proof.
unfold reduce_to_zero'.
eapply hoare_consequence_post.
apply hoare_while.

eapply hoare_consequence_pre. apply hoare_asgn.
intros st [HT Hbp]. unfold assn_sub. constructor.

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.
Example: Division
Finding Loop Invariants
Example: Slow Subtraction
 (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).
Exercise: Slow Assignment
Exercise: 2 stars, standard (slow_assignment)
☐
Exercise: Slow Addition
Exercise: 3 stars, standard, optional (add_slowly_decoration)
Example: Parity
The postcondition does not hold at the beginning of the loop,
since m = parity m does not hold for an arbitrary m, so we
cannot use that as an invariant. To find an invariant that works,
let's think a bit about what this loop does. On each iteration it
decrements X by 2, which preserves the parity of X. So the
parity of X does not change, i.e., it is invariant. The initial
value of X is m, so the parity of X is always equal to the
parity of m. Using parity X = parity m as an invariant we
obtain the following decorated program:
X = m >> (a  OK)
parity X = parity m
WHILE 2 <= X DO
parity X = parity m /\ 2 <= X >> (c  OK)
parity (X2) = parity m
X ::= X  2
parity X = parity m
END
parity X = parity m /\ X < 2 >> (b  OK)
X = parity m
With this invariant, conditions (a), (b), and (c) are all
satisfied. For verifying (b), we observe that, when X < 2, we
have parity X = X (we can easily see this in the definition of
parity). For verifying (c), we observe that, when 2 <= X, we
have parity X = parity (X2).
Translate this proof to Coq. Refer to the reduce_to_zero example
for ideas. You may find the following two lemmas useful:
Exercise: 3 stars, standard, optional (parity_formal)
Lemma parity_ge_2 : forall x,
2 <= x >
parity (x  2) = parity x.
Proof.
induction x; intro. reflexivity.
destruct x. inversion H. inversion H1.
simpl. rewrite < minus_n_O. reflexivity.
Qed.
Lemma parity_lt_2 : forall x,
~ 2 <= x >
parity (x) = x.
Proof.
intros. induction x. reflexivity. destruct x. reflexivity.
exfalso. apply H. omega.
Qed.
Theorem parity_correct : forall m,
{{ fun st => st X = m }}
WHILE 2 <= X DO
X ::= X  2
END
{{ fun st => st X = parity m }}.
Proof.
Admitted.
☐
Example: Finding Square Roots
Example: Squaring
Exercise: Factorial
Exercise: 3 stars, standard (factorial)
☐
Exercise: Min
Exercise: 3 stars, standard (Min_Hoare)
☐
Here is a very inefficient way of adding 3 numbers:
X ::= 0;;
Y ::= 0;;
Z ::= c;;
WHILE ~(X = a) DO
X ::= X + 1;;
Z ::= Z + 1
END;;
WHILE ~(Y = b) DO
Y ::= Y + 1;;
Z ::= Z + 1
END
Show that it does what it should by filling in the blanks in the
following decorated program.
True >>
X ::= 0;;
Y ::= 0;;
Z ::= c;;
WHILE ~(X = a) DO
>>
X ::= X + 1;;
Z ::= Z + 1
END;;
>>
WHILE ~(Y = b) DO
>>
Y ::= Y + 1;;
Z ::= Z + 1
END
>>
Z = a + b + c
Exercise: 3 stars, standard (two_loops)
☐
Exercise: Power Series
Exercise: 4 stars, standard, optional (dpow2_down)
Weakest Preconditions (Optional)
That is, P is the weakest precondition of c for Q
if (a) P is a precondition for Q and c, and (b) P is the
weakest (easiest to satisfy) assertion that guarantees that
Q will hold after executing c.
What are the weakest preconditions of the following commands
for the following postconditions?
1) ? SKIP X = 5
2) ? X ::= Y + Z X = 5
3) ? X ::= Y X = Y
4) ?
TEST X = 0 THEN Y ::= Z + 1 ELSE Y ::= W + 2 FI
Y = 5
5) ?
X ::= 5
X = 0
6) ?
WHILE true DO X ::= 0 END
X = 0
Exercise: 1 star, standard, optional (wp)
Exercise: 3 stars, advanced, optional (is_wp_formal)
Theorem is_wp_example :
is_wp (fun st => st Y <= 4)
(X ::= Y + 1) (fun st => st X <= 5).
Proof.
Admitted.
☐
Show that the precondition in the rule hoare_asgn is in fact the
weakest precondition.
Exercise: 2 stars, advanced, optional (hoare_asgn_weakest)
☐
Show that your havoc_pre rule from the himp_hoare exercise
in the Hoare chapter returns the weakest precondition.
Exercise: 2 stars, advanced, optional (hoare_havoc_weakest)
Module Himp2.
Import Himp.
Lemma hoare_havoc_weakest : forall (P Q : Assertion) (X : string),
{{ P }} HAVOC X {{ Q }} >
P >> havoc_pre X Q.
Proof.
Admitted.
End Himp2.
Import Himp.
Lemma hoare_havoc_weakest : forall (P Q : Assertion) (X : string),
{{ P }} HAVOC X {{ Q }} >
P >> havoc_pre X Q.
Proof.
Admitted.
End Himp2.
☐
Formal Decorated Programs (Advanced)
Syntax
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.
Delimit Scope default with default.
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 "'TEST' 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.
Example dec0 :=
SKIP {{ fun st => True }}.
Example dec1 :=
WHILE true DO {{ fun st => True }} SKIP {{ fun st => True }} END
{{ fun st => True }}.
Set Printing All.
To avoid clashing with the existing Notation definitions for
ordinary commands, 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.
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 }}.
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 _ => TEST 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 postconditions on each SKIP, plus identical pre
and postconditions on the semicolon!
Instead, the rule we've followed is this:
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:
 The postcondition expected by each dcom d is embedded
in d.
 The precondition is supplied by the context.
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:
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 add up to a complete
proof of correctness.
Extracting Verification Conditions
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 =>
(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 *.

eapply hoare_consequence_pre.
apply hoare_skip.
assumption.

destruct H as [H1 H2].
eapply hoare_seq.
apply IHd2. apply H2.
apply IHd1. apply H1.

eapply hoare_consequence_pre.
apply hoare_asgn.
assumption.

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_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.

destruct H as [Hpre [Hbody1 [Hpost1 Hd]]].
eapply hoare_consequence_pre; eauto.
eapply hoare_consequence_post; eauto.
apply hoare_while.
eapply hoare_consequence_pre; eauto.

destruct H as [HP Hd].
eapply hoare_consequence_pre. apply IHd. apply Hd. assumption.

destruct H as [Hd HQ].
eapply hoare_consequence_post. apply IHd. apply Hd. assumption.
Qed.
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.
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 sometimes even immediately solves the
goal (provided that the annotations are correct!).
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. Qed.
Examples
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.
Definition if_minus_plus_com :=
(TEST X <= Y
THEN Z ::= Y  X
ELSE Y ::= X + Z
FI)%imp.
Definition if_minus_plus_dec :=
{{fun st => True}}
TEST 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}}
TEST 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.
Definition div_mod_dec (a b : nat) : decorated :=
{{ fun st => True }} >>
{{ fun st => b * 0 + a = a }}
X ::= a
{{ fun st => b * 0 + st X = a }};;
Y ::= 0
{{ fun st => b * st Y + st X = a }};;
WHILE b <= X DO
{{ fun st => b * st Y + st X = a /\ b <= st X }} >>
{{ fun st => b * (st Y + 1) + (st X  b) = a }}
X ::= X  b
{{ fun st => b * (st Y + 1) + st X = a }};;
Y ::= Y + 1
{{ fun st => b * st Y + st X = a }}
END
{{ fun st => b * st Y + st X = a /\ ~(b <= st X) }} >>
{{ fun st => b * st Y + st X = a /\ (st X < b) }}.
Theorem div_mod_dec_correct : forall a b,
dec_correct (div_mod_dec a b).
Proof. intros a b. verify.
rewrite mult_plus_distr_l. omega.
Qed.
There are actually several ways to phrase the loop invariant for
this program. Here is one natural one, which leads to a rather
long proof:
Inductive ev : nat > Prop :=
 ev_0 : ev O
 ev_SS : forall n : nat, ev n > ev (S (S n)).
Definition find_parity_dec m : decorated :=
{{ fun st => st X = m}} >>
{{ fun st => st X <= m /\ ev (m  st X) }}
WHILE 2 <= X DO
{{ fun st => (st X <= m /\ ev (m  st X)) /\ 2 <= st X }} >>
{{ fun st => st X  2 <= m /\ (ev (m  (st X  2))) }}
X ::= X  2
{{ fun st => st X <= m /\ ev (m  st X) }}
END
{{ fun st => (st X <= m /\ ev (m  st X)) /\ st X < 2 }} >>
{{ fun st => st X=0 <> ev m }}.
Lemma l1 : forall m n p,
p <= n >
n <= m >
m  (n  p) = m  n + p.
Proof. intros. omega. Qed.
Lemma l2 : forall m,
ev m >
ev (m + 2).
Proof. intros. rewrite plus_comm. simpl. constructor. assumption. Qed.
Lemma l3' : forall m,
ev m >
~ev (S m).
Proof. induction m; intros H1 H2. inversion H2. apply IHm.
inversion H2; subst; assumption. assumption. Qed.
Lemma l3 : forall m,
1 <= m >
ev m >
ev (m  1) >
False.
Proof. intros. apply l2 in H1.
assert (G : m  1 + 2 = S m). clear H0 H1. omega.
rewrite G in H1. apply l3' in H0. apply H0. assumption. Qed.
Theorem find_parity_correct : forall m,
dec_correct (find_parity_dec m).
Proof.
intro m. verify;
fold (2 <=? (st X)) in *;
try rewrite leb_iff in *;
try rewrite leb_iff_conv in *; eauto; try omega.

rewrite minus_diag. constructor.

rewrite l1; try assumption.
apply l2; assumption.

rewrite < minus_n_O in H2. assumption.

destruct (st X) as [ [ n]].
+
reflexivity.
+
apply l3 in H; try assumption. inversion H.
+
clear H0 H2. omega.
Qed.
Here is a more intuitive way of writing the invariant:
Definition find_parity_dec' m : decorated :=
{{ fun st => st X = m}} >>
{{ fun st => ev (st X) <> ev m }}
WHILE 2 <= X DO
{{ fun st => (ev (st X) <> ev m) /\ 2 <= st X }} >>
{{ fun st => (ev (st X  2) <> ev m) }}
X ::= X  2
{{ fun st => (ev (st X) <> ev m) }}
END
{{ fun st => (ev (st X) <> ev m) /\ ~(2 <= st X) }} >>
{{ fun st => st X=0 <> ev m }}.
Lemma l4 : forall m,
2 <= m >
(ev (m  2) <> ev m).
Proof.
induction m; intros. split; intro; constructor.
destruct m. inversion H. inversion H1. simpl in *.
rewrite < minus_n_O in *. split; intro.
constructor. assumption.
inversion H0. assumption.
Qed.
Theorem find_parity_correct' : forall m,
dec_correct (find_parity_dec' m).
Proof.
intros m. verify;
fold (2 <=? (st X)) in *;
try rewrite leb_iff in *;
try rewrite leb_iff_conv in *; intuition; eauto; try omega.

rewrite l4 in H0; eauto.

rewrite l4; eauto.

apply H0. constructor.

destruct (st X) as [ [ n]]. +
reflexivity.
+
inversion H.
+
clear H0 H H3. omega.
Qed.
Here is the simplest invariant we've found for this program:
Definition parity_dec m : decorated :=
{{ fun st => st X = m}} >>
{{ fun st => parity (st X) = parity m }}
WHILE 2 <= X DO
{{ fun st => parity (st X) = parity m /\ 2 <= st X }} >>
{{ fun st => parity (st X  2) = parity m }}
X ::= X  2
{{ fun st => parity (st X) = parity m }}
END
{{ fun st => parity (st X) = parity m /\ ~(2 <= st X) }} >>
{{ fun st => st X = parity m }}.
Theorem parity_dec_correct : forall m,
dec_correct (parity_dec m).
Proof.
intros. verify;
fold (2 <=? (st X)) in *;
try rewrite leb_iff in *;
try rewrite leb_iff_conv in *; eauto; try omega.

rewrite < H. apply parity_ge_2. assumption.

rewrite < H. symmetry. apply parity_lt_2. assumption.
Qed.
Definition sqrt_dec m : decorated :=
{{ fun st => st X = m }} >>
{{ fun st => st X = m /\ 0*0 <= m }}
Z ::= 0
{{ fun st => st X = m /\ st Z*st Z <= m }};;
WHILE (Z+1)*(Z+1) <= X DO
{{ fun st => (st X = m /\ st Z*st Z<=m)
/\ (st Z + 1)*(st Z + 1) <= st X }} >>
{{ fun st => st X = m /\ (st Z+1)*(st Z+1)<=m }}
Z ::= Z + 1
{{ fun st => st X = m /\ st Z*st Z<=m }}
END
{{ fun st => (st X = m /\ st Z*st Z<=m)
/\ ~((st Z + 1)*(st Z + 1) <= st X) }} >>
{{ fun st => st Z*st Z<=m /\ m<(st Z+1)*(st Z+1) }}.
Theorem sqrt_correct : forall m,
dec_correct (sqrt_dec m).
Proof. intro m. verify. Qed.
Squaring
Definition square_dec (m : nat) : decorated :=
{{ fun st => st X = m }}
Y ::= X
{{ fun st => st X = m /\ st Y = m }};;
Z ::= 0
{{ fun st => st X = m /\ st Y = m /\ st Z = 0}} >>
{{ fun st => st Z + st X * st Y = m * m }};;
WHILE ~(Y = 0) DO
{{ fun st => st Z + st X * st Y = m * m /\ st Y <> 0 }} >>
{{ fun st => (st Z + st X) + st X * (st Y  1) = m * m }}
Z ::= Z + X
{{ fun st => st Z + st X * (st Y  1) = m * m }};;
Y ::= Y  1
{{ fun st => st Z + st X * st Y = m * m }}
END
{{ fun st => st Z + st X * st Y = m * m /\ st Y = 0 }} >>
{{ fun st => st Z = m * m }}.
Theorem square_dec_correct : forall m,
dec_correct (square_dec m).
Proof.
intro n. verify.

destruct (st Y) as [ y']. apply False_ind. apply H0.
reflexivity.
simpl. rewrite < minus_n_O.
assert (G : forall n m, n * S m = n + n * m). {
clear. intros. induction n. reflexivity. simpl.
rewrite IHn. omega. }
rewrite < H. rewrite G. rewrite plus_assoc. reflexivity.
Qed.
Definition square_dec' (n : nat) : decorated :=
{{ fun st => True }}
X ::= n
{{ fun st => st X = n }};;
Y ::= X
{{ fun st => st X = n /\ st Y = n }};;
Z ::= 0
{{ fun st => st X = n /\ st Y = n /\ st Z = 0 }} >>
{{ fun st => st Z = st X * (st X  st Y)
/\ st X = n /\ st Y <= st X }};;
WHILE ~(Y = 0) DO
{{ fun st => (st Z = st X * (st X  st Y)
/\ st X = n /\ st Y <= st X)
/\ st Y <> 0 }}
Z ::= Z + X
{{ fun st => st Z = st X * (st X  (st Y  1))
/\ st X = n /\ st Y <= st X }};;
Y ::= Y  1
{{ fun st => st Z = st X * (st X  st Y)
/\ st X = n /\ st Y <= st X }}
END
{{ fun st => (st Z = st X * (st X  st Y)
/\ st X = n /\ st Y <= st X)
/\ st Y = 0 }} >>
{{ fun st => st Z = n * n }}.
Theorem square_dec'_correct : forall n,
dec_correct (square_dec' n).
Proof.
intro n. verify.

rewrite minus_diag. omega.
 subst.
rewrite mult_minus_distr_l.
repeat rewrite mult_minus_distr_l. rewrite mult_1_r.
assert (G : forall n m p,
m <= n > p <= m > n  (m  p) = n  m + p).
intros. omega.
rewrite G. reflexivity. apply mult_le_compat_l. assumption.
destruct (st Y). apply False_ind. apply H0. reflexivity.
clear. rewrite mult_succ_r. rewrite plus_comm.
apply le_plus_l.

rewrite < minus_n_O. reflexivity.
Qed.
Definition square_simpler_dec (m : nat) : decorated :=
{{ fun st => st X = m }} >>
{{ fun st => 0 = 0*m /\ st X = m }}
Y ::= 0
{{ fun st => 0 = (st Y)*m /\ st X = m }};;
Z ::= 0
{{ fun st => st Z = (st Y)*m /\ st X = m }}>>
{{ fun st => st Z = (st Y)*m /\ st X = m }};;
WHILE ~(Y = X) DO
{{ fun st => (st Z = (st Y)*m /\ st X = m)
/\ st Y <> st X }} >>
{{ fun st => st Z + st X = ((st Y) + 1)*m /\ st X = m }}
Z ::= Z + X
{{ fun st => st Z = ((st Y) + 1)*m /\ st X = m }};;
Y ::= Y + 1
{{ fun st => st Z = (st Y)*m /\ st X = m }}
END
{{ fun st => (st Z = (st Y)*m /\ st X = m) /\ st Y = st X }} >>
{{ fun st => st Z = m*m }}.
Theorem square_simpler_dec_correct : forall m,
dec_correct (square_simpler_dec m).
Proof.
intro m. verify.
rewrite mult_plus_distr_r. simpl. rewrite < plus_n_O.
reflexivity.
Qed.
Definition two_loops_dec (a b c : nat) : decorated :=
{{ fun st => True }} >>
{{ fun st => c = 0 + c /\ 0 = 0 }}
X ::= 0
{{ fun st => c = st X + c /\ 0 = 0 }};;
Y ::= 0
{{ fun st => c = st X + c /\ st Y = 0 }};;
Z ::= c
{{ fun st => st Z = st X + c /\ st Y = 0 }};;
WHILE ~(X = a) DO
{{ fun st => (st Z = st X + c /\ st Y = 0) /\ st X <> a }} >>
{{ fun st => st Z + 1 = st X + 1 + c /\ st Y = 0 }}
X ::= X + 1
{{ fun st => st Z + 1 = st X + c /\ st Y = 0 }};;
Z ::= Z + 1
{{ fun st => st Z = st X + c /\ st Y = 0 }}
END
{{ fun st => (st Z = st X + c /\ st Y = 0) /\ st X = a }} >>
{{ fun st => st Z = a + st Y + c }};;
WHILE ~(Y = b) DO
{{ fun st => st Z = a + st Y + c /\ st Y <> b }} >>
{{ fun st => st Z + 1 = a + st Y + 1 + c }}
Y ::= Y + 1
{{ fun st => st Z + 1 = a + st Y + c }};;
Z ::= Z + 1
{{ fun st => st Z = a + st Y + c }}
END
{{ fun st => (st Z = a + st Y + c) /\ st Y = b }} >>
{{ fun st => st Z = a + b + c }}.
Theorem two_loops_correct : forall a b c,
dec_correct (two_loops_dec a b c).
Proof. intros a b c. verify. Qed.
Fixpoint pow2 n :=
match n with
 0 => 1
 S n' => 2 * (pow2 n')
end.
Definition dpow2_down (n : nat) :=
{{ fun st => True }} >>
{{ fun st => 1 = (pow2 (0 + 1))1 /\ 1 = pow2 0 }}
X ::= 0
{{ fun st => 1 = (pow2 (0 + 1))1 /\ 1 = pow2 (st X) }};;
Y ::= 1
{{ fun st => st Y = (pow2 (st X + 1))1 /\ 1 = pow2 (st X) }};;
Z ::= 1
{{ fun st => st Y = (pow2 (st X + 1))1 /\ st Z = pow2 (st X) }};;
WHILE ~(X = n) DO
{{ fun st => (st Y = (pow2 (st X + 1))1 /\ st Z = pow2 (st X))
/\ st X <> n }} >>
{{ fun st => st Y + 2 * st Z = (pow2 (st X + 2))1
/\ 2 * st Z = pow2 (st X + 1) }}
Z ::= 2 * Z
{{ fun st => st Y + st Z = (pow2 (st X + 2))1
/\ st Z = pow2 (st X + 1) }};;
Y ::= Y + Z
{{ fun st => st Y = (pow2 (st X + 2))1
/\ st Z = pow2 (st X + 1) }};;
X ::= X + 1
{{ fun st => st Y = (pow2 (st X + 1))1
/\ st Z = pow2 (st X) }}
END
{{ fun st => (st Y = (pow2 (st X + 1))1 /\ st Z = pow2 (st X))
/\ st X = n }} >>
{{ fun st => st Y = pow2 (n+1)  1 }}.
Lemma pow2_plus_1 : forall n,
pow2 (n+1) = pow2 n + pow2 n.
Proof. induction n; simpl. reflexivity. omega. Qed.
Lemma pow2_le_1 : forall n, pow2 n >= 1.
Proof. induction n. simpl. constructor. simpl. omega. Qed.
Theorem dpow2_down_correct : forall n,
dec_correct (dpow2_down n).
Proof.
intro m. verify.

rewrite pow2_plus_1. rewrite < H0. reflexivity.

rewrite < plus_n_O.
rewrite < pow2_plus_1. remember (st X) as n.
replace (pow2 (n + 1)  1 + pow2 (n + 1))
with (pow2 (n + 1) + pow2 (n + 1)  1) by omega.
rewrite < pow2_plus_1.
replace (n + 1 + 1) with (n + 2) by omega.
reflexivity.

rewrite < plus_n_O. rewrite < pow2_plus_1.
reflexivity.

replace (st X + 1 + 1) with (st X + 2) by omega.
reflexivity.
Qed.
Further Exercises
Exercise: 3 stars, advanced (slow_assignment_dec)
Example slow_assignment_dec (m : nat) : decorated
. Admitted.
Theorem slow_assignment_dec_correct : forall m,
dec_correct (slow_assignment_dec m).
Proof. Admitted.
Definition manual_grade_for_check_defn_of_slow_assignment_dec : option (nat*string) := None.
☐
Remember the factorial function we worked with before:
Exercise: 4 stars, advanced (factorial_dec)
Following the pattern of subtract_slowly_dec, write a decorated
program factorial_dec that implements the factorial function and
prove it correct as factorial_dec_correct.
☐
The Fibonacci function is usually written like this:
Fixpoint fib n :=
match n with
 0 => 1
 1 => 1
 _ => fib (pred n) + fib (pred (pred n))
end.
This doesn't pass Coq's termination checker, but here is a
slightly clunkier definition that does:
Exercise: 4 stars, advanced, optional (fib_eqn)
Fixpoint fib n :=
match n with
 0 => 1
 S n' => match n' with
 0 => 1
 S n'' => fib n' + fib n''
end
end.
Prove that fib satisfies the following equation:
☐
The following Imp program leaves the value of fib n in the
variable Y when it terminates:
X ::= 1;;
Y ::= 1;;
Z ::= 1;;
WHILE ~(X = n + 1) DO
T ::= Z;;
Z ::= Z + Y;;
Y ::= T;;
X ::= X + 1
END
Fill in the following definition of dfib and prove that it
satisfies this specification:
True dfib Y = fib n
Exercise: 4 stars, advanced, optional (fib)
Definition T : string := "T".
Definition dfib (n : nat) : decorated
. Admitted.
Theorem dfib_correct : forall n,
dec_correct (dfib n).
Admitted.
☐
The formal decorated programs defined in this section are intended
to look as similar as possible to the informal ones defined earlier
in the chapter. If we drop this requirement, we can eliminate
almost all annotations, just requiring final postconditions and
loop invariants to be provided explicitly. Do this  i.e., define a
new version of dcom with as few annotations as possible and adapt the
rest of the formal development leading up to the verification_correct
theorem.