Module NumC

Require Import Ring.
Require Import ZArith.
Require Import QArith.
Require Import Qcanon.
Require Import Qround.
Require CoqAddOn.
Require List.
Require String.
Require Import OptionMonad.

Inductive trivialMulDiscr :=
  IsZero | IsUnit | IsOppUnit | Other.

Module Type BasicNumSig.

  Parameter t: Set.

  Parameter z: t.
  Parameter u: t.

  Parameter add: t -> t -> t.
  Parameter mul: t -> t -> t.
  Parameter opp: t -> t.
  Parameter sub: t -> t -> t.

  Parameter Ring: ring_theory z u add mul sub opp eq.

  Parameter ZNotU: z <> u.

  Parameter Le: t -> t -> Prop.
  Parameter Lt: t -> t -> Prop.

  Parameter LtNotLe: forall n1 n2 : t, Lt n1 n2 <-> ~ Le n2 n1.
  Parameter LeNotLt: forall n1 n2 : t, Le n1 n2 <-> ~ Lt n2 n1.
  Parameter LtLe: forall n1 n2: t, Lt n1 n2 -> Le n1 n2.

  Parameter eqDec: forall n1 n2: t, {n1 = n2} + {n1 <> n2}.
  Parameter ltLeDec: forall n1 n2: t, {Lt n1 n2} + {Le n2 n1}.
  Parameter dec: forall n1 n2: t, {Lt n1 n2} + {Lt n2 n1} + {n1 = n2}.

  Parameter LeRefl: forall n1: t, Le n1 n1.
  Parameter LeLeEq: forall n1 n2: t, Le n1 n2 /\ Le n2 n1 <-> n1 = n2.

  Parameter LeTrans: forall n1 n2 n3: t, Le n1 n2 -> Le n2 n3 -> Le n1 n3.
  Parameter LtTrans: forall n1 n2 n3: t, Lt n1 n2 -> Lt n2 n3 -> Lt n1 n3.
  Parameter LeLtTrans: forall n1 n2 n3: t, Le n1 n2 -> Lt n2 n3 -> Lt n1 n3.
  Parameter LtLeTrans: forall n1 n2 n3: t, Lt n1 n2 -> Le n2 n3 -> Lt n1 n3.

  Parameter isZero: forall n: t, {n = z} + {n <> z}.

  Parameter mulDiscr: t -> trivialMulDiscr.
  Parameter mulDiscr_correct: forall n,
    match (mulDiscr n) with
    | IsZero => n=z
    | IsUnit => n=u
    | IsOppUnit => n=opp u
    | _ => True
    end.


  Parameter AddLeLe: forall n1 n2 n3 n4: t,
                   Le n1 n2 -> Le n3 n4 -> Le (add n1 n3) (add n2 n4).

  Parameter AddLtLt: forall n1 n2 n3 n4: t,
                   Lt n1 n2 -> Lt n3 n4 -> Lt (add n1 n3) (add n2 n4).


  Parameter AddLeLt: forall n1 n2 n3 n4: t,
                   Le n1 n2 -> Lt n3 n4 -> Lt (add n1 n3) (add n2 n4).

  Parameter AddLtLe: forall n1 n2 n3 n4: t,
                   Lt n1 n2 -> Le n3 n4 -> Lt (add n1 n3) (add n2 n4).


  Parameter MulZL: forall n: t, mul z n = z.

  Parameter MulLe1: forall n1 n2 n3: t,
                 Le z n1 -> Le n2 n3 -> Le (mul n1 n2) (mul n1 n3).

  Parameter MulLe2: forall n1 n2 n3: t,
                 Lt z n1 -> Le (mul n1 n2) (mul n1 n3) -> Le n2 n3.

  Parameter MulLt: forall n1 n2 n3: t,
                 Lt z n1 -> (Lt n2 n3 <-> Lt (mul n1 n2) (mul n1 n3)).

  Parameter OppZ: opp z = z.
  Parameter OppOpp: forall n: t, opp (opp n) = n.
  Parameter OppLt: forall n1 n2: t, Lt n1 n2 <-> Lt (opp n2) (opp n1).
  Parameter OppLe: forall n1 n2: t, Le n1 n2 <-> Le (opp n2) (opp n1).

  Parameter MulUR: forall n1: t, mul n1 u = n1.
  Parameter MulAssoc: forall n1 n2 n3: t, mul n1 (mul n2 n3) = mul (mul n1 n2) n3.
  Parameter AddOppDistr: forall n1 n2: t, add (opp n1) (opp n2) = opp (add n1 n2).
  Parameter MulAddDistr: forall n1 n2 n3: t, mul (add n1 n2) n3 = add (mul n1 n3) (mul n2 n3).
  Parameter MulOppDistrR: forall n1 n2: t, mul n1 (opp n2) = opp (mul n1 n2).
  Parameter MulOppDistrL: forall n1 n2: t, mul (opp n1) n2 = opp (mul n1 n2).
  Parameter MulComm: forall n1 n2: t, mul n1 n2 = mul n2 n1.

  Parameter pr: t -> String.string.

  Parameter prRaw: t -> String.string.

  Hint Rewrite <- OppLt OppLe LeNotLt LtNotLe: num.
  Hint Resolve AddLeLe AddLeLt AddLtLt AddLtLe LeRefl: num.

