rZ.v

Require Import Relation_Definitions.
Parameter rNat:Set.
Parameter zero:rNat.
Parameter rnext:rNat ->rNat.
(* rZ are signed rNat *)

Inductive rZ: Set :=
     rZPlus: rNat ->rZ
    | rZMinus: rNat ->rZ .

(* We single out zero as being intepreted as True *)

Definition rZTrue := (rZPlus zero).

Definition rZFalse := (rZMinus zero).

(* Complementary *)

Definition rZComp: rZ ->rZ :=
   [r:rZ]
      Cases r of
          (rZPlus m) => (rZMinus m)
         | (rZMinus m) => (rZPlus m)
      end.

Theorem rZCompInv: (m:rZ)(rZComp (rZComp m))=m.
Intros m; Case m; Simpl; Auto.
Qed.
Parameter rlt:rNat -> rNat ->Prop.

Axiom rNatDec:(n, m:rNat){n=m}+{~ n=m}.

Axiom rltDec:(m, n:rNat){(rlt m n)}+{(rlt n m) \/ m=n}.

Axiom rltEDec:(m, n:rNat){(rlt m n)}+{(rlt n m)}+{m=n}.

Axiom rltDef2:(m, n:rNat) (rlt m n) ->~ m=n.

Axiom rltTrans:(transitive rNat rlt).

Axiom rltNotRefl:(a:rNat)~ (rlt a a).
Hints Resolve rltNotRefl.

Axiom rnextRlt:(m:rNat)(rlt m (rnext m)).
Hints Resolve rnextRlt.

Axiom rnextNotZero:(m:rNat)(rlt zero (rnext m)).
Hints Resolve rnextNotZero.

Definition rmax: rNat -> rNat ->rNat.
Intros n m; Case (rltDec n m); Intros Rlt0.
Exact m.
Exact n.
Defined.

Lemma rmaxRlt: (n, m, p:rNat) (rlt m n) -> (rlt p n) ->(rlt (rmax m p) n).
Intros n m p; Unfold rmax; Case (rltDec m p); Auto.
Qed.

Lemma rmaxRltLeft: (n, m, p:rNat) (rlt (rmax m p) n) ->(rlt m n).
Intros n m p; Unfold rmax; Case (rltDec m p); Auto; Intros Rlt0.
Intros Rlt1; Apply rltTrans with y := p; Auto.
Qed.

Lemma rmaxRltRight: (n, m, p:rNat) (rlt (rmax m p) n) ->(rlt p n).
Intros n m p; Unfold rmax; Case (rltDec m p); Auto; Intros Rlt0.
Case Rlt0; Clear Rlt0; Intros Rlt0; Auto.
Intros Rlt1; Apply rltTrans with y := m; Auto.
Rewrite <- Rlt0; Auto.
Qed.

Axiom rNextInv:(n, m:rNat) (rlt n (rnext m)) ->n=m \/ (rlt n m).

Lemma rltTransRnext1: (n, m, p:rNat) (rlt n (rnext m)) -> (rlt m p) ->(rlt n p).
Intros n m p H' H'0; Case (rNextInv n m); Auto.
Intros H'1; Rewrite H'1; Auto.
Intros H'1; Apply rltTrans with y := m; Auto.
Qed.

Lemma rltTransRnext2: (n, m, p:rNat) (rlt n m) -> (rlt m (rnext p)) ->(rlt n p).
Intros n m p H' H'0; Case (rNextInv m p); Auto.
Intros H'1; Rewrite <- H'1; Auto.
Intros H'1; Apply rltTrans with y := m; Auto.
Qed.

Lemma rltRnext2Inv: (n, m:rNat) (rlt (rnext n) (rnext m)) ->(rlt n m).
Intros n m H'; Case (rNextInv (rnext n) m); Auto.
Intros H'0; Rewrite <- H'0; Auto.
Intros H'1; Apply rltTrans with y := (rnext n); Auto.
Qed.

Lemma rnextMono: (m, n:rNat) (rlt m n) ->(rlt (rnext m) (rnext n)).
Intros m n H'.
Case (rltDec (rnext m) n); Intros Rlt0; Auto.
Apply rltTrans with y := n; Auto.
Case Rlt0; Intros Rlt1.
Elim (rNextInv n m); Auto; Intros Rlt2; Absurd (rlt m m); Auto.
Rewrite Rlt2 in H'; Auto.
Apply rltTrans with y := n; Auto.
Rewrite <- Rlt1; Auto.
Qed.
Hints Resolve rnextMono.

Lemma rltRmaxLeft: (n, m:rNat)(rlt n (rnext (rmax n m))).
Intros n m; Unfold rmax; Case (rltDec n m); Auto; Intros Rlt0.
Apply rltTrans with y := m; Auto.
Qed.

