Require Import VST.msl.msl_standard.
Require Import VST.msl.Coqlib2.

Set Implicit Arguments.

Lemma share_lemma87:
  forall a b, Share.glb a b = Share.bot -> Share.glb (Share.comp a) b = b.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t (Share.glb (Share.comp a) b) b *)
rewrite <- (Share.glb_top b) at 2.
(* Goal: @eq Share.t (Share.glb (Share.comp a) b) (Share.lub (Share.glb b a) (Share.glb b (Share.comp a))) *)
rewrite (Share.glb_commute b).
(* Goal: @eq Share.t (Share.glb (Share.comp a) b) (Share.glb Share.top b) *)
rewrite <- (Share.comp1 a).
(* Goal: @eq Share.t (Share.glb (Share.comp a) b) (Share.glb (Share.lub a (Share.comp a)) b) *)
rewrite (Share.glb_commute (Share.lub _ _)).
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.glb (Share.comp a) b) (Share.lub (Share.glb b a) (Share.glb b (Share.comp a))) *)
rewrite (Share.glb_commute b).
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb al bl) (Share.glb bl ar)) (Share.glb (Share.lub al ar) br)) Share.bot *)
rewrite H.
(* Goal: @eq Share.t (Share.lub (Share.lub Share.bot (Share.glb bl ar)) (Share.glb (Share.lub al ar) br)) Share.bot *)
rewrite (Share.lub_commute Share.bot), Share.lub_bot.
(* Goal: @eq Share.t (Share.glb (Share.comp a) b) (Share.glb b (Share.comp a)) *)
apply Share.glb_commute.
Qed.

Lemma join_top_comp:
  forall a b, join a b Share.top -> Share.comp a = b.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t sh Share.bot *)
destruct H.
(* Goal: @eq Share.t (Share.comp a) b *)
pose proof (share_lemma87 H).
(* Goal: @eq Share.t (Share.lub a b) (Share.lub (Share.glb L c) (Share.glb (Share.comp L) c)) *)
rewrite <- H1.
(* Goal: Share.Ord (Share.glb Share.Rsh sh) sh *)
rewrite Share.glb_commute.
(* Goal: @eq Share.t Share.Rsh (Share.comp Share.Lsh) *)
symmetry.
(* Goal: @eq Share.t (Share.glb b (Share.comp a)) (Share.comp a) *)
rewrite <- (Share.comp_inv b).
(* Goal: @eq Share.t (Share.glb (Share.comp (Share.comp b)) (Share.comp a)) (Share.comp a) *)
apply share_lemma87.
(* Goal: @eq Share.t (Share.lub sh (Share.glb (Share.comp sh) (Share.comp Share.Rsh))) Share.Lsh *)
rewrite <- Share.demorgan1.
(* Goal: @eq Share.t (Share.comp (Share.lub b a)) Share.bot *)
rewrite Share.lub_commute, H0.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.glb bl L) (Share.glb ar (Share.comp L))) (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L))) Share.bot *)
clear.
(* Goal: @eq Share.t (Share.comp Share.top) Share.bot *)
pose proof (Share.comp1 Share.bot).
(* Goal: @eq Share.t (Share.comp Share.top) Share.bot *)
rewrite Share.lub_commute, Share.lub_bot in H.
(* Goal: @eq Share.t Share.Rsh (Share.glb Share.Rsh (Share.glb Share.Rsh sh)) *)
rewrite <- H.
(* Goal: @eq Share.t (Share.comp (Share.comp (Share.glb (Share.comp sh) (Share.lub sh Share.Rsh)))) Share.Rsh *)
rewrite Share.comp_inv.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
Qed.

Lemma comp_bot: Share.comp Share.bot = Share.top.
Proof.
(* Goal: @eq Share.t (Share.comp Share.bot) Share.top *)
apply join_top_comp.
(* Goal: @join Share.t Share.Join_ba Share.bot Share.top Share.top *)
apply bot_join_eq.
Qed.

Lemma share_distrib1':
      forall w x y z : Share.t,
       Share.glb (Share.lub w x) (Share.lub y z) =
       Share.lub (Share.lub (Share.glb w y)  (Share.glb x y))
                     (Share.lub (Share.glb w z) (Share.glb x z)).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.lub w x) y) (Share.glb (Share.lub w x) z)) (Share.lub (Share.lub (Share.glb w y) (Share.glb x y)) (Share.lub (Share.glb w z) (Share.glb x z))) *)
rewrite <- (Share.glb_commute y), <- (Share.glb_commute z).
(* Goal: @eq Share.t (Share.glb (Share.glb a (Share.lub L (Share.comp L))) b) Share.bot *)
rewrite !Share.distrib1.
(* Goal: @eq Share.t (Share.glb (Share.comp a) b) (Share.glb b (Share.comp a)) *)
f_equal; f_equal; apply Share.glb_commute.
Qed.

Lemma share_distrib2':
   forall w x y z : Share.t,
       Share.lub (Share.glb w x) (Share.glb y z) =
       Share.glb (Share.glb (Share.lub w y) (Share.lub x y))
                      (Share.glb (Share.lub w z) (Share.lub x z)).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t (Share.lub Share.Rsh (Share.glb Share.Lsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
rewrite Share.distrib2.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb w x) y) (Share.lub (Share.glb w x) z)) (Share.glb (Share.glb (Share.lub w y) (Share.lub x y)) (Share.glb (Share.lub w z) (Share.lub x z))) *)
rewrite <- (Share.lub_commute y), <- (Share.lub_commute z).
(* Goal: @eq Share.t (Share.glb (Share.lub y (Share.glb w x)) (Share.lub z (Share.glb w x))) (Share.glb (Share.glb (Share.lub w y) (Share.lub x y)) (Share.glb (Share.lub w z) (Share.lub x z))) *)
rewrite !Share.distrib2.
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub y w) (Share.lub y x)) (Share.glb (Share.lub z w) (Share.lub z x))) (Share.glb (Share.glb (Share.lub w y) (Share.lub x y)) (Share.glb (Share.lub w z) (Share.lub x z))) *)
f_equal; f_equal; apply Share.lub_commute.
Qed.

Lemma lub_bot_e:
  forall x y, Share.lub x y = Share.bot -> x = Share.bot /\ y = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: and (@eq Share.t x Share.bot) (@eq Share.t y Share.bot) *)
pose proof (Share.lub_upper1 x y).
(* Goal: and (@eq Share.t x Share.bot) (@eq Share.t y Share.bot) *)
pose proof (Share.lub_upper2 x y).
(* Goal: and (@eq Share.t x Share.bot) (@eq Share.t y Share.bot) *)
rewrite H in H0,H1.
(* Goal: and (@eq Share.t x Share.bot) (@eq Share.t y Share.bot) *)
split; apply Share.ord_antisym; auto; apply Share.bot_correct.
Qed.

Lemma glb_less_both:
  forall a L b R,
   Share.Ord a L -> Share.Ord b R ->
   Share.Ord (Share.glb a b) (Share.glb L R).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 intros.
(* Goal: Share.Ord (Share.glb a b) (Share.glb L R) *)
 generalize (Share.glb_lower1 a b);intro.
(* Goal: Share.Ord (Share.glb a b) (Share.glb L R) *)
 generalize (Share.glb_lower2 a b);intro.
(* Goal: Share.Ord (Share.glb a b) (Share.glb L R) *)
 generalize (Share.ord_trans _ _ _ H1 H);intro.
(* Goal: Share.Ord (Share.glb a b) (Share.glb L R) *)
 generalize (Share.ord_trans _ _ _ H2 H0);intro.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 eapply Share.glb_greatest;auto.
Qed.

Lemma comp_Lsh_Rsh:
  Share.comp Share.Lsh = Share.Rsh.
Proof.
(* Goal: @eq Share.t (Share.glb Share.Lsh Share.Rsh) Share.bot *)
 unfold Share.Lsh, Share.Rsh.
(* Goal: @eq Share.t (Share.comp (@fst Share.t Share.t (Share.split Share.top))) (@snd Share.t Share.t (Share.split Share.top)) *)
 destruct (Share.split Share.top) eqn:?H; simpl.
(* Goal: @eq Share.t (Share.glb t t0) Share.bot *)
 apply split_join in H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 apply join_top_comp; auto.
Qed.

Lemma share_lemma88:
   forall sh, Share.glb sh Share.Rsh = Share.bot ->
                 join_sub sh Share.Lsh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 intros.
(* Goal: @join_sub Share.t Share.Join_ba sh Share.Lsh *)
 exists (Share.glb (Share.comp sh) Share.Lsh).
(* Goal: @join Share.t Share.Join_ba sh (Share.glb (Share.comp sh) Share.Lsh) Share.Lsh *)
 rewrite <- (Share.comp_inv Share.Lsh) at 1.
(* Goal: @eq Share.t (Share.comp (Share.lub sh (Share.comp (Share.lub sh Share.Rsh)))) (Share.comp Share.Lsh) *)
 rewrite comp_Lsh_Rsh.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 split.
*
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
 rewrite <- Share.glb_assoc.
(* Goal: Share.Ord (Share.glb Share.Rsh sh) sh *)
 rewrite Share.comp2. rewrite Share.glb_commute. apply Share.glb_bot.
*
(* Goal: @eq Share.t (Share.lub sh (Share.glb (Share.comp sh) (Share.comp Share.Rsh))) Share.Lsh *)
 rewrite <- Share.demorgan1.
(* Goal: @eq Share.t Share.Rsh (Share.comp Share.Lsh) *)
 rewrite <- Share.comp_inv; symmetry; rewrite <- Share.comp_inv; symmetry.
