Guest User

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