SHARE
TWEET

Untitled

a guest Aug 22nd, 2019 59 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
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top