(* Goal: @eq Share.t (Share.lub a b) (Share.lub (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) *)
 f_equal.
(* Goal: @eq Share.t (Share.comp (Share.lub sh (Share.comp (Share.lub sh Share.Rsh)))) (Share.comp Share.Lsh) *)
 rewrite comp_Lsh_Rsh.
(* Goal: @eq Share.t (Share.comp (Share.lub sh (Share.comp (Share.lub sh Share.Rsh)))) Share.Rsh *)
 rewrite <- (Share.comp_inv sh) at 1.
(* Goal: @eq Share.t (Share.comp (Share.lub (Share.comp (Share.comp sh)) (Share.comp (Share.lub sh Share.Rsh)))) Share.Rsh *)
 rewrite <- Share.demorgan2.
(* Goal: @eq Share.t (Share.comp (Share.comp (Share.glb (Share.comp sh) (Share.lub sh Share.Rsh)))) Share.Rsh *)
 rewrite Share.comp_inv.
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
 rewrite Share.distrib1.
(* Goal: Share.Ord (Share.glb Share.Rsh sh) sh *)
 rewrite Share.glb_commute.
(* Goal: @eq Share.t (Share.glb (Share.glb L (Share.comp L)) sh1) Share.bot *)
 rewrite Share.comp2.
 rewrite Share.lub_commute,  Share.lub_bot.
(* Goal: @eq Share.t (Share.glb (Share.comp sh) Share.Rsh) Share.Rsh *)
 forget Share.Rsh as b.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 apply share_lemma87; auto.
Qed.

Definition Tsh : share := Share.top.

Definition nonempty_share (sh: share) :=
       sepalg.nonidentity sh.
Definition readable_share (sh: share) :=
       nonempty_share (Share.glb Share.Rsh sh).
Definition writable_share (sh: share) :=
    nonempty_share (Share.glb Share.Lsh sh) /\ join_sub Share.Rsh sh.


Lemma lub_Lsh_Rsh:
 Share.lub Share.Lsh Share.Rsh = Share.top.
Proof.
(* Goal: @eq Share.t (Share.glb Share.Lsh Share.Rsh) Share.bot *)
unfold Share.Lsh, Share.Rsh.
(* Goal: @eq Share.t (Share.glb (@fst Share.t Share.t (Share.split Share.top)) (@snd Share.t Share.t (Share.split Share.top))) Share.bot *)
destruct (Share.split Share.top) eqn:H; simpl.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply Share.split_together; auto.
Qed.

Lemma glb_Lsh_Rsh:
 Share.glb Share.Lsh Share.Rsh = Share.bot.
Proof.
(* Goal: @eq Share.t (Share.glb Share.Lsh Share.Rsh) Share.bot *)
unfold Share.Lsh, Share.Rsh.
(* Goal: @eq Share.t (Share.glb (@fst Share.t Share.t (Share.split Share.top)) (@snd Share.t Share.t (Share.split Share.top))) Share.bot *)
destruct (Share.split Share.top) eqn:H; simpl.
(* Goal: @eq Share.t (Share.glb t t0) Share.bot *)
apply (Share.split_disjoint _ _ _ H).
Qed.

Lemma readable_share_dec:
  forall sh, {readable_share sh}+{~ readable_share sh}.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: sumbool (readable_share sh) (not (readable_share sh)) *)
unfold readable_share, nonempty_share.
(* Goal: sumbool (@nonidentity share Share.Join_ba pa_share (Share.glb Share.Rsh sh)) (not (@nonidentity share Share.Join_ba pa_share (Share.glb Share.Rsh sh))) *)
unfold nonidentity.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
destruct (dec_share_identity (Share.glb Share.Rsh sh)); [ right | left]; auto.
Defined.

Lemma writable_share_dec: forall sh, {writable_share sh} + {~ writable_share sh}.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
  unfold writable_share. intros.
(* Goal: sumbool (and (nonempty_share (Share.glb Share.Lsh sh)) (@join_sub Share.t Share.Join_ba Share.Rsh sh)) (not (and (nonempty_share (Share.glb Share.Lsh sh)) (@join_sub Share.t Share.Join_ba Share.Rsh sh))) *)
  destruct (Share.EqDec_share (Share.glb Share.Rsh sh) Share.Rsh); [|right].
*
(* Goal: sumbool (and (nonempty_share (Share.glb Share.Lsh sh)) (@join_sub Share.t Share.Join_ba Share.Rsh sh)) (not (and (nonempty_share (Share.glb Share.Lsh sh)) (@join_sub Share.t Share.Join_ba Share.Rsh sh))) *)
  destruct (Share.EqDec_share (Share.glb Share.Lsh sh) Share.bot); [right|left].
 + intros [? ?]. rewrite e0 in H. apply H. apply bot_identity.
 +
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
  split. unfold nonempty_share, nonidentity. contradict n.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  apply identity_share_bot; auto.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
  clear n.  
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
  exists (Share.glb Share.Lsh sh).
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
  split.
  -
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
  rewrite <- Share.glb_assoc.
(* Goal: @eq Share.t (Share.glb (Share.glb Share.Rsh Share.Lsh) sh) Share.bot *)
  rewrite (Share.glb_commute Share.Rsh).
(* Goal: @eq Share.t (Share.glb (Share.glb Share.Lsh Share.Rsh) sh) Share.bot *)
  unfold Share.Rsh, Share.Lsh.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  destruct (Share.split Share.top) eqn:?. simpl.
(* Goal: @eq Share.t (Share.glb (Share.glb t t0) sh) Share.bot *)
  apply Share.split_disjoint in Heqp. rewrite Heqp.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_commute, Share.glb_bot. auto.
  -
(* Goal: @eq Share.t (Share.lub Share.Rsh (Share.glb Share.Lsh sh)) sh *)
  apply Share.distrib_spec with Share.Rsh.
  rewrite <- Share.lub_assoc. rewrite Share.lub_idem.
