Commit eacac182 authored by charguer's avatar charguer
Browse files

notation changes

parent 1830f159
......@@ -39,7 +39,7 @@ Parameter ml_list_iter : func.
(* TODO *)
(* (fun l => Hexists t, l ~> Array Id t \* [t = array_make n v]). *)
(* (# Hexists t', l ~> Array Id t' \* [t' = t\(i:=v)]).*)
(* (# Hexists t', l ~> Array Id t' \* [t' = t[i:=v]]).*)
(* todo: where is local_intro_prop' rebound ? *)
......@@ -88,7 +88,7 @@ Qed.
Lemma focus_mscons' : forall (l e:loc) a A (L:list A) (T:A->a->hprop),
[l <> e] \* (l ~> MListSeg e T L) ==>
Hexists x l', Hexists X L',
[L = X::L'] \* (l ~> Ref Id (x,l')) \* (x ~> T X) \* (l' ~> MListSeg e T L').
[L = X::L'] \* (l ~> Ref Id (x,l')) \* (x ~> T X) \* (l' ~> MListSeg e T L').
Proof.
intros. destruct L. lets: (@unfocus_msnil l e _ _ T). (* Show Existentials. *)
hextract. false~.
......@@ -148,7 +148,7 @@ Proof.
Qed.
Lemma focus_ref2_null : forall a1 a2 A1 A2 (T1:htype A1 a1) (T2:htype A2 a2) V1 V2,
null ~> Ref2 T1 T2 V1 V2 ==> [False].
null ~> Ref2 T1 T2 V1 V2 ==> \[False].
Proof.
intros. unfold hdata, Ref2. hchange focus_ref_null. hsimpl.
Qed.
......@@ -161,20 +161,20 @@ Opaque Ref2.
Fixpoint MList A a (T:A->a->hprop) (L:list A) (l:loc) : hprop :=
match L with
| nil => [l = null]
| nil => \[l = null]
| X::L' => l ~> Ref2 T (MList T) X L'
end.
Lemma focus_mnil : forall A a (T:A->a->hprop),
[] ==> null ~> MList T nil.
\[] ==> null ~> MList T nil.
Proof. intros. simpl. hdata_simpl. hsimpl~. Qed.
Lemma unfocus_mnil : forall (l:loc) A a (T:A->a->hprop),
l ~> MList T nil ==> [l = null].
l ~> MList T nil ==> \[l = null].
Proof. intros. simpl. hdata_simpl. hsimpl~. Qed.
Lemma unfocus_mnil' : forall A (L:list A) a (T:A->a->hprop),
null ~> MList T L ==> [L = nil].
null ~> MList T L ==> \[L = nil].
Proof.
intros. destruct L.
simpl. unfold hdata. hextract. intros. hsimpl~.
......@@ -182,7 +182,7 @@ Proof.
Qed.
Lemma unfocus_mnil'' : forall (l:loc) A (L:list A) a (T:A->a->hprop),
l ~> MList T L ==> [l = null <-> L = nil] \* l ~> MList T L.
l ~> MList T L ==> \[l = null <-> L = nil] \* l ~> MList T L.
Proof. skip. (*todo*) Qed.
Lemma focus_mcons : forall (l:loc) a A (X:A) (L':list A) (T:A->a->hprop),
......@@ -193,9 +193,9 @@ Proof.
Qed.
Lemma focus_mcons' : forall (l:loc) a A (L:list A) (T:A->a->hprop),
[l <> null] \* (l ~> MList T L) ==>
\[l <> null] \* (l ~> MList T L) ==>
Hexists x l', Hexists X L',
[L = X::L'] \* (l ~> Ref Id (x,l')) \* (x ~> T X) \* (l' ~> MList T L').
\[L = X::L'] \* (l ~> Ref Id (x,l')) \* (x ~> T X) \* (l' ~> MList T L').
Proof.
intros. destruct L. lets: (@unfocus_mnil l _ _ T). (* Show Existentials. *)
hextract. intros. false~.
......@@ -516,8 +516,8 @@ Ltac xwhile_core_inner I J R X0 cont1 cont2 cont3 :=
Ltac xwhile_fixj I J :=
match type of J with
| _ -> bool => constr:(fun X B => I X \* [B = J X])
| _ -> Prop => constr:(fun X B => I X \* [bool_of (J X) B])
| _ -> bool => constr:(fun X B => I X \* \[B = J X])
| _ -> Prop => constr:(fun X B => I X \* \[bool_of (J X) B])
end.
Ltac xextract_post_clean tt :=
......
......@@ -57,17 +57,17 @@ Notation "x \notindom' E" := (x \notin ((dom E) : set _))
Axiom ml_ref_spec_group : forall a,
Spec ml_ref (v:a) |R>> forall (M:map loc a),
R (Group (Ref Id) M) (fun l => Group (Ref Id) (M\(l:=v)) \* [l\notindom' M]).
R (Group (Ref Id) M) (fun l => Group (Ref Id) (M[l:=v]) \* [l\notindom' M]).
Axiom ml_get_spec_group : forall a,
Spec ml_get (l:loc) |R>> forall (M:map loc a),
forall `{Inhab a}, l \indom M ->
keep R (Group (Ref Id) M) (\= M\(l)).
keep R (Group (Ref Id) M) (\= M[l]).
Axiom ml_set_spec_group : forall a,
Spec ml_set (l:loc) (v:a) |R>> forall (M:map loc a),
forall `{Inhab a}, l \indom M ->
R (Group (Ref Id) M) (# Group (Ref Id) (M\(l:=v))).
R (Group (Ref Id) M) (# Group (Ref Id) (M[l:=v])).
......@@ -279,7 +279,7 @@ Hint Resolve is_repr_in_dom_l is_repr_in_dom_r.
(** General lemmas *)
Lemma is_repr_add_node : forall M r c x y,
r \notin (dom M:set _) -> is_repr M x y -> is_repr (M\(r:=c)) x y.
r \notin (dom M:set _) -> is_repr M x y -> is_repr (M[r:=c]) x y.
Proof. introv N H. induction H; constructors*. Qed.
Lemma binds_diff_false : forall x y M,
......@@ -303,7 +303,7 @@ Hint Resolve node_not_root points_indom.
(** Lemmas about 'forest' *)
Lemma is_forest_add_node : forall M r,
is_forest M -> r \notindom' M -> is_forest (M\(r:=Root)).
is_forest M -> r \notindom' M -> is_forest (M[r:=Root]).
Proof.
introv FM Dr. intros x Dx. destruct (map_indom_update_inv Dx).
subst*.
......@@ -312,7 +312,7 @@ Qed.
Lemma is_forest_add_edge : forall M rx ry,
is_forest M -> binds M rx Root -> binds M ry Root -> rx <> ry ->
is_forest (M\(rx:=Node ry)).
is_forest (M[rx:=Node ry]).
Proof.
introv FM Bx By Neq. intros x D. rewrite* dom_update_in in D.
forwards~ [r R]: FM x. tests (r = rx) as C.
......@@ -331,12 +331,12 @@ Hint Resolve binds_update_neq_inv.
Lemma path_compression : forall M B x r,
describes B M -> B x r ->
describes B (M\(x:=Node r)).
describes B (M[x:=Node r]).
Admitted. (* todo *)
Lemma describes_add_node : forall M B z,
describes B M -> z \notindom' M ->
describes (add_node B z) (M\(z:=Root)).
describes (add_node B z) (M[z:=Root]).
Proof.
introv (PB&FM&DM&EM) Mz. splits.
apply~ per_add_node.
......@@ -346,22 +346,22 @@ Proof.
(* -- case [is_equiv M' -> B'] *)
intros (r&Rx&Ry). tests (r = z).
(* -- subcase [r = z] *)
cuts St: (forall x, is_repr (M\(z:=Root)) x z -> x = z).
cuts St: (forall x, is_repr (M[z:=Root]) x z -> x = z).
rewrite~ (St x). rewrite~ (St y). right. unfolds~.
clears x y. introv H. gen_eq r: z. gen_eq M': (M\(r:=Root)).
clears x y. introv H. gen_eq r: z. gen_eq M': (M[r:=Root]).
induction~ H; intro_subst; intro_subst.
forwards~: IHis_repr. subst y. false. tests (x = z).
applys* (>> binds_diff_false H).
forwards*: points_indom x.
(* -- subcase [r <> z] *)
cuts St: (forall x, is_repr (M\(z:=Root)) x r -> is_repr M x r).
cuts St: (forall x, is_repr (M[z:=Root]) x r -> is_repr M x r).
left. rewrite <- EM. exists* r.
clears x y. introv H. induction H. applys* is_repr_root. eauto 7.
(* -- case [B' -> is_equiv M'] *)
intros [H|[Ex Ey]].
(* -- subcase [B x y] *)
rewrite <- EM in H. destruct H as (r&Rx&Ry).
cuts St: (forall x, is_repr M x r -> is_repr (M\(z:=Root)) x r).
cuts St: (forall x, is_repr M x r -> is_repr (M[z:=Root]) x r).
exists* r.
clears x y. introv H. induction H. eauto.
cuts*: (x <> z). intro_subst. lets~: binds_dom H.
......@@ -393,7 +393,7 @@ Lemma describes_add_edge : forall M B a b ra rb,
describes B M ->
ra <> rb -> ra \in per_dom B -> rb \in per_dom B ->
is_repr M a ra -> is_repr M b rb ->
describes (add_edge B a b) (M\(ra:=Node rb)).
describes (add_edge B a b) (M[ra:=Node rb]).
Proof.
introv (PB&FM&DM&EM) Neq Da Db Ra Rb. splits.
applys~ per_add_edge.
......@@ -407,7 +407,7 @@ Proof.
intros (r&Rx&Ry). tests (r = rb) as C.
(* -- subcase [r = rb] *)
sets B': (add_edge B a b). asserts PB': (per B'). unfold B'. apply~ per_add_edge.
cuts St: (forall x, is_repr (M\(ra:=Node rb)) x rb -> B' x rb). applys~ trans_sym_2.
cuts St: (forall x, is_repr (M[ra:=Node rb]) x rb -> B' x rb). applys~ trans_sym_2.
clears x y. introv H. gen_eq r:rb. gen Rb. induction H; intros.
subst x. applys stclosure_step. left. cuts~: (rb \in per_dom B).
rewrite <- DM. applys~ (map_indom_update_already_inv (binds_dom H)).
......@@ -420,7 +420,7 @@ Proof.
forwards: binds_update_neq_inv x; eauto 3.
forwards [ry Hry]: FM y __; eauto 3. exists* ry.
(* -- case [r <> rb] *)
cuts St: (forall x, is_repr (M\(ra:=Node rb)) x r -> is_repr M x r).
cuts St: (forall x, is_repr (M[ra:=Node rb]) x r -> is_repr M x r).
applys add_edge_le. rewrite <- EM. exists* r.
clears x y. introv H. induction H; cuts*: (x <> ra).
intro_subst. lets N: (binds_get H). rew_map in N. inverts N.
......@@ -428,8 +428,8 @@ Proof.
renames y to rb. applys C. applys* is_repr_inj.
(* -- case [B' -> is_equiv M'] *)
asserts [Sa Sr]:
((forall x, is_repr M x ra -> is_repr (M\(ra:=Node rb)) x rb) /\
(forall x r, r <> ra -> is_repr M x r -> is_repr (M\(ra:=Node rb)) x r)).
((forall x, is_repr M x ra -> is_repr (M[ra:=Node rb]) x rb) /\
(forall x r, r <> ra -> is_repr M x r -> is_repr (M[ra:=Node rb]) x r)).
clears x y. split.
introv H. induction H; eauto 7.
introv Nq H. induction H; eauto 7.
......
......@@ -36,10 +36,10 @@ Ltac auto_tilde ::= try solve [ intros; auto with maths ].
*)
Lemma if_demo_spec :
Spec if_demo (b:bool) |B>>
B [] (fun (x:int) => [0 <= x <= 1]).
B \[] (fun (x:int) => \[0 <= x <= 1]).
Proof.
xcf. intros. xapp. xapps.
xseq (Hexists (x:int), r ~~> x \* [x = 0 \/ x = 1] \* s ~~> 5).
xseq (Hexists (x:int), r ~~> x \* \[x = 0 \/ x = 1] \* s ~~> 5).
xif. xapp~. hsimpl~. xrets~.
introv C. xgc. xapps. intros M. hsimpl. subst. invert C; math.
Qed.
......@@ -66,7 +66,7 @@ Hint Extern 1 (index _ _) => index_solve.
Lemma array_demo_spec :
Spec array_demo () |B>>
B [] (fun n => [n = 3]).
B \[] (fun n => \[n = 3]).
Proof.
xcf.
xapp. xapp. hnf. math. intros L (LL&LV).
......@@ -123,7 +123,7 @@ Qed.
(* below, "keep B H Q" is the same as "B H (Q \*+ H)";
here, it is the same as
"B (r ~> RMyrec n L)
(fun (k:int) => [k = LibList.length L] \* r ~> RMyrec n L)."
(fun (k:int) => \[k = LibList.length L] \* r ~> RMyrec n L)."
*)
(*
......@@ -135,7 +135,7 @@ Lemma myrec_length_items : forall A,
Spec myrec_length_items (r:myrec A) |B>>
forall n (L:list A),
keep B (r ~> RMyrec n L)
(fun (k:int) => [k = LibList.length L]).
(fun (k:int) => \[k = LibList.length L]).
Proof.
xcf. intros. xapps. xrets. auto.
Qed.
......@@ -147,7 +147,7 @@ Qed.
equal to the length of the list Q. *)
Definition SizedList A (Q:list A) (r:myrec A) :=
Hexists n, r ~> RMyrec n Q \* [n = LibList.length Q].
Hexists n, r ~> RMyrec n Q \* \[n = LibList.length Q].
Lemma SizedList_unfocus : forall A (r:myrec A) (Q:list A) (n:int),
n = LibList.length Q ->
......@@ -164,7 +164,7 @@ Implicit Arguments SizedList_unfocus [A].
Definition SizedList' A (Q:list A) (r:myrec A) :=
Hexists n L, r ~> RMyrec n L \*
[n = LibList.length L /\ L = Q].
\[n = LibList.length L /\ L = Q].
Lemma SizedList_equiv : forall A (Q:list A) (r:myrec A),
r ~> SizedList Q ==> r ~> SizedList' Q.
......@@ -186,7 +186,7 @@ Lemma myrec_inv_length_items : forall A,
Spec myrec_inv_length_items (r:myrec A) |B>>
forall (Q:list A),
keep B (r ~> SizedList Q)
(fun (k:int) => [k = LibList.length Q]).
(fun (k:int) => \[k = LibList.length Q]).
Proof.
xcf. intros. hunfold SizedList at 1.
xextract as n En. xapp. intros x. hextract as Ex. subst.
......@@ -247,7 +247,7 @@ Qed.
Lemma half_spec_1 :
forall n x, n >= 0 -> x = n+n ->
(App half x;) [] (\= n).
(App half x;) \[] (fun x => \[x = n]).
Proof.
intros n. induction_wf IH: (int_downto_wf 0) n.
introv P D. xcf_app.
......@@ -269,7 +269,7 @@ Qed.
Lemma half_spec_2 :
forall x n, n >= 0 -> x = n+n ->
(App half x;) [] (\= n).
(App half x;) \[] (fun x => \[x = n]).
Proof.
intros x. induction_wf IH: (int_downto_wf 0) x.
introv P D. xcf_app.
......@@ -293,7 +293,7 @@ Qed.
Lemma half_spec_3 :
Spec half (x:int) |R>>
forall n, n >= 0 -> x = n+n ->
R [] (\= n).
R \[] (\= n).
Proof.
xinduction (downto 0). xcf.
introv IH P D.
......@@ -317,7 +317,7 @@ TODO: fix this
Lemma half_spec_4 :
Spec half (x:int) |R>>
forall n, n >= 0 -> x = n+n ->
R [] (\= n).
R \[] (\= n).
Proof.
xinduction (downto 0). xcf. introv IH P D.
repeat xif. xgo~. xgo~. xapp~ (n-1). xgo~.
......@@ -329,7 +329,7 @@ Qed.
Lemma half_spec_5 :
Spec half (x:int) |R>>
forall n, n >= 0 -> x = n+n ->
R [] (\= n).
R \[] (fun x => \[x = n]).
Proof.
xinduction_heap (unproj21 int (downto 0)).
xcf. intros x n IH P D.
......@@ -343,7 +343,7 @@ Qed.
(* Partial apps *)
Lemma add_spec :
Spec add x y |R>> R [] (\= (x + y)).
Spec add x y |R>> R \[] (fun z => \[z = x + y]).
Proof. xgo*. Qed.
Hint Extern 1 (RegisterSpec add) => Provide add_spec.
......@@ -356,22 +356,22 @@ Proof. xcf. auto. Qed.
Hint Extern 1 (RegisterSpec hof) => Provide hof_spec.
Lemma test_partial_app_1_spec :
Spec test_partial_app_1 () |R>> R [] (\= 3).
Spec test_partial_app_1 () |R>> R \[] (fun x => \[x = 3]).
Proof.
xcf. xapp_partial. intros Sg. xapp. hsimpl*.
(* or: xcf. xlet. xframe - []. xapp_partial. xok. xextract. intros Sg. xapp. hsimpl*. *)
(* or: xcf. xlet. xframe - \[]. xapp_partial. xok. xextract. intros Sg. xapp. hsimpl*. *)
Qed.
Lemma test_partial_app_1_spec' : forall x,
Spec test_partial_app_1 () |R>> R (x ~~> 4) (fun r => [r = 3] \* x ~~> 4).
Spec test_partial_app_1 () |R>> R (x ~~> 4) (fun r => \[r = 3] \* x ~~> 4).
Proof.
xcf. xapp_partial. intros Sg. xapp. hsimpl*.
Qed.
Lemma test_partial_app_1_spec'' : forall x,
Spec test_partial_app_1 () |R>> R (x ~~> 4) (fun r => [r = 3] \* x ~~> 4).
Spec test_partial_app_1 () |R>> R (x ~~> 4) (fun r => \[r = 3] \* x ~~> 4).
Proof.
xcf. xlet. (* how to execute xapp_partial step by step *)
......@@ -393,36 +393,36 @@ Qed.
Lemma test_partial_app_2_spec :
Spec test_partial_app_2 () |R>> R [] (\= 4).
Spec test_partial_app_2 () |R>> R \[] (fun x => \[x = 4]).
Proof.
xcf. xapp_partial as P1. intros HP1.
xapp []. (* effectively inline the code of the function [hof] *)
xapp \[]. (* effectively inline the code of the function [hof] *)
(* -> the empty heap is used to instantiate the variable [H] from [hof_spec] *)
xapp. (* reason about the application of function [P1] *)
hsimpl*.
Qed.
Lemma test_partial_app_2_spec' :
Spec test_partial_app_2 () |R>> R [] (\= 4).
Spec test_partial_app_2 () |R>> R \[] (fun x => \[x = 4]).
Proof.
xcf. xapp_partial as P1. intros HP1.
xapp. (* if we do not provide the argument [H] *)
xapp.
instantiate (1 := []). hsimpl. (* then we later need to instantiate it manually *)
instantiate (1 := \[]). hsimpl. (* then we later need to instantiate it manually *)
(* even though in this particular example, a more powerful version of
hsimpl should be able to do the unification properly *)
hsimpl*.
Qed.
Lemma func4_spec :
Spec func4 a b c d |R>> R [] (\= (a + b + c + d)).
Spec func4 a b c d |R>> R \[] (fun x => \[x = a + b + c + d]).
Proof. xgo*. Qed.
Hint Extern 1 (RegisterSpec func4) => Provide func4_spec.
Lemma test_partial_app_3_spec :
Spec test_partial_app_3 () |R>> R [] (\= 30).
Spec test_partial_app_3 () |R>> R \[] (fun x => \[x = 30]).
Proof.
xcf.
xapp_partial. intros Hf1.
......@@ -439,7 +439,7 @@ Qed.
(* Inlining *)
Lemma test_inlining_spec :
Spec test_inlining () |R>> R [] (\= 4).
Spec test_inlining () |R>> R \[] (fun x => \[x = 4]).
Proof.
xcf.
xfun f. (* use the most-general spec for specifying the local function *)
......@@ -482,7 +482,7 @@ Check _set_content_spec.
Fixpoint CList a A (T:A->a->hprop) (L:list A) (l:loc) : hprop :=
match L with
| nil => []
| nil => \[]
| X::L' => l ~> Cell T (CList T) X L'
end.
......
......@@ -36,7 +36,7 @@ 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)]).
R \[] (fun b => \[b = isTrue (Q = nil)]).
Proof.
xcf. intros (f,r) Q [H M].
xmatch; xrets. (* alternative: xgo. *)
......@@ -50,7 +50,7 @@ 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]).
R \[] (fun q' => \[inv q' Q]).
Proof.
xcf. intros q Q H.
xmatch.
......@@ -67,8 +67,8 @@ 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']).
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.
......@@ -82,7 +82,7 @@ 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)]).
R \[] (fun p => \[inv p (Q & x)]).
Proof.
xcf. intros [x' q'] x Q [I1 I2].
xmatch; xapp~.
......
......@@ -224,7 +224,7 @@ Hint Extern 1 (RegisterSpec empty) => Provide empty_spec.
Lemma is_empty_spec :
Spec is_empty (l: rlist a) |R>>
R [] (fun (b: bool) => [b = isTrue (l = nil)]).
R \[] (fun (b: bool) => \[b = isTrue (l = nil)]).
Proof.
xcf. xgo; hsimpl; fold_bool; fold_prop; eauto.
Qed.
......@@ -234,7 +234,7 @@ Hint Extern 1 (RegisterSpec is_empty) => Provide is_empty_spec.
(* private *)
Lemma size_spec :
Spec size (t: tree a) |R>>
R [] (fun (n: int) => [n = Size t]).
R \[] (fun (n: int) => \[n = Size t]).
Proof. xcf. xgo~. Qed.
Hint Extern 1 (RegisterSpec size) => Provide size_spec.
......@@ -242,7 +242,7 @@ Hint Extern 1 (RegisterSpec size) => Provide size_spec.
Lemma link_spec :
Spec link (t1:tree a) (t2:tree a) |R>>
forall p L1 L2, btree p t1 L1 -> btree p t2 L2 ->
R [] (fun t' => [btree (p+1) t' (L1++L2)]).
R \[] (fun t' => \[btree (p+1) t' (L1++L2)]).
Proof.
xcf. intros. repeat xapps. xret. hsimpl. constructors~.
do 2 (erewrite btree_size_correct; eauto).
......@@ -254,7 +254,7 @@ Hint Extern 1 (RegisterSpec link) => Provide link_spec.
Lemma cons_tree_spec :
Spec cons_tree (t:tree a) (ts:rlist a) |R>>
forall p T L, btree p t T -> inv p ts L ->
R [] (fun ts' => [inv p ts' (T++L)]).
R \[] (fun ts' => \[inv p ts' (T++L)]).
Proof.
xinduction (fun (t:tree a) (ts:rlist a) => length ts).
xcf. introv IH Rt Rts. inverts Rts.
......@@ -270,7 +270,7 @@ Hint Extern 1 (RegisterSpec cons_tree) => Provide cons_tree_spec.
Lemma cons_spec :
Spec cons (x: a) (l: rlist a) |R>>
forall L, Rlist l L ->
R [] (fun l' => [Rlist l' (x::L)]).
R \[] (fun l' => \[Rlist l' (x::L)]).
Proof.
xcf. introv RL. xapp~. hsimpl~.
Qed.
......@@ -280,8 +280,8 @@ Hint Extern 1 (RegisterSpec cons) => Provide cons_spec.
Lemma uncons_tree_spec :
Spec uncons_tree (ts:rlist a) |R>>
forall p L, inv p ts L -> ts <> nil ->
R [] (fun r => let (t',ts') := r : tree a * rlist a in
[exists T' L', btree p t' T' /\ inv p ts' L' /\ L = T' ++ L']).
R \[] (fun r => let (t',ts') := r : tree a * rlist a in
\[exists T' L', btree p t' T' /\ inv p ts' L' /\ L = T' ++ L']).
Proof.
xinduction (fun (ts:rlist a) => length ts).
xcf. introv IH Rts Ne. xmatch; inverts Rts as.
......@@ -304,7 +304,7 @@ Hint Extern 1 (RegisterSpec uncons_tree) => Provide uncons_tree_spec.
Lemma head_spec :
Spec head (l: rlist a) |R>>
forall L, Rlist l L -> l <> nil ->
R [] (fun x => [is_head L x]).
R \[] (fun x => \[is_head L x]).
Proof.
xcf. introv Rts NE.
xapp~ as [t l]. intros (?&?&B&I&?). xmatch.
......@@ -319,7 +319,7 @@ Hint Extern 1 (RegisterSpec head) => Provide head_spec.
Lemma tail_spec :
Spec tail (l: rlist a) |R>>
forall L, Rlist l L -> l <> nil ->
R [] (fun tl => [exists TL, Rlist tl TL -> is_tail L TL]).
R \[] (fun tl => \[exists TL, Rlist tl TL -> is_tail L TL]).
Proof.
xcf. introv Rts NE. xgo~. xextract as H'. unpack H'.
hsimpl. subst. exists___.
......@@ -335,7 +335,7 @@ Require Import LibInt.
Lemma lookup_tree_spec :
Spec lookup_tree (i: int) (t: tree a) |R>>
forall p L, btree p t L -> ZInbound i L ->
R [] (fun x => [ZNth i L x]).
R \[] (fun x => \[ZNth i L x]).
Proof.
xinduction (fun (i:int) t => tree_size t).
xcf. intros i t. introv IH Rt Bi. inverts Rt. xmatch.
......@@ -355,7 +355,7 @@ Hint Extern 1 (RegisterSpec lookup_tree) => Provide lookup_tree_spec.
Lemma update_tree_spec :
Spec update_tree (i: int) (x: a) (t: tree a) |R>>
forall p L, btree p t L -> ZInbound i L ->
R [] (fun t' => [exists L', btree p t' L' /\ ZUpdate i x L L']).
R \[] (fun t' => \[exists L', btree p t' L' /\ ZUpdate i x L L']).
Proof.
xinduction (fun (i:int) (x:a) t => tree_size t).
xcf. intros i x t. introv IH Rt Bi. inverts Rt; xmatch.
......@@ -373,7 +373,7 @@ Hint Extern 1 (RegisterSpec update_tree) => Provide update_tree_spec.
Lemma lookup_spec_ind :
Spec lookup (i:int) (ts: rlist a) |R>>
forall p L, inv p ts L -> ZInbound i L ->
R [] (fun x => [ZNth i L x]).
R \[] (fun x => \[ZNth i L x]).
Proof.
xinduction (fun (i:int) (ts:rlist a) => length ts).
xcf. intros i ts. introv IH Rts Bi. xmatch; inverts Rts.
......@@ -389,7 +389,7 @@ Qed.
Lemma lookup_spec :
Spec lookup (i: int) (ts: rlist a) |R>>
forall L, Rlist ts L -> ZInbound i L ->
R [] (fun x => [ZNth i L x]).
R \[] (fun x => \[ZNth i L x]).
Proof.
xweaken lookup_spec_ind. introv W H Rts Bi.
simpl in Rts. apply~ H.
......@@ -398,7 +398,7 @@ Qed.
Lemma update_spec_ind :
Spec update (i: int) (x: a) (ts: rlist a) |R>>
forall p L, inv p ts L -> ZInbound i L ->
R [] (fun ts' => [exists L', inv p ts' L' /\ ZUpdate i x L L']).
R \[] (fun ts' => \[exists L', inv p ts' L' /\ ZUpdate i x L L']).
Proof.
xinduction (fun (i:int) (x:a) (ts:rlist a) => length ts).
xcf. intros i x ts. introv IH Rts Bi. xmatch; inverts Rts.
......@@ -416,7 +416,7 @@ Qed.
Lemma update_spec :
Spec update (i: int) (x: a) (ts: rlist a) |R>>