Require Import VST.msl.msl_standard.
Require Import VST.msl.Coqlib2.
Require Import VST.veric.shares.

Section UNPROVABLE.

Variable wishes_eq_horses : False.

Lemma unrel_glb:
 forall a b,
    Share.unrel a b = Share.unrel a (Share.glb a b).
(* Goal: forall r sh : Share.t, @eq Share.t (Share.rel r (Share.unrel r sh)) (Share.glb r sh) *)
contradiction wishes_eq_horses.
Qed.

Lemma share_rel_unrel':
  forall r sh,
    Share.rel r (Share.unrel r sh) = Share.glb r sh.
Proof.
(* Goal: forall r sh : Share.t, @eq Share.t (Share.rel r (Share.unrel r sh)) (Share.glb r sh) *)
contradiction wishes_eq_horses.
Qed.

Lemma share_sub_Lsh:
forall sh, identity (Share.unrel Share.Rsh sh) -> join_sub sh Share.Lsh.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
 intros.
 rewrite (Share.decompose_Rsh sh) in H.
 remember (decompose sh).
 symmetry in Heqp. destruct p as [sh1 sh2].
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
 simpl in H.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
 apply identity_share_bot in H. subst.
 generalize (top_correct' sh1);intro.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 sh3) *)
 destruct H.
 exists (Share.recompose (x, Share.bot)).
 rewrite Share.Lsh_recompose.
 assert (sh = Share.recompose (sh1, Share.bot)).
  rewrite <- Heqp. rewrite Share.recompose_decompose. trivial.
 rewrite H0.
 eapply Share.decompose_join.
 rewrite Share.decompose_recompose. f_equal.
 rewrite Share.decompose_recompose. f_equal.
 rewrite Share.decompose_recompose. f_equal.
 split. trivial.
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
 split. apply Share.glb_bot. apply Share.lub_bot.
Qed.

Lemma join_splice2_aux:
forall a1 a2 a3 b1 b2 b3,
Share.lub (Share.rel Share.Lsh (Share.lub a1 a2)) (Share.rel Share.Rsh (Share.lub b1 b2))
= Share.lub (Share.rel Share.Lsh a3) (Share.rel Share.Rsh b3) ->
Share.lub a1 a2 = a3 /\ Share.lub b1 b2 = b3.
Proof with try tauto.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
 intros. rewrite Share.lub_rel_recompose in H.
 generalize (Share.decompose_recompose (Share.lub a1 a2, Share.lub b1 b2));intro.
 rewrite H in H0.
 rewrite Share.lub_rel_recompose in H0.
 rewrite Share.decompose_recompose in H0.
 split;congruence.
Qed.

Lemma share_rel_unrel:
  forall r sh,
    join_sub sh r ->
    Share.rel r (Share.unrel r sh) = sh.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: @eq Share.t (Share.rel r (Share.unrel r sh)) sh *)
rewrite share_rel_unrel'.
(* Goal: @eq Share.t (Share.glb r sh) sh *)
destruct H as [a [H H0]].
(* Goal: @eq Share.t (Share.glb r sh) sh *)
subst r.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.lub (Share.glb Share.Lsh sh) (Share.glb Share.Rsh sh)) sh) sh) sh *)
rewrite Share.glb_commute.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Lsh a1)) (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b1))) (Share.glb (Share.rel Share.Rsh b2) (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)))) Share.bot *)
rewrite Share.distrib1.
(* Goal: @identity share Share.Join_ba (Share.rel Share.Rsh (Share.unrel Share.Rsh sh)) *)
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
rewrite H.
(* Goal: @eq Share.t (Share.lub (Share.rel Share.Lsh sh) Share.bot) (Share.rel Share.Lsh sh) *)
rewrite Share.lub_bot.
(* Goal: @eq Share.t (Share.glb sh sh) sh *)
apply Share.glb_idem.
Qed.

Lemma glb_rel_Lsh_Rsh:
 forall a b, Share.glb (Share.rel Share.Lsh a) (Share.rel Share.Rsh b) = Share.bot.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: @eq Share.t (Share.glb (Share.rel Share.Lsh a) (Share.rel Share.Rsh b)) Share.bot *)
