# Library naturals

Require Import logical.
Require Import algebra.

# Natural Numbers

## 1 Peano Axioms

Inductive nat : Type :=
| O : nat
| S : nat -> nat.

Definition pred (x : nat) : nat := match x with
| O => O
| S x' => x' end.

Theorem axiom3 {x:nat} : O <> S x.
intros x. discriminate.
Qed.

Theorem axiom4 {x y: nat} : S x = S y -> x = y.
intros x y A. apply (f_equal pred A).
Qed.

Theorem axiom5 (p:nat->Prop) : p O -> (forall x:nat , p x -> p (S x)) -> forall x:nat, p x.
intros p base step.
fix IHx 1. intros [|x].
exact base.
exact (step x (IHx x)).
Qed.

## 2 Addition of natural numbers

Theorem satz1 {x y:nat} : x <> y -> S x <> S y.
intros x y A B. exact (A (axiom4 B)).
Qed.

Theorem satz2 {x:nat} : S x <> x.
induction x. discriminate. apply (satz1 IHx).
Qed.

Theorem satz3 {x:nat} : x <> O -> exists y, x = S y.
intros [|y]. tauto. intros _. exists y. reflexivity.
Qed.

Fixpoint add_nat (x y:nat) : nat := match y with
| O => S x
| S y' => S (x + y')
end
where "x + y" := (add_nat x y).

Theorem satz4: forall f:nat->nat->nat,
(forall x, f x O = S x)->(forall x y, f x (S y) = S (f x y))-> forall x y, x+y = f x y.
induction y. rewrite H. reflexivity. rewrite H0. rewrite <- IHy. reflexivity.
Qed.

Associativity of +
Theorem satz5 : associative nat add_nat.
intros x y z. induction z. reflexivity. simpl. apply (f_equal S IHz).
Qed.

Commutativity of +
Lemma satz6H1 (x:nat) : O+x = x+O.
induction x. reflexivity. simpl. apply (f_equal S IHx).
Qed.

Lemma satz6H2 (x y:nat) : S x + y = S ( x + y ).
induction y. reflexivity. simpl. apply (f_equal S IHy).
Qed.

Theorem satz6 : commutative nat add_nat.
intros x. induction x. apply satz6H1. simpl. intros y. rewrite (satz6H2 x y).
exact (f_equal S (IHx y)).
Qed.

Theorem satz7 (x y:nat) : y <> x+y.
induction y. discriminate. intros A. exact (IHy (axiom4 A)).
Qed.

Theorem satz8 {x y z:nat} : y <> z -> x+y <> x+z.
intros x y z A. induction x; intros B. repeat (rewrite satz6H1 in B).
exact (satz1 A B).
repeat (rewrite satz6H2 in B). exact (satz1 IHx B).
Qed.

# Trichotomy

Theorem satz9H0 (x y:nat): x=y\/(exists u,x=y+u)\/(exists u, y=x+u).
induction x; intros [|y]. tauto.
right. right. exists y. rewrite satz6. reflexivity.
right. left. exists x. rewrite satz6. reflexivity.
destruct (IHx y) as [A|[[u A]|[u A]]].
left. apply (f_equal S A).
right. left. exists u. rewrite satz6H2. apply (f_equal S A).
right. right. exists u. rewrite satz6H2. apply (f_equal S A).
Qed.

Mutual exclusion
Definition atmost1of3 (X Y Z:Prop) := (~(X/\Y)/\~(X/\Z))/\~(Y/\Z).

Theorem satz9H1 {x y:nat}: atmost1of3 (x=y) (exists u, x=y+u) (exists u, y = x+u).
intros x y. split.
split; intros [A [u B]]; rewrite A in B; rewrite satz6 in B;
intros [[u1 A][u2 B]]. rewrite A in B. rewrite satz5 in B.
rewrite satz6 in B. contradiction (satz7 _ _ B).
Qed.

## 3 Order of the natural numbers

Inductive definition of <=

Fixpoint leq_nat (x y:nat) : bool := match x , y with
| O , _ => true
| S x , S y => x <= y
| _ , _ => false
end
where "x <= y":=(leq_nat x y).

