diff --git a/examples/Tuto/Tuto_proof.v b/examples/Tuto/Tuto_proof.v index 6f762161c6889b9ba82d42710a509438f208e4fd..7c0d85001daecae69a5ae333c41e8fbbd164f12a 100644 --- a/examples/Tuto/Tuto_proof.v +++ b/examples/Tuto/Tuto_proof.v @@ -1,4 +1,4 @@ -Set Implicit Arguments. +Set Implicit Arguments. Require Import CFML.CFLib. Require Import Stdlib. Require Import Array_proof. @@ -86,6 +86,7 @@ Parameter not_divide_prime_sqrt : forall n r, (** Automation for mathematical subgoals *) Ltac auto_tilde ::= try solve [ intuition eauto with maths ]. + (* TODO: try to use jauto *) Hint Extern 1 (index ?M _) => subst M : maths. Hint Resolve LibListZ.index_make : maths. @@ -593,7 +594,12 @@ Definition Stack A (L:list A) r := 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. +Proof using. dup 2. + { intros. xunfold Stack. hpull. intros. hcancel. auto. + (* Try [hcancel 3] to see how it works *) } + { intros. xunfolds~ Stack. } +Qed. + Lemma Stack_close : forall r A (L:list A) (n:int), n = length L -> @@ -606,13 +612,17 @@ 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]. *) + by providing explicitly the lemmas [Stack_open] and [Stack_close]. + Note that the number of underscores avec [Stack] after the [RegisterOpen] + needs to match the number of arguments of the representation predicate + [Stack], excluding the pointer. (Here, we have one underscore for [L].) *) Hint Extern 1 (RegisterOpen (Stack _)) => Provide Stack_open. Hint Extern 1 (RegisterClose (record_repr _)) => Provide Stack_close. + (** Verification of the code *) Lemma create_spec : forall (A:Type), @@ -620,10 +630,10 @@ Lemma create_spec : forall (A:Type), PRE \[] POST (fun r => r ~> Stack (@nil A)). Proof using. - xcf. - xapp ;=> r. (* ddetails: xapp. intros r. *) - xclose r. (* details: xchange (@Stack_close r). *) - auto. xsimpl. + xcf. dup 2. + { xapp. intros r. (* or just [xapp. => r] *) + xclose r. auto. xsimpl. } + { xapp ;=> r. xclose~ r. } Qed. Lemma size_spec : forall (A:Type) (L:list A) (s:loc), @@ -636,9 +646,14 @@ Lemma size_spec : forall (A:Type) (L:list A) (s:loc), POST (fun n => \[n = length L] \* s ~> Stack L). *) Proof using. - xcf. + xcf. (* TODO: add xopens to do xpull *) xopen s. (* details: xchange (@Stack_open s). *) - xpull ;=> n Hn. xapp. => m. xpull ;=> E. + xpull ;=> n Hn. + (* interesting: do [unfold tag] here, to unfold this identity + function used to decorate the file. *) + xapp. (* computes on-the-fly the record_get specification *) + intros m. + xpull ;=> ->. (* details: [xpull. intros E. subst E.] *) xclose s. (* details: xchange (@Stack_close s). *) auto. xsimpl. math. (* Here we have an issue because Coq is a bit limited. @@ -649,8 +664,9 @@ Qed. Lemma length_zero_iff_nil : forall A (L:list A), length L = 0 <-> L = nil. Proof using. - =>. subst. destruct L; rew_list. (* [rew_list] normalizes list expressions *) - autos*. iff M; false; math. + intros. destruct L; rew_list. (* [rew_list] normalizes list expressions *) + { autos*. (* [intuition eauto] *) } + { iff M; false; math. (* [iff M] is [split; intros M] *) } Qed. Lemma is_empty_spec : forall (A:Type) (L:list A) (s:loc), @@ -664,8 +680,17 @@ Proof using. 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. + xcf. + (* Note that the boolean expression [n = 0] from Caml + was automatically translated into [isTrue (x0__ = 0)]; + Indeed, [Ret_ P] is notation for [Ret (isTrue P)]. *) + xopen s. xpull ;=> n Hn. xapps. xclose~ s. + dup 2. + { xret_no_clean. + reflect_clean tt. (* automatically called by [hsimpl] *) + hsimpl. + subst. apply length_zero_iff_nil. } + { xrets. subst. apply length_zero_iff_nil. } (* *) Unshelve. solve_type. Qed. @@ -681,13 +706,20 @@ Proof using. xcf. xopen s. (* details: xchange (@Stack_open s) *) xpull ;=> n Hn. - xapps. xapps. xapps. xapp. + xapps. xapp. + xapps. xapp. xclose s. (* details: xchange (@Stack_close s) *) - rew_list. math. + rew_list. (* normalizes expression on lists *) + math. xsimpl. (* *) Qed. +Hint Extern 1 (RegisterSpec push) => Provide push_spec. + +(* [xapp] on a call to push. + Otherwise, need to do [xapp_spec push_spec]. *) + Lemma pop_spec : forall (A:Type) (L:list A) (s:loc), L <> nil -> app pop [s] diff --git a/lib/coq/CFBuiltin.v b/lib/coq/CFBuiltin.v index f1903038fb6ec0c5a3a7268567fe2e46b5662d50..74eafa652d9f0b9efc20d5a5ffcdd06585690c54 100644 --- a/lib/coq/CFBuiltin.v +++ b/lib/coq/CFBuiltin.v @@ -15,7 +15,7 @@ Generalizable Variables A. Definition char := Ascii.ascii. -Definition array (A:Type) := loc. +Definition array (A:Type) := loc. (* TODO: deprecate *)