Require Import Vbase Relations ClassicalDescription ClassicalChoice.

Set Implicit Arguments.

Inductive fraction :=
  | pe_full
  | pe_half.

Definition fraction_plus x y :=
  match x, y with
    | pe_half, pe_half ⇒ Some pe_full
    | _, _ ⇒ None
  end.

Definition fraction_le x y :=
  x = y ∨ ∃ rem, fraction_plus x rem = Some y.

Lemma fraction_plusC x y : fraction_plus x y = fraction_plus y x.
Proof.
  destruct x, y; desf.
Qed.

Lemma fraction_plusA :
  ∀ x y xy (P1: fraction_plus x y = Some xy) z xyz
                (P2: fraction_plus xy z = Some xyz),
    ∃ yz, fraction_plus y z = Some yz ∧ fraction_plus x yz = Some xyz.
Proof.
  unfold fraction_plus; ins; desf.
Qed.

Lemma fraction_plus_full_l x : fraction_plus pe_full x = None.
Proof.
  done.
Qed.

Lemma fraction_plus_full_r x : fraction_plus x pe_full = None.
Proof.
  rewrite fraction_plusC; apply fraction_plus_full_l.
Qed.

Lemma fraction_plusK1 x y : fraction_plus x y = Some x → False.
Proof.
  destruct x, y; desf.
Qed.

Lemma fraction_plusK2 x y : fraction_plus x y = Some y → False.
Proof.
  by rewrite fraction_plusC; apply fraction_plusK1.
Qed.

Lemma fraction_plusK x y z w :
  fraction_plus x y = Some w →
  fraction_plus x z = Some w →
  y = z.
Proof.
  destruct x; ins; desf.
Qed.

Lemma fraction_le_refl x :
  fraction_le x x.
Proof.
  vauto.
Qed.

Lemma fraction_le_trans x y z :
  fraction_le x y →
  fraction_le y z →
  fraction_le x z.
Proof.
  unfold fraction_le; ins; desf; eauto.
  right; edestruct fraction_plusA; desf; try (eby eexists); eauto.
Qed.

Lemma fraction_le_antisym x y :
  fraction_le x y →
  fraction_le y x →
  x = y.
Proof.
  unfold fraction_le; ins; desf.
  exfalso; eapply fraction_plusA in H0; desf; eauto using fraction_plusK1.
Qed.

Lemma fraction_le1 x y z :
  fraction_plus x y = Some z →
  fraction_le x z.
Proof.
  vauto.
Qed.

Lemma fraction_le2 x y z :
  fraction_plus x y = Some z →
  fraction_le y z.
Proof.
  by rewrite fraction_plusC; apply fraction_le1.
Qed.

Lemma fraction_le_mon x x' y y' z z' :
  fraction_le x x' →
  fraction_le y y' →
  fraction_plus x y = Some z →
  fraction_plus x' y' = Some z' →
  fraction_le z z'.
Proof.
  unfold fraction_le; ins; desf; eauto; right.

  rewrite fraction_plusC in H; assert (K:=fraction_plusA _ _ H _ H2); desf.
  rewrite fraction_plusC in K0; eauto.

  rewrite fraction_plusC in H0, H2; assert (K:=fraction_plusA _ _ H0 _ H2); desf.
  rewrite fraction_plusC in K, K0; desf; eauto.

  rewrite fraction_plusC in H0, H2; assert (K:=fraction_plusA _ _ H0 _ H2); desf.
  rewrite fraction_plusC in K, K0; desf; eauto.
  rewrite fraction_plusC in H; assert (L:=fraction_plusA _ _ H _ K); desf.
  rewrite fraction_plusC in L0; assert (M:=fraction_plusA _ _ L0 _ K0); desf; eauto.
Qed.

Lemma fraction_le_none1 x x' y :
  fraction_plus x y = None →
  fraction_le x x' →
  fraction_plus x' y = None.
Proof.
  unfold fraction_le; ins; desf.
  case_eq (fraction_plus x' y) as M; exfalso.
  rewrite fraction_plusC in H0.
  eapply fraction_plusA in M; eauto; desf.
Qed.

Lemma fraction_le_none2 x x' y :
  fraction_plus y x = None →
  fraction_le x x' →
  fraction_plus y x' = None.
Proof.
  ins; rewrite fraction_plusC in *; eauto using fraction_le_none1.
Qed.

Lemma fraction_le_full x :
  fraction_le pe_full x ↔ x = pe_full.
Proof.
  unfold fraction_le; split; ins; desf; eauto.
Qed.

Global Opaque fraction_plus fraction_le.