End BasicNumSig.

Inductive cmpT: Set
  := EqT | LeT | LtT.

Inductive cmpG: Set
  := Eq | Le | Lt | Neq.

Definition cmpT2G (c: cmpT): cmpG :=
  match c with
  | EqT => Eq
  | LeT => Le
  | LtT => Lt
  end.

Global Coercion cmpT2G: cmpT >-> cmpG.


Definition cmpG2T (cmp:cmpG): option cmpT :=
   match cmp with
   | Eq => Some EqT
   | Le => Some LeT
   | Lt => Some LtT
   | Neq => None
   end.

Module CmpTheory(N: BasicNumSig).

  Add Ring NRing: N.Ring.

  Definition cmpDenote (cmp: cmpG): N.t -> N.t -> Prop
    := match cmp with
       | Eq => eq
       | Le => N.Le
       | Lt => N.Lt
       | Neq => fun x y => x <> y
       end.
 
  Lemma cmp_add_preserve {cmp n1 n2 n3}:
    cmpDenote cmp n1 n2 -> cmpDenote cmp (N.add n1 n3) (N.add n2 n3).
  Local Hint Resolve cmp_add_preserve: num.
 
  Lemma cmp_zero_left {cmp n1 n2}:
    cmpDenote cmp n1 n2 ->
      cmpDenote cmp N.z (N.add n2 (N.opp n1)).
  Local Hint Resolve cmp_zero_left: num.

  Lemma cmp_transfo {cmp n1 n2 n3 n4}:
    cmpDenote cmp n1 n2 ->
     n4 = (N.add (N.add n2 (N.opp n1)) n3)->
     cmpDenote cmp n3 n4.
  
  Ltac cmp_simplify := eapply cmp_transfo; [ eauto | try ring ].

  Lemma cmpG2T_correct cmp:
    WHEN c <- cmpG2T cmp THEN
    forall v1 v2, cmpDenote c v1 v2 <-> cmpDenote cmp v1 v2.

  Lemma cmpDenote_dec (cmp: cmpG) (n1 n2: N.t): {cmpDenote cmp n1 n2} + {~ cmpDenote cmp n1 n2}.
    refine (match cmp return {cmpDenote cmp n1 n2} + {~ cmpDenote cmp n1 n2} with
              | Eq => N.eqDec n1 n2
              | Le =>
                match N.ltLeDec n2 n1 with
                  | left pf => right (proj1 (N.LtNotLe n2 n1) pf)
                  | right pf => left pf
                end
              | Lt =>
                match N.ltLeDec n1 n2 with
                  | left pf => left pf
                  | right pf => right (proj1 (N.LeNotLt n2 n1) pf)
                end
              | Neq =>
                match N.eqDec n1 n2 with
                  | left pf => right (fun H => H pf)
                  | right pf => left pf
                end
            end).
  Qed.