(* Goal: @eq Share.t (Share.lub Share.Rsh (Share.glb Share.Lsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  rewrite Share.distrib2.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Rsh Share.Lsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  rewrite Share.lub_commute.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  destruct (Share.split Share.top) eqn:?.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  unfold Share.Lsh, Share.Rsh at 1.
(* Goal: @eq Share.t (Share.glb (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t t t0)) (@snd Share.t Share.t (@pair Share.t Share.t t t0))) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  rewrite Heqp. simpl.
(* Goal: @eq Share.t (Share.glb (Share.lub t t0) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  rewrite (Share.split_together _ _ _ Heqp).
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_commute, Share.glb_top. auto.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_absorb. rewrite e. auto.
*
(* Goal: not (@join_sub Share.t Share.Join_ba Share.Rsh sh) *)
  contradict n.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.Rsh *)
  destruct n as [_ [a [? ?]]].
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.Rsh *)
  subst sh.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_absorb. auto.
Qed.

Lemma writable_readable:
 forall sh, writable_share sh -> readable_share sh.
Proof.
(* Goal: forall (sh : share) (_ : writable0_share sh), readable_share sh *)
unfold writable_share, readable_share.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros. destruct H as [_ H].
(* Goal: not (readable_share Share.bot) *)
intro.
(* Goal: False *)
destruct H as [a ?].
(* Goal: @eq Share.t sh Share.bot *)
destruct H.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.Rsh *)
subst sh.
(* Goal: False *)
rewrite Share.glb_absorb in H0.
clear - H0. unfold Share.Rsh in H0.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
destruct (Share.split Share.top) eqn:?. simpl in H0.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply split_nontrivial' in Heqp; auto.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply top_share_nonidentity in Heqp. auto.
Qed.

Lemma readable_share_top:
  readable_share Share.top.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
hnf. intros.
(* Goal: @eq Share.t sh Share.bot *)
rewrite Share.glb_top in H.
(* Goal: False *)
unfold Share.Rsh in H.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
destruct (Share.split Share.top) eqn:?.
(* Goal: False *)
apply split_nontrivial' in Heqp.
(* Goal: False *)
(* Goal: or (@identity Share.t Share.Join_ba t) (@identity Share.t Share.Join_ba t0) *)
apply identity_share_bot in Heqp.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply Share.nontrivial; auto.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
simpl in H; auto.
Qed.
Hint Resolve writable_readable.

Lemma top_pfullshare: forall psh, pshare_sh psh = Share.top -> psh = pfullshare.
Proof.
(* Goal: forall (psh : pshare) (_ : @eq share (pshare_sh psh) Share.top), @eq pshare psh pfullshare *)
intros psh H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply lifted_eq; auto.
Qed.

Lemma fst_split_fullshare_not_bot: fst (Share.split fullshare) <> Share.bot.
Proof.
(* Goal: not (readable_share Share.bot) *)
intro.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
case_eq (Share.split fullshare); intros.
(* Goal: False *)
rewrite H0 in H. simpl in H. subst.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply Share.split_nontrivial in H0; auto.
(* Goal: False *)
apply Share.nontrivial in H0. contradiction.
Qed.

Lemma fst_split_fullshare_not_top: fst (Share.split fullshare) <> Share.top.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
case_eq (Share.split fullshare); intros.
(* Goal: not (readable_share Share.bot) *)
simpl; intro. subst.
(* Goal: False *)
apply nonemp_split_neq1 in H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply H; auto.
(* Goal: @nonidentity Share.t Share.Join_ba pa_share fullshare *)
apply top_share_nonidentity.
Qed.

Lemma glb_Rsh_not_top:
   forall sh, Share.glb Share.Rsh sh <> Share.top.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 intros.
(* Goal: not (readable_share Share.bot) *)
 intro.
(* Goal: False *)
 unfold Share.Rsh in H.
(* Goal: False *)
 destruct (Share.split Share.top) eqn:?H.
(* Goal: False *)
  pose proof (Share.split_disjoint _ _ _ H0).
(* Goal: False *)
 simpl in H.
(* Goal: False *)
  pose proof (Share.glb_lower1 t0 sh).
(* Goal: False *)
  rewrite H in H2.
(* Goal: False *)
  apply leq_join_sub in H2.
(* Goal: False *)
  destruct H2. destruct H2.
(* Goal: False *)
  rewrite Share.lub_commute, Share.lub_top in H3.
(* Goal: @join Share.t Share.Join_ba (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh sh2) (Share.glb Share.Rsh sh3) *)
  subst.
  clear - H0.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  apply nonemp_split_neq2 in H0; auto.
(* Goal: not (readable_share Share.bot) *)
  intro. apply identity_share_bot in H.
(* Goal: False *)
  contradiction Share.nontrivial.
Qed.
Arguments glb_Rsh_not_top sh _ : clear implicits.

Lemma writable_share_top: writable_share Tsh.
Proof.
(* Goal: Join_rshare (@readable_part sh1 rsh1) (@readable_part sh2 rsh2) (@readable_part sh3 rsh3) *)
red.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
split.
*
(* Goal: @eq Share.t b (Share.glb b Share.top) *)
rewrite Share.glb_top. 
(* Goal: nonempty_share Share.Lsh *)
unfold Share.Lsh.
(* Goal: not (readable_share Share.bot) *)
intro.
(* Goal: False *)
destruct (Share.split Share.top) eqn:?H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply split_nontrivial' in H0; auto.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
apply identity_share_bot in H0.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply Share.nontrivial; auto.
*
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh Tsh *)
exists Share.Lsh.
(* Goal: @join Share.t Share.Join_ba Share.Rsh Share.Lsh Tsh *)
apply join_comm.
(* Goal: @join Share.t Share.Join_ba Share.Lsh Share.Rsh Tsh *)
unfold Share.Lsh, Share.Rsh, Tsh.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
destruct (Share.split Share.top) eqn:?. simpl.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply split_join; auto.
Qed.
Hint Resolve writable_share_top.

Lemma writable_readable_share:
 forall sh, writable_share sh -> readable_share sh.
Proof.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply writable_readable; auto.
Qed.
Hint Resolve writable_readable_share.

Definition extern_retainer := fst (Share.split Share.Lsh).

Definition Ews (* extern_write_share *) := 
  Share.lub extern_retainer Share.Rsh.

Lemma writable_Ews: writable_share Ews.
Proof.
(* Goal: writable_share Ews *)
split; unfold Ews.
*
(* Goal: not (@identity Share.t Share.Join_ba extern_retainer) *)
unfold extern_retainer.
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
rewrite Share.distrib1.
(* Goal: nonempty_share (Share.lub (Share.glb Share.Lsh (@fst Share.t Share.t (Share.split Share.Lsh))) (Share.glb Share.Lsh Share.Rsh)) *)
rewrite glb_Lsh_Rsh, Share.lub_bot.
(* Goal: False *)
destruct (Share.split Share.Lsh) eqn:?H.
(* Goal: nonempty_share (Share.glb Share.Lsh (@fst Share.t Share.t (@pair Share.t Share.t t t0))) *)
assert (H1: nonempty_share t). {
(* Goal: not (readable_share Share.bot) *)
 intro. apply identity_share_bot in H0. subst.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 apply Share.split_nontrivial in H; auto.
(* Goal: False *)
 unfold Share.Lsh in H.
(* Goal: False *)
 destruct (Share.split Share.top) eqn:?H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 apply Share.split_nontrivial in H0; auto.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 apply Share.nontrivial; auto.
}
(* Goal: @eq Share.t (Share.glb t t0) Share.bot *)
apply split_join in H.
(* Goal: @eq Share.t (Share.glb (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t t t0)) (@snd Share.t Share.t (@pair Share.t Share.t t t0))) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
simpl.
(* Goal: @eq Share.t sh Share.bot *)
destruct H.
rewrite <- H0.
(* Goal: @eq Share.t (Share.glb (Share.lub t t0) t) t *)
rewrite Share.glb_commute, Share.distrib1.
(* Goal: nonempty_share (Share.lub (Share.glb t t) (Share.glb t t0)) *)
rewrite H, Share.lub_bot.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
rewrite Share.glb_idem; auto.
*
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
apply leq_join_sub.
(* Goal: Share.Ord Share.Rsh (Share.lub extern_retainer Share.Rsh) *)
apply Share.lub_upper2.
Qed.

Lemma writable_Rsh: writable_share Share.Rsh.
Proof.
(* Goal: writable0_share Share.Rsh *)
  unfold writable_share.
Abort.  (* Not true any more *)

Hint Resolve writable_Ews.

Definition Ers (* Extern read share *) := 
  Share.lub extern_retainer (fst (Share.split Share.Rsh)).

Lemma readable_nonidentity: forall sh, readable_share sh -> sepalg.nonidentity sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @nonidentity share Share.Join_ba pa_share sh *)
do 2 red in H.
red in H|-*. contradict H.
(* Goal: @join Share.t Share.Join_ba (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh sh2) (Share.glb Share.Rsh sh3) *)
apply identity_share_bot in H. subst.
(* Goal: @eq Share.t (Share.glb br (Share.glb al Share.bot)) Share.bot *)
rewrite Share.glb_bot.
(* Goal: @identity share Share.Join_ba Share.bot *)
apply bot_identity.
Qed.

Hint Resolve readable_nonidentity.

Lemma sub_glb_bot:
  forall r a c : share,
   sepalg.join_sub a c ->
   Share.glb r c = Share.bot ->
   Share.glb r a = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
apply leq_join_sub in H.
(* Goal: @eq Share.t Share.Rsh (Share.glb Share.Rsh (Share.glb Share.Rsh sh)) *)
apply Share.ord_spec1 in H.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb al bl) (Share.glb bl ar)) (Share.glb (Share.lub al ar) br)) Share.bot *)
rewrite H. rewrite <- Share.glb_assoc.
(* Goal: @eq Share.t (Share.glb (Share.glb r a) c) Share.bot *)
rewrite (Share.glb_commute r).
(* Goal: @eq Share.t (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot *)
rewrite Share.glb_assoc. rewrite H0.
(* Goal: @eq Share.t (Share.glb br Share.bot) Share.bot *)
apply Share.glb_bot.
Qed.

Lemma glb_split: forall sh,
 Share.glb (fst (Share.split sh)) (snd (Share.split sh)) = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t (Share.glb (@fst Share.t Share.t (Share.split sh)) (@snd Share.t Share.t (Share.split sh))) Share.bot *)
destruct (Share.split sh) eqn:?H.
(* Goal: @eq Share.t (Share.glb (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t t t0)) (@snd Share.t Share.t (@pair Share.t Share.t t t0))) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
simpl.
(* Goal: @eq Share.t (Share.glb t t0) Share.bot *)
apply split_join in H.
(* Goal: @eq Share.t sh Share.bot *)
destruct H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
Qed.

Lemma Lsh_nonidentity:   sepalg.nonidentity Share.Lsh.
Proof.
(* Goal: nonempty_share Share.Lsh *)
unfold Share.Lsh.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
destruct (Share.split Share.top) eqn:?. simpl; intro.
(* Goal: @join Share.t Share.Join_ba (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh sh2) (Share.glb Share.Rsh sh3) *)
apply identity_share_bot in H. subst.
(* Goal: False *)
pose proof (Share.split_nontrivial _ _ _ Heqp).
(* Goal: False *)
spec H;[auto | ].
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply Share.nontrivial in H. auto.
Qed.


Lemma Rsh_nonidentity:   sepalg.nonidentity Share.Rsh.
Proof.
(* Goal: @nonidentity Share.t Share.Join_ba pa_share Share.Rsh *)
unfold Share.Rsh.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
destruct (Share.split Share.top) eqn:?. simpl; intro.
(* Goal: @join Share.t Share.Join_ba (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh sh2) (Share.glb Share.Rsh sh3) *)
apply identity_share_bot in H. subst.
(* Goal: False *)
pose proof (Share.split_nontrivial _ _ _ Heqp).
(* Goal: False *)
spec H;[auto | ].
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply Share.nontrivial in H. auto.
Qed.

Lemma nonidentity_extern_retainer: ~identity extern_retainer.
Proof.
(* Goal: not (@identity Share.t Share.Join_ba extern_retainer) *)
unfold extern_retainer.
(* Goal: not (readable_share Share.bot) *)
intro.
(* Goal: False *)
destruct (Share.split Share.Lsh) eqn:?H.
(* Goal: False *)
simpl in H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply split_nontrivial' in H0; auto.
(* Goal: False *)
apply Lsh_nonidentity.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
Qed.

Lemma glb_split_x:
  forall a, Share.glb a (fst (Share.split a)) = fst (Share.split a).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
destruct (Share.split a) eqn:H; simpl in *.
(* Goal: @eq Share.t (Share.glb a t) t *)
destruct (split_join _ _ _ H).
(* Goal: @eq Share.t (Share.glb a t) t *)
subst a.
(* Goal: @eq Share.t (Share.glb (Share.lub t t0) t) t *)
rewrite Share.glb_commute, Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.lub (Share.glb br al) (Share.glb ar br))) Share.bot *)
rewrite H0.
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.glb Share.Lsh Share.Lsh) sh2) sh1) Share.bot *)
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Lsh sh1) (Share.glb Share.Lsh sh2)) (Share.glb Share.Lsh (Share.lub sh1 sh2)) *)
rewrite Share.glb_idem.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot) Share.bot *)
rewrite Share.lub_bot.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
Qed.

