Introduction: Jason Suagee

Stream: new members

[Jason Suagee]

Hi everybody! My name is Jason. I finished a PhD in Mathematics a few years ago but never looked at Lean before. I'm trying to figure out how to use it now and I've got some questions that I can't solve on my own from the documentation.

I was playing the natural numbers game to learn how to use Lean, but there are many things that it doesn't go over. Here's one thing I'm stuck on right now:

I can multiply both sides on the left by a:

example {a x y : ℕ} (h1 : a ≠ 0) : x = y / a :=
by
  apply (Nat.mul_right_inj h1).1

and the goal changes to

a * x = a * (y / a)

But what if instead of
(h1 : a \not= 0)
I have
(h1 : a \not= 1)
and the expression is
x = y / (a-1)
? How do I do multiply both sides on the left by (a - 1)?

I created a sketch of this:

example {a x y : ℕ} (h1 : a ≠ 1) : x = y / (a - 1) :=
by
  -- do something to get (h2 : a - 1 ≠ 0) ?
  apply (Nat.mul_right_inj h2).1

Also,

1. how do you create a new label for

(a - 1 \ne 0)

or is it not done that way?

2. What is the effect of the ".1" notation in the apply statement?

[Edward van de Meent]

1. the have tactic. Alternatively, if you want to apply a lemma but don't have all its arguments, you can put an underscore, like so: apply (Nat.mul_right_inj _).1 and it should create a new goal for the missing proof
2. in this case, it turns an Iff statement into its left-to-right implication. I do agree that it's not very desciptive. More commonly .mp is used instead, for "modus ponens"

[Edward van de Meent]

more generally .1 allows you, when you have a structure containing several pieces of data (think of a tuple), to retrieve its first component (and similar for .2, .3, etc., depending on how many "fields" the structure has). Typically there are more descriptive ways to do this though.

[suhr]

The universal answer to "how to apply a function to the both sides of an equation" is congrArg. For example:

#check
  show ∀ (a x y : Nat), x = y / (a-1) → x * (a - 1) = y / (a-1) * (a - 1)
  from λ(a x y: Nat)(e: x = y/(a-1)) => congrArg (· * (a - 1)) e

You may need to apply some simplifying lemmas after that though.

[Edward van de Meent]

do note that some things we might tell you about won't work for NNG but do work in "normal" Lean. If i understand right, this is done for teaching purposes

[suhr]

I would recommend reading Theorem Proving in Lean 4 and using NNG only as a set of exercises.

[Damiano Testa]

I would recommend to continue with the NNG.

[Daniel Weber]

Just a note that a ≠ 1 doesn't imply a - 1 ≠ 0 for a : ℕ in Lean, because natural number subtraction is actually truncated so 0 - 1 = 0