diff --git a/model/FILES b/model/FILES index 7626e535c8eb47afc1e8e0c46a1a23a396c2754d..d3d215a64c7666e872bd98c27a052f53b31d91e5 100644 --- a/model/FILES +++ b/model/FILES @@ -1,4 +1,4 @@ -LibState +Fmap LambdaSemantics SepFunctor LambdaSep diff --git a/model/Fmap.v b/model/Fmap.v new file mode 100644 index 0000000000000000000000000000000000000000..9f7623b8e7db2da5332efd67bba179f4dba81b05 --- /dev/null +++ b/model/Fmap.v @@ -0,0 +1,792 @@ +(** + +This file contains a representation of finite maps +that may be used for representing a store. It also +provides lemmas and tactics for reasoning about +operations on the store (read, write, union). + +Author: Arthur Charguéraud. +License: MIT. + +*) + +Set Implicit Arguments. +Require Import LibCore. + + +(* ********************************************************************** *) + +Tactic Notation "cases" constr(E) := (* TODO For TLC *) + let H := fresh "Eq" in cases E as H. + + +(* ********************************************************************** *) +(** * Fresh locations *) + +(* ---------------------------------------------------------------------- *) +(** ** Existence of fresh locations *) + +(** These lemmas are useful to prove: + [forall h v, exists l, fmap_disjoint (fmap_single l v) h]. *) + +Definition loc_fresh_gen (L : list nat) := + (1 + fold_right plus O L)%nat. + +Lemma loc_fresh_ind : forall x L, + Mem x L -> + (x < loc_fresh_gen L)%nat. +Proof using. + intros x L. unfold loc_fresh_gen. + induction L; introv M; inverts M; rew_list. + { math. } + { forwards~: IHL. math. } +Qed. + +Definition loc_fresh_property (A:Type) := + forall (L:list A), exists (x:A), ~ Mem x L. + +Lemma loc_fresh_nat : loc_fresh_property nat. +Proof using. + intros L. exists (loc_fresh_gen L). intros M. + lets: loc_fresh_ind M. math. +Qed. + +Hint Resolve loc_fresh_nat. + + +(* ********************************************************************** *) +(** * Maps (partial functions) *) + +(* ---------------------------------------------------------------------- *) +(* ** Representation *) + +(** Type of partial functions from A to B *) + +Definition map (A B : Type) : Type := + A -> option B. + + +(* ---------------------------------------------------------------------- *) +(* ** Operations *) + +(** Disjoint union of two partial functions *) + +Definition map_union (A B : Type) (f1 f2 : map A B) : map A B := + fun (x:A) => match f1 x with + | Some y => Some y + | None => f2 x + end. + +(** Finite domain of a partial function *) + +Definition map_finite (A B : Type) (f : map A B) := + exists (L : list A), forall (x:A), f x <> None -> Mem x L. + +(** Disjointness of domain of two partial functions *) + +Definition map_disjoint (A B : Type) (f1 f2 : map A B) := + forall (x:A), f1 x = None \/ f2 x = None. + +(** Compatibility of two partial functions on the intersection + of their domains *) + +Definition map_agree (A B : Type) (f1 f2 : map A B) := + forall x v1 v2, + f1 x = Some v1 -> + f2 x = Some v2 -> + v1 = v2. + + +(* ---------------------------------------------------------------------- *) +(** Properties *) + +Section MapOps. +Variables (A B : Type). +Implicit Types f : map A B. + +(** Symmetry of disjointness *) + +Lemma map_disjoint_sym : + sym (@map_disjoint A B). +Proof using. + introv H. unfolds map_disjoint. intros z. specializes H z. intuition. +Qed. + +(** Commutativity of disjoint union *) + +Lemma map_union_comm : forall f1 f2, + map_disjoint f1 f2 -> + map_union f1 f2 = map_union f2 f1. +Proof using. + introv H. unfold map. + extens. intros x. unfolds map_disjoint, map_union. + specializes H x. cases (f1 x); cases (f2 x); auto. destruct H; false. +Qed. + +(** Finiteness of union *) + +Lemma map_union_finite : forall f1 f2, + map_finite f1 -> + map_finite f2 -> + map_finite (map_union f1 f2). +Proof using. + introv [L1 F1] [L2 F2]. exists (L1 ++ L2). introv M. + specializes F1 x. specializes F2 x. unfold map_union in M. + apply Mem_app_or. destruct~ (f1 x). +Qed. + +End MapOps. + + +(* ********************************************************************** *) +(** * Finite maps *) + +(* ---------------------------------------------------------------------- *) +(** Definitions *) + +Inductive fmap (A B : Type) : Type := fmap_make { + fmap_data :> map A B; + fmap_finite : map_finite fmap_data }. + +Implicit Arguments fmap_make [A B]. + + +(* ---------------------------------------------------------------------- *) +(** Operations *) + +(** Empty fmap *) + +Program Definition fmap_empty (A B : Type) : fmap A B := + fmap_make (fun l => None) _. +Next Obligation. exists (@nil A). auto_false. Qed. + +Implicit Arguments fmap_empty [[A] [B]]. + +(** Singleton fmap *) + +Program Definition fmap_single A B (x:A) (v:B) : fmap A B := + fmap_make (fun x' => If x = x' then Some v else None) _. +Next Obligation. + exists (x::nil). intros. case_if. subst~. +Qed. + +(** Union of fmaps *) + +Program Definition fmap_union A B (h1 h2:fmap A B) : fmap A B := + fmap_make (map_union h1 h2) _. +Next Obligation. destruct h1. destruct h2. apply~ map_union_finite. Qed. + +Notation "h1 \+ h2" := (fmap_union h1 h2) + (at level 51, right associativity) : fmap_scope. + +Open Scope fmap_scope. + +(** Update of a fmap *) + +Definition fmap_update A B (h:fmap A B) (x:A) (v:B) := + fmap_union (fmap_single x v) h. + (* Note: the union operation first reads in the first argument. *) + + +(* ---------------------------------------------------------------------- *) +(** Properties *) + +(** Inhabited type [fmap] *) + +Global Instance Inhab_fmap A B : Inhab (fmap A B). +Proof using. intros. applys prove_Inhab (@fmap_empty A B). Qed. + +(** Compatible fmaps *) + +Definition fmap_agree A B (h1 h2:fmap A B) := + map_agree h1 h2. + +(** Disjoint fmaps *) + +Definition fmap_disjoint A B (h1 h2 : fmap A B) : Prop := + map_disjoint h1 h2. + +Notation "\# h1 h2" := (fmap_disjoint h1 h2) + (at level 40, h1 at level 0, h2 at level 0, no associativity) : fmap_scope. + +(** Three disjoint fmaps *) + +Definition fmap_disjoint_3 A B (h1 h2 h3 : fmap A B) := + fmap_disjoint h1 h2 + /\ fmap_disjoint h2 h3 + /\ fmap_disjoint h1 h3. + +Notation "\# h1 h2 h3" := (fmap_disjoint_3 h1 h2 h3) + (at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity) + : fmap_scope. + + + +(* ********************************************************************** *) +(* * Lemmas about Fmap *) + +Section FmapProp. +Variables (A B : Type). +Implicit Types f g h : fmap A B. + +(* ---------------------------------------------------------------------- *) +(* ** Equality *) + +Lemma fmap_eq : forall (f1 f2:map A B) F1 F2, + (forall x, f1 x = f2 x) -> + fmap_make f1 F1 = fmap_make f2 F2. +Proof using. + introv H. asserts: (f1 = f2). { unfold map. extens~. } + subst. fequals. (* note: involves proof irrelevance *) +Qed. + + +(* ---------------------------------------------------------------------- *) +(* ** Disjointness *) + +Lemma fmap_disjoint_sym : forall h1 h2, + \# h1 h2 -> \# h2 h1. +Proof using. intros [f1 F1] [f2 F2]. apply map_disjoint_sym. Qed. + +Lemma fmap_disjoint_comm : forall h1 h2, + \# h1 h2 = \# h2 h1. +Proof using. lets: fmap_disjoint_sym. extens*. Qed. + +Lemma fmap_disjoint_empty_l : forall h, + \# fmap_empty h. +Proof using. intros [f F] x. simple~. Qed. + +Lemma fmap_disjoint_empty_r : forall h, + \# h fmap_empty. +Proof using. intros [f F] x. simple~. Qed. + +Hint Resolve fmap_disjoint_sym fmap_disjoint_empty_l fmap_disjoint_empty_r. + +Lemma fmap_disjoint_union_eq_r : forall h1 h2 h3, + \# h1 (h2 \+ h3) = + (\# h1 h2 /\ \# h1 h3). +Proof using. + intros [f1 F1] [f2 F2] [f3 F3]. + unfolds fmap_disjoint, fmap_union. simpls. + unfolds map_disjoint, map_union. extens. iff M [M1 M2]. + split; intros x; specializes M x; + destruct (f2 x); intuition; tryfalse. + intros x. specializes M1 x. specializes M2 x. + destruct (f2 x); intuition. +Qed. + +Lemma fmap_disjoint_union_eq_l : forall h1 h2 h3, + \# (h2 \+ h3) h1 = + (\# h1 h2 /\ \# h1 h3). +Proof using. + intros. rewrite fmap_disjoint_comm. + apply fmap_disjoint_union_eq_r. +Qed. + +Lemma fmap_single_same_loc_disjoint : forall (x:A) (v1 v2:B), + \# (fmap_single x v1) (fmap_single x v2) -> False. +Proof using. + introv D. specializes D x. simpls. case_if. destruct D; tryfalse. +Qed. + +Lemma fmap_disjoint_3_unfold : forall h1 h2 h3, + \# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3). +Proof using. auto. Qed. + +Lemma fmap_disjoint_new : forall null h v, + loc_fresh_property A -> + exists l, \# (fmap_single l v) h /\ l <> null. +Proof using. + intros null (m&(L&M)) v HF. + unfold fmap_disjoint, map_disjoint. simpl. + lets (l&F): (HF (null::L)). + exists l. split. + { intros l'. case_if~. + { right. applys not_not_elim. intros H. applys F. + constructor. applys~ M. } } + { intro_subst. applys~ F. } +Qed. + +Lemma fmap_disjoint_single_set : forall h l v1 v2, + \# (fmap_single l v1) h -> + \# (fmap_single l v2) h. +Proof using. + introv M. unfolds fmap_disjoint, fmap_single, map_disjoint; simpls. + intros l'. specializes M l'. case_if~. destruct M; auto_false. +Qed. + + +(* ---------------------------------------------------------------------- *) +(* ** Union *) + +Lemma fmap_union_idempotent : forall h, + h \+ h = h. +Proof using. + intros [f F]. apply~ fmap_eq. simpl. intros x. + unfold map_union. cases~ (f x). +Qed. + +Lemma fmap_union_empty_l : forall h, + fmap_empty \+ h = h. +Proof using. + intros [f F]. unfold fmap_union, map_union, fmap_empty. simpl. + apply~ fmap_eq. +Qed. + +Lemma fmap_union_empty_r : forall h, + h \+ fmap_empty = h. +Proof using. + intros [f F]. unfold fmap_union, map_union, fmap_empty. simpl. + apply fmap_eq. intros x. destruct~ (f x). +Qed. + +Lemma fmap_union_eq_empty_inv_l : forall h1 h2, + h1 \+ h2 = fmap_empty -> + h1 = fmap_empty. +Proof using. + intros (f1&F1) (f2&F2) M. inverts M as M. + applys fmap_eq. intros l. + unfolds map_union. + lets: func_same_1 l M. + cases (f1 l); auto_false. +Qed. + +Lemma fmap_union_eq_empty_inv_r : forall h1 h2, + h1 \+ h2 = fmap_empty -> + h2 = fmap_empty. +Proof using. + intros (f1&F1) (f2&F2) M. inverts M as M. + applys fmap_eq. intros l. + unfolds map_union. + lets: func_same_1 l M. + cases (f1 l); auto_false. +Qed. + +Lemma fmap_union_comm_disjoint : forall h1 h2, + \# h1 h2 -> + h1 \+ h2 = h2 \+ h1. +Proof using. + intros [f1 F1] [f2 F2] H. simpls. apply fmap_eq. simpl. + intros. rewrite~ map_union_comm. +Qed. + +Lemma fmap_union_comm_agree : forall h1 h2, + fmap_agree h1 h2 -> + h1 \+ h2 = h2 \+ h1. +Proof using. + intros [f1 F1] [f2 F2] H. simpls. apply fmap_eq. simpl. + intros l. specializes H l. unfolds map_union. simpls. + cases (f1 l); cases (f2 l); auto. fequals. applys* H. +Qed. + +Lemma fmap_union_assoc : forall h1 h2 h3, + (h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3). +Proof using. + intros [f1 F1] [f2 F2] [f3 F3]. unfolds fmap_union. simpls. + apply fmap_eq. intros x. unfold map_union. destruct~ (f1 x). +Qed. + +Lemma map_eq_forward : forall h1 h2, + h1 = h2 -> + forall x, fmap_data h1 x = fmap_data h2 x. +Proof using. intros. fequals. Qed. + +(* +Lemma fmap_union_eq_inv : forall h2 h1 h1' : fmap, + \# h1 h2 -> + fmap_agree h1' h2 -> + h1 \+ h2 = h1' \+ h2 -> + h1 = h1'. +Proof using. + intros [f2 F2] [f1 F1] [f1' F1'] D D' E. + applys fmap_eq. intros x. specializes D x. specializes D' x. + lets E': map_eq_forward (rm E) x. simpls. + unfolds map_union. + cases (f1 x); cases (f2 x); try solve [cases (f1' x); destruct D; congruence ]. + destruct D; try false. + rewrite H in E'. inverts E'. + cases (f1' x); cases (f1 x); + destruct D; try congruence. + false. + destruct D'; try congruence. +Qed. +*) + +Lemma fmap_union_eq_inv : forall h2 h1 h1', + \# h1 h2 -> + \# h1' h2 -> + h1 \+ h2 = h1' \+ h2 -> + h1 = h1'. +Proof using. + intros [f2 F2] [f1' F1'] [f1 F1] D D' E. + applys fmap_eq. intros x. specializes D x. specializes D' x. + lets E': map_eq_forward (rm E) x. simpls. + unfolds map_union. + cases (f1' x); cases (f1 x); + destruct D; try congruence; + destruct D'; try congruence. +Qed. + + +(* ---------------------------------------------------------------------- *) +(* ** Compatibility *) + +Lemma fmap_agree_refl : forall h, + fmap_agree h h. +Proof using. + intros h. introv M1 M2. congruence. +Qed. + +Lemma fmap_agree_sym : forall f1 f2, + fmap_agree f1 f2 -> + fmap_agree f2 f1. +Proof using. + introv M. intros l v1 v2 E1 E2. + specializes M l E1. +Qed. + +Lemma fmap_agree_disjoint : forall h1 h2, + fmap_disjoint h1 h2 -> + fmap_agree h1 h2. +Proof using. + introv HD. intros l v1 v2 M1 M2. destruct (HD l); false. +Qed. + +Lemma fmap_agree_empty_l : forall h, + fmap_agree fmap_empty h. +Proof using. intros h l v1 v2 E1 E2. simpls. false. Qed. + +Lemma fmap_agree_empty_r : forall h, + fmap_agree h fmap_empty. +Proof using. + hint fmap_agree_sym, fmap_agree_empty_l. eauto. +Qed. + +Lemma fmap_agree_union_l : forall f1 f2 f3, + fmap_agree f1 f3 -> + fmap_agree f2 f3 -> + fmap_agree (f1 \+ f2) f3. +Proof using. + introv M1 M2. intros l v1 v2 E1 E2. + specializes M1 l. specializes M2 l. + simpls. unfolds map_union. cases (fmap_data f1 l). + { inverts E1. applys* M1. } + { applys* M2. } +Qed. + +Lemma fmap_agree_union_r : forall f1 f2 f3, + fmap_agree f1 f2 -> + fmap_agree f1 f3 -> + fmap_agree f1 (f2 \+ f3). +Proof using. + hint fmap_agree_sym, fmap_agree_union_l. eauto. +Qed. + +Lemma fmap_agree_union_lr : forall f1 g1 f2 g2, + fmap_agree g1 g2 -> + \# f1 f2 (g1 \+ g2) -> + fmap_agree (f1 \+ g1) (f2 \+ g2). +Proof using. + introv M1 (M2a&M2b&M2c). + rewrite fmap_disjoint_union_eq_r in *. + applys fmap_agree_union_l; applys fmap_agree_union_r; + try solve [ applys* fmap_agree_disjoint ]. + auto. +Qed. + +Lemma fmap_agree_union_ll_inv : forall f1 f2 f3, + fmap_agree (f1 \+ f2) f3 -> + fmap_agree f1 f3. +Proof using. + introv M. intros l v1 v2 E1 E2. + specializes M l. simpls. unfolds map_union. + rewrite E1 in M. applys* M. +Qed. + +Lemma fmap_agree_union_rl_inv : forall f1 f2 f3, + fmap_agree f1 (f2 \+ f3) -> + fmap_agree f1 f2. +Proof using. + hint fmap_agree_union_ll_inv, fmap_agree_sym. eauto. +Qed. + +Lemma fmap_agree_union_lr_inv_agree_agree : forall f1 f2 f3, + fmap_agree (f1 \+ f2) f3 -> + fmap_agree f1 f2 -> + fmap_agree f2 f3. +Proof using. + introv M D. rewrite~ (@fmap_union_comm_agree f1 f2) in M. + applys* fmap_agree_union_ll_inv. +Qed. + +Lemma fmap_agree_union_rr_inv_agree : forall f1 f2 f3, + fmap_agree f1 (f2 \+ f3) -> + fmap_agree f2 f3 -> + fmap_agree f1 f3. +Proof using. + hint fmap_agree_union_lr_inv_agree_agree, fmap_agree_sym. eauto. +Qed. + +Lemma fmap_agree_union_l_inv : forall f1 f2 f3, + fmap_agree (f1 \+ f2) f3 -> + fmap_agree f1 f2 -> + fmap_agree f1 f3 + /\ fmap_agree f2 f3. +Proof using. + (* TODO: proofs redundant with others above *) + introv M2 M1. split. + { intros l v1 v2 E1 E2. + specializes M1 l v1 v2 E1. applys~ M2 l v1 v2. + unfold fmap_union, map_union; simpl. rewrite~ E1. } + { intros l v1 v2 E1 E2. + specializes M1 l. specializes M2 l. + unfolds fmap_union, map_union; simpls. + cases (fmap_data f1 l). (* LATER: name b *) + { applys eq_trans b. symmetry. applys~ M1. applys~ M2. } + { auto. } } +Qed. + +Lemma fmap_agree_union_r_inv : forall f1 f2 f3, + fmap_agree f1 (f2 \+ f3) -> + fmap_agree f2 f3 -> + fmap_agree f1 f2 + /\ fmap_agree f1 f3. +Proof using. + hint fmap_agree_sym. + intros. forwards~ (M1&M2): fmap_agree_union_l_inv f2 f3 f1. +Qed. + + +(* ---------------------------------------------------------------------- *) +(* ** Read and write *) + +Lemma fmap_union_single_read : forall f1 f2 l v, + f1 = fmap_single l v -> + fmap_data (f1 \+ f2) l = Some v. +Proof using. + intros. subst. simpl. unfold map_union. case_if~. +Qed. + +Lemma fmap_union_single_write : forall f1 f1' f2 l v v', + f1 = fmap_single l v -> + f1' = fmap_single l v' -> + (f1' \+ f2) = fmap_update (f1 \+ f2) l v'. +Proof using. + intros. subst. unfold fmap_update. + rewrite <- fmap_union_assoc. fequals. + applys fmap_eq. intros l'. + unfolds map_union, fmap_single; simpl. case_if~. +Qed. + +End FmapProp. + +Implicit Arguments fmap_union_assoc [A B]. +Implicit Arguments fmap_union_comm_disjoint [A B]. +Implicit Arguments fmap_union_comm_agree [A B]. + + +(* ********************************************************************** *) +(* * Tactics *) + +(* ---------------------------------------------------------------------- *) +(* ** Tactic [fmap_disjoint] for proving disjointness results *) + +(** [fmap_disjoint] proves goals of the form [\# h1 h2] and + [\# h1 h2 h3] by expanding all hypotheses into binary forms + [\# h1 h2] and then exploiting symmetry and disjointness + with [fmap_empty]. *) + +Hint Resolve fmap_disjoint_sym fmap_disjoint_empty_l fmap_disjoint_empty_r. + +Hint Rewrite + fmap_disjoint_union_eq_l + fmap_disjoint_union_eq_r + fmap_disjoint_3_unfold : rew_disjoint. + +Tactic Notation "rew_disjoint" := + autorewrite with rew_disjoint in *. +Tactic Notation "rew_disjoint" "*" := + rew_disjoint; auto_star. + +Tactic Notation "fmap_disjoint" := + solve [ subst; rew_disjoint; jauto_set; auto ]. + +Tactic Notation "fmap_disjoint_if_needed" := + match goal with + | |- \# _ _ => fmap_disjoint + | |- \# _ _ _ => fmap_disjoint + end. + +Lemma fmap_disjoint_demo : forall A B (h1 h2 h3 h4 h5:fmap A B), + h1 = h2 \+ h3 -> + \# h2 h3 -> + \# h1 h4 h5 -> + \# h3 h2 h5 /\ \# h4 h5. +Proof using. + intros. dup 2. + { subst. rew_disjoint. jauto_set. auto. auto. auto. auto. } + { fmap_disjoint. } +Qed. + + +(* ---------------------------------------------------------------------- *) +(* ** Tactic [fmap_eq] for proving equality of fmaps, + and tactic [rew_fmap] to normalize fmap expressions. *) + +Section StateEq. +Variables (A B : Type). +Implicit Types h : fmap A B. + +(** [fmap_eq] proves equalities between unions of fmaps. + It attempts to discharge the disjointness side-conditions. + Disclaimer: cancels heaps at depth up to 4, but no more. *) + +Lemma fmap_union_eq_cancel_1 : forall h1 h2 h2', + h2 = h2' -> + h1 \+ h2 = h1 \+ h2'. +Proof using. intros. subst. auto. Qed. + +Lemma fmap_union_eq_cancel_1' : forall h1, + h1 = h1. +Proof using. intros. auto. Qed. + +Lemma fmap_union_eq_cancel_2 : forall h1 h1' h2 h2', + \# h1 h1' -> + h2 = h1' \+ h2' -> + h1 \+ h2 = h1' \+ h1 \+ h2'. +Proof using. + intros. subst. rewrite <- fmap_union_assoc. + rewrite (fmap_union_comm_disjoint h1 h1'). + rewrite~ fmap_union_assoc. auto. +Qed. + +Lemma fmap_union_eq_cancel_2' : forall h1 h1' h2, + \# h1 h1' -> + h2 = h1' -> + h1 \+ h2 = h1' \+ h1. +Proof using. + intros. subst. apply~ fmap_union_comm_disjoint. +Qed. + +Lemma fmap_union_eq_cancel_3 : forall h1 h1' h2 h2' h3', + \# h1 (h1' \+ h2') -> + h2 = h1' \+ h2' \+ h3' -> + h1 \+ h2 = h1' \+ h2' \+ h1 \+ h3'. +Proof using. + intros. subst. + rewrite <- (fmap_union_assoc h1' h2' h3'). + rewrite <- (fmap_union_assoc h1' h2' (h1 \+ h3')). + apply~ fmap_union_eq_cancel_2. +Qed. + +Lemma fmap_union_eq_cancel_3' : forall h1 h1' h2 h2', + \# h1 (h1' \+ h2') -> + h2 = h1' \+ h2' -> + h1 \+ h2 = h1' \+ h2' \+ h1. +Proof using. + intros. subst. + rewrite <- (fmap_union_assoc h1' h2' h1). + apply~ fmap_union_eq_cancel_2'. +Qed. + +Lemma fmap_union_eq_cancel_4 : forall h1 h1' h2 h2' h3' h4', + \# h1 ((h1' \+ h2') \+ h3') -> + h2 = h1' \+ h2' \+ h3' \+ h4' -> + h1 \+ h2 = h1' \+ h2' \+ h3' \+ h1 \+ h4'. +Proof using. + intros. subst. + rewrite <- (fmap_union_assoc h1' h2' (h3' \+ h4')). + rewrite <- (fmap_union_assoc h1' h2' (h3' \+ h1 \+ h4')). + apply~ fmap_union_eq_cancel_3. +Qed. + +Lemma fmap_union_eq_cancel_4' : forall h1 h1' h2 h2' h3', + \# h1 (h1' \+ h2' \+ h3') -> + h2 = h1' \+ h2' \+ h3' -> + h1 \+ h2 = h1' \+ h2' \+ h3' \+ h1. +Proof using. + intros. subst. + rewrite <- (fmap_union_assoc h2' h3' h1). + apply~ fmap_union_eq_cancel_3'. +Qed. + +End StateEq. + +Hint Rewrite + fmap_union_assoc + fmap_union_empty_l + fmap_union_empty_r : rew_fmap. + +Tactic Notation "rew_fmap" := + autorewrite with rew_fmap in *. + +Tactic Notation "rew_fmap" "~" := + rew_fmap; auto_tilde. + +Tactic Notation "rew_fmap" "*" := + rew_fmap; auto_star. + +Ltac fmap_eq_step tt := + match goal with | |- ?G => match G with + | ?h1 = ?h1 => apply fmap_union_eq_cancel_1' + | ?h1 \+ ?h2 = ?h1 \+ ?h2' => apply fmap_union_eq_cancel_1 + | ?h1 \+ ?h2 = ?h1' \+ ?h1 => apply fmap_union_eq_cancel_2' + | ?h1 \+ ?h2 = ?h1' \+ ?h1 \+ ?h2' => apply fmap_union_eq_cancel_2 + | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h1 => apply fmap_union_eq_cancel_3' + | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h1 \+ ?h3' => apply fmap_union_eq_cancel_3 + | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h3' \+ ?h1 => apply fmap_union_eq_cancel_4' + | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h3' \+ ?h1 \+ ?h4' => apply fmap_union_eq_cancel_4 + end end. + +Tactic Notation "fmap_eq" := + subst; + rew_fmap; + repeat (fmap_eq_step tt); + try fmap_disjoint_if_needed. + +Tactic Notation "fmap_eq" "~" := + fmap_eq; auto_tilde. + +Tactic Notation "fmap_eq" "*" := + fmap_eq; auto_star. + +Lemma fmap_eq_demo : forall A B (h1 h2 h3 h4 h5:fmap A B), + \# h1 h2 h3 -> + \# (h1 \+ h2 \+ h3) h4 h5 -> + h1 = h2 \+ h3 -> + h4 \+ h1 \+ h5 = h2 \+ h5 \+ h4 \+ h3. +Proof using. + intros. dup 2. + { subst. rew_fmap. + fmap_eq_step tt. fmap_disjoint. + fmap_eq_step tt. + fmap_eq_step tt. fmap_disjoint. auto. } + { fmap_eq. } +Qed. + + +(* ---------------------------------------------------------------------- *) +(* ** Tactic [fmap_red] for proving [red] goals + (reduction according to a big-step semantics) + modulo equalities between fmaps *) + +(** [fmap_red] proves a goal of the form [red h1 t h2 v] + using an hypothesis of the shape [red h1' t h2' v], + generating [h1 = h1'] and [h2 = h2'] as subgoals, and + attempting to solve them using the tactic [fmap_red]. *) + +Ltac fmap_red_base tt := fail. +(* Example: +Ltac fmap_red_base tt := + match goal with H: red _ ?t _ _ |- red _ ?t _ _ => + applys_eq H 2 4; try fmap_eq end. +*) + +Tactic Notation "fmap_red" := + fmap_red_base tt. + +Tactic Notation "fmap_red" "~" := + fmap_red; auto_tilde. + +Tactic Notation "fmap_red" "*" := + fmap_red; auto_star. diff --git a/model/LambdaCF.v b/model/LambdaCF.v index ed65b1aad9f4c0b3dc805a3ad859073a3411e7ee..b29535daa71a9c991d7c72f606db3289d676dd80 100644 --- a/model/LambdaCF.v +++ b/model/LambdaCF.v @@ -14,7 +14,7 @@ Require Export LibFix LambdaSep. Open Scope heap_scope. -(********************************************************************) +(* ********************************************************************** *) (* ** Type of a formula *) (** A formula is a binary relation relating a pre-condition @@ -26,7 +26,7 @@ Global Instance formula_inhab : Inhab formula. Proof using. apply (prove_Inhab (fun _ _ => True)). Qed. -(********************************************************************) +(* ********************************************************************** *) (* ** The [local] predicate *) (** Nested applications [local] are redundant *) @@ -56,10 +56,10 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed. Hint Resolve local_is_local. -(********************************************************************) +(* ********************************************************************** *) (* ** Characteristic formula generator *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Input language for the characteristic formula generator, where functions are named by a let-binding. *) @@ -102,7 +102,7 @@ Fixpoint trm_of_Trm (t : Trm) : trm := Coercion trm_of_Trm : Trm >-> trm. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Size function used as measure for the CF generator: it computes the size of a term, where all values counting for one unit, including closures viewed as values. *) @@ -123,7 +123,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of the [app] predicate *) (** The proposition [app f v H Q] asserts that the application @@ -133,7 +133,7 @@ Definition app f v H Q := triple (trm_app f v) H Q. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of CF blocks *) (** These auxiliary definitions give the characteristic formula @@ -160,7 +160,7 @@ Definition cf_fix (F1of : val -> val -> formula) (F2of F) H Q. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Instance of [app] for primitive operations *) Lemma app_ref : forall v, @@ -176,7 +176,7 @@ Lemma app_set : forall w l v, Proof using. applys rule_set. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of the CF generator *) (** The CF generator is a recursive function, defined using the @@ -218,10 +218,10 @@ Ltac simpl_cf := rewrite cf_unfold; unfold cf_def. -(********************************************************************) +(* ********************************************************************** *) (* ** Soundness proof *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Two substitution lemmas for the soundness proof *) Hint Extern 1 (measure Trm_size _ _) => hnf; simpl; math. @@ -248,7 +248,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Soundness of the CF generator *) Lemma cf_local : forall T, diff --git a/model/LambdaCFComplete.v b/model/LambdaCFComplete.v index 242057a1a4f87e3255494f9c4d0408b708f8ef48..fdd5e7292908689199a6ba486ccfc16958f6aefa 100644 --- a/model/LambdaCFComplete.v +++ b/model/LambdaCFComplete.v @@ -1,5 +1,5 @@ -(********************************************************************) +(* ********************************************************************** *) (* ** Completeness proof *) (* TO BE COMPLETED *) @@ -23,7 +23,7 @@ Lemma local_name : forall F (H:hprop) (Q:val->hprop), Proof. introv L M. rewrite L. intros m Hm. exists (= m) \[] Q. splits~. - { exists~ m state_empty. } + { exists~ m fmap_empty. } { intros h. applys himpl_cancel_r. intros h' Hh'. applys~ hprop_gc_intro. } Qed. @@ -71,7 +71,7 @@ Theorem cf_complete_wrt_semantics : forall (T:Trm) m m' v', Proof using. introv H. gen_eq t: (trm_of_Trm T); gen T; induction H; intros T E. { simpl_Trm. simpl_cf. applys local_erase. hnf. - intros m' E. subst. exists~ (state_empty:state) m. } + intros m' E. subst. exists~ (fmap_empty:state) m. } { simpl_Trm. simpl_cf. applys local_erase. hnf. case_if; applys~ IHred. } { simpl_Trm. diff --git a/model/LambdaCFCredits.v b/model/LambdaCFCredits.v index efc3e347cc5fc6a24cdaae889375206e0f3f1c4c..45e0789ac2e43b1a4e2cd6f454b54b181f4144f3 100644 --- a/model/LambdaCFCredits.v +++ b/model/LambdaCFCredits.v @@ -15,7 +15,7 @@ Require Export LibFix LambdaSepCredits. (* MODIFIED FOR CREDITS *) Open Scope heap_scope. -(********************************************************************) +(* ********************************************************************** *) (* ** Type of a formula *) (** A formula is a binary relation relating a pre-condition @@ -27,7 +27,7 @@ Global Instance formula_inhab : Inhab formula. Proof using. apply (prove_Inhab (fun _ _ => True)). Qed. -(********************************************************************) +(* ********************************************************************** *) (* ** The [local] predicate *) @@ -58,10 +58,10 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed. Hint Resolve local_is_local. -(********************************************************************) +(* ********************************************************************** *) (* ** Characteristic formula generator *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Input language for the characteristic formula generator, where functions are named by a let-binding. *) @@ -104,7 +104,7 @@ Fixpoint trm_of_Trm (t : Trm) : trm := Coercion trm_of_Trm : Trm >-> trm. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Size function used as measure for the CF generator: it computes the size of a term, where all values counting for one unit, including closures viewed as values. *) @@ -125,7 +125,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of the [app] predicate *) (** The proposition [app f v H Q] asserts that the application @@ -135,7 +135,7 @@ Definition app f v H Q := triple (trm_app f v) H Q. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of CF blocks *) (** These auxiliary definitions give the characteristic formula @@ -167,7 +167,7 @@ Definition cf_fix (F1of : val -> val -> formula) (F2of F) H Q. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Instance of [app] for primitive operations *) Lemma app_ref : forall v, @@ -183,7 +183,7 @@ Lemma app_set : forall w l v, Proof using. applys rule_set. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of the CF generator *) (** The CF generator is a recursive function, defined using the @@ -225,10 +225,10 @@ Ltac simpl_cf := rewrite cf_unfold; unfold cf_def. -(********************************************************************) +(* ********************************************************************** *) (* ** Soundness proof *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Two substitution lemmas for the soundness proof *) Hint Extern 1 (measure Trm_size _ _) => hnf; simpl; math. @@ -255,7 +255,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Soundness of the CF generator *) Lemma cf_local : forall T, diff --git a/model/LambdaSemantics.v b/model/LambdaSemantics.v index 3a01add0b2d071480286a0e1f39468ae119fc2fc..9f4e6acb94e45dd625a9e0b418de5d9b5634c2a1 100644 --- a/model/LambdaSemantics.v +++ b/model/LambdaSemantics.v @@ -9,10 +9,10 @@ License: MIT. *) Set Implicit Arguments. -Require Export LibCore LibState. +Require Export LibCore Fmap. -(************************************************************) +(* ********************************************************************** *) (* * Source language syntax *) (** Representation of variables and locations *) @@ -66,17 +66,17 @@ with subst_trm (y : var) (w : val) (t : trm) : trm := -(************************************************************) +(* ********************************************************************** *) (* * Source language semantics *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Big-step evaluation *) Section Red. -Definition state := state loc val. +Definition state := fmap loc val. -Local Open Scope state_scope. +Local Open Scope fmap_scope. Coercion val_prim : prim >-> val. Coercion trm_val : val >-> trm. @@ -101,24 +101,24 @@ Inductive red : state -> trm -> state -> val -> Prop := red m1 (trm_app v1 v2) m2 r | red_ref : forall ma mb v l, l <> null -> - mb = (state_single l v) -> + mb = (fmap_single l v) -> \# ma mb -> red ma (prim_ref v) (mb \+ ma) (val_loc l) | red_get : forall m l v, - state_data m l = Some v -> + fmap_data m l = Some v -> red m (prim_get (val_loc l)) m v | red_set : forall m m' l v, - m' = state_update m l v -> + m' = fmap_update m l v -> red m (prim_set (val_pair (val_loc l) v)) m' val_unit. End Red. -(*------------------------------------------------------------------*) -(* ** Tactic [state_red] for proving [red] goals modulo +(* ---------------------------------------------------------------------- *) +(* ** Tactic [fmap_red] for proving [red] goals modulo equalities between states *) -Ltac state_red_base tt ::= +Ltac fmap_red_base tt ::= match goal with H: red _ ?t _ _ |- red _ ?t _ _ => - applys_eq H 2 4; try state_eq end. + applys_eq H 2 4; try fmap_eq end. diff --git a/model/LambdaSep.v b/model/LambdaSep.v index 09586a808f09904a753878532f2972355c4427c7..ff1f94c7fc71784776e9a12185ae03c03e52429f 100644 --- a/model/LambdaSep.v +++ b/model/LambdaSep.v @@ -16,18 +16,18 @@ License: MIT. Set Implicit Arguments. Require Export LambdaSemantics SepFunctor. -Open Scope state_scope. +Open Scope fmap_scope. Ltac auto_star ::= jauto. -(********************************************************************) +(* ********************************************************************** *) (* * Construction of core of the logic *) Module SepBasicCore. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Types *) Definition heap : Type := (state)%type. @@ -35,24 +35,24 @@ Definition heap : Type := (state)%type. Definition hprop := heap -> Prop. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of heaps *) (** Definitions used for uniformity with other instantiation of the functor *) -Notation "'heap_empty'" := (state_empty : heap) : heap_scope. +Notation "'heap_empty'" := (fmap_empty : heap) : heap_scope. Open Scope heap_scope. -Notation "h1 \u h2" := (state_union h1 h2) +Notation "h1 \u h2" := (fmap_union h1 h2) (at level 51, right associativity) : heap_scope. -Definition heap_union_empty_l := state_union_empty_l. -Definition heap_union_empty_r := state_union_empty_r. -Definition heap_union_comm := state_union_comm_disjoint. +Definition heap_union_empty_l := fmap_union_empty_l. +Definition heap_union_empty_r := fmap_union_empty_r. +Definition heap_union_comm := fmap_union_comm_disjoint. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Operators *) (* \[] *) @@ -84,7 +84,7 @@ Definition hprop_gc := hprop_exists (fun (H:hprop) => H). -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Notation *) Notation "\[]" := (hprop_empty) @@ -97,21 +97,21 @@ Notation "\GC" := (hprop_gc) : heap_scope. Open Scope heap_scope. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic for automation *) (* TODO: check how much is really useful *) -Hint Extern 1 (_ = _ :> heap) => state_eq. +Hint Extern 1 (_ = _ :> heap) => fmap_eq. -Tactic Notation "state_disjoint_pre" := +Tactic Notation "fmap_disjoint_pre" := subst; rew_disjoint; jauto_set. -Hint Extern 1 (\# _ _) => state_disjoint_pre. -Hint Extern 1 (\# _ _ _) => state_disjoint_pre. +Hint Extern 1 (\# _ _) => fmap_disjoint_pre. +Hint Extern 1 (\# _ _ _) => fmap_disjoint_pre. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of empty *) Lemma hprop_empty_intro : @@ -124,7 +124,7 @@ Lemma hprop_empty_inv : forall h, Proof using. auto. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of star *) Section Properties. @@ -159,7 +159,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Interaction of star with other operators *) Lemma hprop_star_exists : forall A (J:A->hprop) H, @@ -181,19 +181,19 @@ End Properties. End SepBasicCore. -(********************************************************************) +(* ********************************************************************** *) (* * Properties of the logic *) Module Export SepBasicSetup := SepLogicSetup SepBasicCore. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Singleton heap *) (** r ~~> v *) Definition hprop_single (l:loc) (v:val) : hprop := - fun h => h = state_single l v /\ l <> null. + fun h => h = fmap_single l v /\ l <> null. Notation "l '~~>' v" := (hprop_single l v) (at level 32, no associativity) : heap_scope. @@ -202,7 +202,7 @@ Lemma hprop_star_single_same_loc_disjoint : forall (l:loc) (v1 v2:val), (l ~~> v1) \* (l ~~> v2) ==> \[False]. Proof using. intros. unfold hprop_single. intros h (h1&h2&E1&E2&D&E). false. - subst. applys* state_single_same_loc_disjoint. + subst. applys* fmap_single_same_loc_disjoint. Qed. Global Opaque hprop_single. @@ -215,11 +215,11 @@ Ltac hcancel_hook H ::= end. -(********************************************************************) +(* ********************************************************************** *) (* * Reasoning Rules *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of triples *) Definition triple t H Q := @@ -230,7 +230,7 @@ Definition triple t H Q := /\ (Q v \* \GC \* H') h'. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Structural rules *) Lemma rule_extract_exists : forall t (A:Type) (J:A->hprop) Q, @@ -285,7 +285,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Term rules *) Lemma rule_val : forall v H Q, @@ -357,8 +357,8 @@ Lemma rule_ref : forall v, triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v). Proof using. intros. intros HF h N. - forwards~ (l&Dl&Nl): (state_disjoint_new null h v). - sets h1': (state_single l v). + forwards~ (l&Dl&Nl): (fmap_disjoint_new null h v). + sets h1': (fmap_single l v). exists (h1' \u h) (val_loc l). splits~. { applys~ red_ref. } { exists h1' h. split. @@ -371,7 +371,7 @@ Lemma rule_get : forall v l, Proof using. intros. intros HF h N. exists h v. splits~. { applys red_get. destruct N as (?&?&(?&?)&?&?&?). - subst h. applys~ state_union_single_read. } + subst h. applys~ fmap_union_single_read. } { rew_heap. rewrite hprop_star_pure. split~. hhsimpl~. } Qed. @@ -379,23 +379,23 @@ Lemma rule_set : forall w l v, triple (prim_set (val_pair (val_loc l) w)) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w). Proof using. intros. intros HF h N. destruct N as (h1&h2&(N0&N1)&N2&N3&N4). - hnf in N1. sets h1': (state_single l w). + hnf in N1. sets h1': (fmap_single l w). exists (h1' \u h2) val_unit. splits~. - { applys red_set. subst h h1. applys~ state_union_single_write. } + { applys red_set. subst h h1. applys~ fmap_union_single_write. } { rew_heap. rewrite hprop_star_pure. split~. { exists h1' h2. splits~. { hnfs~. } { hhsimpl~. } - { subst h1. applys~ state_disjoint_single_set v. } } } + { subst h1. applys~ fmap_disjoint_single_set v. } } } Qed. End RulesPrimitiveOps. -(********************************************************************) +(* ********************************************************************** *) (* * Bonus *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Triples satisfy the [local] predicate *) Lemma is_local_triple : forall t, @@ -415,7 +415,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Alternative, low-level definition of triples *) Definition triple' t H Q := @@ -438,11 +438,11 @@ Proof using. rewrite <- hprop_star_assoc in R2. destruct R2 as (h1''&h2'&N0&N1&N2&N3). subst h2'. destruct N0 as (h1'&h3'&T0&T1&T2&T3). - exists h1' h3' v. splits~. { state_red. } } + exists h1' h3' v. splits~. { fmap_red. } } { introv (h1&h2&N1&N2&D&U). forwards~ (h1'&h3'&v&R1&R2&R3): M h1 h2. exists (h1' \u h3' \u h2) v. splits~. - { state_red. } + { fmap_red. } { exists~ h1' (h3' \u h2). splits~. exists h3' h2. splits~. } } Qed. diff --git a/model/LambdaSepCredits.v b/model/LambdaSepCredits.v index 51853e17ecf12d1b9af5ded22112457d80d20687..a7291eb69bbf7fa6a354b754d9baec018668d00e 100644 --- a/model/LambdaSepCredits.v +++ b/model/LambdaSepCredits.v @@ -25,20 +25,20 @@ License: MIT. Set Implicit Arguments. Require Export LambdaSemantics SepFunctor. -Open Scope state_scope. +Open Scope fmap_scope. -(********************************************************************) +(* ********************************************************************** *) (* * Semantics *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Big-step evaluation with counting of the number of beta reductions (used by the formalization of Separation Logic with time credits) *) Section Redn. Local Open Scope nat_scope. -Local Open Scope state_scope. +Local Open Scope fmap_scope. Inductive red : nat -> state -> trm -> state -> val -> Prop := | red_val : forall m v, @@ -55,25 +55,25 @@ Inductive red : nat -> state -> trm -> state -> val -> Prop := red n m1 (subst_trm f v1 (subst_trm x v2 t)) m2 r -> red (S n) m1 (trm_app v1 v2) m2 r | red_ref : forall ma mb v l, - mb = (state_single l v) -> + mb = (fmap_single l v) -> \# ma mb -> red 0 ma (prim_ref v) (mb \+ ma) (val_loc l) | red_get : forall m l v, - state_data m l = Some v -> + fmap_data m l = Some v -> red 0 m (prim_get (val_loc l)) m v | red_set : forall m m' l v, - m' = state_update m l v -> + m' = fmap_update m l v -> red 0 m (prim_set (val_pair (val_loc l) v)) m' val_unit. End Redn. -(********************************************************************) +(* ********************************************************************** *) (* * Construction of core of the logic *) Module SepCreditsCore. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Representation of credits *) (** Representation of credits *) @@ -86,7 +86,7 @@ Definition credits_zero : credits := 0%nat. Definition credits_one : credits := 1%nat. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Types *) Definition heap : Type := (state * credits)%type. @@ -94,13 +94,13 @@ Definition heap : Type := (state * credits)%type. Definition hprop := heap -> Prop. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Operations on heaps *) (** Empty heap *) Definition heap_empty : heap := - (state_empty, 0%nat). + (fmap_empty, 0%nat). (** Projections *) @@ -135,7 +135,7 @@ Notation "h1 \u h2" := (heap_union h1 h2) (at level 51, right associativity) : heap_scope. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Operators *) Definition hprop_empty : hprop := @@ -158,7 +158,7 @@ Definition hprop_gc := hprop_exists (fun (H:hprop) => H). -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Notation *) Notation "\[]" := (hprop_empty) @@ -171,26 +171,26 @@ Notation "\GC" := (hprop_gc) : heap_scope. Open Scope heap_scope. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic for automation *) -Hint Extern 1 (_ = _ :> heap) => state_eq. +Hint Extern 1 (_ = _ :> heap) => fmap_eq. Lemma heap_disjoint_def : forall h1 h2, - heap_disjoint h1 h2 = state_disjoint (h1^s) (h2^s). + heap_disjoint h1 h2 = fmap_disjoint (h1^s) (h2^s). Proof using. auto. Qed. Hint Rewrite heap_disjoint_def : rew_disjoint. -Tactic Notation "state_disjoint_pre" := +Tactic Notation "fmap_disjoint_pre" := subst; rew_disjoint; jauto_set. -Hint Extern 1 (\# _ _) => state_disjoint_pre. +Hint Extern 1 (\# _ _) => fmap_disjoint_pre. Ltac math_0 ::= unfolds credits. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Equalities on [heap] *) Lemma heap_eq : forall h1 h2, @@ -205,37 +205,37 @@ Lemma heap_eq_forward : forall h1 h2, Proof using. intros (s1,n1) (s2,n2) M. inverts~ M. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of [heap_disjoint] *) Lemma heap_disjoint_sym : forall h1 h2, \# h1 h2 -> \# h2 h1. Proof using. intros [m1 n1] [m2 n2] H. simpls. - hint state_disjoint_sym. autos*. + hint fmap_disjoint_sym. autos*. Qed. Lemma heap_disjoint_comm : forall h1 h2, \# h1 h2 = \# h2 h1. Proof using. intros [m1 n1] [m2 n2]. simpls. - hint state_disjoint_sym. extens*. + hint fmap_disjoint_sym. extens*. Qed. Lemma heap_disjoint_empty_l : forall h, \# heap_empty h. -Proof using. intros [m n]. hint state_disjoint_empty_l. hnfs*. Qed. +Proof using. intros [m n]. hint fmap_disjoint_empty_l. hnfs*. Qed. Lemma heap_disjoint_empty_r : forall h, \# h heap_empty. -Proof using. intros [m n]. hint state_disjoint_empty_r. hnfs*. Qed. +Proof using. intros [m n]. hint fmap_disjoint_empty_r. hnfs*. Qed. Lemma heap_disjoint_union_eq_r : forall h1 h2 h3, \# h1 (h2 \u h3) = (\# h1 h2 /\ \# h1 h3). Proof using. intros [m1 n1] [m2 n2] [m3 n3]. unfolds heap_disjoint, heap_union. simpls. - rewrite state_disjoint_union_eq_r. extens*. + rewrite fmap_disjoint_union_eq_r. extens*. Qed. Lemma heap_disjoint_union_eq_l : forall h1 h2 h3, @@ -256,7 +256,7 @@ Tactic Notation "rew_disjoint" "*" := rew_disjoint; auto_star. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of [heap_union] *) Lemma heap_union_comm : forall h1 h2, @@ -264,21 +264,21 @@ Lemma heap_union_comm : forall h1 h2, h1 \u h2 = h2 \u h1. Proof using. intros [m1 n1] [m2 n2] H. unfold heap_union. - simpl. fequals. state_eq. math. + simpl. fequals. fmap_eq. math. Qed. Lemma heap_union_assoc : forall h1 h2 h3, (h1 \u h2) \u h3 = h1 \u (h2 \u h3). Proof using. intros [m1 n1] [m2 n2] [m3 n3]. unfolds heap_union. - simpl. fequals. state_eq. math. + simpl. fequals. fmap_eq. math. Qed. Lemma heap_union_empty_l : forall h, heap_empty \u h = h. Proof using. intros [m n]. unfold heap_union, heap_empty. simpl. - fequals. apply~ state_union_empty_l. + fequals. apply~ fmap_union_empty_l. Qed. Lemma heap_union_empty_r : forall h, @@ -300,7 +300,7 @@ Hint Resolve heap_union_comm Hint Rewrite heap_union_state : rew_disjoint. -Hint Rewrite heap_union_state : rew_state. +Hint Rewrite heap_union_state : rew_fmap. Hint Rewrite heap_union_empty_l heap_union_empty_r @@ -323,7 +323,7 @@ Ltac heap_eq := solve [ rew_heap; subst; auto ]. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of empty *) Lemma hprop_empty_intro : @@ -336,7 +336,7 @@ Lemma hprop_empty_inv : forall h, Proof using. auto. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of star *) Section Properties. @@ -367,15 +367,15 @@ Proof using. { intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'. exists h1 (h2 \u h3). splits~. { exists h2 h3. splits*. } - { subst. applys heap_eq. split. { state_eq. } { simpl; math. } } } + { subst. applys heap_eq. split. { fmap_eq. } { simpl; math. } } } { intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'. exists (h1 \u h2) h3. splits~. { exists h1 h2. splits*. } - { subst. applys heap_eq. split. { state_eq. } { simpl; math. } } } + { subst. applys heap_eq. split. { fmap_eq. } { simpl; math. } } } Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Interaction of star with other operators *) Lemma hprop_star_exists : forall A (J:A->hprop) H, @@ -398,17 +398,17 @@ End SepCreditsCore. -(********************************************************************) +(* ********************************************************************** *) (* * Properties of the logic *) Module Export SepCreditsSetup := SepLogicSetup SepCreditsCore. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Singleton heap *) Definition hprop_single (l:loc) (v:val) : hprop := - fun h => h^s = state_single l v /\ h^c = credits_zero /\ l <> null. + fun h => h^s = fmap_single l v /\ h^c = credits_zero /\ l <> null. Notation "l '~~>' v" := (hprop_single l v) (at level 32, no associativity) : heap_scope. @@ -418,7 +418,7 @@ Lemma hprop_star_single_same_loc_disjoint : forall (l:loc) (v1 v2:val), Proof using. intros. unfold hprop_single. intros h ((m1&n1)&(m2&n2)&(E1&X1&N1)&(E2&X2&N2)&D&E). false. - subst. applys* state_single_same_loc_disjoint l v1 v2. + subst. applys* fmap_single_same_loc_disjoint l v1 v2. unfolds in D. rewrite <- E1. rewrite <- E2. auto. Qed. @@ -434,23 +434,23 @@ Ltac hcancel_hook H := Global Opaque hprop_single. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Credits heap *) Definition hprop_credits (n:nat) : hprop := - fun h => h^s = state_empty /\ h^c = n. + fun h => h^s = fmap_empty /\ h^c = n. Notation "'\\$' n" := (hprop_credits n) (at level 40, format "\\$ n") : heap_scope. Lemma hprop_credits_inv : forall h n, - (\\$ n) h -> h = (state_empty,n). + (\\$ n) h -> h = (fmap_empty,n). Proof using. intros (m,n') n (M1&M2). simpls. subst*. Qed. Global Opaque hprop_credits. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of credits *) Section Credits. @@ -471,8 +471,8 @@ Proof using. intros c1 c2. unfold hprop_credits, hprop_star, heap_union, heap_disjoint. applys prop_ext_1. intros [m n]. iff [M1 M2] ([m1 n1]&[m2 n2]&(M1&E1)&(M2&E2)&M3&M4). - { exists (state_empty:state,c1) (state_empty:state,c2). simpls. splits*. } - { simpls. inverts M4. subst. split~. state_eq. } + { exists (fmap_empty:state,c1) (fmap_empty:state,c2). simpls. splits*. } + { simpls. inverts M4. subst. split~. fmap_eq. } Qed. Lemma credits_substract : forall (n m : nat), @@ -486,16 +486,16 @@ Qed. End Credits. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactics for reductions *) -Ltac state_red_base tt ::= +Ltac fmap_red_base tt ::= match goal with H: red _ _ ?t _ _ |- red _ _ ?t _ _ => - applys_eq H 2 4; try state_eq end. + applys_eq H 2 4; try fmap_eq end. -(********************************************************************) +(* ********************************************************************** *) (* * Reasoning Rules *) Implicit Types h : heap. @@ -503,7 +503,7 @@ Implicit Types H : hprop. Implicit Types Q : val -> hprop. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of triples *) Definition triple t H Q := @@ -515,14 +515,14 @@ Definition triple t H Q := /\ (h^c = n + h'^c)%nat. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definitions of [pay] *) Definition pay_one H H' := H ==> (\\$ 1%nat) \* H'. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Structural rules *) Lemma rule_extract_exists : forall t (A:Type) (J:A->hprop) Q, @@ -577,7 +577,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Term rules *) Lemma rule_val : forall v H Q, @@ -636,7 +636,7 @@ Proof using. lets (Na&Nb): heap_eq_forward (rm N4). simpls. subst. lets~ (n&h'&v&R&K&C): (rm M) HF h2. exists (S n) h' v. splits~. - { applys* red_app. state_red~. } + { applys* red_app. fmap_red~. } { math. } Qed. @@ -660,8 +660,8 @@ Lemma rule_ref : forall v, triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v). Proof using. intros. intros HF h N. rew_heap in N. - forwards~ (l&Dl&Nl): (state_disjoint_new null (h^s) v). - sets m1': (state_single l v). + forwards~ (l&Dl&Nl): (fmap_disjoint_new null (h^s) v). + sets m1': (fmap_single l v). exists 0%nat ((m1' \+ h^s),h^c) (val_loc l). splits~. { applys~ red_ref. } { exists (m1',0%nat) h. split. @@ -676,7 +676,7 @@ Proof using. destruct N as (h1&h2&(N1a&N1b)&N2&N3&N4). forwards (E1&E2): heap_eq_forward (rm N4). simpls. exists 0%nat h v. splits~. - { applys red_get. rewrite E1. applys~ state_union_single_read. } + { applys red_get. rewrite E1. applys~ fmap_union_single_read. } { rew_heap. rewrite hprop_star_pure. split~. hhsimpl~. } Qed. @@ -685,26 +685,26 @@ Lemma rule_set : forall w l v, Proof using. intros. intros HF h N. destruct N as (h1&h2&(N1a&N1b&N1c)&N2&N3&N4). forwards (E1&E2): heap_eq_forward (rm N4). simpls. - sets m1': (state_single l w). + sets m1': (fmap_single l w). exists 0%nat ((m1' \+ h2^s), h2^c) val_unit. splits~. { applys red_set. rewrite E1. unfold m1'. rewrite N1a. - applys~ state_union_single_write. } + applys~ fmap_union_single_write. } { rew_heap. rewrite hprop_star_pure. split~. { exists (m1',0%nat) h2. splits~. { hnfs~. } { hhsimpl~. } { unfold m1'. unfolds heap_disjoint. rewrite N1a in N3. - applys~ state_disjoint_single_set v. } } } + applys~ fmap_disjoint_single_set v. } } } { simpls. rewrite N1b in E2. unfolds credits_zero. math. } Qed. End RulesPrimitiveOps. -(********************************************************************) +(* ********************************************************************** *) (* * Bonus *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Triples satisfy the [local] predicate *) Lemma is_local_triple : forall t, @@ -725,7 +725,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Alternative, slightly lower-level definition of triples *) Definition triple' t H Q := @@ -749,15 +749,15 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Alternative, lower-level definition of triples *) Definition triple'' t H Q := forall m1 c1 m2, - state_disjoint m1 m2 -> + fmap_disjoint m1 m2 -> H (m1,c1) -> exists n m1' m3' c1' v, - state_disjoint_3 m1' m3' m2 + fmap_disjoint_3 m1' m3' m2 /\ red n (m1 \+ m2) t (m1' \+ m3' \+ m2) v /\ (Q v) (m1',c1') /\ (c1 >= n + c1')%nat. @@ -780,14 +780,14 @@ Proof using. splits~. { subst. rew_disjoint; simpls; rew_disjoint. destruct N2. splits~. } - { state_red. } + { fmap_red. } { math. } } { introv (h1&h2&N1&N2&D&U). forwards~ (n&m1'&m3'&c1'&v&R1&R2&R3&R4): M (h1^s) (h1^c) (h2^s). { applys_eq N1 1. applys~ heap_eq. } lets (?&?): heap_eq_forward (rm U). simpls. exists n (m1' \+ m3' \+ h2^s) (c-n)%nat v. splits~. - { state_red. } + { fmap_red. } { exists (m1',c1') (m3' \+ h2^s, (h2^c + h1^c - n - c1')%nat). splits~. { exists (m3',(h1^c - n - c1')%nat) h2. splits~. { applys heap_eq. splits~. simpls. math. } } diff --git a/model/LambdaSepRO.v b/model/LambdaSepRO.v index 6fee2eb0e5192114c8b43ecc4ea5ba533040df85..037bc6420865776a4209a30bcbe2de4524c24743 100644 --- a/model/LambdaSepRO.v +++ b/model/LambdaSepRO.v @@ -17,11 +17,11 @@ License: MIT. Set Implicit Arguments. Require Export LambdaSemantics SepFunctor. -Open Scope state_scope. +Open Scope fmap_scope. Implicit Arguments exist [A P]. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic for TLC *) (* TODO: move *) @@ -37,28 +37,28 @@ Ltac fequal_base ::= end. -(********************************************************************) +(* ********************************************************************** *) (* * Construction of core of the logic *) Module SepROCore. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Types *) Definition heap : Type := - { h : (state*state)%type | let '(f,r) := h in state_disjoint f r }. + { h : (state*state)%type | let '(f,r) := h in fmap_disjoint f r }. Definition hprop := heap -> Prop. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Operations on heaps *) (** Empty heap *) Program Definition heap_empty : heap := - (state_empty, state_empty). + (fmap_empty, fmap_empty). (** Projections *) @@ -79,7 +79,7 @@ Open Scope heap_scope. (** Starable heaps: disjoint owned heaps, agreeible read-only heaps *) Definition heap_compat (h1 h2 : heap) : Prop := - state_agree h1^r h2^r + fmap_agree h1^r h2^r /\ (\# (h1^f) (h2^f) (h1^r \+ h2^r)). (** Union of heaps. @@ -94,7 +94,7 @@ Proof using. applys prove_Inhab heap_empty. Qed. Program Definition heap_union (h1 h2 : heap) : heap := If (heap_compat h1 h2) then (h1^f \+ h2^f, h1^r \+ h2^r) else arbitrary. Next Obligation. - destruct H. state_disjoint. + destruct H. fmap_disjoint. Qed. Notation "h1 \u h2" := (heap_union h1 h2) @@ -106,11 +106,11 @@ Coercion heap_state (h : heap) : state := (h^f \+ h^r). -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Operators *) Definition hprop_empty : hprop := - fun h => h^f = state_empty /\ h^r = state_empty. + fun h => h^f = fmap_empty /\ h^r = fmap_empty. Program Definition hprop_star (H1 H2 : hprop) : hprop := fun h => exists h1 h2, @@ -129,7 +129,7 @@ Definition hprop_gc := hprop_exists (fun (H:hprop) => H). -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Notation *) Notation "\[]" := (hprop_empty) @@ -142,35 +142,35 @@ Notation "\GC" := (hprop_gc) : heap_scope. Open Scope heap_scope. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic for automation *) -(* Hint Extern 1 (_ = _ :> heap) => state_eq. TODO *) +(* Hint Extern 1 (_ = _ :> heap) => fmap_eq. TODO *) -Tactic Notation "state_disjoint_pre" := +Tactic Notation "fmap_disjoint_pre" := subst; rew_disjoint; jauto_set. -Hint Extern 1 (\# _ _) => state_disjoint_pre. -Hint Extern 1 (\# _ _ _) => state_disjoint_pre. +Hint Extern 1 (\# _ _) => fmap_disjoint_pre. +Hint Extern 1 (\# _ _ _) => fmap_disjoint_pre. -Hint Resolve state_agree_sym. +Hint Resolve fmap_agree_sym. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Equalities on [heap] *) -Lemma heap_state_def : forall h, +Lemma heap_fmap_def : forall h, heap_state h = (h^f \+ h^r). Proof using. auto. Qed. -Hint Rewrite heap_state_def : rew_disjoint. +Hint Rewrite heap_fmap_def : rew_disjoint. Lemma heap_disjoint_components : forall h, \# (h^f) (h^r). Proof using. intros ((f,r)&D). simple~. Qed. Lemma heap_make : forall f r, - state_disjoint f r -> exists (h:heap), h^f = f /\ h^r = r. + fmap_disjoint f r -> exists (h:heap), h^f = f /\ h^r = r. Proof using. introv M. exists~ ((exist (f,r) M : heap)). Qed. Lemma heap_eq : forall h1 h2, @@ -187,7 +187,7 @@ Proof using. intros ((f1&r1)&D1) ((f2&r2)&D2) M. inverts~ M. Qed. Ltac unstate := unfold heap_state; simpl. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Auxiliary function [heap_ro] *) (** [heap_ro h] defines the read-only heap associated with [h], @@ -195,10 +195,10 @@ Ltac unstate := unfold heap_state; simpl. as read-only. *) Program Definition heap_ro h : heap := - (state_empty, h^f \+ h^r). + (fmap_empty, h^f \+ h^r). Lemma heap_ro_f : forall h, - (heap_ro h)^f = state_empty. + (heap_ro h)^f = fmap_empty. Proof using. auto. Qed. Lemma heap_ro_r : forall h, @@ -208,12 +208,12 @@ Proof using. auto. Qed. Lemma heap_ro_state : forall h, heap_state (heap_ro h) = heap_state h. Proof using. - intros h. do 2 rewrite heap_state_def. rewrite heap_ro_f, heap_ro_r. - state_eq. + intros h. do 2 rewrite heap_fmap_def. rewrite heap_ro_f, heap_ro_r. + fmap_eq. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of [heap_union] *) Lemma heap_union_def : forall h1 h2, @@ -238,7 +238,7 @@ Lemma heap_union_f : forall h1 h2, Proof using. introv D. unfold heap_union. rewrite (classicT_left D). destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2). - unstate. state_eq. + unstate. fmap_eq. Qed. Lemma heap_union_r : forall h1 h2, @@ -247,16 +247,16 @@ Lemma heap_union_r : forall h1 h2, Proof using. introv D. unfold heap_union. rewrite (classicT_left D). destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2). - unstate. state_eq. + unstate. fmap_eq. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of [heap_compat] *) Lemma heap_compat_def : forall h1 h2, heap_compat h1 h2 - = ( (state_agree h1^r h2^r) + = ( (fmap_agree h1^r h2^r) /\ (\# (h1^f) (h2^f) (h1^r \+ h2^r))). Proof using. auto. Qed. @@ -274,8 +274,8 @@ Lemma heap_compat_empty_l : forall h, Proof using. intros. lets: heap_disjoint_components h. unfold heap_empty. split; simpl. - { apply state_agree_empty_l. } - { state_disjoint. } + { apply fmap_agree_empty_l. } + { fmap_disjoint. } Qed. Lemma heap_compat_empty_r : forall h, @@ -293,9 +293,9 @@ Proof using. Hint Unfold heap_compat. intros ((f1&r1)&S1) ((f2&r2)&S2) ((f3&r3)&S3). intros (C1&D1) (C2&D2) (C3&D3). split; simpls. - { rewrite heap_union_r; [|auto]. simpl. applys~ state_agree_union_l. } + { rewrite heap_union_r; [|auto]. simpl. applys~ fmap_agree_union_l. } { rewrite heap_union_r; [|auto]. rewrite heap_union_f; [|auto]. - simpl. state_disjoint. } + simpl. fmap_disjoint. } Qed. Lemma heap_compat_union_r : forall h1 h2 h3, @@ -306,12 +306,12 @@ Lemma heap_compat_union_r : forall h1 h2 h3, Proof using. hint heap_compat_sym, heap_compat_union_l. autos*. Qed. Lemma heap_compat_refl_if_ro : forall h, - h^f = state_empty -> + h^f = fmap_empty -> heap_compat h h. Proof using. introv M. split. - { apply state_agree_refl. } - { rewrite M. state_disjoint. } + { apply fmap_agree_refl. } + { rewrite M. fmap_disjoint. } Qed. Lemma heap_compat_ro_l : forall h1 h2, @@ -319,8 +319,8 @@ Lemma heap_compat_ro_l : forall h1 h2, heap_compat (heap_ro h1) h2. Proof using. introv (N1&N2). split; simpl. - { applys~ state_agree_union_l. applys~ state_agree_disjoint. } - { state_disjoint. } + { applys~ fmap_agree_union_l. applys~ fmap_agree_disjoint. } + { fmap_disjoint. } Qed. Lemma heap_compat_ro_r : forall h1 h2, @@ -336,21 +336,21 @@ Lemma heap_compat_ro : forall h1 h2, Proof using. introv (M1&M2). split. { do 2 rewrite heap_ro_r. - applys~ state_agree_union_lr. } - { do 2 rewrite heap_ro_f. state_disjoint. } + applys~ fmap_agree_union_lr. } + { do 2 rewrite heap_ro_f. fmap_disjoint. } Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of [heap_empty] *) -Lemma heap_empty_state : heap_state heap_empty = state_empty. -Proof. unfold heap_empty. unstate. state_eq. Qed. +Lemma heap_empty_state : heap_state heap_empty = fmap_empty. +Proof. unfold heap_empty. unstate. fmap_eq. Qed. Hint Rewrite heap_empty_state : rew_heap. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** More properties of [heap_union] *) Program Lemma heap_union_comm : forall h1 h2, @@ -361,8 +361,8 @@ Proof using. tests E: (heap_compat h1 h2); tests E': (heap_compat h2 h1); try auto_false. fequals. fequals. - { applys state_union_comm_disjoint. { destruct E. state_disjoint. } } - { applys state_union_comm_agree. { destruct~ E. } } + { applys fmap_union_comm_disjoint. { destruct E. fmap_disjoint. } } + { applys fmap_union_comm_agree. { destruct~ E. } } Qed. Lemma heap_union_assoc : forall h1 h2 h3, @@ -381,7 +381,7 @@ Proof using. { applys~ heap_compat_union_r. } rewrites (rm E1). rewrites (rm E2). rewrite~ heap_union_f. rewrite~ heap_union_r. - split; state_eq. + split; fmap_eq. Qed. Hint Resolve heap_union_comm. @@ -392,7 +392,7 @@ Proof using. intros h. unfold heap_union. rewrite (classicT_left (heap_compat_empty_l h)). destruct h as ((f,r)&D). simpl. - fequals_rec; state_eq. + fequals_rec; fmap_eq. Qed. Lemma heap_union_empty_r : forall h, @@ -407,10 +407,10 @@ Lemma heap_union_state : forall h1 h2, Proof using. introv D. unfold heap_union. rewrite (classicT_left D). destruct h1 as ((f1,r1)&D1). destruct h2 as ((f2,r2)&D2). - unstate. state_eq. + unstate. fmap_eq. Qed. -Hint Rewrite heap_union_state : rew_state. +Hint Rewrite heap_union_state : rew_fmap. Hint Rewrite heap_union_empty_l heap_union_empty_r heap_ro_f heap_ro_r heap_union_f heap_union_r : rew_heap. @@ -433,7 +433,7 @@ Ltac heap_eq := solve [ rew_heap; subst; auto ]. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** More properties of [heap_compat] *) Lemma heap_compat_union_l_inv_l : forall h1 h2 h3, @@ -444,7 +444,7 @@ Proof using. introv M2 M1. lets (C1&D1): M1. lets (C2&D2): M2. rew_heap~ in C2. rew_heap~ in D2. - forwards~ (N1&N2): state_agree_union_l_inv C2. + forwards~ (N1&N2): fmap_agree_union_l_inv C2. Qed. Lemma heap_compat_union_l_inv_r : forall h1 h2 h3, @@ -475,7 +475,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of empty *) Lemma hprop_empty_intro : @@ -488,7 +488,7 @@ Lemma hprop_empty_inv : forall h, Proof using. introv M. applys~ heap_eq. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of star *) Section Properties. @@ -511,7 +511,7 @@ Lemma hprop_star_comm : forall H1 H2, H1 \* H2 = H2 \* H1. Proof using. intros. unfold hprop, hprop_star. extens. intros h. - hint state_agree_sym. + hint fmap_agree_sym. iff (h1&h2&M1&M2&D&U). { exists h2 h1. subst. splits~. } { exists h2 h1. subst. splits~. } @@ -538,7 +538,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Interaction of star with other operators *) Lemma hprop_star_exists : forall A (J:A->hprop) H, @@ -559,25 +559,25 @@ End Properties. End SepROCore. -(********************************************************************) +(* ********************************************************************** *) (* * Properties of the logic *) Module Export SepROSetup := SepLogicSetup SepROCore. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Disjunction heap *) Definition hprop_or (H1 H2 : hprop) : hprop := fun h => H1 h \/ H2 h. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Singleton heap *) Definition hprop_single (l:loc) (v:val) : hprop := - fun h => h^f = state_single l v - /\ h^r = state_empty + fun h => h^f = fmap_single l v + /\ h^r = fmap_empty /\ l <> null. Notation "l '~~>' v" := (hprop_single l v) @@ -588,7 +588,7 @@ Lemma hprop_star_single_same_loc_disjoint : forall (l:loc) (v1 v2:val), Proof using. intros. unfold hprop_single. intros h (((m1&n1)&D1)&((m2&n2)&D2)&(E1&X1)&(E2&X2)&D&E). false. - subst. simpls. subst. applys* state_single_same_loc_disjoint l v1 v2. + subst. simpls. subst. applys* fmap_single_same_loc_disjoint l v1 v2. Qed. Global Opaque hprop_single. @@ -604,7 +604,7 @@ Global Opaque hprop_single. -(********************************************************************) +(* ********************************************************************** *) (* * Auxiliary Definitions *) Implicit Types h : heap. @@ -612,18 +612,18 @@ Implicit Types H : hprop. Implicit Types Q : val -> hprop. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definitions of [duplicatable] *) Definition duplicatable (H:hprop) : Prop := H ==> H \* H. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definitions and properties of [normal] *) Program Definition normal (H:hprop) : Prop := - forall h, H h -> h^r = state_empty. + forall h, H h -> h^r = fmap_empty. Definition normal_post A (Q:A->hprop) := forall x, normal (Q x). @@ -653,7 +653,7 @@ Proof using. lets (_&E): heap_eq_forward EQ. simpls. rewrite E. rewrite~ heap_union_r. rewrites (>> N1 P1). rewrites (>> N2 P2). - rewrite~ state_union_empty_r. + rewrite~ fmap_union_empty_r. Qed. Lemma normal_exists : forall A (J:A->hprop), @@ -678,12 +678,12 @@ Lemma normal_himpl : forall H1 H2, Proof using. introv HS HI M. lets: HI M. applys* HS. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definitions and properties of [ROl] *) Definition RO (H:hprop) : hprop := fun h => exists h', H h' - /\ h^f = state_empty + /\ h^f = fmap_empty /\ h^r = h'^f \+ h'^r. Lemma RO_duplicatable : forall H, @@ -694,7 +694,7 @@ Proof using. exists h h. splits~. { applys heap_eq. rewrite~ heap_union_f. rewrite~ heap_union_r. rewrite M2. - split. state_eq. rewrite~ state_union_idempotent. } + split. fmap_eq. rewrite~ fmap_union_idempotent. } Qed. Lemma RO_covariant : forall H1 H2, @@ -710,10 +710,10 @@ Proof using. intros. apply prop_ext_1. intros h. iff (h'&(h''&M1'&M2'&M3')&M2&M3) (h'&M1&M2&M3). { exists h''. splits~. - rewrite M3. rewrite M3'. rewrite M2'. state_eq. } + rewrite M3. rewrite M3'. rewrite M2'. fmap_eq. } { exists h. splits~. { exists h'. split~. } - { rewrite M2. state_eq. } } + { rewrite M2. fmap_eq. } } Qed. Lemma RO_exists : forall A (J:A->hprop), @@ -745,8 +745,8 @@ Proof using. { exists~ h2. } { auto. } { applys heap_eq. rew_heap~. split. - { rewrite M2. state_eq. } - { rewrite M3,N2. rew_heap~. state_eq. } } + { rewrite M2. fmap_eq. } + { rewrite M3,N2. rew_heap~. fmap_eq. } } Qed. Lemma heap_ro_pred : forall (H:hprop) h, @@ -756,27 +756,27 @@ Proof using. introv N. exists h. split~. Qed. -(********************************************************************) +(* ********************************************************************** *) (* * Reasoning rules, low-level proofs *) Module TripleLowLevel. Hint Resolve heap_compat_union_l heap_compat_union_r. -Hint Resolve state_agree_empty_l state_agree_empty_r. +Hint Resolve fmap_agree_empty_l fmap_agree_empty_r. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition and properties of [on_rw_sub] *) Program Definition on_rw_sub H h := exists h1 h2, heap_compat h1 h2 /\ h = h1 \u h2 - /\ h1^r = state_empty + /\ h1^r = fmap_empty /\ H h1. Lemma on_rw_sub_base : forall H h, H h -> - h^r = state_empty -> + h^r = fmap_empty -> on_rw_sub H h. Proof using. intros H h M N. exists h heap_empty. splits~. @@ -793,7 +793,7 @@ Proof using. lets~ (N1a&N1b): heap_compat_union_l_inv N1. exists h3 (h4 \u h2). splits~. { applys~ heap_union_assoc. } - { forwards~: state_union_eq_empty_inv_l N3. } + { forwards~: fmap_union_eq_empty_inv_l N3. } Qed. Lemma on_rw_sub_gc' : forall H h, @@ -832,7 +832,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of triples *) (** Recall that the projection [heap_state : heap >-> state] @@ -848,7 +848,7 @@ Definition triple t (H:hprop) (Q:val->hprop) := /\ on_rw_sub (Q v) h1'. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Structural rules *) Lemma rule_extract_exists : forall t A (J:A->hprop) Q, @@ -890,8 +890,8 @@ Proof using. forwards* (h1'&v&(N1&N2&N3&N4)): (rm M) (h12 \u h2) (rm P11). lets~ (D3&D4): heap_compat_union_r_inv (rm N1). exists (h1' \u h12) v. splits~. - { state_red~. } - { rew_heap~. rewrite N3. state_eq~. } + { fmap_red~. } + { rew_heap~. rewrite N3. fmap_eq~. } { applys~ on_rw_sub_union_r. } Qed. @@ -928,7 +928,7 @@ Proof using. lets E12: (rm N) P12. subst h1. lets~ (D1&D2): heap_compat_union_l_inv (rm D). asserts R12: (heap_state (heap_ro h12) = heap_state h12). - { unstate. rewrite E12. state_eq. } + { unstate. rewrite E12. fmap_eq. } asserts C: (heap_compat (h11 \u heap_ro h12) h2). { apply~ heap_compat_union_l. applys~ heap_compat_ro_l. } forwards~ (h1'&v&(N1&N2&N3&N4)): (rm M) (h11 \u (heap_ro h12)) h2. @@ -937,21 +937,21 @@ Proof using. rew_heap~ in N3. rewrite E12 in N3. lets G: heap_disjoint_components h1'. forwards (h1''&F1&F2): heap_make (h1'^f \+ h12^f) (h11^r). - { rewrite N3 in G. state_disjoint. } + { rewrite N3 in G. fmap_disjoint. } asserts C': (heap_compat h1'' h2). { unfolds. rewrite F1,F2. split. { destruct~ D1. } { lets G2: heap_disjoint_components h2. rewrite N3 in G. - state_disjoint. } } + fmap_disjoint. } } exists h1'' v. splits. { auto. } - { state_red~. + { fmap_red~. { rewrite~ R12. } - { fequals. unstate. rewrite F1,F2,N3. state_eq. } } - { rew_heap~. rewrite F2,E12. state_eq~. } + { fequals. unstate. rewrite F1,F2,N3. fmap_eq. } } + { rew_heap~. rewrite F2,E12. fmap_eq~. } { clears h2. rename h1'' into hd. rename H2 into Hb. sets Ha: (Q1 v). - rename h1' into ha. rewrite~ state_union_empty_r in N3. + rename h1' into ha. rewrite~ fmap_union_empty_r in N3. rename h12 into hb. rename h11 into hc. (* LATER: begin separate lemma *) destruct N4 as (hx&hy&V1&V2&V3&V4). @@ -960,44 +960,44 @@ Proof using. { unfolds. rewrite E12. split. { auto. } { lets Gx: heap_disjoint_components hx. rewrite V3. auto. } } - forwards~ (hyf&W1&W2): heap_make (hy^f) (state_empty:state). - forwards~ (hcr&Y1&Y2): heap_make (state_empty:state) (hc^r). + forwards~ (hyf&W1&W2): heap_make (hy^f) (fmap_empty:state). + forwards~ (hcr&Y1&Y2): heap_make (fmap_empty:state) (hc^r). (* LATER: find a way to automate these lemmas *) - (* LATER: automate disjoint_components use by state_disjoint *) + (* LATER: automate disjoint_components use by fmap_disjoint *) asserts C2: (heap_compat hcr hyf). { unfolds. split. { rewrite~ W2. } - { rewrite Y1,Y2,W1,W2. state_disjoint. } } + { rewrite Y1,Y2,W1,W2. fmap_disjoint. } } asserts C3: (heap_compat hx hcr). { unfolds. split. { rewrite~ V3. } - { rewrite Y1,Y2,V3. state_disjoint. } } + { rewrite Y1,Y2,V3. fmap_disjoint. } } asserts C4: (heap_compat hx hyf). { unfolds. split. { rewrite~ W2. } - { rewrite W1,W2,V3. state_disjoint. } } + { rewrite W1,W2,V3. fmap_disjoint. } } asserts C5: (heap_compat hb hyf). { unfolds. split. { rewrite~ W2. } - { rewrite W1,W2,E12. state_disjoint. } } + { rewrite W1,W2,E12. fmap_disjoint. } } asserts C6: (heap_compat hb hcr). { unfolds. split. { rewrite~ E12. } - { rewrite Y1,Y2,E12. state_disjoint. } } + { rewrite Y1,Y2,E12. fmap_disjoint. } } exists (hx \u hb) (hcr \u hyf). splits. { auto. } { applys heap_eq. split. { rewrite F1,V2. rew_heap~. rewrite Y1,W1. - rewrite state_union_empty_l. - do 2 rewrite state_union_assoc. fequals. - applys state_union_comm_disjoint. auto. } - { rew_heap~. rewrite V3,E12,W2,Y2,F2. state_eq. } } - { rew_heap~. rewrite V3,E12. state_eq. } + rewrite fmap_union_empty_l. + do 2 rewrite fmap_union_assoc. fequals. + applys fmap_union_comm_disjoint. auto. } + { rew_heap~. rewrite V3,E12,W2,Y2,F2. fmap_eq. } } + { rew_heap~. rewrite V3,E12. fmap_eq. } { exists~ hx hb. } } Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Term rules *) Lemma rule_val : forall v H Q, @@ -1048,8 +1048,8 @@ Proof using. rewrite~ heap_union_assoc. } { rewrite~ heap_union_assoc. } } } { rew_heap~. rewrite T3. rew_heap~. rewrite <- N3. rew_heap~. - rewrite (state_union_comm_agree (hx^r \+ hy^r) h12^r). - rewrite~ state_union_assoc. applys state_agree_union_l. + rewrite (fmap_union_comm_agree (hx^r \+ hy^r) h12^r). + rewrite~ fmap_union_assoc. applys fmap_agree_union_l. destruct~ N1aa. destruct~ N1ba. } { applys~ on_rw_sub_union_r. } Qed. @@ -1106,21 +1106,21 @@ Lemma rule_ref : forall v, Proof using. intros. intros h1 h2 _ P1. lets E: hprop_empty_inv P1. subst h1. - forwards~ (l&Dl&Nl): (state_disjoint_new null (heap_state h2) v). - lets~ (h1'&E1&E2): heap_make (state_single l v) (state_empty:state). - asserts E3: (heap_state h1' = state_single l v). - { unstate. rewrite E1,E2. state_eq. } + forwards~ (l&Dl&Nl): (fmap_disjoint_new null (heap_state h2) v). + lets~ (h1'&E1&E2): heap_make (fmap_single l v) (fmap_empty:state). + asserts E3: (heap_state h1' = fmap_single l v). + { unstate. rewrite E1,E2. fmap_eq. } asserts D1': (\# (heap_state h2) (heap_state h1')). - { unfold heap_state at 2. rewrite E1,E2. state_disjoint. } + { unfold heap_state at 2. rewrite E1,E2. fmap_disjoint. } (* LATER: beautify the assertions above *) exists h1' (val_loc l). asserts C: (heap_compat h1' h2). { split. { rewrite~ E2. } { rewrite E1,E2. lets: heap_disjoint_components h2. - state_disjoint. } } + fmap_disjoint. } } splits~. - { rew_heap. rew_state~. applys~ red_ref. } + { rew_heap. rew_fmap~. applys~ red_ref. } { applys~ on_rw_sub_base. exists l. applys~ himpl_inst_prop (l ~~> v). split~. } Qed. @@ -1129,10 +1129,10 @@ Lemma rule_get_ro : forall v l, triple (prim_get (val_loc l)) (RO (l ~~> v)) (fun x => \[x = v]). Proof using. intros. intros h1 h2 D (h1'&(E1'&E2'&NL)&E1&E2). - rewrites E2' in E2. rewrite state_union_empty_r in E2. + rewrites E2' in E2. rewrite fmap_union_empty_r in E2. exists h1 v. splits~. - { rew_state~. applys red_get. rewrite heap_state_def. - rewrite E1,E2,E1'. rew_state. applys~ state_union_single_read. } + { rew_fmap~. applys red_get. rewrite heap_fmap_def. + rewrite E1,E2,E1'. rew_fmap. applys~ fmap_union_single_read. } { exists heap_empty h1. splits~. { applys~ heap_compat_empty_l. } { heap_eq. } @@ -1143,18 +1143,18 @@ Lemma rule_set : forall w l v, triple (prim_set (val_pair (val_loc l) w)) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w). Proof using. intros. intros h1 h2 D (E1&E2&NL). - lets~ (h1'&E1'&E2'): heap_make (state_single l w) (state_empty:state). + lets~ (h1'&E1'&E2'): heap_make (fmap_single l w) (fmap_empty:state). exists h1' val_unit. - asserts Dl: (state_disjoint (state_single l w) (heap_state h2)). + asserts Dl: (fmap_disjoint (fmap_single l w) (heap_state h2)). { destruct D as (D1&D2). rewrite E1 in D2. unstate. - applys state_disjoint_single_set v. auto. } + applys fmap_disjoint_single_set v. auto. } asserts C: (heap_compat h1' h2). { destruct D as (D1&D2). unfolds. rewrite E1',E2'. unfold heap_state in Dl. split~. } splits~. - { rew_state~. applys red_set. - rewrite (@heap_state_def h1'). rewrite (@heap_state_def h1). - rewrite E1,E2,E1',E2'. rew_state. applys~ state_union_single_write v w. } + { rew_fmap~. applys red_set. + rewrite (@heap_fmap_def h1'). rewrite (@heap_fmap_def h1). + rewrite E1,E2,E1',E2'. rew_fmap. applys~ fmap_union_single_write v w. } { rewrite E2,E2'. auto. } { applys~ on_rw_sub_base. applys~ himpl_inst_prop (l ~~> w). split~. } Qed. diff --git a/model/LambdaSepRONew.v b/model/LambdaSepRONew.v index 111f2b02002368fc0f94ea92f1d6df534599c9e4..f82132e78384fd25ce9a393cca2b267095a60732 100644 --- a/model/LambdaSepRONew.v +++ b/model/LambdaSepRONew.v @@ -2,18 +2,18 @@ (* -(********************************************************************) +(* ********************************************************************** *) (* * Reasoning rules, high-level proofs *) (* Module TripleHighLevel. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of triples *) Program Definition only_rw (h:heap) : heap := - (h^f, state_empty). + (h^f, fmap_empty). Program Definition triple t (H:hprop) (Q:val->hprop) := @@ -25,7 +25,7 @@ Program Definition triple t (H:hprop) (Q:val->hprop) := -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Structural rules *) Lemma rule_extract_prop : forall t (P:Prop) H Q, @@ -104,12 +104,12 @@ Proof using. splits~. { applys~ heap_ro_pred. } { applys heap_eq. split. - { rew_heap~. state_eq. } (* todo clean *) - { rewrite~ heap_union_r. rewrite~ state_union_idempotent. } } } } + { rew_heap~. fmap_eq. } (* todo clean *) + { rewrite~ heap_union_r. rewrite~ fmap_union_idempotent. } } } } do 2 rewrite <- (hprop_star_comm_assoc (= heap_ro h2)) in K. destruct K as (h2'&h1'&D'&P2'&P1'&EQ'). subst h2'. (* - (* forwards T: heap_state_def h2. rewrites (>> NH2 P2) in T. rew_state~. *) + (* forwards T: heap_fmap_def h2. rewrites (>> NH2 P2) in T. rew_state~. *) asserts S: (h1'^r = h1^r). { (* todo clean *) clears R P1 P1'. specializes NH2 P2. clears P2. rewrite EQ' in E. rewrite <- (heap_union_comm h1) in E. @@ -121,7 +121,7 @@ Proof using. lets DH2: (heap_disjoint_components h2). rew_heap in *. rewrite NH2 in *. clears NH2. rew_state. (* - applys state_union_eq_inv E. rewrite heap_ro_r. + applys fmap_union_eq_inv E. rewrite heap_ro_r. rewrites (>> NH2 P2). destruct D' as (D1&D2).*) admit. } @@ -136,31 +136,31 @@ Proof using. lets DH2: (heap_disjoint_components h2). rew_heap~ in *. split. - { rewrite~ NH2. applys state_agree_empty_l. } - { rewrite state_disjoint_3_unfold. splits. + { rewrite~ NH2. applys fmap_agree_empty_l. } + { rewrite fmap_disjoint_3_unfold. splits. { auto. } { auto. } - { rewrite NH2. cuts_rewrite (h1'^r = state_empty). + { rewrite NH2. cuts_rewrite (h1'^r = fmap_empty). auto. lets (_&K): heap_eq_forward EQ'. simpls. rew_heap~ in K. - forwards~: state_union_eq_empty_inv_r (eq_sym K). + forwards~: fmap_union_eq_empty_inv_r (eq_sym K). } } } lets (K1&K2): heap_eq_forward EQ'. simpls. rew_heap~ in K2. - forwards~ K3: state_union_eq_empty_inv_r (eq_sym K2). - forwards~ K4: state_union_eq_empty_inv_l (eq_sym K2). - forwards~ K5: state_union_eq_empty_inv_r K4. - forwards~ K6: state_union_eq_empty_inv_l K4. + forwards~ K3: fmap_union_eq_empty_inv_r (eq_sym K2). + forwards~ K4: fmap_union_eq_empty_inv_l (eq_sym K2). + forwards~ K5: fmap_union_eq_empty_inv_r K4. + forwards~ K6: fmap_union_eq_empty_inv_l K4. rew_heap~ in K1. rew_state~. exists (h1' \u h2) v. splits~. - { state_red~. + { fmap_red~. { rewrite~ heap_ro_state. } - { do 3 rewrite heap_state_def. - rewrite E. rew_heap~. rewrite K1,K3,K5,K6. state_eq. simpls. admit. } } + { do 3 rewrite heap_fmap_def. + rewrite E. rew_heap~. rewrite K1,K3,K5,K6. fmap_eq. simpls. admit. } } { asserts_rewrite (only_rw h' = h2 \u h1'). { - applys heap_eq. simpls. rew_heap~. rewrite K5,K6,K3. splits; state_eq~. - rewrite K1. rew_heap~. state_eq. } + applys heap_eq. simpls. rew_heap~. rewrite K5,K6,K3. splits; fmap_eq~. + rewrite K1. rew_heap~. fmap_eq. } rewrite <- (hprop_star_comm H2). rew_heap. exists h2 h1'. splits~. } @@ -170,7 +170,7 @@ lets (K1&K2): heap_eq_forward EQ'. simpls. rew_heap~ in K2. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Term rules *) Lemma rule_val : forall v H Q, @@ -241,29 +241,29 @@ Qed. Section RulesPrimitiveOps. Transparent hprop_star hprop_single. Hint Resolve heap_compat_union_l heap_compat_union_r. -Hint Resolve state_agree_empty_l state_agree_empty_r. +Hint Resolve fmap_agree_empty_l fmap_agree_empty_r. Lemma rule_ref : forall v, triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v). Proof using. intros. intros HF h N. - forwards~ (l&Dl&Nl): (state_disjoint_new null (heap_state h) v). - lets~ (h1'&E1&E2): heap_make (state_single l v) (state_empty:state). - asserts E3: (heap_state h1' = state_single l v). - { unstate. rewrite E1,E2. state_eq. } + forwards~ (l&Dl&Nl): (fmap_disjoint_new null (heap_state h) v). + lets~ (h1'&E1&E2): heap_make (fmap_single l v) (fmap_empty:state). + asserts E3: (heap_state h1' = fmap_single l v). + { unstate. rewrite E1,E2. fmap_eq. } asserts D1': (\# (heap_state h) (heap_state h1')). - { unfold heap_state at 2. rewrite E1,E2. state_disjoint. } + { unfold heap_state at 2. rewrite E1,E2. fmap_disjoint. } asserts C: (heap_compat h1' h). { split. { rewrite~ E2. } { rewrite E1,E2. lets: heap_disjoint_components h. - state_disjoint. } } + fmap_disjoint. } } exists (h1' \u h) (val_loc l). splits~. { rew_state~. applys~ red_ref. } { exists h1' h. split~. splits~. { exists l. applys~ himpl_inst_prop (l ~~> v). hnfs~. } { rew_heap in N. hhsimpl~. } } - { rew_heap~. rewrite E2. state_eq. } + { rew_heap~. rewrite E2. fmap_eq. } Qed. (* Lemma rule_get_ro : forall v l, @@ -273,10 +273,10 @@ Proof using. exists h v. splits~. { applys red_get. destruct N as (h1&h2&D&P1&P2&E). destruct P1 as (h11&(Q1&Q2)&E1&E2). - subst h. rewrite heap_state_def. (* todo: cleanup *) - rewrite state_union_comm_disjoint; [|rew_heap~]. + subst h. rewrite heap_fmap_def. (* todo: cleanup *) + rewrite fmap_union_comm_disjoint; [|rew_heap~]. rew_heap~. rewrite E1,E2,Q1,Q2. rew_state. - applys~ state_union_single_read. } + applys~ fmap_union_single_read. } { rewrite hprop_star_pure. split~. hhsimpl~. } Qed. @@ -285,19 +285,19 @@ Lemma rule_set : forall w l v, Proof using. intros. intros HF h N. destruct N as (h1&h2&D&P1&P2&E). destruct P1 as (Q1&Q2). - lets~ (h1'&E1'&E2'): heap_make (state_single l w) (state_empty:state). - asserts Dl: (state_disjoint (state_single l w) (heap_state h2)). + lets~ (h1'&E1'&E2'): heap_make (fmap_single l w) (fmap_empty:state). + asserts Dl: (fmap_disjoint (fmap_single l w) (heap_state h2)). { destruct D as (D1&D2). rewrite Q1 in D2. unstate. - applys state_disjoint_single_set v. auto. } + applys fmap_disjoint_single_set v. auto. } asserts C: (heap_compat h1' h2). { destruct D as (D1&D2). unfolds. rewrite E1',E2'. unfold heap_state in Dl. split~. } exists (h1' \u h2) val_unit. splits~. { applys red_set. rew_state~. rewrite E. (* todo: cleanup *) - rewrite (@heap_state_def h1'). rewrite (@heap_state_def h2). + rewrite (@heap_fmap_def h1'). rewrite (@heap_fmap_def h2). rewrite E1',E2'. rew_state~. - applys~ state_union_single_write v w. - rewrite (@heap_state_def h1). rewrite Q1,Q2. state_eq. } + applys~ fmap_union_single_write v w. + rewrite (@heap_fmap_def h1). rewrite Q1,Q2. fmap_eq. } { rew_heap. rewrite hprop_star_pure. split~. { exists h1' h2. splits~. { hnfs~. } @@ -313,7 +313,7 @@ End TripleHighLevel. *) -(********************************************************************) +(* ********************************************************************** *) (* * Reasoning rules, high-level proofs *) @@ -322,15 +322,15 @@ End TripleHighLevel. Module TripleHighLevel. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition and properties of [on_rw] *) Program Definition on_rw H h := - H h /\ h^r = state_empty. + H h /\ h^r = fmap_empty. Lemma on_rw_base : forall H h, H h -> - h^r = state_empty -> + h^r = fmap_empty -> on_rw H h. Proof using. intros H h M N. splits~. Qed. @@ -379,7 +379,7 @@ Lemma on_rw_star_l : forall H H', Proof using. intros. intros h ((h1&h2&D&N1&N2&E)&P2). subst h. rew_heap~ in *. - forwards~ Q: state_union_eq_empty_inv_l P2. + forwards~ Q: fmap_union_eq_empty_inv_l P2. exists h1 h2. splits~. { split~. } Qed. @@ -398,7 +398,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of triples *) Definition triple t (H:hprop) (Q:val->hprop) := @@ -410,7 +410,7 @@ Definition triple t (H:hprop) (Q:val->hprop) := /\ h'^r = h^r. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Structural rules *) Lemma rule_extract_prop : forall t (P:Prop) H Q, @@ -491,10 +491,10 @@ Proof using. (*lets DD': DD. rewrite <- Th1'f in DD'.*) asserts Eh': (heap_state h1' = heap_state h'). - { rewrite (heap_state_def h'). - rewrite (heap_state_def h1'). + { rewrite (heap_fmap_def h'). + rewrite (heap_fmap_def h1'). rewrite Th1'f. rewrite E. - state_eq~. } + fmap_eq~. } asserts HC: (heap_compat h2 h1'). { admit. } @@ -511,17 +511,17 @@ F2 : h1''^r = h11^r *) (* - forwards~ (h2'&Th2'f&Th2'r): heap_make (state_empty:state) (state_empty:state). + forwards~ (h2'&Th2'f&Th2'r): heap_make (fmap_empty:state) (fmap_empty:state). asserts Eh': (heap_state h2' \+ heap_state h1' = heap_state h'). - { rewrite (heap_state_def h'). - rewrite (heap_state_def h2'). - rewrite (heap_state_def h1'). + { rewrite (heap_fmap_def h'). + rewrite (heap_fmap_def h2'). + rewrite (heap_fmap_def h1'). rewrite Th1'f,Th2'f,Th2'r. rewrite E. - state_eq~. } + fmap_eq~. } *) exists (h2 \u h1') v. splits~. - { state_red~. + { fmap_red~. { rewrite~ heap_ro_state. } rewrite Eh'. *) @@ -549,11 +549,11 @@ F2 : h1''^r = h11^r splits~. { applys~ heap_ro_pred. } { applys heap_eq. split. - { rew_heap~. state_eq. } (* todo clean *) - { rewrite~ heap_union_r. rewrite~ state_union_idempotent. } } } } + { rew_heap~. fmap_eq. } (* todo clean *) + { rewrite~ heap_union_r. rewrite~ fmap_union_idempotent. } } } } do 2 rewrite <- (hprop_star_comm_assoc (= heap_ro h2)) in K. destruct K as (h2'&h1'&D'&P2'&P1'&EQ'). subst h2'. - (* forwards T: heap_state_def h2. rewrites (>> NH2 P2) in T. rew_state~. *) + (* forwards T: heap_fmap_def h2. rewrites (>> NH2 P2) in T. rew_state~. *) asserts S: (h1'^r = h1^r). { (* todo clean *) clears R P1 P1'. specializes NH2 P2. clears P2. rewrite EQ' in E. rewrite <- (heap_union_comm h1) in E. @@ -565,7 +565,7 @@ F2 : h1''^r = h11^r lets DH2: (heap_disjoint_components h2). rew_heap in *. rewrite NH2 in *. clears NH2. rew_state. (* - applys state_union_eq_inv E. rewrite heap_ro_r. + applys fmap_union_eq_inv E. rewrite heap_ro_r. rewrites (>> NH2 P2). destruct D' as (D1&D2).*) admit. } @@ -577,13 +577,13 @@ F2 : h1''^r = h11^r lets DH2: (heap_disjoint_components h2). rew_heap in *. split. - { rewrite NH2. applys state_agree_empty_l. } - { rewrite state_disjoint_3_unfold. splits. + { rewrite NH2. applys fmap_agree_empty_l. } + { rewrite fmap_disjoint_3_unfold. splits. { auto. } { auto. } { rewrite NH2. rewrite~ S. } } } exists (h2 \u h1') v. splits~. - { state_red~. + { fmap_red~. { rewrite~ heap_ro_state. } { rewrite~ heap_ro_state. } } { @@ -591,7 +591,7 @@ F2 : h1''^r = h11^r Admitted. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Term rules *) Lemma rule_val : forall v H Q, @@ -662,29 +662,29 @@ Qed. Section RulesPrimitiveOps. Transparent hprop_star hprop_single. Hint Resolve heap_compat_union_l heap_compat_union_r. -Hint Resolve state_agree_empty_l state_agree_empty_r. +Hint Resolve fmap_agree_empty_l fmap_agree_empty_r. Lemma rule_ref : forall v, triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v). Proof using. intros. intros HF h N. - forwards~ (l&Dl&Nl): (state_disjoint_new null (heap_state h) v). - lets~ (h1'&E1&E2): heap_make (state_single l v) (state_empty:state). - asserts E3: (heap_state h1' = state_single l v). - { unstate. rewrite E1,E2. state_eq. } + forwards~ (l&Dl&Nl): (fmap_disjoint_new null (heap_state h) v). + lets~ (h1'&E1&E2): heap_make (fmap_single l v) (fmap_empty:state). + asserts E3: (heap_state h1' = fmap_single l v). + { unstate. rewrite E1,E2. fmap_eq. } asserts D1': (\# (heap_state h) (heap_state h1')). - { unfold heap_state at 2. rewrite E1,E2. state_disjoint. } + { unfold heap_state at 2. rewrite E1,E2. fmap_disjoint. } asserts C: (heap_compat h1' h). { split. { rewrite~ E2. } { rewrite E1,E2. lets: heap_disjoint_components h. - state_disjoint. } } + fmap_disjoint. } } exists (h1' \u h) (val_loc l). splits~. { rew_state~. applys~ red_ref. } { exists h1' h. split~. splits~. { exists l. applys~ himpl_inst_prop (l ~~> v). hnfs~. } { rew_heap in N. hhsimpl~. } } - { rew_heap~. rewrite E2. state_eq. } + { rew_heap~. rewrite E2. fmap_eq. } Qed. (* Lemma rule_get_ro : forall v l, @@ -694,10 +694,10 @@ Proof using. exists h v. splits~. { applys red_get. destruct N as (h1&h2&D&P1&P2&E). destruct P1 as (h11&(Q1&Q2)&E1&E2). - subst h. rewrite heap_state_def. (* todo: cleanup *) - rewrite state_union_comm_disjoint; [|rew_heap~]. + subst h. rewrite heap_fmap_def. (* todo: cleanup *) + rewrite fmap_union_comm_disjoint; [|rew_heap~]. rew_heap~. rewrite E1,E2,Q1,Q2. rew_state. - applys~ state_union_single_read. } + applys~ fmap_union_single_read. } { rewrite hprop_star_pure. split~. hhsimpl~. } Qed. @@ -706,19 +706,19 @@ Lemma rule_set : forall w l v, Proof using. intros. intros HF h N. destruct N as (h1&h2&D&P1&P2&E). destruct P1 as (Q1&Q2). - lets~ (h1'&E1'&E2'): heap_make (state_single l w) (state_empty:state). - asserts Dl: (state_disjoint (state_single l w) (heap_state h2)). + lets~ (h1'&E1'&E2'): heap_make (fmap_single l w) (fmap_empty:state). + asserts Dl: (fmap_disjoint (fmap_single l w) (heap_state h2)). { destruct D as (D1&D2). rewrite Q1 in D2. unstate. - applys state_disjoint_single_set v. auto. } + applys fmap_disjoint_single_set v. auto. } asserts C: (heap_compat h1' h2). { destruct D as (D1&D2). unfolds. rewrite E1',E2'. unfold heap_state in Dl. split~. } exists (h1' \u h2) val_unit. splits~. { applys red_set. rew_state~. rewrite E. (* todo: cleanup *) - rewrite (@heap_state_def h1'). rewrite (@heap_state_def h2). + rewrite (@heap_fmap_def h1'). rewrite (@heap_fmap_def h2). rewrite E1',E2'. rew_state~. - applys~ state_union_single_write v w. - rewrite (@heap_state_def h1). rewrite Q1,Q2. state_eq. } + applys~ fmap_union_single_write v w. + rewrite (@heap_fmap_def h1). rewrite Q1,Q2. fmap_eq. } { rew_heap. rewrite hprop_star_pure. split~. { exists h1' h2. splits~. { hnfs~. } diff --git a/model/LibState.v b/model/LibState.v deleted file mode 100644 index 5b56963dcc8d76ff3483a5dd3f5a29cd3e9c671f..0000000000000000000000000000000000000000 --- a/model/LibState.v +++ /dev/null @@ -1,766 +0,0 @@ -(** - -This file contains a representation of finite maps -that may be used for representing a store. It also -provides lemmas and tactics for reasoning about -operations on the store (read, write, union). - -Author: Arthur Charguéraud. -License: MIT. - -*) - -Set Implicit Arguments. -Require Import LibCore. - - -(************************************************************) - -Tactic Notation "cases" constr(E) := (* For TLC *) - let H := fresh "Eq" in cases E as H. - - -(********************************************************************) -(* * States *) - - -(*------------------------------------------------------------------*) -(** Existence of fresh locations *) - -(** These lemmas are useful to prove: - [forall h v, exists l, state_disjoint (state_single l v) h]. *) - -Definition loc_fresh_gen (L : list nat) := - (1 + fold_right plus O L)%nat. - -Lemma loc_fresh_ind : forall l L, - Mem l L -> (l < loc_fresh_gen L)%nat. -Proof using. - intros l L. unfold loc_fresh_gen. - induction L; introv M; inverts M; rew_list. - { math. } - { forwards~: IHL. math. } -Qed. - -Definition loc_fresh_property (A:Type) := - forall (L : list A), exists l, ~ Mem l L. - -Lemma loc_fresh_nat : loc_fresh_property nat. -Proof using. - intros L. exists (loc_fresh_gen L). intros M. - lets: loc_fresh_ind M. math. -Qed. - -Hint Resolve loc_fresh_nat. - - -(*------------------------------------------------------------------*) -(* ** Representation of partial functions *) - -(** Type of partial functions from A to B *) - -Definition pfun (A B : Type) := - A -> option B. - -(** Finite domain of a partial function *) - -Definition pfun_finite (A B : Type) (f : pfun A B) := - exists (L : list A), forall (x:A), f x <> None -> Mem x L. - -(** Disjointness of domain of two partial functions *) - -Definition pfun_disjoint (A B : Type) (f1 f2 : pfun A B) := - forall (x:A), f1 x = None \/ f2 x = None. - -(** Disjoint union of two partial functions *) - -Definition pfun_union (A B : Type) (f1 f2 : pfun A B) := - fun (x:A) => match f1 x with - | Some y => Some y - | None => f2 x - end. - -Definition pfun_agree (A B : Type) (f1 f2 : pfun A B) := - forall x v1 v2, - f1 x = Some v1 -> - f2 x = Some v2 -> - v1 = v2. - - -(*------------------------------------------------------------------*) -(** Representation of state *) - -Section State. -Variables loc : Type. -Variables val : Type. - -(** Representation of heaps *) - -Inductive state : Type := state_of { - state_data :> pfun loc val; - state_finite : pfun_finite state_data }. - -Implicit Arguments state_of []. - -(** Disjoint states *) - -Definition state_disjoint (h1 h2 : state) : Prop := - pfun_disjoint h1 h2. - -Definition state_disjoint_3 h1 h2 h3 := - state_disjoint h1 h2 /\ state_disjoint h2 h3 /\ state_disjoint h1 h3. - -(** Compatible states *) - -Definition state_agree (g1 g2 : state) := - pfun_agree g1 g2. - -(** Finiteness of union *) - -Lemma pfun_union_finite : forall (A B : Type) (f1 f2 : pfun A B), - pfun_finite f1 -> pfun_finite f2 -> pfun_finite (pfun_union f1 f2). -Proof using. - introv [L1 F1] [L2 F2]. exists (L1 ++ L2). introv M. - specializes F1 x. specializes F2 x. unfold pfun_union in M. - apply Mem_app_or. destruct~ (f1 x). -Qed. - -(** Union of states *) - -Program Definition state_union (h1 h2 : state) : state := - state_of (pfun_union h1 h2) _. -Next Obligation. destruct h1. destruct h2. apply~ pfun_union_finite. Qed. - -(** Empty state *) - -Program Definition state_empty : state := - state_of (fun l => None) _. -Next Obligation. exists (@nil loc). auto_false. Qed. - -(** Singleton state *) - -Program Definition state_single (l:loc) (v:val) : state := - state_of (fun l' => If l = l' then Some v else None) _. -Next Obligation. - exists (l::nil). intros. case_if. subst~. -Qed. - -(** Update of a state *) - -Definition state_update (h:state) (l:loc) (v:val) := - state_union (state_single l v) h. - (* Note: the union operation first reads in the first argument. *) - -(** Inhabited type [state] *) - -Global Instance state_inhab : Inhab state. -Proof using. intros. applys prove_Inhab state_empty. Qed. - -Notation "\# h1 h2" := (state_disjoint h1 h2) - (at level 40, h1 at level 0, h2 at level 0, no associativity) : state_scope. - -Notation "\# h1 h2 h3" := (state_disjoint_3 h1 h2 h3) - (at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity) - : state_scope. - -Notation "h1 \+ h2" := (state_union h1 h2) - (at level 51, right associativity) : state_scope. - -Open Scope state_scope. - - -(************************************************************) -(* * Lemmas *) - -(*------------------------------------------------------------------*) -(* ** Equality of states *) - -(** Symmetry of disjointness *) - -Lemma pfun_disjoint_sym : forall (A B : Type), - sym (@pfun_disjoint A B). -Proof using. - introv H. unfolds pfun_disjoint. intros z. specializes H z. intuition. -Qed. - -(** Commutativity of disjoint union *) - -Lemma pfun_union_comm : forall (A B : Type) (f1 f2 : pfun A B), - pfun_disjoint f1 f2 -> - pfun_union f1 f2 = pfun_union f2 f1. -Proof using. - introv H. extens. intros x. unfolds pfun_disjoint, pfun_union. - specializes H x. cases (f1 x); cases (f2 x); auto. destruct H; false. -Qed. - -(** Proving states equals *) - -Lemma state_eq : forall (f1 f2: loc -> option val) F1 F2, - (forall x, f1 x = f2 x) -> - state_of f1 F1 = state_of f2 F2. -Proof using. - introv H. asserts: (f1 = f2). extens~. subst. - fequals. (* note: involves proof irrelevance *) -Qed. - - -(*------------------------------------------------------------------*) -(* ** Properties on states *) - -(** Disjointness *) - -Lemma state_disjoint_sym : forall h1 h2, - \# h1 h2 -> \# h2 h1. -Proof using. intros [f1 F1] [f2 F2]. apply pfun_disjoint_sym. Qed. - -Lemma state_disjoint_comm : forall h1 h2, - \# h1 h2 = \# h2 h1. -Proof using. lets: state_disjoint_sym. extens*. Qed. - -Lemma state_disjoint_empty_l : forall h, - \# state_empty h. -Proof using. intros [f F] x. simple~. Qed. - -Lemma state_disjoint_empty_r : forall h, - \# h state_empty. -Proof using. intros [f F] x. simple~. Qed. - -Hint Resolve state_disjoint_sym state_disjoint_empty_l state_disjoint_empty_r. - -Lemma state_disjoint_union_eq_r : forall h1 h2 h3, - \# h1 (h2 \+ h3) = - (\# h1 h2 /\ \# h1 h3). -Proof using. - intros [f1 F1] [f2 F2] [f3 F3]. - unfolds state_disjoint, state_union. simpls. - unfolds pfun_disjoint, pfun_union. extens. iff M [M1 M2]. - split; intros x; specializes M x; - destruct (f2 x); intuition; tryfalse. - intros x. specializes M1 x. specializes M2 x. - destruct (f2 x); intuition. -Qed. - -Lemma state_disjoint_union_eq_l : forall h1 h2 h3, - \# (h2 \+ h3) h1 = - (\# h1 h2 /\ \# h1 h3). -Proof using. - intros. rewrite state_disjoint_comm. - apply state_disjoint_union_eq_r. -Qed. - -Lemma state_single_same_loc_disjoint : forall (l:loc) (v1 v2:val), - \# (state_single l v1) (state_single l v2) -> False. -Proof using. - introv D. specializes D l. simpls. case_if. destruct D; tryfalse. -Qed. - -Lemma state_disjoint_3_unfold : forall h1 h2 h3, - \# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3). -Proof using. auto. Qed. - -Lemma state_disjoint_new : forall null (h:state) v, - loc_fresh_property loc -> - exists l, \# (state_single l v) h /\ l <> null. -Proof using. - intros null (m&(L&M)) v HF. - unfold state_disjoint, pfun_disjoint. simpl. - lets (l&F): (HF (null::L)). - exists l. split. - { intros l'. case_if~. - { right. applys not_not_elim. intros H. applys F. - constructor. applys~ M. } } - { intro_subst. applys~ F. } -Qed. - -Lemma state_disjoint_single_set : forall (h:state) l v1 v2, - \# (state_single l v1) h -> - \# (state_single l v2) h. -Proof using. - introv M. unfolds state_disjoint, state_single, pfun_disjoint; simpls. - intros l'. specializes M l'. case_if~. destruct M; auto_false. -Qed. - -(** Union *) - -Lemma state_union_idempotent : forall h, - h \+ h = h. -Proof using. - intros [f F]. apply~ state_eq. simpl. intros x. - unfold pfun_union. cases~ (f x). -Qed. - -Lemma state_union_empty_l : forall h, - state_empty \+ h = h. -Proof using. - intros [f F]. unfold state_union, pfun_union, state_empty. simpl. - apply~ state_eq. -Qed. - -Lemma state_union_empty_r : forall h, - h \+ state_empty = h. -Proof using. - intros [f F]. unfold state_union, pfun_union, state_empty. simpl. - apply state_eq. intros x. destruct~ (f x). -Qed. - -Lemma state_union_eq_empty_inv_l : forall h1 h2, - h1 \+ h2 = state_empty -> - h1 = state_empty. -Proof using. - intros (f1&F1) (f2&F2) M. inverts M as M. - applys state_eq. intros l. - unfolds pfun_union. - lets: func_same_1 l M. - cases (f1 l); auto_false. -Qed. - -Lemma state_union_eq_empty_inv_r : forall h1 h2, - h1 \+ h2 = state_empty -> - h2 = state_empty. -Proof using. - intros (f1&F1) (f2&F2) M. inverts M as M. - applys state_eq. intros l. - unfolds pfun_union. - lets: func_same_1 l M. - cases (f1 l); auto_false. -Qed. - -Lemma state_union_comm_disjoint : forall h1 h2, - \# h1 h2 -> - h1 \+ h2 = h2 \+ h1. -Proof using. - intros [f1 F1] [f2 F2] H. simpls. apply state_eq. simpl. - intros. rewrite~ pfun_union_comm. -Qed. - -Lemma state_union_comm_agree : forall h1 h2, - state_agree h1 h2 -> - h1 \+ h2 = h2 \+ h1. -Proof using. - intros [f1 F1] [f2 F2] H. simpls. apply state_eq. simpl. - intros l. specializes H l. unfolds pfun_union. simpls. - cases (f1 l); cases (f2 l); auto. fequals. applys* H. -Qed. - -Lemma state_union_assoc : forall h1 h2 h3, - (h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3). -Proof using. - intros [f1 F1] [f2 F2] [f3 F3]. unfolds state_union. simpls. - apply state_eq. intros x. unfold pfun_union. destruct~ (f1 x). -Qed. - -Lemma pfun_eq_forward : forall (h1 h2 : state), - h1 = h2 -> - forall x, state_data h1 x = state_data h2 x. -Proof using. intros. fequals. Qed. - -(* -Lemma state_union_eq_inv : forall h2 h1 h1' : state, - \# h1 h2 -> - state_agree h1' h2 -> - h1 \+ h2 = h1' \+ h2 -> - h1 = h1'. -Proof using. - intros [f2 F2] [f1 F1] [f1' F1'] D D' E. - applys state_eq. intros x. specializes D x. specializes D' x. - lets E': pfun_eq_forward (rm E) x. simpls. - unfolds pfun_union. - cases (f1 x); cases (f2 x); try solve [cases (f1' x); destruct D; congruence ]. - destruct D; try false. - rewrite H in E'. inverts E'. - cases (f1' x); cases (f1 x); - destruct D; try congruence. - false. - destruct D'; try congruence. -Qed. -*) - -Lemma state_union_eq_inv : forall h2 h1 h1' : state, - \# h1 h2 -> - \# h1' h2 -> - h1 \+ h2 = h1' \+ h2 -> - h1 = h1'. -Proof using. - intros [f2 F2] [f1' F1'] [f1 F1] D D' E. - applys state_eq. intros x. specializes D x. specializes D' x. - lets E': pfun_eq_forward (rm E) x. simpls. - unfolds pfun_union. - cases (f1' x); cases (f1 x); - destruct D; try congruence; - destruct D'; try congruence. -Qed. - -(** Compatibility *) - -Lemma state_agree_refl : forall h, - state_agree h h. -Proof using. - intros h. introv M1 M2. congruence. -Qed. - -Lemma state_agree_sym : forall f1 f2, - state_agree f1 f2 -> - state_agree f2 f1. -Proof using. - introv M. intros l v1 v2 E1 E2. - specializes M l E1. -Qed. - -Lemma state_agree_disjoint : forall h1 h2, - state_disjoint h1 h2 -> - state_agree h1 h2. -Proof using. - introv HD. intros l v1 v2 M1 M2. destruct (HD l); false. -Qed. - -Lemma state_agree_empty_l : forall h, - state_agree state_empty h. -Proof using. intros h l v1 v2 E1 E2. simpls. false. Qed. - -Lemma state_agree_empty_r : forall h, - state_agree h state_empty. -Proof using. - hint state_agree_sym, state_agree_empty_l. eauto. -Qed. - -Lemma state_agree_union_l : forall f1 f2 f3, - state_agree f1 f3 -> - state_agree f2 f3 -> - state_agree (f1 \+ f2) f3. -Proof using. - introv M1 M2. intros l v1 v2 E1 E2. - specializes M1 l. specializes M2 l. - simpls. unfolds pfun_union. cases (state_data f1 l). - { inverts E1. applys* M1. } - { applys* M2. } -Qed. - -Lemma state_agree_union_r : forall f1 f2 f3, - state_agree f1 f2 -> - state_agree f1 f3 -> - state_agree f1 (f2 \+ f3). -Proof using. - hint state_agree_sym, state_agree_union_l. eauto. -Qed. - -Lemma state_agree_union_lr : forall f1 g1 f2 g2, - state_agree g1 g2 -> - \# f1 f2 (g1 \+ g2) -> - state_agree (f1 \+ g1) (f2 \+ g2). -Proof using. - introv M1 (M2a&M2b&M2c). - rewrite state_disjoint_union_eq_r in *. - applys state_agree_union_l; applys state_agree_union_r; - try solve [ applys* state_agree_disjoint ]. - auto. -Qed. - -Lemma state_agree_union_ll_inv : forall f1 f2 f3, - state_agree (f1 \+ f2) f3 -> - state_agree f1 f3. -Proof using. - introv M. intros l v1 v2 E1 E2. - specializes M l. simpls. unfolds pfun_union. - rewrite E1 in M. applys* M. -Qed. - -Lemma state_agree_union_rl_inv : forall f1 f2 f3, - state_agree f1 (f2 \+ f3) -> - state_agree f1 f2. -Proof using. - hint state_agree_union_ll_inv, state_agree_sym. eauto. -Qed. - -Lemma state_agree_union_lr_inv_agree_agree : forall f1 f2 f3, - state_agree (f1 \+ f2) f3 -> - state_agree f1 f2 -> - state_agree f2 f3. -Proof using. - introv M D. rewrite~ (@state_union_comm_agree f1 f2) in M. - applys* state_agree_union_ll_inv. -Qed. - -Lemma state_agree_union_rr_inv_agree : forall f1 f2 f3, - state_agree f1 (f2 \+ f3) -> - state_agree f2 f3 -> - state_agree f1 f3. -Proof using. - hint state_agree_union_lr_inv_agree_agree, state_agree_sym. eauto. -Qed. - -Lemma state_agree_union_l_inv : forall f1 f2 f3, - state_agree (f1 \+ f2) f3 -> - state_agree f1 f2 -> - state_agree f1 f3 - /\ state_agree f2 f3. -Proof using. - (* TODO: proofs redundant with others above *) - introv M2 M1. split. - { intros l v1 v2 E1 E2. - specializes M1 l v1 v2 E1. applys~ M2 l v1 v2. - unfold state_union, pfun_union; simpl. rewrite~ E1. } - { intros l v1 v2 E1 E2. - specializes M1 l. specializes M2 l. - unfolds state_union, pfun_union; simpls. - cases (state_data f1 l). - { applys eq_trans v. symmetry. applys~ M1. applys~ M2. } - { auto. } } -Qed. - -Lemma state_agree_union_r_inv : forall f1 f2 f3, - state_agree f1 (f2 \+ f3) -> - state_agree f2 f3 -> - state_agree f1 f2 - /\ state_agree f1 f3. -Proof using. - hint state_agree_sym. - intros. forwards~ (M1&M2): state_agree_union_l_inv f2 f3 f1. -Qed. - -(** Read and write operations *) - -Lemma state_union_single_read : forall f1 f2 l v, - f1 = state_single l v -> - state_data (f1 \+ f2) l = Some v. -Proof using. - intros. subst. simpl. unfold pfun_union. case_if~. -Qed. - -Lemma state_union_single_write : forall f1 f1' f2 l v v', - f1 = state_single l v -> - f1' = state_single l v' -> - (f1' \+ f2) = state_update (f1 \+ f2) l v'. -Proof using. - intros. subst. unfold state_update. - rewrite <- state_union_assoc. fequals. - applys state_eq. intros l'. - unfolds pfun_union, state_single; simpl. case_if~. -Qed. - -End State. - -Implicit Arguments state_empty [[loc] [val]]. -Implicit Arguments state_union_assoc [loc val]. -Implicit Arguments state_union_comm_disjoint [loc val]. -Implicit Arguments state_union_comm_agree [loc val]. - - -(************************************************************) -(* * Notation *) - -Notation "\# h1 h2" := (state_disjoint h1 h2) - (at level 40, h1 at level 0, h2 at level 0, no associativity) : state_scope. - -Notation "\# h1 h2 h3" := (state_disjoint_3 h1 h2 h3) - (at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity) - : state_scope. - -Notation "h1 \+ h2" := (state_union h1 h2) - (at level 51, right associativity) : state_scope. - -Open Scope state_scope. - - -(************************************************************) -(* * Tactics *) - -(*------------------------------------------------------------------*) -(* ** Proving disjointness results *) - -(** [state_disjoint] proves goals of the form [\# h1 h2] and - [\# h1 h2 h3] by expanding all hypotheses into binary forms - [\# h1 h2] and then exploiting symmetry and disjointness - with [state_empty]. *) - -Hint Resolve state_disjoint_sym state_disjoint_empty_l state_disjoint_empty_r. - -Hint Rewrite - state_disjoint_union_eq_l - state_disjoint_union_eq_r - state_disjoint_3_unfold : rew_disjoint. - -Tactic Notation "rew_disjoint" := - autorewrite with rew_disjoint in *. -Tactic Notation "rew_disjoint" "*" := - rew_disjoint; auto_star. - -Tactic Notation "state_disjoint" := - solve [ subst; rew_disjoint; jauto_set; auto ]. - -Tactic Notation "state_disjoint_if_needed" := - match goal with - | |- \# _ _ => state_disjoint - | |- \# _ _ _ => state_disjoint - end. - -Lemma state_disjoint_demo : forall A B (h1 h2 h3 h4 h5:state A B), - h1 = h2 \+ h3 -> - \# h2 h3 -> - \# h1 h4 h5 -> - \# h3 h2 h5 /\ \# h4 h5. -Proof using. - intros. dup 2. - { subst. rew_disjoint. jauto_set. auto. auto. auto. auto. } - { state_disjoint. } -Qed. - - -(*------------------------------------------------------------------*) -(* ** Tactic [state_eq] for proving equality of states, - and tactic [rew_state] to normalize state expressions. *) - -Section StateEq. -Variables (A B : Type). -Implicit Types h : state A B. - -(** [state_eq] proves equalities between unions of states. - It attempts to discharge the disjointness side-conditions. - Disclaimer: cancels heaps at depth up to 4, but no more. *) - -Lemma state_union_eq_cancel_1 : forall h1 h2 h2', - h2 = h2' -> - h1 \+ h2 = h1 \+ h2'. -Proof using. intros. subst. auto. Qed. - -Lemma state_union_eq_cancel_1' : forall h1, - h1 = h1. -Proof using. intros. auto. Qed. - -Lemma state_union_eq_cancel_2 : forall h1 h1' h2 h2', - \# h1 h1' -> - h2 = h1' \+ h2' -> - h1 \+ h2 = h1' \+ h1 \+ h2'. -Proof using. - intros. subst. rewrite <- state_union_assoc. - rewrite (state_union_comm_disjoint h1 h1'). - rewrite~ state_union_assoc. auto. -Qed. - -Lemma state_union_eq_cancel_2' : forall h1 h1' h2, - \# h1 h1' -> - h2 = h1' -> - h1 \+ h2 = h1' \+ h1. -Proof using. - intros. subst. apply~ state_union_comm_disjoint. -Qed. - -Lemma state_union_eq_cancel_3 : forall h1 h1' h2 h2' h3', - \# h1 (h1' \+ h2') -> - h2 = h1' \+ h2' \+ h3' -> - h1 \+ h2 = h1' \+ h2' \+ h1 \+ h3'. -Proof using. - intros. subst. - rewrite <- (state_union_assoc h1' h2' h3'). - rewrite <- (state_union_assoc h1' h2' (h1 \+ h3')). - apply~ state_union_eq_cancel_2. -Qed. - -Lemma state_union_eq_cancel_3' : forall h1 h1' h2 h2', - \# h1 (h1' \+ h2') -> - h2 = h1' \+ h2' -> - h1 \+ h2 = h1' \+ h2' \+ h1. -Proof using. - intros. subst. - rewrite <- (state_union_assoc h1' h2' h1). - apply~ state_union_eq_cancel_2'. -Qed. - -Lemma state_union_eq_cancel_4 : forall h1 h1' h2 h2' h3' h4', - \# h1 ((h1' \+ h2') \+ h3') -> - h2 = h1' \+ h2' \+ h3' \+ h4' -> - h1 \+ h2 = h1' \+ h2' \+ h3' \+ h1 \+ h4'. -Proof using. - intros. subst. - rewrite <- (state_union_assoc h1' h2' (h3' \+ h4')). - rewrite <- (state_union_assoc h1' h2' (h3' \+ h1 \+ h4')). - apply~ state_union_eq_cancel_3. -Qed. - -Lemma state_union_eq_cancel_4' : forall h1 h1' h2 h2' h3', - \# h1 (h1' \+ h2' \+ h3') -> - h2 = h1' \+ h2' \+ h3' -> - h1 \+ h2 = h1' \+ h2' \+ h3' \+ h1. -Proof using. - intros. subst. - rewrite <- (state_union_assoc h2' h3' h1). - apply~ state_union_eq_cancel_3'. -Qed. - -End StateEq. - -Hint Rewrite - state_union_assoc - state_union_empty_l - state_union_empty_r : rew_state. - -Tactic Notation "rew_state" := - autorewrite with rew_state in *. - -Tactic Notation "rew_state" "~" := - rew_state; auto_tilde. - -Tactic Notation "rew_state" "*" := - rew_state; auto_star. - -Ltac state_eq_step tt := - match goal with | |- ?G => match G with - | ?h1 = ?h1 => apply state_union_eq_cancel_1' - | ?h1 \+ ?h2 = ?h1 \+ ?h2' => apply state_union_eq_cancel_1 - | ?h1 \+ ?h2 = ?h1' \+ ?h1 => apply state_union_eq_cancel_2' - | ?h1 \+ ?h2 = ?h1' \+ ?h1 \+ ?h2' => apply state_union_eq_cancel_2 - | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h1 => apply state_union_eq_cancel_3' - | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h1 \+ ?h3' => apply state_union_eq_cancel_3 - | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h3' \+ ?h1 => apply state_union_eq_cancel_4' - | ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h3' \+ ?h1 \+ ?h4' => apply state_union_eq_cancel_4 - end end. - -Tactic Notation "state_eq" := - subst; - rew_state; - repeat (state_eq_step tt); - try state_disjoint_if_needed. - -Tactic Notation "state_eq" "~" := - state_eq; auto_tilde. - -Tactic Notation "state_eq" "*" := - state_eq; auto_star. - -Lemma state_eq_demo : forall A B (h1 h2 h3 h4 h5:state A B), - \# h1 h2 h3 -> - \# (h1 \+ h2 \+ h3) h4 h5 -> - h1 = h2 \+ h3 -> - h4 \+ h1 \+ h5 = h2 \+ h5 \+ h4 \+ h3. -Proof using. - intros. dup 2. - { subst. rew_state. - state_eq_step tt. state_disjoint. - state_eq_step tt. - state_eq_step tt. state_disjoint. auto. } - { state_eq. } -Qed. - -(*------------------------------------------------------------------*) -(* ** Tactic [state_red] for proving [red] goals modulo - equalities between states *) - -(** [state_red] proves a goal of the form [red h1 t h2 v] - using an hypothesis of the shape [red h1' t h2' v], - generating [h1 = h1'] and [h2 = h2'] as subgoals, and - attempting to solve them using the tactic [state_red]. *) - -Ltac state_red_base tt := fail. -(* Example: -Ltac state_red_base tt := - match goal with H: red _ ?t _ _ |- red _ ?t _ _ => - applys_eq H 2 4; try state_eq end. -*) - -Tactic Notation "state_red" := - state_red_base tt. - -Tactic Notation "state_red" "~" := - state_red; auto_tilde. - -Tactic Notation "state_red" "*" := - state_red; auto_star. diff --git a/model/MLCF.v b/model/MLCF.v index 82812176516f34d91237f05ef1a7866534e8d54f..37144ae6ab108de5abe4dcb09a0ff76c9e0a9510 100644 --- a/model/MLCF.v +++ b/model/MLCF.v @@ -16,7 +16,7 @@ Require Export LibFix MLSep. Open Scope heap_scope. -(********************************************************************) +(* ********************************************************************** *) (* ** Type of a formula *) (** A formula is a binary relation relating a pre-condition @@ -28,7 +28,7 @@ Global Instance formula_inhab : Inhab formula. Proof using. apply (prove_Inhab (fun _ _ => True)). Qed. -(********************************************************************) +(* ********************************************************************** *) (* ** The [local] predicate *) (** Nested applications [local] are redundant *) @@ -58,10 +58,10 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed. Hint Resolve local_is_local. -(********************************************************************) +(* ********************************************************************** *) (* ** Characteristic formula generator *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Input language for the characteristic formula generator, where functions are named by a let-binding. *) @@ -132,7 +132,7 @@ Fixpoint Trm_of_trm (t : trm) : Trm := end. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Size function used as measure for the CF generator: it computes the size of a term, where all values counting for one unit, including closures viewed as values. *) @@ -156,7 +156,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Proof that the reciprocal translation is indeed the reciprocal. *) Section Reciprocal. @@ -203,7 +203,7 @@ Qed. End Reciprocal. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of the [app] predicate *) (** The proposition [app f vs H Q] asserts that the application @@ -213,7 +213,7 @@ Definition app f vs H Q := triple (trm_app f vs) H Q. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of CF blocks *) (** These auxiliary definitions give the characteristic formula @@ -270,7 +270,7 @@ Definition cf_fail : formula := fun H Q => -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Instance of [app] for primitive operations *) (* LATER @@ -290,7 +290,7 @@ Proof using. applys rule_set. Qed. *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of the CF generator *) (** The CF generator is a recursive function, defined using the @@ -348,10 +348,10 @@ Ltac simpl_cf := rewrite cf_unfold; unfold cf_def. -(********************************************************************) +(* ********************************************************************** *) (* ** Soundness proof *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Two substitution lemmas for the soundness proof *) Hint Extern 1 (measure Trm_size _ _) => hnf; simpl; math. @@ -380,7 +380,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Soundness of the CF generator *) Lemma cf_local : forall T, @@ -443,7 +443,7 @@ Theorem cf_sound_final : forall (t:Trm) H Q, Proof using. intros. applys* cf_sound_induction. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Soundness result, practical versions *) Theorem cf_sound : forall (t:trm) H Q, @@ -472,7 +472,7 @@ Proof using. introv EF M. applys* cf_sound_app. Qed. -(********************************************************************) +(* ********************************************************************** *) (* ** CF tactics *) Module MLCFTactics. @@ -480,7 +480,7 @@ Module MLCFTactics. Ltac xlocal_core tt ::= try first [ applys local_is_local | applys is_local_triple | assumption ]. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Notation for characteristic formulae *) Notation "'Val' v" := diff --git a/model/MLCFLifted.v b/model/MLCFLifted.v index 34490b1f72767b647f180563351ea62cb750e046..34dc66999d1485a1be5b93289c557c32457525e5 100644 --- a/model/MLCFLifted.v +++ b/model/MLCFLifted.v @@ -21,11 +21,11 @@ Open Scope charac. Ltac auto_star ::= jauto. -(********************************************************************) +(* ********************************************************************** *) (* CF with Lifting *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Type of a formula *) (** A formula is a binary relation relating a pre-condition @@ -64,7 +64,7 @@ Definition App (f:func) (Vs:dyns) `{Enc A} H (Q:A->hprop) := Triple (trm_app f (encs Vs)) H Q. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** The [local] predicate *) Lemma Local_local : forall A `{EA:Enc A} (F:formula), @@ -85,7 +85,7 @@ Lemma App_is_local : forall (f:func) (Vs:dyns) A `{EA:Enc A}, Proof using. intros. unfold App. applys Triple_is_local. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of CF blocks *) (** These auxiliary definitions give the characteristic formula @@ -137,7 +137,7 @@ Definition Cf_fail : formula := fun `{Enc A} H (Q:A->hprop) => False. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Instance of [app] for primitive operations *) (* LATER @@ -154,7 +154,7 @@ Lemma app_set : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} l (V:A1) (W:A2), Proof using. intros. applys~ Rule_set. Qed. *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Auxiliary *) Lemma Trm_size_Subst : forall t E, @@ -165,7 +165,7 @@ Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of the CF generator *) Definition Cf_def Cf (t:Trm) : formula := @@ -226,10 +226,10 @@ Ltac simpl_Cf := rewrite Cf_unfold; unfold Cf_def. -(********************************************************************) +(* ********************************************************************** *) (* ** Soundness proof *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Two substitution lemmas for the soundness proof *) (** Substitution commutes with the translation from [Trm] to [trm] *) @@ -246,7 +246,7 @@ Lemma Trm_size_Subst_Trm_value : forall (t:Trm) (E:Ctx), Proof using. intros. applys Trm_size_subst_Trm_value. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Soundness of the CF generator *) Lemma Cf_local : forall A `{EA:Enc A} T, @@ -323,7 +323,7 @@ Theorem Cf_sound_final : forall (t:Trm) A `{EA:Enc A} H (Q:A->hprop), Proof using. intros. applys* Cf_sound_induction. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Soundness result, practical versions *) Theorem Cf_sound : forall (t:trm) A `{EA:Enc A} H (Q:A->hprop), @@ -352,7 +352,7 @@ Proof using. introv EF M. applys* Cf_sound_App. Qed. -(********************************************************************) +(* ********************************************************************** *) (* ** CFLifted tactics *) Module MLCFLiftedTactics. @@ -364,7 +364,7 @@ Ltac xlocal_core tt ::= | assumption ]. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Notation for characteristic formulae *) Notation "'Val' v" := @@ -502,7 +502,7 @@ Open Scope charac. End MLCFLiftedTactics. -(********************************************************************) +(* ********************************************************************** *) (* * Even number axiomatization for demos *) (* LATER @@ -519,7 +519,7 @@ Admitted. *) -(********************************************************************) +(* ********************************************************************** *) (* * Himpl demos *) (* LATER @@ -545,7 +545,7 @@ Qed. -(********************************************************************) +(* ********************************************************************** *) (* * DEPRECATED *) (* diff --git a/model/MLExamples.v b/model/MLExamples.v index c670d1122fd76da0c79c53e1543b29af0018b6f3..f065d685f21bf7907d4719e26270bfd218ba4430 100644 --- a/model/MLExamples.v +++ b/model/MLExamples.v @@ -17,7 +17,7 @@ Open Scope charac. Ltac auto_star ::= jauto. -(********************************************************************) +(* ********************************************************************** *) (* * Mutable lists *) (** Layout in memory: @@ -126,7 +126,7 @@ Parameter rule_get_tl : forall p x p', -(********************************************************************) +(* ********************************************************************** *) (* * Definition of the list increment program *) (** Program variables *) @@ -173,7 +173,7 @@ Hint Rewrite subst_val_mlist_length : rew_subst. Ltac simpl_subst := simpl; autorewrite with rew_subst. -(********************************************************************) +(* ********************************************************************** *) (* * Mutable list increment verification, using triples *) Section ProofWithTriples. @@ -208,7 +208,7 @@ Qed. End ProofWithTriples. -(********************************************************************) +(* ********************************************************************** *) (* * Demos of characteristic formulae *) Module MLCFDemo. @@ -220,7 +220,7 @@ Hint Extern 1 (RegisterSpec (app (val_prim prim_get) [_;val_field tl] _ _)) => Provide rule_get_tl. -(********************************************************************) +(* ********************************************************************** *) (* * Mutable list increment verification, using characteristic formulae, without tactics. *) @@ -254,7 +254,7 @@ Proof using. Qed. -(********************************************************************) +(* ********************************************************************** *) (* * Mutable list increment verification, using characteristic formulae *) (** Remark: in Ltac script below, "=>" is an alias for "intros" *) @@ -282,7 +282,7 @@ End MLCFDemo. -(********************************************************************) +(* ********************************************************************** *) (* * Demos of characteristic formulae *) Module MLCFLiftedDemo. @@ -291,7 +291,7 @@ Open Scope charac. -(********************************************************************) +(* ********************************************************************** *) (* * Mutable lists *) (** Layout in memory: @@ -416,12 +416,10 @@ Global Opaque MList. -(********************************************************************) +(* ********************************************************************** *) (* TODO: prove spec of primitives *) Open Scope charac. -Print Visibility. - (** Args contents *) @@ -477,7 +475,7 @@ Hint Extern 1 (RegisterSpec (App (val_prim prim_add) `[_ _] _ _)) => -(********************************************************************) +(* ********************************************************************** *) (* * Mutable list increment verification, using lifted characteristic formulae *) diff --git a/model/MLSemantics.v b/model/MLSemantics.v index 83f891165053e1b8c7b98a674939f07096ef74bb..e71d9b17c83c508a0a8ce746b2ecb943133e91f3 100644 --- a/model/MLSemantics.v +++ b/model/MLSemantics.v @@ -9,10 +9,10 @@ License: MIT. *) Set Implicit Arguments. -Require Export LibCore LibState. +Require Export LibCore Fmap. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* todo: reuse Coq's notation for lsits *) Notation "'[' x1 ']'" := (x1::nil) : list_scope. Notation "'[' x1 ; x2 ']'" := (x1::x2::nil) : list_scope. @@ -21,10 +21,10 @@ Notation "'[' x1 ; x2 ; x3 ; x4 ']'" := (x1::x2::x3::x4::nil) : list_scope. Open Scope list_scope. -(************************************************************) +(* ********************************************************************** *) (* * Source language syntax *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Representation of field names, variables and locations *) Definition field := Z. @@ -40,7 +40,7 @@ Definition null : loc := 0%nat. Global Opaque field var loc. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Syntax of the source language *) Inductive prim : Type := @@ -98,7 +98,7 @@ Coercion trm_val : val >-> trm. Coercion trm_app : val >-> Funclass. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Computable version of list operations *) Section Lists. @@ -136,7 +136,7 @@ End Lists. Infix "++" := list_app : vars_scope. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Computable version of association list operations *) Definition ctx := list (var*val). @@ -155,7 +155,7 @@ Fixpoint ctx_remove (L:vars) (E:ctx) : ctx := end. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Definition of capture-avoiding substitution *) Fixpoint subst_val (E:ctx) (v:val) : val := @@ -182,7 +182,7 @@ with subst_trm (E:ctx) (t:trm) : trm := end. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Free variables *) Section Freevars. @@ -286,37 +286,37 @@ Proof using. Qed. -(************************************************************) +(* ********************************************************************** *) (* * Source language semantics *) Section Red. -Local Open Scope state_scope. +Local Open Scope fmap_scope. Implicit Types t : trm. Implicit Types v : val. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) -Definition state := state (loc*field) val. +Definition state := fmap (loc*field) val. -Definition state_fresh_loc l (m:state) := - l <> null /\ forall f v, \# (state_single (l,f) v) m. +Definition fmap_fresh_loc l (m:state) := + l <> null /\ forall f v, \# (fmap_single (l,f) v) m. -Fixpoint state_record_key_values (l:loc) (ks:fields) (vs:vals) : state := +Fixpoint fmap_record_key_values (l:loc) (ks:fields) (vs:vals) : state := match ks,vs with - | nil,nil => state_empty - | (k::ks'),(v::vs') => state_union (state_single (l,k) v) (state_record_key_values l ks' vs') + | nil,nil => fmap_empty + | (k::ks'),(v::vs') => fmap_union (fmap_single (l,k) v) (fmap_record_key_values l ks' vs') | _,_ => arbitrary end. -Parameter state_record : forall (l:loc) (n:Z), state. -(* todo: fold state_single *) +Parameter fmap_record : forall (l:loc) (n:Z), state. +(* todo: fold fmap_single *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) Inductive red : state -> trm -> state -> val -> Prop := | red_val : forall m v, @@ -343,14 +343,14 @@ Inductive red : state -> trm -> state -> val -> Prop := red m1 (trm_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) m2 r -> red m1 (trm_while t1 t2) m2 r | red_alloc : forall ma mb l (n:int), - state_fresh_loc l ma -> - mb = state_record l n -> + fmap_fresh_loc l ma -> + mb = fmap_record l n -> red ma (prim_alloc [val_int n]) (mb \+ ma) (val_loc l) | red_get : forall m l k v, - state_data m (l,k) = Some v -> + fmap_data m (l,k) = Some v -> red m (prim_get [val_field k; val_loc l]) m v | red_set : forall m m' l k v, - m' = state_update m (l,k) v -> + m' = fmap_update m (l,k) v -> red m (prim_set [val_field k; val_loc l; v]) m' val_unit | red_add : forall m n1 n2 n', n' = n1 + n2 -> @@ -364,7 +364,7 @@ Inductive red : state -> trm -> state -> val -> Prop := End Red. -Local Open Scope state_scope. +Local Open Scope fmap_scope. (* TODO @@ -373,18 +373,18 @@ Parameter red_new_record : forall kvs, *) -(*------------------------------------------------------------------*) -(* ** Tactic [state_red] for proving [red] goals modulo +(* ---------------------------------------------------------------------- *) +(* ** Tactic [fmap_red] for proving [red] goals modulo equalities between states *) -Ltac state_red_base tt ::= +Ltac fmap_red_base tt ::= match goal with H: red _ ?t _ _ |- red _ ?t _ _ => - applys_eq H 2 4; try state_eq end. + applys_eq H 2 4; try fmap_eq end. -(********************************************************************) +(* ********************************************************************** *) (* * Notations *) Bind Scope trm_scope with trm. diff --git a/model/MLSep.v b/model/MLSep.v index 5fafd2d52d995f0dda88cebde5e3a1f9e79b3bf9..09d7e79b89ac6c201525cdbe7c2ca0161537cb28 100644 --- a/model/MLSep.v +++ b/model/MLSep.v @@ -11,18 +11,18 @@ License: MIT. Set Implicit Arguments. Require Export MLSemantics SepFunctor. -Open Scope state_scope. +Open Scope fmap_scope. Ltac auto_star ::= jauto. -(********************************************************************) +(* ********************************************************************** *) (* * Construction of core of the logic *) Module SepMLCore. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Types *) Definition heap : Type := (state)%type. @@ -30,24 +30,24 @@ Definition heap : Type := (state)%type. Definition hprop := heap -> Prop. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of heaps *) (** Definitions used for uniformity with other instantiation of the functor *) -Notation "'heap_empty'" := (state_empty : heap) : heap_scope. +Notation "'heap_empty'" := (fmap_empty : heap) : heap_scope. Open Scope heap_scope. -Notation "h1 \u h2" := (state_union h1 h2) +Notation "h1 \u h2" := (fmap_union h1 h2) (at level 51, right associativity) : heap_scope. -Definition heap_union_empty_l := state_union_empty_l. -Definition heap_union_empty_r := state_union_empty_r. -Definition heap_union_comm := state_union_comm_disjoint. +Definition heap_union_empty_l := fmap_union_empty_l. +Definition heap_union_empty_r := fmap_union_empty_r. +Definition heap_union_comm := fmap_union_comm_disjoint. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Operators *) (* \[] *) @@ -79,7 +79,7 @@ Definition hprop_gc := hprop_exists (fun (H:hprop) => H). -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Notation *) Notation "\[]" := (hprop_empty) @@ -92,21 +92,21 @@ Notation "\GC" := (hprop_gc) : heap_scope. Open Scope heap_scope. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic for automation *) (* TODO: check how much is really useful *) -Hint Extern 1 (_ = _ :> heap) => state_eq. +Hint Extern 1 (_ = _ :> heap) => fmap_eq. -Tactic Notation "state_disjoint_pre" := +Tactic Notation "fmap_disjoint_pre" := subst; rew_disjoint; jauto_set. -Hint Extern 1 (\# _ _) => state_disjoint_pre. -Hint Extern 1 (\# _ _ _) => state_disjoint_pre. +Hint Extern 1 (\# _ _) => fmap_disjoint_pre. +Hint Extern 1 (\# _ _ _) => fmap_disjoint_pre. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of empty *) Lemma hprop_empty_intro : @@ -119,7 +119,7 @@ Lemma hprop_empty_inv : forall h, Proof using. auto. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of star *) Section Properties. @@ -154,7 +154,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Interaction of star with other operators *) Lemma hprop_star_exists : forall A (J:A->hprop) H, @@ -176,19 +176,19 @@ End Properties. End SepMLCore. -(********************************************************************) +(* ********************************************************************** *) (* * Properties of the logic *) Module Export SepMLSetup := SepLogicSetup SepMLCore. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Singleton heap *) (** l . f ~> v *) Definition hprop_single (l:loc) (f:field) (v:val) : hprop := - fun h => h = state_single (l,f) v /\ l <> null. + fun h => h = fmap_single (l,f) v /\ l <> null. (* Notation for parsing *) Notation "l `.` f '~>' v" := (hprop_single l f v) @@ -220,7 +220,7 @@ Lemma hprop_star_single_same_loc_disjoint : forall (l:loc) (f:field) (v1 v2:val) (l `.` f ~> v1) \* (l`.`f ~> v2) ==> \[False]. Proof using. intros. unfold hprop_single. intros h (h1&h2&E1&E2&D&E). false. - subst. applys* state_single_same_loc_disjoint. + subst. applys* fmap_single_same_loc_disjoint. Qed. Implicit Arguments hprop_star_single_same_loc_disjoint []. @@ -235,7 +235,7 @@ Ltac hcancel_hook H ::= end. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Record representation *) (** Representation predicate [r ~> Record L], where [L] @@ -260,11 +260,11 @@ Qed. Global Opaque record. -(********************************************************************) +(* ********************************************************************** *) (* * Reasoning Rules *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of triples *) Definition triple t H Q := @@ -275,7 +275,7 @@ Definition triple t H Q := /\ (Q v \* \GC \* H') h'. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Structural rules *) Lemma rule_extract_exists : forall t (A:Type) (J:A->hprop) Q, @@ -330,7 +330,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Term rules *) Lemma rule_val : forall v H Q, @@ -494,7 +494,7 @@ Parameter rule_set : forall w l f v, -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Derived big-step specifications for get and set on records *) (* TODO: @@ -621,10 +621,10 @@ Parameter rule_set : forall w l f v, *) -(********************************************************************) +(* ********************************************************************** *) (* * Bonus *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Triples satisfy the [local] predicate *) Lemma is_local_triple : forall t, @@ -650,7 +650,7 @@ Ltac xlocal_core tt ::= *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Practical notation for triples *) Notation "'PRE' H 'CODE' t 'POST' Q " := diff --git a/model/MLSepLifted.v b/model/MLSepLifted.v index 567be3f7e0799e0e216472c5f09650be44dc3e18..f5feedef2e60fd0b21c41c0ca56e26cb97d166cf 100644 --- a/model/MLSepLifted.v +++ b/model/MLSepLifted.v @@ -25,17 +25,17 @@ Ltac auto_star ::= jauto. -(********************************************************************) +(* ********************************************************************** *) (* * Lifting *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Func type *) Definition func := val. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Encoders *) Class Enc (A:Type) := @@ -66,7 +66,7 @@ Proof using. Defined. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Representation of values packed with their type and encoder *) (** Representation of dependent pairs *) @@ -116,7 +116,7 @@ Definition encs (ds:dyns) : list val := List.map dyn_val ds. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Decoder *) Fixpoint decode (v:val) : dyn := @@ -161,7 +161,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Lemmas about encoders *) Lemma enc_val_fix_eq : forall F f x t1, @@ -170,7 +170,7 @@ Lemma enc_val_fix_eq : forall F f x t1, Proof using. intros. subst~. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Lifting heap predicates *) Definition hprop_single_enc `{EA:Enc A} (l:loc) (f:field) (V:A) := @@ -188,7 +188,7 @@ Ltac hcancel_hook H ::= | @hprop_single_enc _ _ _ _ _ => hcancel_try_same tt end. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Record representation *) (** Representation predicate [r ~> Record L], where [L] @@ -216,7 +216,7 @@ Qed. Global Opaque Record. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Lifting of postconditions *) Definition PostEnc `{Enc A} (Q:A->hprop) : val->hprop := @@ -240,7 +240,7 @@ Qed. Hint Resolve PostEnc_himpl. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Lifting of substitution *) Definition Ctx := list (var * dyn). @@ -258,14 +258,14 @@ Definition Subst_trm (E:list(var*dyn)) (t:trm) : trm := -(********************************************************************) +(* ********************************************************************** *) (* * Lifting of triples *) Definition Triple (t:trm) `{EA:Enc A} (H:hprop) (Q:A->hprop) := triple t H (PostEnc Q). -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Lifting of structural rules *) Lemma Rule_extract_exists : forall t `{Enc A} (J:A->hprop) (Q:A->hprop), @@ -305,7 +305,7 @@ Lemma Rule_gc_pre : forall t H Q, Proof using. introv M. applys* rule_gc_pre. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Lifting of term rules *) Lemma Rule_val : forall A `{EA:Enc A} (V:A) v H (Q:A->hprop), diff --git a/model/Makefile b/model/Makefile index 3d6b8d03c1ba2f91feb581e8086a2a8a8ab812bb..e3b9902b3d016b5d62656ce676acce8d21b62f6d 100644 --- a/model/Makefile +++ b/model/Makefile @@ -15,9 +15,9 @@ include \$(CFML)/Makefile.common SRC := \$(shell cat FILES) ifeq (\$(ARTHUR),1) - # LibState SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits + # Fmap SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits # LambdaExamples - SRC := LibState SepFunctor MLSemantics MLSep MLSepLifted MLCF MLCFLifted MLExamples + SRC := Fmap SepFunctor MLSemantics MLSep MLSepLifted MLCF MLCFLifted MLExamples LambdaSemantics LambdaSep LambdaSepCredits LambdaSepRO LambdaCF LambdaCFCredits endif PWD := \$(shell pwd) diff --git a/model/SepFunctor.v b/model/SepFunctor.v index ca81ff709f5dd6c5bd23c8e2b3db511bb7332045..1e18362f16f1e08eeca6afb15d00a94e4b4bd737 100644 --- a/model/SepFunctor.v +++ b/model/SepFunctor.v @@ -38,10 +38,10 @@ Ltac is_evar_as_bool E := | exact false ])). -(********************************************************************) +(* ********************************************************************** *) (** * Entailment *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition of entailment *) (** TLC defines [pred_le P Q] as [forall x, P x -> Q x]. *) @@ -57,7 +57,7 @@ Notation "P ===> Q" := (rel_le P Q) Open Scope heap_scope. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of entailment *) Section HimplProp. @@ -114,7 +114,7 @@ Implicit Arguments himpl_antisym [A H1 H2]. Hint Resolve himpl_refl rel_le_refl. -(********************************************************************) +(* ********************************************************************** *) (** * Abstract predicates for the Separation Logic *) Module Type SepLogicCore. @@ -181,7 +181,7 @@ Parameter himpl_frame_l : forall H2 H1 H1', End SepLogicCore. -(********************************************************************) +(* ********************************************************************** *) (** * Functor *) Module SepLogicSetup (SL : SepLogicCore). @@ -191,7 +191,7 @@ Implicit Types h : heap. Implicit Types H : hprop. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Representation predicates *) Definition repr (A:Type) (S:A->hprop) (x:A) : hprop := @@ -203,7 +203,7 @@ Definition Id {A:Type} (X:A) (x:A) := \[ X = x ]. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Notation *) Notation "x '~>' S" := (repr S x) @@ -244,14 +244,14 @@ Notation "\GC" := (hprop_gc) : heap_scope. Open Scope heap_scope. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of types *) Global Instance hprop_inhab : Inhab hprop. Proof using. intros. apply (prove_Inhab hprop_empty). Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Derived properties of [hprop] operators *) Lemma hprop_star_empty_r : forall H, @@ -305,7 +305,7 @@ Lemma hprop_gc_intro : forall h, Proof using. intros. exists~ (=h). Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Derived properties of [himpl] *) Lemma himpl_frame_r : forall H1 H2 H2', @@ -361,14 +361,14 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Opaque operators *) Global Opaque hprop_empty hprop_pure hprop_star hprop_exists hprop_gc. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Derived reasoning rules *) Lemma rule_extract_prop_from_extract_exists : @@ -390,14 +390,14 @@ Implicit Arguments rule_extract_prop_from_extract_exists [T]. -(*------------------------------------------------------------------*) -(*------------------------------------------------------------------*) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) +(* ---------------------------------------------------------------------- *) +(* ---------------------------------------------------------------------- *) (* TODO: move the remaining of this file to a different file *) -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** [rew_heap] tactic to normalize expressions with [hprop_star] *) Lemma star_post_empty : forall B (Q:B->hprop), @@ -429,7 +429,7 @@ Tactic Notation "rew_heap" "*" "in" hyp(H) := rew_heap in H; auto_star. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Auxiliary lemmas useful for manual proofs *) Lemma hprop_star_comm_assoc : forall H1 H2 H3, @@ -441,7 +441,7 @@ Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Auxiliary tactics used by many tactics *) (* [xprecondition tt] returns the current pre-condition. *) @@ -466,7 +466,7 @@ Ltac xpostcondition_is_evar tt := is_evar_as_bool Q. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** Auxiliary tactics used by [hpull] and [hsimpl] *) Ltac remove_empty_heaps_from H := @@ -513,7 +513,7 @@ Ltac remove_empty_heaps_formula tt := -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (** [hpull] tactic for extraction from [H1] on a goal [H1 ==> H2] *) (** Lemmas *) @@ -639,7 +639,7 @@ Proof using. Abort. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic [hpull_check] tests whether it would be useful to call [hpull] to extract things from the precondition. Applies to a goal of the form [H ==> H']. *) @@ -693,7 +693,7 @@ Lemma hpull_check_demo_2 : forall H1 H2 H3 H, Proof using. intros. (* hpull_check tt. --> blocks *) Abort. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic [hsimpl] to simplify a goal [H1 ==> H2] by cancelling equal items, and instantiating existentials from [H2]. *) @@ -1200,7 +1200,7 @@ Proof using. Abort. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic [hhsimpl] to prove [H h] from [H' h] *) Ltac hhsimpl_core := @@ -1214,7 +1214,7 @@ Tactic Notation "hhsimpl" "~" := hhsimpl; auto_tilde. Tactic Notation "hhsimpl" "*" := hhsimpl; auto_star. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic [hchange] *) Lemma hchange_lemma : forall H1 H1' H H' H2, @@ -1301,7 +1301,7 @@ Tactic Notation "hchange" constr(E1) constr(E2) constr(E3) := hchange E1; hchange E2 E3. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic [xunfold] to unfold heap predicates *) Tactic Notation "ltac_set" "(" ident(X) ":=" constr(E) ")" "at" constr(K) := @@ -1439,7 +1439,7 @@ Tactic Notation "xunfold" constr(E) "at" constr(n) := -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Definition and properties of [local] *) (** Type of characteristic formulae on values of type B *) @@ -1468,7 +1468,7 @@ Definition is_local_pred A B (S:A->~~B) := forall x, is_local (S x). -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Properties of [local] *) (** The [local] operator can be freely erased from a conclusion *) @@ -1670,7 +1670,7 @@ Proof using. Qed. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic [xlocal] to prove side-conditions of the form [local F]. *) Ltac xlocal_core tt := @@ -1680,7 +1680,7 @@ Tactic Notation "xlocal" := xlocal_core tt. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic [xpull_check] tests whether it would be useful to call [xpull] to extract things from the precondition. Applies to a goal of the form [F H Q]. *) @@ -1690,7 +1690,7 @@ Ltac xpull_check tt := hpull_check_rec H. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** Tactic [xpull] to extract existentials and pure facts from pre-conditions. *) @@ -1773,7 +1773,7 @@ Tactic Notation "xpull" "~" := xpull; auto_tilde. Tactic Notation "xpull" "*" := xpull; auto_star. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) (* ** [xapply] and [xapplys] *) (** [xapply E] applies a lemma [E] modulo frame/weakening. @@ -1943,7 +1943,7 @@ Tactic Notation "xspec" constr(f) := ltac_database_get database_spec f. -(*------------------------------------------------------------------*) +(* ---------------------------------------------------------------------- *) Global Opaque repr.