Lemma readable_Ers: readable_share Ers.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
hnf; intros.
(* Goal: False *)
unfold Ers in H.
(* Goal: False *)
unfold extern_retainer in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
rewrite Share.distrib1 in H.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.bot *)
apply identity_share_bot in H.
(* Goal: False *)
match type of H with Share.lub ?A _ = _ => forget A as a end.
(* Goal: False *)
rewrite glb_split_x in H.
(* Goal: False *)
pose proof (Share.lub_upper2 a (fst (Share.split Share.Rsh))).
(* Goal: False *)
rewrite H in H0.
(* Goal: False *)
apply leq_join_sub in H0.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
destruct H0.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply split_identity in H0; auto.
clear - H0.
destruct (Share.split Share.Rsh) eqn:?. simpl in *.
(* Goal: @join Share.t Share.Join_ba (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh sh2) (Share.glb Share.Rsh sh3) *)
apply identity_share_bot in H0. subst.
(* Goal: False *)
pose proof (Share.split_nontrivial _ _ _ Heqp).
(* Goal: False *)
spec H;[auto | ].
(* Goal: False *)
assert (identity Share.Rsh) by (rewrite H; auto).
(* Goal: False *)
contradiction Rsh_nonidentity.
Qed.

Lemma join_sub_readable:
  forall sh sh', sepalg.join_sub sh sh' -> readable_share sh -> readable_share sh'.
Proof.
unfold readable_share;
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
hnf in H0|-*.
(* Goal: not (writable0_share sh3) *)
contradict H0.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
apply identity_share_bot in H0.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
eapply sub_glb_bot in H0; eauto.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.lub (Share.glb br al) (Share.glb ar br))) Share.bot *)
rewrite H0.
(* Goal: @identity share Share.Join_ba Share.bot *)
apply bot_identity.
Qed.

Lemma join_unreadable_shares:
 forall sh1 sh2 sh,
  sepalg.join sh1 sh2 sh ->
  ~ readable_share sh1 ->
  ~ readable_share sh2 ->
 ~ readable_share sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
unfold readable_share; intros.
unfold nonempty_share in *.
unfold sepalg.nonidentity in *.
(* Goal: not (writable0_share sh3) *)
contradict H0. contradict H1. contradict H0.
(* Goal: @eq Share.t sh Share.bot *)
destruct H.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.Rsh *)
subst sh.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub sh1 sh2)) *)
apply identity_share_bot in H1.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
apply identity_share_bot in H0.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub sh1 sh2)) *)
rewrite Share.distrib1, H0,H1.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot) Share.bot *)
rewrite Share.lub_bot.
(* Goal: @identity share Share.Join_ba Share.bot *)
apply bot_identity.
Qed.

Lemma readable_share_join_left:
  forall sh1 sh2 sh,
    sepalg.join sh1 sh2 sh ->
    readable_share sh1 -> readable_share sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
unfold readable_share, nonempty_share, nonidentity in *.
(* Goal: not (writable0_share sh3) *)
contradict H0.
(* Goal: @eq Share.t sh Share.bot *)
destruct H.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.Rsh *)
subst sh.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
rewrite Share.distrib1 in H0.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
pose proof (Share.lub_upper1 (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh sh2)).
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
apply identity_share_bot in H0. rewrite H0 in H1.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
pose proof Share.bot_correct (Share.glb Share.Rsh sh1).
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
pose proof (Share.ord_antisym _ _ H1 H2).
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh1) *)
rewrite H3.
(* Goal: @identity share Share.Join_ba Share.bot *)
apply bot_identity.
Qed.

Lemma readable_share_join:
  forall sh1 sh2 sh,
    sepalg.join sh1 sh2 sh ->
    readable_share sh1 \/ readable_share sh2 -> readable_share sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
  intros.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
  destruct H0.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  + eapply readable_share_join_left; eauto.
  + apply join_comm in H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
    eapply readable_share_join_left; eauto.
Qed.

Lemma Lsh_bot_neq: Share.Lsh <> Share.bot.
Proof.
(* Goal: not (@eq Share.t Share.Lsh Share.bot) *)
  pose proof Lsh_nonidentity.
(* Goal: not (@eq Share.t Share.Lsh Share.bot) *)
  pose proof bot_identity.
(* Goal: not (readable_share Share.bot) *)
  intro.
  rewrite <- H1 in H0.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  apply H; auto.
Qed.

Lemma not_nonunit_bot: forall sh, ~ nonunit sh <-> sh = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
  intros; split; intros.
  + destruct (dec_share_identity sh).
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
    - apply identity_share_bot; auto.
(* Goal: False *)
    - exfalso; apply H.
(* Goal: @nonunit Share.t Share.Join_ba sh *)
      apply nonidentity_nonunit.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
      auto.
  + subst.
(* Goal: not (readable_share Share.bot) *)
    intro.
(* Goal: False *)
    apply nonunit_nonidentity in H.
(* Goal: False *)
    apply H.
(* Goal: @identity share Share.Join_ba Share.bot *)
    apply bot_identity.
Qed.


Lemma join_readable1:
  forall sh1 sh2 sh3,
    join sh1 sh2 sh3 ->
    readable_share sh1 -> readable_share sh3.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
eapply readable_share_join; eauto.
Qed.

Lemma join_readable2:
  forall sh1 sh2 sh3,
    join sh1 sh2 sh3 ->
    readable_share sh2 -> readable_share sh3.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
eapply readable_share_join; eauto.
Qed.

Lemma bot_unreadable: ~readable_share Share.bot.
Proof.
(* Goal: not (readable_share Share.bot) *)
intro.
(* Goal: False *)
unfold readable_share, nonempty_share, nonidentity in H.
(* Goal: False *)
apply H; clear H.
(* Goal: @identity share Share.Join_ba Share.bot *)
rewrite Share.glb_bot. apply bot_identity.
Qed.

Definition pure_readable_share (sh: Share.t) :=
  Share.glb Share.Lsh sh = Share.bot /\ readable_share sh.

Definition rshare := sig pure_readable_share.

Definition readable_part: forall (sh: Share.t) (rsh: readable_share sh), rshare.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: rshare *)
exists (Share.glb Share.Rsh sh).
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
split.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
rewrite <- Share.glb_assoc. rewrite glb_Lsh_Rsh.
(* Goal: Share.Ord (Share.glb Share.Rsh sh) sh *)
rewrite Share.glb_commute. apply Share.glb_bot.
(* Goal: readable_share (Share.glb Share.Rsh sh) *)
unfold readable_share.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
rewrite <- Share.glb_assoc.
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.glb Share.Lsh Share.Lsh) sh2) sh1) Share.bot *)
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Lsh sh1) (Share.glb Share.Lsh sh2)) (Share.glb Share.Lsh (Share.lub sh1 sh2)) *)
rewrite Share.glb_idem.
(* Goal: nonempty_share (Share.glb Share.Rsh sh) *)
apply rsh.
Defined.

Lemma readable_not_identity: forall sh P,
  readable_share sh -> identity sh -> P.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 intros.
(* Goal: P *)
 unfold readable_share in H.
(* Goal: P *)
 unfold nonempty_share, nonidentity in H. contradiction H.
(* Goal: @join Share.t Share.Join_ba (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh sh2) (Share.glb Share.Rsh sh3) *)
 apply identity_share_bot in H0; subst.
(* Goal: @identity share Share.Join_ba Share.bot *)
 rewrite Share.glb_bot. apply bot_identity.
Qed.
Arguments readable_not_identity sh P _ _ : clear implicits.

Lemma comp_parts:  
  forall L R : Share.t,
  Share.comp L = R ->
  forall sh: Share.t, sh = Share.lub (Share.glb L sh) (Share.glb R sh).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @join Share.t Share.Join_ba a b c *)
subst R.
rewrite <- !(Share.glb_commute sh).
rewrite <- Share.distrib1.
(* Goal: @eq Share.t sh (Share.glb sh (Share.lub L (Share.comp L))) *)
rewrite Share.comp1.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
rewrite Share.glb_top. auto.
Qed.

Lemma join_comp_parts:  
  forall L R : Share.t,
  Share.comp L = R ->
  forall a b c : Share.t,
  join a b c ->
  (join (Share.glb L a) (Share.glb L b) (Share.glb L c) /\
   join (Share.glb R a) (Share.glb R b) (Share.glb R c)).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
split; split.
*
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
rewrite (comp_parts H a) in H0.
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
rewrite (comp_parts H b) in H0.
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
rewrite (comp_parts H c) in H0.
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
destruct H0 as [H0 _].
pose proof (@glb_less_both
             (Share.glb L a) (Share.lub (Share.glb L a) (Share.glb R a))
             (Share.glb L b) (Share.lub (Share.glb L b) (Share.glb R b))).
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
apply Share.ord_antisym; [ | apply Share.bot_correct].
(* Goal: Share.Ord (Share.glb (Share.glb L a) (Share.glb L b)) Share.bot *)
eapply Share.ord_trans; try apply H1; try apply Share.lub_upper1.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.lub (Share.glb br al) (Share.glb ar br))) Share.bot *)
rewrite H0. apply Share.ord_refl.
*
(* Goal: @eq Share.t (Share.lub (Share.glb R a) (Share.glb R b)) (Share.glb R c) *)
destruct H0 as [_ H0].
(* Goal: @eq Share.t (Share.lub (Share.glb R a) (Share.glb R b)) (Share.glb R c) *)
subst c.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
rewrite <- Share.distrib1. auto.
*
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
rewrite (comp_parts H a) in H0.
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
rewrite (comp_parts H b) in H0.
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
rewrite (comp_parts H c) in H0.
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
destruct H0 as [H0 _].
pose proof (@glb_less_both
             (Share.glb R a) (Share.lub (Share.glb L a) (Share.glb R a))
             (Share.glb R b) (Share.lub (Share.glb L b) (Share.glb R b))).
