Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import Program.
Require Import Omega.

Set Implicit Arguments.
Obligation Tactic := intros; desc; try done.

Lemma lift_plus_helper A B (p : A → option B) (PF : ∀ x, p x ≠ None) :
  { f | ∀ x, p x = Some (f x) }.
Proof.
  apply constructive_definite_description.
  rewrite <- unique_existence; split.
    apply choice with (R := fun x y ⇒ p x = Some y).
    by intro x; specialize (PF x); destruct (p x); vauto.
  clear; red; intros; apply functional_extensionality; intro a.
  specialize (H a); specialize (H0 a); congruence.
Qed.

Definition lift_plus A B p (f g : A → B) : option (A → B) :=
  match excluded_middle_informative (∀ x, p (f x) (g x) ≠ None) with
    | left PF ⇒ Some (proj1_sig (lift_plus_helper (fun x ⇒ p (f x) (g x)) PF))
    | _ ⇒ None
  end.

Lemma lift_plus_someD A B p (f g : A → B) h :
  lift_plus p f g = Some h ↔ ∀ x, p (f x) (g x) = Some (h x).
Proof.
  unfold lift_plus, proj1_sig; ins; desf; split; ins; desf.
    f_equal; apply functional_extensionality; intro a; clear Heq.
    specialize (H a); specialize (e a); congruence.
  destruct n; congruence.
Qed.

Lemma lift_plus_noneD A B p (f g : A → B) :
  lift_plus p f g = None ↔ ∃ x, p (f x) (g x) = None.
Proof.
  unfold lift_plus, proj1_sig; ins; desf; split; ins; desf.
    by clear Heq; specialize (n x0); desf.
  apply NNPP; intro M; destruct n; red; ins; eauto.
Qed.

Lemma lift_plus_emp_l A B p (f : A → B) e (E: ∀ x, p e x = Some x) :
  lift_plus p (fun _ ⇒ e) f = Some f.
Proof. by rewrite lift_plus_someD; eauto. Qed.

Lemma lift_plusC B p (C: ∀ x y, p x y = p y x) A (f g : A → B) :
  lift_plus p f g = lift_plus p g f.
Proof.
  unfold lift_plus, proj1_sig; desf; clear Heq; try clear Heq0.
    by f_equal; extensionality a; generalize (e a), (e0 a); rewrite C;
       clear; congruence.
    by destruct n0; intros; rewrite C.
    by destruct n; intros; rewrite C.
Qed.

Lemma lift_plusA B p
  (ASSOC: ∀ x y xy (P1: p x y = Some xy) z xyz (P2: p xy z = Some xyz),
          ∃ yz, p y z = Some yz ∧ p x yz = Some xyz)
  A (x y xy : A → B) (P1: lift_plus p x y = Some xy) z xyz
  (P2: lift_plus p xy z = Some xyz) :
    ∃ yz, lift_plus p y z = Some yz ∧ lift_plus p x yz = Some xyz.
Proof.
  unfold lift_plus, proj1_sig in *; desf; clear Heq Heq0; try clear Heq1.
  eexists; split; try done; desf; try clear Heq.
  f_equal; extensionality a.
  generalize (e a), (e0 a), (e1 a), (e2 a); clear e e0 e1 e2; ins.
  exploit (ASSOC (x a) (y a)); eauto; ins; desf.

  destruct n2; intros a ?.
  generalize (e a), (e0 a), (e1 a); clear e e0 e1; ins.
  exploit (ASSOC (x a) (y a)); eauto; ins; desf.

  destruct n; intros a ?.
  generalize (e a), (e0 a); clear e e0; ins.
  exploit (ASSOC (x a) (y a)); eauto; ins; desf.
Qed.

