Require Export VST.msl.msl_standard.
Require Export VST.veric.base.
Require Export VST.veric.shares.
Require Import VST.msl.ghost.

Section Reference.
(* One common kind of PCM is one in which a central authority has a reference copy, and clients pass around
   partial knowledge. When a client recovers all pieces, it can gain full knowledge. *)
(* This is related to the snapshot PCM, but the snapshots aren't duplicable. *)

Lemma join_Bot : forall a b, sepalg.join a b Share.bot -> a = Share.bot /\ b = Share.bot.
Proof.
(* Goal: forall (a b : Share.t) (_ : @join Share.t Share.Join_ba a b Share.bot), and (@eq Share.t a Share.bot) (@eq Share.t b Share.bot) *)
  intros ?? (? & ?).
(* Goal: and (@eq Share.t a Share.bot) (@eq Share.t b Share.bot) *)
  apply lub_bot_e; auto.
Qed.

Global Program Instance pos_PCM (P : Ghost) : Ghost := { G := option (share * G);
  valid a := match a with Some (sh, _) => sh <> Share.bot | _ => True end;
  Join_G a b c := match a, b, c with
  | Some (sha, a'), Some (shb, b'), Some (shc, c') =>
      sha <> Share.bot /\ shb <> Share.bot /\ sepalg.join sha shb shc /\ join a' b' c'
  | Some (sh, a), None, Some c' | None, Some (sh, a), Some c' => c' = (sh, a)
  | None, None, None => True
  | _, _, _ => False
  end }.
Next Obligation.
(* Goal: and (forall (sh : share) (a : @G P) (c' : prod share (@G P)), not (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (and (forall (sh : share) (a : @G P) (c' : prod share (@G P)), not (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (and (not (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (forall (sha : share) (a' : @G P) (shb : share) (b' : @G P) (shc : share) (c' : @G P), not (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sha a')) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) (@Some (prod share (@G P)) (@pair share (@G P) s g)))))))) *)
repeat split; intros; intro H; decompose [and] H; congruence.
Defined.
Next Obligation.
(* Goal: and (forall (sh : share) (a : @G P) (c' : prod share (@G P)), not (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (and (forall (sh : share) (a : @G P) (c' : prod share (@G P)), not (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (and (not (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (forall (sha : share) (a' : @G P) (shb : share) (b' : @G P) (shc : share) (c' : @G P), not (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sha a')) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) (@Some (prod share (@G P)) (@pair share (@G P) s g)))))))) *)
repeat split; intros; intro H; decompose [and] H; congruence.
Defined.
Next Obligation.
(* Goal: and (forall (sh : share) (a : @G P) (c' : prod share (@G P)), not (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (and (forall (sh : share) (a : @G P) (c' : prod share (@G P)), not (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (and (not (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (forall (sha : share) (a' : @G P) (shb : share) (b' : @G P) (shc : share) (c' : @G P), not (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sha a')) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) (@Some (prod share (@G P)) (@pair share (@G P) s g)))))))) *)
repeat split; intros; intro H; decompose [and] H; congruence.
Defined.
Next Obligation.
(* Goal: and (forall (sh : share) (a : @G P) (c' : prod share (@G P)), not (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (and (forall (sh : share) (a : @G P) (c' : prod share (@G P)), not (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (and (not (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@None (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)))))) (forall (sha : share) (a' : @G P) (shb : share) (b' : @G P) (shc : share) (c' : @G P), not (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) (@None (prod share (@G P)))) (and (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sha a')) (@None (prod share (@G P)))) (@eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) (@Some (prod share (@G P)) (@pair share (@G P) s g)))))))) *)
repeat split; intros; intro H; decompose [and] H; congruence.
Defined.
Next Obligation.
(* Goal: @Sep_alg (option (prod share (@G P))) (fun a b c : option (prod share (@G P)) => match a as c' return (forall (_ : @eq (option (prod share (@G P))) c' a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p1) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (@G P) (@Join_G P) a0 b' c'))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p) c) => False | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => True end end end (@eq_refl (option (prod share (@G P))) a) (@eq_refl (option (prod share (@G P))) b) (@eq_refl (option (prod share (@G P))) c)) *)
exists (fun _ => None); auto.
(* Goal: forall t : option (prod share (@G P)), @unit_for (option (prod share (@G P))) (fun a b c : option (prod share (@G P)) => match a as c' return (forall (_ : @eq (option (prod share (@G P))) c' a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p1) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (@G P) (@Join_G P) a0 b' c'))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p) c) => False | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => True end end end (@eq_refl (option (prod share (@G P))) a) (@eq_refl (option (prod share (@G P))) b) (@eq_refl (option (prod share (@G P))) c)) (@None (prod share (@G P))) t *)
intros [[]|]; constructor.
Defined.
Next Obligation.
(* Goal: @Perm_alg (option (prod share (@G P))) (fun a b c : option (prod share (@G P)) => match a as c' return (forall (_ : @eq (option (prod share (@G P))) c' a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p1) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (@G P) (@Join_G P) a0 b' c'))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p) c) => False | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => True end end end (@eq_refl (option (prod share (@G P))) a) (@eq_refl (option (prod share (@G P))) b) (@eq_refl (option (prod share (@G P))) c)) *)
constructor.
  - intros [[]|] [[]|] [[]|] [[]|]; unfold join; simpl; auto; try contradiction; try congruence.