assert (H := rel_leq Share.Lsh a).
(* Goal: @eq Share.t (Share.glb (Share.rel Share.Lsh a) (Share.rel Share.Rsh b)) Share.bot *)
assert (H0 := rel_leq Share.Rsh b).
(* Goal: @eq Share.t (Share.glb (Share.rel Share.Lsh a) (Share.rel Share.Rsh b)) Share.bot *)
apply leq_join_sub in H.
(* Goal: @eq Share.t (Share.glb (Share.rel Share.Lsh a) (Share.rel Share.Rsh b)) Share.bot *)
apply leq_join_sub in H0.
(* Goal: @eq Share.t (Share.glb (Share.rel Share.Lsh a) (Share.rel Share.Rsh b)) Share.bot *)
forget (Share.rel Share.Lsh a) as aL.
(* Goal: @eq Share.t (Share.glb aL (Share.rel Share.Rsh b)) Share.bot *)
forget (Share.rel Share.Rsh b) as bR.
(* Goal: @eq Share.t (Share.glb aL bR) Share.bot *)
apply Share.ord_antisym; [ | apply Share.bot_correct].
(* Goal: Share.Ord (Share.glb aL bR) Share.bot *)
rewrite <- glb_Lsh_Rsh.
(* Goal: Share.Ord (Share.glb aL bR) (Share.glb Share.Lsh Share.Rsh) *)
forget Share.Lsh as L.
(* Goal: Share.Ord (Share.glb aL bR) (Share.glb L Share.Rsh) *)
forget Share.Rsh as R.
(* Goal: Share.Ord (Share.glb aL bR) (Share.glb L R) *)
apply glb_less_both; auto.
Qed.

Lemma glb_Rsh_rel_Lsh_sh:
 forall sh,
  Share.glb Share.Rsh (Share.rel Share.Lsh sh) = Share.bot.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
destruct (Share.split Share.top) eqn:?.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.rel Share.Lsh sh)) Share.bot *)
unfold Share.Rsh, Share.Lsh. rewrite Heqp; simpl.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.lub (Share.glb Share.Lsh sh) (Share.glb Share.Rsh sh)) sh) sh) sh *)
rewrite Share.glb_commute.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
destruct (rel_join t t t0 _ (split_join _ _ _ Heqp)).
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
clear - H Heqp.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
pose proof (rel_leq t t0).
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
rewrite <- leq_join_sub in H0.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
rewrite Share.ord_spec1 in H0.
(* Goal: False *)
rewrite H0 in H.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
rewrite <- Share.glb_assoc in H.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
rewrite <- Share.rel_preserves_glb in H.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
pose proof (rel_leq t (Share.glb t t0)).
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
apply leq_join_sub in H1.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
apply Share.ord_spec1 in H1. rewrite <- H1 in H.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
clear H1.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
pose proof bot_identity. rewrite <- H in H1.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
apply (rel_nontrivial) in H1.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
destruct H1.
(* Goal: @identity Share.t Share.Join_ba sh *)
apply split_nontrivial' in Heqp; auto.
(* Goal: False *)
(* Goal: or (@identity Share.t Share.Join_ba t) (@identity Share.t Share.Join_ba Share.bot) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply identity_share_bot in Heqp.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
apply Share.nontrivial in Heqp; contradiction.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
clear H.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
apply identity_share_bot in H1.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
clear - H1.
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
pose proof (rel_leq t sh).
(* Goal: @eq Share.t (Share.glb (Share.rel t sh) t0) Share.bot *)
forget (Share.rel t sh) as b.
(* Goal: @eq Share.t (Share.glb b t0) Share.bot *)
destruct H as [a [? ?]].
(* Goal: @eq Share.t (Share.glb b t0) Share.bot *)
subst t.
(* Goal: @eq Share.t (Share.glb b t0) Share.bot *)
rewrite Share.glb_commute in H1; rewrite Share.distrib1 in H1.
(* Goal: @eq Share.t (Share.glb b t0) Share.bot *)
rewrite Share.glb_commute in H1.
(* Goal: @eq Share.t (Share.glb b t0) Share.bot *)
pose proof (Share.lub_upper1 (Share.glb b t0) (Share.glb t0 a)).
(* Goal: @eq Share.t (Share.glb b t0) Share.bot *)
rewrite H1 in H0.
(* Goal: @eq Share.t (Share.glb b t0) Share.bot *)
apply Share.ord_antisym; auto.
(* Goal: Share.Ord Share.bot (Share.glb b t0) *)
apply Share.bot_correct.
Qed.

Lemma right_nonempty_readable:
  forall rsh sh, sepalg.nonidentity sh <->
     readable_share (Share.splice rsh sh).
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share sh) (readable_share (Share.splice rsh sh)) *)
unfold readable_share, Share.splice.
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share sh) (nonempty_share (Share.glb Share.Rsh (Share.lub (Share.rel Share.Lsh rsh) (Share.rel Share.Rsh sh)))) *)
unfold nonempty_share,nonidentity.
assert (identity sh <-> identity (Share.glb Share.Rsh (Share.lub (Share.rel Share.Lsh rsh) (Share.rel Share.Rsh sh))));
  [ | intuition].
