Skip to content

GitLab

C
cfml
Commit 443ed16c authored by charguer's avatar charguer
Browse files
Options

compile

parent d62cc173
Show whitespace changes
Inline Side-by-side
Showing with 58 additions and 42 deletions
model/ExampleList.v
View file @ 443ed16c
......@@ -540,7 +540,7 @@ Proof using.
\[b = isTrue (L1 <> nil)] \* \[L = rev L2 ++ L1]
\* rp ~~> p \* p ~> MList L1 \* rs ~~> s \* s ~> MList L2).
exists __ I (@list_sub A) __. splits.
{ prove_wf. }
{ solve_wf. }
{ hchange MList_nil. unfold I. hsimpl*. }
{ intros F LF b L1 IH. unfold I at 1. xpull ;=> p s L2 E1 E2. clears b.
xlet. { xapps. xapps~. } xpull; isubst.
......
model/ExampleListNonlifted.v
View file @ 443ed16c
......@@ -374,7 +374,7 @@ Proof using.
{ applys local_erase. xapplys rule_neq. }
intros X. xpull. intros EX. subst X.
applys local_erase. esplit. splits. eauto.
{ intros C. rew_istrue. xchange (MList_not_null_inv_cons p). { auto. }
{ intros C. rew_bool_eq in *. xchange (MList_not_null_inv_cons p). { auto. }
xpull. intros p' x L' EL.
applys local_erase. esplit. split.
{ applys local_erase. xapplys rule_get_tl. }
......@@ -383,8 +383,8 @@ Proof using.
{ applys local_erase. xapplys IH. { subst~. } }
{ intros r. xpull. intros Er. xchange (MList_cons p).
subst r L. applys local_erase. xapplys rule_add.
{ intros. subst. rew_length. fequals. math. } } }
{ intros C. rew_istrue. applys local_erase. unfolds. inverts C.
{ intros. subst. rew_list. fequals. math. } } }
{ intros C. rew_bool_eq in *. applys local_erase. unfolds. inverts C.
xchange MList_null_inv. hpull. intros EL.
hsimpl. subst~. }
Qed.
......@@ -407,7 +407,7 @@ Proof using.
xpull ;=> E. subst p''.
xlet as r. { xapp IH. { subst~. } }
xpull ;=> Er. subst r L. xchange (MList_cons p).
xapp. { hsimpl. intros. subst. rew_length. fequals. math. } }
xapp. { hsimpl. intros. subst. rew_list. fequals. math. } }
{ xval. inverts C. xchange MList_null_inv.
hpull ;=> EL. hsimpl. subst~. }
Qed.
......@@ -426,7 +426,7 @@ Proof using.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL. subst L.
xapps. xapps~ IH.
xchange (MList_cons p).
xapps. hsimpl. isubst. rew_length. fequals. math. }
xapps. hsimpl. isubst. rew_list. fequals. math. }
{ inverts C. xchanges MList_null_inv ;=> EL. subst. xvals~. }
Qed.
......@@ -615,7 +615,7 @@ Proof using.
xapps. xapps.
xchanges (MListSeg_then_MCell_inv_neq pf pb) ;=> R.
(* xchange (MListSeg_then_MCell_inv_neq pf pb). xpull ;=> R. *)
xapp. hsimpl. isubst. fequals. rew_istrue. rewrite R. iff; congruence.
xapp. hsimpl. isubst. fequals. rew_bool_eq. rewrite R. iff; congruence.
Qed.
Hint Extern 1 (Register_spec val_is_empty) => Provide rule_is_empty.
......@@ -716,7 +716,7 @@ Lemma rule_transfer : forall p1 p2 L1 L2,
(MQueue L1 p1 \* MQueue L2 p2)
(fun r => \[r = val_unit] \* MQueue (L1 ++ L2) p1 \* MQueue nil p2).
Proof using.
xcf. xapps. xapps. xif ;=> C; fold_bool; rew_istrue. (* todo cleanup *)
xcf. xapps. xapps. xif ;=> C; rew_bool_eq.
{ unfold MQueue. xpull ;=> pf2 pb2 vx2 vy2 pf1 pb1 vx1 vy1.
destruct L2 as [|x L2']; tryfalse.
rewrite MListSeg_cons_eq. xpull ;=> pf2'.
......
model/ExampleTrees.v
View file @ 443ed16c
......@@ -17,6 +17,16 @@ Implicit Types p : loc.
Implicit Types E : (LibSet.set int).
(**--TODO: move*)
Instance Le_total_order_Z : Le_total_order (A:=Z).
Proof using.
constructor. constructor. constructor; unfolds.
math. math. math. unfolds.
intros. tests: (x <= y). left~. right. math.
Qed.
(* ********************************************************************** *)
(* * Formalization of binary trees *)
......@@ -106,7 +116,7 @@ Proof using.
{ xunfold MTree. applys himpl_antisym; hsimpl~. }
{ xunfold MTree. applys himpl_antisym.
{ hpull ;=> p'. hchange (hRecord_not_null null).
{ simpl. unfold hd. auto. }
{ simpl. unfold item. auto. }
{ hpull; auto_false. } }
{ hpull. } }
Qed. (* todo: factorize with proof for lists *)
......@@ -329,7 +339,7 @@ Global Opaque Stree.
(* ---------------------------------------------------------------------- *)
(* ** Automation *)
Hint Extern 1 (_ = _ :> LibSet.set _) => permut_simpl : set.
Hint Extern 1 (_ = _ :> LibSet.set _) => set_prove : set.
Ltac auto_tilde ::= eauto.
Ltac auto_star ::= try solve [ intuition (eauto with set) ].
......
model/ExampleUnionFind.v
View file @ 443ed16c
......@@ -245,7 +245,7 @@ Proof using.
{ rewrite~ @index_update_eq. }
{ rewrite~ @index_update_eq in H. }
{ rewrite~ @read_update_neq. }
{ rewrite~ @read_update_eq. }
{ rewrite~ @read_update_same. }
Qed.
Lemma repr_update_neq : forall L a b L' x z,
......@@ -366,6 +366,9 @@ Definition val_root :=
in
F X.
Hint Rewrite @index_map_eq : rew_array. (*--TODO move *)
Lemma rule_root : forall n R p x,
index n x ->
triple (val_root p x)
......@@ -374,13 +377,15 @@ Lemma rule_root : forall n R p x,
Proof using.
introv Dx. xcf. xval as F ;=> EF.
unfold UF. xpull ;=> L (Hn&HR).
forwards~ Ix: index_length_eq (rm Dx) Hn.
forwards~ Ix: index_of_index_length' (rm Dx) Hn.
forwards~ Hx: HR x.
forwards (d&Hx'): reprn_of_repr Hx.
applys local_erase.
gen x. induction_wf IH: lt_wf d. hide IH. intros.
rewrite EF. xcf. rewrite <- EF.
xapp as vy. rew_arr~. rewrite read_map; auto. intros Evy. subst vy.
xapp as vy. rew_array~. rewrite (@read_map int _ val _); auto.
(* --todo: should be rewrite read_map. *)
intros Evy. subst vy.
xapps. xif ;=> C; inverts Hx' as; try solve [ intros; false ].
{ introv _ _ Ex. xvals~. }
{ rename d0 into d. introv _ _ Nx. sets y: (L[x]).
......@@ -416,24 +421,25 @@ Lemma rule_compress : forall n R p x z,
Proof using.
introv Dx Ez. xcf. xval as F ;=> EF.
unfold UF. xpull ;=> L (Hn&HR).
forwards~ Ix: index_length_eq (rm Dx) Hn.
forwards~ Ix: index_of_index_length' (rm Dx) Hn.
forwards~ Hx: HR x.
applys local_erase. (* TODO: avoid *)
forwards (d&Hx'): reprn_of_repr Hx.
gen L x. induction_wf IH: lt_wf d. hide IH. intros.
rewrite EF. xcf. rewrite <- EF.
xapps. xif ;=> C.
{ xapps~. xapp~. rewrite read_map; auto.
{ xapps~. xapp~. rewrite (@read_map int _ val _); auto.
(* --todo: should be rewrite read_map. *)
inverts Hx' as; try solve [ intros; false ].
introv _ Nx Ry. sets y: (L[x]). rename d0 into d.
forwards~ ER: roots_inv_R y (R x) HR.
rewrite <- update_map; auto.
rewrite <- map_update; auto.
sets_eq L': (L[x:=z]).
forwards~ (I1&I2&K1&K2): udpate_inv L' L x z.
subst z. forwards~ HR': roots_compress L' HR.
forwards~ Hy: HR' y.
xapp~ (>> IH d).
{ subst L'. rew_arr~. }
{ subst L'. rew_array~. }
{ applys~ roots_compress' HR. }
{ hsimpl~. } }
{ xvals~. }
......@@ -487,11 +493,11 @@ Lemma rule_union : forall n R p x y,
Proof using.
introv Dx Dy. xcf. xapps~. xapps~. xapps. xif ;=> C.
{ unfold UF. xpull ;=> L (Hn&HR).
forwards~ Ix: index_length_eq (rm Dx) Hn.
forwards~ Iy: index_length_eq (rm Dy) Hn.
forwards~ Ix: index_of_index_length' (rm Dx) Hn.
forwards~ Iy: index_of_index_length' (rm Dy) Hn.
xapp~. (* todo: xapps does not do the right thing *)
{ hpull ;=> r Er. rewrite~ <- update_map; auto.
hsimpl~. rew_arr~. split~.
{ hpull ;=> r Er. rewrite~ <- map_update; auto.
hsimpl~. rew_array~. split~.
{ applys~ roots_link L R x y. } } }
{ xvals~. rewrite~ link_related. }
Qed.
......
model/LambdaCFLifted.v
View file @ 443ed16c
......@@ -168,7 +168,7 @@ Proof using.
destruct t; fequals.
{ fequals~. }
{ fequals~. }
{ fequals~. applys~ fun_ext_dep_3. }
{ fequals~. applys~ fun_ext_3. }
{ fequals~. }
{ destruct t1; fequals~. destruct v0; fequals~.
destruct t2; fequals~. destruct v0; fequals~.
......@@ -454,13 +454,13 @@ Hint Extern 1 (Register_Spec (val_prim val_ptr_add)) => Provide Rule_ptr_add.
(* ** [hsimpl] and [xpull] cleanup of boolean reflection *)
Ltac hsimpl_post_before_generalize tt ::=
autorewrite with rew_isTrue.
autorewrite with rew_bool_eq.
Ltac himpl_post_processing_for_hyp H ::=
autorewrite with rew_isTrue in H.
autorewrite with rew_bool_eq in H.
Ltac xpull_post_processing_for_hyp H ::=
autorewrite with rew_isTrue in H.
autorewrite with rew_bool_eq in H.
(*--------------------------------------------------------*)
......
model/LambdaSepLifted.v
View file @ 443ed16c
......@@ -689,7 +689,7 @@ Lemma Rule_alloc_nat : forall (n:nat),
(fun l => \[l <> null] \* Alloc n l).
Proof using.
intros. xapplys~ Rule_alloc. { math. }
{ intros. rewrite abs_pos_nat. hsimpl. }
{ intros. rewrite abs_nat. hsimpl. }
Qed.
Lemma Rule_eq_val : forall v1 v2,
......
model/LambdaSepRO.v
View file @ 443ed16c
......@@ -22,12 +22,12 @@ Arguments exist [A] [P].
(* ---------------------------------------------------------------------- *)
(* TODO: merge into TLC *)
(* --TODO: merge into TLC *)
Ltac fequal_base ::=
let go := f_equal_fixed; [ fequal_base | ] in
match goal with
| |- exist _ _ = exist _ _ => apply exist_eq
| |- exist _ _ = exist _ _ => apply exist_eq_exist
| |- (_,_,_) = (_,_,_) => go
| |- (_,_,_,_) = (_,_,_,_) => go
| |- (_,_,_,_,_) = (_,_,_,_,_) => go
......@@ -222,7 +222,7 @@ Lemma heap_union_def : forall h1 h2,
h1 \u h2 = exist (h1^f \+ h2^f, h1^r \+ h2^r) D.
Proof using.
introv M. unfold heap_union.
rewrite (classicT_left M). esplit. destruct~ M.
rewrite (classicT_l M). esplit. destruct~ M.
Qed.
Lemma heap_union_spec : forall h1 h2,
......@@ -237,7 +237,7 @@ Lemma heap_union_f : forall h1 h2,
heap_compat h1 h2 ->
(h1 \u h2)^f = h1^f \+ h2^f.
Proof using.
introv D. unfold heap_union. rewrite (classicT_left D).
introv D. unfold heap_union. rewrite (classicT_l D).
destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2).
unstate. fmap_eq.
Qed.
......@@ -246,7 +246,7 @@ Lemma heap_union_r : forall h1 h2,
heap_compat h1 h2 ->
(h1 \u h2)^r = h1^r \+ h2^r.
Proof using.
introv D. unfold heap_union. rewrite (classicT_left D).
introv D. unfold heap_union. rewrite (classicT_l D).
destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2).
unstate. fmap_eq.
Qed.
......@@ -391,7 +391,7 @@ Lemma heap_union_empty_l : forall h,
heap_empty \u h = h.
Proof using.
intros h. unfold heap_union.
rewrite (classicT_left (heap_compat_empty_l h)).
rewrite (classicT_l (heap_compat_empty_l h)).
destruct h as ((f,r)&D). simpl.
fequals_rec; fmap_eq.
Qed.
......@@ -406,7 +406,7 @@ Lemma heap_union_state : forall h1 h2,
heap_compat h1 h2 ->
heap_state (h1 \u h2) = heap_state h1 \+ heap_state h2.
Proof using.
introv D. unfold heap_union. rewrite (classicT_left D).
introv D. unfold heap_union. rewrite (classicT_l D).
destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2).
unstate. fmap_eq.
Qed.
......
model/LambdaStructLifted.v
View file @ 443ed16c
......@@ -137,7 +137,7 @@ Lemma Rule_neq : forall `{EA:Enc A} (v1 v2:A),
Proof using.
intros. xcf.
xapps~. (* Details: xlet. xapp~.xpull ;=> X E. subst. *)
xapps. isubst. hsimpl. rew_refl~.
xapps. isubst. hsimpl. rew_isTrue~.
Qed.
Hint Extern 1 (Register_Spec val_neq) => Provide Rule_neq.
......@@ -164,7 +164,7 @@ Fixpoint Record (L:Record_fields) (r:loc) : hprop :=
(* TODO: currently restricted due to [r `.` f ~> V] not ensuring [r<>null] *)
Lemma hRecord_not_null : forall (r:loc) (L:Record_fields),
(* L <> nil -> *)
Mem (0%nat:field) (List.map fst L) ->
mem (0%nat:field) (List.map fst L) ->
(r ~> Record L) ==> (r ~> Record L) \* \[r <> null].
Proof using.
introv M. induction L as [|(f,[A EA v]) L'].
......@@ -278,8 +278,8 @@ Proof using.
destruct vo as [[T ET v]|]; inverts M. intros r.
induction L as [|[F D] L']; [false|].
destruct D as [A EA V]. simpl in E.
xunfold Record at 1. xunfold Record at 2. case_if.
{ inverts E. xapplys~ Rule_get_field. }
xunfold Record at 1. xunfold Record at 2. case_if. (*--todo fix subst *)
{ subst. inverts E. xapplys~ Rule_get_field. }
{ specializes IHL' (rm E). xapplys~ IHL'. }
Qed.
......@@ -311,9 +311,9 @@ Proof using.
destruct do as [L'|]; inverts M.
gen L'. induction L as [|[f' D] T]; intros; [false|].
destruct D as [A' EA' V]. simpl in E.
xunfold Record at 1. simpl. case_if.
{ inverts E. xapply~ Rule_set_field. intros _. xunfold Record at 2. simpl. hsimpl. }
{ cases (record_set_compute_dyn f (Dyn W) T) as C; [|false].
xunfold Record at 1. simpl. case_if. (*--todo fix subst *)
{ subst. inverts E. xapply~ Rule_set_field. intros _. xunfold Record at 2. simpl. hsimpl. }
{ cases (record_set_compute_dyn f (Dyn W) T) as C'; [|false].
inverts E. specializes~ IHT r. xapply IHT. hsimpl.
intros. xunfold Record at 2. simpl. hsimpl~. }
Qed.
......@@ -474,7 +474,7 @@ Proof using.
destruct n' as [|n'']. { inverts Exs. } simpl in Exs.
invert Exs. intros Ei Exs'. subst i. rewrite <- Exs'.
asserts N: (x <> n). { math. }
rewrite Substs_cons. rewrite combine_cons. rew_list.
rewrite Substs_cons. rewrite combine_cons. rew_listx.
rewrite Subst_seq.
asserts_rewrite (Subst x V (val_set_field x (trm_var n) (trm_var x))
= val_set_field x (trm_var n) (enc V)).
......
model/Makefile
View file @ 443ed16c
......@@ -16,7 +16,7 @@ SRC := $(shell cat FILES)
ifeq ($(ARTHUR),1)
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleBasic ExampleList ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
endif
PWD := $(shell pwd)
......
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