Skip to content

Commit

Permalink
Improving for coqdoc
Browse files Browse the repository at this point in the history
  • Loading branch information
@mk12
mk12 committed Dec 26, 2018
1 parent e1266f8 commit 0a0bf43
Show file tree
Hide file tree
Showing 2 changed files with 119 additions and 37 deletions.
137 changes: 106 additions & 31 deletions coq/Chapter2.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,75 +3,81 @@
(* Formalization of Analysis I: Chapter 2 *)
(******************************************************************************)

(** * Chapter 2: The natural numbers *)

Set Warnings "-notation-overridden".

Require Import Common.

(** Definition 2.1.1: The natural numbers *)
(** ** Section 2.1: The Peano axioms *)

(** *** Definition 2.1.1: The natural numbers *)
Inductive N : Set :=
| O : N
| S : N → N.

(** Axiom 2.1: 0 is a natural number *)
(** *** Axiom 2.1: 0 is a natural number *)
Goal N.
Proof O.

(** Axiom 2.2: Every natural number has a successor *)
(** *** Axiom 2.2: Every natural number has a successor *)
Goal N → N.
Proof S.

(** Definition 2.1.3: Arabic numerals are defined as natural numbers *)
(** *** Definition 2.1.3: Arabic numerals are defined as natural numbers *)
Fixpoint num (n : nat) : N :=
match n with
| Datatypes.O => O
| Datatypes.S m => S (num m)
end.

(** Proposition 2.1.4: 3 is a natural number *)
(** *** Proposition 2.1.4: 3 is a natural number *)
Goal N.
Proof num 3.

(** Axiom 2.3: 0 is not a successor of any natural number *)
(** *** Axiom 2.3: 0 is not a successor of any natural number *)
Theorem succ_ne_zero {n : N} : S n ≠ O.
Proof. discriminate. Qed.

(** Proposition 2.1.6: 4 is not equal to 0 *)
(** *** Proposition 2.1.6: 4 is not equal to 0 *)
Goal num 4 ≠ O.
Proof succ_ne_zero.

(** Axiom 2.4: Different natural numbers have different successors *)
(** *** Axiom 2.4: Different natural numbers have different successors *)
Theorem succ_inj {n m : N} (H : S n = S m) : n = m.
Proof. injection H. trivial. Qed.

(** Proposition 2.1.8: 6 is not equal to 2 *)
(** *** Proposition 2.1.8: 6 is not equal to 2 *)
Goal num 6 ≠ num 2.
Proof mt succ_inj (mt succ_inj succ_ne_zero).

(** Axiom 2.5: Principle of mathematical induction *)
(** *** Axiom 2.5: Principle of mathematical induction *)
Goal ∀ (p : N → Prop) (HO : p O) (HS : ∀ n : N, p n → p (S n)) (n : N), p n.
Proof.
induction n as [|n IHn].
- show (p O). exact HO.
- show (p (S n)). exact (HS n IHn).
Qed.

(** Proposition 2.1.16: Recursive definitions *)
(** *** Proposition 2.1.16: Recursive definitions *)
Definition recursive_def (f : N → N → N) (c : N) : N → N :=
fix a n :=
match n with
| O => c
| S m => f m (a m)
end.

(** Definition 2.2.1: Addition of natural numbers *)
(** ** Section 2.2: Addition *)

(** *** Definition 2.2.1: Addition of natural numbers *)
Fixpoint add (n m : N) : N :=
match n with
| O => m
| S n' => S (add n' m)
end.
Infix "+" := add.

(** Lemma 2.2.2 *)
(** *** Lemma 2.2.2 *)
Theorem add_zero_right {n : N} : n + O = n.
Proof.
induction n as [|n IHn].
Expand All @@ -81,7 +87,7 @@ Proof.
simpl. rewrite IHn. reflexivity.
Qed.

(** Lemma 2.2.3 *)
(** *** Lemma 2.2.3 *)
Theorem add_succ_right {n m : N} : n + S m = S (n + m).
Proof.
induction n as [|n IHn].
Expand All @@ -91,7 +97,7 @@ Proof.
simpl. rewrite IHn. reflexivity.
Qed.