(* Goal: iff (@identity Share.t Share.Join_ba sh) (@identity Share.t Share.Join_ba (Share.glb Share.Rsh (Share.lub (Share.rel Share.Lsh rsh) (Share.rel Share.Rsh sh)))) *)
split; intro.
*
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply identity_share_bot in H. subst.
(* Goal: @identity share Share.Join_ba (Share.rel Share.Rsh Share.bot) *)
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
rewrite Share.rel_bot1.
(* Goal: @eq Share.t (Share.lub (Share.rel Share.Lsh sh) Share.bot) (Share.rel Share.Lsh sh) *)
rewrite Share.lub_bot.
(* Goal: @identity Share.t Share.Join_ba (Share.glb Share.Rsh (Share.rel Share.Lsh rsh)) *)
rewrite glb_Rsh_rel_Lsh_sh.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply bot_identity.
*
(* Goal: @identity Share.t Share.Join_ba sh *)
rewrite Share.distrib1 in H.
(* Goal: @identity Share.t Share.Join_ba sh *)
rewrite glb_Rsh_rel_Lsh_sh in H.
(* Goal: @identity Share.t Share.Join_ba sh *)
rewrite Share.lub_commute, Share.lub_bot in H.
assert (identity (Share.glb (Share.rel Share.Rsh Share.top) (Share.rel Share.Rsh sh)))
  by (rewrite Share.rel_top1; auto).
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
clear H.
(* Goal: @identity Share.t Share.Join_ba sh *)
rewrite <- Share.rel_preserves_glb in H0.
(* Goal: @identity Share.t Share.Join_ba sh *)
rewrite Share.glb_commute, Share.glb_top in H0.
(* Goal: @identity Share.t Share.Join_ba sh *)
apply rel_nontrivial in H0.
(* Goal: @identity Share.t Share.Join_ba sh *)
destruct H0; auto.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
unfold Share.Rsh in H.
destruct (Share.split Share.top) eqn:?; simpl in *.
(* Goal: @identity Share.t Share.Join_ba sh *)
apply split_nontrivial' in Heqp; auto.
(* Goal: @identity Share.t Share.Join_ba sh *)
apply top_share_nonidentity in Heqp.
(* Goal: @identity Share.t Share.Join_ba sh *)
contradiction.
Qed.

Lemma writable_share_right: forall sh, writable_share sh -> Share.unrel Share.Rsh sh = Share.top.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
 intros.
(* Goal: @eq Share.t (Share.unrel Share.Rsh sh) Share.top *)
 apply Share.contains_Rsh_e.
(* Goal: @join_sub Share.t Share.Join_ba Share.Rsh sh *)
 apply H.
Qed.

Lemma unrel_bot:
 forall sh, nonidentity sh -> Share.unrel sh Share.bot = Share.bot.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: @eq Share.t (Share.unrel sh Share.bot) Share.bot *)
rewrite <- (Share.rel_bot1 sh) at 1.
(* Goal: @eq Share.t (Share.unrel sh (Share.rel sh Share.bot)) Share.bot *)
rewrite Share.unrel_rel; auto.
Qed.

Lemma join_splice2_aux1:
  forall a1 a2 b1 b2,
  Share.lub (Share.rel Share.Lsh (Share.glb a1 a2)) (Share.rel Share.Rsh (Share.glb b1 b2)) = Share.bot ->
  Share.glb a1 a2 = Share.bot /\ Share.glb b1 b2 = Share.bot.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
