4_equality.lean

-- Отношения

universe u
variables α β : Type u                              -- Рассмотрим некоторый произвольный тип α
variable r : α → α → Prop                           -- Введем на нем бинарное отноешние r

variable trans_r : ∀ {x y z : α},                   -- мы можем объявить его транзитивным, указав следующий факт
                     r x y → r y z → r x z

variables a b c : α                                 -- тогда имея набор переменных типа α
variables (hab : r a b) (hbc : r b c)               -- и утверждений о связи их отношениями
#check trans_r hab hbc -- r a c                     -- мы можем вывести новое отношение r a c

variable refl_r : ∀ {x : α}, r x x                  -- рефлексивность r
variable symm_r : ∀ {x y : α}, r x y → r y x        -- симметричность r
                                                    -- теперь r — отношение эквивалентности

example (a b c d : α) (hab : r a b)                 -- данными утверждениями можно воспользоваться, чтоб
        (hcb : r c b) (hcd : r c d) : r a d :=      -- доказать наличие r-отношения между a и d
  trans_r (trans_r hab (symm_r hcb)) hcd

-- Эквивалентность

#check @eq.refl  -- ∀ {α : Type u}, α = α           -- эквивалентность, конечно, есть в стандартной библиотеке
#check @eq.symm  -- ∀ {α : Type u} {a b : α},
                 --   a = b → b = a
#check @eq.trans -- ∀ {α : Type u} {a b c : α},
                 --   a = b → b = c → a = c

example (a b c d : α) (hab : a = b)                 -- тот же пример можно вывести из стандартной библиотеки
        (hcb : c = b) (hcd : c = d) : a = d :=
  eq.trans (eq.trans hab (eq.symm hcb)) hcd

example (a b c d : α) (hab : a = b)                 -- тот же пример в projection notation (нечитаемо)
        (hcb : c = b) (hcd : c = d) : a = d :=
  (hab.trans hcb.symm).trans hcd

example (f : α → β) (a : α) : (λ x, f x) a = f a := -- благодаря выполнению редукции такая штука может быть доказана автоматом
  eq.refl _
example (a : α) (b : β) : (a, b).1 = a :=           -- и такая тоже
  eq.refl _
example : 39 + 3 = 42 := eq.refl _                  -- и даже такая

#check @rfl -- ∀ {α : Type u}, {a : α}, a = a       -- для этого даже вводят специальную функцию rfl == eq.refl _
                                                    -- все примеры выше можно переписать через нее

example (a : α) (b : β) : (a, b).1 = a := rfl

#check @eq.subst -- ∀ {a : Type u} {a b : α} {p : α → Prop},
                 --   a = b → p a = p b             -- важное утверждение, что мы можем менять равные элементы
                                                    -- внутри любого предиката

variable p : α → Prop
example (h₁ : a = b) (h₂ : p a) : p b :=            -- пример использования eq.subst
  eq.subst h₁ h₂

example (h₁ : a = b) (h₂ : p a) : p b := h₁ ▸ h₂    -- альтернативный синтаксис для eq.subst (▸ получается через \t)

#check @congr_arg -- ∀ {α : Type u} {β : Type v}    -- аналогично предикатам, замена аргумента может производиться и
                  --   {a₁ a₂ : α} (f : α → β),     -- внутри функции над элементами произвольных вселенных
                  --   a₁ = a₂ → f a₁ = f a₂        -- это называется конгруэнтностью по аргументу

#check @congr_fun -- ∀ {α : Type u} {β : α → Type v}-- при этом заменяться может и сама функцию
                  --   {f g : Π (x : α), β x},
                  --   f = g → ∀ x : α, f a = g a

#check @congr     -- ∀ {α : Type u} {β : Type v}    -- или даже функцию и аргумент одновременно
                  --   {f₁ f₂ : α → β}
                  --   {a₁ a₂ : α},
                  --   f₁ = f₂ → a₁ = a₂ → f₁ a₁ = f₂ a₂

example (h : a = b) (f : α → β) : f a = f b :=      -- примеры использования функций
  congr_arg f h

example (f g : α → β) (h : f = g) : f a = g a :=
  congr_fun h a

example (f g : α → β)
        (h₁ : f = g)
        (h₂ : a = b) : f a = g b :=
  congr h₁ h₂

-- Доказательства равенства

example (a b c d e : ℕ)                                   -- рассмотрим пример, когда имея несколько утверждений о равенстве
        (h₁ : a = b) (h₂ : b = c + 1)                     -- требуется установить новое равенство
        (h₃ : c = d) (h₄ : e = 1 + d) : a = e :=
  have h₅ : a = c + 1,     from eq.trans h₁ h₂,           -- a = b = c + 1 можно получить из транзитивности равенства
  have h₆ : c + 1 = d + 1, from congr_arg _ h₃,           -- чтоб перейти из a = c + 1 в a = d + 1 путем замены c на d,
                                                          -- докажем из c = d равенство c + 1 = d + 1 через рассмотренный выше congr_arg
  have h₇ : a = d + 1,     from eq.trans h₅ h₆,           -- теперь можем показать a = c + 1 = d + 1 из транзитивности
  have h₈ : 1 + d = d + 1, from nat.add_comm 1 d,         -- чтоб перейти из a = d + 1 в a = e путем замены e на d + 1,
                                                          -- докажем из коммунтативности сложения (nat.add_comm) 1 + d = d + 1
  have h₉ : e = d + 1,     from eq.trans h₄ h₈,           -- теперь можем показать e = 1 + d = d + 1 из транзитивности
  show a = e,              from eq.trans h₇ (eq.symm h₉)  -- так как цифры кончились, склеим два пункта в один :)
                                                          -- из симметрии заменим e = d + 1 на d + 1 = e, а далее
                                                          -- можем показать a = d + 1 = e из транзитивности

