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

Ghost monoid


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 GESome (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
  |}.

This page has been generated by coqdoc