Lemma lift_plusA2 B p
  (ASSOC: ∀ x y xy (P1: p x y = Some xy) z (P2: p xy z = None),
    p y z = None ∨ ∃ yz, p y z = Some yz ∧ p x yz = None)
  A (x y xy : A → B) (P1: lift_plus p x y = Some xy) z
  (P2: lift_plus p xy z = None) :
   lift_plus p y z = None ∨
   ∃ yz, lift_plus p y z = Some yz ∧ lift_plus p x yz = None.
Proof.
  unfold lift_plus, proj1_sig in *; desf; vauto.
  right; clear Heq Heq0; try clear Heq1.
  eexists; split; try done; desf; try clear Heq.
  destruct n0; ins; intro.
  eapply ASSOC in H; eauto; desf; congruence.
Qed.

Lemma lift_plus_some_inv A B p (a b c : A → B) (EQ : lift_plus p a b = Some c) l :
  p (a l) (b l) = Some (c l).
Proof.
  unfold lift_plus in *; desf; destruct lift_plus_helper; ins.
Qed.

Lemma lift_plus_none_inv A B p (a b : A → B) (EQ : lift_plus p a b = None) :
  ∃ l, p (a l) (b l) = None.
Proof.
  unfold lift_plus in *; desf; apply NNPP; intro; destruct n; red; eauto.
Qed.

Section olift.

  Variable A : Type.
  Variable op1 : A → A.
  Variable bop : A → A → option A.

  Definition olift_unary ao :=
    match ao with
      | None ⇒ None
      | Some a ⇒ Some (op1 a)
    end.

  Definition olift_plus ao bo :=
    match ao, bo with
        None, bo ⇒ Some bo
      | Some a, None ⇒ Some (Some a)
      | Some a, Some b ⇒ match bop a b with
                            | Some v ⇒ Some (Some v)
                            | None ⇒ None
                          end
    end.

  Lemma olift_plusC (C: ∀ x y, bop x y = bop y x) a b :
    olift_plus a b = olift_plus b a.
  Proof.
    unfold olift_plus, proj1_sig; desf; congruence.
  Qed.

  Lemma olift_plusA
        (ASSOC: ∀ x y xy (P1: bop x y = Some xy) z xyz (P2: bop xy z = Some xyz),
          ∃ yz, bop y z = Some yz ∧ bop x yz = Some xyz)
        x y xy (P1: olift_plus x y = Some xy) z xyz
        (P2: olift_plus xy z = Some xyz) :
    ∃ yz, olift_plus y z = Some yz ∧ olift_plus x yz = Some xyz.
  Proof.
    unfold olift_plus, proj1_sig in *; desf; eauto.
    by exploit (ASSOC a2); eauto; intro; desf; repeat eexists; ins; desf.
    by exploit (ASSOC a1); eauto; intro; desf; repeat eexists; ins; desf.
    by repeat eexists; ins; desf.
    by repeat eexists; ins; desf.
  Qed.

  Lemma olift_plusA2
        (ASSOC: ∀ x y xy (P1: bop x y = Some xy) z (P2: bop xy z = None),
                  bop y z = None ∨ ∃ yz, bop y z = Some yz ∧ bop x yz = None)
        x y xy (P1: olift_plus x y = Some xy) z
        (P2: olift_plus xy z = None) :
    olift_plus y z = None ∨
    ∃ yz, olift_plus y z = Some yz ∧ olift_plus x yz = None.
  Proof.
    unfold olift_plus, proj1_sig in *; desf; vauto.
    by exploit (ASSOC a2); eauto; intro; desf; right; eexists; split; desf.
    by right; eexists; split; desf.
  Qed.

  Lemma olift_distr :
    ∀
      (D : ∀ x y xy, bop x y = Some xy → bop (op1 x) (op1 y) = Some (op1 xy))
      x y xy,
      olift_plus x y = Some xy →
      olift_plus (olift_unary x) (olift_unary y) = Some (olift_unary xy).
  Proof.
    unfold olift_plus, olift_unary; ins; desf; erewrite D in *; eauto; desf.
  Qed.

  Lemma olift_idemp :
    ∀ (IDEM : ∀ x, op1 (op1 x) = op1 x) x,
      olift_unary (olift_unary x) = olift_unary x.
  Proof.
    unfold olift_unary; ins; desf; rewrite IDEM in *; eauto.
  Qed.

  Lemma olift_pidemp :
    ∀ (IDEM : ∀ x, bop x (op1 x) = Some x) x,
      olift_plus x (olift_unary x) = Some x.
  Proof.
    unfold olift_plus, olift_unary; ins; desf; rewrite IDEM in *; desf; eauto.
  Qed.

  Lemma olift_max :
    ∀
      (MAX: ∀ x y xy z,
              bop x y = Some xy → bop xy z = Some x → op1 y = y)
      x y xy z
      (P1 : olift_plus x y = Some xy)
      (P2 : olift_plus xy z = Some x),
    olift_unary y = y.
  Proof.
    unfold olift_plus, olift_unary; ins; desf; f_equal; eauto.
  Qed.

  Lemma olift_pcancel :
    ∀
      u (UNIT: ∀ x, bop x (u x) = Some x)
        (UNIT2: ∀ x, bop (op1 x) (u x) = Some (op1 x))
        (MAX: ∀ x y xy z,
              bop x y = Some xy → bop xy z = Some x → op1 y = y)
        (DIST : ∀ x y xy, bop x y = Some xy → bop (op1 x) (op1 y) = Some (op1 xy))
      (PCANCEL : ∀ x y1 y2 z,
                   bop x y1 = Some z →
                   bop x y2 = Some z →
                   bop (op1 x) y1 = bop (op1 x) y2) x y1 y2 z
      (P1 : olift_plus x y1 = Some z)
      (P2 : olift_plus x y2 = Some z),
      olift_plus (olift_unary x) y1 = olift_plus (olift_unary x) y2.
  Proof.
    unfold olift_plus in *; ins; desf; ins; desf; eauto;
    try (by erewrite (PCANCEL a4 a0 a2) in *; desf; eauto);
    try (by erewrite (PCANCEL a3 a0 a2) in *; desf; eauto);
    try (by erewrite (PCANCEL a3 a0 a1) in *; desf; eauto);
    try (by erewrite (PCANCEL a1 a0 (u a1)) in *; desf; eauto; rewrite UNIT2 in *; desf);
    exploit (MAX a2); eauto; eapply DIST in Heq1; eauto; congruence.
  Qed.