Notation "x < y":=(S x <= y).
Notation "x == y":=(andb (x<=y) (y<=x))(at level 70, no associativity).

Definition eq_nat (x y:nat) := x == y.

Lemma leq_nat_linear : linear nat leq_nat.
unfold linear.
fix IHx 1. intros [|x] [|y]. left. exact I.
left. exact I.
right. exact I.
apply (IHx x y).
Qed.

Lemma leq_nat_antisymmetric : antisymmetric nat leq_nat.
unfold antisymmetric.
fix IHx 1. intros [|x] [|y].
intros _ _. reflexivity.
intros _ [].
intros [].
intros A B. apply (f_equal S (IHx x y A B)).
Qed.

Lemma lt_nat_add_const {x y:nat} : x < x + y.
induction x; intros y. rewrite satz6. exact I.
rewrite satz6H2. apply IHx.
Qed.

Lemma leq_nat_reflexive: reflexive nat leq_nat.
unfold reflexive.
induction x.
exact I.
exact IHx.
Qed.

Lemma lt_nat_irreflexive {x :nat} : ~ x < x.
induction x.
intros [].
exact IHx.
Qed.

Lemma eq_nat_reflexive : forall x, x == x.
induction x.
exact I.
exact IHx.
Qed.

Lemma leq_nat_weak {x y:nat} : x < y -> x <= y.
fix IHx 1. intros [|x] [|y].
intros []. intros _. exact I.
intros []. apply (IHx x y).
Qed.

Proof of the equivalence between Landau's and the inductive definition

Lemma nat_order_equiv_a {x y : nat} : (exists u, y = x + u) -> x < y.
intros x y [u A]. rewrite A. apply lt_nat_add_const.
Qed.

Lemma nat_order_equiv_b {x y:nat} : x < y -> exists u, y = x + u.
induction x. destruct y. intros []. intros _. exists y. rewrite satz6. reflexivity.
destruct y. intros []. simpl. intros A. destruct (IHx y A) as [u B]. exists u. rewrite satz6H2.
apply (f_equal S B).
Qed.

Lemma nat_order_equiv_c {x y :nat} : x = y -> x == y.
intros x y A. rewrite A. apply eq_nat_reflexive.
Qed.

Lemma nat_order_equiv_d {x y :nat} : x==y -> x=y.
fix IHx 1. intros x y A. destruct x.
destruct y. reflexivity.
exact (f_equal S (IHx x y A)).
Qed.

Lemma nat_order_equiv_e {x y:nat} : x <= y -> x = y \/ x < y.
induction x; destruct y; try tauto.
intros A.
destruct (IHx y A) as [B|B].
left. exact (f_equal S B).
right. destruct (IHx y A) as [C|_].
rewrite C in B. contradiction (lt_nat_irreflexive B).
exact B.
Qed.

Lemma nat_order_equiv_f {x y:nat} : x = y \/ x < y -> x <=y.
fix IHy 2.
intros x y [A|A].
rewrite A. apply leq_nat_reflexive.
destruct y.
destruct x. exact I.
apply (IHy x y). right. exact A.
Qed.

Trichotomy

Theorem satz10H0 : trichotomy nat (fun x y => x < y).
intros x. induction x ; intros [|y] ; try (simpl ; tauto).
destruct (IHx y) as [A|[[]|A]]; tauto. Qed.

Mutual exclusion

Lemma satz10H1 (x y:nat): y<x -> x=y -> False.
induction x; intros [|y].
intros [].
intros _. discriminate.
intros _. discriminate.
intros A B. apply (IHx y A (f_equal pred B)).
Qed.

Lemma satz10H2 (x y:nat): y<x -> x<y -> False.
induction x; intros [|y].
intros [].
intros [].
intros _ [].
apply IHx.
Qed.

Lemma satz10H3 (x y:nat): x<y -> x=y -> False.
induction x; intros [|y].
intros [].
intros _. discriminate.
intros [].
intros A B. apply (IHx y A (f_equal pred B)).
Qed.