Proof. intros.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
  rewrite !Share.rel_preserves_glb in H.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 sh3) *)
  apply lub_bot_e in H; destruct H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
  rewrite <- Share.rel_preserves_glb in H, H0.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
  pose proof (rel_nontrivial Share.Lsh (Share.glb a1 a2)).
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
  rewrite H in H1. specialize (H1 bot_identity). clear H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
  pose proof (rel_nontrivial Share.Rsh (Share.glb b1 b2)).
(* Goal: False *)
  rewrite H0 in H. specialize (H bot_identity). clear H0.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
  destruct H1. contradiction (Lsh_nonidentity H0).
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 sh3) *)
  destruct H. contradiction (Rsh_nonidentity H).
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
  apply identity_share_bot in H.
(* Goal: False *)
  apply identity_share_bot in H0.
(* Goal: @eq Share.t (Share.splice sh2 sh3) (Share.splice sh2 sh3) *)
  auto.
Qed.

Lemma join_splice:
  forall a1 a2 a3 b1 b2 b3,
 sepalg.join a1 a2 a3 ->
 sepalg.join b1 b2 b3 ->
 sepalg.join (Share.splice a1 b1)  (Share.splice a2 b2)  (Share.splice a3 b3).
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: @eq Share.t (Share.splice (Share.unrel Share.Lsh sh) (Share.unrel Share.Rsh sh)) sh *)
unfold Share.splice.
(* Goal: @join Share.t Share.Join_ba (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)) (Share.lub (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b2)) (Share.lub (Share.rel Share.Lsh a3) (Share.rel Share.Rsh b3)) *)
destruct H, H0.
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
split.
*
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Lsh a1)) (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b1))) (Share.glb (Share.rel Share.Rsh b2) (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)))) Share.bot *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)) (Share.rel Share.Lsh a2)) (Share.glb (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)) (Share.rel Share.Rsh b2))) Share.bot *)
do 2 rewrite (Share.glb_commute (Share.lub _ _)).
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Lsh a1)) (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b1))) (Share.glb (Share.rel Share.Rsh b2) (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)))) Share.bot *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Lsh a1)) (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b1))) (Share.glb (Share.rel Share.Rsh b2) (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)))) Share.bot *)
rewrite Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Lsh a1)) (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b1))) (Share.lub (Share.glb (Share.rel Share.Rsh b2) (Share.rel Share.Lsh a1)) (Share.glb (Share.rel Share.Rsh b2) (Share.rel Share.Rsh b1)))) Share.bot *)
rewrite !(Share.glb_commute (Share.rel _ a2)).
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb (Share.rel Share.Lsh a1) (Share.rel Share.Lsh a2)) (Share.glb (Share.rel Share.Rsh b1) (Share.rel Share.Lsh a2))) (Share.lub (Share.glb (Share.rel Share.Rsh b2) (Share.rel Share.Lsh a1)) (Share.glb (Share.rel Share.Rsh b2) (Share.rel Share.Rsh b1)))) Share.bot *)
rewrite !(Share.glb_commute (Share.rel _ b2)).
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb (Share.rel Share.Lsh a1) (Share.rel Share.Lsh a2)) (Share.glb (Share.rel Share.Rsh b1) (Share.rel Share.Lsh a2))) (Share.lub (Share.glb (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b2)) (Share.glb (Share.rel Share.Rsh b1) (Share.rel Share.Rsh b2)))) Share.bot *)
rewrite <- !Share.rel_preserves_glb.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.rel Share.Lsh (Share.glb a1 a2)) (Share.glb (Share.rel Share.Rsh b1) (Share.rel Share.Lsh a2))) (Share.lub (Share.glb (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b2)) (Share.rel Share.Rsh (Share.glb b1 b2)))) Share.bot *)
rewrite H,H0.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.rel Share.Lsh Share.bot) (Share.glb (Share.rel Share.Rsh b1) (Share.rel Share.Lsh a2))) (Share.lub (Share.glb (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b2)) (Share.rel Share.Rsh Share.bot))) Share.bot *)
rewrite !Share.rel_bot1.
(* Goal: @eq Share.t (Share.lub (Share.lub Share.bot (Share.glb (Share.rel Share.Rsh b1) (Share.rel Share.Lsh a2))) (Share.lub (Share.glb (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b2)) Share.bot)) Share.bot *)
rewrite (Share.lub_commute Share.bot).
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb (Share.rel Share.Rsh b1) (Share.rel Share.Lsh a2)) Share.bot) (Share.lub (Share.glb (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b2)) Share.bot)) Share.bot *)
rewrite !Share.lub_bot.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.lub (Share.glb Share.Lsh sh) (Share.glb Share.Rsh sh)) sh) sh) sh *)
rewrite Share.glb_commute.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b1)) (Share.glb (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b2))) Share.bot *)
rewrite !glb_rel_Lsh_Rsh.
(* Goal: @eq Share.t (Share.lub Share.bot Share.bot) Share.bot *)
apply Share.lub_bot.
*
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)) (Share.lub (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b2))) (Share.lub (Share.rel Share.Lsh a3) (Share.rel Share.Rsh b3)) *)
subst a3 b3.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)) (Share.lub (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b2))) (Share.lub (Share.rel Share.Lsh (Share.lub a1 a2)) (Share.rel Share.Rsh (Share.lub b1 b2))) *)
rewrite !Share.rel_preserves_lub.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Rsh b1)) (Share.lub (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b2))) (Share.lub (Share.lub (Share.rel Share.Lsh a1) (Share.rel Share.Lsh a2)) (Share.lub (Share.rel Share.Rsh b1) (Share.rel Share.Rsh b2))) *)
forget (Share.rel Share.Lsh a1) as La1.
(* Goal: @eq Share.t (Share.lub (Share.lub La1 (Share.rel Share.Rsh b1)) (Share.lub (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b2))) (Share.lub (Share.lub La1 (Share.rel Share.Lsh a2)) (Share.lub (Share.rel Share.Rsh b1) (Share.rel Share.Rsh b2))) *)
forget (Share.rel Share.Rsh b1) as Rb1.
(* Goal: @eq Share.t (Share.lub (Share.lub La1 Rb1) (Share.lub (Share.rel Share.Lsh a2) (Share.rel Share.Rsh b2))) (Share.lub (Share.lub La1 (Share.rel Share.Lsh a2)) (Share.lub Rb1 (Share.rel Share.Rsh b2))) *)
forget (Share.rel Share.Lsh a2) as La2.
(* Goal: @eq Share.t (Share.lub (Share.lub La1 Rb1) (Share.lub La2 (Share.rel Share.Rsh b2))) (Share.lub (Share.lub La1 La2) (Share.lub Rb1 (Share.rel Share.Rsh b2))) *)
forget (Share.rel Share.Rsh b2) as Rb2.
(* Goal: @eq Share.t (Share.lub (Share.lub La2 Rb2) Rb1) (Share.lub La2 (Share.lub Rb1 Rb2)) *)
rewrite !Share.lub_assoc.
(* Goal: @eq Share.t (Share.lub La2 (Share.lub Rb2 Rb1)) (Share.lub La2 (Share.lub Rb1 Rb2)) *)
f_equal.
(* Goal: @eq Share.t (Share.glb sh (Share.lub (Share.lub (Share.glb Share.Lsh sh) (Share.glb Share.Rsh sh)) sh)) sh *)
rewrite Share.lub_commute.
(* Goal: @eq Share.t (Share.lub (Share.lub La2 Rb2) Rb1) (Share.lub La2 (Share.lub Rb1 Rb2)) *)
rewrite !Share.lub_assoc.
(* Goal: @eq Share.t (Share.lub La2 (Share.lub Rb2 Rb1)) (Share.lub La2 (Share.lub Rb1 Rb2)) *)
f_equal.
(* Goal: @eq Share.t (Share.lub Rb2 Rb1) (Share.lub Rb1 Rb2) *)
apply Share.lub_commute.
Qed.

