Как доказать a = b → a + 1 = b + 1 в худой?

Question

Я работаю над 4-й главой учебного пособия.

Я хотел бы быть в состоянии доказать простые равенства, такие как a = b → a + 1 = b + 1 без использования среды Calc. Другими словами, я хотел бы явно построить проверочный термин:

example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry

Мое лучшее предположение, что мне нужно использовать eq.subst и некоторая уместная лемма о равенстве натуральных чисел из стандартной библиотеки, но я в растерянности. Самый близкий пример, который я могу найти, это:

example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b := eq.subst H1 H2

Answer 1

Вы можете использовать congr_arg лемма

lemma congr_arg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) :
  a₁ = a₂ → f a₁ = f a₂

Это означает, что если вы предоставляете равные входные данные для функции, выходные значения также будут равны.

Доказательство выглядит так:

example (a b : nat) (H : a = b) : a + 1 = b + 1 :=
  congr_arg (λ n, n + 1) H

Обратите внимание, что Лин может сделать вывод, что наша функция λ n, n + 1 Таким образом, доказательство может быть упрощено в congr_arg _ H,

Answer 2

В то время как congr_arg это хорошее решение в целом, этот конкретный пример действительно может быть решен с eq.subst + унификация высшего порядка (которая congr_arg использует внутренне).

example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
eq.subst H1 rfl

Answer 3

Поскольку у вас есть равенство (a = b), вы также можете переписать цель, используя тактический режим:

example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
by rw H1

См. Главу 5 Доказательства теорем в Lean для введения в тактику.

Answer 4

Более общий: a = b -> a + c = b + c в кольце

import algebra.ring
open algebra

variable {A : Type}

variables [s : ring A] (a b c : A)
include s

example (a b c : A) (H1 : a = b) : a + c = b + c :=
eq.subst H1 rfl