(* Goal: forall (_ : and (not (@eq share s Share.bot)) (and (not (@eq share s0 Share.bot)) (and (Share.Join_ba s s0 s1) (@Join_G P g g0 g1)))) (_ : and (not (@eq share s Share.bot)) (and (not (@eq share s0 Share.bot)) (and (Share.Join_ba s s0 s2) (@Join_G P g g0 g2)))), @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1)) (@Some (prod share (@G P)) (@pair share (@G P) s2 g2)) *)
    intros (? & ? & ? & ?) (? & ? & ? & ?); f_equal; f_equal; eapply join_eq; eauto.
  - intros [[]|] [[]|] [[]|] [[]|] [[]|]; try contradiction; unfold join; simpl;
      intros; decompose [and] H; decompose [and] H0;
      repeat match goal with H : (_, _) = (_, _) |- _ => inv H end;
      try solve [eexists (Some _); split; auto; simpl; auto]; try solve [exists None; split; auto].
    + destruct (join_assoc H2 H6) as (sh' & ? & ?), (join_assoc H5 H9) as (a' & ? & ?).
(* Goal: @sigT (option (prod share (@G P))) (fun f : option (prod share (@G P)) => and (match f as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0)) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0))) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1)) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1))) (_ : @eq (option (prod share (@G P))) a' f), Prop) with | Some p => let (shc, c') as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0)) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0))) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1)) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1))) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) f), Prop) := p in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0)) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0))) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1)) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1))) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) f) => and (not (@eq share s0 Share.bot)) (and (not (@eq share s1 Share.bot)) (and (Share.Join_ba s0 s1 shc) (@Join_G P g0 g1 c'))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0)) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0))) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1)) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1))) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) f) => False end (@eq_refl (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0))) (@eq_refl (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1))) (@eq_refl (option (prod share (@G P))) f)) (match f as b' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)) (@Some (prod share (@G P)) (@pair share (@G P) s g))) (_ : @eq (option (prod share (@G P))) b' f) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3)) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3))), Prop) with | Some p => let (shb, b') as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)) (@Some (prod share (@G P)) (@pair share (@G P) s g))) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) f) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3)) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3))), Prop) := p in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)) (@Some (prod share (@G P)) (@pair share (@G P) s g))) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) f) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3)) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3))) => and (not (@eq share s Share.bot)) (and (not (@eq share shb Share.bot)) (and (Share.Join_ba s shb s3) (@Join_G P g b' g3))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)) (@Some (prod share (@G P)) (@pair share (@G P) s g))) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) f) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3)) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3))) => @eq (prod share (@G P)) (@pair share (@G P) s3 g3) (@pair share (@G P) s g) end (@eq_refl (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g))) (@eq_refl (option (prod share (@G P))) f) (@eq_refl (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s3 g3))))) *)
      exists (Some (sh', a')); repeat (split; auto).
(* Goal: not (@eq share sh' Share.bot) *)
      intro; subst.
(* Goal: False *)
      apply join_Bot in H8 as []; auto.
    + exists (Some (s2, g2)); auto.
  - intros [[]|] [[]|] [[]|]; try contradiction; unfold join; auto.
(* Goal: forall _ : and (not (@eq share s Share.bot)) (and (not (@eq share s0 Share.bot)) (and (Share.Join_ba s s0 s1) (@Join_G P g g0 g1))), and (not (@eq share s0 Share.bot)) (and (not (@eq share s Share.bot)) (and (Share.Join_ba s0 s s1) (@Join_G P g0 g g1))) *)
    intros (? & ? & ? & ?); split; auto; split; auto; split; apply join_comm; auto.
  - intros [[]|] [[]|] [[]|] [[]|]; try contradiction; auto.
(* Goal: forall (_ : @join (option (prod share (@G P))) (fun a b c : option (prod share (@G P)) => match a as c' return (forall (_ : @eq (option (prod share (@G P))) c' a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p1) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (@G P) (@Join_G P) a0 b' c'))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p) c) => False | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => True end end end (@eq_refl (option (prod share (@G P))) a) (@eq_refl (option (prod share (@G P))) b) (@eq_refl (option (prod share (@G P))) c)) (@Some (prod share (@G P)) (@pair share (@G P) s g)) (@Some (prod share (@G P)) (@pair share (@G P) s0 g0)) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1))) (_ : @join (option (prod share (@G P))) (fun a b c : option (prod share (@G P)) => match a as c' return (forall (_ : @eq (option (prod share (@G P))) c' a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p1) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (@G P) (@Join_G P) a0 b' c'))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p) c) => False | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => True end end end (@eq_refl (option (prod share (@G P))) a) (@eq_refl (option (prod share (@G P))) b) (@eq_refl (option (prod share (@G P))) c)) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1)) (@Some (prod share (@G P)) (@pair share (@G P) s2 g2)) (@Some (prod share (@G P)) (@pair share (@G P) s g))), @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) s g)) (@Some (prod share (@G P)) (@pair share (@G P) s1 g1)) *)
    intros (? & ? & ? & ?) (? & ? & ? & ?); f_equal; f_equal; eapply join_positivity; eauto.
