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

Inductive Qtoken :=
  | TokPlus (f: Q) (POS: f ≥ 0) (QRED: f = Qred f)
  | TokMinus (f: Q) (POS: f ≥ 0) (QRED: f = Qred f).


Lemma Tok_equal (Tok: ∀ f : Q, 0 ≤ f → f = Qred f → Qtoken) a a' POS POS' QRED QRED':
  a = a' → Tok a POS QRED = Tok a' POS' QRED'.

Program Definition Tok_plus t1 t2 :=
  match t1, t2 return option Qtoken with
    | TokPlus f _ _, TokPlus g _ _ ⇒ Some (TokPlus (Qred (f + g)) _ (eq_sym (Qred_Qred (f + g))))
    | TokPlus f _ _, TokMinus g _ _
    | TokMinus g _ _, TokPlus f _ _ ⇒ match excluded_middle_informative (Qred (g - f) ≥ 0)
                                       return option Qtoken with
                                       | left GE ⇒ Some (TokMinus (Qred (g - f)) GE (eq_sym (Qred_Qred (g - f))))
                                       | right _ ⇒ None
                                       end
    | _,_ ⇒ None
  end.

Definition Tok_leq t1 t2 : bool :=
  match t1, t2 with
    | TokMinus _ _ _, TokPlus _ _ _ ⇒ true
    | TokMinus f _ _, TokMinus g _ _
    | TokPlus f _ _, TokPlus g _ _ ⇒ mydec (f ≤ g)
    | _, _ ⇒ false
  end.

Program Definition TokenMonoid :=
  {| salg := Qtoken;
     salg_emp := TokPlus 0 _ _;
     salg_plus := Tok_plus;
     salg_strip := (fun _ ⇒ TokPlus 0 _ _);
     salg_leq := Tok_leq
  |}.