rNat.v

(* Axiomatizing of the real natural for stalmark *)
Require Export Relation_Definitions.
Parameter rNat:Set.
Parameter rle:rNat -> rNat ->Prop.
Parameter rlt:rNat -> rNat ->Prop.
Parameter rO:rNat.
Parameter rnext:rNat ->rNat.

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

Axiom rleDec:(m, n:rNat){(rle m n)}+{(rle n m)}.

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

Axiom rleNext:(m, n:rNat) (rle m (rnext n)) ->m=(rnext n) \/ (rle m n).

Axiom rltDef1:(m, n:rNat) (rlt m n) ->(rle m n).

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

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

Axiom rltTrans:(transitive rNat rlt).

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

Theorem rleCase: (m, n:rNat)(rle m n) \/ (rle n m).
Intros m n; Case (rleDec m n); Auto.
Qed.

Axiom rleRefl:(reflexive rNat rle).

Axiom rleTrans:(transitive rNat rle).

Axiom rleAntiSym:(n, m:rNat) (rle n m) -> (rle m n) ->n=m.

Axiom rOMin:(n:rNat)(rle rO n).

Axiom rnextLe:(x:rNat)(rle x (rnext x)).

Axiom rnextNeq:(x:rNat)~ x=(rnext x).

Axiom rNextInj:(a, b:rNat) (rnext a)=(rnext b) ->a=b.
Hints Resolve rltNotRefl rltDef3 rleRefl rOMin rnextLe rnextNeq.
Parameter rpred:rNat ->rNat.

Axiom rpredrnext:(x:rNat) ~ x=rO ->(rnext (rpred x))=x.

Definition rmax: rNat -> rNat ->rNat.
Intros n m; Case (rleDec n m).
Intros H'; Exact m.
Intros H'; Exact n.
Defined.

Theorem rmaxLeft: (n, m:rNat)(rle n (rmax n m)).
Intros n m; Unfold rmax; Case (rleDec n m); Auto.
Qed.

Theorem rmaxRight: (n, m:rNat)(rle m (rmax n m)).
Intros n m; Unfold rmax; Case (rleDec n m); Auto.
Qed.

Theorem rmaxCase: (n, m:rNat)n=(rmax n m) \/ m=(rmax n m).
Intros n m; Unfold rmax; Case (rleDec n m); Auto.
Qed.

Theorem rnextLeNeq: (x, y:rNat) (rle y x) ->~ y=(rnext x).
Intros x y H'; Red; Intros H'0.
Generalize H'; Absurd x=(rnext x); Auto.
Apply rleAntiSym; Auto.
Rewrite <- H'0; Auto.
Qed.
(*Some properties of rNat *)

Lemma rmaxRLe: (n, m, p:rNat) (rle m n) -> (rle p n) ->(rle (rmax m p) n).
Intros n m p.
Elim (rmaxCase m p); Intros H'1; Rewrite <- H'1; Auto.
Qed.

Theorem rmaxrLeRight: (m, n:rNat) (rle n m) ->(rmax n m)=m.
Intros m n; Unfold rmax; Case (rleDec n m); Auto.
Intros H' H'0; Apply rleAntiSym; Auto.
Qed.

Theorem rmaxrLeLeft: (m, n:rNat) (rle m n) ->(rmax n m)=n.
Intros m n; Unfold rmax; Case (rleDec n m); Auto.
Intros H' H'0; Apply rleAntiSym; Auto.
Qed.

Theorem rmaxO: (n:rNat)(rmax n rO)=n.
Intros n.
Apply rmaxrLeLeft; Auto.
Qed.
Hints Resolve rmaxRLe rmaxLeft rmaxRight rleRefl rnextLe rmaxO.

Definition rleDecBis: (m, n:rNat){(rle m n)}+{~ (rle m n)}.
Intros m n; Case (rleDec m n); Auto.
Intros H'; Case (rNatDec m n); Auto.
Intros H'0; Rewrite H'0.
Left; Apply rleRefl.
Intros H'0; Right; Red; Intros H'1.
Apply H'0; Apply rleAntiSym; Auto.
Defined.

