import data.real.basic

namespace sfu2023
-- https://www.sfu.ca/~jlevinso/teaching/lean/jl2023.lean
-- solutions: -- https://www.sfu.ca/~jlevinso/teaching/lean/jl2023_solutions.lean

/-!
## A warmup exercise
-/

example (p q r : Prop) 
  (hpr : p → r) (hqp : q → p) : q → r :=
begin
  intro hq,  -- Assume we know q. We want to show r.
  apply hpr, -- Since p implies r, it suffices to show p.
  apply hqp, -- Since q implies p, it suffices to show q.
  exact hq,  -- We have a proof of q (hq).
end

/- Use this lemma: -/
#check add_le_add 
-- add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d

example (x y z : ℕ) : (x ≤ 5) → (1 ≤ y) → (x + 1 ≤ y + 5) :=
begin
  intros hx hy,
  rw add_comm y 5,
  apply add_le_add,
  exact hx,
  exact hy,
end


/-- ## A real analysis exercise -/

/- The standard definition of 
convergence of a real-valued sequence. -/
def converges_to (a : ℕ → ℝ) (l : ℝ) : Prop :=
∀ (ε : ℝ) (hε : ε > 0),
∃ (n : ℕ), ∀ (m : ℕ) (hm : n ≤ m), |a m - l| < ε

/--
Let's prove:
  If aₙ converges to l and bₙ converges to s, 
  then aₙ + bₙ converges to l + s.

-- Human proof ("ε/2 argument") :
Let `ε > 0`.
Since aₙ converges to l, we can find `N₁` such that, 
for all n ≥ N₁, |aₙ - l| < ε/2.

Similarly, we can find `N₂` such that, 
for all n ≥ N₂, |bₙ - s| < ε/2.

Let's take `N := max(N₁, N₂)`. 
Suppose m ≥ N (so m ≥ N₁ and m ≥ N₂). 
Then, by the triangle inequality,
|(aₙ + bₙ) - (l + s)| = |(aₙ - l) + (bₙ - s)|
                  ... ≤ |aₙ - l| + |bₙ - s|
                  ... < ε/2 + ε/2 = ε. □

Here's the Lean proof:
-/

lemma converges_to_of_add 
  (a b : ℕ → ℝ) (l₁ l₂ : ℝ)
  (ha : converges_to a l₁) (hb : converges_to b l₂) :
converges_to (a + b) (l₁ + l₂) :=
begin
  unfold converges_to at *,
  -- Let ε > 0.
  intros ε hε,
  -- Obtain N1 and N2.
  specialize ha (ε/2) (by linarith),
  obtain ⟨N1, hN1⟩ := ha,
  specialize hb (ε/2) (by linarith),
  obtain ⟨N2, hN2⟩ := hb,
  -- Use N = max(N1, N2).
  use max N1 N2,
  -- Suppose m ≥ N.
  intros m hm,
  rw max_le_iff at hm,
  specialize hN1 m hm.1,
  specialize hN2 m hm.2,
  -- Calculate!
  calc |(a + b) m - (l₁ + l₂)| = |a m + b m - (l₁ + l₂)|   : by refl
                           ... = |(a m - l₁) + (b m - l₂)| : by { congr, ring }
                           ... ≤ |a m - l₁| + |b m - l₂|   : abs_add (a m - l₁) (b m - l₂)
                           ... < ε/2 + ε/2                 : by linarith
                           ... = ε                         : by linarith,
end





/-
For last step of proof:
  calc |(a + b) m - (l₁ + l₂)| = |a m + b m - (l₁ + l₂)|   : sorry
                           ... = |(a m - l₁) + (b m - l₂)| : sorry
                           ... ≤ |a m - l₁| + |b m - l₂|   : sorry
                           ... < ε/2 + ε/2                 : sorry
                           ... = ε                         : sorry,
-/

def continuous_at (f : ℝ → ℝ) (x : ℝ) : Prop :=
∀ (ε : ℝ) (hε : ε > 0),
∃ (δ : ℝ) (hδ : δ > 0),
∀ (y : ℝ), |x - y| < δ → |f x - f y| < ε

def continuous (f : ℝ → ℝ) : Prop :=
∀ x, continuous_at f x



/-- ## An abstract algebra exercise
Let's define groups. What is a group?

It consists of some data:
  - An __underlying type__ G (underlying set),
  - a  __binary operation__ ** : G × G → G,
  - an __identity element__ e : G,
  - and an __inversion operation__ inv : G → G,
and some facts:
  - ... satisfying the axioms of associativity, identity, inverses.