Lemma rltRmaxRight: (n, m:rNat)(rlt m (rnext (rmax n m))).
Intros n m; Unfold rmax; Case (rltDec n m); Auto; Intros Rlt0.
Case Rlt0; Clear Rlt0; Intros Rlt0; Auto.
Apply rltTrans with y := n; Auto.
Rewrite <- Rlt0; Auto.
Qed.
Hints Resolve rltRmaxLeft rltRmaxRight.

Theorem rltAntiSym: (a, b:rNat) (rlt a b) ->~ (rlt b a).
Intros a b H'; Red; Intros H'0; Absurd (rlt a a); Auto.
Apply rltTrans with y := b; Auto.
Qed.

Definition rZDec: (a, b:rZ){a=b}+{~ a=b}.
Intros a b; Case a; Case b; Try (Intros; Right; Red; Intros; Discriminate);
Intros a' b'; Case (rNatDec a' b'); Intros Eq1;
Try (Left; Rewrite Eq1; Auto; Fail); Auto; Intros; Right; Red; Intros Eq2;
Apply Eq1; Inversion Eq2; Auto.
Defined.

(*Absolute value*)

Definition valRz :=
   [a:rZ]
      Cases a of
          (rZPlus b) => b
         | (rZMinus b) => b
      end.

Definition rZlt := [a, b:rZ](rlt (valRz a) (valRz b)).

Definition eqRz := [a, b:rZ](valRz a)=(valRz b).
Hints Unfold eqRz rZlt.

Theorem eqrZRefl: (reflexive rZ eqRz).
Red; Intros a; Case a; Simpl; Auto.
Qed.
Hints Resolve eqrZRefl.

Theorem eqrZSym: (symmetric rZ eqRz).
Red; Intros a b; Case a; Case b; Simpl; Auto.
Qed.
Hints Resolve eqrZSym.

Theorem eqrZTrans: (transitive rZ eqRz).
Red; Auto.
Unfold eqRz; Intros x y z H'; Rewrite H'; Auto.
Qed.
Hints Resolve eqrZTrans.

Definition rZltDec: (a, b:rZ){(rZlt a b)}+{(rZlt b a) \/ (eqRz a b)}.
Intros a b; Exact (rltDec (valRz a) (valRz b)).
Defined.

Definition rZltEDec: (a, b:rZ){(rZlt a b)}+{(rZlt b a)}+{(eqRz a b)}.
Intros a b; Exact (rltEDec (valRz a) (valRz b)); Auto.
Defined.

Theorem rZltEqComp:
  (a, b, c, d:rZ) (rZlt a b) -> (eqRz a c) -> (eqRz b d) ->(rZlt c d).
Intros a b c d; Unfold rZlt eqRz; Case a; Case b; Case c; Case d; Simpl;
Intros a' b' c' d' H'0 H'1 H'2; Try Rewrite <- H'1; Try Rewrite <- H'2; Auto.
Qed.

Theorem rZltDef2: (a, b:rZ) (rZlt a b) ->~ (eqRz a b).
Intros a b H; Unfold eqRz; Apply rltDef2; Auto.
Qed.
Hints Resolve rZltDef2.

Theorem rZltTrans: (transitive rZ rZlt).
Red.
Intros x y z H' H'0; Red; Apply rltTrans with y := (valRz y); Auto.
Qed.
Hints Resolve rZltTrans.

Theorem rZltNotRefl: (a:rZ)~ (rZlt a a).
Intros a; Unfold rZlt; Auto.
Qed.
Hints Resolve rZltNotRefl.

Theorem rZltAntiSym: (a, b:rZ) (rZlt a b) ->~ (rZlt b a).
Intros a b H'; Red; Intros H'0; Absurd (rZlt a a); Auto.
Apply rZltTrans with y := b; Auto.
Qed.
Hints Resolve rZltAntiSym.

Theorem NotEqComp: (a:rZ)~ a=(rZComp a).
Intros a; Case a; Red; Intros H'; Discriminate.
Qed.
Hints Resolve NotEqComp.

Theorem eqRzComp: (a:rZ)(eqRz a (rZComp a)).
Intros a; Case a; Auto.
Qed.
Hints Resolve eqRzComp.

Theorem valRzComp: (a:rZ)(valRz (rZComp a))=(valRz a).
Intros a; Case a; Auto.
Qed.

Theorem rZCompInvol: (a:rZ)a=(rZComp (rZComp a)).
Intros a; Case a; Simpl; Auto.
Qed.
Hints Resolve rZCompInvol.

Theorem rZCompEq: (a, b:rZ) (rZComp a)=(rZComp b) ->a=b.
Intros a b; Case a; Case b; Simpl; Auto; Intros a' b' H; Inversion H; Auto.
Qed.

Definition min: rZ -> rZ ->rZ :=
   [a, b:rZ]
      Cases (rZltDec a b) of
          (left _) => a
         | (right _) => b
      end.

Definition max: rZ -> rZ ->rZ :=
   [a, b:rZ]
      Cases (rZltDec a b) of
          (left _) => b
         | (right _) => a
      end.