Defined.
Next Obligation.
destruct a as [[]|]; destruct b as [[]|]; destruct c as [[]|]; try trivial;
unfold join in *; try contradiction.
- decompose [and] H; assumption.
- congruence.
Defined.

Definition completable {P : Ghost} (a: @G (pos_PCM P)) r := exists x, join a x (Some (Tsh, r)).

Local Obligation Tactic := idtac.

Global Program Instance ref_PCM (P : Ghost) : Ghost :=
{ valid a := valid (fst a) /\ match snd a with Some r => completable (fst a) r | None => True end;
  Join_G a b c := @Join_G (pos_PCM P) (fst a) (fst b) (fst c) /\
    @psepalg.Join_lower _ (psepalg.Join_discrete _) (snd a) (snd b) (snd c) }.
Next Obligation.
(* Goal: forall P : Ghost, @Sep_alg (prod (@G (pos_PCM P)) (option (@G P))) (fun a b c : prod (@G (pos_PCM P)) (option (@G P)) => and (@Join_G (pos_PCM P) (@fst (@G (pos_PCM P)) (option (@G P)) a) (@fst (@G (pos_PCM P)) (option (@G P)) b) (@fst (@G (pos_PCM P)) (option (@G P)) c)) (@Join_lower (@G P) (Join_discrete (@G P)) (@snd (@G (pos_PCM P)) (option (@G P)) a) (@snd (@G (pos_PCM P)) (option (@G P)) b) (@snd (@G (pos_PCM P)) (option (@G P)) c))) *)
  intros P; apply sepalg_generators.Sep_prod.
  + apply @Sep_G.
  + apply psepalg.Sep_option.