example (a b c d e : ℕ)                                   -- можем доказать то же через удобную и наглядную конструкцию calc,
        (h₁ : a = b) (h₂ : b = c + 1)                     -- придуманную специально для этих случаев; она заменяет обычные 
        (h₃ : c = d) (h₄ : e = 1 + d) : a = e :=          -- в таких доказательствах цепочки транзитивности
  calc
    a   = b     : h₁                                      -- утверждение о равенстве : доказательство (тут тривиально)
    ... = c + 1 : h₂                                      -- три точки говорят, что мы пользуемся транзитивностью равенства
    ... = d + 1 : congr_arg _ h₃                          -- как и раньше равенство достигается из конгруэнтности аргументов функции λ x, x + 1
    ... = 1 + d : nat.add_comm d (1 : ℕ)                  -- аналогично получаем из коммутативности сложения
    ... = e     : eq.symm h₄                              -- результат

-- обощенный синтаксис calc:
-- calc
--   expr₀ op₁ expr₁ : proof₁
--   ...   op₂ expr₂ : proof₂
--   {еще много строк}
--   ...   opn exprn : proofn

example (a b c d e : ℕ)                                   -- еще раз то же можно доказать с помощью тактики rw
        (h₁ : a = b) (h₂ : b = c + 1)                     -- подробнее тактики мы рассмотрим далее, здесь же ограничимся тем, что
        (h₃ : c = d) (h₄ : e = 1 + d) : a = e :=          -- такая тактика позволяет переписать кусок выражения с правой стороны
  calc                                                    -- от равества, что избавляет нас от необходимости пользоваться конгруэнтностью
    a   = b     : by rw h₁
    ... = c + 1 : by rw h₂                                -- применение тактики: by {tactic} {argumets}
    ... = d + 1 : by rw h₃                                -- в данном случае: by rw {равенство, на основании которого переписывается правая часть}
    ... = 1 + d : by rw nat.add_comm
    ... = e     : by rw h₄

example (a b c d e : ℕ)                                   -- несколько последовательных переписываний можно схлопнуть
        (h₁ : a = b) (h₂ : b = c + 1)                     -- передав тактике rw в качестве аргумента список равенств
        (h₃ : c = d) (h₄ : e = 1 + d) : a = e :=
  calc
    a   = d + 1 : by rw [h₁, h₂, h₃]
    ... = 1 + d : by rw nat.add_comm
    ... = e     : by rw h₄
    
example (a b c d e : ℕ)                                   -- или даже вот так
        (h₁ : a = b) (h₂ : b = c + 1)
        (h₃ : c = d) (h₄ : e = 1 + d) : a = e :=
  by rw [h₁, h₂, h₃, nat.add_comm, h₄]

example (a b c d e : ℕ)                                   -- для самых ленивых существует тактика simp
        (h₁ : a = b) (h₂ : b = c + 1)                     -- она перебирает все переданные ей в качестве аргумента
        (h₃ : c = d) (h₄ : e = 1 + d) : a = e :=          -- равенства, а также пробует пользоваться ассоциативностью
  by simp [h₁, h₂, h₃, h₄]                                -- пока что-нибудь не выведет

theorem T1 (a b c d e : ℕ)                                -- прелесть в том, что построив такое доказательство,
           (h₁ : a = b) (h₂ : b = c + 1)                  -- мы даже сможем его распечатать и понять, как оно было осуществлено
           (h₃ : c = d) (h₄ : e = 1 + d) : a = e :=
  by simp [h₄, h₂, h₁, h₃]

#print T1

example (x y : ℕ) :                                       -- напоследок докажем формулу квадрата суммы
          (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
  calc
    (x + y) * (x + y) = (x + y) * x + (x + y) * y       : by rw mul_add
    ...               = x * x + y * x + (x + y) * y     : by rw add_mul
    ...               = x * x + y * x + (x * y + y * y) : by rw add_mul
    ...               = x * x + y * x + x * y + y * y   : by rw ←add_assoc -- стрелочка ← (\l) показывает, что 
                                                                           -- применяемое равенство требуется
                                                                           -- переписать в обратную сторону

#check @add_assoc -- ∀ {α : Type u} (a b c : α) [_ : add_semigroup α] (a b c : α), a + b + c = a + (b + c)
                  -- во-первых, пока опустим add_semigroup α, на это посмотрим позже, но вообще это просто typeclass
                  -- во-вторых, утверждение гласит, что a + b + c = a + (b + c), а нам нужно переписать наоборот:
                  -- формулу со скобками представить без скобок, потому и нужна стрелка ←

lemma T2 (x y : ℕ) :                                      -- и так тоже сработает (ассоциативность применится сама)
          (x + y) * (x + y) = x * x + y * x + 
                              x * y + y * y :=
  by simp [mul_add, add_mul]

#print T2

example (f : ℕ → ℕ)                                       -- теми же способами можно доказывать неравества
        (h : ∀ x : ℕ, f x ≤ f (x + 1)) : f 0 ≤ f 3 :=
  calc
    f 0 ≤ f 1 : h 0
    ... ≤ f 2 : h 1
    ... ≤ f 3 : h 2