Module Itv


Require String.
Require Import NumC.
Require Import DomainInterfaces.

Module Type AffItvSig (N: NumSig) <: ItvSig N.

  Parameter t: Set.

  Parameter sat: t -> N.t -> Prop.

Build a singleton interval
  Definition Mk1Spec (n: N.t) (i: t): Prop
    := forall n': N.t, n = n' <-> sat i n'.

  Parameter mk1Dep: forall n: N.t, {i: t | Mk1Spec n i}.
  Parameter mk1: N.t -> t.
  Parameter Mk1_correct: forall n: N.t, Mk1Spec n (mk1 n).

Sum of two intervals
  Definition AddSpec (i1 i2 i: t): Prop
    := forall n1 n2: N.t, sat i1 n1 /\ sat i2 n2 -> sat i (N.add n1 n2).

  Parameter addDep: forall i1 i2: t, {i: t | AddSpec i1 i2 i}.
  Parameter add: t -> t -> t.
  Parameter Add_correct: forall i1 i2: t, AddSpec i1 i2 (add i1 i2).

Opposite of an interval
  Definition OppSpec (i1 i2: t): Prop
    := forall n: N.t, sat i1 n <-> sat i2 (N.opp n).

  Parameter oppDep: forall i0: t, {i: t | OppSpec i0 i}.
  Parameter opp: t -> t.
  Parameter Opp_correct: forall i1: t, OppSpec i1 (opp i1).

