Require Import VST.msl.base.
Require Import VST.msl.boolean_alg.
Require Import VST.msl.sepalg.
Require Import VST.msl.functors.
Require Import VST.msl.sepalg_functors.
Require Import VST.msl.sepalg_generators.
Require Import VST.msl.shares.
Require Import VST.msl.cross_split.
Require Import VST.msl.psepalg.
Require Import VST.msl.pshares.
Require Import VST.msl.eq_dec.

Require VST.msl.predicates_sa.

Lemma in_app:   (* THIS IS FROM compcert/Coqlib.v *)
  forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
  intros. split; intro. apply in_app_or. auto. apply in_or_app. auto.
Qed.

Definition list_disjoint {A: Type} (l1 l2: list A) : Prop :=   (* THIS IS FROM compcert/Coqlib.v *)
  forall (x y: A), In x l1 -> In y l2 -> x <> y.

Inductive pshareval_join' {A}{JA: Join A}
  : option (pshare * A) ->  option (pshare * A) ->  option (pshare * A) -> Prop :=
  | pshareval_None1: forall x, pshareval_join' None x x
  | pshareval_None2: forall x, pshareval_join' x None x
  | pshareval_Some: forall x y z,
      join (fst x) (fst y) (fst z) ->
      join (snd x) (snd y) (snd z) ->
      pshareval_join' (Some x) (Some y) (Some z).

Lemma pshareval_join_e{A}{JA: Join A}:  forall a b c, join a b c -> pshareval_join' a b c.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
inv H; [constructor 1 | constructor 2 | constructor 3]; auto.
(* Goal: @join A JA (@snd pshare A a1) (@snd pshare A a2) (@snd pshare A a3) *)
apply H0.
(* Goal: @join A JA (@snd pshare A a1) (@snd pshare A a2) (@snd pshare A a3) *)
apply H0.
Qed.

Lemma pshareval_join_i{A}{JA: Join A}: forall a b c, pshareval_join' a b c -> join a b c.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
inv H; [constructor 1 | constructor 2 | constructor 3]; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
split; auto.
Qed.

Module Type ENV.

Parameter env: forall (key: Type) (A: Type), Type.

Section ENVSEC.
Context {key: Type}{A: Type}.

Instance JA: Join A := Join_equiv A. (* It's a feature, not a bug, that this Instance is not visible as an Instance
   outside the Section *)

Parameter env_get: forall (rho: env key A) (id: key), option (pshare * A).
Parameter env_set_sh: forall {KE: EqDec key} (id: key) (v: option (pshare * A)) (rho: env key A), env key A.

Definition env_set  {KE: EqDec key} (id: key) (v: A) (rho: env key A) : env key A :=
     env_set_sh id (Some (pfullshare, v)) rho.

Axiom env_gss: forall {KE: EqDec key}  i a rho, env_get (env_set i a rho) i = Some (pfullshare, a).
Axiom env_gso: forall {KE: EqDec key}  i j a rho, i <> j -> env_get (env_set j a rho) i = env_get rho i.

Axiom env_gss_sh: forall {KE: EqDec key} i v rho,
  env_get (env_set_sh i v rho) i = v.

Axiom env_gso_sh: forall {KE: EqDec key} i j v rho, i <> j ->
   env_get (env_set_sh j v rho) i = env_get rho i.

Definition finite_idfun (f: key -> option (pshare * A)) :=
  exists l, forall a, ~In a l -> f a = None.

Parameter mk_env:  forall (f: key -> option (pshare * A)), finite_idfun f -> env key A.
(*
Arguments mk_env.
*)

Axiom env_get_mk_env:  forall (f: key -> option (pshare * A)) P, env_get (mk_env f P) = f.

Axiom env_finite: forall rho, finite_idfun (env_get rho).

Axiom env_ext: forall rho1 rho2, env_get rho1 = env_get rho2 -> rho1=rho2.

Axiom env_funct: forall rho1 rho2,
  rho1 = rho2 -> forall id sh1 sh2 v1 v2, env_get rho1 id = Some(sh1, v1)
  -> env_get rho2 id = Some(sh2, v2)
  -> v1 = v2.

Parameter empty_env : env key A.

Axiom env_get_empty: forall id, env_get empty_env id = None.

(* SEPARATION ALGEBRAS *)
(* We use the Section to hide these instances, because  variables-as-resources clients
  will want Join_env, but global-variables users will want Join_equiv.
  Only the variables-as-resources clients should add these instances,
  which is done in the Module EnvSA,  below
*)
Instance Join_env: Join (env key A) :=
    fun (rho1 rho2 rho3: env key A) => join (env_get rho1) (env_get rho2) (env_get rho3).
Parameter Perm_env: forall {PA: Perm_alg A}, Perm_alg (env key A).  Existing Instance Perm_env.

Instance Sep_env {SA: Sep_alg A}: Sep_alg (env key A).
(* Goal: @Sep_alg (env key A) Join_env *)
 refine (mkSep Join_env (fun _ => empty_env) _ _).
(* Goal: forall t : env key A, @unit_for (env key A) Join_env empty_env t *)
(* Goal: forall (a b c : env key A) (_ : @join (env key A) Join_env a b c), @eq (env key A) empty_env empty_env *)
 repeat intro; rewrite env_get_empty; constructor.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
 auto.
Defined.

Instance Sing_env  {SA: Sep_alg A} : Sing_alg (env key A).
(* Goal: @Sing_alg (env key A) Join_env (@Sep_env SA) *)
  refine (mkSing empty_env _). reflexivity.
Defined.

Parameter Canc_env: forall {PA: Perm_alg A}{CA: Canc_alg A}, Canc_alg (env key A). Existing Instance Canc_env.
Parameter Disj_env: forall {PA: Perm_alg A}{DA: Disj_alg A}, Disj_alg (env key A).   Existing Instance Disj_env.
Parameter Cross_env : Cross_alg (env key A).  Existing Instance Cross_env.


(* env_mapsto and the lemmas about it are in a Separation Logic, not just a separation algebra.
  We have two style of separation logic (direct and ageable), and this module Env is usable with
   either kind.  Thus, we build primitives whose names start with _ to avoid polluting the
  namespace; then we reveal them at appropriate types in EnvSL and EnvASL, below.
*)
Import VST.msl.predicates_sa.

(* ENV_MAPSTO *)
Parameter _env_mapsto: forall {KE: EqDec key}  (id: key) (sh: Share.t) (v: A), pred (env key A).

Axiom _env_mapsto_exists: forall {KE: EqDec key}  id sh v, exists rho, _env_mapsto id (pshare_sh sh) v rho.

Axiom _env_get_mapsto: forall {KE: EqDec key}  id v rho,
  (exists sh, env_get rho id = Some (sh,v)) =
  (exp (fun sh => _env_mapsto id sh v) * TT)%pred rho.

Axiom _env_get_mapsto': forall {KE: EqDec key}  id (sh: pshare) v rho,
  env_get rho id = Some(pfullshare,v) ->
       (_env_mapsto id (pshare_sh sh) v * TT)%pred rho.

Axiom _env_mapsto_set: forall {KE: EqDec key} id v,
  _env_mapsto id Share.top v (env_set id v empty_env).

Axiom _env_mapsto_set_sh: forall {KE: EqDec key} id (sh: pshare) v,
  _env_mapsto id (pshare_sh sh) v (env_set_sh id (Some (sh, v)) empty_env).

Axiom _env_mapsto_get: forall {KE: EqDec key}  id sh v rho,
  _env_mapsto id sh v rho
   -> exists Pf,
        env_get rho id = Some (exist nonunit sh Pf, v).

Axiom _env_mapsto_get_neq: forall {KE: EqDec key}  (id1 id2: key) (sh: Share.t) (v: A) rho,
  id1 <> id2 -> _env_mapsto id1 sh v rho -> env_get rho id2 = None.

Axiom _env_mapsto_empty_env: forall {KE: EqDec key}  id v sh, ~(_env_mapsto id sh v empty_env).

Axiom _env_mapsto_splittable: forall {KE: EqDec key}  id v (sh sh1 sh2: pshare) rho,
  join sh1 sh2 sh
  -> (_env_mapsto id (pshare_sh sh) v rho
        <-> (_env_mapsto id (pshare_sh sh1) v * _env_mapsto id (pshare_sh sh2) v)%pred rho).
End ENVSEC.

End ENV.

Module Env: ENV.

Section ENVSEC.
Context {key: Type}{A: Type}.
Instance JA: Join A := Join_equiv A.

Definition env := fpm key (pshare * A).

Definition env_get (rho: env) (id: key) : option (pshare * A) := lookup_fpm rho id.

Definition env_set_sh {KE: EqDec key} (id: key) (v: option (pshare * A)) (rho: env) : env :=
  insert'_fpm _ id v rho.

Definition env_set {KE: EqDec key} (id: key) (v: A) (rho: env) : env :=
  insert_fpm _ id (pfullshare,v) rho.

Lemma env_gss {KE: EqDec key} : forall i a rho, env_get (env_set i a rho) i = Some (pfullshare, a).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @eq (option (prod pshare A)) (env_get (@env_set KE i a rho) i) (@Some (prod pshare A) (@pair pshare A pfullshare a)) *)
apply fpm_gss.
Qed.

Lemma env_gso {KE: EqDec key}: forall i j a rho, i <> j -> env_get (env_set j a rho) i = env_get rho i.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
apply fpm_gso; auto.
Qed.

Lemma env_gss_sh {KE: EqDec key}: forall i v rho, env_get (env_set_sh i v rho) i = v.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
  intros. unfold env_get, env_set_sh.
(* Goal: @eq (option (prod pshare A)) (@lookup_fpm key (prod pshare A) (@insert'_fpm key KE (prod pshare A) j v rho) i) (@lookup_fpm key (prod pshare A) rho i) *)
  unfold lookup_fpm, insert'_fpm; simpl. destruct rho as [f Hf]. simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  destruct (eq_dec i i); auto. contradiction n; auto.
Qed.

Lemma env_gso_sh {KE: EqDec key} : forall i j v rho, i <> j -> env_get (env_set_sh j v rho) i = env_get rho i.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
  intros. unfold env_get, env_set_sh.
(* Goal: @eq (option (prod pshare A)) (@lookup_fpm key (prod pshare A) (@insert'_fpm key KE (prod pshare A) j v rho) i) (@lookup_fpm key (prod pshare A) rho i) *)
  unfold lookup_fpm, insert'_fpm; simpl. destruct rho as [f Hf]. simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  destruct (eq_dec j i); auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  subst; contradiction H; auto.
Qed.

Definition finite_idfun (f: key -> option (pshare * A)) :=
          (exists l, forall a, ~In a l -> f a = None).

Definition mk_env_aux: forall f, finite_idfun f -> finMap f.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @finMap key (prod pshare A) f *)
unfold finMap.
destruct H as  [l ?].
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (if @in_dec key (@eq_dec key KE) a ids then @None (prod pshare A) else @env_get key A rho a) (@None (prod pshare A))) *)
exists l.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
unfold compose; simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
rewrite H; auto.
Qed.

Definition mk_env (f: key -> option (pshare * A))  (FIN: finite_idfun f):  env :=
   exist _ _ (mk_env_aux _ FIN).

Lemma env_get_mk_env: forall (f: key -> option (pshare * A)) P, env_get (mk_env f P) = f.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @eq (forall _ : key, option (prod pshare A)) (env_get (mk_env f P)) f *)
unfold mk_env, env_get.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @eq (forall _ : key, option (prod pshare A)) (fun id : key => f id) f *)
unfold compose.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
extensionality id; auto.
Qed.

Lemma env_finite: forall rho, finite_idfun (env_get rho).
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: finite_idfun (env_get rho) *)
destruct rho.
(* Goal: finite_idfun (env_get (@exist (forall _ : key, option (prod pshare A)) (@finMap key (prod pshare A)) x f)) *)
unfold finite_idfun, finMap in *.
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (env_get (@exist (forall _ : key, option (prod pshare A)) (fun f : forall _ : key, option (prod pshare A) => @ex (list key) (fun l0 : list key => forall (a0 : key) (_ : not (@In key a0 l0)), @eq (option (prod pshare A)) (f a0) (@None (prod pshare A)))) x f) a) (@None (prod pshare A))) *)
generalize f; intros [l ?].
(* Goal: @ex (list key) (fun l0 : list key => forall (a : key) (_ : not (@In key a l0)), @eq (option (prod pshare A)) (env_get (@exist (forall _ : key, option (prod pshare A)) (fun f : forall _ : key, option (prod pshare A) => @ex (list key) (fun l : list key => forall (a0 : key) (_ : not (@In key a0 l)), @eq (option (prod pshare A)) (f a0) (@None (prod pshare A)))) x (@ex_intro (list key) (fun l : list key => forall (a0 : key) (_ : not (@In key a0 l)), @eq (option (prod pshare A)) (x a0) (@None (prod pshare A))) l e)) a) (@None (prod pshare A))) *)
exists l; simpl in *.
(* Goal: forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (x a) (@None (prod pshare A)) *)
intros; unfold compose in *.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
apply e; auto.
Qed.

