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).

Arguments TokPlus: clear implicits.
Arguments TokMinus: clear implicits.

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'.
Proof.
  ins; revert POS POS' QRED QRED'; desf.
  ins; f_equal; apply proof_irrelevance.
Qed.

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.
Next Obligation. by ins; rewrite Qred_correct; apply nonnegative_sum. Qed.

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
  |}.
Next Obligation.
  destruct x, y; ins; desf.
  by f_equal; apply Tok_equal, Qplus_comm_red.
Qed.
Next Obligation.
  ins; desf; desf.
  × f_equal; apply Tok_equal.
    rewrite QRED; apply Qred_complete.
    rewrite Qplus_0_l; congruence.
  × f_equal; apply Tok_equal.
    rewrite QRED; apply Qred_complete.
    unfold Qminus; rewrite Qopp_zero, Qplus_0_r; congruence.
  × destruct n; unfold Qminus; rewrite Qopp_zero, Qplus_0_r; congruence.
Qed.
Next Obligation.
  assert (F: ∀ a b c, a + b + c == a + c + b).
    by ins; rewrite <- Qplus_assoc, (Qplus_comm b), Qplus_assoc.
  assert (G: ∀ a b c, 0 ≤ c → 0 ≤ a + - c + - b → 0 ≤ a + - b).
  {
    ins. specialize (Qplus_le_compat _ _ _ _ H H0).
    by rewrite (Qplus_comm a), !Qplus_assoc, Qplus_opp_r, !Qplus_0_l.
  }
  ins; destruct x, y, z; ins; desf; eexists; split; try edone; ins; desf; f_equal;
  first [ apply Tok_equal | exfalso ]; try apply Qred_complete;
  rewrite ?Qred_correct in *; unfold Qminus in *; rewrite ?Qopp_plus, ?Qplus_assoc in *; eauto 3; try edone.
  all: try by exfalso; eauto 3.
  all: by rewrite F in n.
  Grab Existential Variables. all: done.
Qed.
Next Obligation.
  ins; destruct x, y, z; ins; desf;
    first [by left | right; ins; desf; eexists; split; try edone; desf; exfalso].
  by clear - q0 n; by unfold Qminus in *; rewrite !Qred_correct, (Qplus_comm f), Qopp_plus, Qplus_assoc in ×.
  by clear - q1 n; unfold Qminus in *; rewrite !Qred_correct, <- Qplus_assoc, (Qplus_comm (-f)) in ×.
  by clear - q0 n; unfold Qminus in *; rewrite !Qred_correct, Qopp_plus, Qplus_assoc in ×.
Qed.
Next Obligation.
  ins; destruct g, g'; ins; desf.
  apply Tok_equal.
  apply Qeq_weaken in H; rewrite Qred_correct in H.
  apply nonnegative_sum_eq_zero in H; desf.
  rewrite QRED, <- Qred_zero.
  by apply Qred_complete.
Qed.
Next Obligation.
  by ins; f_equal; apply Tok_equal.
Qed.
Next Obligation.
  ins; destruct x; ins; desf.
  × f_equal; apply Tok_equal.
    by rewrite QRED; apply Qred_complete; rewrite Qred_correct, Qplus_0_r.
  × f_equal; apply Tok_equal.
    by rewrite QRED; apply Qred_complete; unfold Qminus; rewrite Qred_correct, Qplus_0_r.
  × by destruct n; unfold Qminus; rewrite Qred_correct, Qopp_zero, Qplus_0_r.
Qed.
Next Obligation.
  ins; destruct x, y, z; ins; desf; ins; desf; apply Tok_equal.
  × apply Qeq_weaken in H0; rewrite !Qred_correct in H0.
    rewrite <- (Qplus_0_r f) in H0 at 2.
    rewrite <- Qplus_assoc, Qplus_inj_l in H0.
    apply nonnegative_sum_eq_zero in H0; desf.
    rewrite QRED0, <- Qred_zero.
    by apply Qred_complete.
  × apply Qeq_weaken in H0; rewrite !Qred_correct in H0.
    unfold Qminus in H0; rewrite <- (Qplus_0_r f) in H0 at 2.
    rewrite <- Qplus_assoc, Qplus_inj_l, <- Qopp_plus, Qopp_equal, Qopp_opp, Qopp_zero in H0.
    apply nonnegative_sum_eq_zero in H0; desf.
    rewrite QRED0, <- Qred_zero.
    by apply Qred_complete.
Qed.
Next Obligation.
  desf; ins; desf; f_equal; first [apply Tok_equal | exfalso];
    try by (rewrite <- H0 in H; destruct g; ins; desf).
  × rewrite <- H0 in H; destruct g; ins; desf.
    + apply Qeq_weaken in H; rewrite !Qred_correct, Qplus_inj_l in H.
      by apply Qred_complete; rewrite !Qplus_0_l.
    + apply Qeq_weaken in H; unfold Qminus in H; rewrite !Qred_correct, Qplus_inj_l, <- Qopp_equal in H.
      by apply Qred_complete; rewrite !Qplus_0_l.
  × rewrite <- H0 in H; destruct g; ins; desf.
    apply Qeq_weaken in H; unfold Qminus in H; rewrite !Qred_correct, Qplus_inj_r in H.
    by unfold Qminus; apply Qred_complete; rewrite !Qplus_0_r.
  × by destruct n; unfold Qminus; rewrite Qred_correct, Qopp_zero, Qplus_0_r.
  × by destruct n; unfold Qminus; rewrite Qred_correct, Qopp_zero, Qplus_0_r.
Qed.
Next Obligation.
  destruct x; ins;
  unfold mydec; desf;
  destruct n; apply Qle_refl.
Qed.
Next Obligation.
  destruct x, y; ins;
  apply Tok_equal; unfold mydec in *; desf;
  by rewrite QRED, QRED0; apply Qred_complete, Qle_antisym.
Qed.
Next Obligation.
  destruct x, y, z; ins; unfold mydec in *; desf;
  eby destruct n; eapply Qle_trans.
Qed.
Next Obligation.
  by destruct x, y; ins; unfold mydec; desf; eauto;
     apply Qnot_le_lt in n ; apply Qnot_le_lt in n0;
     exploit Qlt_irrefl; ins; eauto using Qlt_trans.
Qed.