-
Notifications
You must be signed in to change notification settings - Fork 0
/
chapter2.v
122 lines (103 loc) · 2.64 KB
/
chapter2.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
Require Import Coq.Arith.PeanoNat.
Theorem l_one : forall m n : nat,
m <> n -> S m <> S n.
Proof.
auto.
Qed.
Theorem l_two : forall n : nat,
S n <> n.
Proof.
intros n.
induction n as [| n' Hn'].
- unfold not. discriminate.
- apply (l_one (S n') n'). assumption.
Qed.
Theorem l_three : forall x : nat,
x <> 1 -> exists u : nat, x <> S u.
Proof.
intros x H.
induction x as [| x' Hx'].
- exists 0. unfold not. discriminate.
- exists 0. apply H.
Qed.
Theorem l_four_a : forall x : nat,
x + 1 = S x.
Proof.
intros. induction x as [| x' Hx'].
- compute. reflexivity.
- simpl. rewrite Hx'. reflexivity.
Qed.
Theorem l_four_b : forall x y : nat,
x + (S y) = S (x + y).
Proof.
intros. induction x as [| x' Hx'].
- simpl. reflexivity.
- simpl. rewrite <- Hx'. reflexivity.
Qed.
Theorem l_five : forall x y z : nat,
(x + y) + z = x + (y + z).
Proof.
intros. induction x as [| x' Hx'].
- simpl. reflexivity.
- simpl. rewrite Hx'. reflexivity.
Qed.
Theorem plus_x_O : forall x : nat,
x = x + 0.
Proof.
intros. induction x as [| x' Hx'].
- reflexivity.
- simpl. rewrite <- Hx'. reflexivity.
Qed.
Theorem plus_n_Sm : forall x y : nat,
S (x + y) = x + S y.
Proof.
intros. induction x as [| x' Hx'].
- simpl. reflexivity.
- simpl. rewrite Hx'. reflexivity.
Qed.
Theorem l_six : forall x y : nat,
x + y = y + x.
Proof.
intros. induction x as [| x' Hx'].
- simpl. rewrite <- plus_x_O. reflexivity.
- simpl. rewrite Hx'. rewrite plus_n_Sm. reflexivity.
Qed.
Theorem ineq_x_0 : forall x : nat,
x <> 0 -> 0 <> x.
Proof.
intros. induction x as [| x' Hx'].
- contradiction.
- simpl. auto.
Qed.
(* Landau's nat starts at 1 so I had to add the extra
implication x <> 0 for this to work *)
Theorem l_seven : forall x y : nat,
x <> 0 -> y <> x + y.
Proof.
intros. induction y as [| y' Hy'].
- simpl. rewrite l_six. simpl. apply ineq_x_0. assumption.
- rewrite <- plus_n_Sm. apply (l_one y' (x + y')). assumption.
Qed.
Theorem l_eight : forall x y z : nat,
y <> z -> x + y <> x + z.
Proof.
intros. induction x as [| x' Hx'].
- simpl. assumption.
- simpl. apply (l_one (x' + y) (x' + z)). assumption.
Qed.
(* Had to change a bit the proposition here *)
Theorem l_nine_a : forall x y : nat,
x = y -> (exists u : nat, x <> y + u) /\ (exists v : nat, y <> x + v).
Proof.
intros x y H.
split.
exists 1. rewrite <- H.
simpl. rewrite l_four_a. auto.
exists 1. rewrite <- H.
simpl. rewrite l_four_a. auto.
Qed.
Theorem l_nine_b : forall x y : nat,
(exists u : nat, x = y + u) -> (x <> y) /\ (exists v : nat, y <> x + v).
Proof.
intros x y H.
Qed.