A mechanisation of Peano arithmetic theorems in Coq

peano.v

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

Theorem zero_no_succ: forall n, S n <> O.
Proof. intros. unfold not. intro H0. inversion H0. Qed.

Theorem succ_eq_succ: forall m n, S m = S n -> m = n.
Proof. intros. inversion H. reflexivity. Qed.

Theorem n_neq_succ: forall n, n <> S n.
Proof. intros. intro H. induction n. inversion H.
apply succ_eq_succ in H. apply IHn. apply H. Qed.

Theorem nonzero_has_pred: forall n: nat, n <> O -> exists m, (S m) = n.
Proof. intros. destruct n. contradiction. exists n. reflexivity. Qed.

Inductive leq: nat -> nat -> Prop :=
| leq_eq: forall n, leq n n
| leq_succ: forall n m, leq n m -> leq n (S m).

Theorem n_leq_succ_n: forall n, leq n (S n).
Proof. intro n. apply leq_succ. apply leq_eq. Qed.

Theorem zero_leq_zero: forall n, leq n O -> n = O.
Proof. intros. inversion H. reflexivity. Qed.

Theorem zero_leq: forall n, leq O n.
Proof. intro n. induction n. apply leq_eq. apply leq_succ. apply IHn. Qed.

Fixpoint plus (n m: nat) : nat :=
match m with | O => n | S p => S (plus n p) end.

Theorem one_plus_n: forall n, plus (S O) n = S n.
Proof. induction n. simpl. reflexivity. simpl.
rewrite IHn. reflexivity. Qed.

Theorem right_identity_plus: forall n, plus n O = n.
Proof. simpl. reflexivity. Qed.

Theorem left_identity_plus: forall n, plus O n = n.
Proof. induction n. simpl. reflexivity. simpl.
rewrite IHn. reflexivity. Qed.

Theorem plus_associative: forall m n p, plus (plus m n) p = plus m (plus n p).
Proof. induction p. simpl. reflexivity. simpl.
rewrite IHp. reflexivity. Qed.

Lemma successor_shift: forall m n, plus m (S n) = plus (S m) n.
Proof. induction n. simpl. reflexivity. simpl.
rewrite <- IHn. simpl. reflexivity. Qed.

Theorem plus_commutative: forall m n, plus m n = plus n m.
Proof. induction n. rewrite left_identity_plus.
apply right_identity_plus. simpl. rewrite IHn.
apply successor_shift. Qed.

Theorem plus_cancellative: forall m n p, plus m n = plus m p -> n = p.
Proof. intros. induction m. rewrite ?left_identity_plus in H.
apply H. apply IHm. rewrite <- ?successor_shift in H.
simpl in H. apply succ_eq_succ. apply H. Qed.

Theorem leq_plus: forall n p, leq n (plus n p).
Proof. intros. induction p. simpl. apply leq_eq.
apply leq_succ in IHp. simpl. apply IHp. Qed.

Theorem plus_zero_zero: forall m n, plus m n = O -> m = O /\ n = O.
Proof. intros. destruct n, m. auto. all: discriminate H. Qed.

Definition I := S O.

Fixpoint mul (n m: nat) : nat :=
match m with | O => O | S p => plus (mul n p) n end.

Theorem right_annihilator_mul: forall n, mul n O = O.
Proof. intro n. simpl. reflexivity. Qed.

Theorem left_annihilator_mul: forall n, mul O n = O.
Proof. intro n. induction n. simpl.
reflexivity. simpl. apply IHn. Qed.

Theorem right_identity_mul: forall n, mul n I = n.
Proof. intro n. simpl. apply left_identity_plus. Qed.

Theorem left_identity_mul: forall n, mul I n = n.
Proof. intro n. induction n. apply right_annihilator_mul.
simpl. rewrite IHn. reflexivity. Qed.

Theorem mp_distributive: forall m n p, mul (plus m n) p = plus (mul m p) (mul n p).
Proof. induction p. apply right_annihilator_mul. simpl.
rewrite IHp. rewrite ?plus_associative.
rewrite <- (plus_associative (mul n p) m n).
rewrite <- (plus_associative m (mul n p) n).
rewrite (plus_commutative m (mul n p)).
reflexivity. Qed.