(** Proposition 2.2.4: Addition is commutative *)
(** *** Proposition 2.2.4: Addition is commutative *)
Theorem add_comm {n m : N} : n + m = m + n.
Proof.
induction n as [|n IHn].
Expand All @@ -101,7 +107,7 @@ Proof.
simpl. rewrite add_succ_right, IHn. reflexivity.
Qed.

(** Proposition 2.2.5: Addition is associative *)
(** *** Proposition 2.2.5: Addition is associative *)
Theorem add_assoc {a b c : N} : (a + b) + c = a + (b + c).
Proof.
induction a as [|a IHa].
Expand All @@ -111,7 +117,7 @@ Proof.
simpl. rewrite IHa. reflexivity.
Qed.

(** Proposition 2.2.6: Cancellation law *)
(** *** Proposition 2.2.6: Cancellation law *)
Theorem add_cancel {a b c : N} (H : a + b = a + c) : b = c.
Proof.
induction a as [|a IHa].
Expand All @@ -126,14 +132,14 @@ Proof.
exact (add_cancel H).
Qed.

(** Add to both sides of an equation **)
(** Add to both sides of an equation *)
Theorem add_eqn {a b c d : N} (Hab : a = b) (Hcd : c = d) : a + c = b + d.
Proof. rewrite Hab, Hcd. reflexivity. Qed.

(** Definition 2.2.7: Positive natural numbers *)
(** *** Definition 2.2.7: Positive natural numbers *)
Definition pos (n : N) : Prop := n ≠ O.

(** Proposition 2.2.8 *)
(** *** Proposition 2.2.8 *)
Theorem add_pos {a b : N} (H : pos a) : pos (a + b).
Proof.
destruct b.
Expand All @@ -143,7 +149,7 @@ Proof.
rewrite add_succ_right. exact succ_ne_zero.
Qed.

(** Corollary 2.2.9 *)
(** *** Corollary 2.2.9 *)
Theorem add_eq_zero {a b : N} (H : a + b = O) : a = O ∧ b = O.
Proof.
destruct a.
Expand All @@ -153,17 +159,17 @@ Proof.
simpl in H. contradiction (succ_ne_zero H).
Qed.

(** Lemma 2.2.10 *)
(** *** Lemma 2.2.10 *)
Theorem pos_pred {a : N} (H : pos a): ∃ b : N, S b = a.
Proof.
destruct a.
- show (∃ b : N, S b = O).
contradiction H. reflexivity.
contradiction (H eq_refl).
- show (∃ b : N, S b = S a).
exists a. reflexivity.
Qed.

(** Definition 2.2.11: Ordering of the natural numbers *)
(** *** Definition 2.2.11: Ordering of the natural numbers *)
Definition le (n m : N) : Prop := ∃ a : N, m = n + a.
Definition lt (n m : N) : Prop := le n m ∧ n ≠ m.
Definition ge (n m: N) : Prop := le m n.
Expand All @@ -173,7 +179,7 @@ Infix "<" := lt.
Infix "≥" := ge.
Infix ">" := gt.

(** Proposition 2.2.12: Basic properties of order for natural numbers *)
(** *** Proposition 2.2.12: Basic properties of order for natural numbers *)
Section order_properties.
Context {a b c : N}.