Theorem satz17a : transitive nat leq_nat.
intros x; induction x; intros [|y] [|z]; try (simpl;tauto).
exact (IHx y z).
Qed.

Theorem satz16a {x y z:nat}: x<=y -> y<z -> x<z.
intros x y z. exact (@satz17a (S x) (S y) _).
Qed.

Theorem satz16b {x y z:nat} : x<y -> y<=z->x<z.
intros x y z. exact (@satz17a (S x) y z).
Qed.

Transitivity of <
Theorem satz15a : forall x y z, x < y -> y < z -> x < z.
intros x; induction x; intros [|y] [|z]; try (simpl;tauto).
exact (IHx y z).
Qed.

Theorem satz18 (x y:nat) : x<x+y.
Qed.

Theorem satz19a {x y z:nat} : x<y -> x+z<y+z.
induction z; simpl; tauto.
Qed.

Theorem satz19b (x y z:nat) : x=y -> x+z=y+z.
intros x y z A. rewrite A. reflexivity.
Qed.

Theorem satz20a {x y z:nat} : x+z<y+z->x<y.
induction z; simpl; tauto.
Qed.

Theorem satz20b {x y z:nat} : x+z=y+z->x=y.
induction z; intros A.
exact (f_equal pred A).
exact (IHz (f_equal pred A)).
Qed.

Theorem satz21 {x y z u:nat} : x<y -> z<u -> x+z<y+u.
intros x y z u A B.
apply (satz15a (x+z) (y+z) (y+u)).
exact (satz19a A).
rewrite (satz6 y z),(satz6 y u).
exact (satz19a B).
Qed.

Lemma satz23' {x y z:nat} : x<=y -> x+z<=y+z.
induction z; intros A.
exact A.
exact (IHz A).
Qed.