End olift.

Section plift.

  Variable A : Type.
  Variable f : A → Type.
  Variable op1 : ∀ A, f A → f A.
  Variable bop : ∀ A, f A → f A → option (f A).
  Implicit Types x y : { m : A & f m }.

  Definition plift_unary x : { m : A & f m } :=
    match x with
      | (existT _ m p) ⇒ existT _ m (op1 p)
    end.

  Definition plift_plus x1 x2 : option { m : A & f m } :=
    match x1, x2 with
      | existT _ m1 p1, existT _ m2 p2 ⇒
        match excluded_middle_informative (m2 = m1) with
          | left PF ⇒
            match bop p1 (eq_rect _ _ p2 _ PF) with
              | Some res ⇒
                Some (existT _ m1 res)
              | None ⇒ None
            end
          | right _ ⇒ None
        end
    end.

  Lemma plift_plusC (C: ∀ m (x y : f m), bop x y = bop y x) a b :
    plift_plus a b = plift_plus b a.
  Proof.
    unfold plift_plus; desf; ins; rewrite <- eq_rect_eq in *; congruence.
  Qed.

  Lemma plift_plusA
        (ASSOC: ∀ m (x y xy : f m) (P1: bop x y = Some xy) z xyz (P2: bop xy z = Some xyz),
                ∃ yz, bop y z = Some yz ∧ bop x yz = Some xyz)
        (x y xy : { m : A & f m }) (P1: plift_plus x y = Some xy) z xyz
        (P2: plift_plus xy z = Some xyz) :
    ∃ yz, plift_plus y z = Some yz ∧ plift_plus x yz = Some xyz.
  Proof.
    destruct x, y, z; ins; desf; ins; desf; rewrite <- eq_rect_eq in *;
    generalize (ASSOC _ _ _ _ Heq0 _ _ Heq1); ins; desf;
    repeat eexists; ins; desf; rewrite <- eq_rect_eq in *; desf.
  Qed.

  Lemma plift_plusA2
        (ASSOC: ∀ m (x y xy : f m) (P1: bop x y = Some xy) z (P2: bop xy z = None),
                  bop y z = None ∨ ∃ yz, bop y z = Some yz ∧ bop x yz = None)
        (x y xy : { m : A & f m }) (P1: plift_plus x y = Some xy) z
        (P2: plift_plus xy z = None) :
    plift_plus y z = None ∨
    ∃ yz, plift_plus y z = Some yz ∧ plift_plus x yz = None.
  Proof.
    destruct x, y, z; ins; desf; ins; desf; vauto; rewrite <- eq_rect_eq in ×.
    generalize (ASSOC _ _ _ _ Heq0 _ Heq1); ins; desf;
    right; repeat eexists; ins; desf; rewrite <- eq_rect_eq in *; desf.
  Qed.

  Lemma plift_distr :
    ∀
      (D : ∀ m (x y xy : f m), bop x y = Some xy → bop (op1 x) (op1 y) = Some (op1 xy))
      x y xy,
      plift_plus x y = Some xy →
      plift_plus (plift_unary x) (plift_unary y) = Some (plift_unary xy).
  Proof.
    destruct x, y; ins; desf; rewrite <- eq_rect_eq in *; erewrite D in *; eauto; desf.
  Qed.

  Lemma plift_idemp :
    ∀ (IDEM : ∀ m (x : f m), op1 (op1 x) = op1 x) x,
      plift_unary (plift_unary x) = plift_unary x.
  Proof.
    destruct x; ins; desf; rewrite IDEM in *; eauto.
  Qed.

  Lemma plift_pidemp :
    ∀ (IDEM : ∀ m (x : f m), bop x (op1 x) = Some x) x,
      plift_plus x (plift_unary x) = Some x.
  Proof.
    destruct x; ins; desf; rewrite <- eq_rect_eq, IDEM in *; desf; eauto.
  Qed.

  Lemma plift_max :
    ∀
      (MAX: ∀ m (x y xy z: f m),
              bop x y = Some xy → bop xy z = Some x → op1 y = y)
      x y xy z
      (P1 : plift_plus x y = Some xy)
      (P2 : plift_plus xy z = Some x),
    plift_unary y = y.
  Proof.
    destruct x, y, z; ins; desf; ins; desf; ins; f_equal; eauto.
  Qed.

  Lemma plift_pcancel :
    ∀
      (PCANCEL : ∀ m (x y1 y2 z : f m),
                   bop x y1 = Some z →
                   bop x y2 = Some z →
                   bop (op1 x) y1 = bop (op1 x) y2) x y1 y2 z
      (P1 : plift_plus x y1 = Some z)
      (P2 : plift_plus x y2 = Some z),
      plift_plus (plift_unary x) y1 = plift_plus (plift_unary x) y2.
  Proof.
    unfold plift_plus in *; ins; desf; ins; desf; eauto.
      by erewrite (PCANCEL _ f5 f1 f3) in *; desf; eauto.
      by erewrite (PCANCEL _ f4 f1 f3) in *; desf; eauto.
      by erewrite (PCANCEL _ f4 f1 f2) in *; desf; eauto.
  Qed.