Defined.
Next Obligation.
(* Goal: forall P : Ghost, @Perm_alg (prod (@G (pos_PCM P)) (option (@G P))) (fun a b c : prod (@G (pos_PCM P)) (option (@G P)) => and (@Join_G (pos_PCM P) (@fst (@G (pos_PCM P)) (option (@G P)) a) (@fst (@G (pos_PCM P)) (option (@G P)) b) (@fst (@G (pos_PCM P)) (option (@G P)) c)) (@Join_lower (@G P) (Join_discrete (@G P)) (@snd (@G (pos_PCM P)) (option (@G P)) a) (@snd (@G (pos_PCM P)) (option (@G P)) b) (@snd (@G (pos_PCM P)) (option (@G P)) c))) *)
  intros P; apply sepalg_generators.Perm_prod.
  + apply @Perm_G.
  + apply psepalg.Perm_option.
Defined.
Next Obligation.
(* Goal: forall (P : Ghost) (a b c : prod (@G (pos_PCM P)) (option (@G P))) (_ : @join (prod (@G (pos_PCM P)) (option (@G P))) (fun a0 b0 c0 : prod (@G (pos_PCM P)) (option (@G P)) => and (@Join_G (pos_PCM P) (@fst (@G (pos_PCM P)) (option (@G P)) a0) (@fst (@G (pos_PCM P)) (option (@G P)) b0) (@fst (@G (pos_PCM P)) (option (@G P)) c0)) (@Join_lower (@G P) (Join_discrete (@G P)) (@snd (@G (pos_PCM P)) (option (@G P)) a0) (@snd (@G (pos_PCM P)) (option (@G P)) b0) (@snd (@G (pos_PCM P)) (option (@G P)) c0))) a b c) (_ : (fun a0 : prod (@G (pos_PCM P)) (option (@G P)) => and (@valid (pos_PCM P) (@fst (@G (pos_PCM P)) (option (@G P)) a0)) (let filtered_var := @snd (@G (pos_PCM P)) (option (@G P)) a0 in let program_branch_0 := fun (r : @G P) (_ : @eq (option (@G P)) (@Some (@G P) r) filtered_var) => @completable P (@fst (@G (pos_PCM P)) (option (@G P)) a0) r in let program_branch_1 := fun _ : @eq (option (@G P)) (@None (@G P)) filtered_var => True in match filtered_var as anonymous' return (forall _ : @eq (option (@G P)) anonymous' filtered_var, Prop) with | Some r => program_branch_0 r | None => program_branch_1 end (@eq_refl (option (@G P)) filtered_var))) c), (fun a0 : prod (@G (pos_PCM P)) (option (@G P)) => and (@valid (pos_PCM P) (@fst (@G (pos_PCM P)) (option (@G P)) a0)) (let filtered_var := @snd (@G (pos_PCM P)) (option (@G P)) a0 in let program_branch_0 := fun (r : @G P) (_ : @eq (option (@G P)) (@Some (@G P) r) filtered_var) => @completable P (@fst (@G (pos_PCM P)) (option (@G P)) a0) r in let program_branch_1 := fun _ : @eq (option (@G P)) (@None (@G P)) filtered_var => True in match filtered_var as anonymous' return (forall _ : @eq (option (@G P)) anonymous' filtered_var, Prop) with | Some r => program_branch_0 r | None => program_branch_1 end (@eq_refl (option (@G P)) filtered_var))) a *)
  intros P ??? [? J] []; split; [eapply join_valid; eauto|].
(* Goal: let filtered_var := @snd (@G (pos_PCM P)) (option (@G P)) a in let program_branch_0 := fun (r : @G P) (_ : @eq (option (@G P)) (@Some (@G P) r) filtered_var) => @completable P (@fst (@G (pos_PCM P)) (option (@G P)) a) r in let program_branch_1 := fun _ : @eq (option (@G P)) (@None (@G P)) filtered_var => True in match filtered_var as anonymous' return (forall _ : @eq (option (@G P)) anonymous' filtered_var, Prop) with | Some r => program_branch_0 r | None => program_branch_1 end (@eq_refl (option (@G P)) filtered_var) *)
  destruct a, b, c; simpl in *; inv J; auto.
  + destruct o1; auto.
(* Goal: @completable P g g2 *)
    destruct H1.