Theorem satz23a {x y z u:nat} : x<=y -> z<=u -> x+z<=y+u.
intros x y z u A B.
destruct (nat_order_equiv_e B) as [C|C];
destruct (nat_order_equiv_e A) as [D|D].
rewrite C. exact (satz23' A).
rewrite C. exact (satz23' A).
rewrite <-D, (satz6 x u), (satz6 x z). exact (satz23' B).
apply nat_order_equiv_f.
right. exact (satz21 D C).
Qed.

Theorem satz22a {x y z u:nat} : x<=y -> z<u -> x+z<y+u.
intros x y z u A B.
exact (satz23a A B).
Qed.

Theorem satz22b {x y z u:nat} : x<y -> z<=u -> x+z<y+u.
intros x y z u A C.
rewrite<- satz6H2.
exact (satz23a A C).
Qed.

Theorem satz24 (x:nat) : O<=x.
intros x; exact I.
Qed.

## Well-Ordering-Principle non-constructive

Remark: This is very close to the proof of Landau

Given a set p the set M contains all natural numbers less or equal than all members of p

Definition min (p:nat->Prop) (m:nat) := p m /\ forall x, p x -> m<=x.

Definition WP : Prop := forall p:nat -> Prop, (exists x, p x) -> exists m, min p m.

Definition M (p : nat -> Prop) := fun x:nat => forall y, p y -> x<=y.

O is in the set M.
Lemma OInM (p:nat->Prop) : M p O.
Proof. intros p y _. exact I.
Qed.

Not all natural numbers are in M.
Lemma exNotInM (p :nat->Prop) : (exists x, p x) -> ~ forall y, M p y.
Proof. intros p [x A] B.
contradiction (lt_nat_irreflexive (B (S x) x A)).
Qed.

Lemma deMorgan (p :nat->Prop) : XM -> (forall x:nat, ~ (p x /\ ~ p (S x))) -> forall x, p x-> p (S x).
Proof. intros p xm A x B.
destruct (xm (p (S x))). exact H.
destruct (A x).
split.
exact B.
exact H.
Qed.

Lemma quantRule (p:nat->Prop) : ~ (exists x, p x) -> forall x, ~ p x.
Proof. intros p. intros A x px. apply A. exists x. exact px.
Qed.

There exists an m in M such that m+1 is not in M. This is our candidate.
Lemma exInM (p :nat->Prop) : XM ->(exists x, p x) -> exists m, M p m /\ ~ M p (S m).
Proof. intros p xm A.
destruct (xm (exists m, M p m /\ ~ M p (S m))) as [B|B].
exact B.
contradiction ((exNotInM _ A) (axiom5 _ (OInM _) (deMorgan _ xm (quantRule _ B)))).
Qed.

If we have x in M but not in p, then x+1 is also in M.
Lemma help {p :nat->Prop} {x:nat} : M p x -> ~ p x -> M p (S x).
Proof. intros p x A B y py.
unfold M in A.
destruct (nat_order_equiv_e (A y py)) as [C|C].
rewrite <-C in py. contradiction (B py).
exact C.
Qed.

Conclusion
Theorem XM_WP : XM -> WP.
Proof. intros xm p A.
destruct (exInM p xm A) as [m B].
exists m. split.
destruct (xm (p m)) as [C|C]. exact C.
destruct B as [B D]. contradiction (D (help B C)).
destruct B as [B C]. exact B.
Qed.

Necessity of XM
Theorem WP_XM : WP -> XM.
intros wp x.
destruct (wp (fun n => match n with O => x | _ => True end)) as [[|m] [A B]].
exists (S O); tauto.
tauto. right. exact (B O).
Qed.

Constructive version of Satz 27

Helping lemmata for the the proof of the Well-Ordering-Principle

Fixpoint first (p:nat->bool) (x:nat) :=
match x with
|O => O
|S x => if p (first p x) then first p x else (S x)
end.

Lemma ltPred {x:nat} : x < S x.
induction x. exact I.
exact IHx.
Qed.

Lemma first_correct_a {p : nat->bool} (x:nat) : first p x <= x.
induction x. exact I.
simpl. case_eq (p (first p x)); intros _.
exact (satz15a (first p x) (S x) (S (S x)) IHx ltPred).
apply ltPred.
Qed.

Lemma firstMember {p :nat->bool} (x:nat) : p x -> p (first p x).
induction x. intros. tauto.
simpl. case_eq (p (first p x)); intros A.
intros _. apply (reflect_eq2 A). tauto.
Qed.

Lemma firstConstant {p :nat->bool} :
forall x, p (first p x) -> forall y, x < y -> first p x = first p y.
induction y; intros B. contradiction B.
destruct (nat_order_equiv_e B) as [C|C].
rewrite<- C. simpl.
rewrite (reflect_eq1 H).
reflexivity.
simpl. rewrite<- (IHy C).
rewrite (reflect_eq1 H). reflexivity.
Qed.

Lemma firstConstant' {p :nat->bool} :
forall x, p x -> forall y, x < y -> first p x = first p y.
intros p x A y B.
apply (firstConstant _ (firstMember _ A) _ B).
Qed.

Lemma first_correct_b (p:nat->bool) (x y:nat) : x <= y -> p x -> p (first p y).
intros f x y A B.
destruct (nat_order_equiv_e A) as [C|C].
subst x. apply (firstMember _ B).
rewrite <-(firstConstant x (firstMember _ B) y C).
apply (firstMember _ B).
Qed.

Lemma first_correct_c (p q:nat->bool) : (forall x, p x = q x) -> forall x, first p x = first q x.
intros f g A. induction x.
reflexivity.
unfold first. fold first.
rewrite IHx,A.
reflexivity.
Qed.

Well-Ordering-Principle

Theorem satz27 (p :nat->bool) : (exists x, p x) ->
exists m, p m /\ forall y, p y -> m <= y.
intros p [x A].
exists (first p x).
split. exact (firstMember x A).
intros y B. destruct (satz10H0 x y) as [C|[C|C]].
apply (satz17a _ _ _ (first_correct_a x)).
apply (leq_nat_weak C).
rewrite C. apply first_correct_a.
rewrite<- (firstConstant y (firstMember _ B)). apply first_correct_a.
apply C.
Qed.

## 4 Multiplication of natural numbers

Fixpoint mul_nat (x y:nat) : nat := match y with
| O => x
| S y' => x*y' + x
end
where "x * y" := (mul_nat x y).

Lemma leq_nat_mul_const {x y:nat} : x <= x*y.
induction y.
apply leq_nat_reflexive.
simpl. rewrite satz6.
apply nat_order_equiv_f.
Qed.

Theorem satz28 : forall f:nat->nat->nat,
(forall x, f x O = x)->(forall x y, f x (S y) = f x y + x)-> forall x y, x*y = f x y.
intros f A B x y. induction y. rewrite A. reflexivity.
rewrite B. rewrite <- IHy. reflexivity.
Qed.

Commutativity of *
Theorem satz29' {x:nat} : O*x = x*O.
induction x. reflexivity. simpl. rewrite IHx. reflexivity.
Qed.

Theorem satz29'' {x y:nat} : S x * y = x*y+y.
induction y. reflexivity. simpl. rewrite IHy. rewrite satz5.
rewrite (satz6 y x). rewrite <- satz5. reflexivity.
Qed.

Theorem satz29 : commutative nat mul_nat.
intros x. induction x; intros y. apply satz29'.
simpl. rewrite <-(IHx y). apply satz29''.
Qed.

Theorem satz30 : distributes nat add_nat mul_nat.
intros x y z. induction z. reflexivity. simpl. rewrite IHz. apply satz5.
Qed.

Theorem satz30' {x y z:nat} : (x+y)*z = x*z+y*z.
intros x y z. rewrite satz29. rewrite satz30. repeat rewrite (satz29 z). reflexivity.
Qed.

Associativity of *
Theorem satz31 : associative nat mul_nat.
intros x y z. induction z. reflexivity. simpl. rewrite IHz.
symmetry. exact (satz30 _ _ _).
Qed.

Theorem satz32a {x y z:nat} : x<y ->x*z<y*z.
induction z. intros A. exact A.
intros B. exact (satz21 (IHz B) B).
Qed.

Theorem satz32b (x y z:nat) : x=y -> x*z=y*z.
intros x y z A. rewrite A. reflexivity.
Qed.

leq_nat
Theorem satz32c {x y z:nat} : x <= y -> x*z <= y*z.
induction z. tauto.
intros A. exact (satz23a (IHz A) A).
Qed.

Theorem satz33a {x y z:nat} : x*z<y*z -> x<y.
intros x y z A. destruct (satz10H0 x y) as [B|[B|B]].
exact B.
contradiction (satz10H3 _ _ A (satz32b _ _ _ B)).
contradiction (satz10H2 _ _ A (satz32a B)).
Qed.

Theorem satz33b {x y z:nat} : x*z=y*z -> x=y.
intros x y z A. destruct (satz10H0 x y) as [B|[B|B]].
contradiction (satz10H3 _ _ (satz32a B) A).
exact B.
contradiction (satz10H1 _ _ (satz32a B) A).
Qed.

Theorem satz34 {x y z u:nat} : x<y -> z<u -> x*z<y*u.
intros x y z u A B. apply (satz15a (x*z) (y*z) (y*u)).
apply (satz32a A).
rewrite (satz29 y z),(satz29 y u). exact (satz32a B).
Qed.

Theorem satz36 {x y z u:nat} : x<=y -> z<=u -> x*z<=y*u.
intros x y z u A B. apply (satz17a _ (y*z)).
apply (satz32c A).
rewrite (satz29 y u), (satz29 y z).
apply (satz32c B).
Qed.

Subtraction of the natural numbers

Fixpoint sub_nat (x y:nat) : y<x -> nat := match x,y with
| O , y => fun (l:y<O) => match l with end
| S x' , O => fun _ => x'
| S x' , S y' => fun (l:S y'<S x') => sub_nat x' y' l
end.

Theorem sub_nat_correct_a (x y:nat) (l:x<y) : x + (sub_nat y x l) = y.
fix IHx 1.
intros [|x] [|y].
intros [].
intros A. simpl. rewrite satz6H1. reflexivity.
intros [].
intros A. simpl. rewrite satz6H2. rewrite (IHx x y A).
reflexivity.
Qed.

Theorem sub_nat_correct_b {x y:nat} : x < y -> exists z, x + z = y.
intros x y A. exists (sub_nat y x A).
apply sub_nat_correct_a.
Qed.

Theorem mul_nat_identity_l : identity_l nat O mul_nat.
intros x; rewrite satz29; tauto.
Qed.

Theorem complete_induction (p: nat->Prop) :
(forall n, (forall m, m < n -> p m) -> p n) -> forall n, p n.

Proof. intros p H n. apply H.
induction n; intros x A.
apply H. intros m B. apply IHn.
apply (satz17a _ _ _ B A).
Qed.

Theorem sqrt_twoH0 {x y:nat} : x * x < y * y -> x < y.
intros x y A.
destruct (satz10H0 x y) as [B|[B|B]].
apply B.
destruct (satz10H1 _ _ A). rewrite B; reflexivity.
destruct (satz10H2 _ _ A). apply (satz34 B B).
Qed.

Theorem sqrt_twoH1 {x y:nat} : (x + y)*(x + y) = x * x + S O * x * y + y * y.
intros x y.
rewrite satz30.
rewrite (satz29 _ x),(satz29 _ y),satz30,satz30.
rewrite <-satz5,(satz5 _ (x*y)),(satz29 y x).
rewrite (satz31 (S O)),(satz29 (S O)). tauto.
Qed.

Theorem mul_nat_a (x:nat) : x + x = S O * x.
intros x. rewrite satz29; tauto.
Qed.

Theorem sqrt_two {y x:nat} : x * x = S O * y * y -> False.
apply (complete_induction (fun y => forall x, x * x = S O * y * y -> False)).
intros y K x A.
cut (y < x).
intros B.
cut (x < S O * y).
intros C.
cut (sub_nat x y B < y).
intros D.
set (u:=sub_nat x y B).
fold u in D.
set (t:=sub_nat y u D).
cut (t * t = S O * u * u).
intros G.
apply (K u D _ G).
apply (@satz20b _ _ (x*x)).
repeat rewrite (satz6 _ (x*x)).
rewrite <-(sub_nat_correct_a _ _ B).
fold u.
rewrite sqrt_twoH1.
rewrite satz5.
rewrite (satz31 (S O) y u),(satz29 y u),<-(satz31 (S O)).
generalize (@satz19b t (sub_nat y u D) u (refl_equal t)).
rewrite (satz6 (sub_nat y u D) u),sub_nat_correct_a.
intros G; rewrite <-G.
rewrite (@satz30 (S O * u)),(satz6 (S O * u * t)),G,<-(satz5 (y*y)).
rewrite (satz5 _ (S O * u * t)),<-(satz5 _ (u*u)),(satz6 _ (u*u)),
<-sqrt_twoH1. rewrite (satz6 u t),G,(satz6 _ (y*y)),<-(satz5 (y*y)).
rewrite mul_nat_a,(satz5 (y*y)),<-satz30,(satz6 u t),G.
rewrite (satz31 _ u y),(satz29 u y),<-(satz31 _ y u).
rewrite <-sqrt_twoH1.
generalize (@satz19b u (sub_nat x y B) y (refl_equal u)).
rewrite (satz6 (sub_nat x y B) y),sub_nat_correct_a,(satz6 u y).
intros H; rewrite H,<-satz31,A. tauto.
apply (@satz20a _ _ y).
rewrite (satz6 _ y),(sub_nat_correct_a _ _ B).
rewrite satz29 in C. apply C.
apply sqrt_twoH0.
rewrite A.
rewrite (satz29 (S O * y)).
apply satz32a.
rewrite <-(mul_nat_identity_l y),<-satz31.
apply satz32a. exact I.
apply sqrt_twoH0.
rewrite <-(mul_nat_identity_l (y*y)),A,satz31.
apply satz32a. exact I.
Qed.