# Library CoinductiveExamples.ARITH.Omega

Require Import Acc_and_Inf.

Section Arithmetic_with_an_explicit_infinity.

CoInductive Nat : Set :=
| Z : Nat
| SUCC : Nat Nat.

Theorem Nat_unfold :
x : Nat, x = match x return Nat with
| ZZ
| SUCC xSUCC x
end.
intros.
case x.
trivial.
intros.
trivial.
Qed.

CoInductive EqNat : Nat Nat Prop :=
| eqZ : EqNat Z Z
| eqSUCC : n m : Nat, EqNat n m EqNat (SUCC n) (SUCC m).

Lemma EqNat_reflex : x : Nat, EqNat x x.
cofix u.
simple destruct x.
apply eqZ.

intros.
apply eqSUCC.
apply u.
Qed.

Lemma EqNat_inj : x y : Nat, x = y EqNat x y.
intros.
rewrite H.
apply EqNat_reflex.
Qed.

Inductive Le (n : Nat) : Nat Prop :=
| Le_n : Le n (SUCC n)
| Le_S : m : Nat, Le n m Le n (SUCC m).

Lemma Nat_Induction :
x : Nat,
Acc Le x
P : Nat Prop, P Z ( x : Nat, P x P (SUCC x)) P x.
intros x H.
elim H.
intros x0.
case x0.
intros.
assumption.
intros.
apply H3.
apply (H1 n).
apply Le_n.
assumption.
assumption.
Qed.

Lemma is_definitional_for_finite_numbers :
x : Nat, Acc Le x y : Nat, EqNat x y x = y.
intros x H.
apply (Nat_Induction x H).
intros.
inversion_clear H0.
trivial.
intros.
inversion_clear H1.
cut (x0 = m).
intros.
rewrite H1.
trivial.
apply H0.
assumption.
Qed.

CoFixpoint Plus : Nat Nat Nat :=
fun n m : Natmatch n with
| Zm
| SUCC pSUCC (Plus p m)
end.

Fixpoint ntoN (n : nat) : Nat :=
match n with
| OZ
| S mSUCC (ntoN m)
end.

Lemma natInj : n m : nat, ntoN n = ntoN m n = m.
fix 1.
intro n.
case n.
simple destruct m.
trivial.

simpl in |- ×.
intros.
cut (Z SUCC (ntoN n0)).
intros.
case H0.
assumption.
discriminate.

simple destruct m.
simpl in |- ×.
intros.
cut (SUCC (ntoN n0) Z).
intros.
case H0.
assumption.
discriminate.

simpl in |- ×.
intros.
cut (n0 = n1).
intros.
rewrite H0.
trivial.
apply (natInj n0 n1).
injection H; trivial.
Qed.

Section The_Infinity.

CoFixpoint OO : Nat := SUCC OO.

Definition OO_unfold : OO = SUCC OO := Nat_unfold OO.

Lemma Plus_Idemp : x : Nat, EqNat (Plus OO x) OO.
cofix u.
intros.
rewrite OO_unfold.
rewrite (Nat_unfold (Plus (SUCC OO) x)).
simpl in |- ×.
apply eqSUCC.
apply u.
Qed.

Lemma OO_is_infinite : Inf Nat Le OO.
cofix u.
rewrite OO_unfold.
apply (inf Nat Le (SUCC OO) OO).
apply (Le_n OO).
apply u.
Qed.

Lemma OO_is_not_Acc : ¬ Acc Le OO.
red in |- ×.
intros.
apply (NotBoth Nat Le OO).
assumption.
apply OO_is_infinite.
Qed.

Lemma only_OO_expands_forever : x : Nat, x = SUCC x EqNat x OO.
cofix u.
intros.
rewrite H.
rewrite OO_unfold.
apply eqSUCC.
apply u.
assumption.
Qed.

Lemma Z_is_minimum : x : Nat, Acc Le x Le Z (SUCC x).
intros.
apply (Nat_Induction x H).
apply Le_n.
intros.
apply Le_S.
assumption.
Qed.

Lemma only_OO_is_grater_than_OO : y : Nat, Le OO y EqNat OO y.
cofix u.
intros y H.
case H.
apply EqNat_inj.
apply OO_unfold.
intros.
rewrite OO_unfold.
apply eqSUCC.
apply u.
assumption.
Qed.

Lemma all_infinite_is_OO : x : Nat, Inf Nat Le x EqNat x OO.
cofix u.
rewrite OO_unfold.
intros.
case H.
intros.
inversion_clear H0.
apply eqSUCC.
apply u.
assumption.
apply eqSUCC.
apply u.
apply (inf Nat Le m y).
assumption.
assumption.
Qed.

Lemma OO_is_infiniteII : Inf Nat (fun x y : NatLe y x) OO.
cofix u.
apply (inf Nat (fun x y : NatLe y x) OO OO).
pattern OO at 2 in |- ×.
rewrite OO_unfold.
apply Le_n.
apply u.
Qed.

End The_Infinity.

End Arithmetic_with_an_explicit_infinity.