(* * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor. * *) Require Import base. Require Import sepalg. Require Import sepalg_generators. Require Import boolean_alg. Require Import tree_shares. Module Type SHARE. Parameter t:Type. Parameter sa:sepalg t. Existing Instance sa. Parameter top:t. Parameter bot:t. Axiom bot_identity : identity bot. Axiom top_correct : forall x:t, join_sub x top. Axiom shares_nontrivial : top <> bot. Axiom cross_split : forall a b c d z, join a b z -> join c d z -> { x:(t*t*t*t) & match x with (ac,ad,bc,bd) => join ac ad a /\ join bc bd b /\ join ac bc c /\ join ad bd d end }. (* Splitting stuff *) Parameter split : t -> t * t. Axiom split_join : forall x1 x2 x, split x = (x1,x2) -> join x1 x2 x. Axiom split_nontrivial : forall x1 x2 x, split x = (x1, x2) -> (identity x1 \/ identity x2) -> identity x. (* Token factory stuff *) Parameter isTokenFactory : t -> nat -> Prop. Parameter isToken : t -> nat -> Prop. Parameter splitToken : forall fac x n, isTokenFactory fac x -> { fac':t & {tok:t | isTokenFactory fac' (n+x) /\ isToken tok n /\ join fac' tok fac}}. Axiom absorbToken : forall fac x n, { fac':t & {tok:t | isTokenFactory fac' (n+x) /\ isToken tok n /\ join fac' tok fac}} -> isTokenFactory fac x. Axiom mergeToken : forall tok1 n1 tok2 n2 tok', isToken tok1 n1 -> isToken tok2 n2 -> join tok1 tok2 tok' -> isToken tok' (n1+n2). Axiom unmergeToken : forall tok n1 n2, isToken tok (n1+n2) -> { tok1:t & { tok2:t & isToken tok1 n1 /\ isToken tok2 n2 /\ join tok1 tok2 tok }}. Axiom factoryOverlap : forall f1 f2 n1 n2, isTokenFactory f1 n1 -> isTokenFactory f2 n2 -> joins f1 f2 -> False. Axiom fullFactory : forall x, isTokenFactory x 0 <-> x = top. Axiom identityToken : forall x, isToken x 0 <-> identity x. Axiom nonidentityToken : forall x n, (n > 0)%nat -> isToken x n -> nonidentity x. Axiom nonidentityFactory : forall x n, isTokenFactory x n -> nonidentity x. (* Relativization stuff *) Parameter rel : t -> t -> t. Axiom rel_leq : forall a x, join_sub (rel a x) a. Axiom rel_inj_l : forall a x y, a <> bot -> rel a x = rel a y -> x = y. Axiom rel_inj_r : forall a b x, x <> bot -> rel a x = rel b x -> a = b. Axiom rel_assoc : forall x y z, rel x (rel y z) = rel (rel x y) z. Axiom rel_bot1 : forall a, rel a bot = bot. Axiom rel_bot2 : forall x, rel bot x = bot. Axiom rel_top1 : forall a, rel a top = a. Axiom rel_top2 : forall x, rel top x = x. Axiom rel_join : forall a x y z, join x y z -> join (rel a x) (rel a y) (rel a z). Axiom rel_join2 : forall a x y s, nonidentity a -> join (rel a x) (rel a y) s -> exists z, s = rel a z /\ join x y z. Axiom rel_nontrivial : forall a x, identity (rel a x) -> (identity a \/ identity x). End SHARE. Module Share : SHARE. Import TreeLattice. Definition t:=t. Definition sa:=ba_sa. Definition top := top. Definition bot := bot. Theorem leq_join_sub : forall s1 s2:t, s1 <= s2 <-> join_sub s1 s2. Proof. split; intros. pose (s' := glb s2 (comp s1)). exists s'. simpl; split. subst s'. rewrite glb_commute. rewrite glb_assoc. rewrite (glb_commute (comp s1) s1). rewrite comp2. apply glb_bot. subst s'. rewrite distrib2. rewrite comp1. rewrite glb_top. rewrite <- ord_spec2; auto. destruct H as [s' H]. destruct H. rewrite ord_spec2. rewrite <- H0. rewrite <- lub_assoc. rewrite lub_idem; auto. Qed. Lemma top_correct : forall x:t, join_sub x top. Proof. intros; rewrite <- leq_join_sub; auto with ba. Qed. Lemma bot_identity : identity bot. Proof. hnf; intros. destruct H. rewrite lub_commute in H0. rewrite lub_bot in H0. auto. Qed. Lemma shares_nontrivial : top <> bot. Proof. exact lat_nontrivial. Qed. Lemma identity_share_bot : forall s, identity s -> s = Share.bot. Proof. intros. apply identities_unique; auto. apply bot_identity. exists s. apply join_com. destruct (top_correct s). assert (x = top). apply H; auto. subst x; auto. destruct (top_correct bot). assert (x = top). apply bot_identity; auto. subst x; auto. apply join_com in H1. destruct (join_assoc _ _ _ _ _ H0 H1); intuition. assert (x = top). apply H; auto. subst x. replace bot with s. rewrite identity_unit_equiv in H. trivial. apply joins_units_eq with top bot; firstorder. Qed. Definition isTokenFactory : t -> nat -> Prop := TokenFactory.isTokenFactory. Definition isToken : t -> nat -> Prop := TokenFactory.isToken. Definition splitToken : forall fac x n, isTokenFactory fac x -> { fac':t & {tok:t | isTokenFactory fac' (n+x) /\ isToken tok n /\ join fac' tok fac}} := TokenFactory.splitToken. Definition absorbToken : forall fac x n, { fac':t & {tok:t | isTokenFactory fac' (n+x) /\ isToken tok n /\ join fac' tok fac}} -> isTokenFactory fac x := TokenFactory.absorbToken. Definition mergeToken : forall tok1 n1 tok2 n2 tok', isToken tok1 n1 -> isToken tok2 n2 -> join tok1 tok2 tok' -> isToken tok' (n1+n2) := TokenFactory.mergeToken. Definition unmergeToken : forall tok n1 n2, isToken tok (n1+n2) -> { tok1:t & { tok2:t & isToken tok1 n1 /\ isToken tok2 n2 /\ join tok1 tok2 tok }} := TokenFactory.unmergeToken. Lemma factoryOverlap : forall f1 f2 n1 n2, isTokenFactory f1 n1 -> isTokenFactory f2 n2 -> joins f1 f2 -> False. Proof. intros. destruct H1. destruct H1. apply (TokenFactory.factoryOverlap f1 f2 n1 n2 H H0 H1). Qed. Definition fullFactory : forall x, isTokenFactory x 0 <-> x = top := TokenFactory.fullFactory. Lemma identityToken : forall x, isToken x 0 <-> identity x. Proof. intro x; destruct (TokenFactory.identityToken x); split; intros. hnf; intros. rewrite H in H2; auto. apply bot_identity; auto. apply H0. apply identity_share_bot; auto. Qed. Lemma nonidentityToken : forall x n, (n > 0)%nat -> isToken x n -> nonidentity x. Proof. intros. generalize (TokenFactory.nonidentityToken x n H H0). repeat intro. apply H1. apply identity_share_bot; auto. Qed. Lemma nonidentityFactory : forall x n, isTokenFactory x n -> nonidentity x. Proof. intros. generalize (TokenFactory.nonidentityFactory x n H); repeat intro. apply H0. apply identity_share_bot; auto. Qed. Definition split : t -> t * t := Splittable.split. Lemma split_join : forall x1 x2 x, split x = (x1,x2) -> join x1 x2 x. Proof. intros; split. apply Splittable.split_disjoint with x; auto. apply Splittable.split_together; auto. Qed. Lemma split_nontrivial : forall x1 x2 x, split x = (x1, x2) -> (identity x1 \/ identity x2) -> identity x. Proof. intros. rewrite (Splittable.split_nontrivial x1 x2 x H). apply bot_identity. destruct H0. left; apply identity_share_bot; auto. right; apply identity_share_bot; auto. Qed. Definition rel : t -> t -> t := Relativ.rel. Lemma rel_leq : forall a x, join_sub (rel a x) a. Proof. intros. rewrite <- leq_join_sub. intros. rewrite ord_spec1. pattern a at 3. replace a with (rel a top). rewrite <- Relativ.rel_preserves_glb. rewrite glb_top. auto. apply Relativ.rel_top1. Qed. Definition rel_inj_l : forall a x y, a <> bot -> rel a x = rel a y -> x = y := Relativ.rel_inj_l. Definition rel_inj_r : forall a b x, x <> bot -> rel a x = rel b x -> a = b := Relativ.rel_inj_r. Definition rel_assoc : forall x y z, rel x (rel y z) = rel (rel x y) z := Relativ.rel_assoc. Definition rel_bot1 : forall a, rel a bot = bot := Relativ.rel_bot1. Definition rel_bot2 : forall x, rel bot x = bot := Relativ.rel_bot2. Definition rel_top1 : forall a, rel a top = a := Relativ.rel_top1. Definition rel_top2 : forall x, rel top x = x := Relativ.rel_top2. Lemma rel_join : forall a x y z, join x y z -> join (rel a x) (rel a y) (rel a z). Proof. simpl; unfold ba_join; intuition. rewrite <- Relativ.rel_preserves_glb. replace BA.bot with (Relativ.rel a bot). replace (Relativ.BAF.BA.glb x y) with bot; auto. apply Relativ.rel_bot1. rewrite <- Relativ.rel_preserves_lub. replace (Relativ.BAF.BA.lub x y) with z; auto. Qed. Lemma rel_join2 : forall a x y s, nonidentity a -> join (rel a x) (rel a y) s -> exists z, s = rel a z /\ join x y z. Proof. simpl; intros. destruct H0. exists (lub x y). split. rewrite <- H1. symmetry. apply Relativ.rel_preserves_lub. split; auto. rewrite <- Relativ.rel_preserves_glb in H0. replace BA.bot with (Relativ.rel a bot) in H0. apply Relativ.rel_inj_l with a; auto. hnf; intros; apply H. subst a; apply bot_identity. apply Relativ.rel_bot1. Qed. Lemma rel_nontrivial : forall a x, identity (Share.rel a x) -> (identity a \/ identity x). Proof. intros a x H. destruct (eq_dec a bot); auto. subst a. left. apply bot_identity. right. assert (rel a x = bot). apply identity_share_bot; auto. assert (x = bot). replace bot with (rel a bot) in H0. apply rel_inj_l with a; auto. apply rel_bot1. subst x; apply bot_identity. Qed. Lemma cross_split : forall a b c d z, join a b z -> join c d z -> { x:(t*t*t*t) & match x with (ac,ad,bc,bd) => join ac ad a /\ join bc bd b /\ join ac bc c /\ join ad bd d end }. Proof. simpl; unfold ba_join; intuition. exists (glb a c, glb a d, glb b c, glb b d); intuition. rewrite (glb_commute a d). rewrite glb_assoc. rewrite <- (glb_assoc c d a). rewrite H. rewrite (glb_commute BA.bot a). rewrite glb_bot. rewrite glb_bot. auto. rewrite <- distrib1; rewrite H3; rewrite <- H2; auto with ba. rewrite (glb_commute b d). rewrite glb_assoc. rewrite <- (glb_assoc c d b). rewrite H. rewrite (glb_commute BA.bot b). rewrite glb_bot. rewrite glb_bot. auto. rewrite <- distrib1; rewrite H3; rewrite <- H2; auto with ba. rewrite (glb_commute a c). rewrite glb_assoc. rewrite <- (glb_assoc a b c). rewrite H1. rewrite (glb_commute BA.bot c). rewrite glb_bot. rewrite glb_bot. auto. rewrite (glb_commute a c). rewrite (glb_commute b c). rewrite <- distrib1; rewrite H2; rewrite <- H3; auto with ba. rewrite (glb_commute a d). rewrite glb_assoc. rewrite <- (glb_assoc a b d). rewrite H1. rewrite (glb_commute BA.bot d). rewrite glb_bot. rewrite glb_bot. auto. rewrite (glb_commute a d). rewrite (glb_commute b d). rewrite <- distrib1; rewrite H2; rewrite <- H3; auto with ba. Qed. End Share. Lemma bot_correct : forall x, join_sub Share.bot x. Proof. intros s. destruct (Share.top_correct s). exists s. destruct (Share.top_correct Share.bot). assert (x0 = Share.top). apply Share.bot_identity; auto. subst x0. apply join_com in H0. destruct (join_assoc _ _ _ _ _ H H0); intuition. apply join_com in H2. destruct (join_assoc _ _ _ _ _ H1 H2); intuition. assert (s = x1). apply Share.bot_identity; auto. subst x1; auto. Qed. Lemma identity_share_bot : forall s, identity s -> s = Share.bot. Proof. intros. apply identities_unique; auto. apply Share.bot_identity. exists s. apply join_com. destruct (bot_correct s). assert (x = s). apply Share.bot_identity; auto. subst x; auto. Qed. Lemma top_share_nonidentity : nonidentity Share.top. Proof. hnf; intros. assert (Share.top = Share.bot). apply identity_share_bot; auto. apply Share.shares_nontrivial; auto. Qed. Lemma bot_joins : forall x, joins Share.bot x. Proof. intro x; exists x. destruct (join_ex_identities x); intuition. destruct H0. generalize (H _ _ H0). intros; subst; auto. replace Share.bot with x0; auto. apply identity_share_bot; auto. Qed. (* A pshare is a "positive share", that is, a nonidentity share. *) Definition pshare := pjoinable Share.sa. Definition pshare_sh (psh: pshare) : Share.t := projT1 psh. Definition pshare_nonidentity (psh: pshare) : nonidentity (pshare_sh psh) := projT2 psh. Coercion pshare_sh : pshare >-> Share.t. Definition mk_pshare (sh: Share.t) (p: nonidentity sh) := existT nonidentity sh p. Definition pfullshare : pshare := mk_pshare Share.top top_share_nonidentity. Lemma pshare_eq_e: forall (sh sh' : pshare), pshare_sh sh = pshare_sh sh' -> sh=sh'. Proof. destruct sh; destruct sh'. simpl. intros; subst x0. rewrite (proof_irr n n0); auto. Qed. Implicit Arguments pshare_eq_e [sh sh']. Theorem pshare_leq_join : forall s1 s2:pshare, join_sub (projT1 s1) (projT1 s2) -> joins (projT1 s1) (projT1 s2) -> False. Proof. simpl; intros. generalize (join_sub_joins H H0); intros. destruct H1. assert (pshare_sh s1 = x). apply join_self; auto. subst x. contradiction (pshare_nonidentity s1). destruct s1. (* Compat change *) apply unit_identity with x; auto. Qed. Lemma pshare_join_full_false1 : forall (p:pshare), joins (projT1 pfullshare) (projT1 p) -> False. Proof. intros. contradiction (pshare_nonidentity p). rewrite joins_sym in H. generalize (join_sub_joins (Share.top_correct _) H); intros. destruct H0. assert (pshare_sh p = x). apply join_self; auto. subst x. destruct p. (* Compat change *) apply unit_identity with x; auto. Qed. Lemma pshare_join_full_false2 : forall (p:pshare), joins (projT1 p) (projT1 pfullshare) -> False. Proof. intros. destruct H. eapply pshare_join_full_false1. exists x. apply join_com; eauto. Qed. Lemma pshare_join_full_false3: forall (p1: pshare) sh3, join (projT1 p1) (projT1 pfullshare) sh3 -> False. Proof. intros. eapply pshare_join_full_false1. eexists; apply join_com; eauto. Qed. Lemma pshare_join_full_false4: forall (p1: pshare) sh3, join (projT1 pfullshare) (projT1 p1) sh3 -> False. Proof. intros. eapply pshare_join_full_false1. eexists; eauto. Qed. Ltac pfullshare_join := elimtype False; solve [ eapply pshare_join_full_false1; eauto | eapply pshare_join_full_false2; eauto | eapply pshare_join_full_false3; eauto | eapply pshare_join_full_false4; eauto ]. Lemma rel_congruence : forall a x1 x2, join_sub x1 x2 -> join_sub (Share.rel a x1) (Share.rel a x2). Proof. intros. destruct H. exists (Share.rel a x). apply Share.rel_join; auto. Qed. Definition prel (a x:pshare) : pshare. intros [a ?] [x ?]. refine (existT _ (Share.rel a x) _ : pshare). hnf; intros. destruct (Share.rel_nontrivial a x); auto. Defined. Lemma prel_pfullshare : forall (a x:pshare), pshare_sh x = Share.top -> prel a x = a. Proof. intros [a ?] [x ?] H. apply pshare_eq_e; simpl. injection H; intros; subst x. apply Share.rel_top1. Qed. Lemma join_sub_pfullshare: forall (p: pshare), join_sub (projT1 pfullshare) (projT1 p) -> p=pfullshare. Proof. intros. destruct H as [sh ?]. unfold pfullshare in *. simpl in H. destruct p; simpl in *. assert (x = Share.top). destruct (Share.top_correct x). destruct (join_assoc _ _ _ _ _ H H0) as [f [? ?]]. generalize (split_identity _ _ H1 (unit_identity _ _ (join_com _ _ _ H2))); intro. assert (joins sh Share.top) by (econstructor; apply join_com; eauto). generalize (identity_unit H3 H4); intro. unfold unit_for in H5. eapply join_eq. eauto. apply join_com; auto. subst. rewrite (proof_irr n top_share_nonidentity). auto. Qed.