Lemma env_ext: forall rho1 rho2, env_get rho1 = env_get rho2 -> rho1=rho2.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @eq env rho1 rho2 *)
destruct rho1; destruct rho2; simpl in *.
(* Goal: @eq env (@exist (forall _ : key, option (prod pshare A)) (@finMap key (prod pshare A)) x f) (@exist (forall _ : key, option (prod pshare A)) (@finMap key (prod pshare A)) x0 f0) *)
apply exist_ext.
(* Goal: @eq (forall _ : key, option (prod pshare A)) x x0 *)
unfold env_get in *.
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
simpl in *.
(* Goal: @eq (forall _ : key, option (prod pshare A)) (@env_get key A (@restrict_env key A KE (@nil key) ge)) (@env_get key A (@empty_env key A)) *)
extensionality id.
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
generalize (equal_f  H id); intro.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (x id); destruct (x0 id); inv H0; auto.
Qed.

Lemma env_funct: forall rho1 rho2,
  rho1 = rho2 -> forall id sh1 sh2 v1 v2, env_get rho1 id = Some(sh1, v1)
  -> env_get rho2 id = Some(sh2, v2)
  -> v1 = v2.
Proof.
(* Goal: forall (rho1 rho2 : env) (_ : @eq env rho1 rho2) (id : key) (sh1 sh2 : pshare) (v1 v2 : A) (_ : @eq (option (prod pshare A)) (env_get rho1 id) (@Some (prod pshare A) (@pair pshare A sh1 v1))) (_ : @eq (option (prod pshare A)) (env_get rho2 id) (@Some (prod pshare A) (@pair pshare A sh2 v2))), @eq A v1 v2 *)
  intros rho1 rho2 H id sh1 sh2 v1 v2 H1 H2.
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
  destruct rho1; destruct rho2; unfold env_get in *; simpl in *.
(* Goal: @eq A v1 v2 *)
  inversion H; subst x0. inv H. congruence.
Qed.

Lemma finite_idfun_empty: finite_idfun (fun _ => None).
Proof.
(* Goal: finite_idfun (fun _ : key => @None (prod pshare A)) *)
exists nil.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
auto.
Qed.

Definition empty_env : env := mk_env _ finite_idfun_empty.

Lemma env_get_empty: forall id, env_get empty_env id = None.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
unfold empty_env. rewrite env_get_mk_env; auto.
Qed.

Instance Join_env: Join env :=
    fun (rho1 rho2 rho3: env) => join (env_get rho1) (env_get rho2) (env_get rho3).

Lemma Join_env_eq: Join_env = Join_fpm (Join_prod _ Join_pshare _ JA).
Proof.
(* Goal: @eq (Join env) Join_env (@Join_fpm key (prod pshare A) (Join_prod pshare Join_pshare A JA)) *)
  repeat intro.
 extensionality rho1 rho2 rho3;
destruct rho1 as [rho1 V1]; destruct rho2 as [rho2 V2]; destruct rho3 as [rho3 V3].
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
unfold Join_env, Join_fpm; simpl.
apply prop_ext; split; intros H id; specialize ( H id);
unfold env_get in * ; simpl in *; clear - H;
destruct (rho1 id) as [[[sh1 v1] n1]| ];
destruct (rho2 id) as [[[sh2 v2] n2]| ];
destruct (rho3 id) as [[[sh3 v3] n3]| ];
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
inv H; simpl in *;  try constructor; auto.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v1) n3)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v3) n3)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v2) n3)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v3) n3)) *)
rewrite (proof_irr v1 v3); constructor.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v2) n3)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v3) n3)) *)
rewrite (proof_irr v2 v3); constructor.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v1) n3)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v3) n3)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v2) n3)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v3) n3)) *)
rewrite (proof_irr v1 v3); constructor.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v2) n3)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh3 v3) n3)) *)
rewrite (proof_irr v2 v3); constructor.
Qed.

Instance Perm_env {PA: Perm_alg A}: @Perm_alg env Join_env.
Proof.
(* Goal: @Cross_alg env Join_env *)
  rewrite Join_env_eq. apply Perm_fpm; auto with typeclass_instances.
Qed.

Instance Sep_env {SA: Sep_alg A}: @Sep_alg env Join_env.
(* Goal: @Sep_alg (env key A) Join_env *)
 refine (mkSep Join_env (fun _ => empty_env) _ _).
(* Goal: forall t : env key A, @unit_for (env key A) Join_env empty_env t *)
(* Goal: forall (a b c : env key A) (_ : @join (env key A) Join_env a b c), @eq (env key A) empty_env empty_env *)
 repeat intro; rewrite env_get_empty; constructor.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
 auto.
Defined.

Instance Sing_env {SA: Sep_alg A}: @Sing_alg env Join_env Sep_env.
(* Goal: @Sing_alg (env key A) Join_env (@Sep_env SA) *)
  refine (mkSing empty_env _). reflexivity.
Defined.

Instance Canc_env {PA: Perm_alg A}{CA: Canc_alg A}: @Canc_alg env Join_env.
(* Goal: @Cross_alg env Join_env *)
Proof.   rewrite Join_env_eq. apply Canc_fpm; auto with typeclass_instances.
Qed.

Instance Disj_env {PA: Perm_alg A}{DA: Disj_alg A}: @Disj_alg env Join_env.
(* Goal: @Cross_alg env Join_env *)
Proof.   rewrite Join_env_eq. apply Disj_fpm; auto with typeclass_instances.
Qed.

Instance Cross_env: Cross_alg env.
Proof.
(* Goal: @Cross_alg env Join_env *)
 rewrite Join_env_eq.
(* Goal: @Cross_alg env (@Join_fpm key (prod pshare A) (Join_prod pshare Join_pshare A JA)) *)
 unfold env.
(* Goal: @Cross_alg (fpm key (prod pshare A)) (@Join_fpm key (prod pshare A) (Join_prod pshare Join_pshare A JA)) *)
 pose (bij := @fpm_bij key _ _ (@lift_prod_bij share _ A)).
(* Goal: @Cross_alg (fpm key (prod pshare A)) (@Join_fpm key (prod pshare A) (Join_prod pshare Join_pshare A JA)) *)
 pose (J := @Join_fpm key _ (@Join_lift _ (Join_prod share _ _ JA))).
(* Goal: @Cross_alg (fpm key (prod pshare A)) (@Join_fpm key (prod pshare A) (Join_prod pshare Join_pshare A JA)) *)
 unfold pshare.
 replace
  (@Join_fpm key (@lifted Share.t Share.Join_ba * A)
     (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A
        JA))
  with (Join_bij
       (fpm key
          (@lifted (share * A)
             (Join_prod share Share.Join_ba A JA))) _
       (fpm key (@lifted share Share.Join_ba * A)) bij).
