diff --git a/examples/Tuto/Tuto_proof.v b/examples/Tuto/Tuto_proof.v index b2b64c3f65be00538160513fbfbb324bc85a1e84..6f762161c6889b9ba82d42710a509438f208e4fd 100644 --- a/examples/Tuto/Tuto_proof.v +++ b/examples/Tuto/Tuto_proof.v @@ -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, (* *) app example_two_ref [n] PRE \[] POST (fun x: int => \[ x = n+1 ]). + (* \[v = n+1]). - (* *) -Proof using. - (* *) - 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~. } - (* *) + { (* 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 *) (* *) =>> 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~. (* *) 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 *) (* *) 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 *) (* *) => 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)]). (* *) 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. *) (* *) xcf. xopen s. xpull ;=> n Hn. xapps. xclose~ s. xrets. subst. apply length_zero_iff_nil. (* *) -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. + (* Hint: use [xcf], [xapp], [xapps], [xpull], [xsimpl], + [xopen], [xclose] and [rew_list] *) (* *) xcf. - xopen s. (* Same as [xchange (@Stack_open s)] *) + xopen s. (* details: xchange (@Stack_open s) *) xpull ;=> n Hn. xapps. xapps. xapps. xapp. - xclose s. (* Same as [xchange (@Stack_close s)] *) + xclose s. (* details: xchange (@Stack_close s) *) rew_list. math. xsimpl. (* *) @@ -664,6 +694,7 @@ Lemma pop_spec : forall (A:Type) (L:list A) (s:loc), PRE (s ~> Stack L) POST (fun x => Hexists L', \[L = x::L'] \* s ~> Stack L'). Proof using. + (* Hint: also use [rew_list in H] *) (* *) =>> HL. xcf. xopen s. xpull ;=> n Hn. xapps. xmatch. xapps. xapps. xapps. xret. xclose~ s. rew_list in Hn. math. @@ -676,13 +707,15 @@ Qed. (** Array *) (*---------------------------------------------------------------------*) -(*---- -let demo_array () = - let t = Array.make 3 true in - t.(0) <- false; - t.(1) <- false; - t -----*) +(* +[[ + let demo_array () = + let t = Array.make 3 true in + t.(0) <- false; + t.(1) <- false; + t +]] +*) Lemma demo_array_spec : app demo_array [tt] @@ -691,54 +724,57 @@ Lemma demo_array_spec : \* \[forall k, 0 <= k < 3 -> M[k] = isTrue(k > 1)]). Proof using. dup 2. - { xcf. + { (* Detailed proof: *) + xcf. xapp. math. => M EM. xapp. autos. xapp. autos. xret. xsimpl. =>> Hk. subst M. rew_array; autos. case_ifs. math. math. math. } - { xcf. xapp~. => M EM. xapp~. xapp~. xrets. + { (* Shorter proof *) + xcf. xapp~. => M EM. xapp~. xapp~. xrets. =>> Hk. subst M. rew_array~. case_ifs; math. } Qed. (*---------------------------------------------------------------------*) -(*---- -let exercise_array () = - let t = Array.make 3 true in - t.(2) <- false; - t.(1) <- t.(2); - t -----*) - -(* LATER - Lemma example_array_spec : - App example_array tt; - \[] - (fun (t:loc) => Hexists M, (t ~> Array M) \* - \[length M = 3 - /\ forall k, 0 <= k < 3 -> M[k] = isTrue(k<1)]). - Proof using. - xcf. - xapp. autos. intros M EM. subst M. - xapp. autos. - xapp~ as v. intros Ev. - xapp~. - xret. - xsimpl. split. - rew_array~. - introv Hk. rew_array~. case_ifs. - subst v. rew_array~. case_if~. math. - math. - math. - (* Optional forward reasoning after [intros Ev]: - asserts Ev': (v = false). - subst. rew_array~. case_if~. - clear Ev. subst v. *) - Qed. +(* +[[ + let exercise_array () = + let t = Array.make 3 true in + t.(2) <- false; + t.(1) <- t.(2); + t +]] *) +Lemma exercise_array_spec : + App exercise_array tt; + \[] + (fun (t:loc) => Hexists M, (t ~> Array M) \* + \[length M = 3 + /\ forall k, 0 <= k < 3 -> M[k] = isTrue(k<1)]). +Proof using. + xcf. + xapp. autos. intros M EM. subst M. + xapp. autos. + xapp~ as v. intros Ev. + xapp~. + xret. + xsimpl. split. + rew_array~. + introv Hk. rew_array~. case_ifs. + subst v. rew_array~. case_if~. math. + math. + math. + (* Optional forward reasoning after [intros Ev]: + asserts Ev': (v = false). + subst. rew_array~. case_if~. + clear Ev. subst v. *) +Qed. + +