(*
 * Copyright (c) 2009-2016, Andrew Appel, Robert Dockins,
    Aquinas Hobor and Le Xuan Bach
 *
 *)

Require Import VST.msl.base.
Require Import VST.msl.sepalg.
Require Import VST.msl.psepalg.
Require Import VST.msl.sepalg_generators.
Require Import VST.msl.boolean_alg.
Require Import VST.msl.eq_dec.

Require VST.msl.tree_shares.

Module Share : SHARE_MODEL := tree_shares.Share.
Import Share.

Definition share : Type := Share.t.

Instance pa_share : Perm_alg share := Share.pa.
Instance sa_share : Sep_alg share := Share.sa.
Instance ca_share : Canc_alg share := Share.ca.
Definition emptyshare : share := Share.bot.
Definition fullshare : share := Share.top.

Theorem leq_join_sub : forall s1 s2:Share.t,
  s1 <= s2 <-> join_sub s1 s2.
Proof.
(* Goal: iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  split; intros.
(* Goal: @join_sub t Join_ba s1 s2 *)
(* Goal: Ord s1 s2 *)
  pose (s' := glb s2 (comp s1)).
(* Goal: @join_sub t Join_ba s1 s2 *)
(* Goal: Ord s1 s2 *)
  exists s'.
(* Goal: @join t Join_ba s1 s' s2 *)
(* Goal: Ord s1 s2 *)
  simpl; split.
(* Goal: @eq t (lub s1 s') s2 *)
(* Goal: Ord s1 s2 *)
  subst s'.
(* Goal: @eq t (lub bot (glb c b)) bot *)
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite glb_commute.
(* Goal: @eq t (glb (glb d a) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite glb_assoc.
(* Goal: @eq t (glb s2 (glb (comp s1) s1)) bot *)
(* Goal: @eq t (lub s1 s') s2 *)
(* Goal: Ord s1 s2 *)
  rewrite (glb_commute (comp s1) s1).
(* Goal: @eq t (glb (glb sh1 (comp sh1)) sh3) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite comp2.
(* Goal: @eq t (glb s2 bot) bot *)
(* Goal: @eq t (lub s1 s') s2 *)
(* Goal: Ord s1 s2 *)
  apply glb_bot.
(* Goal: @eq t (lub s1 s') s2 *)
(* Goal: Ord s1 s2 *)
  subst s'.
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite distrib2.
(* Goal: @eq t (glb (lub sh1 sh3) (lub sh1 (comp sh1))) sh3 *)
  rewrite comp1.
(* Goal: @eq t (glb (lub sh1 sh3) top) sh3 *)
  rewrite glb_top.
(* Goal: @eq t (lub s1 s2) s2 *)
(* Goal: Ord s1 s2 *)
  rewrite <- ord_spec2; auto.

(* Goal: Ord s1 s2 *)
  destruct H as [s' H].
(* Goal: @join t Join_ba sh1 (glb sh3 (comp sh1)) sh3 *)
  destruct H.
(* Goal: Ord s1 s2 *)
  rewrite ord_spec2.
(* Goal: Ord sh1 sh3 *)
  rewrite <- H0.
(* Goal: @eq t (lub s1 (lub s1 s')) (lub s1 s') *)
  rewrite <- lub_assoc.
(* Goal: @eq t (lub (lub s1 s1) s') (lub s1 s') *)
  rewrite lub_idem; auto.
Qed.

Lemma top_correct' : forall x:t, join_sub x top.
Proof.
(* Goal: forall x : t, @join_sub t Join_ba x top *)
  intros; rewrite <- leq_join_sub; auto with ba.
Qed.

Lemma bot_identity : identity bot.
Proof.
(* Goal: @nonidentity t Join_ba pa_share top *)
  hnf; intros.
(* Goal: @join t Join_ba sh1 (glb sh3 (comp sh1)) sh3 *)
  destruct H.
(* Goal: @eq t a b *)
  rewrite lub_commute in H0.
(* Goal: False *)
  rewrite lub_bot in H0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  auto.
Qed.

Hint Resolve bot_identity.

Lemma identity_share_bot : forall s,
  identity s -> s = bot.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply identities_unique; auto.
(* Goal: @join_sub t Join_ba bot s *)
  exists s.
  apply join_comm.

(* Goal: @join_sub t Join_ba bot s *)
  destruct (top_correct' s).
  assert (x = top).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply H; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  subst x; auto.
(* Goal: @join t Join_ba bot s s *)
  destruct (top_correct' bot).
  assert (x = top).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply bot_identity; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  subst x; auto.
  apply join_comm in H1.
  destruct (join_assoc H0 H1); intuition.
  assert (x = top).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply H; auto.
  subst x.
  replace bot with s.
  rewrite identity_unit_equiv in H.
(* Goal: @join share Join_ba emptyshare x x *)
  trivial.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  eapply joins_units_eq; try apply H0. exists top; eauto.
(* Goal: @eq t (glb s2 bot) bot *)
(* Goal: @eq t (lub s1 s') s2 *)
(* Goal: Ord s1 s2 *)
  simpl. split. apply glb_bot. apply lub_bot.
Qed.

Lemma factoryOverlap' : forall f1 f2 n1 n2,
  isTokenFactory f1 n1 -> isTokenFactory f2 n2 -> joins f1 f2 -> False.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
  destruct H1.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
  destruct H1.
(* Goal: False *)
  apply (factoryOverlap f1 f2 n1 n2 H H0 H1).
Qed.

Lemma identityToken' : forall x, isToken x 0 <-> identity x.
Proof.
(* Goal: iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intro x; destruct (identityToken x); split; intros.
(* Goal: @nonidentity t Join_ba pa_share top *)
  hnf; intros.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  rewrite H in H2; auto.
(* Goal: False *)
  apply H0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply identity_share_bot; auto.
Qed.

Lemma nonidentityToken' : forall x n, (n > 0)%nat -> isToken x n -> nonidentity x.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @nonidentity t Join_ba pa_share x *)
  generalize (nonidentityToken x n H H0).
(* Goal: @Trip_alg t Join_ba *)
  repeat intro.
(* Goal: False *)
  apply H1.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply identity_share_bot; auto.
Qed.

Lemma nonidentityFactory' : forall x n, isTokenFactory x n -> nonidentity x.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @Trip_alg t Join_ba *)
  generalize (nonidentityFactory x n H); repeat intro.
(* Goal: False *)
  apply H0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply identity_share_bot; auto.
Qed.

Lemma split_join : forall x1 x2 x,
  split x = (x1,x2) -> join x1 x2 x.
Proof.
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
  intros; split.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply split_disjoint with x; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply split_together; auto.
Qed.

Lemma split_nontrivial' : forall x1 x2 x,
  split x = (x1, x2) ->
    (identity x1 \/ identity x2) ->
    identity x.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @identity t Join_ba x *)
  rewrite (split_nontrivial x1 x2 x H).
(* Goal: @identity t Join_ba bot *)
(* Goal: or (@identity t Join_ba a) (@identity t Join_ba x) *)
  apply bot_identity.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  destruct H0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  left; apply identity_share_bot; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  right; apply identity_share_bot; auto.
Qed.

Lemma rel_leq : forall a x, join_sub (rel a x) a.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @join_sub t Join_ba (rel a x) a *)
  rewrite <- leq_join_sub.

(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: Ord (rel a x) a *)
  rewrite ord_spec1.
(* Goal: @eq t (rel a x) (glb (rel a x) a) *)
  pattern a at 3.
(* Goal: (fun t0 : t => @eq t (rel a x) (glb (rel a x) t0)) a *)
  replace a with (rel a top).
(* Goal: @eq t (glb (rel a x) (rel a y)) bot *)
(* Goal: @eq t (lub (rel a x) (rel a y)) (rel a (lub x y)) *)
  rewrite <- rel_preserves_glb.
(* Goal: @eq t (glb (lub sh1 sh3) top) sh3 *)
  rewrite glb_top.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  auto.
(* Goal: @eq t (rel a top) a *)
  apply rel_top1.
Qed.

Lemma rel_join : forall a x y z,
  join x y z ->
  join (rel a x) (rel a y) (rel a z).
Proof.
(* Goal: forall (a x y z : t) (_ : @join t Join_ba x y z), @join t Join_ba (rel a x) (rel a y) (rel a z) *)
  simpl; intuition. inv H.
(* Goal: @join (option B) (@Join_lower B JB) (@Some B v) (@None B) (@Some B v) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
  constructor.
(* Goal: @eq t (glb (rel a x) (rel a y)) bot *)
(* Goal: @eq t (lub (rel a x) (rel a y)) (rel a (lub x y)) *)
  rewrite <- rel_preserves_glb.
(* Goal: @eq t (rel a (glb x y)) bot *)
(* Goal: @eq t (lub (rel a x) (rel a y)) (rel a (lub x y)) *)
  replace bot with (rel a bot).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  replace (glb x y) with bot; auto.
(* Goal: @eq t (rel a bot) bot *)
(* Goal: @identity t Join_ba x *)
  apply rel_bot1.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  rewrite <- rel_preserves_lub. auto.
Qed.

Lemma rel_join2 : forall a x y s,
  nonidentity a ->
  join (rel a x) (rel a y) s ->
  exists z, s = rel a z /\ join x y z.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  simpl; intros.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  destruct H0.
(* Goal: @ex t (fun z : t => and (@eq t s (rel a z)) (@join t Join_ba x y z)) *)
  exists (lub x y).
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
  split.
(* Goal: @eq t s (rel a (lub x y)) *)
(* Goal: @join t Join_ba x y (lub x y) *)
  rewrite <- H1.
(* Goal: @eq t (lub (rel a x) (rel a y)) (rel a (lub x y)) *)
(* Goal: @join t Join_ba x y (lub x y) *)
  symmetry.
(* Goal: @eq t (rel a (lub x y)) (lub (rel a x) (rel a y)) *)
(* Goal: @join t Join_ba x y (lub x y) *)
  apply rel_preserves_lub.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  split; auto.
(* Goal: @eq t (glb x y) bot *)
  rewrite <- rel_preserves_glb in H0.
(* Goal: @eq t x bot *)
(* Goal: @identity t Join_ba x *)
  replace bot with (rel a bot) in H0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply rel_inj_l with a; auto.
(* Goal: not (@eq t a bot) *)
(* Goal: @eq t (rel a bot) bot *)
  hnf; intros; apply H.
(* Goal: @identity t Join_ba bot *)
(* Goal: or (@identity t Join_ba a) (@identity t Join_ba x) *)
  subst a; apply bot_identity.
(* Goal: @eq t (rel a bot) bot *)
(* Goal: @identity t Join_ba x *)
  apply rel_bot1.
Qed.

Lemma rel_nontrivial : forall a x,
  identity (rel a x) ->
  (identity a \/ identity x).
Proof.
(* Goal: forall (a x : t) (_ : @identity t Join_ba (rel a x)), or (@identity t Join_ba a) (@identity t Join_ba x) *)
  intros a x H.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  destruct (eq_dec a bot); auto.
(* Goal: or (@identity t Join_ba a) (@identity t Join_ba x) *)
(* Goal: or (@identity t Join_ba a) (@identity t Join_ba x) *)
  subst a.
(* Goal: @identity t Join_ba bot *)
(* Goal: or (@identity t Join_ba a) (@identity t Join_ba x) *)
  left. apply bot_identity.

(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  right.
(* Goal: @identity t Join_ba x *)
  assert (rel a x = bot).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply identity_share_bot; auto.
(* Goal: @identity t Join_ba x *)
  assert (x = bot).
(* Goal: @eq t x bot *)
(* Goal: @identity t Join_ba x *)
  replace bot with (rel a bot) in H0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply rel_inj_l with a; auto.
(* Goal: @eq t (rel a bot) bot *)
(* Goal: @identity t Join_ba x *)
  apply rel_bot1.
(* Goal: @identity t Join_ba bot *)
(* Goal: or (@identity t Join_ba a) (@identity t Join_ba x) *)
  subst x; apply bot_identity.
Qed.

Instance share_cross_split : Cross_alg t.
Proof.
(* Goal: forall (a x y z : t) (_ : @join t Join_ba x y z), @join t Join_ba (rel a x) (rel a y) (rel a z) *)
  hnf; simpl; intuition. destruct H as [H1 H2]. destruct H0 as [H H3].
(* Goal: @join (option B) (@Join_lower B JB) (@Some B v) (@None B) (@Some B v) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
  exists (glb a c, glb a d, glb b c, glb b d); intuition; constructor.
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute a d).
(* Goal: @eq t (glb (glb d a) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite glb_assoc.
(* Goal: @eq t (glb a (glb c (glb d a))) bot *)
(* Goal: @eq t (lub (glb a c) (glb a d)) a *)
(* Goal: @eq t (glb (glb b c) (glb b d)) bot *)
(* Goal: @eq t (lub (glb b c) (glb b d)) b *)
(* Goal: @eq t (glb (glb a c) (glb b c)) bot *)
(* Goal: @eq t (lub (glb a c) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite <- (glb_assoc c d a).
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a' (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
  rewrite H.
(* Goal: @eq t (glb a (glb bot a)) bot *)
(* Goal: @eq t (lub (glb a c) (glb a d)) a *)
(* Goal: @eq t (glb (glb b c) (glb b d)) bot *)
(* Goal: @eq t (lub (glb b c) (glb b d)) b *)
(* Goal: @eq t (glb (glb a c) (glb b c)) bot *)
(* Goal: @eq t (lub (glb a c) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute bot a).
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  auto.
  rewrite <- distrib1;  rewrite H3; rewrite <- H2; auto with ba.
(* Goal: @eq t (lub (glb d a) (glb b d)) d *)
  rewrite (glb_commute b d).
(* Goal: @eq t (glb (glb d a) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite glb_assoc.
(* Goal: @eq t (glb b (glb c (glb d b))) bot *)
(* Goal: @eq t (lub (glb b c) (glb b d)) b *)
(* Goal: @eq t (glb (glb a c) (glb b c)) bot *)
(* Goal: @eq t (lub (glb a c) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite <- (glb_assoc c d b).
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a' (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
  rewrite H.
(* Goal: @eq t (glb b (glb bot b)) bot *)
(* Goal: @eq t (lub (glb b c) (glb b d)) b *)
(* Goal: @eq t (glb (glb a c) (glb b c)) bot *)
(* Goal: @eq t (lub (glb a c) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute bot b).
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  auto.
  rewrite <- distrib1;  rewrite H3; rewrite <- H2; auto with ba.
(* Goal: @eq t (lub (glb a c) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute a c).
(* Goal: @eq t (glb (glb d a) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite glb_assoc.
(* Goal: @eq t (glb c (glb a (glb b c))) bot *)
(* Goal: @eq t (lub (glb a c) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite <- (glb_assoc a b c).
(* Goal: @join (option B) (@Join_lower B JB) (@Some B v) (map_val a m2) (map_val a x) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
  rewrite H1.
(* Goal: @eq t (glb c (glb bot c)) bot *)
(* Goal: @eq t (lub (glb a c) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute bot c).
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  auto.
(* Goal: @eq t (lub (glb a c) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute a c).
(* Goal: @eq t (lub (glb c a) (glb b c)) c *)
(* Goal: @eq t (glb (glb a d) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute b c).
(* Goal: @eq t (lub (glb d a) (glb d b)) d *)
  rewrite <- distrib1; rewrite H2; rewrite <- H3; auto with ba.
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute a d).
(* Goal: @eq t (glb (glb d a) (glb b d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite glb_assoc.
(* Goal: @eq t (glb d (glb a (glb b d))) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite <- (glb_assoc a b d).
(* Goal: @join (option B) (@Join_lower B JB) (@Some B v) (map_val a m2) (map_val a x) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
  rewrite H1.
(* Goal: @eq t (glb d (glb bot d)) bot *)
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute bot d).
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  auto.
(* Goal: @eq t (lub (glb a d) (glb b d)) d *)
  rewrite (glb_commute a d).
(* Goal: @eq t (lub (glb d a) (glb b d)) d *)
  rewrite (glb_commute b d).
(* Goal: @eq t (lub (glb d a) (glb d b)) d *)
  rewrite <- distrib1; rewrite H2; rewrite <- H3; auto with ba.
Qed.

Lemma bot_correct' : forall x, join_sub bot x.
Proof.
(* Goal: forall x : t, @join_sub t Join_ba bot x *)
  intros s.
(* Goal: @join_sub t Join_ba bot s *)
  destruct (top_correct' s).
(* Goal: @join_sub t Join_ba bot s *)
  exists s.
(* Goal: @join t Join_ba bot s s *)
  destruct (top_correct' bot).
(* Goal: @join t Join_ba bot s s *)
  assert (x0 = top).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply bot_identity; auto.
(* Goal: @eq map (@exist (forall _ : A, option (prod (@lifted t Join_ba) B)) (@finMap A (prod (@lifted t Join_ba) B)) x f) (@exist (forall _ : A, option (prod (@lifted t Join_ba) B)) (@finMap A (prod (@lifted t Join_ba) B)) x0 f0) *)
(* Goal: @eq (forall _ : A, option (prod (@lifted t Join_ba) B)) x x0 *)
  subst x0.
(* Goal: @join t Join_ba bot s s *)
  apply join_comm in H0.
(* Goal: @join t Join_ba bot s s *)
  destruct (join_assoc H H0); intuition.
(* Goal: @identity share Join_ba sigma' *)
  apply join_comm in H2.
(* Goal: @join t Join_ba bot s s *)
  destruct (join_assoc H1 H2); intuition.
(* Goal: @join t Join_ba bot s s *)
  assert (s = x1).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply bot_identity; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  subst x1; auto.
Qed.

Lemma top_share_nonidentity : nonidentity top.
Proof.
(* Goal: @nonidentity t Join_ba pa_share top *)
  hnf; intros.
(* Goal: False *)
  assert (top = bot).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply identity_share_bot; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply nontrivial; auto.
Qed.

Lemma top_share_nonunit: nonunit top.
Proof.
(* Goal: @Trip_alg t Join_ba *)
  repeat intro. unfold unit_for in H.
(* Goal: @join t Join_ba sh1 (glb sh3 (comp sh1)) sh3 *)
  destruct H. rewrite glb_commute in H. rewrite glb_top in H. subst.
(* Goal: False *)
  rewrite lub_bot in H0. apply nontrivial; auto.
Qed.

Lemma bot_join_eq : forall x, join bot x x.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @join t Join_ba bot x x *)
  destruct (join_ex_identities x); intuition.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  destruct H0.
(* Goal: @join t Join_ba bot x x *)
  generalize (H _ _ H0).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  intros; subst; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  replace bot with x0; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply identity_share_bot; auto.
Qed.

Lemma join_bot_eq : forall x, join x bot x.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @join t Join_ba x bot x *)
  apply join_comm, bot_join_eq.
Qed.

Lemma bot_joins : forall x, joins bot x.
Proof.
(* Goal: forall x : t, @joins t Join_ba bot x *)
  intro x; exists x; apply bot_join_eq.
Qed.

Lemma dec_share_identity : forall x:t, { identity x } + { ~identity x }.
Proof.
(* Goal: @unit_for map Join_map empty_map empty_map *)
  intro x.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
  destruct (eq_dec x bot); subst.
(* Goal: @identity t Join_ba bot *)
(* Goal: or (@identity t Join_ba a) (@identity t Join_ba x) *)
  left; apply bot_identity.
(* Goal: sumbool (@identity t Join_ba x) (not (@identity t Join_ba x)) *)
  right; intro; elim n.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply identity_share_bot; auto.
Qed.

Lemma dec_share_nonunit : forall x:t, { nonunit x } + { ~ nonunit x }.
Proof.
(* Goal: @unit_for map Join_map empty_map empty_map *)
  intro x.
(* Goal: sumbool (@nonunit t Join_ba x) (not (@nonunit t Join_ba x)) *)
  destruct (dec_share_identity x) as [H | H]; [right | left].
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  + intro; revert H. apply nonunit_nonidentity; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  + apply nonidentity_nonunit; auto.
Qed.

Lemma fullshare_full : full fullshare.
Proof.
(* Goal: @full share Join_ba fullshare *)
  unfold full.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  generalize (Share.top_correct);intros.
(* Goal: @identity share Join_ba sigma' *)
  destruct H as [sigma'' ?].
(* Goal: @identity share Join_ba sigma' *)
  specialize (H0 sigma'').
(* Goal: @identity share Join_ba sigma' *)
  rewrite leq_join_sub in H0.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  destruct H0.
(* Goal: @identity share Join_ba sigma' *)
  destruct (join_assoc H H0) as [s [H1 H2]].
(* Goal: @identity share Join_ba sigma' *)
  apply join_comm in H2. apply unit_identity in H2.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  eapply split_identity; eauto.
Qed.

Lemma join_sub_fullshare : forall sh,
  join_sub fullshare sh -> sh = fullshare.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @eq share sh fullshare *)
  generalize fullshare_full; intro.
(* Goal: @eq share sh fullshare *)
  apply full_maximal in H0.
(* Goal: @eq share sh fullshare *)
  specialize ( H0 sh H).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  auto.
Qed.

Lemma dec_share_full : forall (sh : Share.t),
  {full sh} + {~full sh}.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
Proof with auto.
(* Goal: forall sh : share, @join share Join_ba emptyshare sh sh *)
  intro sh.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
  destruct (eq_dec sh top); subst.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a b)) (@In (prod A B) (@pair A B a b) l) *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  left. apply fullshare_full.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  right. intro. apply n.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  generalize (Share.top_correct sh);intro.
  apply leq_join_sub in H0.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  destruct H0.
  specialize ( H x). spec H. exists top...
  specialize ( H sh top (join_comm H0))...
Qed.

Lemma rel_congruence : forall a x1 x2,
  join_sub x1 x2 ->
  join_sub (rel a x1) (rel a x2).
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @join t Join_ba sh1 (glb sh3 (comp sh1)) sh3 *)
  destruct H.
(* Goal: @join_sub t Join_ba (rel a x1) (rel a x2) *)
  exists (rel a x).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  apply rel_join; auto.
Qed.

Lemma share_split_injective:
  forall sh1 sh2, Share.split sh1 = Share.split sh2 -> sh1=sh2.
Proof.
  intros sh1 sh2;
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    case_eq (Share.split sh1); case_eq (Share.split sh2); intros.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  generalize (split_join _ _ _ H); intro.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  generalize (split_join _ _ _ H0); intro.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
  inv H1.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  eapply join_eq; eauto.
Qed.

Lemma share_joins_constructive:
  forall sh1 sh2 : t , joins sh1 sh2 ->  {sh3 | join sh1 sh2 sh3}.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @sig t (fun sh3 : t => @join t Join_ba sh1 sh2 sh3) *)
  exists (lub sh1 sh2).
(* Goal: @join t Join_ba sh1 (glb sh3 (comp sh1)) sh3 *)
  destruct H.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  destruct H; split; auto.
Qed.

Lemma share_join_sub_constructive:
  forall sh1 sh3 : t , join_sub sh1 sh3 ->  {sh2 | join sh1 sh2 sh3}.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  intros.
(* Goal: @sig t (fun sh2 : t => @join t Join_ba sh1 sh2 sh3) *)
  exists (glb sh3 (comp sh1)).
(* Goal: @join t Join_ba sh1 (glb sh3 (comp sh1)) sh3 *)
  destruct H.
(* Goal: @join t Join_ba sh1 (glb sh3 (comp sh1)) sh3 *)
  destruct H.
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
  split.
(* Goal: @eq t (glb sh1 (glb sh3 (comp sh1))) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite (glb_commute sh3 (comp sh1)).
(* Goal: @eq t (glb sh1 (glb (comp sh1) sh3)) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite <- glb_assoc.
(* Goal: @eq t (glb (glb sh1 (comp sh1)) sh3) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite comp2.
(* Goal: @eq t (lub bot (glb c b)) bot *)
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite glb_commute.
(* Goal: @eq t (glb sh3 bot) bot *)
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite glb_bot.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  auto.
(* Goal: @eq t (lub sh1 (glb sh3 (comp sh1))) sh3 *)
  rewrite distrib2.
(* Goal: @eq t (glb (lub sh1 sh3) (lub sh1 (comp sh1))) sh3 *)
  rewrite comp1.
(* Goal: @eq t (glb (lub sh1 sh3) top) sh3 *)
  rewrite glb_top.
(* Goal: @eq t (lub sh1 sh3) sh3 *)
  rewrite <- ord_spec2.
(* Goal: Ord sh1 sh3 *)
  rewrite <- H0.
(* Goal: Ord sh1 (lub sh1 x) *)
  apply lub_upper1.
Qed.

Lemma triple_join_exists_share : Trip_alg t.
Proof.
(* Goal: @Trip_alg t Join_ba *)
  repeat intro.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
  destruct H; destruct H0; destruct H1.
(* Goal: @sig t (fun abc : t => @join t Join_ba ab c abc) *)
  exists (lub a (lub b c)).
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
  split.
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite <- H2.
(* Goal: @eq t (lub bot (glb c b)) bot *)
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite glb_commute.
(* Goal: @eq t (glb c (lub a b)) bot *)
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite distrib1.
(* Goal: @eq t (lub bot (glb c b)) bot *)
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite glb_commute.
(* Goal: @join (option B) (@Join_lower B JB) (@Some B v) (map_val a m2) (map_val a x) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
  rewrite H1.
(* Goal: @eq t (lub bot (glb c b)) bot *)
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite glb_commute.
(* Goal: @eq t (lub bot (glb b c)) bot *)
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite H0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  rewrite lub_bot; auto.
(* Goal: @eq t (lub ab c) (lub a (lub b c)) *)
  rewrite <- H2.
(* Goal: @eq t (lub (lub a b) c) (lub a (lub b c)) *)
  apply lub_assoc.
Qed.

Lemma nonemp_split_neq1: forall sh sh1 sh2, nonidentity sh -> split sh = (sh1, sh2) -> sh1 <> sh.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
Proof with auto.
  intros until sh2; intros H H0.
  destruct (dec_share_identity sh2).
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  generalize (split_nontrivial' _ _ _ H0); intro.
  spec H1...
  destruct (eq_dec sh1 sh)...
  subst sh1.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  generalize (split_join _ _ _ H0); intro.
  apply join_comm in H1.
  apply unit_identity in H1...
Qed.

Lemma nonemp_split_neq2: forall sh sh1 sh2, nonidentity sh -> split sh = (sh1, sh2) -> sh2 <> sh.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
Proof with auto.
  intros until sh2; intros H H0.
  destruct (dec_share_identity sh1).
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  generalize (split_nontrivial' _ _ _ H0); intro.
  spec H1...
  destruct (eq_dec sh2 sh)...
  subst sh2.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  generalize (split_join _ _ _ H0); intro.
  apply unit_identity in H1...
Qed.

Lemma bot_unit: forall sh,
  join emptyshare sh sh.
Proof.
(* Goal: forall sh : share, @join share Join_ba emptyshare sh sh *)
  intro sh.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
  generalize (bot_joins sh); generalize bot_identity; intros.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  destruct H0.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
  specialize ( H sh x H0). subst.
(* Goal: @join share Join_ba emptyshare x x *)
  trivial.
Qed.

Hint Resolve bot_unit.

Lemma join_bot: join emptyshare emptyshare emptyshare.
Proof.
(* Goal: @join share Join_ba emptyshare emptyshare emptyshare *)
  apply bot_unit.
Qed.


Lemma share_rel_nonidentity:
  forall {sh1 sh2}, nonidentity sh1 -> nonidentity sh2 -> nonidentity (Share.rel sh1 sh2).
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
intros.
(* Goal: @nonidentity t Join_ba pa_share (rel sh1 sh2) *)
unfold nonidentity in *.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
generalize (rel_nontrivial sh1 sh2); intro. intuition.
Qed.

Lemma share_rel_nonunit: forall {sh1 sh2: Share.t},
       nonunit sh1 -> nonunit sh2 -> nonunit (Share.rel sh1 sh2).
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
Proof. intros. apply nonidentity_nonunit. apply share_rel_nonidentity.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
intro. apply (@identity_unit _ _ _ sh1 Share.bot) in H1. apply H in H1; auto.
(* Goal: @joins t Join_ba sh2 bot *)
apply joins_comm. apply bot_joins.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
intro. apply (@identity_unit _ _ _ sh2 Share.bot) in H1. apply H0 in H1; auto.
(* Goal: @joins t Join_ba sh2 bot *)
apply joins_comm. apply bot_joins.
Qed.


Lemma decompose_bijection: forall sh1 sh2,
 sh1 = sh2 <-> decompose sh1 = decompose sh2.
Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
 intros.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
 split;intros. subst;trivial.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
 generalize (recompose_decompose sh1);intro.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
 generalize (recompose_decompose sh2);intro.
(* Goal: @eq t sh1 sh2 *)
 congruence.
Qed.

Module ShareMap.
Section SM.
  Variable A:Type.
  Variable EqDec_A : EqDec A.

  Variable B:Type.
  Variable JB: Join B.
  Variable paB : Perm_alg B.
  Variable saB : Sep_alg B.

  Definition map := fpm A (lifted Share.Join_ba * B).
  Instance Join_map : Join map := Join_fpm _.
  Instance pa_map : Perm_alg map := Perm_fpm _ _.
  Instance sa_map : Sep_alg map := Sep_fpm _ _.
  Instance ca_map {CA: Canc_alg B} : Canc_alg map := Canc_fpm _.
  Instance da_map {DA: Disj_alg B} : Disj_alg map := @Disj_fpm _ _ _ _ _ _.

  Definition map_share (a:A) (m:map) : share :=
    match lookup_fpm m a with
    | Some (sh,_) => lifted_obj sh
    | None => Share.bot
    end.

  Definition map_val (a:A) (m:map) : option B :=
    match lookup_fpm m a with
    | Some (_,b) => Some b
    | None => None
    end.

  Definition empty_map : map := empty_fpm _ _.

  Definition map_upd (a:A) (b:B) (m:map) : option map :=
    match lookup_fpm m a with
    | Some (sh,_) =>
        if eq_dec (lifted_obj sh) fullshare
           then Some (insert_fpm _ a (sh,b) m)
           else None
    | None => None
    end.

Lemma join_lifted {t} {J: Join t}:
    forall (a b c: lifted J), join a b c -> join (lifted_obj a) (lifted_obj b) (lifted_obj c).
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
Proof. destruct a; destruct b; destruct c; simpl; intros. apply H.
Qed.

  Lemma map_join_char : forall m1 m2 m3,
    join m1 m2 m3 <->
    (forall a,
       join (map_share a m1) (map_share a m2) (map_share a m3) /\
       join (map_val a m1) (map_val a m2) (map_val a m3)).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
  Proof with auto.
(* Goal: iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    split; intros.
    hnf in H. specialize ( H a).
(* Goal: iff (@eq (option B) (map_val a m) (@None B)) (@eq share (map_share a m) bot) *)
    unfold map_val, map_share, lookup_fpm.
    destruct (proj1_sig m1 a) as [[sh1 a1] | ];
    destruct (proj1_sig m2 a) as [[sh2 a2] | ];
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct (proj1_sig m3 a) as [[sh3 a3] | ]; inv H; try solve [inv H0]; simpl; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct H3; simpl in *; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    split. apply join_lifted; auto. constructor; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    split; apply join_unit2; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    split; apply join_unit1; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    split; apply join_unit1; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    split; apply join_unit1; auto.

(* Goal: @join t Join_ba sh1 (glb sh3 (comp sh1)) sh3 *)
    intro a. specialize ( H a). destruct H.
        unfold map_val, map_share, lookup_fpm in *.
    destruct (proj1_sig m1 a) as [[sh1 a1] | ];
    destruct (proj1_sig m2 a) as [[sh2 a2] | ];
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct (proj1_sig m3 a) as [[sh3 a3] | ]; inv H0; try solve [inv H1]; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    constructor. split; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    apply join_unit2_e in H; auto. apply join_unit2; auto.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    repeat f_equal. destruct sh1; destruct sh3; simpl in *; subst.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite (proof_irr n n0); auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    apply join_unit1_e in H; auto. apply join_unit1; auto.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    repeat f_equal. destruct sh2; destruct sh3; simpl in *; subst.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite (proof_irr n n0); auto.
(* Goal: @join (option B) (@Join_lower B JB) (@Some B v) (@None B) (@Some B v) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
    constructor. constructor.
 Qed.

  Lemma empty_map_identity {CAB: Disj_alg B}: identity empty_map.
  Proof.
(* Goal: @identity map Join_map empty_map *)
    rewrite identity_unit_equiv.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    intro x. simpl. auto. constructor.
  Qed.

  Lemma map_identity_unique {CAB: Disj_alg B}: forall m1 m2:map,
    identity m1 -> identity m2 -> m1 = m2.
  Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    intros.
(* Goal: @eq map m1 m2 *)
    destruct m1; destruct m2; simpl in *.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    cut (x = x0). intros. subst x0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    replace f0 with f; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    apply proof_irr; auto.
(* Goal: @eq (forall _ : A, option (prod (@lifted t Join_ba) B)) x x0 *)
    rewrite identity_unit_equiv in H, H0.
(* Goal: @eq (forall _ : A, option (prod (@lifted t Join_ba) B)) x x0 *)
    extensionality a.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    specialize ( H a); specialize ( H0 a).
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    apply lower_inv in H.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    apply lower_inv in H0.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    destruct H; destruct H0; simpl in *.
(* Goal: @eq t sh1 sh2 *)
    intuition; congruence.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    destruct s0 as [? [? [? [? [? [? ?]]]]]].
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite H in H1. inv H1. rewrite H0 in H; inv H.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    destruct x3. destruct H2. simpl in *. apply no_units in H. contradiction.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    destruct s as [? [? [? [? [? [? ?]]]]]].
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite H in H0; inv H0. rewrite H1 in H; inv H.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    destruct x2. destruct H2. simpl in *. apply no_units in H. contradiction.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    destruct s as [? [? [? [? [? [? ?]]]]]].
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite H in H0; inv H0. rewrite H1 in H; inv H.
(* Goal: @eq (option (prod (@lifted t Join_ba) B)) (x a) (x0 a) *)
    destruct x2. destruct H2. simpl in *. apply no_units in H. contradiction.
  Qed.

  Lemma map_identity_is_empty  {CAB: Disj_alg B} : forall m,
    identity m -> m = empty_map.
  Proof.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    intros; apply map_identity_unique; auto.
(* Goal: @identity map Join_map empty_map *)
    apply empty_map_identity.
  Qed.

  Lemma empty_map_join {CAB: Disj_alg B} : forall m,
    join empty_map m m.
  Proof.
(* Goal: forall m : map, @join map Join_map empty_map m m *)
    intro m. destruct (join_ex_units m).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    replace empty_map with x; auto.
(* Goal: @eq map x empty_map *)
    apply map_identity_is_empty.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    eapply unit_identity; eauto.
  Qed.

  Lemma map_val_bot  : forall a m,
    map_val a m = None <-> map_share a m = Share.bot.
  Proof.
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    do 2 intro.
(* Goal: iff (@eq (option B) (map_val a m) (@None B)) (@eq share (map_share a m) bot) *)
    unfold map_val, map_share, lookup_fpm.
(* Goal: not (@identity t Join_ba (rel sh1 sh2)) *)
    destruct (proj1_sig m a); intuition.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    disc.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    contradiction (no_units a0 a0). destruct a0. simpl in *. subst.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    contradiction (n bot). auto.
  Qed.

  Lemma map_upd_success : forall a v m,
    map_share a m = Share.top ->
    exists m', map_upd a v m = Some m'.
  Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    intros.
(* Goal: @ex map (fun m' : map => @eq (option map) match @lookup_fpm A (prod (@lifted t Join_ba) B) m a with | Some (pair sh b as p) => if @eq_dec t EqDec_share (@lifted_obj t Join_ba sh) fullshare then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B sh v) m) else @None map | None => @None map end (@Some map m')) *)
    unfold map_upd. simpl.
(* Goal: @ex map (fun m' : map => @eq (option map) match @lookup_fpm A (prod (@lifted t Join_ba) B) m a with | Some (pair sh b as p) => if @eq_dec t EqDec_share (@lifted_obj t Join_ba sh) fullshare then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B sh v) m) else @None map | None => @None map end (@Some map m')) *)
    unfold map_share, lookup_fpm in*.
    destruct (proj1_sig  m a).
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    destruct p.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a' (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    rewrite H.
(* Goal: @ex map (fun m' : map => @eq (option map) (if @eq_dec t EqDec_share top fullshare then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) else @None map) (@Some map m')) *)
(* Goal: @ex map (fun m' : map => @eq (option map) (@None map) (@Some map m')) *)
    unfold fullshare.
(* Goal: @ex map (fun m' : map => @eq (option map) (if @eq_dec t EqDec_share top top then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) else @None map) (@Some map m')) *)
(* Goal: @ex map (fun m' : map => @eq (option map) (@None map) (@Some map m')) *)
    destruct (eq_dec top top).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    eauto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    elim n; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    elim Share.nontrivial; auto.
  Qed.

  Lemma map_set_share1 : forall a v m m',
    map_upd a v m = Some m' ->
    map_share a m = Share.top.
  Proof.
(* Goal: forall (i j : A) (v : B) (m m' : map) (_ : not (@eq A i j)) (_ : @eq (option map) (map_upd j v m) (@Some map m')), @eq share (map_share i m) (map_share i m') *)
    unfold map_upd, map_share.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    intros.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    destruct (lookup_fpm m a); disc.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    destruct p.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct (eq_dec (lifted_obj l) fullshare); disc; auto.
  Qed.

  Lemma map_set_share2 : forall a v m m',
    map_upd a v m = Some m' ->
    map_share a m' = Share.top.
  Proof.
(* Goal: forall (i j : A) (v : B) (m m' : map) (_ : not (@eq A i j)) (_ : @eq (option map) (map_upd j v m) (@Some map m')), @eq share (map_share i m) (map_share i m') *)
    unfold map_upd, map_share.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    intros. destruct (lookup_fpm m a); disc.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    destruct p. destruct (eq_dec (lifted_obj l) fullshare); disc.
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    inv H.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gss. auto.
  Qed.

  Lemma map_set_share3 : forall a v m m',
    map_upd a v m = Some m' ->
    forall a',
      map_share a' m = map_share a' m'.
  Proof.
(* Goal: forall (i j : A) (v : B) (m m' : map) (_ : not (@eq A i j)) (_ : @eq (option map) (map_upd j v m) (@Some map m')), @eq share (map_share i m) (map_share i m') *)
    unfold map_upd, map_share.
(* Goal: forall (a : A) (v : B) (m m' : map) (_ : @eq (option map) match @lookup_fpm A (prod (@lifted t Join_ba) B) m a with | Some (pair sh b as p) => if @eq_dec t EqDec_share (@lifted_obj t Join_ba sh) fullshare then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B sh v) m) else @None map | None => @None map end (@Some map m')), @eq (option B) match @lookup_fpm A (prod (@lifted t Join_ba) B) m' a with | Some (pair l b as p) => @Some B b | None => @None B end (@Some B v) *)
    intros a v m m'.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    case_eq (lookup_fpm m a); intros; disc.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    destruct p.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    destruct (eq_dec (lifted_obj l) fullshare); disc.
(* Goal: @eq (option B) match @lookup_fpm A (prod (@lifted t Join_ba) B) m' a with | Some (pair l b as p) => @Some B b | None => @None B end (@Some B v) *)
    inv H0.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    destruct (eq_dec a a'). subst.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a' (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    rewrite H.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gss. auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gso; auto.
  Qed.

  Lemma map_gss_val: forall a v m m',
        map_upd a v m = Some m' ->
        map_val a m' = Some v.
  Proof.
(* Goal: forall (i j : A) (v : B) (m m' : map) (_ : not (@eq A i j)) (_ : @eq (option map) (map_upd j v m) (@Some map m')), @eq (option B) (map_val i m) (map_val i m') *)
    unfold map_upd, map_val.
(* Goal: forall (a : A) (v : B) (m m' : map) (_ : @eq (option map) match @lookup_fpm A (prod (@lifted t Join_ba) B) m a with | Some (pair sh b as p) => if @eq_dec t EqDec_share (@lifted_obj t Join_ba sh) fullshare then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B sh v) m) else @None map | None => @None map end (@Some map m')), @eq (option B) match @lookup_fpm A (prod (@lifted t Join_ba) B) m' a with | Some (pair l b as p) => @Some B b | None => @None B end (@Some B v) *)
    intros a v m m'.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    case_eq (lookup_fpm m a); intros; disc.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    destruct p.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    destruct (eq_dec (lifted_obj l) fullshare); disc.
(* Goal: @eq (option B) match @lookup_fpm A (prod (@lifted t Join_ba) B) m' a with | Some (pair l b as p) => @Some B b | None => @None B end (@Some B v) *)
    inv H0.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gss. auto.
  Qed.

  Lemma map_gso_val : forall i j v m m',
       i <> j ->
       map_upd j v m = Some m' ->
       map_val i m = map_val i m'.
  Proof.
(* Goal: forall (i j : A) (v : B) (m m' : map) (_ : not (@eq A i j)) (_ : @eq (option map) (map_upd j v m) (@Some map m')), @eq (option B) (map_val i m) (map_val i m') *)
    unfold map_upd, map_val.
(* Goal: forall (i j : A) (v : B) (m m' : map) (_ : not (@eq A i j)) (_ : @eq (option map) match @lookup_fpm A (prod (@lifted t Join_ba) B) m j with | Some (pair sh b as p) => if @eq_dec t EqDec_share (@lifted_obj t Join_ba sh) fullshare then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) j (@pair (@lifted t Join_ba) B sh v) m) else @None map | None => @None map end (@Some map m')), @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    intros i j v m m'.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    case_eq (lookup_fpm m j); intros; disc.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    destruct p.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    destruct (eq_dec (lifted_obj l) fullshare); disc.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    inv H1.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gso; auto.
  Qed.

  Lemma map_gso_share : forall i j v m m',
    i <> j ->
    map_upd j v m = Some m' ->
    map_share i m = map_share i m'.
  Proof.
(* Goal: forall (i j : A) (v : B) (m m' : map) (_ : not (@eq A i j)) (_ : @eq (option map) (map_upd j v m) (@Some map m')), @eq share (map_share i m) (map_share i m') *)
    unfold map_upd, map_share.
(* Goal: forall (i j : A) (v : B) (m m' : map) (_ : not (@eq A i j)) (_ : @eq (option map) match @lookup_fpm A (prod (@lifted t Join_ba) B) m j with | Some (pair sh b as p) => if @eq_dec t EqDec_share (@lifted_obj t Join_ba sh) fullshare then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) j (@pair (@lifted t Join_ba) B sh v) m) else @None map | None => @None map end (@Some map m')), @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    intros i j v m m'.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    case_eq (lookup_fpm m j); intros; disc.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    destruct p.
(* Goal: @eq share (@lifted_obj t Join_ba a0) bot *)
(* Goal: @eq (option B) (@Some B b) (@None B) *)
    destruct (eq_dec (lifted_obj l) fullshare); disc.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) m' i with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    inv H1.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gso; auto.
  Qed.

  Lemma map_upd_join : forall m1 m2 m3 a v m1',
    map_upd a v m1 = Some m1' ->
    join m1 m2 m3 ->
    exists m3', map_upd a v m3 = Some m3' /\
      join m1' m2 m3'.
  Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    intros.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    rewrite map_join_char in H0.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    destruct (H0 a).
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    generalize H; intros.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    apply map_set_share1 in H.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    rewrite H in H1.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    destruct H1.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    rewrite glb_commute in H1.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    rewrite glb_top in H1.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    rewrite H1 in H4.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    rewrite lub_bot in H4.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    symmetry in H4.
(* Goal: @ex map (fun m3' : map => and (@eq (option map) (map_upd a v m3) (@Some map m3')) (@join map Join_map m1' m2 m3')) *)
    destruct (map_upd_success a v _ H4).
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    exists x; split; auto.
(* Goal: @join map Join_map m1' m2 x *)
    clear H2.
(* Goal: @join map Join_map m1' m2 x *)
    rewrite map_join_char.
(* Goal: forall a : A, and (@join share Join_ba (map_share a m1') (map_share a m2) (map_share a x)) (@join (option B) (@Join_lower B JB) (map_val a m1') (map_val a m2) (map_val a x)) *)
    intro a'.
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
    destruct (eq_dec a a').
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
    subst a'. split.
(* Goal: @join share Join_ba (map_share a m1') (map_share a m2) (map_share a x) *)
(* Goal: @join (option B) (@Join_lower B JB) (map_val a m1') (map_val a m2) (map_val a x) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
    apply map_set_share2 in H3. rewrite H3.
(* Goal: @join share Join_ba top (map_share a m2) (map_share a x) *)
(* Goal: @join (option B) (@Join_lower B JB) (map_val a m1') (map_val a m2) (map_val a x) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
    apply map_set_share2 in H5. rewrite H5.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite H1. apply join_unit2; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    erewrite map_gss_val; eauto.
(* Goal: @join (option B) (@Join_lower B JB) (@Some B v) (map_val a m2) (map_val a x) *)
(* Goal: and (@join share Join_ba (map_share a' m1') (map_share a' m2) (map_share a' x)) (@join (option B) (@Join_lower B JB) (map_val a' m1') (map_val a' m2) (map_val a' x)) *)
    apply map_val_bot in H1. rewrite H1.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    erewrite map_gss_val; eauto. constructor.
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
    destruct (H0 a'). split.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite <- (map_gso_share a' a v m1 m1'); auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite <- (map_gso_share a' a v m3 x); auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite <- (map_gso_val a' a v m1 m1'); auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite <- (map_gso_val a' a v m3 x); auto.
  Qed.

  Definition build_map (l:list (A * B)) : map :=
     fold_right
      (fun (ab:A * B) m =>
        insert_fpm EqDec_A
           (fst ab)
           (mk_lifted fullshare top_share_nonunit,snd ab) m)
      empty_map l.

  Lemma build_map_results : forall (l:list (A*B)) a b,
    NoDup (List.map (@fst _ _) l) ->
    (In (a,b) l <->
    (map_val a (build_map l) = Some b /\
     map_share a (build_map l) = Share.top)).
  Proof.
(* Goal: @ex map (fun m' : map => @eq (option map) match @lookup_fpm A (prod (@lifted t Join_ba) B) m a with | Some (pair sh b as p) => if @eq_dec t EqDec_share (@lifted_obj t Join_ba sh) fullshare then @Some (fpm A (prod (@lifted t Join_ba) B)) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B sh v) m) else @None map | None => @None map end (@Some map m')) *)
    induction l; simpl.
(* Goal: iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    split; intros. elim H0.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct H0.
(* Goal: False *)
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    unfold build_map in H0. simpl in H0.
(* Goal: False *)
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    unfold map_val in H0.
(* Goal: False *)
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    simpl in H0. discriminate.
(* Goal: iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    intros. split; intros.
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
(* Goal: @eq share match @lookup_fpm A (prod (@lifted t Join_ba) B) m a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end match @lookup_fpm A (prod (@lifted t Join_ba) B) (@insert_fpm A EqDec_A (prod (@lifted t Join_ba) B) a (@pair (@lifted t Join_ba) B l v) m) a' with | Some (pair sh b as p) => @lifted_obj t Join_ba sh | None => bot end *)
    destruct H0; subst.
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold build_map.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    simpl fold_right.
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
    split.
(* Goal: @eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (@fold_right (fpm A (prod (@lifted share Join_ba) B)) (prod A B) (fun (ab : prod A B) (m : fpm A (prod (@lifted share Join_ba) B)) => @insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B ab) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B ab)) m) empty_map l))) (@Some B b) *)
(* Goal: @eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (@fold_right (fpm A (prod (@lifted share Join_ba) B)) (prod A B) (fun (ab : prod A B) (m : fpm A (prod (@lifted share Join_ba) B)) => @insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B ab) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B ab)) m) empty_map l))) top *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold map_val.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gss. simpl; auto.
(* Goal: @eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (@fold_right (fpm A (prod (@lifted share Join_ba) B)) (prod A B) (fun (ab : prod A B) (m : fpm A (prod (@lifted share Join_ba) B)) => @insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B ab) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B ab)) m) empty_map l))) top *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold map_share.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gss. simpl; auto.
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    generalize H0; intro H1.
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite IHl in H0.
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    inv H.
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    assert (fst a <> a0).
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    intro. subst a0.
(* Goal: False *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    elim H4.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    clear -H1. induction l; simpl in *; intuition; subst; auto.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct H0.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold build_map. simpl fold_right.
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
    split.
(* Goal: @eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (@fold_right (fpm A (prod (@lifted share Join_ba) B)) (prod A B) (fun (ab : prod A B) (m : fpm A (prod (@lifted share Join_ba) B)) => @insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B ab) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B ab)) m) empty_map l))) (@Some B b) *)
(* Goal: @eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (@fold_right (fpm A (prod (@lifted share Join_ba) B)) (prod A B) (fun (ab : prod A B) (m : fpm A (prod (@lifted share Join_ba) B)) => @insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B ab) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B ab)) m) empty_map l))) top *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold map_val.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gso; auto.
(* Goal: @eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (@fold_right (fpm A (prod (@lifted share Join_ba) B)) (prod A B) (fun (ab : prod A B) (m : fpm A (prod (@lifted share Join_ba) B)) => @insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B ab) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B ab)) m) empty_map l))) top *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold map_share.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gso; auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    inv H. auto.
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    inv H.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct H0.
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct a.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    destruct (eq_dec a a0).
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    subst a0.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a b)) (@In (prod A B) (@pair A B a b) l) *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    left. f_equal.
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold build_map in H.
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold map_val in H.
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    simpl fold_right in H.
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gss in H.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    inv H. auto.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    right.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite IHl; auto.
(* Goal: and (@eq (option B) (map_val a0 (build_map l)) (@Some B b)) (@eq share (map_share a0 (build_map l)) top) *)
    split.
(* Goal: @eq (option B) (map_val a0 (build_map l)) (@Some B b) *)
(* Goal: @eq share (map_share a0 (build_map l)) top *)
    revert H.
(* Goal: forall _ : @eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B (@pair A B a b0)) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B (@pair A B a b0))) (build_map l))) (@Some B b), @eq (option B) (map_val a0 (build_map l)) (@Some B b) *)
(* Goal: @eq share (map_share a0 (build_map l)) top *)
    unfold build_map, map_val.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    simpl fold_right.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gso; auto.
(* Goal: @eq share (map_share a0 (build_map l)) top *)
    revert H0.
(* Goal: forall _ : @eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B (@pair A B a b0)) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B (@pair A B a b0))) (build_map l))) top, @eq share (map_share a0 (build_map l)) top *)
    unfold build_map, map_share.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    simpl fold_right.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gso; auto.
  Qed.

  Lemma build_map_join : forall (l1 l2:list (A * B)),
    NoDup (List.map (@fst _ _) (l1++l2)) ->
    join  (build_map l1)
          (build_map l2)
          (build_map (l1++l2)).
  Proof.
(* Goal: forall (a0 : A) (b : B) (_ : @NoDup A (@cons A (@fst A B a) (@List.map (prod A B) A (@fst A B) l))), iff (or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l)) (and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top)) *)
    induction l1; intros.
    simpl app.
    unfold build_map at 1.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    simpl fold_right.
    apply empty_fpm_join; auto with typeclass_instances.
(* Goal: @eq B b0 b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    inv H.
    simpl app.
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    unfold build_map.
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    simpl fold_right.
    apply insert_fpm_join. auto with typeclass_instances.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    2: apply (IHl1 l2); auto.
    assert (~In (fst a) (List.map (@fst _ _) l2)).
(* Goal: not (@eq A (@fst A B a) a0) *)
(* Goal: and (@eq (option B) (map_val a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) (@Some B b)) (@eq share (map_share a0 (@insert_fpm A EqDec_A (prod (@lifted share Join_ba) B) (@fst A B a) (@pair (@lifted share Join_ba) B (@mk_lifted share Join_ba fullshare top_share_nonunit) (@snd A B a)) (build_map l))) top) *)
(* Goal: @NoDup A (@List.map (prod A B) A (@fst A B) l) *)
(* Goal: or (@eq (prod A B) a (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    intro.
    elim H2.
    rewrite map_app.
    apply in_or_app.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    auto.
    clear -H.
(* Goal: @unit_for (@lifted t Join_ba) (@Join_lift t Join_ba) (@exist t (@nonunit t Join_ba) x n) (@exist t (@nonunit t Join_ba) x n) *)
    induction l2; simpl in *.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    auto.
(* Goal: @eq B b b *)
(* Goal: or (@eq (prod A B) (@pair A B a b0) (@pair A B a0 b)) (@In (prod A B) (@pair A B a0 b) l) *)
    rewrite fpm_gso; auto.
  Qed.

End SM.
End ShareMap.

