CODEWITHSUNDEEP
dependent-typeformal-verificationlean
Adam Kurkiewicz
Adam Kurkiewicz

Reputation: 1632

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

Upvotes: 7

Views: 1527

Answers (4)

Anton Trunov
Anton Trunov

Reputation: 15424

You can use the congrArg lemma

lemma congrArg {α : 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 :=
  congrArg (fun n => n + 1) h

Note, that Lean is able to infer that our function is fun n => n + 1, so the proof can be simplified into congrArg _ h.

Upvotes: 7

Lambda Fairy
Lambda Fairy

Reputation: 14734

Since you have an equality (a = b), you can also rewrite the goal using tactic mode:

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

See Chapter 5 of Theorem Proving in Lean for an introduction to tactics.

Upvotes: 3

Juan Ospina
Juan Ospina

Reputation: 1347

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

Upvotes: 1

Sebastian Ullrich
Sebastian Ullrich

Reputation: 1230

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

Upvotes: 4

Related Questions