Lemma splice_bot2:
 forall sh, Share.splice sh Share.bot = Share.rel Share.Lsh sh.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: @eq Share.t (Share.splice (Share.unrel Share.Lsh sh) (Share.unrel Share.Rsh sh)) sh *)
unfold Share.splice.
(* Goal: @identity share Share.Join_ba (Share.rel Share.Rsh Share.bot) *)
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
rewrite Share.rel_bot1.
(* Goal: @eq Share.t (Share.lub (Share.rel Share.Lsh sh) Share.bot) (Share.rel Share.Lsh sh) *)
rewrite Share.lub_bot.
(* Goal: @eq Share.t (Share.splice sh2 sh3) (Share.splice sh2 sh3) *)
auto.
Qed.

Lemma splice_unrel_unrel:
  forall sh,
   Share.splice (Share.unrel Share.Lsh sh) (Share.unrel Share.Rsh sh) = sh.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: @eq Share.t (Share.splice (Share.unrel Share.Lsh sh) (Share.unrel Share.Rsh sh)) sh *)
unfold Share.splice.
(* Goal: @eq Share.t (Share.lub (Share.rel Share.Lsh (Share.unrel Share.Lsh sh)) (Share.rel Share.Rsh (Share.unrel Share.Rsh sh))) sh *)
rewrite !share_rel_unrel'.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Lsh sh) (Share.glb Share.Rsh sh)) sh *)
rewrite share_distrib2'.
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub sh Share.Rsh)) (Share.glb (Share.lub Share.Lsh sh) (Share.lub sh sh))) sh *)
rewrite Share.lub_idem.
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub Share.Lsh Share.Rsh) (Share.lub sh Share.Rsh)) (Share.glb (Share.lub Share.Lsh sh) sh)) sh *)
rewrite lub_Lsh_Rsh.
(* Goal: @eq Share.t (Share.glb (Share.glb Share.top (Share.lub sh Share.Rsh)) (Share.glb (Share.lub Share.Lsh sh) sh)) sh *)
rewrite (Share.glb_commute Share.top).
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub sh Share.Rsh) Share.top) (Share.glb (Share.lub Share.Lsh sh) sh)) sh *)
rewrite Share.glb_top.
(* Goal: @eq Share.t (Share.glb (Share.lub sh Share.Rsh) (Share.glb (Share.lub Share.Lsh sh) sh)) sh *)
rewrite <- Share.glb_assoc.
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub sh Share.Rsh) (Share.lub Share.Lsh sh)) sh) sh *)
rewrite (Share.lub_commute sh).
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub Share.Rsh sh) (Share.lub Share.Lsh sh)) sh) sh *)
rewrite share_distrib1'.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.lub (Share.glb Share.Rsh Share.Lsh) (Share.glb sh Share.Lsh)) (Share.lub (Share.glb Share.Rsh sh) (Share.glb sh sh))) sh) sh *)
rewrite (Share.glb_commute Share.Rsh).
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.lub (Share.glb Share.Lsh Share.Rsh) (Share.glb sh Share.Lsh)) (Share.lub (Share.glb Share.Rsh sh) (Share.glb sh sh))) sh) sh *)
rewrite glb_Lsh_Rsh.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.lub Share.bot (Share.glb sh Share.Lsh)) (Share.lub (Share.glb Share.Rsh sh) (Share.glb sh sh))) sh) sh *)
rewrite (Share.lub_commute Share.bot), Share.lub_bot.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb sh Share.Lsh) (Share.lub (Share.glb Share.Rsh sh) (Share.glb sh sh))) sh) sh *)
rewrite Share.glb_idem.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb sh Share.Lsh) (Share.lub (Share.glb Share.Rsh sh) sh)) sh) sh *)
rewrite (Share.glb_commute sh).
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb Share.Lsh sh) (Share.lub (Share.glb Share.Rsh sh) sh)) sh) sh *)
rewrite <- Share.lub_assoc.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.lub (Share.glb Share.Lsh sh) (Share.glb Share.Rsh sh)) sh) sh) sh *)
rewrite Share.glb_commute.
(* Goal: @eq Share.t (Share.glb sh (Share.lub (Share.lub (Share.glb Share.Lsh sh) (Share.glb Share.Rsh sh)) sh)) sh *)
rewrite Share.lub_commute.
(* Goal: @eq Share.t (Share.glb sh (Share.lub sh (Share.lub (Share.glb Share.Lsh sh) (Share.glb Share.Rsh sh)))) sh *)
rewrite Share.glb_absorb.
(* Goal: @eq Share.t (Share.splice sh2 sh3) (Share.splice sh2 sh3) *)
auto.
Qed.