End plift.

Ltac inv_lplus a :=
  repeat match goal with
           | H : lift_plus _ _ _ = Some _ |- _ ⇒
             apply lift_plus_some_inv with (l:=a) in H
           | H : Some _ = lift_plus _ _ _ |- _ ⇒
             symmetry in H; apply lift_plus_some_inv with (l:=a) in H
         end.

Ltac inv_lplus2 a :=
  repeat match goal with
           | H : lift_plus _ _ _ = None |- _ ⇒
             apply lift_plus_none_inv in H; destruct H as [a H]
           | H : None = lift_plus _ _ _ |- _ ⇒
             symmetry in H; apply lift_plus_none_inv in H; destruct H as [a H]
           | H : lift_plus _ _ _ = Some _ |- _ ⇒
             apply lift_plus_some_inv with (l:=a) in H
           | H : Some _ = lift_plus _ _ _ |- _ ⇒
             symmetry in H; apply lift_plus_some_inv with (l:=a) in H
         end.

Record salg_mod := mk_salg
  { salg :> Type
  ; salg_emp : salg
  ; salg_plus : salg → salg → option salg
  ; salg_strip : salg → salg
  ; salg_leq : salg → salg → bool
  ; salg_plusC :
      ∀ x y, salg_plus x y = salg_plus y x
  ; salg_plusI :
      ∀ x, salg_plus salg_emp x = Some x
  ; salg_plusA :
      ∀ x y xy (P1: salg_plus x y = Some xy) z xyz
                    (P2: salg_plus xy z = Some xyz),
    ∃ yz, salg_plus x yz = Some xyz ∧
               salg_plus y z = Some yz
  ; salg_plusA2 :
      ∀ x y xy (P1: salg_plus x y = Some xy) z
                    (P2: salg_plus xy z = None),
        salg_plus y z = None
        ∨ ∃ yz, salg_plus x yz = None ∧
                      salg_plus y z = Some yz
  ; salg_eq_empD :
      ∀ g g', salg_plus g g' = Some salg_emp →
                   g = salg_emp
  ; salg_strip_emp :
      salg_strip salg_emp = salg_emp
  ; salg_strip_plus :
      ∀ x y xy,
        salg_plus x y = Some xy →
        salg_plus (salg_strip x) (salg_strip y) = Some (salg_strip xy)
  ; salg_plus_strip_idemp :
      ∀ x, salg_plus x (salg_strip x) = Some x
  ; salg_strip_max :
      ∀ x y xy z,
        salg_plus x y = Some xy →
        salg_plus xy z = Some x →
        salg_strip y = y
  ; salg_pcancel :
      ∀ g g1 g2 gg,
        salg_plus g g1 = Some gg →
        salg_plus g g2 = Some gg →
        salg_plus (salg_strip g) g1 =
        salg_plus (salg_strip g) g2
  ; salg_leq_refl : ∀ x, salg_leq x x
  ; salg_leq_as : ∀ x y, salg_leq x y → salg_leq y x → x = y
  ; salg_leq_trans : ∀ x y z, salg_leq x y → salg_leq y z → salg_leq x z
  ; salg_leq_total : ∀ x y, salg_leq x y ∨ salg_leq y x
  }.