(* Goal: @eq Share.t (Share.glb (Share.glb R a) (Share.glb R b)) Share.bot *)
apply Share.ord_antisym; [ | apply Share.bot_correct].
(* Goal: Share.Ord Share.Rsh (Share.lub extern_retainer Share.Rsh) *)
eapply Share.ord_trans; try apply H1; try apply Share.lub_upper2.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.lub (Share.glb br al) (Share.glb ar br))) Share.bot *)
rewrite H0. apply Share.ord_refl.
*
(* Goal: @eq Share.t (Share.lub (Share.glb R a) (Share.glb R b)) (Share.glb R c) *)
destruct H0 as [_ H0].
(* Goal: @eq Share.t (Share.lub (Share.glb R a) (Share.glb R b)) (Share.glb R c) *)
subst c.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
rewrite <- Share.distrib1. auto.
Qed.

Lemma join_pure_readable:
  forall sh1 sh2 sh3,
    join sh1 sh2 sh3 ->
    pure_readable_share sh1 -> 
    pure_readable_share sh2 -> 
    pure_readable_share sh3.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: pure_readable_share sh3 *)
destruct H0,H1.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
split.
(* Goal: @eq Share.t (Share.glb Share.Lsh sh3) Share.bot *)
(* Goal: readable_share sh3 *)
destruct (join_comp_parts comp_Lsh_Rsh H).
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
rewrite H0,H1 in *. apply join_unit1_e in H4; auto.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
eapply readable_share_join; eauto.
Qed.


Instance Join_rshare: Join rshare :=
  fun a b c => join (proj1_sig a) (proj1_sig b) (proj1_sig c).

Instance Perm_rshare: Perm_alg rshare. (* move me! *)
Proof.
(* Goal: @Perm_alg rshare Join_rshare *)
  unfold rshare.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
  constructor; intros.
*
(* Goal: @eq (@sig Share.t pure_readable_share) z z' *)
  destruct z, z'. apply exist_ext.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  do 2 red in H, H0. simpl in *. eapply join_eq; eauto.
* 
  destruct a,b,c,d,e; do 2 red in H,H0. simpl in *.
(* Goal: @sigT (@sig Share.t pure_readable_share) (fun f : @sig Share.t pure_readable_share => and (@join (@sig Share.t pure_readable_share) Join_rshare (@exist Share.t pure_readable_share x0 p0) (@exist Share.t pure_readable_share x1 p1) f) (@join (@sig Share.t pure_readable_share) Join_rshare (@exist Share.t pure_readable_share x p) f (@exist Share.t pure_readable_share x3 p3))) *)
  destruct (join_assoc H H0) as [a [? ?]].
(* Goal: @sigT (@sig Share.t pure_readable_share) (fun f : @sig Share.t pure_readable_share => and (@join (@sig Share.t pure_readable_share) Join_rshare (@exist Share.t pure_readable_share x0 p0) (@exist Share.t pure_readable_share x1 p1) f) (@join (@sig Share.t pure_readable_share) Join_rshare (@exist Share.t pure_readable_share x p) f (@exist Share.t pure_readable_share x3 p3))) *)
  assert (pure_readable_share a).
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  eapply join_pure_readable; eauto.
(* Goal: @sigT (@sig Share.t pure_readable_share) (fun f : @sig Share.t pure_readable_share => and (@join (@sig Share.t pure_readable_share) Join_rshare (@exist Share.t pure_readable_share x0 p0) (@exist Share.t pure_readable_share x1 p1) f) (@join (@sig Share.t pure_readable_share) Join_rshare (@exist Share.t pure_readable_share x p) f (@exist Share.t pure_readable_share x3 p3))) *)
  exists (exist pure_readable_share _ H3).
(* Goal: and (@join (@sig Share.t pure_readable_share) Join_rshare (@exist Share.t pure_readable_share x0 p0) (@exist Share.t pure_readable_share x1 p1) (@exist Share.t pure_readable_share a H3)) (@join (@sig Share.t pure_readable_share) Join_rshare (@exist Share.t pure_readable_share x p) (@exist Share.t pure_readable_share a H3) (@exist Share.t pure_readable_share x3 p3)) *)
  split; eassumption.
*
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  destruct a,b,c; do 2 red in H|-*; simpl in *. apply join_comm; auto.
*
  destruct a,a',b,b'; do 2 red in H,H0; simpl in *.
(* Goal: @eq rshare (@readable_part sh1 rsh1) (@readable_part sh3 rsh3) *)
  apply exist_ext.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  eapply join_positivity; eauto.
Qed.

Lemma dec_readable sh : {readable_share sh}+{~readable_share sh}.
Proof.
(* Goal: sumbool (readable_share sh) (not (readable_share sh)) *)
unfold readable_share, nonempty_share, nonidentity.
(* Goal: sumbool (not (@identity share Share.Join_ba (Share.glb Share.Rsh sh))) (not (not (@identity share Share.Join_ba (Share.glb Share.Rsh sh)))) *)
destruct (dec_share_identity (Share.glb Share.Rsh sh));[right|left].
(* Goal: not (readable_share Share.bot) *)
intro. contradiction.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
Defined.

Lemma dec_pure_readable sh : {pure_readable_share sh}+{~pure_readable_share sh}.
Proof.
(* Goal: sumbool (pure_readable_share sh) (not (pure_readable_share sh)) *)
unfold pure_readable_share.
(* Goal: sumbool (and (@eq Share.t (Share.glb Share.Lsh sh) Share.bot) (readable_share sh)) (not (and (@eq Share.t (Share.glb Share.Lsh sh) Share.bot) (readable_share sh))) *)
apply sumbool_dec_and.
(* Goal: sumbool (@eq Share.t (Share.glb Share.Lsh sh) Share.bot) (not (@eq Share.t (Share.glb Share.Lsh sh) Share.bot)) *)
(* Goal: sumbool (readable_share sh) (not (readable_share sh)) *)
apply eq_dec.
(* Goal: sumbool (readable_share sh) (not (readable_share sh)) *)
unfold readable_share, nonempty_share, nonidentity.
(* Goal: sumbool (not (@identity share Share.Join_ba (Share.glb Share.Rsh sh))) (not (not (@identity share Share.Join_ba (Share.glb Share.Rsh sh)))) *)
destruct (dec_share_identity (Share.glb Share.Rsh sh));[right|left].
(* Goal: not (readable_share Share.bot) *)
intro. contradiction.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
Defined.

Lemma dec_share_identity': forall sh: Share.t, Decidable.decidable (identity sh).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
destruct (dec_share_identity sh); [left|right]; auto.
Qed.

Lemma not_not_share_identity: forall sh: Share.t,
  ~ ~ (identity sh) -> identity sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 apply (Decidable.not_not _ (dec_share_identity' _)). auto.
Qed.

Lemma join_readable_part_eq:
  forall sh1 (rsh1: readable_share sh1)
         sh2 (nsh2: ~readable_share sh2)
         sh3 (rsh3: readable_share sh3),
        join sh1 sh2 sh3 -> 
        readable_part rsh1 = readable_part rsh3.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 intros.
(* Goal: @eq rshare (@readable_part sh1 rsh1) (@readable_part sh3 rsh3) *)
 apply exist_ext.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh sh3) *)
 apply not_not_share_identity in nsh2.
(* Goal: @eq Share.t sh Share.bot *)
 destruct H. subst sh3.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh1) (Share.glb Share.Rsh (Share.lub sh1 sh2)) *)
 apply identity_share_bot in nsh2.
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
 rewrite Share.distrib1. rewrite nsh2. rewrite Share.lub_bot.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 auto.
Qed.

Lemma join_readable_part:
  forall sh1 (rsh1: readable_share sh1) sh2 (rsh2: readable_share sh2) sh3 (rsh3: readable_share sh3),
   join sh1 sh2 sh3 ->
  join (readable_part rsh1) (readable_part rsh2)(readable_part rsh3).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t (Share.glb (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t t t0)) (@snd Share.t Share.t (@pair Share.t Share.t t t0))) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
red. red. simpl.
(* Goal: @eq Share.t sh Share.bot *)
destruct H. subst.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
split.
(* Goal: @eq Share.t (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot *)
rewrite Share.glb_assoc. rewrite (Share.glb_commute sh1).
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
rewrite <- Share.glb_assoc.
rewrite <- (Share.glb_assoc Share.Rsh).
(* Goal: @eq Share.t (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot *)
rewrite Share.glb_idem. rewrite Share.glb_assoc.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb al bl) (Share.glb bl ar)) (Share.glb (Share.lub al ar) br)) Share.bot *)
rewrite (Share.glb_commute sh2). rewrite H.
(* Goal: @eq Share.t (Share.glb br Share.bot) Share.bot *)
apply Share.glb_bot.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
rewrite <- Share.distrib1. auto.
Qed.

Lemma share_self_join_bot:
  forall sh: Share.t, join sh sh sh -> sh = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 intros.
(* Goal: @eq Share.t sh Share.bot *)
  destruct H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_idem in H. auto.
Qed.

Definition retainer_part (sh: Share.t) := Share.glb Share.Lsh sh.

Lemma retainer_part_nonreadable:
  forall sh, ~readable_share (retainer_part sh).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 intros.
(* Goal: not (readable_share (retainer_part sh)) *)
 unfold readable_share, retainer_part, nonempty_share, nonidentity.