Theorem mul_commutative: forall m n, mul m n = mul n m.
Proof. intros. induction m. simpl. apply left_annihilator_mul. simpl.
rewrite <- one_plus_n. rewrite mp_distributive.
rewrite left_identity_mul.
rewrite IHm. apply (plus_commutative n (mul n m)). Qed.

Theorem mul_associative: forall m n p, mul (mul m n) p = mul m (mul n p).
Proof. induction p. simpl. reflexivity. simpl. rewrite IHp.
rewrite (mul_commutative m (plus (mul n p) n)).
rewrite (mp_distributive (mul n p) n m).
rewrite (mul_commutative m (mul n p)).
rewrite (mul_commutative m n). reflexivity. Qed.

Theorem mul_zero_zero: forall m n, mul m n = O -> m = O \/ n = O.
Proof. intros. destruct m, n. all: auto. discriminate H. Qed.

Theorem leq_transitive: forall m n p, leq m n /\ leq n p -> leq m p.
Proof. intros. destruct H. induction H0. apply H. apply leq_succ. auto. Qed.

Theorem leq_addition: forall m n, leq m n -> exists p, plus m p = n.
Proof. intros. induction n.
inversion H. exists O. apply left_identity_plus.
inversion H. exists O. apply right_identity_plus.
destruct IHn. apply H2. exists (S x). simpl. rewrite H3. reflexivity. Qed.

Lemma leq_succ_neg: forall n, leq (S n) n -> False.
Proof. intros. apply leq_addition in H. destruct H.
rewrite <- successor_shift in H. rewrite <- right_identity_plus in H.
apply (plus_cancellative n (S x) O) in H. inversion H. Qed.

Theorem leq_antisymmetric: forall m n, leq m n /\ leq n m -> m = n.
Proof. intros. destruct H. induction H. reflexivity.
assert (leq (S m) m). apply (leq_transitive (S m) n m). auto.
apply leq_succ_neg in H1. contradiction. Qed.

Theorem addition_leq: forall m n, (exists p, plus m p = n) -> leq m n.
Proof. intros. destruct H. rewrite <- H. apply leq_plus. Qed.

Theorem leq_connex: forall m n, leq m n \/ leq n m.
Proof. intros. induction n. right. apply zero_leq.
destruct IHn. left. apply leq_succ. apply H.
apply leq_addition in H. inversion H. destruct x.
left. rewrite <- H0. simpl. apply n_leq_succ_n.
right. apply addition_leq. exists x. rewrite <- successor_shift.
apply H0. Qed.

Theorem plus_preserves_leq: forall a b c, leq a b -> leq (plus a c) (plus b c).
Proof. intros. apply leq_addition in H. apply addition_leq.
inversion H. exists x. rewrite (plus_commutative a c).
rewrite plus_associative. rewrite H0. rewrite plus_commutative.
reflexivity. Qed.

Theorem mul_preserves_leq: forall a b c, leq a b -> leq (mul a c) (mul b c).
Proof. intros. apply leq_addition in H. apply addition_leq.
inversion H. exists (mul x c). rewrite <- mp_distributive.
rewrite H0. reflexivity. Qed.

Theorem mul_cancellative: forall m n p, mul m (S p) = mul n (S p) -> m = n.
Proof. induction m; destruct n; intro p. auto.
rewrite left_annihilator_mul. intro.
symmetry in H. apply mul_zero_zero in H. destruct H. auto. inversion H.
rewrite left_annihilator_mul. intro.
apply mul_zero_zero in H. destruct H. auto. inversion H.
simpl. intro. apply succ_eq_succ in H.
rewrite mul_commutative in H. simpl in H.
rewrite (plus_commutative (mul p m) p) in H. rewrite plus_associative in H.
rewrite (mul_commutative (S n) p) in H. simpl in H.
rewrite (plus_commutative (mul p n) p) in H. rewrite plus_associative in H.
apply plus_cancellative in H.
rewrite mul_commutative in H. rewrite (mul_commutative p n) in H.
simpl in IHm. apply IHm in H.
rewrite H. reflexivity. Qed.