Commit 9eb3194c authored by Black Rook's avatar Black Rook

Slight tutorial update; more details.

parent 410635e3
Set Implicit Arguments. Set Implicit Arguments.
Require Import CFML.CFLib. Require Import CFML.CFLib.
Require Import Stdlib. Require Import Stdlib.
Require Import Array_proof. Require Import Array_proof.
...@@ -86,6 +86,7 @@ Parameter not_divide_prime_sqrt : forall n r, ...@@ -86,6 +86,7 @@ Parameter not_divide_prime_sqrt : forall n r,
(** Automation for mathematical subgoals *) (** Automation for mathematical subgoals *)
Ltac auto_tilde ::= try solve [ intuition eauto with maths ]. Ltac auto_tilde ::= try solve [ intuition eauto with maths ].
(* TODO: try to use jauto *)
Hint Extern 1 (index ?M _) => subst M : maths. Hint Extern 1 (index ?M _) => subst M : maths.
Hint Resolve LibListZ.index_make : maths. Hint Resolve LibListZ.index_make : maths.
...@@ -593,7 +594,12 @@ Definition Stack A (L:list A) r := ...@@ -593,7 +594,12 @@ Definition Stack A (L:list A) r :=
Lemma Stack_open : forall r A (L:list A), Lemma Stack_open : forall r A (L:list A),
r ~> Stack L ==> r ~> Stack L ==>
Hexists n, r ~> `{ items' := L; size' := n } \* \[ n = length 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), Lemma Stack_close : forall r A (L:list A) (n:int),
n = length L -> n = length L ->
...@@ -606,13 +612,17 @@ Arguments Stack_close : clear implicits. ...@@ -606,13 +612,17 @@ Arguments Stack_close : clear implicits.
(** Customization of [xopen] and [xclose] tactics for [Stack]. (** Customization of [xopen] and [xclose] tactics for [Stack].
These tactics avoid the need to call [hchange] or [xchange] 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 _)) => Hint Extern 1 (RegisterOpen (Stack _)) =>
Provide Stack_open. Provide Stack_open.
Hint Extern 1 (RegisterClose (record_repr _)) => Hint Extern 1 (RegisterClose (record_repr _)) =>
Provide Stack_close. Provide Stack_close.
(** Verification of the code *) (** Verification of the code *)
Lemma create_spec : forall (A:Type), Lemma create_spec : forall (A:Type),
...@@ -620,10 +630,10 @@ Lemma create_spec : forall (A:Type), ...@@ -620,10 +630,10 @@ Lemma create_spec : forall (A:Type),
PRE \[] PRE \[]
POST (fun r => r ~> Stack (@nil A)). POST (fun r => r ~> Stack (@nil A)).
Proof using. Proof using.
xcf. xcf. dup 2.
xapp ;=> r. (* ddetails: xapp. intros r. *) { xapp. intros r. (* or just [xapp. => r] *)
xclose r. (* details: xchange (@Stack_close r). *) xclose r. auto. xsimpl. }
auto. xsimpl. { xapp ;=> r. xclose~ r. }
Qed. Qed.
Lemma size_spec : forall (A:Type) (L:list A) (s:loc), 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), ...@@ -636,9 +646,14 @@ Lemma size_spec : forall (A:Type) (L:list A) (s:loc),
POST (fun n => \[n = length L] \* s ~> Stack L). POST (fun n => \[n = length L] \* s ~> Stack L).
*) *)
Proof using. Proof using.
xcf. xcf. (* TODO: add xopens to do xpull *)
xopen s. (* details: xchange (@Stack_open s). *) 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). *) xclose s. (* details: xchange (@Stack_close s). *)
auto. xsimpl. math. auto. xsimpl. math.
(* Here we have an issue because Coq is a bit limited. (* Here we have an issue because Coq is a bit limited.
...@@ -649,8 +664,9 @@ Qed. ...@@ -649,8 +664,9 @@ Qed.
Lemma length_zero_iff_nil : forall A (L:list A), Lemma length_zero_iff_nil : forall A (L:list A),
length L = 0 <-> L = nil. length L = 0 <-> L = nil.
Proof using. Proof using.
=>. subst. destruct L; rew_list. (* [rew_list] normalizes list expressions *) intros. destruct L; rew_list. (* [rew_list] normalizes list expressions *)
autos*. iff M; false; math. { autos*. (* [intuition eauto] *) }
{ iff M; false; math. (* [iff M] is [split; intros M] *) }
Qed. Qed.
Lemma is_empty_spec : forall (A:Type) (L:list A) (s:loc), Lemma is_empty_spec : forall (A:Type) (L:list A) (s:loc),
...@@ -664,8 +680,17 @@ Proof using. ...@@ -664,8 +680,17 @@ Proof using.
Also use [xcf], [xpull], [xapps], [xrets], Also use [xcf], [xpull], [xapps], [xrets],
and lemma [length_zero_iff_nil] from above. *) and lemma [length_zero_iff_nil] from above. *)
(* <EXO> *) (* <EXO> *)
xcf. xopen s. xpull ;=> n Hn. xapps. xclose~ s. xrets. xcf.
subst. apply length_zero_iff_nil. (* 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. }
(* </EXO> *) (* </EXO> *)
Unshelve. solve_type. Unshelve. solve_type.
Qed. Qed.
...@@ -681,13 +706,20 @@ Proof using. ...@@ -681,13 +706,20 @@ Proof using.
xcf. xcf.
xopen s. (* details: xchange (@Stack_open s) *) xopen s. (* details: xchange (@Stack_open s) *)
xpull ;=> n Hn. xpull ;=> n Hn.
xapps. xapps. xapps. xapp. xapps. xapp.
xapps. xapp.
xclose s. (* details: xchange (@Stack_close s) *) xclose s. (* details: xchange (@Stack_close s) *)
rew_list. math. rew_list. (* normalizes expression on lists *)
math.
xsimpl. xsimpl.
(* </EXO> *) (* </EXO> *)
Qed. 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), Lemma pop_spec : forall (A:Type) (L:list A) (s:loc),
L <> nil -> L <> nil ->
app pop [s] app pop [s]
......
...@@ -15,7 +15,7 @@ Generalizable Variables A. ...@@ -15,7 +15,7 @@ Generalizable Variables A.
Definition char := Ascii.ascii. Definition char := Ascii.ascii.
Definition array (A:Type) := loc. Definition array (A:Type) := loc. (* TODO: deprecate *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment