Require Import Vbase Classical.

Set Implicit Arguments.

Structure Permission :=
  { perm :> Type;
    Pzero : perm;
    Pfull : perm;
    Pundef : perm;
    Pfull_is_not_Pzero : Pfull ≠ Pzero;
    Pfull_is_not_Pundef : Pfull ≠ Pundef;
    permission_plus : perm → perm → perm;
    permission_plusC :
      ∀ x y, permission_plus x y = permission_plus y x;
    permission_plusA :
      ∀ x y z, permission_plus (permission_plus x y) z = permission_plus x (permission_plus y z);
    permission_plus_cancel :
      ∀ x x' y, permission_plus x y ≠ Pundef → permission_plus x y = permission_plus x' y → x = x';
    permission_plus_zero_r :
      ∀ x, permission_plus x Pzero = x;
    permission_plus_undef_r :
      ∀ x, permission_plus x Pundef = Pundef;
    permission_plus_eq_zero :
      ∀ x y, permission_plus x y = Pzero → x = Pzero ∧ y = Pzero;
    nonextendable_full_permission:
      ∀ x, permission_plus Pfull x ≠ Pundef → x = Pzero;
    permission_leq : rel perm;
    permission_leq_refl : reflexive permission_leq;
    permission_leq_as : antisymmetric permission_leq;
    permission_leq_trans : transitive permission_leq;
    permission_leq_total : total permission_leq
  }.

Infix "##" := (@permission_plus _) (at level 35, right associativity).
Infix "<#" := (@permission_leq _) (at level 36, right associativity).

Lemma permission_plusAC (PS: Permission) (x y z: PS): y ## x ## z = x ## y ## z.
Proof.
  by rewrite permission_plusC, permission_plusA, (permission_plusC _ z).
Qed.

Lemma permission_plus_zero_l PS x: (Pzero PS) ## x = x.
Proof.
  by rewrite permission_plusC; apply permission_plus_zero_r.
Qed.

Lemma permission_plus_undef_l PS x: (Pundef PS) ## x = (Pundef PS).
Proof.
  by rewrite permission_plusC; apply permission_plus_undef_r.
Qed.

Lemma Pzero_is_not_Pundef PS: Pzero PS ≠ Pundef PS.
Proof.
  intro.
  assert (Z := permission_plus_zero_r _ (Pfull PS)).
  assert (U := permission_plus_undef_r _ (Pfull PS)).
  rewrite H in Z.
  eapply (Pfull_is_not_Pzero PS).
  congruence.
Qed.

Lemma permission_plus_not_zero (PS: Permission) (x y: PS) :
  x ## y ≠ Pzero PS → x ≠ Pzero PS ∨ y ≠ Pzero PS.
Proof.
  ins.
  apply NNPP; intro CONTRA.
  apply not_or_and in CONTRA; desf.
  apply NNPP in CONTRA; desf.
  rewrite permission_plus_zero_l in H.
  done.
Qed.

Ltac pplus_eq_zero :=
  repeat (match goal with H : _ ## _ = Pzero _ |- _ ⇒ apply permission_plus_eq_zero in H; desc; try subst end).

Ltac pplus_zero_simpl :=
  repeat first [rewrite permission_plus_zero_r in × | rewrite permission_plus_zero_l in *].