Commit 3d310509 by charguer

### renaming_fmap

parent 556f9fd9
 LibState Fmap LambdaSemantics SepFunctor LambdaSep ... ...
 ... ... @@ -14,36 +14,36 @@ Set Implicit Arguments. Require Import LibCore. (************************************************************) (* ********************************************************************** *) Tactic Notation "cases" constr(E) := (* For TLC *) Tactic Notation "cases" constr(E) := (* TODO For TLC *) let H := fresh "Eq" in cases E as H. (********************************************************************) (* * States *) (* ********************************************************************** *) (** * Fresh locations *) (*------------------------------------------------------------------*) (** Existence of fresh locations *) (* ---------------------------------------------------------------------- *) (** ** Existence of fresh locations *) (** These lemmas are useful to prove: [forall h v, exists l, state_disjoint (state_single l v) h]. *) [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 l L, Mem l L -> (l < loc_fresh_gen L)%nat. Lemma loc_fresh_ind : forall x L, Mem x L -> (x < loc_fresh_gen L)%nat. Proof using. intros l L. unfold loc_fresh_gen. 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 l, ~ Mem l L. forall (L:list A), exists (x:A), ~ Mem x L. Lemma loc_fresh_nat : loc_fresh_property nat. Proof using. ... ... @@ -54,216 +54,251 @@ Qed. Hint Resolve loc_fresh_nat. (*------------------------------------------------------------------*) (* ** Representation of partial functions *) (* ********************************************************************** *) (** * Maps (partial functions) *) (* ---------------------------------------------------------------------- *) (* ** Representation *) (** Type of partial functions from A to B *) Definition pfun (A B : Type) := Definition map (A B : Type) : 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. (* ---------------------------------------------------------------------- *) (* ** Operations *) (** Disjoint union of two partial functions *) Definition pfun_union (A B : Type) (f1 f2 : pfun A B) := 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. 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. (** 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. (*------------------------------------------------------------------*) (** Representation of state *) (** Disjointness of domain of two partial functions *) Section State. Variables loc : Type. Variables val : Type. Definition map_disjoint (A B : Type) (f1 f2 : map A B) := forall (x:A), f1 x = None \/ f2 x = None. (** Representation of heaps *) (** 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. Inductive state : Type := state_of { state_data :> pfun loc val; state_finite : pfun_finite state_data }. Implicit Arguments state_of []. (* ---------------------------------------------------------------------- *) (** Properties *) (** Disjoint states *) Section MapOps. Variables (A B : Type). Implicit Types f : map A B. Definition state_disjoint (h1 h2 : state) : Prop := pfun_disjoint h1 h2. (** Symmetry of disjointness *) Definition state_disjoint_3 h1 h2 h3 := state_disjoint h1 h2 /\ state_disjoint h2 h3 /\ state_disjoint h1 h3. Lemma map_disjoint_sym : sym (@map_disjoint A B). Proof using. introv H. unfolds map_disjoint. intros z. specializes H z. intuition. Qed. (** Compatible states *) (** Commutativity of disjoint union *) Definition state_agree (g1 g2 : state) := pfun_agree g1 g2. 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 pfun_union_finite : forall (A B : Type) (f1 f2 : pfun A B), pfun_finite f1 -> pfun_finite f2 -> pfun_finite (pfun_union f1 f2). 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 pfun_union in M. specializes F1 x. specializes F2 x. unfold map_union in M. apply Mem_app_or. destruct~ (f1 x). Qed. (** Union of states *) End MapOps. (* ********************************************************************** *) (** * Finite maps *) (* ---------------------------------------------------------------------- *) (** Definitions *) Inductive fmap (A B : Type) : Type := fmap_make { fmap_data :> map A B; fmap_finite : map_finite fmap_data }. 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. Implicit Arguments fmap_make [A B]. (** Empty state *) Program Definition state_empty : state := state_of (fun l => None) _. Next Obligation. exists (@nil loc). auto_false. Qed. (* ---------------------------------------------------------------------- *) (** Operations *) (** Singleton state *) (** Empty fmap *) Program Definition state_single (l:loc) (v:val) : state := state_of (fun l' => If l = l' then Some v else None) _. 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 (l::nil). intros. case_if. subst~. exists (x::nil). intros. case_if. subst~. Qed. (** Update of a state *) (** 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. Definition state_update (h:state) (l:loc) (v:val) := state_union (state_single l v) h. 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. *) (** Inhabited type [state] *) Global Instance state_inhab : Inhab state. Proof using. intros. applys prove_Inhab state_empty. Qed. (* ---------------------------------------------------------------------- *) (** Properties *) Notation "\# h1 h2" := (state_disjoint h1 h2) (at level 40, h1 at level 0, h2 at level 0, no associativity) : state_scope. (** Inhabited type [fmap] *) 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. Global Instance Inhab_fmap A B : Inhab (fmap A B). Proof using. intros. applys prove_Inhab (@fmap_empty A B). Qed. Notation "h1 \+ h2" := (state_union h1 h2) (at level 51, right associativity) : state_scope. (** Compatible fmaps *) Open Scope state_scope. Definition fmap_agree A B (h1 h2:fmap A B) := map_agree h1 h2. (** Disjoint fmaps *) (************************************************************) (* * Lemmas *) Definition fmap_disjoint A B (h1 h2 : fmap A B) : Prop := map_disjoint h1 h2. (*------------------------------------------------------------------*) (* ** Equality of states *) Notation "\# h1 h2" := (fmap_disjoint h1 h2) (at level 40, h1 at level 0, h2 at level 0, no associativity) : fmap_scope. (** Symmetry of disjointness *) (** Three disjoint fmaps *) 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. Definition fmap_disjoint_3 A B (h1 h2 h3 : fmap A B) := fmap_disjoint h1 h2 /\ fmap_disjoint h2 h3 /\ fmap_disjoint h1 h3. (** Commutativity of disjoint union *) 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. 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, (* ********************************************************************** *) (* * 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) -> state_of f1 F1 = state_of f2 F2. fmap_make f1 F1 = fmap_make f2 F2. Proof using. introv H. asserts: (f1 = f2). extens~. subst. fequals. (* note: involves proof irrelevance *) introv H. asserts: (f1 = f2). { unfold map. extens~. } subst. fequals. (* note: involves proof irrelevance *) Qed. (*------------------------------------------------------------------*) (* ** Properties on states *) (* ---------------------------------------------------------------------- *) (* ** Disjointness *) (** Disjointness *) Lemma state_disjoint_sym : forall h1 h2, Lemma fmap_disjoint_sym : forall h1 h2, \# h1 h2 -> \# h2 h1. Proof using. intros [f1 F1] [f2 F2]. apply pfun_disjoint_sym. Qed. Proof using. intros [f1 F1] [f2 F2]. apply map_disjoint_sym. Qed. Lemma state_disjoint_comm : forall h1 h2, Lemma fmap_disjoint_comm : forall h1 h2, \# h1 h2 = \# h2 h1. Proof using. lets: state_disjoint_sym. extens*. Qed. Proof using. lets: fmap_disjoint_sym. extens*. Qed. Lemma state_disjoint_empty_l : forall h, \# state_empty h. Lemma fmap_disjoint_empty_l : forall h, \# fmap_empty h. Proof using. intros [f F] x. simple~. Qed. Lemma state_disjoint_empty_r : forall h, \# h state_empty. Lemma fmap_disjoint_empty_r : forall h, \# h fmap_empty. Proof using. intros [f F] x. simple~. Qed. Hint Resolve state_disjoint_sym state_disjoint_empty_l state_disjoint_empty_r. Hint Resolve fmap_disjoint_sym fmap_disjoint_empty_l fmap_disjoint_empty_r. Lemma state_disjoint_union_eq_r : forall h1 h2 h3, 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 state_disjoint, state_union. simpls. unfolds pfun_disjoint, pfun_union. extens. iff M [M1 M2]. 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 state_disjoint_union_eq_l : forall h1 h2 h3, Lemma fmap_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. intros. rewrite fmap_disjoint_comm. apply fmap_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. 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 l. simpls. case_if. destruct D; tryfalse. introv D. specializes D x. simpls. case_if. destruct D; tryfalse. Qed. Lemma state_disjoint_3_unfold : forall h1 h2 h3, Lemma fmap_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. 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 state_disjoint, pfun_disjoint. simpl. unfold fmap_disjoint, map_disjoint. simpl. lets (l&F): (HF (null::L)). exists l. split. { intros l'. case_if~. ... ... @@ -272,99 +307,101 @@ Proof using. { 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. 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 state_disjoint, state_single, pfun_disjoint; simpls. introv M. unfolds fmap_disjoint, fmap_single, map_disjoint; simpls. intros l'. specializes M l'. case_if~. destruct M; auto_false. Qed. (** Union *) Lemma state_union_idempotent : forall h, (* ---------------------------------------------------------------------- *) (* ** Union *) Lemma fmap_union_idempotent : forall h, h \+ h = h. Proof using. intros [f F]. apply~ state_eq. simpl. intros x. unfold pfun_union. cases~ (f x). intros [f F]. apply~ fmap_eq. simpl. intros x. unfold map_union. cases~ (f x). Qed. Lemma state_union_empty_l : forall h, state_empty \+ h = h. Lemma fmap_union_empty_l : forall h, fmap_empty \+ h = h. Proof using. intros [f F]. unfold state_union, pfun_union, state_empty. simpl. apply~ state_eq. intros [f F]. unfold fmap_union, map_union, fmap_empty. simpl. apply~ fmap_eq. Qed. Lemma state_union_empty_r : forall h, h \+ state_empty = h. Lemma fmap_union_empty_r : forall h, h \+ fmap_empty = h. Proof using. intros [f F]. unfold state_union, pfun_union, state_empty. simpl. apply state_eq. intros x. destruct~ (f x). intros [f F]. unfold fmap_union, map_union, fmap_empty. simpl. apply fmap_eq. intros x. destruct~ (f x). Qed. Lemma state_union_eq_empty_inv_l : forall h1 h2, h1 \+ h2 = state_empty -> h1 = state_empty. 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 state_eq. intros l. unfolds pfun_union. applys fmap_eq. intros l. unfolds map_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. 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 state_eq. intros l. unfolds pfun_union. applys fmap_eq. intros l. unfolds map_union. lets: func_same_1 l M. cases (f1 l); auto_false. Qed. Lemma state_union_comm_disjoint : forall h1 h2, Lemma fmap_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. intros [f1 F1] [f2 F2] H. simpls. apply fmap_eq. simpl. intros. rewrite~ map_union_comm. Qed. Lemma state_union_comm_agree : forall h1 h2, state_agree h1 h2 -> 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 state_eq. simpl. intros l. specializes H l. unfolds pfun_union. simpls. 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 state_union_assoc : forall h1 h2 h3, Lemma fmap_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). intros [f1 F1] [f2 F2] [f3 F3]. unfolds fmap_union. simpls. apply fmap_eq. intros x. unfold map_union. destruct~ (f1 x). Qed. Lemma pfun_eq_forward : forall (h1 h2 : state), Lemma map_eq_forward : forall h1 h2, h1 = h2 -> forall x, state_data h1 x = state_data h2 x. forall x, fmap_data h1 x = fmap_data h2 x. Proof using. intros. fequals. Qed. (* Lemma state_union_eq_inv : forall h2 h1 h1' : state, Lemma fmap_union_eq_inv : forall h2 h1 h1' : fmap, \# h1 h2 -> state_agree 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 state_eq. intros x. specializes D x. specializes D' x. lets E': pfun_eq_forward (rm E) x. simpls. unfolds pfun_union. 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'. ... ... @@ -375,225 +412,212 @@ Proof using. Qed. *) Lemma state_union_eq_inv : forall h2 h1 h1' : state, 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 state_eq. intros x. specializes D x. specializes D' x. lets E': pfun_eq_forward (rm E) x. simpls. unfolds pfun_union. 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 state_agree_refl : forall h, state_agree h h. (* ---------------------------------------------------------------------- *) (* ** Compatibility *) Lemma fmap_agree_refl : forall h, fmap_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. 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 state_agree_disjoint : forall h1 h2, state_disjoint h1 h2 -> state_agree h1 h2. 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 state_agree_empty_l : forall h, state_agree state_empty h. 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 state_agree_empty_r : forall h, state_agree h state_empty. Lemma fmap_agree_empty_r : forall h, fmap_agree h fmap_empty. Proof using. hint state_agree_sym, state_agree_empty_l. eauto. hint fmap_agree_sym, fmap_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. 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 pfun_union. cases (state_data f1 l). simpls. unfolds map_union. cases (fmap_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). 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 state_agree_sym, state_agree_union_l. eauto. hint fmap_agree_sym, fmap_agree_union_l. eauto. Qed. Lemma state_agree_union_lr : forall f1 g1 f2 g2, state_agree g1 g2 -> Lemma fmap_agree_union_lr : forall f1 g1 f2 g2, fmap_agree g1 g2 -> \# f1 f2 (g1 \+ g2) -> state_agree (f1 \+ g1) (f2 \+ g2). fmap_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;