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) }.

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).

Lemma lift_plus_noneD A B p (f g : A → B) :
  lift_plus p f g = None ↔ ∃ x, p (f x) (g x) = None.

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.

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.

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.

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.

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).

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.

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.

  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.

  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.

  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).

  Lemma olift_idemp :
    ∀ (IDEM : ∀ x, op1 (op1 x) = op1 x) x,
      olift_unary (olift_unary x) = olift_unary x.

  Lemma olift_pidemp :
    ∀ (IDEM : ∀ x, bop x (op1 x) = Some x) x,
      olift_plus x (olift_unary x) = Some x.

  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.

  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.

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.

  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.

  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.

  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).

  Lemma plift_idemp :
    ∀ (IDEM : ∀ m (x : f m), op1 (op1 x) = op1 x) x,
      plift_unary (plift_unary x) = plift_unary x.

  Lemma plift_pidemp :
    ∀ (IDEM : ∀ m (x : f m), bop x (op1 x) = Some x) x,
      plift_plus x (plift_unary x) = Some x.

  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.

  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.

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.

Lemma salg_plus_emp_r :
  ∀ m x, salg_plus m x (salg_emp m) = Some x.

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.

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.

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 |}.

Program Definition gres_one (n : nat) g :=
  {| gres_fun := fun n' ⇒ if (n==n')%bool then g else None |}.

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.

Program Definition gres_strip (g : ghost_resource) :=
  {| gres_fun := fun l ⇒ olift_unary (plift_unary _ salg_strip) (g l) |}.

Lemma gres_ext f g : (∀ n, gres_fun f n = gres_fun g n) → f = g.

Lemma gres_plusC x y : gres_plus x y = gres_plus y x.

Lemma gres_plusI x : gres_plus gres_emp x = Some x.

Lemma gres_plus_emp_r x : gres_plus x gres_emp = Some x.

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.

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.

Lemma gres_eq_empD x y : gres_plus x y = Some gres_emp → x = gres_emp.

Lemma gres_strip_emp : gres_strip gres_emp = gres_emp.

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).

Lemma gres_strip_idemp x : gres_strip (gres_strip x) = gres_strip x.

Lemma gres_plus_strip_idemp x : gres_plus x (gres_strip x) = Some x.

Lemma gres_strip_max x y xy z :
  gres_plus x y = Some xy →
  gres_plus xy z = Some x →
  gres_strip y = y.

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.

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.

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.

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).

Lemma gres_plus_totalC: ∀ g1 g2, gres_plus_total g1 g2 = gres_plus_total g2 g1.

Lemma gres_plus_total_emp_r: ∀ g, gres_plus_total g gres_emp = g.

Lemma gres_plus_total_emp_l: ∀ g, gres_plus_total gres_emp g = g.