Finished proof from class

[Jay McCarthy]

Definition fact_inv (x : nat) : Assertion :=
fun st =>
(st Y) * (real_fact (st Z)) = real_fact x.

Example fact_dec (x:nat) : dcom := (
{{ fun st => st X = x }} =>
{{ fun st => (assn_sub Z (AId X) (assn_sub Y (ANum 1) (fact_inv x))) st }}
Z ::= (AId X)
{{ fun st => (assn_sub Y (ANum 1) (fact_inv x)) st }};
Y ::= ANum 1
{{ fun st => fact_inv x st }};
WHILE BNot (BEq (AId Z) (ANum 0)) DO
{{ fun st => fact_inv x st /\ negb (beq_nat (st Z) 0) = true}} =>
{{ fun st => (assn_sub Y (AMult (AId Y) (AId Z))
(assn_sub Z (AMinus (AId Z) (ANum 1)) (fact_inv x))) st }}
Y ::= AMult (AId Y) (AId Z)
{{ fun st => (assn_sub Z (AMinus (AId Z) (ANum 1)) (fact_inv x)) st }};
Z ::= AMinus (AId Z) (ANum 1)
{{ fun st => fact_inv x st }}
END
{{ fun st => fact_inv x st /\ negb (beq_nat (st Z) 0) <> true }} =>
{{ fun st => st Y = real_fact x }}
)%dcom.

Theorem fact_dec_correct : forall x,
dec_correct (fact_dec x).
Proof.
intros x. verify.

unfold fact_inv. rewrite update_eq. rewrite update_neq. rewrite update_eq.
rewrite H. omega. reflexivity.

unfold fact_inv in *. rewrite <- H.
rewrite update_eq. rewrite update_neq; [|reflexivity].
rewrite update_eq. rewrite update_neq; [|reflexivity].
destruct (st Z) as [|z].
omega.
replace (S z - 1) with z; [|omega].
replace (real_fact (S z)) with (S z * real_fact z).
rewrite mult_assoc. reflexivity.
reflexivity.

unfold fact_inv in *. rewrite <- H.
rewrite H0. simpl. omega.
Qed.

Notice that all the busy nose-following was done for us.

--
Jay McCarthy <j...@cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93