Lemma salg_strip_idemp :
  ∀ m x, salg_strip m (salg_strip m x) = salg_strip m x.
Proof.
  ins; eapply salg_strip_max; [by apply salg_plus_strip_idemp|].
  by rewrite salg_plusC; apply salg_plusI.
Qed.

Lemma salg_plus_emp_r :
  ∀ m x, salg_plus m x (salg_emp m) = Some x.
Proof.
  by ins; rewrite salg_plusC, salg_plusI.
Qed.

Lemma salg_plusA3 :
  ∀ (A: salg_mod) x y xy z,
  salg_plus A x y = Some xy →
  salg_plus A x z = None ∨ salg_plus A y z = None →
  salg_plus A xy z = None.
Proof.
  ins; case_eq (salg_plus A xy z) as N; ins.
  rewrite salg_plusC in H.
  eapply salg_plusA in N; eauto; desf.
  rewrite salg_plusC in N; eapply salg_plusA in N; eauto; desf.
  rewrite salg_plusC in N1; desf.
Qed.

Lemma salg_plusA4 :
  ∀ (A: salg_mod) x y xy yz z,
    salg_plus A x y = Some xy →
    salg_plus A y z = Some yz →
    salg_plus A x yz = None →
    salg_plus A xy z = None.
Proof.
  ins; case_eq (salg_plus A xy z) as N; ins.
  eapply salg_plusA in N; eauto; desf.