Expand All @@ -193,8 +199,7 @@ Section order_properties.
intros [n Hn] [m Hm].
assert (n = O) as H0. {
rewrite Hn, add_assoc in Hm.
apply eq_sym, add_cancel_zero, add_eq_zero, proj1 in Hm.
exact Hm.
exact (proj1 (add_eq_zero (add_cancel_zero (eq_sym Hm)))).
}
rewrite Hn, H0, add_zero_right.
reflexivity.
Expand All @@ -203,10 +208,80 @@ Section order_properties.
Theorem ge_iff_add_ge : a ≥ b ↔ a + c ≥ b + c.
Proof.
split.
- intros [n Hn].
- show (a ≥ b → a + c ≥ b + c).
intros [n Hn].
exists n.
assert (a + c = b + n + c) as H0 by apply (add_eqn Hn eq_refl).
assert (a + c = b + n + c) as H0 by exact (add_eqn Hn eq_refl).
rewrite add_assoc, (@add_comm n c), <-add_assoc in H0.
exact H0.
- intros [n Hn].
End order_properties.
- show (a + c ≥ b + c → a ≥ b ).
intros [n Hn].
exists n.
rewrite add_assoc, (@add_comm c n), <-add_assoc in Hn.
rewrite (@add_comm a c), (@add_comm (b + n) c) in Hn.
exact (add_cancel Hn).
Qed.

Theorem lt_iff_pos : a < b ↔ ∃ d : N, b = a + d ∧ pos d.
Proof.
split.
- show (a < b → ∃ d : N, b = a + d ∧ pos d).
intros [[n Hn] HNab].
exists n.
split.
+ show (b = a + n).
exact Hn.
+ show (pos n).
intro HZn.
rewrite HZn, add_zero_right in Hn.
assert (a = b) as Hab by exact (symmetry Hn).
contradiction (HNab Hab).
- show ((∃ d : N, b = a + d ∧ pos d) → a < b).
intros [n [Hn HPn]].
split.
+ show (a ≤ b).
exists n. exact Hn.
+ show (a ≠ b).
intro Hab.
rewrite Hab in Hn.
assert (n = O) as HZn by exact (add_cancel_zero (eq_sym Hn)).
contradiction (HPn HZn).
Qed.

Theorem lt_iff_succ_le : a < b ↔ S a ≤ b.
Proof.
split.
- show (a < b → S a ≤ b).
intro HLT.
destruct (proj1 lt_iff_pos HLT) as [n [Hn HPn]].
destruct (pos_pred HPn) as [m Hm].
exists m.
rewrite <-Hm, add_succ_right in Hn.
exact Hn.
- show (S a ≤ b → a < b).
intros [n Hn].
split.
+ show (a ≤ b).
exists (S n). rewrite add_succ_right. exact Hn.
+ show (a ≠ b).
intro Hab.
rewrite Hab in Hn.
simpl in Hn.
rewrite <-add_succ_right in Hn.
contradiction (succ_ne_zero (add_cancel_zero (eq_sym Hn))).
Qed.

(** The following properties are not in the textbook. *)

Theorem lt_succ_iff_le : a < S b ↔ a ≤ b.
Proof.
split.
- show (a < S b → a ≤ b).
intro HLT.
(* Check @lt_iff_pos.
(* destruct (proj1 order_properties.lt_iff_pos HLT) as [[n Hn] HPn]. *) *)
admit.
- show (a ≤ b → a < S b).
admit.
Admitted.
End order_properties.
19 changes: 13 additions & 6 deletions coq/Common.v
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,26 @@
(******************************************************************************)
(* Copyright 2018 Mitchell Kember. Subject to the MIT License. *)
(* Formalization of Analysis I: Common theorems *)
(* Formalization of Analysis I: Common *)
(******************************************************************************)

(* Require Export Coq.Logic.Classical. *)
(** * Common *)

(** ** Libraries *)
Require Export Coq.Setoids.Setoid.
Require Export Coq.Unicode.Utf8.

(** Restate the current goal *)
(** ** Tactics *)

(** *** Restate the current goal *)
Ltac show G := tryif change G then idtac else fail 0 "Not the current goal".

(** Modus tollens *)
Theorem mt {p q : Prop} (Hpq : p → q) (Hnq : ¬ q) : ¬ p.
(** ** Theorems *)

(** *** Modus tollens *)
Theorem mt {p q : Prop} (Hpq : p → q) (HNq : ¬ q) : ¬ p.
Proof.
intro Hp.
contradiction Hnq.
contradiction HNq.
exact (Hpq Hp).
Qed.

0 comments on commit 0a0bf43

Please sign in to comment.