(* Goal: @Cross_alg (fpm key (prod (@lifted Share.t Share.Join_ba) A)) (Join_bij (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) J (fpm key (prod (@lifted share Share.Join_ba) A)) bij) *)
(* Goal: @eq (Join (fpm key (prod (@lifted share Share.Join_ba) A))) (Join_bij (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) J (fpm key (prod (@lifted share Share.Join_ba) A)) bij) (@Join_fpm key (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) *)
 apply (Cross_bij _ _ _ bij).
(* Goal: @Cross_alg (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A)))) J *)
(* Goal: @eq (Join (fpm key (prod (@lifted share Share.Join_ba) A))) (Join_bij (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) J (fpm key (prod (@lifted share Share.Join_ba) A)) bij) (@Join_fpm key (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) *)
 apply cross_split_fpm; auto with typeclass_instances.
(* Goal: forall x : prod share A, sumbool (@identity (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A)) x) (not (@identity (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A)) x)) *)
(* Goal: @eq (Join (fpm key (prod (@lifted share Share.Join_ba) A))) (Join_bij (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) J (fpm key (prod (@lifted share Share.Join_ba) A)) bij) (@Join_fpm key (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) *)
 intros [sh v]. destruct (dec_share_identity sh); [left | right].
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
 apply identity_unit_equiv in i. apply identity_unit_equiv. split; auto.
(* Goal: not (@identity (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A)) (@pair share A sh v)) *)
(* Goal: @eq (Join (fpm key (prod (@lifted share Share.Join_ba) A))) (Join_bij (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) J (fpm key (prod (@lifted share Share.Join_ba) A)) bij) (@Join_fpm key (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) *)
 contradict n.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
 apply identity_unit_equiv in n. apply identity_unit_equiv. destruct n; auto.
(* Goal: @eq (Join (fpm key (prod (@lifted share Share.Join_ba) A))) (Join_bij (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) J (fpm key (prod (@lifted share Share.Join_ba) A)) bij) (@Join_fpm key (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) *)
 extensionality x y z.
(* Goal: @eq Prop (Join_bij (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) J (fpm key (prod (@lifted share Share.Join_ba) A)) bij x y z) (@Join_fpm key (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA) x y z) *)
 unfold J, bij; clear J bij.
(* Goal: @eq Prop (Join_bij (fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) (@Join_fpm key (@lifted (prod share A) (Join_prod share Share.Join_ba A JA)) (@Join_lift (prod share A) (Join_prod share Share.Join_ba A JA))) (fpm key (prod (@lifted share Share.Join_ba) A)) (@fpm_bij key (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (prod (@lifted share Share.Join_ba) A) (@lift_prod_bij share Share.Join_ba A)) x y z) (@Join_fpm key (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA) x y z) *)
 apply forall_ext; intro i.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
 unfold finMap; simpl.
 change  (@proj1_sig (key -> option (@lifted Share.t Share.Join_ba * A))
     (fun f : key -> option (@lifted Share.t Share.Join_ba * A) =>
      exists l : list key,
        forall a : key,
        ~ @In key a l -> f a = @None (@lifted Share.t Share.Join_ba * A)))
  with (@proj1_sig (key -> option (@lifted share Share.Join_ba * A))
      (@finMap key (@lifted share Share.Join_ba * A))).
 set  (xi := proj1_sig x i); clearbody xi.
(* Goal: @eq Prop (@join (option (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) (@Join_lower (@lifted (prod share A) (Join_prod share Share.Join_ba A JA)) (@Join_lift (prod share A) (Join_prod share Share.Join_ba A JA))) match xi with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end match @proj1_sig (forall _ : key, option (prod (@lifted share Share.Join_ba) A)) (@finMap key (prod (@lifted share Share.Join_ba) A)) y i with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end match @proj1_sig (forall _ : key, option (prod (@lifted share Share.Join_ba) A)) (@finMap key (prod (@lifted share Share.Join_ba) A)) z i with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end) (@join (option (prod (@lifted Share.t Share.Join_ba) A)) (@Join_lower (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) xi (@proj1_sig (forall _ : key, option (prod (@lifted share Share.Join_ba) A)) (@finMap key (prod (@lifted share Share.Join_ba) A)) y i) (@proj1_sig (forall _ : key, option (prod (@lifted share Share.Join_ba) A)) (@finMap key (prod (@lifted share Share.Join_ba) A)) z i)) *)
 set (yi:= proj1_sig y i); clearbody yi.
(* Goal: @eq Prop (@join (option (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) (@Join_lower (@lifted (prod share A) (Join_prod share Share.Join_ba A JA)) (@Join_lift (prod share A) (Join_prod share Share.Join_ba A JA))) match xi with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end match yi with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end match @proj1_sig (forall _ : key, option (prod (@lifted share Share.Join_ba) A)) (@finMap key (prod (@lifted share Share.Join_ba) A)) z i with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end) (@join (option (prod (@lifted Share.t Share.Join_ba) A)) (@Join_lower (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) xi yi (@proj1_sig (forall _ : key, option (prod (@lifted share Share.Join_ba) A)) (@finMap key (prod (@lifted share Share.Join_ba) A)) z i)) *)
 set (zi:= proj1_sig z i); clearbody zi.
(* Goal: @eq Prop (@join (option (@lifted (prod share A) (Join_prod share Share.Join_ba A JA))) (@Join_lower (@lifted (prod share A) (Join_prod share Share.Join_ba A JA)) (@Join_lift (prod share A) (Join_prod share Share.Join_ba A JA))) match xi with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end match yi with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end match zi with | Some j => @Some (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) (@lift_prod2 share Share.Join_ba A j) | None => @None (@lifted (prod share A) (Join_prod share Share.Join_ba A (Join_equiv A))) end) (@join (option (prod (@lifted Share.t Share.Join_ba) A)) (@Join_lower (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) xi yi zi) *)
 clear.
 destruct xi; destruct yi; destruct zi;
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
 apply prop_ext; split; intro; inv H; try constructor.
(* Goal: @join (option (prod (@lifted Share.t Share.Join_ba) A)) (@Join_lower (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) (@None (prod (@lifted share Share.Join_ba) A)) (@Some (prod (@lifted share Share.Join_ba) A) p) (@Some (prod (@lifted share Share.Join_ba) A) p0) *)
 destruct p as [[x Hx] x']. destruct p0 as [[y Hy] y']. destruct p1 as [[z Hz] z'].
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  simpl in *. inv H3; simpl in *. split; auto.
(* Goal: @join (option (prod (@lifted Share.t Share.Join_ba) A)) (@Join_lower (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) (@None (prod (@lifted share Share.Join_ba) A)) (@Some (prod (@lifted share Share.Join_ba) A) p) (@Some (prod (@lifted share Share.Join_ba) A) p0) *)
 destruct p as [[x Hx] x']. destruct p0 as [[y Hy] y']. destruct p1 as [[z Hz] z'].
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  simpl in *. inv H3; simpl in *. split; auto.
(* Goal: @join (option (prod (@lifted Share.t Share.Join_ba) A)) (@Join_lower (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) (@None (prod (@lifted share Share.Join_ba) A)) (@Some (prod (@lifted share Share.Join_ba) A) p) (@Some (prod (@lifted share Share.Join_ba) A) p0) *)
 destruct p as [[x Hx] x']. destruct p0 as [[z Hz] z'].
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
 simpl in H1. inv H1. apply join_unit2; auto.
(* Goal: @eq (option (prod (@lifted Share.t Share.Join_ba) A)) (@Some (prod (@lifted share Share.Join_ba) A) (@pair (@lifted share Share.Join_ba) A (@exist share (@nonunit share Share.Join_ba) z Hx) z')) (@Some (prod (@lifted share Share.Join_ba) A) (@pair (@lifted share Share.Join_ba) A (@exist share (@nonunit share Share.Join_ba) z Hz) z')) *)
 repeat f_equal; apply proof_irr.
(* Goal: @join (option (prod (@lifted Share.t Share.Join_ba) A)) (@Join_lower (prod (@lifted Share.t Share.Join_ba) A) (Join_prod (@lifted Share.t Share.Join_ba) Join_pshare A JA)) (@None (prod (@lifted share Share.Join_ba) A)) (@Some (prod (@lifted share Share.Join_ba) A) p) (@Some (prod (@lifted share Share.Join_ba) A) p0) *)
 destruct p as [[x Hx] x']. destruct p0 as [[z Hz] z'].
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
 simpl in H0. inv H0. apply join_unit1; auto.
(* Goal: @eq (option (prod (@lifted Share.t Share.Join_ba) A)) (@Some (prod (@lifted share Share.Join_ba) A) (@pair (@lifted share Share.Join_ba) A (@exist share (@nonunit share Share.Join_ba) z Hx) z')) (@Some (prod (@lifted share Share.Join_ba) A) (@pair (@lifted share Share.Join_ba) A (@exist share (@nonunit share Share.Join_ba) z Hz) z')) *)
 repeat f_equal; apply proof_irr.
Qed.

Import VST.msl.predicates_sa.

Definition _env_mapsto {KE: EqDec key} (id: key) (sh: Share.t) (v: A) : pred env :=
    fun rho => exists p,
   forall id', env_get rho id' = if eq_dec id id' then Some (exist _ sh p,v) else None.

Lemma _env_mapsto_exists{KE: EqDec key}: forall id sh v, exists rho, _env_mapsto id (pshare_sh sh) v rho.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
assert (finite_idfun (fun id' => if eq_dec id id' then Some (sh, v) else None)).
(* Goal: finite_idfun (fun id' : key => if @eq_dec key KE id id' then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) *)
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
exists (id::nil).
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @eq (option (prod pshare A)) (if @eq_dec key KE id a then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (@None (prod pshare A)) *)
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
simpl in H.
(* Goal: @eq (option (prod pshare A)) (if @eq_dec key KE id a then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (@None (prod pshare A)) *)
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
intuition.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (eq_dec id a); try contradiction; auto.
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
exists (mk_env _ H).
(* Goal: forall (id1 id2 : key) (sh : Share.t) (v : A) (rho : env) (_ : not (@eq key id1 id2)) (_ : @_env_mapsto KE id1 sh v rho), @eq (option (prod pshare A)) (env_get rho id2) (@None (prod pshare A)) *)
unfold _env_mapsto.
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
destruct sh; simpl in *.
(* Goal: @ex (@nonunit Share.t Share.Join_ba x) (fun p : @nonunit Share.t Share.Join_ba x => forall id' : key, @eq (option (prod pshare A)) (if @eq_dec key KE id id' then @Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) x n) v) else @None (prod pshare A)) (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) x p) v) else @None (prod pshare A))) *)
exists n.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
auto.
Qed.

Lemma _env_get_mapsto {KE: EqDec key}:  forall (id: key) (v: A) (rho: env),
  (exists sh, env_get rho id = Some (sh,v)) =
  (exp (fun sh => _env_mapsto id sh v) * TT)%pred rho.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
apply prop_ext; split; intros.
(* Goal: @sepcon env Join_env (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v)) (@TT env) rho *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
destruct H as [sh ?].
(* Goal: @sepcon env Join_env (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v)) (@TT env) rho *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
destruct (_env_mapsto_exists id sh v) as [rho1 ?].
(* Goal: @sepcon env Join_env (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v)) (@TT env) rho *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
exists rho1.
(* Goal: @ex env (fun y : env => and (@join env Join_env rho1 y rho) (and (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1) (@TT env y))) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
assert (finite_idfun (fun id' => if eq_dec id id' then None else env_get rho id')).
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (if @in_dec key (@eq_dec key KE) a ids then @None (prod pshare A) else @env_get key A rho a) (@None (prod pshare A))) *)
destruct (env_finite rho) as [l ?].
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (if @in_dec key (@eq_dec key KE) a ids then @None (prod pshare A) else @env_get key A rho a) (@None (prod pshare A))) *)
exists l.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (eq_dec id a); auto.
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
exists (mk_env _ H1).
(* Goal: and (@join env Join_env (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) rho) (and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env))) *)
split.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @join env Join_env rho1 (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1) rho *)
(* Goal: and (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1) (@TT env (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1)) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
intro x.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
rewrite env_get_mk_env.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
destruct H0.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get rho1 x) (if @eq_dec key KE id x then @None (prod pshare A) else env_get rho x) (env_get rho x) *)
(* Goal: and (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1) (@TT env (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1)) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
rename x into id0.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get rho1 id0) (if @eq_dec key KE id id0 then @None (prod pshare A) else env_get rho id0) (env_get rho id0) *)
(* Goal: and (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1) (@TT env (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1)) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
specialize ( H0 id0).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get rho1 id0) (if @eq_dec key KE id id0 then @None (prod pshare A) else env_get rho id0) (env_get rho id0) *)
(* Goal: and (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1) (@TT env (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1)) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
destruct (eq_dec id id0).
(* Goal: @identity (env key A) (@Join_env key A) rho *)
subst.
(* Goal: @eq (option (prod pshare A)) (@env_get key A w1 id') (@env_get key A w2 id') *)
(* Goal: @eq (option (prod pshare A)) (@env_get key A w1 id') (@env_get key A w2 id') *)
rewrite H; rewrite H0.
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
destruct sh; simpl in *.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) x x0) v)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) x n) v)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get rho1 id0) (env_get rho id0) (env_get rho id0) *)
(* Goal: and (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1) (@TT env (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1)) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
rewrite (proof_irr x0 n); constructor.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get rho1 id0) (env_get rho id0) (env_get rho id0) *)
(* Goal: and (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1) (@TT env (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1)) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
rewrite H0.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
(* Goal: and (@join env Join_env (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) rho) (and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env))) *)
split.
(* Goal: @exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1 *)
(* Goal: @TT env (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
exists (pshare_sh sh).
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
auto.
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
destruct H as [?w [?w [? [[sh ?] _]]]].
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
destruct H0.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
specialize ( H0 id).
(* Goal: @eq A v1 v2 *)
destruct (eq_dec id id); try congruence.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
specialize ( H id).
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh sh) (pshare_sh sh'))) *)
rewrite H0 in H.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
inv H.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
econstructor; eauto.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
destruct a2; destruct a3; destruct H4 as [? [? ?]]; simpl in *; subst.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
econstructor; eauto.
Qed.

Lemma _env_get_mapsto'  {KE: EqDec key}: forall id (sh: pshare) v rho,
  env_get rho id = Some(pfullshare,v) -> (_env_mapsto id (pshare_sh sh) v * TT)%pred rho.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
destruct (top_correct' (pshare_sh sh)) as [sh2 ?].
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
assert (finite_idfun (fun i => if eq_dec i id then Some (sh,v) else None)).
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
exists (id::nil); intros. simpl in H1.
(* Goal: @eq (option (prod pshare A)) (if @eq_dec key KE id a then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (@None (prod pshare A)) *)
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
assert (id <> a) by intuition.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (eq_dec a id); auto. contradiction H2; auto.
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
destruct (dec_share_identity sh2).
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
assert (finite_idfun (fun i => if eq_dec i id then None else env_get rho i)).
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (if @in_dec key (@eq_dec key KE) a ids then @None (prod pshare A) else @env_get key A rho a) (@None (prod pshare A))) *)
destruct (env_finite rho) as [l ?].
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
exists l; intros. destruct (eq_dec a id); auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
exists (mk_env _ H1); exists (mk_env _ H2); split; [|split]; auto.
(* Goal: @join env Join_env (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba sh2 (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da sh2 n)) v) else env_get rho i) H2) rho *)
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
intro i'.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
do 2 rewrite env_get_mk_env.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (if @eq_dec key KE i' id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (if @eq_dec key KE i' id then @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba sh2 (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da sh2 n)) v) else env_get rho i') (env_get rho i') *)
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
destruct (eq_dec i' id).
(* Goal: @identity (env key A) (@Join_env key A) rho *)
subst. rewrite H.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@Some (prod pshare A) (@pair pshare A sh v)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A pfullshare v)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@None (prod pshare A)) (env_get rho i') (env_get rho i') *)
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
apply join_comm in H0.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@Some (prod pshare A) (@pair pshare A sh v)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A pfullshare v)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@None (prod pshare A)) (env_get rho i') (env_get rho i') *)
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
apply i in H0.
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
destruct sh; simpl in *.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
subst.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) Share.top n) v)) (@None (prod pshare A)) (@Some (prod pshare A) (@pair pshare A pfullshare v)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@None (prod pshare A)) (env_get rho i') (env_get rho i') *)
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
rewrite (proof_irr n top_share_nonunit).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
exists (proj2_sig sh).
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
rewrite env_get_mk_env.
(* Goal: @eq (option (prod pshare A)) (if @eq_dec key KE id' id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) v) else @None (prod pshare A)) *)
destruct (eq_dec id' id).
(* Goal: @eq A v1 v2 *)
subst. destruct (eq_dec id id); try congruence.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
f_equal. f_equal. destruct sh; simpl. auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (eq_dec id' id); try contradiction; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (eq_dec id id'); try contradiction; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
contradiction n; auto.
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
assert (finite_idfun (fun i => if eq_dec i id then Some(mk_lifted sh2 (nonidentity_nonunit n), v) else env_get rho i)).
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (if @in_dec key (@eq_dec key KE) a ids then @None (prod pshare A) else @env_get key A rho a) (@None (prod pshare A))) *)
destruct (env_finite rho) as [l ?].
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
exists l; intros. destruct (eq_dec a id); auto.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
subst.
(* Goal: @eq (option (prod pshare A)) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba sh2 (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da sh2 n)) v)) (@None (prod pshare A)) *)
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
specialize ( H2 id H3).
(* Goal: @eq (option (prod pshare A)) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba sh2 (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da sh2 n)) v)) (@None (prod pshare A)) *)
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh) v) (@TT env) rho *)
rewrite H in H2; inv H2.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
exists (mk_env _ H1); exists (mk_env _ H2); split; [|split]; auto.
(* Goal: @join env Join_env (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba sh2 (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da sh2 n)) v) else env_get rho i) H2) rho *)
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
intro i'.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
do 2 rewrite env_get_mk_env.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (if @eq_dec key KE i' id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (if @eq_dec key KE i' id then @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba sh2 (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da sh2 n)) v) else env_get rho i') (env_get rho i') *)
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
destruct (eq_dec i' id).
(* Goal: @identity (env key A) (@Join_env key A) rho *)
subst. rewrite H.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
constructor; simpl; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
constructor; simpl; auto.
(* Goal: @join A (@JA A) a a a *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
apply join_equiv_refl.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
(* Goal: @_env_mapsto KE id (pshare_sh sh) v (mk_env (fun i : key => if @eq_dec key KE i id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) H1) *)
exists (proj2_sig sh).
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
rewrite env_get_mk_env.
(* Goal: @eq (option (prod pshare A)) (if @eq_dec key KE id' id then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) v) else @None (prod pshare A)) *)
destruct (eq_dec id' id).
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
subst. destruct (eq_dec id id); try contradiction n0; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
f_equal. f_equal. destruct sh; simpl.  auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (eq_dec id id'); auto. contradiction n0; auto.
Qed.

Lemma _env_mapsto_set{KE: EqDec key}: forall id v,
  _env_mapsto id Share.top v (env_set id v empty_env).
Proof.
(* Goal: forall (id : key) (v : A), @_env_mapsto KE id Share.top v (@env_set KE id v empty_env) *)
  intros id v.
(* Goal: @_env_mapsto KE id Share.top v (@env_set KE id v empty_env) *)
  exists top_share_nonunit.
(* Goal: @join env Join_env (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) rho *)
(* Goal: and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env)) *)
  intros id'.
(* Goal: @eq (option (prod pshare A)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v)) empty_env) id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf)) Pf) v) else @None (prod pshare A)) *)
  destruct (eq_dec id id') as [Hid|].
(* Goal: @eq (option (prod pshare A)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v)) empty_env) id') (@Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf)) Pf) v)) *)
(* Goal: @eq (option (prod pshare A)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v)) empty_env) id') (@None (prod pshare A)) *)
    rewrite <- Hid.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
    rewrite env_gss; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
    rewrite env_gso; auto.