Lemma join_splice2:
  forall a1 a2 a3 b1 b2 b3 : Share.t,
  join (Share.splice a1 b1) (Share.splice a2 b2) (Share.splice a3 b3) ->
  join a1 a2 a3 /\ join b1 b2 b3.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: and (@join Share.t Share.Join_ba a1 a2 a3) (@join Share.t Share.Join_ba b1 b2 b3) *)
unfold Share.splice in H.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 sh3) *)
destruct H.
(* Goal: and (@join Share.t Share.Join_ba a1 a2 a3) (@join Share.t Share.Join_ba b1 b2 b3) *)
unfold join, Share.Join_ba.
assert ((Share.glb a1 a2 = Share.bot /\ Share.glb b1 b2 = Share.bot)
         /\ (Share.lub a1 a2 = a3 /\ Share.lub b1 b2 = b3)); [ | intuition].
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
split.
*
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
clear - H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite share_distrib1' in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite (Share.lub_commute (Share.glb _ _)) in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite Share.lub_assoc in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite <- (Share.lub_assoc (Share.glb (Share.rel Share.Lsh _) _)) in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite (Share.lub_commute (Share.lub _ _)) in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite <- Share.lub_assoc in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite <- !Share.rel_preserves_glb in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite (Share.glb_commute (Share.rel Share.Rsh _)) in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite !glb_rel_Lsh_Rsh in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite (Share.lub_commute Share.bot), !Share.lub_bot in H.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
rewrite Share.lub_commute in H.
(* Goal: @eq Share.t (Share.splice sh2 sh3) (Share.splice sh2 sh3) *)
apply join_splice2_aux1; auto.
*
(* Goal: and (@eq Share.t (Share.lub a1 a2) a3) (@eq Share.t (Share.lub b1 b2) b3) *)
clear - H0.
(* Goal: and (@eq Share.t (Share.lub a1 a2) a3) (@eq Share.t (Share.lub b1 b2) b3) *)
rewrite Share.lub_assoc in H0.
(* Goal: and (@eq Share.t (Share.lub a1 a2) a3) (@eq Share.t (Share.lub b1 b2) b3) *)
rewrite (Share.lub_commute (Share.rel Share.Rsh _)) in H0.
(* Goal: and (@eq Share.t (Share.lub a1 a2) a3) (@eq Share.t (Share.lub b1 b2) b3) *)
rewrite <- !Share.lub_assoc in H0.
(* Goal: and (@eq Share.t (Share.lub a1 a2) a3) (@eq Share.t (Share.lub b1 b2) b3) *)
rewrite <- Share.rel_preserves_lub in H0.
(* Goal: and (@eq Share.t (Share.lub a1 a2) a3) (@eq Share.t (Share.lub b1 b2) b3) *)
rewrite Share.lub_assoc in H0.
(* Goal: and (@eq Share.t (Share.lub a1 a2) a3) (@eq Share.t (Share.lub b1 b2) b3) *)
rewrite <- Share.rel_preserves_lub in H0.
(* Goal: and (@eq Share.t (Share.lub a1 a2) a3) (@eq Share.t (Share.lub b1 b2) b3) *)
rewrite (Share.lub_commute b2) in H0.
(* Goal: @eq Share.t (Share.splice sh2 sh3) (Share.splice sh2 sh3) *)
apply join_splice2_aux; auto.
Qed.

