6

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

Adam Kurkiewicz
  • 1,526
  • 1
  • 15
  • 34
  • 1
    Please note that the linked tutorial is for *Lean 2*. You can find documentation for the current version of Lean at http://leanprover.github.io/documentation/. – Sebastian Ullrich Jan 31 '17 at 12:36
  • Thanks @Kha, I can see that lean 3 includes a newer, improved version of the tutorial: https://leanprover.github.io/theorem_proving_in_lean/ (at least without unimplemented TODOs), I'll switch and use it accordingly. – Adam Kurkiewicz Jan 31 '17 at 13:44
  • BTW, this new version of the tutorial is super-cool, it shows the types of terms on mouse-hover! – Adam Kurkiewicz Jan 31 '17 at 13:54
  • Unfortunately, the [feature appears to have a bug](https://github.com/leanprover/leanprover.github.io/issues/61) – Adam Kurkiewicz Jan 31 '17 at 14:08

4 Answers4

7

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
  • Thanks, that indeed works, and from now on I will know how to use `congr_arg`. However, I don't understand the type declaration of `congr_arg`. The unknowns are: 1. Universe variables `u v`. Are they covered further in lean tutorial? 2. `Sort` keyword. Is there any place I could get a quick understanding of these, or should I just patiently carry on with the tutorial? – Adam Kurkiewicz Jan 31 '17 at 14:38
  • 1
    Universe variables are covered in sect. 2.2 of [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/). [issue #1341](https://github.com/leanprover/lean/issues/1341) explains the `Sort` keyword. *For now* you can just ignore these subtleties and think of the `congr_arg` lemma as a function that produces a proof of `f a₁ = f a₂` from a proof of `a₁ = a₂`, for any function `f : α → β`, where `Sort` just tells you that `α` and `β` are some types. HTH. – Anton Trunov Jan 31 '17 at 15:22
4

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
Sebastian Ullrich
  • 1,170
  • 6
  • 10
1

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.

Lambda Fairy
  • 13,814
  • 7
  • 42
  • 68
0

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
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15