Qed.

Lemma _env_mapsto_set_sh{KE: EqDec key}: forall id (sh: pshare) v,
  _env_mapsto id (pshare_sh sh) v (env_set_sh id (Some (sh,v)) empty_env).
Proof.
(* Goal: forall (id : key) (sh : pshare) (v : A), @_env_mapsto KE id (pshare_sh sh) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh v)) empty_env) *)
  intros id [sh Pf] v.
(* Goal: @_env_mapsto KE id (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf)) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v)) empty_env) *)
  exists Pf.
(* Goal: @join env Join_env (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) rho *)
(* Goal: and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env)) *)
  intros id'.
(* Goal: @eq (option (prod pshare A)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v)) empty_env) id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf)) Pf) v) else @None (prod pshare A)) *)
  destruct (eq_dec id id') as [Hid|].
(* Goal: @eq (option (prod pshare A)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v)) empty_env) id') (@Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf)) Pf) v)) *)
(* Goal: @eq (option (prod pshare A)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v)) empty_env) id') (@None (prod pshare A)) *)
    rewrite <- Hid.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
    rewrite env_gss_sh; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
    rewrite env_gso_sh; auto.
Qed.

Lemma _env_mapsto_get{KE: EqDec key}: forall id sh v rho,
  _env_mapsto id sh v rho
   -> exists Pf: nonunit sh,
        env_get rho id = Some (exist nonunit sh Pf, v).
Proof.
(* Goal: forall (id : key) (sh : Share.t) (v : A) (rho : env) (_ : @_env_mapsto KE id sh v rho), @ex (@nonunit Share.t Share.Join_ba sh) (fun Pf : @nonunit Share.t Share.Join_ba sh => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v))) *)
  unfold _env_mapsto, env_get.
(* Goal: forall (id : key) (sh : Share.t) (v : A) (rho : env) (_ : @ex (@nonunit Share.t Share.Join_ba sh) (fun p : @nonunit Share.t Share.Join_ba sh => forall id' : key, @eq (option (prod pshare A)) (@lookup_fpm key (prod pshare A) rho id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh p) v) else @None (prod pshare A)))), @ex (@nonunit Share.t Share.Join_ba sh) (fun Pf : @nonunit Share.t Share.Join_ba sh => @eq (option (prod pshare A)) (@lookup_fpm key (prod pshare A) rho id) (@Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v))) *)
  intros id sh v rho [p H1].
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
  specialize ( H1 id); simpl in *.
(* Goal: @ex (@nonunit Share.t Share.Join_ba sh) (fun Pf : @nonunit Share.t Share.Join_ba sh => @eq (option (prod pshare A)) (@lookup_fpm key (prod pshare A) rho id) (@Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh Pf) v))) *)
  destruct (eq_dec id id); firstorder.
Qed.

Lemma _env_mapsto_empty_env {KE: EqDec key} : forall id v sh,
  ~(_env_mapsto id sh v empty_env).
Proof.
(* Goal: forall (id : key) (v : A) (sh : Share.t), not (@_env_mapsto KE id sh v empty_env) *)
  unfold not, _env_mapsto.
(* Goal: forall (id : key) (v : A) (sh : Share.t) (_ : @ex (@nonunit Share.t Share.Join_ba sh) (fun p : @nonunit Share.t Share.Join_ba sh => forall id' : key, @eq (option (prod pshare A)) (env_get empty_env id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh p) v) else @None (prod pshare A)))), False *)
  intros ? ? ? [p H].
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
  specialize ( H id).
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  destruct (eq_dec id id); auto.
(* Goal: False *)
  inversion H.
Qed.

Lemma _env_mapsto_get_neq {KE: EqDec key} : forall (id1 id2: key) (sh: Share.t) (v: A) rho,
  id1 <> id2 -> _env_mapsto id1 sh v rho -> env_get rho id2 = None.
Proof.
(* Goal: forall (id1 id2 : key) (sh : Share.t) (v : A) (rho : env) (_ : not (@eq key id1 id2)) (_ : @_env_mapsto KE id1 sh v rho), @eq (option (prod pshare A)) (env_get rho id2) (@None (prod pshare A)) *)
  unfold _env_mapsto.
(* Goal: forall (id1 id2 : key) (sh : Share.t) (v : A) (rho : env) (_ : not (@eq key id1 id2)) (_ : @ex (@nonunit Share.t Share.Join_ba sh) (fun p : @nonunit Share.t Share.Join_ba sh => forall id' : key, @eq (option (prod pshare A)) (env_get rho id') (if @eq_dec key KE id1 id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh p) v) else @None (prod pshare A)))), @eq (option (prod pshare A)) (env_get rho id2) (@None (prod pshare A)) *)
  intros id1 id2 sh v rho Hneq [p H1].
(* Goal: @eq (option (prod pshare A)) (env_get rho id2) (@None (prod pshare A)) *)
  specialize ( H1 id2).
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  destruct (eq_dec id1 id2); try contradiction ;auto.
Qed.

Lemma _env_mapsto_splittable1 {KE: EqDec key}: forall id v (sh sh1 sh2: pshare) rho,
  join (proj1_sig sh1) (proj1_sig sh2) (proj1_sig sh)
  -> (_env_mapsto id  (pshare_sh sh1) v * _env_mapsto id (pshare_sh sh2) v)%pred rho
  -> _env_mapsto id (pshare_sh sh) v rho.
Proof.
(* Goal: forall (id : key) (v : A) (sh sh1 sh2 : pshare) (rho : env) (_ : @join Share.t Share.Join_ba (@proj1_sig Share.t (@nonunit Share.t Share.Join_ba) sh1) (@proj1_sig Share.t (@nonunit Share.t Share.Join_ba) sh2) (@proj1_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) (_ : @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh1) v) (@_env_mapsto KE id (pshare_sh sh2) v) rho), @_env_mapsto KE id (pshare_sh sh) v rho *)
  intros id v sh sh1 sh2 rho H1 H2.
(* Goal: @_env_mapsto KE id (pshare_sh sh) v rho *)
  destruct H2 as [rho1 [rho2 [Hrho_join [[Pf1 H_env_mapsto1] [Pf2 H_env_mapsto2]]]]].
(* Goal: @_env_mapsto KE id (pshare_sh sh) v rho *)
  exists (proj2_sig sh); intro id'.
(* Goal: @eq (option (prod pshare A)) (env_get rho id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) v) else @None (prod pshare A)) *)
  specialize ( H_env_mapsto1 id'); specialize ( H_env_mapsto2 id').
(* Goal: @eq (option (prod pshare A)) (env_get rho id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) v) else @None (prod pshare A)) *)
  generalize Hrho_join; clear Hrho_join; unfold join; simpl; intros Hrho_join.
