# Untitled

a guest
Aug 22nd, 2019
65
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. import .power
2.
3. section order
4.
5. definition minimal_lt (P : ℕ → Prop) [decidable_pred P]
6. : ℕ → option (Σ' k : ℕ, P k)
7. | 0 := none
8. | (n+1) := minimal_lt n
9. <|> (if h' : P n then some ⟨n, h'⟩ else none)
10.
11. lemma option.alt_eq_none {α} : ∀ o o' : option α,
12. (o <|> o') = none ↔ o = none ∧ o' = none :=
13. by intros; cases o; cases o'; simp [(<|>), option.orelse]
14.
15. lemma option.alt_eq_some {α} : ∀ (o o' : option α) (a : α),
16. (o <|> o') = some a
17. ↔ o = some a ∨ (o = none ∧ o' = some a) :=
18. by intros; cases o; cases o'; simp [(<|>), option.orelse]
19.
20. lemma option.none_alt_eq_some {α} : ∀ (o : option α) (a : α),
21. (none <|> o) = some a ↔ o = some a := by intros; rw option.alt_eq_some; simp
22.
23. lemma minimal_lt_spec1 {P : ℕ → Prop} [decidable_pred P]
24. : ∀ n, minimal_lt P n = none ↔ (∀ k < n, ¬ P k) :=
25. begin
26. intro, induction n with n ih; simp [minimal_lt],
27. case nat.zero { intros k hk, cases hk },
28. case nat.succ {
29. rw option.alt_eq_none,
30. by_cases P n,
31. { rw dif_pos h, rw ih, simp, intro hneg,
32. specialize hneg n _ h, assumption, apply nat.lt_succ_self, },
33. { rw dif_neg h, rw ih, simp, constructor; intro h',
34. { intro k, by_cases k < n, intro _, apply h', assumption,
35. intro h'', cases eq_or_lt_of_not_lt h, rw h_1, assumption,
36. exfalso, cases h'', apply nat.lt_irrefl _ h_1,
37. apply h, assumption },
38. { intros, apply h', transitivity, assumption, apply nat.lt_succ_self } } }
39. end
40.
41. lemma minimal_lt_spec2 {P : ℕ → Prop} [decidable_pred P]
42. : ∀ n k h, minimal_lt P n = some ⟨k, h⟩
43. ↔ (k < n ∧ (∀ j, j < k → ¬ P j)) :=
44. begin
45. intros n, induction n with n ih; intros k h; simp [minimal_lt],
46. { intro h, cases h, apply nat.not_lt_zero, assumption },
47. { destruct minimal_lt P n,
48. { intro H, rw H,
49. rw minimal_lt_spec1 at H,
50. rw option.none_alt_eq_some,
51. by_cases P n,
52. { rw dif_pos h, transitivity n = k,
53. { constructor; intro h, cases h, refl, congr, assumption },
54. { constructor; intro h,
55. constructor, rw h, apply nat.lt_succ_self,
56. intros j hj, rw ← h at hj, apply H, assumption,
57. cases h, cases h_left, refl,
58. exfalso, apply H k; assumption } },
59. { rw dif_neg h, simp, intro h',
60. cases h', cases h'_left, contradiction,
61. apply H, assumption, assumption } },
62. { intros val hval, cases val with j hj,
63. rw hval, rw ih at hval, simp [(<|>), option.orelse],
64. transitivity j = k,
65. { constructor; intro h; cases h, assumption, constructor; refl },
66. constructor; intro h,
67. { subst h, constructor,
68. { transitivity n, exact hval.left, apply nat.lt_succ_self },
69. exact hval.right },
70. { cases nat.lt_trichotomy j k,
71. { exfalso, apply h.right; assumption },
72. cases h_1, assumption,
73. { exfalso, apply hval.right; assumption } } } }
74. end
75.
76.
77. def dec_order {G} [group G] [decidable_eq G] (g : G) (bound : ℕ) (hgt : bound > 0) (h : g^bound = 1) : ℕ :=
78. option.get_or_else (option.map psigma.fst (minimal_lt (λ k, k > 0 ∧ g^k = 1) (bound + 1))) bound
79.
80. lemma dec_order_spec {G} [group G] [decidable_eq G] (g : G) (bound : ℕ) (hgt : bound > 0) (h : g^bound = 1)
81. : dec_order g bound hgt h ≤ bound
82. ∧ 0 < dec_order g bound hgt h
83. ∧ (g^(dec_order g bound hgt h) = 1)
84. ∧ (∀ j, j < dec_order g bound hgt h → g^j = 1 → j = 0) :=
85. begin
86. destruct minimal_lt (λ (k : ℕ), k > 0 ∧ g ^ k = 1) (bound + 1),
87. { simp [dec_order],
88. intro h', rw h', rw minimal_lt_spec1 at h',
89. exfalso, apply h', apply nat.lt_succ_self, constructor; assumption },
90. { intros val hval, cases val with n hn, cases hn with hngt hn,
91. have : dec_order g bound hgt h = n,
92. { simp [dec_order], rw hval, simp [option.map, option.bind, option.get_or_else] },
93. rw this, rw minimal_lt_spec2 at hval, constructor,
94. { apply nat.le_of_lt_succ, exact hval.left },
95. { constructor, assumption, constructor, assumption, intros j hjlt hj,
96. suffices : ¬ j > 0,
97. { cases nat.zero_le j, refl, exfalso, apply this, apply nat.zero_lt_succ },
98. suffices : ¬(j > 0 ∧ g ^ j = 1),
99. { rw decidable.not_and_iff_or_not at this, cases this, assumption, contradiction },
100. apply hval.right, assumption } }
101. end
102.
103. section classical
104.
105. inductive order {G} [group G] (g : G)
106. | infinite : (∀ n : ℕ, g^n = 1 → n = 0) → order
107. | finite : ∀ n : ℕ, 0 < n → g^n = 1 → (∀ k : ℕ, k < n → g^k = 1 → k = 0) → order
108.
109. local attribute [instance] classical.prop_decidable
110.
111. def power_zero_of_no_finite_order {G} [group G] (g : G)
112. (h : ¬∃ (n : ℕ), n > 0 ∧ g ^ n = 1) (n : ℕ) (h' : g ^ n = 1) : n = 0 :=
113. begin
114. by_contra, apply h, existsi n,
115. constructor, apply nat.lt_of_le_and_ne,
116. apply nat.zero_le, apply ne.symm, assumption, assumption
117. end
118.
119. def no_infinite_order_of_finite_order {G} [group G] (g : G)
120. (h : ∃ (n : ℕ), n > 0 ∧ g ^ n = 1) : ¬ ∀ (n : ℕ) (h' : g ^ n = 1), n = 0 :=
121. begin
122. intro h', cases h with n hn, cases hn with hgt hn,
123. rw h' n hn at hgt, apply nat.lt_irrefl _ hgt
124. end
125.
126. noncomputable def classical.order {G} [group G] (g : G) : order g :=
127. if h : ∃ n, n > 0 ∧ g^n = 1
128. then order.finite (dec_order g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right)
129. (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.left
130. (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.left
131. (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.right
132. else order.infinite \$ power_zero_of_no_finite_order g h
133.
134. noncomputable def classical.order' {G} [group G] (g : G) : ℕ :=
135. match classical.order g with
136. | order.infinite _ := 0
137. | order.finite n _ _ _ := n
138. end
139.
140. lemma classical.order'_spec1 {G} [group G] (g : G)
141. : classical.order' g = 0 ↔ ∀ n, g^n = 1 → n = 0 :=
142. begin
143. dsimp [classical.order', classical.order],
144. by_cases h : ∃ n, n > 0 ∧ g^n = 1,
145. { rw dif_pos h, simp [classical.order'._match_1],
146. transitivity false,
147. { rw iff_false, rw (_ : ∀ n, ¬ (n = 0) ↔ 0 < n),
148. apply and.left (and.right (dec_order_spec g _ _ _)),
149. intro n; cases n, simp *, apply nat.lt_irrefl,
150. transitivity true, rw iff_true, apply nat.succ_ne_zero,
151. rw true_iff, apply nat.zero_lt_succ },
152. { rw false_iff, apply no_infinite_order_of_finite_order g h, } },
153. { rw dif_neg h, simp [classical.order'._match_1],
154. apply power_zero_of_no_finite_order g h }
155. end
156.
157. lemma classical.order'_spec2 {G} [group G] (g : G)
158. : ∀ n, 0 < n → (classical.order' g = n
159. ↔ g^n = 1 ∧ (∀ k : ℕ, k < n → g^k = 1 → k = 0)) :=
160. begin
161. intros n hn,
162. dsimp [classical.order', classical.order],
163. by_cases h : ∃ n, n > 0 ∧ g^n = 1,
164. { rw dif_pos h, simp [classical.order'._match_1],
165. constructor, { intro h, subst h, apply (dec_order_spec g _ _ _).right.right },
166. intro h', cases nat.lt_trichotomy _ n,
167. tactic.swap, cases h_1, exact h_1,
168. { suffices : n = 0, { exfalso, rw this at hn, apply nat.lt_irrefl _ hn },
169. apply (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.right,
170. assumption, exact h'.left },
171. { suffices : dec_order g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right = 0,
172. have this' := (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.left,
173. rw this at this', exfalso, apply nat.lt_irrefl _ this',
174. apply h'.right, assumption, apply (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.left } },
175. { rw dif_neg h, simp [classical.order'._match_1], transitivity false,
176. { rw iff_false, intro h, rw h at hn, apply nat.lt_irrefl _ hn },
177. { rw false_iff, intro h', apply h,
178. existsi n, constructor, assumption, exact h'.left } }
179. end
180.
181. end classical
182.
183. def cyclic_subgroup {G} [group G] (g : G) : set G :=
184. { h : G | ∃ n : ℤ, h = g^^n }
185.
186. end order
RAW Paste Data