Lemma nonidentity_rel_Lsh: forall t, nonidentity (Share.rel Share.Lsh t) -> nonidentity t.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
  intros.
(* Goal: @nonidentity Share.t Share.Join_ba pa_share t *)
  rewrite <- splice_bot2 in H.
(* Goal: forall _ : @nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh), @nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh) *)
  intro.
(* Goal: and (@eq Share.t (Share.glb a1 a2) Share.bot) (@eq Share.t (Share.glb b1 b2) Share.bot) *)
  apply H; clear H.
(* Goal: @identity Share.t Share.Join_ba (Share.splice t Share.bot) *)
  intros ? ? ?.
  rewrite <- (splice_unrel_unrel a), <- (splice_unrel_unrel b) in H |- *.
(* Goal: @eq Share.t (Share.splice (Share.unrel Share.Lsh a) (Share.unrel Share.Rsh a)) (Share.splice (Share.unrel Share.Lsh b) (Share.unrel Share.Rsh b)) *)
  forget (Share.unrel Share.Lsh a) as sh0.
(* Goal: @eq Share.t (Share.splice sh0 (Share.unrel Share.Rsh a)) (Share.splice (Share.unrel Share.Lsh b) (Share.unrel Share.Rsh b)) *)
  forget (Share.unrel Share.Rsh a) as sh1.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice (Share.unrel Share.Lsh b) (Share.unrel Share.Rsh b)) *)
  forget (Share.unrel Share.Lsh b) as sh2.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 (Share.unrel Share.Rsh b)) *)
  forget (Share.unrel Share.Rsh b) as sh3.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 sh3) *)
  apply join_splice2 in H.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 sh3) *)
  destruct H.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 sh3) *)
  apply H0 in H.
