rZ.v

(* Definition of signed real natural *)
Require Export rNat.
Require Export Bool.

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

Theorem TDiffF: ~ rZTrue=rZFalse.
Red; Intros H1; Discriminate H1.
Qed.

Theorem FDiffT: ~ rZFalse=rZTrue.
Red; Intros H1; Discriminate H1.
Qed.
Hints Resolve TDiffF FDiffT.

Definition rZDec: (i, j:rZ){i=j}+{~ i=j}.
Intros i; Case i.
Intros j; Case j.
Left; Auto.
Right; Red; Intros H'; Inversion H'.
Intros r; Right; Red; Intros H'; Inversion H'.
Intros r; Right; Red; Intros H'; Inversion H'.
Intros j; Case j.
Right; Red; Intros H'; Inversion H'.
Left; Auto.
Intros r; Right; Red; Intros H'; Inversion H'.
Intros r; Right; Red; Intros H'; Inversion H'.
Intros r j; Case j.
Right; Red; Intros H'; Inversion H'.
Right; Red; Intros H'; Inversion H'.
Intros r0; Case (rNatDec r r0); Intros H.
Rewrite H; Left; Auto.
Right; Red; Intros H'; Apply H; Inversion H'; Auto.
Intros r0; Right; Red; Intros H'; Inversion H'.
Intros r j; Case j.
Right; Red; Intros H'; Inversion H'.
Right; Red; Intros H'; Inversion H'.
Intros r0; Right; Red; Intros H'; Inversion H'.
Intros r0; Case (rNatDec r r0); Intros H.
Rewrite H; Left; Auto.
Right; Red; Intros H'; Apply H; Inversion H'; Auto.
Defined.

Definition fEval: (rNat ->bool) -> rZ ->bool :=
   [f:rNat ->bool] [r:rZ]
      Cases r of
          rZTrue => true
         | rZFalse => false
         | (rZPlus n) => (f n)
         | (rZMinus n) => (negb (f n))
      end.

Definition valRz: rZ ->rNat :=
   [r:rZ]
      Cases r of
          rZTrue => rO
         | rZFalse => rO
         | (rZPlus m) => m
         | (rZMinus m) => m
      end.

Definition rZLe: rZ -> rNat ->Prop := [r:rZ] [n:rNat](rle (valRz r) n).

Mutual Inductive inRz: rNat -> rZ ->Prop :=
     inRzPlus: (n:rNat)(inRz n (rZPlus n))
    | rMinus: (n:rNat)(inRz n (rZPlus n)) .

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

Theorem rZDiff: (r:rZ)~ r=(rZComp r).
Intros r; Case r; Clear r; Simpl; Red; Intros r H' Orelse Intros H';
Inversion H'.
Qed.
Hints Resolve rZDiff.

Theorem rZCompInv: (m:rZ)(rZComp (rZComp m))=m.
Intros m; Case m; Simpl; Auto.
Qed.

Theorem rZCompComp: (m, p:rZ) m=p ->(rZComp m)=(rZComp p).
Intros m p H'; Rewrite H'; Auto.
Qed.

Theorem eqrZComp: (a, b:rZ) (rZComp a)=(rZComp b) ->a=b.
Intros a b H'.
Rewrite <- (rZCompInv a); Rewrite <- (rZCompInv b); Rewrite <- H'; Auto.
Qed.
Hints Resolve rZCompComp rZCompInv.

Theorem rZLeComp: (n:rNat) (m:rZ) (rZLe m n) ->(rZLe (rZComp m) n).
Intros n m; Elim m; Simpl; Auto.
Qed.
Hints Resolve rZLeComp.

Theorem rZLeTrue: (n:rNat)(rZLe rZTrue n).
Intros n; Unfold rZLe; Simpl; Apply rOMin; Auto.
Qed.

Theorem rZLeFalse: (n:rNat)(rZLe rZFalse n).
Intros n; Unfold rZLe; Simpl; Apply rOMin; Auto.
Qed.
Hints Resolve rZLeTrue rZLeFalse.

Theorem rZLeTrans: (n, m:rNat) (p:rZ) (rZLe p n) -> (rle n m) ->(rZLe p m).
Intros n m p; Case p; Unfold rZLe; Simpl; Auto.
Intros n' H' H'0; Apply rleTrans with y := n; Auto.
Intros n' H' H'0; Apply rleTrans with y := n; Auto.
Qed.

Theorem rZLeCompRev: (n:rNat) (m:rZ) (rZLe (rZComp m) n) ->(rZLe m n).
Intros n m; Elim m; Simpl; Auto.
Qed.

25/03/99, 16:00