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.

Arguments QP : clear implicits.

Lemma QP_equal a a' UNIT UNIT' QRED QRED':
  a = a' → QP a UNIT QRED = QP a' UNIT' QRED'.
Proof.
  ins; revert UNIT UNIT' QRED QRED'; desf.
  ins; f_equal; apply proof_irrelevance.
Qed.

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
  |}.
Next Obligation.
  destruct x, y; ins; desf; try done.
  by apply QP_equal, Qred_complete, Qplus_comm.
  by destruct n; rewrite Qplus_comm.
  by destruct n; rewrite Qplus_comm.
Qed.
Next Obligation.
  destruct x, y, z; ins; desf; ins; desf.
  × apply QP_equal.
    by apply Qred_complete; rewrite !Qred_correct, Qplus_assoc.
  × destruct n; rewrite !Qred_correct, Qplus_assoc in *; eauto.
  × destruct n; rewrite !Qred_correct, Qplus_assoc in *; eauto.
  × destruct n; rewrite !Qred_correct, ?Qplus_assoc in ×.
    split; desf.
    by apply nonnegative_sum.
    apply Qplus_le_compat with (x := - f) (y := 0) in a2.
    by rewrite !Qplus_assoc, Qplus_opp_l, !Qplus_0_l in a2.
    by rewrite <- Qopp_zero; apply Qopp_le_compat.
  × destruct n; rewrite !Qred_correct, Qplus_assoc in ×.
    split; desf.
    by apply nonnegative_sum.
    apply Qplus_le_compat with (z := - f1) (t := 0) in a1.
    by rewrite <- !Qplus_assoc, Qplus_opp_r, !Qplus_0_r in a1.
    by rewrite <- Qopp_zero; apply Qopp_le_compat.
Qed.
Next Obligation.
  destruct x, x', y; ins; desf.
  apply QP_equal.
  rewrite QRED, QRED0.
  eapply Qred_complete, Qplus_inj_r.
  eby apply Qeq_weaken in H0; rewrite !Qred_correct in H0.
Qed.
Next Obligation.
  destruct x; ins; desf.
  by apply QP_equal; rewrite QRED at 2; apply Qred_complete; rewrite Qplus_0_r.
  by destruct n; rewrite Qred_correct, Qplus_0_r; eauto.
Qed.
Next Obligation. by destruct x. Qed.
Next Obligation.
  destruct x, y; ins; desf.
  apply Qeq_weaken in H; rewrite Qred_correct in H.
  exploit nonnegative_sum_eq_zero; try exact H; ins; desf.
  apply Qred_complete in x0; apply Qred_complete in x1; rewrite Qred_zero, <- QRED, <- QRED0 in ×.
  by split; apply QP_equal; desf.
Qed.
Next Obligation.
  destruct x; ins; desf.
  apply QP_equal.
  rewrite QRED, <- Qred_zero; apply Qred_complete.
  apply Qle_antisym; try done.
  clear H; rewrite Qred_correct in ×.
  eapply Qplus_le_r; desf.
  eby rewrite Qplus_0_r.
Qed.
Next Obligation.
  red. destruct x; ins.
  unfold mydec; desf.
  destruct n; apply Qle_refl.
Qed.
Next Obligation.
  red. destruct x, y; ins.
  apply QP_equal.
  unfold mydec in *; desf.
  by rewrite QRED, QRED0; apply Qred_complete, Qle_antisym.
Qed.
Next Obligation.
  red. destruct x, y, z; ins.
  unfold mydec in *; desf.
  eby destruct n; eapply Qle_trans.
Qed.
Next Obligation.
  red. destruct x, y; ins.
  unfold mydec; desf.
  eby exfalso; eapply Qlt_irrefl, Qlt_trans; apply Qnot_le_lt.
Qed.