(* Goal: @eq Share.t (Share.splice sh0 sh1) (Share.splice sh2 sh3) *)
  apply bot_identity in H1.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
  subst.
(* Goal: @eq Share.t (Share.splice sh2 sh3) (Share.splice sh2 sh3) *)
  auto.
Qed.

Lemma readable_share_unrel_Rsh: forall sh, readable_share sh <-> nonunit (Share.unrel Share.Rsh sh).
unfold readable_share in *.
Proof.
(* Goal: forall sh : share, iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
intros.
(* Goal: iff (nonempty_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
unfold nonempty_share.
(* Goal: iff (@nonidentity share Share.Join_ba pa_share (Share.glb Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
transitivity (nonidentity (Share.unrel Share.Rsh sh)).
(* Goal: iff (@nonidentity share Share.Join_ba pa_share (Share.glb Share.Rsh sh)) (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
unfold nonidentity.
(* Goal: iff (not (@identity share Share.Join_ba (Share.glb Share.Rsh sh))) (not (@identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh))) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
split; intro; contradict H.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply identity_share_bot in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
rewrite <- share_rel_unrel'.
(* Goal: @identity share Share.Join_ba (Share.rel Share.Rsh (Share.unrel Share.Rsh sh)) *)
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
rewrite H.
(* Goal: @identity share Share.Join_ba (Share.rel Share.Rsh Share.bot) *)
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
rewrite Share.rel_bot1.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply bot_identity.
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
rewrite <- share_rel_unrel' in H.
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply rel_nontrivial in H.
(* Goal: @eq Share.t (Share.splice sh2 sh3) (Share.splice sh2 sh3) *)
destruct H; auto.
(* Goal: @identity Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
elimtype False.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply identity_share_bot in H.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
unfold Share.Rsh in H.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
destruct (Share.split Share.top) eqn:?. simpl in H. subst.
(* Goal: False *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply split_nontrivial' in Heqp.
(* Goal: False *)
(* Goal: or (@identity Share.t Share.Join_ba t) (@identity Share.t Share.Join_ba Share.bot) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply identity_share_bot in Heqp.
(* Goal: @eq Share.t (Share.splice sh2 sh3) (Share.splice sh2 sh3) *)
apply Share.nontrivial; auto.
(* Goal: or (@identity Share.t Share.Join_ba t) (@identity Share.t Share.Join_ba Share.bot) *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
right.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
apply bot_identity.
(* Goal: iff (@nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh)) (@nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh)) *)
split.
(* Goal: forall _ : @nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh), @nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh) *)
(* Goal: forall _ : @nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh), @nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh) *)
apply nonidentity_nonunit.
(* Goal: forall _ : @nonunit Share.t Share.Join_ba (Share.unrel Share.Rsh sh), @nonidentity Share.t Share.Join_ba pa_share (Share.unrel Share.Rsh sh) *)
intro.
hnf in H|-*; intro.
(* Goal: False *)
apply identity_share_bot in H0.
(* Goal: False *)
rewrite H0 in H.
(* Goal: False *)
apply (H Share.top).
(* Goal: @unit_for Share.t Share.Join_ba Share.bot Share.top *)
red.
(* Goal: @join Share.t Share.Join_ba Share.bot Share.top Share.top *)
apply bot_join_eq.
Qed.

End UNPROVABLE.