Theorem minProp1: (a, b:rZ) (rZlt a b) ->(min a b)=a.
Intros a b; Unfold min; Case (rZltDec a b); Simpl; Auto.
Intros H'; Case H'; Intros H'0 H'1.
Absurd (rZlt b a); Auto.
Absurd (eqRz a b); Auto.
Qed.

Theorem minProp2: (a, b:rZ) (rZlt b a) ->(min a b)=b.
Intros a b; Unfold min; Case (rZltDec a b); Simpl; Auto.
Intros H'0 H'1; Absurd (rZlt b a); Auto.
Qed.

Theorem minProp3: (a, b:rZ) (rZlt a b) ->(min b a)=a.
Intros a b; Unfold min; Case (rZltDec b a); Simpl; Auto.
Intros H'0 H'1; Absurd (rZlt b a); Auto.
Qed.

Theorem minProp4: (a, b:rZ) (rZlt b a) ->(min b a)=b.
Intros a b; Unfold min; Case (rZltDec b a); Simpl; Auto.
Intros H'; Case H'; Intros H'0 H'1.
Absurd (rZlt b a); Auto.
Absurd (eqRz b a); Auto.
Qed.

Theorem minProp5: (a, b:rZ) (eqRz a b) ->(min a b)=b.
Intros a b; Unfold min; Case (rZltDec a b); Simpl; Auto.
Intros H'0 H'1; Absurd (eqRz a b); Auto.
Qed.

Theorem minProp6: (a, b:rZ) (eqRz a b) ->(min b a)=a.
Intros a b; Unfold min; Case (rZltDec b a); Simpl; Auto.
Intros H' H'0; Absurd (eqRz b a); Auto.
Qed.

Theorem maxProp1: (a, b:rZ) (rZlt a b) ->(max a b)=b.
Intros a b; Unfold max; Case (rZltDec a b); Simpl; Auto.
Intros H'; Case H'; Intros H'0 H'1.
Absurd (rZlt b a); Auto.
Absurd (eqRz a b); Auto.
Qed.

Theorem maxProp2: (a, b:rZ) (rZlt b a) ->(max a b)=a.
Intros a b; Unfold max; Case (rZltDec a b); Simpl; Auto.
Intros H'0 H'1; Absurd (rZlt b a); Auto.
Qed.

Theorem maxProp3: (a, b:rZ) (rZlt a b) ->(max b a)=b.
Intros a b; Unfold max; Case (rZltDec b a); Simpl; Auto.
Intros H'0 H'1; Absurd (rZlt b a); Auto.
Qed.

Theorem maxProp4: (a, b:rZ) (rZlt b a) ->(max b a)=a.
Intros a b; Unfold max; Case (rZltDec b a); Simpl; Auto.
Intros H'; Case H'; Intros H'0 H'1.
Absurd (rZlt b a); Auto.
Absurd (eqRz b a); Auto.
Qed.

Theorem maxProp5: (a, b:rZ) (eqRz a b) ->(max a b)=a.
Intros a b; Unfold max; Case (rZltDec a b); Simpl; Auto.
Intros H' H'0; Absurd (eqRz a b); Auto.
Qed.

Theorem maxProp6: (a, b:rZ) (eqRz a b) ->(max b a)=b.
Intros a b; Unfold max; Case (rZltDec b a); Simpl; Auto.
Intros H' H'0; Absurd (eqRz b a); Auto.
Qed.

Definition rZSignDec: (a, b:rZ){a=b}+{a=(rZComp b)}+{~ (eqRz a b)}.
Intros a b; Case a; Case b; Intros a' b'; Case (rNatDec a' b'); Simpl; Auto;
Intros Eqa'b'.
Left; Left; Rewrite Eqa'b'; Auto.
Left; Right; Rewrite Eqa'b'; Auto.
Left; Right; Rewrite Eqa'b'; Auto.
Left; Left; Rewrite Eqa'b'; Auto.
Defined.

Definition liftRz :=
   [f:rNat ->rZ] [a:rZ]
      Cases a of
          (rZPlus a') => (f a')
         | (rZMinus a') => (rZComp (f a'))
      end.

Definition samePol := [a:rZ] [b:rNat](liftRz [a:rNat](rZPlus b) a).

Definition rVlt := [a:rZ] [b:rNat](rlt (valRz a) b).

Theorem rVltrZComp: (a:rZ) (b:rNat) (rVlt a b) ->(rVlt (rZComp a) b).
Intros a b; Case a; Simpl; Auto.
Qed.
Hints Resolve rVltrZComp.

Definition samePolRz := [a, b:rZ](liftRz [c:rNat]b a).
Require Import PolyList.
Parameter rZList:rNat ->(list rNat).

Axiom rZListIn:(a, b:rNat) (rlt a b) ->(In a (rZList b)).

Axiom InrZList:(a, b:rNat) (In a (rZList b)) ->(rlt a b).

Definition mBL := [n, a, b:rNat](rlt b a) /\ (rlt a n).

Axiom mBLWf:(n:rNat)(well_founded rNat (mBL n)).

05/07/100, 11:37