Require Import Vbase Classical.

Set Implicit Arguments.

The permission structure

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.

Lemma permission_plus_zero_l PS x: (Pzero PS) ## x = x.

Lemma permission_plus_undef_l PS x: (Pundef PS) ## x = (Pundef PS).

Lemma Pzero_is_not_Pundef PS: Pzero PS Pundef PS.

Lemma permission_plus_not_zero (PS: Permission) (x y: PS) :
  x ## y Pzero PS x Pzero PS y Pzero PS.

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 *].


This page has been generated by coqdoc