Commit 4d27c29f by charguer

### mutable_queue

parent 09fdfa70
 ... ... @@ -21,7 +21,7 @@ let push x s = let pop s = if s.front = [] then begin s.front <- s.back; s.front <- List.rev s.back; s.back <- []; end; match s.front with ... ...
 ... ... @@ -18,7 +18,7 @@ Qed. (*******************************************************************) (** Representation Predicate *) Definition Queue A (L:list A) q := Definition Queue A (L:list A) (q:t_ A) := Hexists (f:list A) (b:list A) (n:int), q ~> `{ front' := f; back' := b; size' := n } \* \[ L = f ++ rev b ] \* \[ n = length L ]. ... ... @@ -59,7 +59,7 @@ Hint Extern 1 (RegisterClose (record_repr _)) => (*******************************************************************) (** Create *) Lemma create_spec : forall (A:Type), Lemma create_spec : forall A, app create [tt] PRE \[] POST (fun q => q ~> Queue (@nil A)). ... ... @@ -87,8 +87,7 @@ Proof using. xopen q. (* details: xchange (@Stack_open s). *) xpull ;=> f b n I1 I2. xapp. xpull. intros ->. xclose q. (* details: xchange (@Stack_close s). *) { subst*. } xclose q. { subst*. } (* details: xchange (@Stack_close s). *) xsimpl*. (* Here we have an issue because Coq is unable to infer a type. *) Unshelve. solve_type. ... ... @@ -108,30 +107,19 @@ Proof using. Unshelve. solve_type. Qed. (* (*******************************************************************) (** Push *) Lemma push_spec : forall (A:Type) (L:list A) (s:loc) (x:A), app push [x s] PRE (s ~> Stack L) POST (# s ~> Stack (x::L)). Lemma push_spec : forall A (L:list A) q x, app push [x q] PRE (q ~> Queue L) POST (fun (_:unit) => q ~> Queue (L ++ x::nil)). Proof using. (* Hint: use [xcf], [xapp], [xapps], [xpull], [xsimpl], [xopen], [xclose] and [rew_list] *) (* *) xcf. xopen s. (* details: xchange (@Stack_open s) *) xpull ;=> n Hn. xapps. xapp. xapps. xapp. xclose s. (* details: xchange (@Stack_close s) *) rew_list. (* normalizes expression on lists *) math. xsimpl. (* *) xcf. xopen q. xpull. intros f b n I1 I2. xapps. xapp. xapps. xapp. xclose q. { subst. rew_list. math. } xsimpl. subst. rew_list*. Qed. Hint Extern 1 (RegisterSpec push) => Provide push_spec. ... ... @@ -140,17 +128,25 @@ Hint Extern 1 (RegisterSpec push) => Provide push_spec. (*******************************************************************) (** Pop *) Lemma pop_spec : forall (A:Type) (L:list A) (s:loc), Lemma pop_spec : forall A (L:list A) q, L <> nil -> app pop [s] PRE (s ~> Stack L) POST (fun x => Hexists L', \[L = x::L'] \* s ~> Stack L'). app pop [q] PRE (q ~> Queue L) POST (fun x => Hexists L', \[L = x::L'] \* q ~> Queue 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. (* *) introv N. xcf. xopen q. xpull. intros f b n I1 I2. xapps. xapps. xpolymorphic_eq. xseq (fun (_:unit) => Hexists f' b', q ~> `{ front' := f'; back' := b'; size' := n } \* \[ L = f' ++ rev b' ] \* \[ f' = nil -> b' = nil ]). { xif. { xapps. xrets. xapps. xapps. xsimpl. { auto. } { subst. rew_list*. } } { xrets. { intros. false. } { auto. } } } { clears f b. intros f b I1 I3. xapps. xmatch. { xfail. rewrite I3 in I1. { rew_list in *. false. } { auto. } } { xapps. xapps. xapps. xret. xclose q. { subst L. rew_list in *. math. } xsimpl. subst L. rew_list*. } } Qed. *) \ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!