(* Goal: @eq (option (prod pshare A)) (env_get rho id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) v) else @None (prod pshare A)) *)
  specialize ( Hrho_join id').
(* Goal: @eq (option (prod pshare A)) (env_get rho id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) v) else @None (prod pshare A)) *)
  rewrite H_env_mapsto1 in Hrho_join; rewrite H_env_mapsto2 in Hrho_join.
(* Goal: @eq (option (prod pshare A)) (env_get rho id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) v) else @None (prod pshare A)) *)
  destruct (eq_dec id id').

  (* id = id' *)
(* Goal: @identity (env key A) (@Join_env key A) rho *)
  inversion Hrho_join; simpl in *; subst.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
  destruct a3; destruct H3 as [? [? ?]]; simpl in *; subst.
(* Goal: @eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A p a)) (@Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) a)) *)
(* Goal: @eq (option (prod pshare A)) (env_get rho id') (@None (prod pshare A)) *)
  apply (f_equal (fun x => Some(x, a))).
(* Goal: @eq pshare p (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) (@proj2_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) *)
(* Goal: @eq (option (prod pshare A)) (env_get rho id') (@None (prod pshare A)) *)
  apply lifted_eq.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  eapply join_eq; eauto.

  (* id <> id' *)
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  inversion Hrho_join; auto.
Qed.

Lemma _env_mapsto_splittable2{KE: EqDec key}: forall id v (sh sh1 sh2: pshare) rho,
  join (proj1_sig sh1) (proj1_sig sh2) (proj1_sig sh)
  -> _env_mapsto id (pshare_sh sh) v rho
  -> (_env_mapsto id (pshare_sh sh1) v * _env_mapsto id (pshare_sh sh2) v)%pred rho.
Proof.
(* Goal: forall (id : key) (v : A) (sh sh1 sh2 : pshare) (rho : env) (_ : @join Share.t Share.Join_ba (@proj1_sig Share.t (@nonunit Share.t Share.Join_ba) sh1) (@proj1_sig Share.t (@nonunit Share.t Share.Join_ba) sh2) (@proj1_sig Share.t (@nonunit Share.t Share.Join_ba) sh)) (_ : @_env_mapsto KE id (pshare_sh sh) v rho), @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh1) v) (@_env_mapsto KE id (pshare_sh sh2) v) rho *)
  intros id v sh sh1 sh2 rho Hjoin H.
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh1) v) (@_env_mapsto KE id (pshare_sh sh2) v) rho *)
  destruct H as [? H0].
(* Goal: @sepcon env Join_env (@_env_mapsto KE id (pshare_sh sh1) v) (@_env_mapsto KE id (pshare_sh sh2) v) rho *)
  exists (env_set_sh id (Some (sh1,v)) empty_env); exists (env_set_sh id (Some(sh2,v)) empty_env).
(* Goal: and (@join env Join_env (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) rho) (and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env))) *)
  split.

(* Goal: @join env Join_env (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) rho *)
(* Goal: and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env)) *)
  intros id'.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get rho1 id0) (env_get rho id0) (env_get rho id0) *)
(* Goal: and (@exp env Share.t (fun sh : Share.t => @_env_mapsto KE id sh v) rho1) (@TT env (mk_env (fun id' : key => if @eq_dec key KE id id' then @None (prod pshare A) else env_get rho id') H1)) *)
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
  specialize ( H0 id'); rewrite H0.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) id') (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) id') (if @eq_dec key KE id id' then @Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) x) v) else @None (prod pshare A)) *)
(* Goal: and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env)) *)
  destruct (eq_dec id id') as [Hid_id'_eq | Hid_id'_neq].

  (* id = id' *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) id') (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) id') (@Some (prod (@sig Share.t (@nonunit Share.t Share.Join_ba)) A) (@pair (@sig Share.t (@nonunit Share.t Share.Join_ba)) A (@exist Share.t (@nonunit Share.t Share.Join_ba) (pshare_sh sh) x) v)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) id') (env_get (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) id') (@None (prod pshare A)) *)
(* Goal: and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env)) *)
  subst id'.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
  do 2 rewrite env_gss_sh. constructor.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  constructor; auto.
(* Goal: @join A (@JA A) a a a *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
  apply join_equiv_refl.

  (* id <> id' *)
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  rewrite (env_gso_sh); auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  rewrite (env_gso_sh); auto.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
  rewrite env_get_empty. constructor.

(* Goal: and (@join env Join_env (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env) (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env) rho) (and (@_env_mapsto KE id (pshare_sh sh1) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh1 v)) empty_env)) (@_env_mapsto KE id (pshare_sh sh2) v (@env_set_sh KE id (@Some (prod pshare A) (@pair pshare A sh2 v)) empty_env))) *)
  destruct sh1 as [sh1 n1]; destruct sh2 as [sh2 n2];  unfold _env_mapsto; split.
(* Goal: forall a : env key A, @eq (env key A) (@core (env key A) Join_env (@Sep_env SA) a) empty_env *)
  exists n1; reflexivity.
(* Goal: forall a : env key A, @eq (env key A) (@core (env key A) Join_env (@Sep_env SA) a) empty_env *)
  exists n2; reflexivity.
Qed.

Lemma _env_mapsto_splittable {KE: EqDec key}: forall id v (sh sh1 sh2: pshare) rho,
  join (proj1_sig sh1) (proj1_sig sh2) (proj1_sig sh)
  -> (_env_mapsto id (pshare_sh sh) v rho
        <-> (_env_mapsto id (pshare_sh sh1) v * _env_mapsto id (pshare_sh sh2)  v)%pred rho).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
  intros.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
  split; intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  eapply _env_mapsto_splittable2; eauto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  eapply _env_mapsto_splittable1; eauto.
Qed.

End ENVSEC.
End Env.
Export Env.

Module EnvSA.

Existing Instance Join_env.
Existing Instance Perm_env.
Existing Instance Sep_env.
Existing Instance Sing_env.
Existing Instance Canc_env.
Existing Instance Disj_env.
Existing Instance Cross_env.

Lemma empty_env_unit {key: Type}{A: Type}:
    forall rho: env key A, unit_for empty_env rho.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intro; intros.
(* Goal: @unit_for (env key A) (@Join_env key A) (@empty_env key A) rho *)
unfold unit_for.
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
intro.
(* Goal: @eq (option (prod pshare A)) (@None (prod pshare A)) (@env_get key A (@empty_env key A) id) *)
rewrite env_get_empty.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
Qed.

Lemma empty_env_unit' {key: Type}{A: Type}: forall rho: env key A, join empty_env rho rho.
Proof.
(* Goal: forall rho : env key A, @join (env key A) (@Join_env key A) (@empty_env key A) rho rho *)
intros; apply empty_env_unit.
Qed.
Hint Resolve @empty_env_unit @empty_env_unit'.

Lemma env_join_sub1 {key: Type}{A: Type}:
  forall rho1 rho2: env key A, (forall id x, env_get rho1 id = Some x -> env_get rho2 id = Some x) ->
     join_sub rho1 rho2.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
pose (JA := Join_equiv A).
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
assert (forall i: key, cjoin_sub (env_get rho1 i) (env_get rho2 i)).

(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
intro.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
case_eq (env_get rho1 i); intros.
(* Goal: @cjoin_sub (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@Some (prod pshare A) p) (@env_get key A rho2 i) *)
(* Goal: @cjoin_sub (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@None (prod pshare A)) (@env_get key A rho2 i) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
specialize (H _ _ H0).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
exists None. rewrite H. constructor.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
econstructor; constructor.
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
assert (finite_idfun (fun i => proj1_sig (X i))).
(* Goal: @finite_idfun key A (fun i : key => @proj1_sig (option (prod pshare A)) (fun b : option (prod pshare A) => @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@env_get key A rho1 i) b (@env_get key A rho2 i)) (X i)) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
destruct (env_finite rho2) as [l ?].
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
exists l; intros.
(* Goal: @eq (option (prod pshare A)) (@proj1_sig (option (prod pshare A)) (fun b : option (prod pshare A) => @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@env_get key A rho1 a) b (@env_get key A rho2 a)) (X a)) (@None (prod pshare A)) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
specialize (H0 _ H1).
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
generalize (X a); intro.
(* Goal: @eq (option (prod pshare A)) (@proj1_sig (option (prod pshare A)) (fun b : option (prod pshare A) => @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@env_get key A rho1 a) b (@env_get key A rho2 a)) c) (@None (prod pshare A)) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
destruct c.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
rewrite H0 in j; inv j; auto.
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
exists (mk_env _ H0).
(* Goal: @join (env key A) (@Join_env key A) rho1 (@mk_env key A (fun i : key => @proj1_sig (option (prod pshare A)) (fun b : option (prod pshare A) => @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@env_get key A rho1 i) b (@env_get key A rho2 i)) (X i)) H0) rho2 *)
intro i.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
rewrite env_get_mk_env.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@Env.JA A))) (@env_get key A rho1 i) (@proj1_sig (option (prod pshare A)) (fun b : option (prod pshare A) => @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A JA)) (@env_get key A rho1 i) b (@env_get key A rho2 i)) (X i)) (@env_get key A rho2 i) *)
destruct (X i).
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
auto.
Qed.

Lemma env_get_join_sub {key: Type}{A: Type}: forall (rho rho': env key A) id sh v,
   join_sub rho rho' -> env_get rho id = Some (sh,v) ->
     exists sh', env_get rho' id = Some (sh', v) /\ join_sub (pshare_sh sh)  (pshare_sh sh').
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh sh) (pshare_sh sh'))) *)
destruct H.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
specialize ( H id).
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh sh) (pshare_sh sh'))) *)
rewrite H0 in H.
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh sh) (pshare_sh sh'))) *)
clear H0 rho.
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh sh) (pshare_sh sh'))) *)
destruct sh as [sh n].
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'))) *)
destruct (env_get rho' id) as [[[sh' n'] v'] |]; [|inv H].
revert H;
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
destruct (env_get x id) as [[[shx nx] vx] | ]; intro H; inv H.
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
simpl in *.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
destruct H3 as [? [? ?]]; simpl in *; subst.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
econstructor; split; eauto. econstructor; eauto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
econstructor; split; eauto.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl. apply join_sub_refl.
Qed.

Lemma env_at_joins {key: Type}{A: Type}{KE: EqDec key}:
  forall rho1 rho2: env key A,
         (forall id, @joins _ (@Join_lower (pshare * A) (Join_prod pshare Join_pshare A (Join_equiv _))) (env_get rho1 id) (env_get rho2 id)) ->
               joins rho1 rho2.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
