Commit b4f27557 authored by charguer's avatar charguer
Browse files

tour1

parent 18d4c8a2
(*
Set Implicit Arguments.
Require Import CFTactics.
Require Import BatchedQueue_ml.
Module BatchedQueueSpec.
(** instantiations *)
Module Import Q := MLBatchedQueue.
(** invariant *)
Definition inv A (q:queue A) (Q:list A) :=
let (f,r) := q in
Q = (f ++ rev r)
/\ (f = nil -> r = nil).
(** automation *)
Hint Unfold inv.
Ltac auto_tilde ::= eauto.
(** useful facts *)
(** verification *)
Lemma empty_spec : forall A,
inv (@empty A) (@nil A).
Proof.
(* todo arthur: fix display of top_label, and fix tactic below *)
intros. rewrite~ empty_cf.
Qed.
Hint Extern 1 (RegisterSpec empty) => Provide empty_spec.
Lemma is_empty_spec : forall A,
Spec is_empty (q:queue A) |R>> forall Q,
inv q Q ->
R \[] (fun b => \[b = isTrue (Q = nil)]).
Proof.
xcf. intros (f,r) Q [H M].
xmatch; xrets. (* alternative: xgo. *)
fold_bool; rew_refl. (* todo: have a tactic for this *) rewrite~ M in H.
fold_bool; rew_refl. intros E. rewrite E in H.
destruct (nil_eq_app_rev_inv H). false.
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
Lemma checkf_spec : forall A,
Spec checkf (q: queue A) |R>> forall Q,
(let (f,r) := q in Q = (f ++ rev r)) ->
R \[] (fun q' => \[inv q' Q]).
Proof.
xcf. intros q Q H.
xmatch.
- xlet; xret.
hsimpl. subst. rewrite~ <-app_nil_r.
- xret. hsimpl. destruct q.
assert (l <> nil) as H1 by congruence.
assert (l = nil -> l0 = nil) by (intro; false).
auto.
Qed.
Hint Extern 1 (RegisterSpec checkf) => Provide checkf_spec.
Lemma pop_spec : forall A,
Spec pop (q: queue A) |R>> forall Q,
inv q Q -> Q <> nil ->
R \[] (fun p => let '(x, q') := p in Hexists Q',
\[Q = x::Q' /\ inv q' Q']).
Proof.
xcf. intros [x q] Q [I1 I2] H.
xmatch.
- xfail. rewrite I2 in I1. apply (H I1). auto.
- xlet. xapp~.
xret. hsimpl. eauto.
Qed.
Hint Extern 1 (RegisterSpec pop) => Provide pop_spec.
Lemma push_spec : forall A,
Spec push (q: queue A) (x: A) |R>> forall Q,
inv q Q ->
R \[] (fun p => \[inv p (Q & x)]).
Proof.
xcf. intros [x' q'] x Q [I1 I2].
xmatch; xapp~.
hsimpl. subst. rewrite~ <-app_rev_cons.
Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
End BatchedQueueSpec.
*)
\ No newline at end of file
type 'a queue = 'a list * 'a list
let empty : 'a queue = ([],[])
let is_empty q =
match (q : 'a queue) with
| [], _ -> true
| _ -> false
let check = function
| [], r -> (List.rev r, [])
| q -> q
let push (f,r) x =
check (f, x::r)
let pop = function
| [], _ -> raise Not_found
| x::f, r -> (x, check (f,r))
type 'a queue = 'a list * 'a list
val empty : 'a queue
val is_empty : 'a queue -> bool
val push : 'a queue -> 'a -> 'a queue
val pop : 'a queue -> 'a * 'a queue
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import FunctionalQueue_ml.
(*******************************************************************)
(** Representation Predicate *)
Definition inv A (L:list A) (q:queue_ A) :=
let (f,r) := q in
(L = f ++ rev r)
/\ (f = nil -> r = nil).
Hint Unfold inv.
Hint Extern 1 (_ = _ : list _) => rew_list.
(*******************************************************************)
(** Empty *)
Lemma empty_spec : forall A,
inv (@nil A) (@empty A).
Proof.
intros. rewrite* empty__cf.
Qed.
Hint Extern 1 (RegisterSpec empty) => Provide empty_spec.
(*******************************************************************)
(** IsEmpty *)
Lemma is_empty_spec : forall A (L:list A) q,
inv L q ->
app is_empty [q]
PRE \[]
POST (fun b => \[b = isTrue (L = nil)]).
Proof.
intros A L (f,r) [I1 I2]. xcf. dup.
(* Detailed proof *)
{ xmatch.
{ xret. xsimpl. rewrite I1. rewrite I2. auto. auto. }
{ xret. xsimpl. rewrite I1. applys app_not_empty_l. intros E. false* C. } }
(* Shorter proof *)
{ xmatch; xrets.
{ rewrite* I2 in I1. }
{ intros E. subst L. applys* app_not_empty_l. } }
Qed.
Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
(*******************************************************************)
(** Check *)
Lemma check_spec : forall A (f r : list A),
app check [(f,r)]
PRE \[]
POST (fun q => \[inv (f ++ rev r) q]).
Proof.
xcf. xmatch.
{ (* xlet as f. xret. xpull. intros E. xret. xsimpl. unfolds. rew_list*. *)
xrets. xrets*. }
{ xrets. split. { auto. } { intros ->. false* C. } }
Qed.
Hint Extern 1 (RegisterSpec check) => Provide check_spec.
(*******************************************************************)
(** Push *)
Lemma push_spec : forall A (L:list A) q x,
inv L q ->
app push [q x]
PRE \[]
POST (fun q' => \[inv (L ++ x::nil) q']).
Proof.
intros A L [f r] x [I1 I2]. xcf. xmatch. xapp.
xpull. intros I'. xsimpl. rewrite I1.
rew_list in *. auto.
Qed.
Hint Extern 1 (RegisterSpec push) => Provide push_spec.
(*******************************************************************)
(** Pop *)
Lemma pop_spec : forall A (L:list A) q,
inv L q ->
L <> nil ->
app pop [q]
PRE \[]
POST (fun '(x, q') => \[exists L', L = x::L' /\ inv L' q']).
Proof.
intros A L [f r] [I1 I2] N. xcf. xmatch.
{ xfail. rewrite* I2 in I1. }
{ xapp. intros I'. xrets. rew_list in *. eauto. }
Qed.
Hint Extern 1 (RegisterSpec pop) => Provide pop_spec.
include ../Makefile.example
module StackList = struct
type 'a t = {
mutable items : 'a list;
mutable size : int }
let create () =
{ items = [];
size = 0 }
let size s =
s.size
let is_empty s =
s.size = 0
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
end
(*
(*******************************************************************)
(** Unfolding and folding of the representation predicate *)
Lemma Queue_open : forall A (L:list A) f r,
(f,r) ~> Queue L ==>
\[L = f ++ rev r /\ (f = nil -> r = nil)].
Proof using.
dup 2.
{ intros. xunfold Queue. hpull. intros. hcancel. auto.
(* Try [hcancel 3] to see how it works *) }
{ intros. xunfolds~ Queue. }
Qed.
Lemma Queue_close : forall A f r,
(f = nil -> r = nil) ->
\[] ==> (f,r) ~> Queue (f ++ rev r).
Proof using. intros. xunfolds~ Stack. Qed.
Arguments Queue_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 [Queue_open] and [Queue_close].
Note that the number of underscores avec [Queue] after the [RegisterOpen]
needs to match the number of arguments of the representation predicate
[Queue], excluding the pointer. (Here, we have one underscore for [L].) *)
Hint Extern 1 (RegisterOpen (Queue _)) =>
Provide Stack_open.
Hint Extern 1 (RegisterClose (record_repr _)) =>
Provide Stack_close.
--------------
(** Definition of [r ~> Stack L], which is a notation for [Stack L r] of type [hprop] *)
Definition Queue A (L:list A) r :=
Hexists n,
r ~> `{ items' := L; size' := n }
\* \[ n = length L ].
(** Verification of the code *)
Lemma create_spec : forall (A:Type),
app create [tt]
PRE \[]
POST (fun r => r ~> Stack (@nil A)).
Proof using.
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),
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. (* TODO: add xopens to do xpull *)
xopen s. (* details: xchange (@Stack_open s). *)
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.
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.
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),
(* <EXO> *)
app is_empty [s]
INV (s ~> Stack L)
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.
(* 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> *)
Unshelve. solve_type.
Qed.
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)).
Proof using.
(* Hint: use [xcf], [xapp], [xapps], [xpull], [xsimpl],
[xopen], [xclose] and [rew_list] *)
(* <EXO> *)
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.
(* </EXO> *)
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]
PRE (s ~> Stack L)
POST (fun x => Hexists L', \[L = x::L'] \* s ~> Stack L').
Proof using.
(* Hint: also use [rew_list in H] *)
(* <EXO> *)
=>> HL. xcf. xopen s. xpull ;=> n Hn. xapps. xmatch.
xapps. xapps. xapps. xret. xclose~ s. rew_list in Hn. math.
(* </EXO> *)
Qed.
*)
\ No newline at end of file
Set Implicit Arguments.
Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Array_proof.
......@@ -128,7 +128,7 @@ Hint Rewrite math_plus_one_twice math_minus_same
Lemma example_let_spec : forall n,
app example_let [n]
PRE \[]
POST (fun (v:int) => \[v = 2*n]).
POST (fun (v:int) => \[v = 2*n]).
(* post-condition also written: POST \[= (2 * n)] *)
Proof using.
(* Hint: the proof uses [xcf], [xret], [xsimpl], [math].
......@@ -166,7 +166,7 @@ normalized to:
Lemma example_incr_spec : forall r n,
app example_incr [r]
PRE (r ~~> n)
POST (fun (_:unit) => (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].
......@@ -213,12 +213,12 @@ Proof using.
(* Hint: the proof uses [xcf], [xapp], [xapps], and [xret] or [xrets]. *)
dup 3.
{ (* detailed proof *)
xcf.
xcf.
xapp. (* details: xlet. xapp. simpl. *)
xapp. xapp. xapp.
xapp. xapp. xapp.
xapps. (* details: xapp. intro. subst. *)
xapps. xapps. xapps. xapps.
xrets. (* details: xret. xsimpl. *)
xrets. (* details: xret. xsimpl. *)
math. }
{ (* shorter proof, not recommended for nontrivial code *)
xcf. xgo. subst. math. }
......@@ -300,7 +300,7 @@ Proof using.
xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1)) ).
{ math. }
{ xsimpl.
rewrite~ fib_base. (* details: math. math. rewrite fib_base. *)
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.
......@@ -421,7 +421,7 @@ Qed.
(*---------------------------------------------------------------------*)
(* TODO: add demos using the other xfor and xwhile approach *)
(* TODO: add demos using the other xfor and xwhile approach *)
(*---------------------------------------------------------------------*)
......@@ -464,7 +464,7 @@ Proof using.
xclean. (* cleans up results of boolean tests *)
destruct Hb as (Hvp&Hkk).
xapps. xapps. math.
xrets.
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)]).
......@@ -612,7 +612,7 @@ 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].) *)
......@@ -650,9 +650,9 @@ Proof using.
xopen s. (* details: xchange (@Stack_open s). *)
xpull ;=> n Hn.
(* interesting: do [unfold tag] here, to unfold this identity
function used to decorate the file. *)
function used to decorate the file. *)
xapp. (* computes on-the-fly the record_get specification *)
intros m.
intros m.
xpull ;=> ->. (* details: [xpull. intros E. subst E.] *)
xclose s. (* details: xchange (@Stack_close s). *)
auto. xsimpl. math.
......@@ -664,7 +664,7 @@ Qed.
Lemma length_zero_iff_nil : forall A (L:list A),
length L = 0 <-> L = nil.
Proof using.
intros. destruct L; rew_list. (* [rew_list] normalizes list expressions *)
intros. destruct L; rew_list. (* [rew_list] normalizes list expressions *)
{ autos*. (* [intuition eauto] *) }
{ iff M; false; math. (* [iff M] is [split; intros M] *) }
Qed.
......@@ -684,11 +684,11 @@ Proof using.
(* 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.
xopen s. xpull ;=> n Hn. xapps. xclose~ s.
dup 2.
{ xret_no_clean.
{ xret_no_clean.
reflect_clean tt. (* automatically called by [hsimpl] *)
hsimpl.
hsimpl.
subst. apply length_zero_iff_nil. }
{ xrets. subst. apply length_zero_iff_nil. }
(* </EXO> *)
......@@ -706,7 +706,7 @@ Proof using.
xcf.
xopen s. (* details: xchange (@Stack_open s) *)
xpull ;=> n Hn.
xapps. xapp.
xapps. xapp.
xapps. xapp.
xclose s. (* details: xchange (@Stack_close s) *)
rew_list. (* normalizes expression on lists *)
......
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