Fastest proof of a trivial statement

Stream: new members

[Ioannis Konstantoulas]

I have code of the following form all around my code base (pure Lean 4, no mathlib):

if pred_n_eq_one  : n - 1 = 1 then
      have : n = 2 := sorry

The fastest way to prove that for me is calc:

  if n_eq_2 : n - 1 = 1 then
      have : n = 2 := Eq.symm <| calc
        2 = 1 + 1 := by simp
        _ = n - 1 + 1 := by rw [n_eq_2]
        _ = n := Nat.sub_add_cancel <| calc
          1 = n - 1 := n_eq_2.symm
          _ ≤ n := Nat.pred_le n

There has to be a simpler (and shorter, but chiefly simpler) way to prove this. What am I missing? Simple simp and simp_arith invocations do not work.

[Vincent Beffara]

Something starting with cases n?

[Alex J. Best]

theorem a (_h : n - 1 = 1) :
   n = 2 :=
   match n with
   | 2 => rfl

#print a

[Ioannis Konstantoulas]

Where can I find some explanation of how this works? I have not encountered this use for match in TPIL so far, and it simplifies things so much that I cannot help but feel extremely frustrated.

[Alex J. Best]

I should say this proof is a bit of a trick, and while its good to understand how it works its not a proof style I use myself that often. Match is explained in https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html, the key point is that from the hypotheses the pattern matcher is smart enough to work out that the other possible ways of constructing a natural dont work, by definition of sub.

[Ioannis Konstantoulas]

Alex J. Best said:

I should say this proof is a bit of a trick, and while its good to understand how it works its not a proof style I use myself that often. Match is explained in https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html, the key point is that from the hypotheses the pattern matcher is smart enough to work out that the other possible ways of constructing a natural dont work, by definition of sub.

Thank you very much for your feedback.

[Alex J. Best]

And please don't feel frustrated, that wasn't my intention. But a big part of learning any programming langauge (or indeed anything) is to get a good handle on the fundamentals, before moving on to more advanced / esoteric features

[Ioannis Konstantoulas]

Alex J. Best said:

And please don't feel frustrated, that wasn't my intention. But a big part of learning any programming langauge (or indeed anything) is to get a good handle on the fundamentals, before moving on to more advanced / esoteric features

Following that thought, is my code above about the shortest/simplest "elementary" proof of the theorem that doesn't use such tricks?

[Vincent Beffara]

My suggestion of using cases is kind of in between: either n is 0 and then the assumption fails, or it is a successor and then the assumption simplifies and you can conclude using subst or something.

[Arend Mellendijk]

Scratch this - missed the 'no mathilb' part

Here's a much shorter proof that doesn't use any tricks

import Mathlib.Data.Nat.Basic

example (n : ℕ) (hn : n-1 = 1) : n = 2 :=
  Nat.eq_add_of_sub_eq (le_of_lt (Nat.lt_of_sub_eq_succ hn)) hn

[Alex J. Best]

Ioannis Konstantoulas said:

Alex J. Best said:

And please don't feel frustrated, that wasn't my intention. But a big part of learning any programming langauge (or indeed anything) is to get a good handle on the fundamentals, before moving on to more advanced / esoteric features

Following that thought, is my code above about the shortest/simplest "elementary" proof of the theorem that doesn't use such tricks?

Well its a bit hard to measure shortest / simplest, and by not using any of std or mathlib you place a lot of restrictions on what you can use, the material built in to lean is mostly just what is required to build lean itself and some very fundamental tactics.
Maybe a clearer version of my proof above is osmething like

theorem a (h : n - 1 = 1) :
   n = 2 := by
match n with
| 0 => simp at h
| 1 => simp at h
| 2 => rfl
| n + 3 =>
  simp [Nat.add_sub_assoc] at h
  injection h

[Ioannis Konstantoulas]

Thank you very much for your responses, everyone; I learned a lot!

[Mario Carneiro]

Alex J. Best said:

theorem a (_h : n - 1 = 1) :
   n = 2 :=
   match n with
   | 2 => rfl

#print a

By the way there is an even more amusing way to write that:

theorem a (_h : n - 1 = 1) : n = 2 :=
   let 2 := n; rfl

#print a

[Eric Rodriguez]

what language feature is this!?

[Mario Carneiro]

it's the same language feature as the one already demonstrated, because let pat := e1; e2 macro expands to match e1 with | pat => e2