unfold joins in H.
pose (share_of rho id := match @env_get key A rho id with
                                       | None => Share.bot
                                       | Some (p,v) => pshare_sh p
                                       end).
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
assert (forall id, joins (share_of rho1 id) (share_of rho2 id)).
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @joins share Share.Join_ba (share_of rho1 id) (share_of rho2 id) *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
destruct (H id) as [x H0].
(* Goal: @joins share Share.Join_ba (share_of rho1 id) (share_of rho2 id) *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
clear - H0.
(* Goal: @join_sub share Share.Join_ba (share_of rho1 id) (share_of rho2 id) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
unfold share_of.
(* Goal: @joins share Share.Join_ba match @env_get key A rho1 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end match @env_get key A rho2 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
inv H0.
(* Goal: @joins share Share.Join_ba Share.bot match @env_get key A rho1 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end *)
(* Goal: @joins share Share.Join_ba (let (p, _) := a1 in pshare_sh p) (let (p, _) := a2 in pshare_sh p) *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
apply bot_joins.
(* Goal: @joins share Share.Join_ba match @env_get key A rho1 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end Share.bot *)
(* Goal: @joins share Share.Join_ba (let (p, _) := a1 in pshare_sh p) (let (p, _) := a2 in pshare_sh p) *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
rewrite joins_sym.
(* Goal: @joins share Share.Join_ba Share.bot match @env_get key A rho1 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end *)
(* Goal: @joins share Share.Join_ba (let (p, _) := a1 in pshare_sh p) (let (p, _) := a2 in pshare_sh p) *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
apply bot_joins.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct a1; destruct a2; destruct a3; destruct H2 as [? [? ?]]; simpl in *. subst. eauto.
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
pose (h id := proj1_sig (share_joins_constructive _ _ (H0 id))).
pose (g sh (v: A) := match dec_share_identity sh with
                         | left _ => None
                         | right p => Some (mk_lifted _ (nonidentity_nonunit p), v)
                         end).
pose (f id := match env_get rho1 id, env_get rho2 id with
                     | None, shv => shv
                     | shv, None => shv
                     | Some (_,v), _ => g (h id) v
                      end).
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
assert (finite_idfun f).
(* Goal: @finite_idfun key A f *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
destruct (env_finite rho1) as [l1 ?].
(* Goal: @finite_idfun key A f *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
destruct (env_finite rho2) as [l2 ?].
(* Goal: @finite_idfun A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
exists (l1++l2).
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @eq (option (prod pshare A)) (f a) (@None (prod pshare A)) *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
rewrite in_app in H3.
(* Goal: @eq (option (prod pshare A)) (f a) (@None (prod pshare A)) *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
destruct (In_dec eq_dec a l1) as [H3' | H3'].
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
contradiction H3; auto.
(* Goal: @eq (option (prod pshare A)) (if @eq_dec key KE id a then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (@None (prod pshare A)) *)
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
assert (H4: ~In a l2) by intuition.
(* Goal: @eq (option (prod pshare A)) (f a) (@None (prod pshare A)) *)
(* Goal: @joins (env key A) (@Join_env key A) rho1 rho2 *)
specialize ( H1 a H3'). specialize ( H2 a H4).
(* Goal: @eq (option (prod pshare A)) (f a) (@None (prod pshare A)) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
unfold f.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
rewrite H1; rewrite H2; auto.
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
exists (mk_env _ H1).
(* Goal: @join (env A B) (@Join_env A B) ab c (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) *)
intro id.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
rewrite env_get_mk_env.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) (f id) (@env_get key A rho2 id) *)
unfold f; clear H1 f.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => g (h id) v | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
unfold g, h; clear g h.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) (@env_get key A rho2 id) match @env_get key A rho1 id with | Some (pair p0 v as p) => match @env_get key A rho2 id with | Some p1 => match dec_share_identity (@proj1_sig Share.t (fun sh3 : Share.t => @join Share.t Share.Join_ba (share_of rho1 id) (share_of rho2 id) sh3) (share_joins_constructive (share_of rho1 id) (share_of rho2 id) (H0 id))) with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p2 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba (@proj1_sig Share.t (fun sh3 : Share.t => @join Share.t Share.Join_ba (share_of rho1 id) (share_of rho2 id) sh3) (share_joins_constructive (share_of rho1 id) (share_of rho2 id) (H0 id))) (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da (@proj1_sig Share.t (fun sh3 : Share.t => @join Share.t Share.Join_ba (share_of rho1 id) (share_of rho2 id) sh3) (share_joins_constructive (share_of rho1 id) (share_of rho2 id) (H0 id))) p2)) v) end | None => @Some (prod pshare A) (@pair pshare A p0 v) end | None => @env_get key A rho2 id end *)
destruct (share_joins_constructive (share_of rho1 id) (share_of rho2 id) (H0 id)).
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
specialize ( H id). destruct H as [c ?].
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
unfold share_of in *; clear share_of.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
specialize ( H0 id).
destruct (env_get rho1 id) as [[sh1 v1]|];
destruct (env_get rho2 id) as [[sh2 v2]|];
try solve [constructor].
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
inv H.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
destruct a3; destruct H3 as [? [? ?]].  simpl in H,H1,H2; subst.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh2 v2)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
destruct (dec_share_identity x).
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
generalize (split_identity _ _ j i); intro.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 a)) (@Some (prod pshare A) (@pair pshare A sh2 a)) (@None (prod (@lifted Share.t Share.Join_ba) A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 a)) (@Some (prod pshare A) (@pair pshare A sh2 a)) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x n)) a)) *)
elimtype False; clear - H1.
(* Goal: False *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 a)) (@Some (prod pshare A) (@pair pshare A sh2 a)) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x n)) a)) *)
revert H1; apply nonunit_nonidentity.
(* Goal: @nonunit share Share.Join_ba (pshare_sh sh2) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba (pshare_sh sh2) (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da (pshare_sh sh2) n)) v2)) (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
apply pshare_nonunit.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
constructor; auto. constructor; auto. simpl. apply join_equiv_refl.
Qed.

Lemma env_at_join_sub {key: Type}{A: Type}{KE: EqDec key}:
  forall rho1 rho2, (forall id: key, @join_sub _ (@Join_lower (pshare * A) (Join_prod pshare Join_pshare A (Join_equiv _))) (env_get rho1 id) (env_get rho2 id)) -> join_sub rho1 rho2.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
unfold join_sub in H.
pose (share_of rho id := match @env_get key A rho id with
                                       | None => Share.bot
                                       | Some (p,v) => pshare_sh p
                                       end).
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
assert (forall id, join_sub (share_of rho1 id) (share_of rho2 id)).
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh sh) (pshare_sh sh'))) *)
specialize (H id); destruct H.
(* Goal: @join_sub share Share.Join_ba (share_of rho1 id) (share_of rho2 id) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
unfold share_of.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
inv H.
(* Goal: @join_sub share Share.Join_ba Share.bot match @env_get key A rho2 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end *)
(* Goal: @join_sub share Share.Join_ba match @env_get key A rho1 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end match @env_get key A rho1 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end *)
(* Goal: @join_sub share Share.Join_ba (let (p, _) := a1 in pshare_sh p) (let (p, _) := a3 in pshare_sh p) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
apply bot_correct'.
(* Goal: @join_sub share Share.Join_ba match @env_get key A rho1 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end match @env_get key A rho1 id with | Some (pair p v as p0) => pshare_sh p | None => Share.bot end *)
(* Goal: @join_sub share Share.Join_ba (let (p, _) := a1 in pshare_sh p) (let (p, _) := a3 in pshare_sh p) *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
apply join_sub_refl.
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
destruct a1; destruct a2; destruct a3; destruct H3 as [? [? ?]]; simpl in *. subst.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
econstructor; eauto.
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
pose (h id := proj1_sig (share_join_sub_constructive _ _ (H0 id))).
pose (g sh (v: A) := match dec_share_identity sh with
                         | left _ => None
                         | right p => Some (mk_lifted _ (nonidentity_nonunit p), v)
                         end).
pose (f id := match env_get rho2 id with
                     | None => None
                     | Some (_,v) => g (h id) v
                      end).
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
assert (finite_idfun f).
(* Goal: @finite_idfun key A f *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
destruct (env_finite rho2) as [l2 ?].
(* Goal: @finite_idfun key A f *)
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
exists l2.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
unfold f. rewrite H1; auto.
(* Goal: @join_sub (env key A) (@Join_env key A) rho1 rho2 *)
exists (mk_env _ H1).
(* Goal: @join (env A B) (@Join_env A B) ab c (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) *)
intro id.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
rewrite env_get_mk_env.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) (f id) (@env_get key A rho2 id) *)
unfold f; clear H1 f.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => g (h id) v | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
unfold g, h; clear g h.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity (@proj1_sig Share.t (fun sh2 : Share.t => @join Share.t Share.Join_ba (share_of rho1 id) sh2 (share_of rho2 id)) (share_join_sub_constructive (share_of rho1 id) (share_of rho2 id) (H0 id))) with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba (@proj1_sig Share.t (fun sh2 : Share.t => @join Share.t Share.Join_ba (share_of rho1 id) sh2 (share_of rho2 id)) (share_join_sub_constructive (share_of rho1 id) (share_of rho2 id) (H0 id))) (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da (@proj1_sig Share.t (fun sh2 : Share.t => @join Share.t Share.Join_ba (share_of rho1 id) sh2 (share_of rho2 id)) (share_join_sub_constructive (share_of rho1 id) (share_of rho2 id) (H0 id))) p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
destruct (share_join_sub_constructive (share_of rho1 id) (share_of rho2 id) (H0 id)).
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
specialize ( H id). destruct H as [c ?].
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
unfold share_of in *; clear share_of.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A rho1 id) match @env_get key A rho2 id with | Some (pair p0 v as p) => match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p1 => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p1)) v) end | None => @None (prod (@lifted Share.t Share.Join_ba) A) end (@env_get key A rho2 id) *)
specialize ( H0 id).
destruct (env_get rho1 id) as [[sh1 v1]|];
destruct (env_get rho2 id) as [[sh2 v2]|].
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
inv H.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh2 v2)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
destruct (dec_share_identity x).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh2 v2)) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x n)) v2)) (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
contradiction n.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
apply unit_identity with (pshare_sh sh2); apply join_comm; auto.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
destruct H4 as [? [? ?]]; simpl snd in *; subst.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
generalize (join_canc (join_comm j) (join_comm H)); intro; subst.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 (@snd pshare A a2))) match dec_share_identity (@lifted_obj Share.t Share.Join_ba (@fst pshare A a2)) with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba (@lifted_obj Share.t Share.Join_ba (@fst pshare A a2)) (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da (@lifted_obj Share.t Share.Join_ba (@fst pshare A a2)) p)) (@snd pshare A a2)) end (@Some (prod pshare A) (@pair pshare A sh2 (@snd pshare A a2))) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
destruct (dec_share_identity (lifted_obj (fst a2))).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 (@snd pshare A a2))) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@Some (prod pshare A) (@pair pshare A sh2 (@snd pshare A a2))) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 (@snd pshare A a2))) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba (@lifted_obj Share.t Share.Join_ba (@fst pshare A a2)) (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da (@lifted_obj Share.t Share.Join_ba (@fst pshare A a2)) n)) (@snd pshare A a2))) (@Some (prod pshare A) (@pair pshare A sh2 (@snd pshare A a2))) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
contradiction (@nonunit_nonidentity _ _ _ _ (lifted_obj (fst a2))).
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (fst a2); simpl; auto.
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh n)) (pshare_sh sh'0))) *)
(* Goal: @ex pshare (fun sh'0 : pshare => and (@eq (option (prod pshare A)) (@Some (prod pshare A) (@pair pshare A (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n') v')) (@Some (prod pshare A) (@pair pshare A sh'0 v'))) (@join_sub share Share.Join_ba (pshare_sh (@exist Share.t (@nonunit Share.t Share.Join_ba) sh' n)) (pshare_sh sh'0))) *)
destruct a2; simpl in *. destruct p; simpl in *.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
constructor; simpl; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
constructor; auto.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl. apply join_equiv_refl.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@Some (prod pshare A) (@pair pshare A sh1 v1)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
inv H.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity x with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba x (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da x p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
apply bot_identity in j.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
subst.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) match dec_share_identity (pshare_sh sh2) with | left i => @None (prod (@lifted Share.t Share.Join_ba) A) | right p => @Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba (pshare_sh sh2) (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da (pshare_sh sh2) p)) v2) end (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
destruct (dec_share_identity (pshare_sh sh2)).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba (pshare_sh sh2) (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da (pshare_sh sh2) n)) v2)) (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
contradiction (@nonunit_nonidentity _ _ _ _ (pshare_sh sh2)).
(* Goal: @nonunit share Share.Join_ba (pshare_sh sh2) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@Some (prod (@lifted Share.t Share.Join_ba) A) (@pair (@lifted Share.t Share.Join_ba) A (@mk_lifted Share.t Share.Join_ba (pshare_sh sh2) (@nonidentity_nonunit Share.t Share.Join_ba pa_share sa_share Share.da (pshare_sh sh2) n)) v2)) (@Some (prod pshare A) (@pair pshare A sh2 v2)) *)
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod (@lifted Share.t Share.Join_ba) A)) (@None (prod pshare A)) *)
apply pshare_nonunit.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
apply join_unit1; auto.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
f_equal. f_equal. unfold mk_lifted; destruct sh2; simpl. f_equal. apply proof_irr.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
Qed.


