How to prove a = b → a + 1 = b + 1 in lean?

问题:

I'm working my way through the chapter 4 of the lean tutorial.

I'd like to be able to prove simple equalities, such as a = b → a + 1 = b + 1 without having to use the calc environment. In other words I'd like to explicitly construct the proof term of:

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

My best guess is that I need to use eq.subst and some relevant lemma about equality on natural numbers from the standard library, but I'm at loss. The closest lean example I can find is this:

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

回答1:

While congr_arg is a good solution in general, this specific example can indeed be solved with eq.subst + higher-order unification (which congr_arg uses internally).

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

回答2:

You can use the congr_arg lemma

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

which means if you supply equal inputs to a function, the output values will be equal too.

The proof goes like this:

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

Note, that Lean is able to infer that our function is λ n, n + 1, so the proof can be simplified into congr_arg _ H.

回答3:

More general : a = b -> a + c = b + c in a Ring

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