(* Goal: not (readable_share Share.bot) *)
 intro. apply H; clear H.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
 rewrite <- Share.glb_assoc.
(* Goal: @eq Share.t (Share.glb (Share.glb Share.Rsh Share.Lsh) sh) Share.bot *)
 rewrite (Share.glb_commute Share.Rsh). 
(* Goal: @eq Share.t (Share.glb (Share.glb Share.Lsh Share.Rsh) sh) Share.bot *)
 rewrite glb_Lsh_Rsh.
(* Goal: @eq Share.t (Share.glb Share.bot sh) Share.bot *)
 rewrite Share.glb_commute, Share.glb_bot.
(* Goal: @identity share Share.Join_ba Share.bot *)
 apply bot_identity.
Qed.
Arguments retainer_part_nonreadable: clear implicits.

Lemma readable_share_lub:
 forall a b: Share.t, readable_share b -> readable_share (Share.lub a b).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
do 3 red in H|-*.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a b))) *)
contradict H.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.bot *)
apply identity_share_bot in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
rewrite Share.distrib1 in H.
(* Goal: @eq Share.t sh Share.bot *)
apply lub_bot_e in H. destruct H.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.lub (Share.glb br al) (Share.glb ar br))) Share.bot *)
rewrite H0.
(* Goal: @identity share Share.Join_ba Share.bot *)
apply bot_identity.
Qed.

Lemma retainer_part_join: forall sh1 sh2 sh3, 
  join sh1 sh2 sh3 -> join (retainer_part sh1) (retainer_part sh2) (retainer_part sh3).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @join Share.t Share.Join_ba (retainer_part sh1) (retainer_part sh2) (retainer_part sh3) *)
 unfold retainer_part.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 destruct H; subst; simpl  in *; split.
(* Goal: @eq Share.t (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot *)
 rewrite Share.glb_assoc. rewrite (Share.glb_commute sh1).
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
 rewrite <- Share.glb_assoc. rewrite <- Share.glb_assoc. rewrite Share.glb_idem.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb al bl) (Share.glb bl ar)) (Share.glb (Share.lub al ar) br)) Share.bot *)
 rewrite Share.glb_assoc. rewrite (Share.glb_commute sh2). rewrite H. 
(* Goal: @eq Share.t (Share.glb br Share.bot) Share.bot *)
 apply Share.glb_bot.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 rewrite <- Share.distrib1. auto.
Qed.

Lemma not_readable_Rsh_part:
 forall sh, ~ readable_share sh -> Share.glb Share.Rsh sh = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.bot *)
apply not_not_share_identity in H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply identity_share_bot in H. auto.
Qed.

Lemma join_parts1:
  forall L R (HC: Share.comp L = R) sh1 sh2 sh,         
         join sh1 sh2 (Share.glb L sh) ->
         Share.glb L sh1 = sh1 /\
         Share.glb R sh1 = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: and (@eq Share.t (Share.glb L sh1) sh1) (@eq Share.t (Share.glb R sh1) Share.bot) *)
cut (Share.glb L sh1 = sh1).
*
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
intro. split; auto.
rewrite <- H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
rewrite <- Share.glb_assoc.
(* Goal: @eq Share.t (Share.glb (Share.glb R L) sh1) Share.bot *)
rewrite (Share.glb_commute R).
(* Goal: @eq Share.t (Share.glb (Share.glb L (Share.comp L)) sh1) Share.bot *)
subst R. rewrite Share.comp2.
(* Goal: Share.Ord (Share.glb Share.Rsh sh) sh *)
rewrite Share.glb_commute.
(* Goal: @eq Share.t (Share.glb br Share.bot) Share.bot *)
apply Share.glb_bot.
*
(* Goal: @eq Share.t (Share.glb L sh1) sh1 *)
assert (Share.Ord sh1 L).
(* Goal: Share.Ord sh1 L *)
(* Goal: @eq Share.t (Share.glb L sh1) sh1 *)
apply Share.ord_trans with (Share.glb L sh).
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
apply leq_join_sub.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
exists sh2; auto.
(* Goal: Share.Ord (Share.glb sh Share.Rsh) sh *)
apply Share.glb_lower1.
(* Goal: @eq Share.t (Share.glb L sh1) sh1 *)
clear H.
(* Goal: @eq Share.t (Share.glb L sh1) sh1 *)
apply Share.ord_spec1 in H0.
(* Goal: @eq Share.t Share.Rsh (Share.comp Share.Lsh) *)
symmetry.
(* Goal: Share.Ord (Share.glb Share.Rsh sh) sh *)
rewrite Share.glb_commute.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
Qed.

Lemma join_parts:
  forall L R (HC: Share.comp L = R) sh1 sh2 sh,         
         join sh1 sh2 (Share.glb L sh) ->
         Share.glb L sh1 = sh1 /\
         Share.glb R sh1 = Share.bot /\
         Share.glb L sh2 = sh2 /\
         Share.glb R sh2 = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: and (@eq Share.t (Share.glb L sh1) sh1) (and (@eq Share.t (Share.glb R sh1) Share.bot) (and (@eq Share.t (Share.glb L sh2) sh2) (@eq Share.t (Share.glb R sh2) Share.bot))) *)
destruct (join_parts1 HC H).
(* Goal: and (@eq Share.t (Share.glb L sh1) sh1) (and (@eq Share.t (Share.glb R sh1) Share.bot) (and (@eq Share.t (Share.glb L sh2) sh2) (@eq Share.t (Share.glb R sh2) Share.bot))) *)
destruct (join_parts1 HC (join_comm H)).
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
split3; auto.
Qed.

Lemma comp_Rsh_Lsh: Share.comp Share.Rsh = Share.Lsh.
Proof.
rewrite <- (Share.comp_inv Share.Lsh).
(* Goal: @eq Share.t Share.Rsh (Share.comp Share.Lsh) *)
f_equal. symmetry. apply comp_Lsh_Rsh.
Qed.

Lemma glb_twice: forall a b, Share.glb a (Share.glb a b) = Share.glb a b.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros. rewrite <- Share.glb_assoc. rewrite Share.glb_idem; auto.
Qed.

Lemma glb_Lsh_Rsh':
  forall sh, Share.glb Share.Lsh (Share.glb Share.Rsh sh) = Share.bot.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
rewrite <- Share.glb_assoc. rewrite glb_Lsh_Rsh.
(* Goal: @eq Share.t (Share.glb br Share.bot) Share.bot *)
rewrite Share.glb_commute; apply Share.glb_bot.
Qed.

Lemma comp_parts_join:
 forall L R (HC: Share.comp L = R) a b c,
  join (Share.glb L a) (Share.glb L b) (Share.glb L c) ->
  join (Share.glb R a) (Share.glb R b) (Share.glb R c) ->
  join a b c.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @join Share.t Share.Join_ba a b c *)