Lemma identity_empty_env {key: Type}{A: Type}{KE: EqDec key}:  forall rho: env key A, identity rho <-> rho = empty_env.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
split; intros.
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
generalize (identity_unit (a:=empty_env)H); intro.
(* Goal: @eq (env key A) rho (@empty_env key A) *)
(* Goal: @identity (env key A) (@Join_env key A) rho *)
spec H0.
(* Goal: @joins (env key A) (@Join_env key A) rho (@empty_env key A) *)
(* Goal: @eq (env key A) rho (@empty_env key A) *)
(* Goal: @identity (env key A) (@Join_env key A) rho *)
exists rho; apply join_comm; apply empty_env_unit.
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
generalize (empty_env_unit rho); intro.
(* Goal: @eq (env key A) rho (@empty_env key A) *)
(* Goal: @identity (env key A) (@Join_env key A) rho *)
unfold unit_for in *.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
generalize (join_eq H0 (join_comm H1)); intro; auto.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
subst.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
apply unit_identity with empty_env; auto.
Qed.

End EnvSA.

Module EnvSL.
Import EnvSA.
Import VST.msl.predicates_sa.

Definition env_mapsto: forall {key A}{KE: EqDec key} (id: key) (sh: Share.t) (v: A) , pred (env key A) := @_env_mapsto.
Arguments env_mapsto [key] [A] [KE] _ _ _ _.

Lemma env_mapsto_exists{key A}{KE: EqDec key}: forall id sh (v: A), exists rho, _env_mapsto id (pshare_sh sh) v rho.
Proof. apply _env_mapsto_exists. Qed.

Lemma env_get_mapsto {key A}{KE: EqDec key}:  forall (id: key) (v: A) (rho: env _ _),
  (exists sh, env_get rho id = Some (sh,v)) =
  (exp (fun sh => _env_mapsto id sh v) * TT)%pred rho.
Proof. apply _env_get_mapsto. Qed.

Lemma env_get_mapsto'  {key A}{KE: EqDec key}: forall id (sh: pshare) (v: A) rho,
  env_get rho id = Some(pfullshare,v) -> (_env_mapsto id (pshare_sh sh) v * TT)%pred rho.
Proof. apply _env_get_mapsto'. Qed.

Lemma env_mapsto_set {key A}{KE: EqDec key}: forall id (v: A),
    env_mapsto id Share.top v (env_set id v empty_env).
Proof. apply _env_mapsto_set. Qed.

Lemma env_mapsto_set_sh{key A}{KE: EqDec key}: forall id (sh: pshare) (v: A),
  _env_mapsto id (pshare_sh sh) v (env_set_sh id (Some (sh,v)) empty_env).
Proof. apply _env_mapsto_set_sh. Qed.

Lemma env_mapsto_get{key A}{KE: EqDec key}: forall id sh (v:A) rho,
  env_mapsto id sh v rho
   -> exists Pf: nonunit sh,
        env_get rho id = Some (exist nonunit sh Pf, v).
Proof. apply _env_mapsto_get. Qed.

Lemma env_mapsto_empty_env {key A}{KE: EqDec key} : forall id (v:A) sh,
  ~(env_mapsto id sh v empty_env).
  Proof. apply _env_mapsto_empty_env. Qed.

Lemma env_mapsto_get_neq {key A}{KE: EqDec key} : forall (id1 id2: key) (sh: Share.t) (v: A) rho,
  id1 <> id2 -> env_mapsto id1 sh v rho -> env_get rho id2 = None.
Proof. apply _env_mapsto_get_neq. Qed.

Lemma env_mapsto_splittable {key A}{KE: EqDec key}: forall id (v:A) (sh sh1 sh2: pshare) rho,
  join (proj1_sig sh1) (proj1_sig sh2) (proj1_sig sh)
  -> (_env_mapsto id (pshare_sh sh) v rho
        <-> (_env_mapsto id (pshare_sh sh1) v * _env_mapsto id (pshare_sh sh2)  v)%pred rho).
Proof. apply _env_mapsto_splittable. Qed.

Lemma env_mapsto_positive{key: Type}{A: Type}{KE: EqDec key}: forall id sh (v: A) rho,
  env_mapsto id sh v rho -> nonidentity sh.
Proof.
(* Goal: forall (id : key) (sh : Share.t) (v : A) (rho : env key A) (_ : @env_mapsto key A KE id sh v rho), @nonidentity Share.t Share.Join_ba pa_share sh *)
  intros until rho.
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh sh) (pshare_sh sh'))) *)
  intro H; apply env_mapsto_get in H; destruct H.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
  apply nonunit_nonidentity; auto.
Qed.

Lemma emp_empty_env {key: Type}{A: Type}:  forall rho: env key A, emp rho <-> rho = empty_env.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
split; intros.
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
generalize (identity_unit (a:=empty_env)H); intro.
(* Goal: @eq (env key A) rho (@empty_env key A) *)
(* Goal: @identity (env key A) (@Join_env key A) rho *)
spec H0.
(* Goal: @joins (env key A) (@Join_env key A) rho (@empty_env key A) *)
(* Goal: @eq (env key A) rho (@empty_env key A) *)
(* Goal: @identity (env key A) (@Join_env key A) rho *)
exists rho; apply join_comm; apply empty_env_unit.
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
generalize (empty_env_unit rho); intro.
(* Goal: @eq (env key A) rho (@empty_env key A) *)
(* Goal: @identity (env key A) (@Join_env key A) rho *)
unfold unit_for in *.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
generalize (join_eq H0 (join_comm H1)); intro; auto.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
subst.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
apply unit_identity with empty_env; auto.
Qed.

Lemma emp_empty_env' {key}{A}: emp (@empty_env key A).
Proof.
(* Goal: @identity (env key A) (@Join_env key A) (@empty_env key A) *)
rewrite emp_empty_env.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
auto.
Qed.
Hint Resolve @emp_empty_env'.

Lemma env_mapsto_cohere{key: Type}{A: Type}{KE: EqDec key}: forall id sh1 (v1: A) sh2 v2,
  (env_mapsto id sh1 v1 * TT) && (env_mapsto id sh2 v2 * TT)
    |-- !!(v1=v2).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
  intros.
(* Goal: @derives (env key A) (@andp (env key A) (@sepcon (env key A) (@Join_env key A) (@env_mapsto key A KE id sh1 v1) (@TT (env key A))) (@sepcon (env key A) (@Join_env key A) (@env_mapsto key A KE id sh2 v2) (@TT (env key A)))) (@prop (env key A) (@eq A v1 v2)) *)
  intros w [? ?].
(* Goal: @prop (env key A) (@eq A v1 v2) w *)
  unfold prop.
(* Goal: @eq A v1 v2 *)
  destruct H as [?w [?w [? [? _]]]].
(* Goal: @eq A v1 v2 *)
  destruct H0 as [?w [?w [? [? _]]]].
(* Goal: @eq A v1 v2 *)
  apply env_mapsto_get in H1; destruct H1.
(* Goal: @eq A v1 v2 *)
  apply env_mapsto_get in H2; destruct H2.
(* Goal: @eq A v1 v2 *)
  destruct (env_get_join_sub _ _ _ _ _ (join_join_sub H) H1) as [sh' [? ?]].
(* Goal: @eq A v1 v2 *)
  destruct (env_get_join_sub _ _ _ _ _ (join_join_sub H0) H2) as [sh'' [? ?]].
(* Goal: @eq A v1 v2 *)
  congruence.
Qed.

Lemma env_mapsto_precise{key: Type}{A: Type}{KE: EqDec key}: forall id sh (v:A), precise (env_mapsto id sh v).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
  intros; intro; intros.
(* Goal: @eq (env key A) (@restrict_env key A KE (@nil key) ge) (@empty_env key A : env key A) *)
  apply env_ext.
(* Goal: @eq (forall _ : key, option (prod pshare A)) (@env_get key A w1) (@env_get key A w2) *)
  extensionality id'.
(* Goal: @identity (env key A) (@Join_env key A) rho *)
  destruct (eq_dec id id'); auto; subst.
(* Goal: @ex pshare (fun sh' : pshare => and (@eq (option (prod pshare A)) (@env_get key A rho' id) (@Some (prod pshare A) (@pair pshare A sh' v))) (@join_sub share Share.Join_ba (pshare_sh sh) (pshare_sh sh'))) *)
    apply env_mapsto_get in H; destruct H.
(* Goal: @ex pshare (fun sh : pshare => @eq (option (prod pshare A)) (env_get rho id) (@Some (prod pshare A) (@pair pshare A sh v))) *)
    apply env_mapsto_get in H0; destruct H0.
(* Goal: @eq (option (prod pshare A)) (@env_get key A w1 id') (@env_get key A w2 id') *)
(* Goal: @eq (option (prod pshare A)) (@env_get key A w1 id') (@env_get key A w2 id') *)
    rewrite H; rewrite H0.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
    repeat f_equal; auto. apply proof_irr.

(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
    eapply env_mapsto_get_neq in H; eauto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
    eapply env_mapsto_get_neq in H0; eauto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
    rewrite H; rewrite H0; auto.
Qed.

Definition own_var {key: Type}{A: Type}{KE: EqDec key} (sh: pshare) (id: key) : pred (env key A) :=
  exp (env_mapsto id (pshare_sh sh)).

Definition see_var {key: Type}{A: Type}{KE: EqDec key} (id: key) : pred (env key A) :=
  exp (fun sh: pshare => own_var sh id).

Definition own_all {key: Type}{A: Type}{KE: EqDec key} (l: list key) : pred (env key A) :=
   list_sepcon (map (own_var pfullshare) l).

Lemma own_all_nil {key: Type}{A: Type}{KE: EqDec key} : own_all nil = (emp: pred (env key A)).
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
Proof. unfold own_all; simpl; auto. Qed.

Opaque env_mapsto.
End EnvSL.



Definition restrict_env' {key: Type}{A: Type}{KE: EqDec key} (ids: list key) (rho: env key A) (id: key) : option (pshare * A) :=
  if  In_dec eq_dec id ids
                      then env_get rho id
                      else None.

Lemma restrict_env'_finite {key: Type}{A: Type}{KE: EqDec key} : forall ids (rho: env key A), finite_idfun (restrict_env' ids rho).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
unfold finite_idfun, restrict_env'; intros.
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (if @in_dec key (@eq_dec key KE) a ids then @env_get key A rho a else @None (prod pshare A)) (@None (prod pshare A))) *)
exists ids.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (in_dec eq_dec a ids); try contradiction; auto.
Qed.

