Commit 410635e3 authored by charguer's avatar charguer

tutorial cfml cleanup

parent 4c566616
......@@ -34,7 +34,8 @@ CFML tactics:
- [xcf]
- [xsimpl], or [xsimpl X1 .. X2] (to instantiate Hexists)
- [xpull]
- [xret], or [xapps] for substitution/simplification
- [xclean] sometimes needed to do simplifications
- [xret], or [xrets] for substitution/simplification
- [xapp], or [xapps] for substitution
- [xfor_inv (fun i => H)]
- [xwhile_inv_basic (fun b k => [b = isTrue(..)] \* H) (downto n)]
......@@ -113,59 +114,69 @@ Hint Rewrite math_plus_one_twice math_minus_same
(** Basic operations *)
(*---------------------------------------------------------------------*)
(*----
let example_let n =
let a = n+1 in
let b = n-1 in
a + b
----*)
(**
[[
let example_let n =
let a = n+1 in
let b = n-1 in
a + b
]]
*)
Lemma example_let_spec : forall n,
app example_let [n]
PRE \[]
POST (fun (v:int) => \[v = 2*n]). (* POST \[= (2 * n)] *)
POST (fun (v:int) => \[v = 2*n]).
(* post-condition also written: POST \[= (2 * n)] *)
Proof using.
dup 2.
{ xcf.
(* Hint: the proof uses [xcf], [xret], [xsimpl], [math].
[xlet] is optional; if used then [xpull] is also needed. *)
dup 3.
{ (* detailed proof *)
xcf.
xlet. xret. simpl. xpull. intros Ha.
xlet. xret. simpl. xpull. intros Hb.
xret. (*hnf.*) xsimpl. math. }
{ xcf. xret ;=> Ha. xret. intros Hb. xret. xsimpl. math. }
(* use: [xcf], [xret], [xsimpl], [math];
[xlet] is optional; if used then [xpull] is also needed. *)
{ (* shorter proof *)
xcf. xret ;=> Ha. xret ;=> Hb. xret. xsimpl. math. }
{ (* real proof *)
xcf. xrets. xrets. xrets. math. }
Qed.
(*---------------------------------------------------------------------*)
(*----
let example_incr r =
r := !r + 1
let example_incr r =
let x0__ := get r in
set r (x0__ + 1)
----*)
(**
[[
let example_incr r =
r := !r + 1
]]
normalized to:
[[
let example_incr r =
let x0__ := get r in
set r (x0__ + 1)
]]
*)
Lemma example_incr_spec : forall r n,
app example_incr [r]
PRE (r ~~> n)
POST (fun (_:unit) => (r ~~> (n+1))). (* POST (# r ~~> (n+1)). *)
POST (fun (_:unit) => (r ~~> (n+1))).
(* post-condition also written: POST (# r ~~> (n+1)). *)
Proof using.
(* Hint: the proof uses [xcf], [xapp].
[xapps] is a shortand for [xapp] followed with [subst]. *)
dup 3.
{ xcf. xlet. xapp. simpl. xpull. intros. subst. xapp. }
{ xcf. xapp. intros. subst. xapp. }
{ xcf. xapps. xapp. }
(* use: [xcf], [xapp];
[xapps] is a shortand for [xapp] followed with [subst] *)
Qed.
(*
Let x0__ := app get [r] in
app set [r (x0__ + 1)]
*)
(* Remark: here are the specifications of get and set from Pervasives_proof.
(* Note: recall the specifications of get and set from Pervasives_proof:
Lemma get_spec : forall A (v:A) r,
app get [r]
......@@ -178,7 +189,9 @@ Qed.
*)
(*---------------------------------------------------------------------*)
(*----
(**
[[
let example_two_ref n =
let i = ref 0 in
let r = ref n in
......@@ -186,70 +199,60 @@ let example_two_ref n =
incr i;
r := !i + !r;
!i + !r
----*)
]]
*)
Lemma example_two_ref_spec : forall n: int,
(* <EXO> *)
app example_two_ref [n]
PRE \[]
POST (fun x: int => \[ x = n+1 ]).
(* </EXO *)
Proof using.
(*
(* Hint: the proof uses [xcf], [xapp], [xapps], and [xret] or [xrets]. *)
dup 3.
{xcf. xlet. xapp. simpl. xpull. intros.
xapp.
xapp.
xapp.
xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math.
}
{xcf. xgo. subst. math. }
*)
xcf. xapp. xapp. xapp. xapp. xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math.
Qed.
(*
app example_two_ref [n]
PRE \[]
POST (fun (v:int) => \[v = n+1]).
(* </EXO> *)
Proof using.
(* <EXO> *)
dup.
{ xcf.
xapps.
xapps.
xapps.
xapps.
xapps.
xapps.
xapps.
xapps.
xapps.
xret.
xsimpl.
{ (* detailed proof *)
xcf.
xapp. (* details: xlet. xapp. simpl. *)
xapp. xapp. xapp.
xapps. (* details: xapp. intro. subst. *)
xapps. xapps. xapps. xapps.
xrets. (* details: xret. xsimpl. *)
math. }
{ xcf. xgo~. }
(* </EXO> *)
{ (* shorter proof, not recommended for nontrivial code *)
xcf. xgo. subst. math. }
{ (* real proof *)
xcf. xgo~. }
Qed.
*)
(***********************************************************************)
(** For loops *)
(*---------------------------------------------------------------------*)
(*----
let facto_for n =
let r = ref 1 in
for i = 1 to n do
r := !r * i;
done;
!r
----*)
(**
[[
let facto_for n =
let r = ref 1 in
for i = 1 to n do
r := !r * i;
done;
!r
]]
*)
(* Reasoning principle for the loop [for i = a to b to t done] when [b+1>=a]
implemented by tactic [xfor_inv I].
I a initial invariant
I i -> I (i+1) when executing [t] on some [i] in the range from [a] to [b]
I (b+1) final invariant
*)
Lemma facto_for_spec : forall n,
n >= 1 ->
......@@ -262,79 +265,46 @@ Proof using.
{ math. }
{ xsimpl. forwards: facto_zero. easy. }
{ =>> Hi. xapps. xapps. xsimpl.
rew_maths. rewrite (@facto_succ i). ring. math. }
xapps. xsimpl. rew_maths. auto.
rew_maths. rewrite (@facto_succ i). ring. math. }
xapps. xsimpl. rew_maths. auto.
Qed.
(* Remark: reasoning principle for the loop [for i = a to b to t done] when [b+1>=a]
I a initial invariant
I i -> I (i+1) when executing [t] on some [i] in the range from [a] to [b]
I (b+1) final invariant
(*---------------------------------------------------------------------*)
(**
[[
let fib_for n =
let a = ref 0 in
let b = ref 1 in
for i = 0 to n-1 do
let c = !a + !b in
a := !b;
b := c;
done;
!a
]]
*)
(*---------------------------------------------------------------------*)
(*----
let fib_for n =
let a = ref 0 in
let b = ref 1 in
for i = 0 to n-1 do
let c = !a + !b in
a := !b;
b := c;
done;
!a
----*)
Lemma fib_for_spec : forall n,
n >= 1 ->
app fib_for [n]
PRE \[]
POST (fun (v:int) => \[v = fib n]).
Proof using.
(* Hint: follow the pattern from the previous example *)
(* <EXO> *)
=>> Hn. xcf. xapps. xapps.
xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1)) ).
{ math. }
{ xsimpl. rewrite fib_base. math. math. rewrite~ fib_base. (*math. math.*) }
{ xsimpl.
rewrite~ fib_base. (* details: math. math. rewrite fib_base. *)
rewrite~ fib_base. }
{ =>> Hi. xapps. xapps. xrets. xapps. xapps. xapps. xsimpl.
rew_maths. rewrite~ (@fib_succ (i+2)). rew_maths. math_rewrite ((i + 2)-1 = i+1). math. }
xapps. xsimpl~.
rew_maths. rewrite~ (@fib_succ (i+2)). rew_maths.
math_rewrite ((i + 2)-1 = i+1). math. }
xapps. xsimpl~.
(* </EXO> *)
Qed.
......@@ -358,16 +328,37 @@ Qed.
(** While loops *)
(*---------------------------------------------------------------------*)
(*----
let example_while n =
let i = ref 0 in
let r = ref 0 in
while !i < n do
incr i;
incr r;
done;
!r
----*)
(**
[[
let example_while n =
let i = ref 0 in
let r = ref 0 in
while !i < n do
incr i;
incr r;
done;
!r
]]
*)
(* Reasoning principle for the loop [while t1 do t2] using an invariant
implemented by tactic [xwhile_inv_basic J W].
J b i true for some boolean [b] and some initial index [k]
J b i when executing [t1] on some [i]
->
J b' i
J true i when executing [t2] on some [i], should restablish the
-> invariant for some [b'] and some [i'] smaller than [i]
J b' i' w.r.t. [W], that is [W i' i].
J false i for some [i] describes the final state
*)
Lemma example_while_spec : forall n,
n >= 0 ->
......@@ -389,16 +380,19 @@ Qed.
(*---------------------------------------------------------------------*)
(*----
let facto_while n =
let r = ref 1 in
let i = ref 1 in
while !i <= n do
r := !i * !r;
incr i;
done;
!r
----*)
(**
[[
let facto_while n =
let r = ref 1 in
let i = ref 1 in
while !i <= n do
r := !i * !r;
incr i;
done;
!r
]]
*)
Lemma facto_while_spec : forall n,
n >= 2 ->
......@@ -406,6 +400,7 @@ Lemma facto_while_spec : forall n,
PRE \[]
POST (fun (v:int) => \[v = facto n]).
Proof using.
(* Hint: follow the pattern from previous example *)
(* <EXO> *)
introv Hn. xcf. xapps. xapps.
xwhile_inv_basic (fun b k => \[b = isTrue (k <= n)] \* \[2 <= k <= n+1]
......@@ -424,17 +419,24 @@ Qed.
(*---------------------------------------------------------------------*)
(*----
let is_prime n =
let i = ref 2 in
let p = ref true in
while !p && (!i * !i <= n) do
if (n mod !i) = 0
then p := false;
incr i;
done;
!p
----*)
(* TODO: add demos using the other xfor and xwhile approach *)
(*---------------------------------------------------------------------*)
(**
[[
let is_prime n =
let i = ref 2 in
let p = ref true in
while !p && (!i * !i <= n) do
if (n mod !i) = 0
then p := false;
incr i;
done;
!p
]]
*)
Require Import Psatz.
Tactic Notation "math_nia" := math_setup; nia.
......@@ -458,11 +460,13 @@ Proof using.
{ xapps. xapps. xrets*. }
{ xsimpl*. } }
{ => k. xpull ;=> vp Hb Hp Hk.
(* TODO: xclean. *) xclean. destruct Hb as (Hvp&Hkk).
xclean. (* cleans up results of boolean tests *)
destruct Hb as (Hvp&Hkk).
xapps. xapps. math.
xrets. xseq. xif (# Hexists (vp':bool), i ~~> k \* p ~~> vp' \*
xrets.
xseq. (* TODO: later try to change xif to remove xseq *)
xif (# Hexists (vp':bool), i ~~> k \* p ~~> vp' \*
\[if vp' then (forall d, 1 < d < (k+1) -> Z.rem n d <> 0) else (~ prime n)]).
(* TODO: remove xseq *)
{ xapps. xsimpl. applys~ divide_not_prime. math_nia. }
{ xrets. rewrite Hvp in *. =>> Hd. tests: (d = k). auto. applys~ Hp. }
xpull ;=> vp' Hvp'. xapps. xsimpl.
......@@ -481,12 +485,15 @@ Qed.
(** Recursion *)
(*---------------------------------------------------------------------*)
(*----
let rec facto_rec n =
if n <= 1
then 1
else n * facto_rec(n-1)
----*)
(**
[[
let rec facto_rec n =
if n <= 1
then 1
else n * facto_rec(n-1)
]]
*)
Lemma facto_rec_spec : forall n,
n >= 1 ->
......@@ -497,18 +504,21 @@ Proof using.
=> n. induction_wf IH: (downto 0) n. unfolds downto. => Hn.
xcf. xif.
{ xrets. math_rewrite (n=1). rewrite~ facto_one. }
{ xapps. math. math. (* could be written [xapps~] *)
{ xapps. math. math. (* optimization: could be written [xapps~] *)
xrets. rewrite~ (@facto_succ n). }
Qed.
(*---------------------------------------------------------------------*)
(*----
let rec fib_rec n =
if n <= 1
then 1
else fib_rec(n-1) + fib_rec(n-2)
----*)
(**
[[
let rec fib_rec n =
if n <= 1
then 1
else fib_rec(n-1) + fib_rec(n-2)
]]
*)
Lemma fib_rec_spec : forall n,
n >= 0 ->
......@@ -516,6 +526,7 @@ Lemma fib_rec_spec : forall n,
PRE \[]
POST (fun (v:int) => \[v = fib n]).
Proof using.
(* Hint: follow the pattern for the previous example *)
(* <EXO> *)
=> n. induction_wf IH: (downto 0) n. => Hn.
xcf. xif.
......@@ -530,42 +541,46 @@ Qed.
(** Stack *)
(*---------------------------------------------------------------------*)
(*----
module StackList = struct
type 'a t = {
mutable items : 'a list;
mutable size : int }
(*
[[
module StackList = struct
type 'a t = {
mutable items : 'a list;
mutable size : int }
let create () =
{ items = [];
size = 0 }
let create () =
{ items = [];
size = 0 }
let size s =
s.size
let size s =
s.size
let is_empty s =
s.size = 0
let is_empty s =
s.size = 0
let push x s =
s.items <- x :: s.items;
s.size <- s.size + 1
let push x s =
s.items <- x :: s.items;
s.size <- s.size + 1
let pop s =
match s.items with
| hd::tl ->
s.items <- tl;
s.size <- s.size - 1;
hd
| [] -> assert false
let pop s =
match s.items with
| hd::tl ->
s.items <- tl;
s.size <- s.size - 1;
hd
| [] -> assert false
end
----*)
end
]]
*)
Module StackListProof.
Import StackList_ml.
(** Definition of [r ~> Stack L], which is a notation for [Stack L r] of type [hprop] *)
Definition Stack A (L:list A) r :=
......@@ -573,59 +588,69 @@ Definition Stack A (L:list A) r :=
r ~> `{ items' := L; size' := n }
\* \[ n = length L ].
(** Unfolding and folding lemmas paraphrasing the definition of [Stack] *)
Lemma Stack_open : forall r A (L:list A),
r ~> Stack L ==>
Hexists n, r ~> `{ items' := L; size' := n } \* \[ n = length L ].
Proof using. intros. xunfolds~ Stack. Qed.
(**--- begin customization of [xopen] and [xclose] for [Stack] ---*)
Lemma Stack_close : forall r A (L:list A) (n:int),
n = length L ->
r ~> `{ items' := L; size' := n } ==>
r ~> Stack L.
Proof using. intros. xunfolds~ Stack. Qed.
Lemma Stack_open : forall r A (L:list A),
r ~> Stack L ==>
Hexists n, r ~> `{ items' := L; size' := n } \* \[ n = length L ].
Proof using. intros. xunfolds~ Stack. Qed.
Arguments Stack_close : clear implicits.
Lemma Stack_close : forall r A (L:list A) (n:int),
n = length L ->
r ~> `{ items' := L; size' := n } ==>
r ~> Stack L.
Proof using. intros. xunfolds~ Stack. Qed.
Arguments Stack_close : clear implicits.
(** Customization of [xopen] and [xclose] tactics for [Stack].
These tactics avoid the need to call [hchange] or [xchange]
by providing explicitly the lemmas [Stack_open] and [Stack_close]. *)
Hint Extern 1 (RegisterOpen (Stack _)) =>
Provide Stack_open.
Hint Extern 1 (RegisterClose (record_repr _)) =>
Provide Stack_close.
Hint Extern 1 (RegisterOpen (Stack _)) =>
Provide Stack_open.
Hint Extern 1 (RegisterClose (record_repr _)) =>
Provide Stack_close.
(*--- end ---*)
(** Verification of the code *)
Lemma create_spec : forall (A:Type),
app create [tt]
PRE \[]
POST (fun r => r ~> Stack (@nil A)).
Proof using.
xcf. xapps. => r. xclose r. auto. xsimpl.
xcf.
xapp ;=> r. (* ddetails: xapp. intros r. *)
xclose r. (* details: xchange (@Stack_close r). *)
auto. xsimpl.
Qed.
Lemma size_spec : forall (A:Type) (L:list A) (s:loc),
app size [s]
INV (s ~> Stack L)
POST (fun n => \[n = length L]).
(* Remark: the above is a notation for:
app size [s]
PRE (s ~> Stack L)
POST (fun n => \[n = length L] \* s ~> Stack L).
*)
Proof using.
xcf.
xopen s. xpull ;=> n Hn. xapp. => m. xpull ;=> E.
xclose s. auto. xsimpl. math.
Unshelve. solve_type. (* todo: xcf A *)
xopen s. (* details: xchange (@Stack_open s). *)
xpull ;=> n Hn. xapp. => m. xpull ;=> E.
xclose s. (* details: xchange (@Stack_close s). *)
auto. xsimpl. math.
(* Here we have an issue because Coq is a bit limited.
Workaround to discharge the remaining type: *)
Unshelve. solve_type. (* TODO: support [xcf A] in the beginning *)
Qed.
Lemma length_zero_iff_nil : forall A (L:list A),
length L = 0 <-> L = nil.
Proof using.
=>. subst. destruct L; rew_list. autos*. iff M; false; math.
=>. subst. destruct L; rew_list. (* [rew_list] normalizes list expressions *)
autos*. iff M; false; math.
Qed.
Lemma is_empty_spec : forall (A:Type) (L:list A) (s:loc),
......@@ -635,11 +660,14 @@ Lemma is_empty_spec : forall (A:Type) (L:list A) (s:loc),
POST (fun b => \[b = isTrue (L = nil)]).
(* </EXO> *)
Proof using.
(* Hint: use [xopen] then [xclose] like in [size_spec].
Also use [xcf], [xpull], [xapps], [xrets],
and lemma [length_zero_iff_nil] from above. *)
(* <EXO> *)
xcf. xopen s. xpull ;=> n Hn. xapps. xclose~ s. xrets.
subst. apply length_zero_iff_nil.
(* </EXO> *)
Unshelve. solve_type. (* todo: xcf A *)
Unshelve. solve_type.
Qed.
Lemma push_spec : forall (A:Type) (L:list A) (s:loc) (x:A),
......@@ -647,12 +675,14 @@ Lemma push_spec : forall (A:Type) (L:list A) (s:loc) (x:A),
PRE (s ~> Stack L)
POST (# s ~> Stack (x::L)).
Proof using.