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

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

Generic pointwise lifting of a partial binary operator to a function, where the lifted operator is defined on two functions if and only if it is defined on all elements of those functions.

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 PFSome (proj1_sig (lift_plus_helper (fun xp (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.

Generic lifting of a partial binary operator to operate on arguments of option type, making None be the unit element of the lifted operator.

Section olift.

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

  Definition olift_unary ao :=
    match ao with
      | NoneNone
      | Some aSome (op1 a)
    end.

  Definition olift_plus ao bo :=
    match ao, bo with
        None, boSome bo
      | Some a, NoneSome (Some a)
      | Some a, Some bmatch bop a b with
                            | Some vSome (Some v)
                            | NoneNone
                          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.

Generic lifting of a partial binary operator to operate on existential packages.

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

Some useful tactics for exploiting assumptions with lift_plus.

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.

Definition of separation algebras

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.

Lifting to functions of existential packages of separation algebras

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

Definition of ghost resources
Empty ghost resource

Program Definition gres_emp :=
  {| gres_fun := fun _ None |}.

Singleton ghost resource

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

Ghost resource composition

Program Definition gres_plus (g1 g2 : ghost_resource) :=
  match lift_plus (olift_plus (plift_plus _ salg_plus)) g1 g2 with
    | Some gSome {| gres_fun := g |}
    | NoneNone
  end.

Ghost resource striping

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

ACIK properties of ghost resource composition

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.


A total version of gres_plus, coinciding with gres_plus whenever gres_plus is defined.

This page has been generated by coqdoc