This is a new kind (type) of object since it bundles three definitions 
(*, e, ⁻¹) and several propositions (the group axioms).
-/

/- A type with a binary operation, satisfying no axioms. -/
class has_mul (X : Type) :=
(mul : X → X → X)

infix ` ** `:1000 := has_mul.mul 
-- Now we can write a ** b.

/- Definition of a group! -/
class group (G : Type) extends has_mul G :=
(e : G) -- identity element
(inv : G → G)
(mul_assoc : ∀ g1 g2 g3 : G, (g1 ** g2) ** g3 = g1 ** (g2 ** g3))
(left_identity : ∀ g, e ** g = g)
(right_identity : ∀ g, g ** e = g)
(left_inv : ∀ g, inv g ** g = e)
(right_inv : ∀ g, g ** inv g = e)


/-- ## Examples of groups!

## 1. The group structure on the power set of X, 
## by the symmetric difference.

**Note**: make sure to add the @[simps] command below, it was missing from the live demo.
Without it, all the `simp` tactics below will need to say `simp [has_mul.mul]`.

-/
@[simps] instance boolean_algebra.has_mul (X : Type) : has_mul (set X) :=
{ mul := λ s t, (s ∪ t) \ (s ∩ t) }

instance boolean_algebra.group (X : Type) : group (set X) :=
{ e              := ∅,
  inv            := id,
  mul_assoc      :=
    begin
      intros g1 g2 g3,
      ext,
      simp,
      tauto!,
    end,
  left_identity  := by { intro g, simp },
  right_identity := by { intro g, simp },
  left_inv       := by { intro g, simp },
  right_inv      := by { intro g, simp }, }

/-- ## 2. The symmetric group

An __equivalence__ `f : X ≃ Y` is a pair of functions 
    `(f : X → Y) (g : Y → X)`
together with proofs that `f ∘ g = id` and `g ∘ f = id`.
The non-symbolic name for `f : X ≃ Y` is `f : equiv X Y`.

You can think of this as a slightly-more concrete version of a bijection
(i.e. the inverse function is packaged with f).

Formally, (f : X ≃ Y) has four fields:
 * f.to_fun    : X → Y
 * f.inv_fun   : Y → X
 * f.left_inv  : f.inv_fun ∘ f.to_fun = id
 * f.right_inv : f.to_fun ∘ f.inv_fun = id

We will put a group structure on (X ≃ X). This is the type of equivalences
from X to itself.

**Note**: make sure to add the @[simps] command below, it was missing from the live demo.
Without it, all the `simp` tactics below will need to say `simp [has_mul.mul]`.

-/
@[simps] instance equiv_self.has_mul (X : Type) : has_mul (X ≃ X) :=
{ mul := equiv.trans }

instance equiv_self.group (X : Type) : group (X ≃ X) :=
{ e              := equiv.refl X,
  inv            := equiv.symm,
  mul_assoc      := by { intros f1 f2 f3, simp [equiv.trans] },
  left_identity  := by { intro f, simp },
  right_identity := by { intro f, simp },
  left_inv       := by { intro f, simp },
  right_inv      := by { intro f, simp }
}

/-- ## 3. The infinite dihedral group 

The infinite dihedral group has two generators "r" (a rotation) and "s"
(a reflection), satisfying the relations
  `s² = e`, `r s = s r⁻¹`

Every element can therefore be written uniquely as either rⁿ or s rⁿ.
-/

inductive dih : Type
| r  (n : ℤ) : dih -- an element of the form rⁿ
| sr (n : ℤ) : dih -- an element of the form srⁿ

namespace dih

@[simp] def dih_mul : dih → dih → dih
| (r n)  (r m)  := r (n + m)
| (sr n) (r m)  := sr (n + m)
| (r n)  (sr m) := sr (m - n)
| (sr n) (sr m) := r (m - n)

@[simp] def dih_inv : dih → dih
| (r n)  := r (-n)
| (sr n) := sr n

@[reducible]
instance dih.has_mul : has_mul dih := { mul := dih_mul }

instance dih.group : group dih :=
{ e := r 0,
  inv := dih_inv,
  mul_assoc := begin
    -- (read this proof last)
    rintros ⟨⟩ ⟨⟩ ⟨⟩; -- equivalent to intros g1 g2 g3, cases g1, simp, ring, ...
    by { simp, ring },
  end,
  left_identity := begin
    intro g,
    cases g,
    simp,
    simp,
  end,
  right_identity := λ g, by { cases g, simp, simp }, -- alternate phrasing
  left_inv       := λ g, by { cases g, simp, simp },
  right_inv      := λ g, by { cases g, simp, simp },
}

end dih

end sfu2023