Require Import Relations Classical ClassicalDescription.
Require Import Vbase extralib.
Require Import permission fslassn.
Require Import QArith helpers_rationals.

Set Implicit Arguments.

Obligation Tactic := try done.

Inductive Qperm :=
  | QP (f : Q) (UNIT: 0 ≤ f ≤ 1) (QRED: f = Qred f)
  | QPundef.


Lemma QP_equal a a' UNIT UNIT' QRED QRED':
  a = a' → QP a UNIT QRED = QP a' UNIT' QRED'.

Definition QPplus f g :=
  match f, g return Qperm with
    | QPundef, _ ⇒ QPundef
    | _, QPundef ⇒ QPundef
    | QP f' _ _, QP g' _ _ ⇒ match excluded_middle_informative (0 ≤ Qred (f' + g') ≤ 1) with
                             | left U ⇒ QP (Qred (f' + g')) U (eq_sym (Qred_Qred (f' + g')))
                             | right _ ⇒ QPundef
                           end
  end.

Definition QPleq f g : bool :=
  match f, g with
    | QPundef, _ ⇒ true
    | QP _ _ _, QPundef ⇒ false
    | QP f' _ _, QP g' _ _ ⇒ mydec (f' ≤ g')
  end.

Program Definition Fractional_Permissions :=
  {| perm := Qperm;
     Pzero := QP 0 _ _;
     Pfull := QP 1 _ _;
     Pundef := QPundef;
     permission_plus := QPplus;
     permission_leq := QPleq
  |}.