subst R.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
split.
*
(* Goal: @eq Share.t (Share.lub a b) c *)
destruct H,H0.
(* Goal: @eq Share.t (Share.glb a b) Share.bot *)
clear H1 H2.
rewrite <- (Share.glb_top a), <- (Share.glb_commute Share.top).
rewrite <- (Share.comp1 L).
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub L (Share.comp L)) a) b) Share.bot *)
rewrite !(Share.glb_commute (Share.lub _ _)).
(* Goal: @eq Share.t (Share.glb (Share.glb a (Share.lub L (Share.comp L))) b) Share.bot *)
rewrite !Share.distrib1.
rewrite <- (Share.glb_top b), <- (Share.glb_commute Share.top).
rewrite <- (Share.comp1 L).
(* Goal: @eq Share.t b (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b)) *)
rewrite !(Share.glb_commute _ b).
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb a L) (Share.glb a (Share.comp L))) (Share.glb b (Share.lub L (Share.comp L)))) Share.bot *)
rewrite (Share.distrib1 b).
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb a L) (Share.glb a (Share.comp L))) (Share.lub (Share.glb b L) (Share.glb b (Share.comp L)))) Share.bot *)
rewrite !(Share.glb_commute a).
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) (Share.lub (Share.glb b L) (Share.glb b (Share.comp L)))) Share.bot *)
rewrite !(Share.glb_commute b).
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) Share.bot *)
pose proof (Share.glb_lower1 L a).
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) Share.bot *)
pose proof (Share.glb_lower1 L b).
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) Share.bot *)
pose proof (Share.glb_lower2 a (Share.comp L)). rewrite Share.glb_commute in H3.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) Share.bot *)
pose proof (Share.glb_lower2 b (Share.comp L)). rewrite Share.glb_commute in H4.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) Share.bot *)
forget (Share.glb L a) as al.
(* Goal: @eq Share.t (Share.glb (Share.lub al (Share.glb (Share.comp L) a)) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) Share.bot *)
forget (Share.glb (Share.comp L) a) as ar.
(* Goal: @eq Share.t (Share.glb (Share.lub al ar) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) Share.bot *)
forget (Share.glb L b) as bl.
(* Goal: @eq Share.t (Share.glb (Share.lub al ar) (Share.lub bl (Share.glb (Share.comp L) b))) Share.bot *)
forget (Share.glb (Share.comp L) b) as br.
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.lub al ar) bl) (Share.glb (Share.lub al ar) br)) Share.bot *)
rewrite (Share.glb_commute _ bl).
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb al bl) (Share.glb bl ar)) (Share.glb (Share.lub al ar) br)) Share.bot *)
rewrite Share.glb_commute. rewrite H.
(* Goal: @eq Share.t (Share.lub (Share.lub Share.bot (Share.glb bl ar)) (Share.glb (Share.lub al ar) br)) Share.bot *)
rewrite (Share.lub_commute Share.bot), Share.lub_bot.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.glb (Share.lub al ar) br)) Share.bot *)
rewrite (Share.glb_commute _ br).
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.lub (Share.glb br al) (Share.glb ar br))) Share.bot *)
rewrite (Share.glb_commute br ar). rewrite H0.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot) Share.bot *)
rewrite Share.lub_bot.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.glb br al)) Share.bot *)
apply Share.ord_spec1 in H1.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.glb br al)) Share.bot *)
apply Share.ord_spec1 in H2.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.glb br al)) Share.bot *)
apply Share.ord_spec1 in H3.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.glb br al)) Share.bot *)
apply Share.ord_spec1 in H4.
(* Goal: @eq Share.t (Share.lub (Share.glb bl ar) (Share.glb br al)) Share.bot *)
rewrite H1,H2,H3,H4.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.glb bl L) (Share.glb ar (Share.comp L))) (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L))) Share.bot *)
clear.
rewrite Share.glb_assoc. rewrite (Share.glb_commute ar). rewrite <- (Share.glb_assoc L).
(* Goal: @eq Share.t (Share.glb br (Share.glb (Share.glb L (Share.comp L)) al)) Share.bot *)
rewrite (Share.comp2 L).
(* Goal: @eq Share.t (Share.glb br (Share.glb al Share.bot)) Share.bot *)
rewrite (Share.glb_commute Share.bot). rewrite Share.glb_bot.
(* Goal: @eq Share.t (Share.glb br (Share.glb al Share.bot)) Share.bot *)
rewrite Share.glb_bot.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot) Share.bot *)
rewrite (Share.lub_commute Share.bot). rewrite Share.lub_bot.
(* Goal: @eq Share.t (Share.glb (Share.glb br (Share.comp L)) (Share.glb al L)) Share.bot *)
rewrite Share.glb_assoc. rewrite (Share.glb_commute al).
rewrite <- (Share.glb_assoc (Share.comp L)).
(* Goal: @eq Share.t (Share.glb br (Share.glb (Share.glb (Share.comp L) L) al)) Share.bot *)
rewrite (Share.glb_commute (Share.comp L)).
(* Goal: @eq Share.t (Share.glb br (Share.glb al Share.bot)) Share.bot *)
rewrite (Share.comp2 L). rewrite (Share.glb_commute Share.bot). rewrite Share.glb_bot.
(* Goal: @eq Share.t (Share.glb br Share.bot) Share.bot *)
apply Share.glb_bot.
*
(* Goal: @eq Share.t (Share.lub a b) c *)
destruct H,H0.
(* Goal: @eq Share.t (Share.lub a b) c *)
clear H H0.
rewrite <- (Share.glb_top c).
rewrite <- (Share.comp1 L).
(* Goal: @eq Share.t (Share.lub a b) (Share.glb c (Share.lub L (Share.comp L))) *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.lub a b) (Share.lub (Share.glb c L) (Share.glb c (Share.comp L))) *)
rewrite !(Share.glb_commute c).
(* Goal: @eq Share.t (Share.lub a b) (Share.lub (Share.glb L c) (Share.glb (Share.comp L) c)) *)
rewrite <- H1. rewrite <- H2.
(* Goal: @eq Share.t (Share.lub a b) (Share.lub (Share.glb L a) (Share.lub (Share.lub (Share.glb (Share.comp L) a) (Share.glb L b)) (Share.glb (Share.comp L) b))) *)
rewrite Share.lub_assoc.
rewrite <- (Share.lub_assoc (Share.glb L b)).
(* Goal: @eq Share.t (Share.lub a b) (Share.lub (Share.glb L a) (Share.lub (Share.lub (Share.glb L b) (Share.glb (Share.comp L) a)) (Share.glb (Share.comp L) b))) *)
rewrite (Share.lub_commute (Share.glb L b)).
(* Goal: @eq Share.t (Share.lub a b) (Share.lub (Share.glb L a) (Share.lub (Share.lub (Share.glb (Share.comp L) a) (Share.glb L b)) (Share.glb (Share.comp L) b))) *)
rewrite Share.lub_assoc.
rewrite <- Share.lub_assoc.
(* Goal: @eq Share.t (Share.lub a b) (Share.lub (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b))) *)
f_equal.
(* Goal: @eq Share.t a (Share.lub (Share.glb L a) (Share.glb (Share.comp L) a)) *)
(* Goal: @eq Share.t b (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b)) *)
rewrite !(Share.glb_commute _ a).
rewrite <- Share.distrib1.
(* Goal: @eq Share.t b (Share.glb b (Share.lub L (Share.comp L))) *)
rewrite (Share.comp1 L).
(* Goal: @eq Share.t b (Share.glb b Share.top) *)
rewrite Share.glb_top.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
(* Goal: @eq Share.t b (Share.lub (Share.glb L b) (Share.glb (Share.comp L) b)) *)
rewrite !(Share.glb_commute _ b).
rewrite <- Share.distrib1.
(* Goal: @eq Share.t b (Share.glb b (Share.lub L (Share.comp L))) *)
rewrite (Share.comp1 L).
(* Goal: @eq Share.t b (Share.glb b Share.top) *)
rewrite Share.glb_top.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
auto.
Qed.


Lemma left_right_join:
 forall a b c,
  join (Share.glb Share.Lsh a) (Share.glb Share.Lsh b) (Share.glb Share.Lsh c) ->
  join (Share.glb Share.Rsh a) (Share.glb Share.Rsh b) (Share.glb Share.Rsh c) ->
  join a b c.
Proof.
(* Goal: forall (a b c : Share.t) (_ : @join Share.t Share.Join_ba (Share.glb Share.Lsh a) (Share.glb Share.Lsh b) (Share.glb Share.Lsh c)) (_ : @join Share.t Share.Join_ba (Share.glb Share.Rsh a) (Share.glb Share.Rsh b) (Share.glb Share.Rsh c)), @join Share.t Share.Join_ba a b c *)
apply comp_parts_join.
(* Goal: @eq Share.t (Share.comp Share.Lsh) Share.Rsh *)
apply comp_Lsh_Rsh.
Qed.

Lemma lub_bot': forall sh, Share.lub Share.bot sh = sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Rsh Share.Lsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
rewrite Share.lub_commute.
(* Goal: @eq Share.t (Share.lub sh Share.bot) sh *)
apply Share.lub_bot.
Qed.

Lemma glb_Rsh_Lsh: Share.glb Share.Rsh Share.Lsh = Share.bot.
Proof.
(* Goal: Share.Ord (Share.glb Share.Rsh sh) sh *)
rewrite Share.glb_commute.
apply glb_Lsh_Rsh.
Qed.

Lemma join_writable1: forall sh1 sh2 sh,
   join sh1 sh2 sh -> writable_share sh1 -> writable_share sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
red in H0|-*.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
destruct H0 as [H1 H0]; split.
*
unfold nonempty_share, nonidentity in *.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Lsh sh)) *)
contradict H1.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
destruct H0.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Lsh sh1) *)
destruct (join_comp_parts comp_Rsh_Lsh H) as [_ ?].
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply split_identity in H2; auto.
*
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
eapply join_sub_trans; [apply H0 | ].
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
exists sh2; auto.
Qed.

Lemma join_writable_readable:
(* Goal: nonempty_share t *)
(* Goal: nonempty_share (Share.glb Share.Lsh (@fst Share.t Share.t (@pair Share.t Share.t t t0))) *)
  forall {sh1 sh2 sh}, 
   join sh1 sh2 sh -> writable_share sh1 -> readable_share sh2 -> False.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: False *)
red in H0,H1.
(* Goal: False *)
destruct H0 as [_ [a ?]].
(* Goal: False *)
destruct (join_assoc (join_comm H0) H) as [f [? ?]].
(* Goal: False *)
destruct H2.
(* Goal: False *)
rewrite H2 in H1.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply H1; auto.
Qed.

Definition writable0_share (sh: share) :=
    join_sub Share.Rsh sh.

Lemma writable_writable0: forall sh,
  writable_share sh -> writable0_share sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @eq Share.t sh Share.bot *)
destruct H. auto.
Qed.
Hint Resolve writable_writable0.

Lemma writable0_readable: forall sh,
  writable0_share sh -> readable_share sh.
Proof.
(* Goal: forall (sh : share) (_ : writable0_share sh), readable_share sh *)
unfold writable_share, readable_share.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: not (readable_share Share.bot) *)
intro.
(* Goal: False *)
destruct H as [a ?].
(* Goal: @eq Share.t sh Share.bot *)
destruct H.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.Rsh *)
subst sh.
(* Goal: False *)
rewrite Share.glb_absorb in H0.
clear - H0. unfold Share.Rsh in H0.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
destruct (Share.split Share.top) eqn:?. simpl in H0.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply split_nontrivial' in Heqp; auto.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply top_share_nonidentity in Heqp. auto.
Qed.
Hint Resolve writable0_readable.

Lemma writable0_Rsh: writable0_share Share.Rsh.
Proof.
(* Goal: writable0_share Share.Rsh *)
  unfold writable_share.
(* Goal: writable0_share Share.Rsh *)
  apply join_sub_refl.
Qed.

Lemma join_writable0_readable:
(* Goal: nonempty_share t *)
(* Goal: nonempty_share (Share.glb Share.Lsh (@fst Share.t Share.t (@pair Share.t Share.t t t0))) *)
  forall {sh1 sh2 sh}, 
   join sh1 sh2 sh -> writable0_share sh1 -> readable_share sh2 -> False.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: False *)