(* Goal: @completable P g g2 *)
    destruct (join_assoc H H1) as (? & ? & ?); eexists; eauto.
  + inv H2.
Defined.

End Reference.

Program Instance exclusive_PCM A : Ghost := { valid a := True; Join_G := Join_lower (Join_discrete A) }.


Definition ext_PCM Z : Ghost := ref_PCM (exclusive_PCM Z).

Lemma valid_ext : forall {Z} (ora : Z), @valid (ext_PCM _) (Some (Tsh, Some ora), None).
Proof.
(* Goal: forall (Z : Type) (ora : Z), @valid (ext_PCM Z) (@pair (option (prod share (option Z))) (option (option Z)) (@Some (prod share (option Z)) (@pair share (option Z) Tsh (@Some Z ora))) (@Some (option Z) (@Some Z ora))) *)
  intros; simpl; split; auto.
(* Goal: not (@eq share Tsh Share.bot) *)
  apply Share.nontrivial.
Qed.

Definition ext_ghost {Z} (ora : Z) : {g : ghost.Ghost & {a : ghost.G | ghost.valid a}} :=
  existT _ (ext_PCM _) (exist _ _ (valid_ext ora)).

Lemma valid_ext_ref : forall {Z} (ora : Z), @valid (ext_PCM _) (None, Some (Some ora)).
Proof.
(* Goal: forall (Z : Type) (ora : Z), @valid (ext_PCM Z) (@pair (option (prod share (option Z))) (option (option Z)) (@Some (prod share (option Z)) (@pair share (option Z) Tsh (@Some Z ora))) (@Some (option Z) (@Some Z ora))) *)
  intros; simpl; split; auto.
(* Goal: @Perm_alg (option (prod share (@G P))) (fun a b c : option (prod share (@G P)) => match a as c' return (forall (_ : @eq (option (prod share (@G P))) c' a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p1) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (@G P) (@Join_G P) a0 b' c'))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p) c) => False | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => True end end end (@eq_refl (option (prod share (@G P))) a) (@eq_refl (option (prod share (@G P))) b) (@eq_refl (option (prod share (@G P))) c)) *)
  eexists (Some (_, _)); constructor.
Qed.

Definition ext_ref {Z} (ora : Z) : {g : ghost.Ghost & {a : ghost.G | ghost.valid a}} :=
  existT _ (ext_PCM _) (exist _ _ (valid_ext_ref ora)).

Lemma valid_ext_both : forall {Z} (ora : Z), @valid (ext_PCM _) (Some (Tsh, Some ora), Some (Some ora)).
Proof.
(* Goal: forall (Z : Type) (ora : Z), @valid (ext_PCM Z) (@pair (option (prod share (option Z))) (option (option Z)) (@Some (prod share (option Z)) (@pair share (option Z) Tsh (@Some Z ora))) (@Some (option Z) (@Some Z ora))) *)
  intros; simpl; split; auto.
  - apply Share.nontrivial.
(* Goal: @Perm_alg (option (prod share (@G P))) (fun a b c : option (prod share (@G P)) => match a as c' return (forall (_ : @eq (option (prod share (@G P))) c' a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) a) (_ : @eq (option (prod share (@G P))) b b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p1) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (@G P) (@Join_G P) a0 b' c'))) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) shb b')) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) b' b) (_ : @eq (option (prod share (@G P))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p0) b) (_ : @eq (option (prod share (@G P))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) c') c) => @eq (prod share (@G P)) c' (@pair share (@G P) sh a0) | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) (@pair share (@G P) sh a0)) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@Some (prod share (@G P)) p) c) => False | None => fun (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) a) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) b) (_ : @eq (option (prod share (@G P))) (@None (prod share (@G P))) c) => True end end end (@eq_refl (option (prod share (@G P))) a) (@eq_refl (option (prod share (@G P))) b) (@eq_refl (option (prod share (@G P))) c)) *)
  - exists None; constructor.
Qed.

Definition ext_both {Z} (ora : Z) : {g : ghost.Ghost & {a : ghost.G | ghost.valid a}} :=
  existT _ (ext_PCM _) (exist _ _ (valid_ext_both ora)).