Lemma rmaxDoubleLeft: (n, m, p:rNat)(rle n (rmax (rmax n m) p)).
Intros n m p; Apply rleTrans with y := (rmax n m); Auto.
Qed.

Lemma rmaxDoubleRight: (n, m, p:rNat)(rle m (rmax (rmax n m) p)).
Intros n m p; Apply rleTrans with y := (rmax n m); Auto.
Qed.
Hints Resolve rmaxDoubleLeft rmaxDoubleRight.

Theorem rmaxRle: (m, n, p:rNat) (rmax n p)=n -> (rle n m) ->(rmax m p)=m.
Intros m n p H' H'0.
Case (rmaxCase m p); Auto.
Intros H'1.
Rewrite (rleAntiSym m n); Auto.
Apply rleTrans with y := p; Auto.
Rewrite H'1; Auto.
Rewrite <- H'; Auto.
Qed.

Theorem notRnextRle: (m:rNat)~ (rle (rnext m) m).
Intros m; Red; Intros H'; Case (rnextNeq m).
Apply rleAntiSym; Auto.
Qed.

Theorem rNatOr: (a, b:rNat)a=b \/ ~ a=b.
Intros a b; Case (rNatDec a b); Auto.
Qed.

Theorem rnextRle: (a, b:rNat) (rle a b) ->(rle (rnext a) (rnext b)).
Intros a b H'.
Case (rleCase (rnext a) (rnext b)); Auto.
Intros H'0.
Elim (rleNext (rnext b) a); [Intros H'4; Rewrite <- H'4 | Intros H'4 | Idtac];
Auto.
Absurd (rle (rnext b) b); Auto.
Apply notRnextRle; Auto.
Apply rleTrans with y := a; Auto.
Qed.
Hints Resolve rnextRle.

Theorem rLerNext: (a, b:rNat) (rle (rnext a) (rnext b)) ->(rle a b).
Intros a b H'.
Case (rleNext (rnext a) b); Auto.
Intros H'0; Rewrite (rNextInj a b); Auto.
Intros H'0; Apply rleTrans with y := (rnext a); Auto.
Qed.

Theorem rOrltMin: (a:rNat)~ (rlt a rO).
Intros a; Red; Intros H'0.
Absurd a=rO; Auto.
Apply rltDef2; Auto.
Apply rleAntiSym; Auto.
Apply rltDef1; Auto.
Qed.

Theorem rONotNext: (r:rNat)~ rO=(rnext r).
Intros r; Apply rnextLeNeq; Auto.
Qed.
Hints Resolve rONotNext notRnextRle rOrltMin.

Theorem rltnextrle: (a, b:rNat) (rlt a (rnext b)) ->(rle a b).
Intros a b H'.
Apply rLerNext; Auto.
Case (rleDec (rnext a) (rnext b)); Intros H'0; Auto.
Case (rleNext (rnext b) a); Auto.
Intros H'1; Rewrite H'1; Auto.
Intros H'1.
Absurd (rlt (rnext b) (rnext b)); Auto.
Apply rltTrans with y := a; Auto.
Apply rltDef3; Auto.
Red; Intros H'2; Absurd (rlt a (rnext b)); Auto.
Rewrite <- H'2; Auto.
Qed.

Theorem rnextrpred: (a:rNat)(rpred (rnext a))=a.
Intros a; Cut ~ (rnext a)=rO; Auto.
Intros H'.
Apply rNextInj; Auto.
Rewrite rpredrnext; Auto.
Qed.

Theorem rltNot: (a, b:rNat) (rlt a b) ->~ (rlt b a).
Intros a b H'; Red; Intros H'0; Absurd a=b; Auto.
Apply rltDef2; Auto.
Apply rleAntiSym; Apply rltDef1; Auto.
Qed.

Theorem rltNext: (a, b:rNat) (rlt a b) ->(rlt (rnext a) (rnext b)).
Intros a b H'.
Apply rltDef3; Auto.
Apply rnextRle; Auto.
Apply rltDef1; Auto.
Red; Intros H'0; Absurd (rlt a b); Auto.
Rewrite (rNextInj a b); Auto.
Qed.
Hints Resolve rltNot rltNext.

25/03/99, 15:50