(* This is a proof script formalising Section 3.2.4 of my bachelor's thesis on foundations of mathematics.
Presented as a website, you can hover the mouse over the definitions and statements to see their effects.
The commands inbetween Proof and Qed manipulate the proof state, which is also visible by hovering over theses commands. *)
Definition add (m n : nat) :=
nat_rect _ m (fun _ n' => S n') n.
Definition mul (m n : nat) :=
nat_rect _ O (fun _ n' => add m n') n.
Compute (add (S O) (S O)).
(* output: S (S O) *)
Compute (mul (S O) (S O)).
(* output: S O *)
Definition cases (A : Type) (a b : A) n :=
nat_rect _ a (fun _ _ => b) n.
Compute (cases nat O (S O) O).
(* output: O *)
Compute (cases nat O (S O) (S O)).
(* output: S O *)
(* zero is no successor *)
Lemma disjoint n :
O <> S n.
Proof.
intros H. change (cases Prop False True O).
rewrite H. simpl. auto.
Qed.
(* predecessor function *)
Definition pred n :=
nat_rect (fun _ => nat) O (fun m _ => m) n.
Lemma pred_S n :
pred (S n) = n.
Proof.
simpl. reflexivity.
Qed.
(* taking successors is injective *)
Lemma inject m n :
S m = S n -> m = n.
Proof.
intros H. rewrite <- (pred_S m).
rewrite H. apply pred_S.
Qed.
(* natural induction *)
Lemma induct (P : nat -> Prop) :
P O -> (forall n, P n -> P (S n)) -> (forall n, P n).
Proof.
apply nat_rect.
Qed.
(* inductive definition of non-strict ordering *)
Inductive le n : nat -> Prop :=
| le1 : le n n
| le2 m : le n m -> le n (S m).
Hint Resolve le1.
Notation "m <= n" := (le m n).
(* reflexivity *)
Lemma le_refl n :
n <= n.
Proof.
constructor.
Qed.
(* transitivity *)
Lemma le_trans n m s :
n <= m -> m <= s -> n <= s.
Proof.
intros H1 H2. induction H2.
- assumption.
- constructor. apply IHle.
Qed.
(* antisymmetry *)
Lemma le_pred n m :
S n <= S m -> n <= m.
Proof.
inversion 1; subst; trivial.
apply (le_trans n (S n)); trivial.
now constructor.
Qed.
Lemma le_anti n m :
n <= m -> m <= n -> n = m.
Proof.
revert m. induction n; intros [|m].
- reflexivity.
- inversion 2.
- inversion 1.
- repeat inversion 1; subst; trivial.
rewrite (IHn m); eauto using le_pred.
Qed.
(* linearity *)
Lemma le_O n :
O <= n.
Proof.
induction n; now constructor.
Qed.
Lemma le_succ n m :
n <= m -> S n <= S m.
Proof.
induction 1; now constructor.
Qed.
Lemma le_lin n m :
n <= m \/ m <= n.
Proof.
revert m. induction n; intros [|m].
- now left.
- left. apply le_O.
- right. apply le_O.
- destruct (IHn m) as [H|H].
+ left. now apply le_succ.
+ right. now apply le_succ.
Qed.
(* well-foundedness *)
Definition lt n m :=
S n <= m.
Notation "n < m" := (lt n m).
Inductive WF n : Prop :=
WFI : (forall m, m < n -> WF m) -> WF n.
Lemma le_wf n :
WF n.
Proof.
induction n; constructor.
- inversion 1.
- intros m. inversion 1; subst.
+ assumption.
+ now apply IHn.
Qed.