Multiplication by a constant
  Definition MulcSpec (i1: t) (n: N.t) (i2: t): Prop
    := forall n': N.t, sat i1 n' -> sat i2 (N.mul n n').

  Parameter mulcDep: forall (i0: t) (n: N.t), {i: t | MulcSpec i0 n i}.
  Parameter mulc: t -> N.t -> t.
  Parameter Mulc_correct: forall (i1: t) (n: N.t), MulcSpec i1 n (mulc i1 n).

  Parameter pr: t -> String.string.

End AffItvSig.

Module StdItv (N: NumSig).
  Inductive bndT: Set
    :=
    | Infty: bndT
    | Open: N.t -> bndT
    | Closed: N.t -> bndT.

  Inductive BndOk: bndT -> bndT -> Prop
    :=
    | BndInftyLow: forall up: bndT, BndOk Infty up
    | BndInftyUp: forall low: bndT, BndOk low Infty
    | BndClosed: forall low up: N.t, N.Le low up -> BndOk (Closed low) (Closed up)
    | BndOpen: forall low up: N.t, N.Lt low up -> BndOk (Open low) (Open up)
    | BndOpenClosed: forall low up: N.t, N.Lt low up -> BndOk (Open low) (Closed up)
    | BndClosedOpen: forall low up: N.t, N.Lt low up -> BndOk (Closed low) (Open up).

  Inductive tInd: Set
    := Bot: tInd | NotBot: forall low up: bndT, BndOk low up -> tInd.

  Definition t: Set
    := tInd.

  Definition satLower (b: bndT) (x: N.t): Prop :=
    match b with
      | Infty => True
      | Open n => N.Lt n x
      | Closed n => N.Le n x
    end.

  Definition satUpper (b: bndT) (x: N.t): Prop :=
    match b with
      | Infty => True
      | Open n => N.Lt x n
      | Closed n => N.Le x n
    end.

  Definition sat (i: t) (x: N.t): Prop
    := match i with
         | Bot => False
         | NotBot low up _ => satLower low x /\ satUpper up x
       end.

  Definition MkSpec (l u: bndT) (i: t): Prop
    := forall x: N.t, satLower l x -> satUpper u x -> sat i x.

  Definition mk (l u: bndT): {i: t | MkSpec l u i}.
    refine (
        match l
              return {i: t | MkSpec l u i}
        with
          | Infty => exist _ (NotBot Infty u (BndInftyLow _)) _
          | Open n1 =>
            match u
                  return {i: t | MkSpec (Open n1) u i}
            with
              | Infty => exist _ (NotBot (Open n1) Infty (BndInftyUp _)) _
              | Open n2 =>
                match N.ltLeDec n1 n2 with
                  | left pf => exist _ (NotBot (Open n1) (Open n2) (BndOpen _ _ pf)) _
                  | right pf => exist _ Bot _
                end
              | Closed n2 =>
                match N.ltLeDec n1 n2 with
                  | left pf => exist _ (NotBot (Open n1) (Closed n2) (BndOpenClosed _ _ pf)) _
                  | right pf => exist _ Bot _
                end
            end
          | Closed n1 =>
            match u
                  return {i: t | MkSpec (Closed n1) u i}
            with
              | Infty => exist _ (NotBot (Closed n1) Infty (BndInftyUp _)) _
              | Open n2 =>
                match N.ltLeDec n1 n2 with
                  | left pf => exist _ (NotBot (Closed n1) (Open n2) (BndClosedOpen _ _ pf)) _
                  | right pf => exist _ Bot _
                end
              | Closed n2 =>
                match N.ltLeDec n2 n1 with
                  | left pf => exist _ Bot _
                  | right pf => exist _ (NotBot (Closed n1) (Closed n2) (BndClosed _ _ pf)) _
                end
            end
        end);
    unfold MkSpec;
    intros x hl hu;
    simpl;
    try intuition;
    unfold satLower in hl;
    unfold satUpper in hu;
    (apply N.LeNotLt in pf||apply N.LtNotLe in pf);
    try destruct pf;
    [apply N.LtTrans with (n2 := x)
    |apply N.LtLeTrans with (n2 := x)
    |apply N.LeLtTrans with (n2 := x)
    |apply N.LeTrans with (n2 := x)];
    assumption.
  Defined.

  Definition Mk1Spec (n: N.t) (i: t): Prop
    := forall n': N.t, n = n' <-> sat i n'.

  Definition mk1Dep (n: N.t): {i: t | Mk1Spec n i}.
    refine (exist _ (NotBot (Closed n) (Closed n) (BndClosed _ _ (N.LeRefl _))) _).
    unfold Mk1Spec.
    simpl.
    intro n'.
    split;
      apply N.LeLeEq.
  Defined.
  Definition mk1: N.t -> t
    := fun n => proj1_sig (mk1Dep n).

  Lemma Mk1_correct: forall n: N.t, Mk1Spec n (mk1 n).
  Proof (fun n => proj2_sig (mk1Dep n)).

  Definition AddSpec (i1 i2 i: t): Prop
    := forall n1 n2: N.t, sat i1 n1 /\ sat i2 n2 -> sat i (N.add n1 n2).

  Definition bndAdd (b1 b2: bndT): bndT
    := match b1 with
         | Infty => Infty
         | Open n1 =>
           match b2 with
             | Infty => Infty
             | Open n2 => Open (N.add n1 n2)
             | Closed n2 => Open (N.add n1 n2)
           end
         | Closed n1 =>
           match b2 with
             | Infty => Infty
             | Open n2 => Open (N.add n1 n2)
             | Closed n2 => Closed (N.add n1 n2)
           end
       end.

  Definition addDep (i1 i2: t): {i: t | AddSpec i1 i2 i}.
    refine (
        match i1
              return {i: t | AddSpec i1 i2 i}
        with
          | Bot => exist _ Bot _
          | NotBot l1 u1 pf1 =>
            match i2
                  return {i: t | AddSpec (NotBot l1 u1 pf1) i2 i}
            with
              | Bot => exist _ Bot _
              | NotBot l2 u2 pf2 =>
                let pfb: BndOk (bndAdd l1 l2) (bndAdd u1 u2) := _ in
                exist _ (NotBot (bndAdd l1 l2) (bndAdd u1 u2) pfb) _
            end
        end);
    match goal with
      | |- AddSpec _ _ Bot =>
        unfold AddSpec;
          intros n1 n2 [h1 h2];
          match goal with
            | hyp: sat Bot _ |- _ => destruct hyp
          end
      | |- AddSpec _ _ _ =>
        unfold AddSpec, bndAdd;
          intros n1 n2 [[h1 h2] [h3 h4]]
      | |- BndOk _ _ =>
        unfold bndAdd
      | _ => idtac
    end;
      destruct l1;
        destruct l2;
        destruct u1;
        destruct u2;
        simpl;
        repeat constructor;
        inversion pf1;
        inversion pf2;
        try simpl in h1, h2, h3, h4;
        match goal with
          | hyp1: N.Lt ?n1 ?n2, hyp2: N.Lt ?n3 ?n4
            |- N.Lt (N.add ?n1 ?n3) (N.add ?n2 ?n4)
            => apply N.AddLtLt; assumption
          | hyp1: N.Le ?n1 ?n2, hyp2: N.Lt ?n3 ?n4
            |- N.Lt (N.add ?n1 ?n3) (N.add ?n2 ?n4)
            => apply N.AddLeLt; assumption
          | hyp1: N.Lt ?n1 ?n2, hyp2: N.Le ?n3 ?n4
            |- N.Lt (N.add ?n1 ?n3) (N.add ?n2 ?n4)
            => apply N.AddLtLe; assumption
          | hyp1: N.Le ?n1 ?n2, hyp2: N.Le ?n3 ?n4
            |- N.Le (N.add ?n1 ?n3) (N.add ?n2 ?n4)
            => apply N.AddLeLe; assumption
          | _ => idtac
        end.
  Defined.
  Definition add: t -> t -> t
    := fun i1 i2 => proj1_sig (addDep i1 i2).

  Lemma Add_correct: forall i1 i2: t, AddSpec i1 i2 (add i1 i2).
  Proof (fun i1 i2 => proj2_sig (addDep i1 i2)).

  Definition OppSpec (i1 i2: t): Prop
    := forall n: N.t, sat i1 n <-> sat i2 (N.opp n).

  Definition bndOpp: bndT -> bndT
    := fun b =>
         match b with
           | Infty => Infty
           | Open n => Open (N.opp n)
           | Closed n => Closed (N.opp n)
         end.

  Definition oppDep (i0: t): {i: t | OppSpec i0 i}.
    refine (
        match i0
              return {i: t | OppSpec i0 i}
        with
          | Bot => exist _ Bot _
          | NotBot l u pfb =>
            let pfb': BndOk (bndOpp u) (bndOpp l) := _ in
            exist _ (NotBot (bndOpp u) (bndOpp l) pfb') _
        end);
    match goal with
      | |- OppSpec Bot Bot =>
        intro n;
          split;
          destruct 1
      | |- OppSpec _ _ =>
        intro n
      | _ => idtac
    end;
    destruct u;
      destruct l;
      constructor;
      inversion pfb;
      match goal with
        | |- sat _ _ -> sat _ _ =>
          simpl;
            intros [h1 h2];
            split;
            try constructor
        | _ => idtac
      end;
      match goal with
        | |- N.Lt (N.opp ?n1) (N.opp ?n2) => apply (proj1 (N.OppLt n2 n1))
        | |- N.Le (N.opp ?n1) (N.opp ?n2) => apply (proj1 (N.OppLe n2 n1))
        | |- N.Lt ?n1 ?n2 => apply (proj2 (N.OppLt n1 n2))
        | |- N.Le ?n1 ?n2 => apply (proj2 (N.OppLe n1 n2))
      end;
      assumption.
  Defined.
  Definition opp: t -> t
    := fun i => proj1_sig (oppDep i).

  Lemma Opp_correct: forall i1: t, OppSpec i1 (opp i1).
  Proof (fun i => proj2_sig (oppDep i)).

  Definition MulcSpec (i1: t) (n: N.t) (i2: t): Prop
    := forall n': N.t, sat i1 n' -> sat i2 (N.mul n n').

  Definition MulcStrongSpec (i1: t) (n: N.t) (i2: t): Prop
    := forall n': N.t, sat i1 n' <-> sat i2 (N.mul n n').

  Definition bndMulc: bndT -> N.t -> bndT
    := fun i n =>
         match i with
           | Infty => Infty
           | Open n' => Open (N.mul n n')
           | Closed n' => Closed (N.mul n n')
         end.

  Definition mulcPos (i0: t) (n0: {n: N.t | N.Lt N.z n}):
    {i: t | MulcStrongSpec i0 (proj1_sig n0) i}.
    refine (
        match n0
              return {i: t | MulcStrongSpec i0 (proj1_sig n0) i}
        with (exist n pfn) =>
             match i0
                   return {i: t | MulcStrongSpec i0 n i}
             with
               | Bot => exist _ Bot _
               | NotBot l u pfb =>
            let pfb': BndOk (bndMulc l n) (bndMulc u n) := _ in
            exist _ (NotBot (bndMulc l n) (bndMulc u n) pfb') _
             end
        end);
    match goal with
      | |- MulcStrongSpec Bot _ Bot =>
        intro n';
          split;
          destruct 1
      | |- MulcStrongSpec _ _ _ =>
        intro n'
      | _ => idtac
    end;
    destruct l;
      destruct u;
      inversion pfb;
      match goal with
        | |- sat _ _ <-> sat _ _ => simpl; split; intros [h1 h2]
        | _ => idtac
      end;
      repeat constructor;
      match goal with
        | h: N.Lt ?n1 ?n2 |- N.Lt (N.mul ?n ?n1) (N.mul ?n ?n2) => apply N.MulLt
        | h: N.Le ?n1 ?n2 |- N.Le (N.mul ?n ?n1) (N.mul ?n ?n2) => apply N.MulLe1
        | h1: N.Lt N.z ?n, h2: N.Lt (N.mul ?n ?n1) (N.mul ?n ?n2) |- N.Lt ?n1 ?n2
          => apply ((proj2 (N.MulLt _ _ _ h1)) h2)
        | h1: N.Lt N.z ?n, h2: N.Le (N.mul ?n ?n1) (N.mul ?n ?n2) |- N.Le ?n1 ?n2
          => apply (N.MulLe2 _ _ _ h1 h2)
        | _ => idtac
      end;
      match goal with
        | hyp: N.Lt ?n1 ?n2 |- N.Le ?n1 ?n2 => apply N.LtLe
        | _ => idtac
      end;
      assumption.
  Defined.
  Definition mulcZ (i0: t): {i: t | MulcSpec i0 N.z i}.
    refine (
        match i0
              return {i: t | MulcSpec i0 N.z i}
        with
          | Bot => exist _ Bot _
          | NotBot l u pfb =>
            match l
                  return forall pf: BndOk l u,
                           {i: t | MulcSpec (NotBot l u pf) N.z i}
            with
              | Infty =>
                fun pfb =>
                  match u
                        return
                        {i: t | MulcSpec (NotBot Infty u (BndInftyLow _)) N.z i}
                  with
                    | Infty => exist _ (NotBot Infty Infty (BndInftyLow _)) _
                    | _ => exist _ (NotBot Infty (Closed N.z) (BndInftyLow _)) _
                  end
              | Open n1 =>
                fun pfb =>
                  match u
                        return forall pf: BndOk (Open n1) u,
                                 {i: t | MulcSpec (NotBot (Open n1) u pf) N.z i}
                  with
                    | Infty =>
                      fun pfb =>
                        exist _ (NotBot (Closed N.z) Infty (BndInftyUp _)) _
                    | _ =>
                      fun pfb =>
                        let pfb': BndOk (Closed N.z) (Closed N.z) := _ in
                        exist _ (NotBot (Closed N.z) (Closed N.z) pfb') _
                  end pfb
              | Closed n1 =>
                fun pfb =>
                  match u
                        return forall pf: BndOk (Closed n1) u,
                                 {i: t | MulcSpec (NotBot (Closed n1) u pf) N.z i}
                  with
                    | Infty =>
                      fun pfb =>
                        exist _ (NotBot (Closed N.z) Infty (BndInftyUp _)) _
                    | _ =>
                      fun pfb =>
                        let pfb': BndOk (Closed N.z) (Closed N.z) := _ in
                        exist _ (NotBot (Closed N.z) (Closed N.z) pfb') _
                  end pfb
            end pfb
        end);
    match goal with
      | |- MulcSpec _ _ _ =>
        unfold MulcSpec;
          intros n' h;
          match goal with
            | hyp: sat Bot _ |- _ => destruct hyp
            | hyp: sat _ _ |- _ =>
              destruct hyp as [h1 h2];
                simpl
          end
      | _ => idtac
    end;
    repeat constructor;
    try rewrite N.MulZL;
    apply N.LeRefl.
  Defined.
  Definition mulcDep (i0: t) (n: N.t): {i: t | MulcSpec i0 n i}.
    refine (
        match N.dec N.z n with
          | inleft pfn0 =>
            match pfn0 with
              | left pfn =>
                let (i, pfi) := mulcPos i0 (exist _ n pfn) in
                exist _ i _
              | right pfn =>
                let pfn: N.Lt N.z (N.opp n) := _ in
                let (i, pfi) := mulcPos i0 (exist _ (N.opp n) pfn) in
                let (i', pfi') := oppDep i in
                exist _ i' _
            end
          | inright pfn =>
            let (i, pfi) := mulcZ i0 in
            exist _ i _
        end).
    - unfold MulcSpec.
      unfold MulcStrongSpec in pfi.
      simpl in pfi.
      intros.
      apply pfi;
        assumption.
    - replace N.z with (N.opp N.z) by apply N.OppZ.
      apply (proj1 (N.OppLt n N.z));
        assumption.
    - unfold MulcSpec.
      unfold OppSpec in pfi'.
      unfold MulcStrongSpec in pfi.
      simpl in pfi.
      intros n' h.
      rewrite <- (N.OppOpp (N.mul n n')).
      apply (pfi' (N.opp (N.mul n n'))).
      rewrite <- N.MulOppDistrL.
      apply pfi.
      assumption.
    - subst n.
      assumption.
  Defined.
  Definition mulc: t -> N.t -> t
    := fun i n => proj1_sig (mulcDep i n).

  Lemma Mulc_correct: forall (i1: t) (n: N.t), MulcSpec i1 n (mulc i1 n).
  Proof (fun i n => proj2_sig (mulcDep i n)).

  Import String.
  Local Open Scope string_scope.

  Definition pr: t -> string
    := fun i =>
         match i with
           | Bot => "bot"
           | NotBot l u _ =>
             let lstr :=
                 match l with
                   | Infty => "]-infty"
                   | Open n => "]" ++ (N.pr n)
                   | Closed n => "[" ++ (N.pr n)
                 end
             in
             let ustr :=
                 match u with
                   | Infty => "+infty["
                   | Open n => (N.pr n) ++ "["
                   | Closed n => (N.pr n) ++ "]"
                 end
             in
             lstr ++ ", " ++ ustr
         end.

End StdItv.

Module QItv <: AffItvSig (QNum).
  Include StdItv QNum.

  Definition ShiftSpec (i1 i2: t) (n: QNum.t): Prop
    := forall x: QNum.t, sat i1 x -> sat i2 (QNum.add n x).

  Definition shiftDep (i0: t) (n: QNum.t): {i: t | ShiftSpec i0 i n}.
    refine (
        match i0
              return {i: t | ShiftSpec i0 i n}
        with
          | Bot => exist _ Bot (fun x (h: sat Bot x) => match h with end)
          | NotBot low up pf =>
            let (i1, pf1) :=
                match low, up
                      return BndOk low up -> {i: bndT * bndT |
                              BndOk (fst i) (snd i) /\
                              (forall x, satLower low x -> satLower (fst i) (QNum.add n x)) /\
                              (forall x, satUpper up x -> satUpper (snd i) (QNum.add n x))}
                with
                  | Infty, Infty =>
                    fun pfb => exist _ (Infty, Infty) _
                  | Infty, Open n1 =>
                    fun pfb => exist _ (Infty, Open (QNum.add n n1)) _
                  | Infty, Closed n1 =>
                    fun pfb => exist _ (Infty, Closed (QNum.add n n1)) _
                  | Open n1, Infty =>
                    fun pfb => exist _ (Open (QNum.add n n1), Infty) _
                  | Open n1, Open n2 =>
                    fun pfb => exist _ (Open (QNum.add n n1), Open (QNum.add n n2)) _
                  | Open n1, Closed n2 =>
                    fun pfb => exist _ (Open (QNum.add n n1), Closed (QNum.add n n2)) _
                  | Closed n1, Infty =>
                    fun pfb => exist _ (Closed (QNum.add n n1), Infty) _
                  | Closed n1, Open n2 =>
                    fun pfb => exist _ (Closed (QNum.add n n1), Open (QNum.add n n2)) _
                  | Closed n1, Closed n2 =>
                    fun pfb => exist _ (Closed (QNum.add n n1), Closed (QNum.add n n2)) _
                end pf
            in
            let pf': BndOk (fst i1) (snd i1) := _ in
            exist _ (NotBot (fst i1) (snd i1) pf') _
        end);
    repeat split;
    simpl;
    intros;
    match goal with
      | |- BndOk _ _ => constructor; inversion pfb
      | _ => idtac
    end; auto with num;
    match goal with
      | h: sat _ _ |- _ => unfold sat in h
      | _ => idtac
    end;
      intuition.
  Defined.
  Definition shift: t -> QNum.t -> t
    := fun i n => proj1_sig (shiftDep i n).

  Lemma Shift_correct: forall (i: t) (n: QNum.t), ShiftSpec i (shift i n) n.
  Proof (fun i n => proj2_sig (shiftDep i n)).

End QItv.

Module ZItv <: AffItvSig (ZNum).

  Include StdItv ZNum.

  Local Hint Resolve ZtoQ.CeilLeZ ZtoQ.FloorLeZ QNum.LtLe.

  Require Import ZArith.

  Lemma ZNumLtLeSucc z1 z2: ZNum.Lt z1 z2 -> ZNum.Le (z1+1)%Z z2.
Proof.
    unfold ZNum.Lt, ZNum.Le. omega.
  Qed.

  Program Definition tightenL (qb: QItv.bndT): {zb: bndT | forall z: ZNum.t, QItv.satLower qb (ZtoQ.ofZ z) -> satLower zb z } :=
    match qb with
    | QItv.Infty => Infty
    | QItv.Open q => if ZtoQ.isInZ q then Closed ((ZtoQ.ceil q)+1)%Z else Closed (ZtoQ.ceil q)
    | QItv.Closed q => Closed (ZtoQ.ceil q)
    end.
  Obligation 2.
   rewrite ZtoQ.Ceil_exact; auto.
   apply ZNumLtLeSucc.
   rewrite ZtoQ.LtCommutes, <- H.
   auto.
  Qed.   Obligation 3.
    rewrite <- (ZtoQ.CeilZ z); auto.
  Qed.   Obligation 4.
    rewrite <- (ZtoQ.CeilZ z); auto.
  Qed.
  Lemma ZNumLtLePred z1 z2: ZNum.Lt z1 z2 -> ZNum.Le z1 (z2-1)%Z.
Proof.
    unfold ZNum.Lt, ZNum.Le. omega.
  Qed.

  Program Definition tightenU (qb: QItv.bndT): {zb: bndT | forall z: ZNum.t, QItv.satUpper qb (ZtoQ.ofZ z) -> satUpper zb z } :=
     match qb with
     | QItv.Infty => Infty
     | QItv.Open q => if ZtoQ.isInZ q then Closed ((ZtoQ.floor q)-1)%Z else Closed (ZtoQ.floor q)
     | QItv.Closed q => Closed (ZtoQ.floor q)
     end.
  Obligation 2.
   rewrite ZtoQ.Floor_exact; auto.
   apply ZNumLtLePred.
   rewrite ZtoQ.LtCommutes, <- H.
   auto.
  Qed.   Obligation 3.
   rewrite <- (ZtoQ.FloorZ z); auto.
  Qed.   Obligation 4.
   rewrite <- (ZtoQ.FloorZ z); auto.
  Qed.
  Definition FromQItvSpec (qi: QItv.t) (zi: t): Prop
    := forall z: ZNum.t, QItv.sat qi (ZtoQ.ofZ z) -> sat zi z.

  Definition fromQItv (qi: QItv.t): {zi: t | FromQItvSpec qi zi}.
    refine (
        match qi
                return {zi: t | FromQItvSpec qi zi}
        with
          | QItv.Bot => exist _ Bot _
          | QItv.NotBot low up pf0 =>
            let (l, pfl) := tightenL low in
            let (u, pfu) := tightenU up in
            let (i, pfi) := mk l u in
            exist _ i _
        end);
    unfold FromQItvSpec;
    simpl;
    intros z h.
    - destruct h.
    - unfold MkSpec in pfi.
      apply pfi;
        [apply pfl|apply pfu];
        intuition.
  Defined.
End ZItv.
Generated by coq2html