import .power

section order

definition minimal_lt (P : ℕ → Prop) [decidable_pred P]
  : ℕ → option (Σ' k : ℕ, P k)
| 0 := none
| (n+1) := minimal_lt n
        <|> (if h' : P n then some ⟨n, h'⟩ else none)

lemma option.alt_eq_none {α} : ∀ o o' : option α,
  (o <|> o') = none ↔ o = none ∧ o' = none :=
by intros; cases o; cases o'; simp [(<|>), option.orelse]

lemma option.alt_eq_some {α} : ∀ (o o' : option α) (a : α),
  (o <|> o') = some a
  ↔ o = some a ∨ (o = none ∧ o' = some a) :=
by intros; cases o; cases o'; simp [(<|>), option.orelse]

lemma option.none_alt_eq_some {α} : ∀ (o : option α) (a : α),
  (none <|> o) = some a ↔ o = some a := by intros; rw option.alt_eq_some; simp

lemma minimal_lt_spec1 {P : ℕ → Prop} [decidable_pred P]
  : ∀ n, minimal_lt P n = none ↔ (∀ k < n, ¬ P k) :=
begin
  intro, induction n with n ih; simp [minimal_lt],
  case nat.zero { intros k hk, cases hk },
  case nat.succ {
    rw option.alt_eq_none,
    by_cases P n,
    { rw dif_pos h, rw ih, simp, intro hneg,
      specialize hneg n _ h, assumption, apply nat.lt_succ_self, },
    { rw dif_neg h, rw ih, simp, constructor; intro h',
      { intro k, by_cases k < n, intro _, apply h', assumption,
        intro h'', cases eq_or_lt_of_not_lt h, rw h_1, assumption,
        exfalso, cases h'', apply nat.lt_irrefl _ h_1,
        apply h, assumption },
      { intros, apply h', transitivity, assumption, apply nat.lt_succ_self } } }
end

lemma minimal_lt_spec2 {P : ℕ → Prop} [decidable_pred P]
  : ∀ n k h, minimal_lt P n = some ⟨k, h⟩
           ↔ (k < n ∧ (∀ j, j < k → ¬ P j)) :=
begin
  intros n, induction n with n ih; intros k h; simp [minimal_lt],
  { intro h, cases h, apply nat.not_lt_zero, assumption },
  { destruct minimal_lt P n,
    { intro H, rw H,
      rw minimal_lt_spec1 at H,
      rw option.none_alt_eq_some,
      by_cases P n,
      { rw dif_pos h, transitivity n = k,
        { constructor; intro h, cases h, refl, congr, assumption },
        { constructor; intro h,
          constructor, rw h, apply nat.lt_succ_self,
          intros j hj, rw ← h at hj, apply H, assumption,
          cases h, cases h_left, refl,
          exfalso, apply H k; assumption } },
      { rw dif_neg h, simp, intro h',
        cases h', cases h'_left, contradiction,
        apply H, assumption, assumption } },
    { intros val hval, cases val with j hj,
      rw hval, rw ih at hval, simp [(<|>), option.orelse],
      transitivity j = k,
      { constructor; intro h; cases h, assumption, constructor; refl },
      constructor; intro h,
      { subst h, constructor,
        { transitivity n, exact hval.left, apply nat.lt_succ_self },
        exact hval.right },
      { cases nat.lt_trichotomy j k,
        { exfalso, apply h.right; assumption },
        cases h_1, assumption,
        { exfalso, apply hval.right; assumption } } } }
end


def dec_order {G} [group G] [decidable_eq G] (g : G) (bound : ℕ) (hgt : bound > 0) (h : g^bound = 1) : ℕ :=
option.get_or_else (option.map psigma.fst (minimal_lt (λ k, k > 0 ∧ g^k = 1) (bound + 1))) bound

lemma dec_order_spec {G} [group G] [decidable_eq G] (g : G) (bound : ℕ) (hgt : bound > 0) (h : g^bound = 1)
  : dec_order g bound hgt h ≤ bound
  ∧ 0 < dec_order g bound hgt h
  ∧ (g^(dec_order g bound hgt h) = 1)
  ∧ (∀ j, j < dec_order g bound hgt h → g^j = 1 → j = 0) :=
begin
  destruct minimal_lt (λ (k : ℕ), k > 0 ∧ g ^ k = 1) (bound + 1),
  { simp [dec_order],
    intro h', rw h', rw minimal_lt_spec1 at h',
    exfalso, apply h', apply nat.lt_succ_self, constructor; assumption },
  { intros val hval, cases val with n hn, cases hn with hngt hn,
    have : dec_order g bound hgt h = n,
    { simp [dec_order],  rw hval, simp [option.map, option.bind, option.get_or_else] },
    rw this, rw minimal_lt_spec2 at hval, constructor,
    { apply nat.le_of_lt_succ, exact hval.left },
    { constructor, assumption, constructor, assumption, intros j hjlt hj,
      suffices : ¬ j > 0,
      { cases nat.zero_le j, refl, exfalso, apply this, apply nat.zero_lt_succ },
      suffices : ¬(j > 0 ∧ g ^ j = 1),
      { rw decidable.not_and_iff_or_not at this, cases this, assumption, contradiction },
      apply hval.right, assumption } }
end

section classical

inductive order {G} [group G] (g : G)
| infinite : (∀ n : ℕ, g^n = 1 → n = 0) → order
| finite : ∀ n : ℕ, 0 < n → g^n = 1 → (∀ k : ℕ, k < n → g^k = 1 → k = 0) → order

local attribute [instance] classical.prop_decidable

def power_zero_of_no_finite_order {G} [group G] (g : G)
  (h : ¬∃ (n : ℕ), n > 0 ∧ g ^ n = 1) (n : ℕ) (h' : g ^ n = 1) : n = 0 :=
begin
  by_contra, apply h, existsi n,
  constructor, apply nat.lt_of_le_and_ne,
  apply nat.zero_le, apply ne.symm, assumption, assumption
end

def no_infinite_order_of_finite_order {G} [group G] (g : G)
  (h : ∃ (n : ℕ), n > 0 ∧ g ^ n = 1) : ¬ ∀ (n : ℕ) (h' : g ^ n = 1), n = 0 :=
begin
  intro h', cases h with n hn, cases hn with hgt hn,
  rw h' n hn at hgt, apply nat.lt_irrefl _ hgt
end

noncomputable def classical.order {G} [group G] (g : G) : order g :=
if h : ∃ n, n > 0 ∧ g^n = 1
then order.finite (dec_order g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right)
                  (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.left
                  (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.left
                  (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.right
else order.infinite $ power_zero_of_no_finite_order g h

noncomputable def classical.order' {G} [group G] (g : G) : ℕ :=
match classical.order g with
| order.infinite _ := 0
| order.finite n _ _ _ := n
end

lemma classical.order'_spec1 {G} [group G] (g : G)
  : classical.order' g = 0 ↔ ∀ n, g^n = 1 → n = 0 :=
begin
  dsimp [classical.order', classical.order],
  by_cases h : ∃ n, n > 0 ∧ g^n = 1,
  { rw dif_pos h, simp [classical.order'._match_1],
    transitivity false,
    { rw iff_false, rw (_ : ∀ n, ¬ (n = 0) ↔ 0 < n),
      apply and.left (and.right (dec_order_spec g _ _ _)),
      intro n; cases n, simp *, apply nat.lt_irrefl,
      transitivity true, rw iff_true, apply nat.succ_ne_zero,
      rw true_iff, apply nat.zero_lt_succ },
    { rw false_iff, apply no_infinite_order_of_finite_order g h, } },
  { rw dif_neg h, simp [classical.order'._match_1],
    apply power_zero_of_no_finite_order g h }
end

lemma classical.order'_spec2 {G} [group G] (g : G)
  : ∀ n, 0 < n → (classical.order' g = n
                 ↔ g^n = 1 ∧ (∀ k : ℕ, k < n → g^k = 1 → k = 0)) :=
begin
  intros n hn,
  dsimp [classical.order', classical.order],
  by_cases h : ∃ n, n > 0 ∧ g^n = 1,
  { rw dif_pos h, simp [classical.order'._match_1],
     constructor, { intro h, subst h, apply (dec_order_spec g _ _ _).right.right },
     intro h', cases nat.lt_trichotomy _ n,
     tactic.swap, cases h_1, exact h_1,
     { suffices : n = 0, { exfalso, rw this at hn, apply nat.lt_irrefl _ hn },
       apply (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.right.right,
       assumption, exact h'.left },
     { suffices : dec_order g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right = 0,
       have this' := (dec_order_spec g (classical.some h) (classical.some_spec h).left (classical.some_spec h).right).right.left,
       rw this at this', exfalso, apply nat.lt_irrefl _ this',
       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 } },
  { rw dif_neg h, simp [classical.order'._match_1], transitivity false,
    { rw iff_false, intro h, rw h at hn, apply nat.lt_irrefl _ hn },
    { rw false_iff, intro h', apply h,
      existsi n, constructor, assumption, exact h'.left } }
end

end classical

def cyclic_subgroup {G} [group G] (g : G) : set G :=
  { h : G | ∃ n : ℤ, h = g^^n }

end order