Qed.

Structure ghost_resource :=
  mk_gres {
      gres_fun :> nat → option { m : salg_mod & salg m } ;
      gres_finite :
        ∃ max, ∀ n', max < n' → gres_fun n' = None
    }.

Program Definition gres_emp :=
  {| gres_fun := fun _ ⇒ None |}.
Next Obligation. by ∃ 0. Qed.

Program Definition gres_one (n : nat) g :=
  {| gres_fun := fun n' ⇒ if (n==n')%bool then g else None |}.
Next Obligation.
  ∃ (S n); ins; desf; desf; exfalso; omega.
Qed.

Program Definition gres_plus (g1 g2 : ghost_resource) :=
  match lift_plus (olift_plus (plift_plus _ salg_plus)) g1 g2 with
    | Some g ⇒ Some {| gres_fun := g |}
    | None ⇒ None
  end.
Next Obligation.
  destruct g1, g2; desf.
  subst filtered_var.
  ∃ (max + max0); ins; inv_lplus n'.
  unfold olift_plus in *; desf; desf.
  rewrite gres_finite0 in *; ins; omega.
  rewrite gres_finite0 in *; ins; omega.
  rewrite gres_finite1 in *; ins; omega.
Qed.

Program Definition gres_strip (g : ghost_resource) :=
  {| gres_fun := fun l ⇒ olift_unary (plift_unary _ salg_strip) (g l) |}.
Next Obligation.
  destruct g; desf; ∃ max; ins; inv_lplus n'.
  by rewrite gres_finite0.
Qed.

Lemma gres_ext f g : (∀ n, gres_fun f n = gres_fun g n) → f = g.
Proof.
  ins; apply functional_extensionality in H.
  destruct f, g; ins; subst; f_equal; apply proof_irrelevance.
Qed.

Lemma gres_plusC x y : gres_plus x y = gres_plus y x.
Proof.
  intros; unfold gres_plus; repeat des_eqrefl; f_equal;
    try first [apply gres_ext; ins | exfalso];
    rewrite lift_plusC in EQ; try congruence;
    apply olift_plusC, plift_plusC, salg_plusC.
Qed.

Lemma gres_plusI x : gres_plus gres_emp x = Some x.
Proof.
  unfold gres_plus, gres_emp; ins; des_eqrefl; f_equal;
  try first [apply gres_ext; ins | exfalso];
  rewrite lift_plus_emp_l in EQ; try congruence; ins.
Qed.

Lemma gres_plus_emp_r x : gres_plus x gres_emp = Some x.
Proof.
  rewrite gres_plusC; apply gres_plusI.
Qed.

Lemma gres_plusA :
  ∀ x y xy (P1: gres_plus x y = Some xy) z xyz
                (P2: gres_plus xy z = Some xyz),
    ∃ yz, gres_plus x yz = Some xyz ∧ gres_plus y z = Some yz.
Proof.
  unfold gres_plus; ins; repeat des_eqrefl; desf; ins.
    eexists; split; ins; ins; des_eqrefl; f_equal;
    try first [apply gres_ext; ins | exfalso];
    symmetry in EQ0, EQ1, EQ, EQ2;
    eapply lift_plusA in EQ; eauto; ins; desf;
    eapply olift_plusA; eauto; eapply plift_plusA;
    by clear; ins; destruct (salg_plusA _ _ _ P1 _ P2); desf; eauto.
  exfalso; symmetry in EQ0, EQ1, EQ;
  eapply lift_plusA in EQ; eauto; ins; desf.
  eapply olift_plusA; eauto; eapply plift_plusA;
  by clear; ins; destruct (salg_plusA _ _ _ P1 _ P2); desf; eauto.