red in H0,H1.
(* Goal: False *)
destruct H0 as [a ?].
(* Goal: False *)
destruct (join_assoc (join_comm H0) H) as [f [? ?]].
(* Goal: False *)
destruct H2.
(* Goal: False *)
rewrite H2 in H1.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
apply H1; auto.
Qed.

Lemma join_writable01: forall sh1 sh2 sh,
   join sh1 sh2 sh -> writable0_share sh1 -> writable0_share sh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
red in H0|-*.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
eapply join_sub_trans; [apply H0 | ].
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
exists sh2; auto.
Qed.

Lemma writable0_share_dec: forall sh, {writable0_share sh} + {~ writable0_share sh}.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
  unfold writable0_share. intros.
(* Goal: sumbool (@join_sub Share.t Share.Join_ba Share.Rsh sh) (not (@join_sub Share.t Share.Join_ba Share.Rsh sh)) *)
  destruct (Share.EqDec_share (Share.glb Share.Rsh sh) Share.Rsh); [left|right].
*
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
  exists (Share.glb Share.Lsh sh).
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
  split.
  -
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh sh)) Share.bot *)
  rewrite <- Share.glb_assoc.
(* Goal: @eq Share.t (Share.glb (Share.glb Share.Rsh Share.Lsh) sh) Share.bot *)
  rewrite (Share.glb_commute Share.Rsh).
(* Goal: @eq Share.t (Share.glb (Share.glb Share.Lsh Share.Rsh) sh) Share.bot *)
  unfold Share.Rsh, Share.Lsh.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  destruct (Share.split Share.top) eqn:?. simpl.
(* Goal: @eq Share.t (Share.glb (Share.glb t t0) sh) Share.bot *)
  apply Share.split_disjoint in Heqp. rewrite Heqp.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_commute, Share.glb_bot. auto.
  -
(* Goal: @eq Share.t (Share.lub Share.Rsh (Share.glb Share.Lsh sh)) sh *)
  apply Share.distrib_spec with Share.Rsh.
  rewrite <- Share.lub_assoc. rewrite Share.lub_idem.
(* Goal: @eq Share.t (Share.lub Share.Rsh (Share.glb Share.Lsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  rewrite Share.distrib2.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Rsh Share.Lsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  rewrite Share.lub_commute.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  destruct (Share.split Share.top) eqn:?.
(* Goal: @eq Share.t (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  unfold Share.Lsh, Share.Rsh at 1.
(* Goal: @eq Share.t (Share.glb (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t t t0)) (@snd Share.t Share.t (@pair Share.t Share.t t t0))) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  rewrite Heqp. simpl.
(* Goal: @eq Share.t (Share.glb (Share.lub t t0) (Share.lub Share.Rsh sh)) (Share.lub Share.Rsh sh) *)
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub Share.Rsh (Share.glb Share.Lsh sh))) (Share.glb Share.Rsh sh) *)
  rewrite (Share.split_together _ _ _ Heqp).
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_commute, Share.glb_top. auto.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_absorb. rewrite e. auto.
*
(* Goal: not (@join_sub Share.t Share.Join_ba Share.Rsh sh) *)
  contradict n.
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.Rsh *)
  destruct n as [a [? ?]].
(* Goal: @eq Share.t (Share.glb Share.Rsh sh) Share.Rsh *)
  subst sh.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
  rewrite Share.glb_absorb. auto.
Qed.

Lemma writable0_share_glb_Rsh:
  forall sh, writable0_share sh -> writable0_share (Share.glb Share.Rsh sh).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
unfold writable0_share in *.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
apply leq_join_sub in H.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
apply leq_join_sub.
(* Goal: Share.Ord Share.Rsh (Share.glb Share.Rsh sh) *)
apply Share.ord_spec1.
(* Goal: @eq Share.t Share.Rsh (Share.glb Share.Rsh (Share.glb Share.Rsh sh)) *)
apply Share.ord_spec1 in H.
(* Goal: @eq Share.t Share.Rsh (Share.glb Share.Rsh (Share.glb Share.Rsh sh)) *)
rewrite <- H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
rewrite Share.glb_idem; auto.
Qed.

Lemma glb_split_lemma1:
  forall a b, Share.glb Share.Rsh a = Share.glb Share.Rsh b ->
     Share.glb Share.Rsh (fst (Share.split a)) =
     Share.glb Share.Rsh (fst (Share.split b)).
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
Abort.  (* Probably true, but not absolutely needed *)

Lemma glb_split_lemma2:
  forall a b, Share.glb Share.Rsh a = Share.glb Share.Rsh b ->
     Share.glb Share.Rsh (snd (Share.split a)) =
     Share.glb Share.Rsh (snd (Share.split b)).
Proof.
Abort.  (* Probably true, but not absolutely needed *)

Lemma fst_split_glb_orthogonal: forall sh : share,
identity (Share.glb Share.Rsh (fst (Share.split sh))) ->
identity (Share.glb Share.Rsh sh).
Proof.
Abort. (* not true? *)

Lemma snd_split_glb_orthogonal: forall sh : share,
identity (Share.glb Share.Rsh (snd (Share.split sh))) ->
identity (Share.glb Share.Rsh sh).
Abort.  (* not needed? *)

(** the following lemmas are useful in the concurrency proofs *)


  Lemma writable_not_join_readable:
    forall sh1 sh2,
      joins sh1 sh2 ->
      writable_share sh1 ->
      ~ readable_share sh2.
  Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
    intros.
(* Goal: not (readable_share Share.bot) *)
    intro.
(* Goal: False *)
    destruct H as [sh ?].
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
    apply join_writable_readable in H; eauto.
 Qed.

  Lemma writable_not_join_writable :
    forall sh1 sh2,
      joins sh1 sh2 ->
      writable_share sh1 ->
      ~ writable_share sh2.
   Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
     intros. intro.
(* Goal: False *)
    pose proof (writable_not_join_readable H H0).
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
    apply H2. auto.
   Qed.

  Lemma only_bot_joins_top:
    forall sh, joins Share.top sh -> sh = Share.bot.
  Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
    intros. destruct H. destruct H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
    rewrite Share.glb_commute in H. rewrite Share.glb_top in H. auto.
  Qed.

(*
  Lemma glb_Rsh_not_top:
    forall sh, ~ Share.glb Share.Rsh sh = Share.top.
  Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
    intros. apply glb_Rsh_not_top.
  Qed.
*)
  Lemma writable0_right:
    forall sh,  writable0_share (Share.glb Share.Rsh sh) ->
           writable0_share sh.
  Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
     intros.
     unfold writable0_share in *.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
     apply leq_join_sub in H.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
     apply leq_join_sub.
(* Goal: Share.Ord Share.Rsh sh *)
     eapply Share.ord_trans; try eassumption.
(* Goal: Share.Ord (Share.glb Share.Rsh sh) sh *)
     rewrite Share.glb_commute.
(* Goal: Share.Ord (Share.glb sh Share.Rsh) sh *)
     apply Share.glb_lower1.
  Qed.

Lemma join_readable_unreadable:
  forall sh1 sh2 sh3,
    join sh1 sh2 sh3 ->
    ~ writable0_share sh1 ->
    ~ readable_share sh2 ->
    ~ writable0_share sh3.
 (* Not true for for writable, only for writable0 *)
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
 intros.
(* Goal: not (writable0_share sh3) *)
 contradict H0.
 unfold writable0_share in *.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 destruct H0.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 destruct (join_comp_parts comp_Lsh_Rsh H) as [_ ?].
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 destruct (join_comp_parts comp_Lsh_Rsh H0) as [_ ?].
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 rewrite Share.glb_idem in H3.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 apply not_readable_Rsh_part in H1.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 rewrite H1 in H2.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 apply join_unit2_e in H2; [ | apply bot_identity].
 rewrite <- H2 in H3.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 assert (join_sub Share.Rsh (Share.glb Share.Rsh sh1)).
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 eexists; eauto.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh1 *)
 apply leq_join_sub in H4.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
 eapply leq_join_sub.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
 eapply Share.ord_trans; eauto.
(* Goal: Share.Ord (Share.glb Share.Rsh sh1) sh1 *)
 apply Share.glb_lower2.
Qed.

Lemma readable_glb:
   forall sh,
     readable_share sh ->
     readable_share (Share.glb Share.Rsh sh).
 Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
   intros.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
   unfold readable_share in *. rewrite glb_twice. auto.
 Qed.

 Lemma unreadable_glb:
   forall sh,
     ~readable_share sh ->
     ~readable_share (Share.glb Share.Rsh sh).
 Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
   intros.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
   unfold readable_share in *. rewrite glb_twice. auto.
 Qed.

  Lemma nonreadable_emptyshare: ~ readable_share emptyshare.
  Proof.
(* Goal: not (readable_share emptyshare) *)
    unfold emptyshare.
(* Goal: not (readable_share Share.bot) *)
    intro.
(* Goal: False *)
    hnf in H.
(* Goal: False *)
    rewrite Share.glb_bot in H.
(* Goal: not (nonempty_share (Share.glb Share.Rsh sh)) *)
    apply H; auto.
  Qed.
  
Lemma join_comp_Tsh:
  forall sh, sepalg.join sh (Share.comp sh) Tsh.
Proof.
(* Goal: forall sh : Share.t, @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
intros.
(* Goal: @join Share.t Share.Join_ba sh (Share.comp sh) Tsh *)
split.
(* Goal: @eq Share.t (Share.glb sh (Share.comp sh)) Share.bot *)
(* Goal: @eq Share.t (Share.lub sh (Share.comp sh)) Tsh *)
apply Share.comp2.
(* Goal: @eq Share.t (Share.lub sh (Share.comp sh)) Tsh *)
apply Share.comp1.
Qed.