Definition restrict_env {key: Type}{A: Type}{KE: EqDec key} (ids: list key) (rho:env key A) : env key A :=
  mk_env _ (restrict_env'_finite ids rho).

Definition restrict_env_comp' {key: Type}{A: Type}{KE: EqDec key} (ids: list key) (rho: env key A) (id: key) : option (pshare * A) :=
  if  In_dec eq_dec id ids
                      then None
                      else env_get rho id.

Lemma restrict_env_comp'_finite {key: Type}{A: Type}{KE: EqDec key}:
    forall ids (rho: env key A), finite_idfun (restrict_env_comp' ids rho).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
unfold finite_idfun, restrict_env_comp'; intros.
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (if @in_dec key (@eq_dec key KE) a ids then @None (prod pshare A) else @env_get key A rho a) (@None (prod pshare A))) *)
destruct (env_finite rho) as [l ?].
(* Goal: @ex (list key) (fun l : list key => forall (a : key) (_ : not (@In key a l)), @eq (option (prod pshare A)) (if @in_dec key (@eq_dec key KE) a ids then @None (prod pshare A) else @env_get key A rho a) (@None (prod pshare A))) *)
exists l.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (in_dec eq_dec a ids); try contradiction; auto.
Qed.

Definition restrict_env_comp  {key: Type}{A: Type}{KE: EqDec key} (ids: list key) (rho:env key A) : env key A:=
  mk_env _ (restrict_env_comp'_finite ids rho).

Lemma restrict_env_nil  {key: Type}{A: Type}{KE: EqDec key}:
  forall ge, restrict_env nil ge = (empty_env: env key A).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @eq (forall _ : key, option (prod pshare A)) (@env_get key A (@restrict_env key A KE (@nil key) ge)) (@env_get key A (@empty_env key A)) *)
apply env_ext. extensionality id.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
unfold restrict_env; rewrite env_get_mk_env; unfold restrict_env'; simpl.
(* Goal: @eq (option (prod pshare A)) (@None (prod pshare A)) (@env_get key A (@empty_env key A) id) *)
rewrite env_get_empty.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
auto.
Qed.

Lemma restrict_env_app  {key: Type}{A: Type}{KE: EqDec key} :
  forall ids1 ids2 (rho: env key A),  list_disjoint ids1 ids2 ->
    join (restrict_env ids1 rho) (restrict_env ids2 rho) (restrict_env (ids1++ids2) rho).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (env A B) (@Join_env A B) ab c (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) *)
intro id.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
unfold restrict_env; simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
repeat rewrite env_get_mk_env.
(* Goal: @eq (option (prod pshare A)) (@restrict_env' key A KE (@rev key ids) w id) (@restrict_env' key A KE ids w id) *)
unfold restrict_env'.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (if @in_dec key (@eq_dec key KE) id ids1 then @env_get key A rho id else @None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id ids2 then @env_get key A rho id else @None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id (@app key ids1 ids2) then @env_get key A rho id else @None (prod pshare A)) *)
unfold list_disjoint in H.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (if @in_dec key (@eq_dec key KE) id ids1 then @env_get key A rho id else @None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id ids2 then @env_get key A rho id else @None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id (@app key ids1 ids2) then @env_get key A rho id else @None (prod pshare A)) *)
specialize ( H id id).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (if @in_dec key (@eq_dec key KE) id ids1 then @env_get key A rho id else @None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id ids2 then @env_get key A rho id else @None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id (@app key ids1 ids2) then @env_get key A rho id else @None (prod pshare A)) *)
destruct (in_dec eq_dec id ids1).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id ids2 then @env_get key A rho id else @None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id (@app key ids1 ids2) then @env_get key A rho id else @None (prod pshare A)) *)
destruct (in_dec eq_dec id ids2).
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
contradiction H; auto.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id (@app key ids1 ids2) then @env_get key A rho id else @None (prod pshare A)) *)
destruct (in_dec eq_dec id (ids1++ids2)).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
contradiction n0;
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
rewrite in_app; auto.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id ids2 then @env_get key A rho id else @None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id (@app key ids1 ids2) then @env_get key A rho id else @None (prod pshare A)) *)
destruct (in_dec eq_dec id ids2).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id (@app key ids1 ids2) then @env_get key A rho id else @None (prod pshare A)) *)
destruct (in_dec eq_dec id (ids1++ids2)).
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
contradiction n0;
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
rewrite in_app; auto.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (if @in_dec key (@eq_dec key KE) id (@app key ids1 ids2) then @env_get key A rho id else @None (prod pshare A)) *)
destruct (in_dec eq_dec id (ids1++ids2)).
(* Goal: @eq (option (prod pshare A)) (if @eq_dec key KE id a then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (@None (prod pshare A)) *)
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
rewrite in_app in i; intuition.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
constructor.
Qed.

Lemma restrict_env_comp_join {key: Type}{A: Type}{KE: EqDec key}:
  forall ids (ge: env key A), join (restrict_env ids ge) (restrict_env_comp ids ge) ge.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @join (env A B) (@Join_env A B) ab c (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) *)
intro id.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@env_get key A (@restrict_env key A KE ids ge) id) (@env_get key A (@restrict_env_comp key A KE ids ge) id) (@env_get key A ge id) *)
unfold restrict_env, restrict_env_comp.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
repeat rewrite env_get_mk_env.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@restrict_env' key A KE ids ge id) (@restrict_env_comp' key A KE ids ge id) (@env_get key A ge id) *)
unfold restrict_env', restrict_env_comp'.
(* Goal: @join (option (prod pshare A)) (@Join_lower (prod pshare A) (Join_prod pshare Join_pshare A (@JA A))) (@None (prod pshare A)) (@None (prod pshare A)) (@None (prod pshare A)) *)
destruct (in_dec eq_dec id ids); constructor.
Qed.

Lemma restrict_env_rev {key: Type}{A: Type}{KE: EqDec key}:
    forall ids, @restrict_env key A _ (rev ids) = restrict_env ids.
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intros.
(* Goal: @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
extensionality w.
(* Goal: @eq (env key A) (@restrict_env key A KE (@rev key ids) w) (@restrict_env key A KE ids w) *)
unfold restrict_env.
(* Goal: @eq (forall _ : key, option (prod pshare A)) (@env_get key A (@restrict_env key A KE (@nil key) ge)) (@env_get key A (@empty_env key A)) *)
apply env_ext; extensionality id.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
repeat rewrite env_get_mk_env.
(* Goal: @eq (option (prod pshare A)) (@restrict_env' key A KE (@rev key ids) w id) (@restrict_env' key A KE ids w id) *)
unfold restrict_env'.
destruct (in_dec eq_dec id (rev ids));
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
destruct (in_dec eq_dec id ids); auto.
(* Goal: @eq (option (prod pshare A)) (@env_get key A w id) (@None (prod pshare A)) *)
(* Goal: @eq (option (prod pshare A)) (@None (prod pshare A)) (@env_get key A w id) *)
rewrite <- In_rev in i; contradiction.
(* Goal: @eq (option (prod pshare A)) (@None (prod pshare A)) (@env_get key A w id) *)
rewrite In_rev in i; contradiction.
Qed.


Instance Trip_pshareval {B} : @Trip_alg (option (pshare * B)) (Join_lower (Join_prod _ _ _ (Join_equiv B))).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intro; intros.
apply pshareval_join_e in H.
apply pshareval_join_e in H0.
apply pshareval_join_e in H1.
destruct a as [[[sa pa] va]|];
destruct b as [[[sb pb] vb]|];
destruct ab as [[[sab pab] vab]|]; try solve [elimtype False; inv H];
destruct c as [[[sc pc] vc]|];
destruct bc as [[[sbc pbc] vbc]|]; try solve [elimtype False; inv H0];
destruct ac as [[[sac pac] vac]|]; try solve [elimtype False; inv H1];
simpl in *;
try (assert (Hx: join sa sb sab /\ va = vb /\ vb = vab)
     by (inv H; simpl in *; intuition;
            match goal with H: @join B _ _ _ _ |- _ => destruct H end;
             congruence);
    decompose [and] Hx; clear H Hx; subst vab);
try (assert (Hx: join sb sc sbc /\ vb = vc /\ vb = vbc)
    by (inv H0; simpl in *; intuition;
            match goal with H: @join B _ _ _ _ |- _ => destruct H end;
             congruence);
    decompose [and] Hx; clear H0 Hx; subst vbc);
try (assert (Hx: join sa sc sac /\ va = vc /\ va = vac)
    by (inv H1; simpl in *; intuition;
            match goal with H: @join B _ _ _ _ |- _ => destruct H end;
             congruence);
    decompose [and] Hx; clear H1 Hx; subst vac);
subst; subst;
try solve [econstructor; constructor].
destruct (triple_join_exists_share _ _ _ _ _ _ H2 H H0) as [sabc ?].
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
assert (nonidentity sabc). eapply join_nonidentity. apply nonunit_nonidentity; apply pab. eauto.
exists (Some (mk_lifted _ (nonidentity_nonunit H1), vc)).
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
constructor; split; simpl; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
exists (Some (mk_lifted _ pac, vbc)); econstructor; simpl; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
inv H0. inv H. constructor; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
exists (Some (mk_lifted _ pbc, vac)); inv H1; inv H; constructor; simpl; auto.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
constructor; auto.
Qed.

Instance Trip_env {A} {EA: EqDec A} {B} {JB: Join B}: Trip_alg (env A B).
Proof.
(* Goal: forall ids : list key, @eq (forall _ : env key A, env key A) (@restrict_env key A KE (@rev key ids)) (@restrict_env key A KE ids) *)
intro; intros.
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
pose (f id := Trip_pshareval _ _ _ _ _ _ (H id) (H0 id) (H1 id)).
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
assert (finite_idfun (fun id => proj1_sig (f id))).
(* Goal: @finite_idfun A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
destruct (env_finite ab) as [l1 H3].
(* Goal: @finite_idfun A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
destruct (env_finite c) as [l2 H4].
(* Goal: @finite_idfun A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
exists (l1++l2).
(* Goal: forall (a : A) (_ : not (@In A a (@app A l1 l2))), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab a) (@env_get A B c a) abc) (f a)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
intro id; specialize ( H3 id); specialize ( H4 id).
(* Goal: forall _ : not (@In A id (@app A l1 l2)), @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
intro.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
assert (~ (In id l1 \/ In id l2)).
(* Goal: not (or (@In A id l1) (@In A id l2)) *)
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
contradict H2.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
rewrite in_app. auto.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
clear H2.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
destruct (In_dec eq_dec id l1) as [H5' | H5'].
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
contradiction H5; auto.
(* Goal: @eq (option (prod pshare A)) (if @eq_dec key KE id a then @Some (prod pshare A) (@pair pshare A sh v) else @None (prod pshare A)) (@None (prod pshare A)) *)
(* Goal: @ex env (fun rho : env => @_env_mapsto KE id (pshare_sh sh) v rho) *)
assert (H6: ~In id l2) by intuition.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
destruct (f id).
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
simpl.
(* Goal: @eq (option (prod pshare B)) x (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
apply pshareval_join_e in j.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
rewrite H3 in j; rewrite H4 in j; inv j; auto.
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
exists (mk_env (fun id => proj1_sig (f id)) H2).
(* Goal: @join (env A B) (@Join_env A B) ab c (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) *)
intro id.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) (@env_get A B (@mk_env A B (fun id : A => @proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (f id)) H2) id) *)
rewrite env_get_mk_env.
(* Goal: @eq (option (prod pshare B)) (@proj1_sig (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) (@exist (option (prod pshare B)) (fun abc : option (prod pshare B) => @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (Join_equiv B))) (@env_get A B ab id) (@env_get A B c id) abc) x j)) (@None (prod pshare B)) *)
(* Goal: @sig (env A B) (fun abc : env A B => @join (env A B) (@Join_env A B) ab c abc) *)
destruct (f id); simpl.
(* Goal: @join (option (prod pshare B)) (@Join_lower (prod pshare B) (Join_prod pshare Join_pshare B (@JA B))) (@env_get A B ab id) (@env_get A B c id) x *)
auto.
Qed.