Qed.

Lemma gres_plusA2 :
  ∀ x y xy (P1: gres_plus x y = Some xy) z (P2: gres_plus xy z = None),
    gres_plus y z = None
    ∨ ∃ yz, gres_plus x yz = None ∧ gres_plus y z = Some yz.
Proof.
  unfold gres_plus; ins; repeat des_eqrefl; desf; ins.
  symmetry in EQ, EQ0; eapply lift_plusA2 in EQ; eauto; desf;
   [left | right | ins]; try des_eqrefl; ins;
    try (exfalso; congruence).
  eexists; split; ins; ins; des_eqrefl; ins; exfalso; congruence.
  eapply olift_plusA2; eauto; eapply plift_plusA2; clear; ins.
  eapply salg_plusA2 in P2; eauto; desf; eauto.
Qed.

Lemma gres_eq_empD x y : gres_plus x y = Some gres_emp → x = gres_emp.
Proof.
  unfold gres_plus, gres_emp; ins; des_eqrefl; apply gres_ext; ins; desf.
  inv_lplus n; unfold olift_plus in *; desf.
Qed.

Lemma gres_strip_emp : gres_strip gres_emp = gres_emp.
Proof.
  by apply gres_ext; ins; apply elem_gres_strip_emp.
Qed.

Lemma gres_strip_plus x y xy :
  gres_plus x y = Some xy →
  gres_plus (gres_strip x) (gres_strip y) = Some (gres_strip xy).
Proof.
  unfold gres_plus; ins; repeat (des_eqrefl; ins); f_equal;
    first [apply gres_ext | exfalso]; ins; desf; ins;
  inv_lplus2 n;
  eapply olift_distr in EQ; eauto using plift_distr, salg_strip_plus; desf.
Qed.

Lemma gres_strip_idemp x : gres_strip (gres_strip x) = gres_strip x.
Proof.
  apply gres_ext; ins; apply olift_idemp, plift_idemp, salg_strip_idemp.
Qed.

Lemma gres_plus_strip_idemp x : gres_plus x (gres_strip x) = Some x.
Proof.
  unfold gres_plus; des_eqrefl; f_equal; try apply gres_ext; ins;
  inv_lplus2 n; rewrite olift_pidemp in EQ; desf;
  eauto using plift_pidemp, salg_plus_strip_idemp.
Qed.

Lemma gres_strip_max x y xy z :
  gres_plus x y = Some xy →
  gres_plus xy z = Some x →
  gres_strip y = y.
Proof.
  unfold gres_plus; ins; apply gres_ext; ins.
  ins; repeat (des_eqrefl; ins); desf.
  destruct x, y, z; ins; desf; inv_lplus n.
  eapply olift_max; eauto using plift_max, salg_strip_max.
Qed.

Lemma gres_pcancel :
  ∀ g g1 g2 gg,
    gres_plus g g1 = Some gg →
    gres_plus g g2 = Some gg →
    gres_plus (gres_strip g) g1 = gres_plus (gres_strip g) g2.
Proof.
  unfold gres_plus; ins; repeat (des_eqrefl; ins); f_equal;
  first [ apply gres_ext; ins | exfalso ]; desf; inv_lplus2 n.

  assert (Some (o1 n) = Some (o2 n)); desf.
  rewrite <- EQ1, <- EQ2; eapply olift_pcancel with
    (u := fun x ⇒ match x with
                     | (existT _ m p) ⇒
                       existT _ m (salg_emp m) end);
  eauto using plift_pcancel, salg_pcancel, plift_max, salg_strip_max,
              plift_distr, salg_strip_plus; ins; desf; ins; desf; ins;
  rewrite <- ?eq_rect_eq, ?salg_plus_emp_r in *; desf.

  assert (Some (o1 n) = None); desf.
  rewrite <- EQ1, <- EQ2; eapply olift_pcancel with
    (u := fun x ⇒ match x with
                     | (existT _ m p) ⇒
                       existT _ m (salg_emp m) end);
  eauto using plift_pcancel, salg_pcancel, plift_max, salg_strip_max,
              plift_distr, salg_strip_plus; ins; desf; ins; desf; ins;
  rewrite <- ?eq_rect_eq, ?salg_plus_emp_r in *; desf.

  assert (None = Some (o1 n)); desf.
  rewrite <- EQ1, <- EQ2; eapply olift_pcancel with
    (u := fun x ⇒ match x with
                     | (existT _ m p) ⇒
                       existT _ m (salg_emp m) end);
  eauto using plift_pcancel, salg_pcancel, plift_max, salg_strip_max,
              plift_distr, salg_strip_plus; ins; desf; ins; desf; ins;
  rewrite <- ?eq_rect_eq, ?salg_plus_emp_r in *; desf.
