-
Notifications
You must be signed in to change notification settings - Fork 0
/
quotient.v
103 lines (97 loc) · 3.45 KB
/
quotient.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
Require Import Arith.
Require Import Lia.
Definition nonnegative_nat (n : nat) := n >= 0.
Definition positive_nat (n : nat) := n >= 1.
Theorem QPRIME_GE_Q: forall n q q' r r': nat,
positive_nat(n) /\ nonnegative_nat(q) /\ nonnegative_nat(q') /\ nonnegative_nat(r) /\ nonnegative_nat(r') /\ n * q + r = (n - 1) * q' + r' /\ n >= q + 2 /\ r < n /\ r' < n - 1 -> q' >= q.
Proof.
intros n q q' r r' H.
destruct (lt_eq_lt_dec q' q) as [[Hlt | Heq] | Hgt].
exfalso.
assert (q' <= q - 1) by (lia).
destruct (lt_eq_lt_dec q' 0) as [[Hqneg | Hqzero] | Hqpos].
exfalso.
easy.
assert (q = 1) by (lia).
assert (Hn: n < n) by (lia).
apply Nat.lt_irrefl in Hn.
contradiction.
assert ((n - 1) * q' <= (n - 1) * (q - 1)) by (apply Nat.mul_le_mono_nonneg_l; lia).
assert (Hr: r' < r') by (lia).
apply Nat.lt_irrefl in Hr.
contradiction.
rewrite Heq.
auto.
apply le_S_n.
apply le_S.
assumption.
Qed.
Theorem QPRIME_IS_AT_MOST_Q_PLUS_1: forall n q q' r r': nat,
positive_nat(n) /\ nonnegative_nat(q) /\ nonnegative_nat(q') /\ nonnegative_nat(r) /\ nonnegative_nat(r') /\ n * q + r = (n - 1) * q' + r' /\ n >= q + 2 /\ r < n /\ r' < n - 1 -> q' <= q + 1.
Proof.
intros n q q' r r' H.
pose (gap := q' - q).
assert (q' >= q) by (apply QPRIME_GE_Q in H; lia).
destruct (lt_eq_lt_dec 1 gap) as [[Hlt | Heq] | Hgt].
exfalso.
assert (q' >= q + 2) by (lia).
assert ((n - 1) * q' >= (n - 1) * (q + 2)) by (apply Nat.mul_le_mono_nonneg_l; lia).
assert (Hr: r > r) by (lia).
apply Nat.lt_irrefl in Hr.
contradiction.
lia.
lia.
Qed.
Theorem Q_MUST_BE_EITHER_Q_OR_Q_PLUS_1: forall q q': nat, q' >= q /\ q' <= q + 1 -> q' = q \/ q' = q + 1.
Proof.
lia.
Qed.
Theorem MAIN: forall n q q' r r' a b: nat,
nonnegative_nat(a) /\ nonnegative_nat(b) /\ positive_nat(n) /\ nonnegative_nat(q) /\ nonnegative_nat(q') /\ nonnegative_nat(r) /\ nonnegative_nat(r') /\ a * b = n * q + r
/\ a * b = (n - 1) * q' + r' /\ a < n /\ b < n /\ r < n /\ r' < n - 1 /\ n > 1 -> (r > r' -> r' = r + q + 1 - n) /\ (r <= r' -> r' = r + q).
Proof.
intros n q q' r r' a b H.
pose (product := a * b).
destruct (lt_eq_lt_dec product 0) as [[Hlt | Heq] | Hgt].
exfalso.
lia.
assert (q = 0 /\ r = 0 /\ q' = 0 /\ r' = 0 /\ r = r') by (lia).
split.
- lia.
- lia.
-
assert (a > 0 /\ b > 0) by (lia).
assert (b * a < b * n) by (apply Nat.mul_lt_mono_pos_l; lia).
assert (n * b < n * n) by (apply Nat.mul_lt_mono_pos_l; lia).
assert (n * q < n * n -> q < n) by (apply Nat.mul_lt_mono_pos_l; lia).
assert (n >= q + 1) by (lia).
pose (q_plus_one := q + 1).
destruct (lt_eq_lt_dec n q_plus_one) as [[Hlt2 | Heq2] | Hgt2].
-- exfalso. lia.
--
assert (a > 0 /\ a <= n - 1 /\ b > 0 /\ b <= n - 1) by (lia).
assert (a * b <= (n - 1) * b) by (apply Nat.mul_le_mono_pos_r; lia).
assert ((n - 1) * b <= (n - 1) * (n - 1)) by (apply Nat.mul_le_mono_pos_l; lia).
assert (n-1 <= 0) by (lia).
exfalso.
lia.
--
assert (n >= q + 2) by (lia).
assert (n * q + r = (n - 1) * q' + r') by (lia).
assert (q' <= q + 1).
apply QPRIME_IS_AT_MOST_Q_PLUS_1 with (n:=n) (r:=r) (r':=r').
easy.
assert (H8:q' = q \/ q' = q + 1).
apply Q_MUST_BE_EITHER_Q_OR_Q_PLUS_1.
split.
apply QPRIME_GE_Q with (n:=n) (r:=r) (r':=r').
easy.
easy.
destruct H8 as [H8a | H8b].
assert (r' = r + q /\ r <= r') by (lia).
split.
lia.
easy.
assert (r - n = r' - q - 1) by (lia).
lia.
Qed.