From 443ed16cd59de7e25ac0a9e8ab4e3b4ae5f38c4a Mon Sep 17 00:00:00 2001 From: charguer Date: Fri, 1 Dec 2017 18:36:56 +0100 Subject: [PATCH] compile --- model/ExampleList.v | 2 +- model/ExampleListNonlifted.v | 14 +++++++------- model/ExampleTrees.v | 14 ++++++++++++-- model/ExampleUnionFind.v | 28 +++++++++++++++++----------- model/LambdaCFLifted.v | 8 ++++---- model/LambdaSepLifted.v | 2 +- model/LambdaSepRO.v | 14 +++++++------- model/LambdaStructLifted.v | 16 ++++++++-------- model/Makefile | 2 +- 9 files changed, 58 insertions(+), 42 deletions(-) diff --git a/model/ExampleList.v b/model/ExampleList.v index a569890..c4600aa 100644 --- a/model/ExampleList.v +++ b/model/ExampleList.v @@ -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. diff --git a/model/ExampleListNonlifted.v b/model/ExampleListNonlifted.v index 4f79a31..b5c5b52 100644 --- a/model/ExampleListNonlifted.v +++ b/model/ExampleListNonlifted.v @@ -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'. diff --git a/model/ExampleTrees.v b/model/ExampleTrees.v index 6001e8e..3a1538c 100644 --- a/model/ExampleTrees.v +++ b/model/ExampleTrees.v @@ -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) ]. diff --git a/model/ExampleUnionFind.v b/model/ExampleUnionFind.v index 99214e1..c245fe4 100644 --- a/model/ExampleUnionFind.v +++ b/model/ExampleUnionFind.v @@ -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. diff --git a/model/LambdaCFLifted.v b/model/LambdaCFLifted.v index b1b2a68..8d47659 100644 --- a/model/LambdaCFLifted.v +++ b/model/LambdaCFLifted.v @@ -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. (*--------------------------------------------------------*) diff --git a/model/LambdaSepLifted.v b/model/LambdaSepLifted.v index 2bbff8b..5c05c66 100644 --- a/model/LambdaSepLifted.v +++ b/model/LambdaSepLifted.v @@ -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, diff --git a/model/LambdaSepRO.v b/model/LambdaSepRO.v index 3ad9646..529b61b 100644 --- a/model/LambdaSepRO.v +++ b/model/LambdaSepRO.v @@ -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. diff --git a/model/LambdaStructLifted.v b/model/LambdaStructLifted.v index eec389e..a2c4e66 100644 --- a/model/LambdaStructLifted.v +++ b/model/LambdaStructLifted.v @@ -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)). diff --git a/model/Makefile b/model/Makefile index 1113096..a604d16 100644 --- a/model/Makefile +++ b/model/Makefile @@ -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) -- GitLab