Qed.

Arguments gres_plusA [x y xy] P1 [z xyz] P2.
Arguments gres_plusA2 [x y xy] P1 [z] P2.
Arguments gres_eq_empD [x y] P.
Arguments gres_pcancel [g g1 g2 gg] P1 P2.

Definition gres_plus_total g1 g2 :=
  match gres_plus g1 g2 with
    | Some g ⇒ g
    | None ⇒ gres_emp
  end.

Lemma gres_plus_gres_plus_total_not_none g1 g2 g3:
  gres_plus g2 g3 ≠ None →
  gres_plus g1 (gres_plus_total g2 g3) ≠ None
  → gres_plus g1 g2 ≠ None.
Proof.
  ins; unfold gres_plus_total in *; desf.
  destruct (gres_plus g1 g) eqn:X; try done.
  rewrite gres_plusC in *; generalize (gres_plusA Heq X).
  ins; desf; congruence.
Qed.

Lemma gres_plus_gres_plus_totalA g1 g2 g3: gres_plus g1 g2 ≠ None → gres_plus g2 g3 ≠ None
                    → gres_plus g1 (gres_plus_total g2 g3) = gres_plus (gres_plus_total g1 g2) g3.
Proof.
  ins; unfold gres_plus_total; desf.
  destruct (gres_plus g1 g) eqn:X; destruct (gres_plus g0 g3) eqn:Y; try done;
  try generalize (gres_plusA Heq X); try generalize (gres_plusA Heq0 Y);
  try generalize (gres_plusA2 Heq X); try generalize (gres_plusA2 Heq0 Y); ins; desf.
Qed.

Lemma gres_plus_totalA g1 g2 g3:
  gres_plus g1 g2 ≠ None → gres_plus g2 g3 ≠ None → gres_plus g1 (gres_plus_total g2 g3) ≠ None
  → gres_plus_total (gres_plus_total g1 g2) g3 = gres_plus_total g1 (gres_plus_total g2 g3).
Proof.
  ins.
  assert (gres_plus (gres_plus_total g1 g2) g3 ≠ None) by (by rewrite <- gres_plus_gres_plus_totalA).
  unfold gres_plus_total in *; desf.
  rewrite gres_plusC in Heq0; generalize (gres_plusA Heq1 Heq), (gres_plusA Heq2 Heq0); ins; desf.
  rewrite gres_plusC in Heq0; congruence.
Qed.

Lemma gres_plus_totalC: ∀ g1 g2, gres_plus_total g1 g2 = gres_plus_total g2 g1.
Proof.
  unfold gres_plus_total; ins; desf; rewrite (gres_plusC g1) in *; congruence.
Qed.

Lemma gres_plus_total_emp_r: ∀ g, gres_plus_total g gres_emp = g.
Proof.
  by ins; unfold gres_plus_total; rewrite gres_plus_emp_r.
Qed.

Lemma gres_plus_total_emp_l: ∀ g, gres_plus_total gres_emp g = g.
Proof.
  by ins; rewrite gres_plus_totalC, gres_plus_total_emp_r.
Qed.