How does constructor interact with inequalities.

Stream: lean4

[Shreyas Srinivas]

I have an #mwe for something that I find weird. I am trying to understand whatconstructor is doing here.

def N (m : ℕ) := {n : ℕ // n ≥ m}

def incr_m {m : ℕ} (n : N m) : N (m+1) := by
  constructor
  constructor

#print incr_m

Explanation : N m is the set of natural numbers greater than or equal to m. incr_m is supposed to be something like below:

def incr_m {m : ℕ} (n : N m) : N (m+1) := by
  constructor
  case val => exact n.val + 1
  case property => linarith [n.property]

printing this yields

def incr_m : {m : ℕ} → N m → N (m + 1) :=
fun {m} n => { val := ↑n + 1, property := (_ : m + 1 ≤ ↑n + 1) }

which is fine.

But I have been playing around with repeat' in the last few days. In the #mwe just applying repeat' constructor closed all goals. Then I manually repeated it and in two applications it claimed that all goals were met. So I printed it out

def incr_m : {m : ℕ} → N m → N (m + 1) :=
fun {m} n => { val := m + 1, property := (_ : Nat.le (m + 1) (m + 1)) }

How did constructor magically infer the function I wanted to compute (incorrectly of course)?

[Shreyas Srinivas]

I thought constructor was lean4's equivalent of lean 3's split

[Alex J. Best]

(your mwe is missing imports)
constructor is the lean 4 equivalent of the lean 3 tactic constructor which tries all constructors of an inductive type in turn, split on the other hand is a special case of this when the type has only one constructor (e.g. an and statement, where applying this constructor splits the goal into two).
I think whats happening here is that the definition of le on naturals is an inductive type docs4#Nat.le with two constructors, i.e. lean knows that there are only two ways (possibly chained) to prove a natural is le another.
The constructor tactic simply to tries to apply each of these in turn, so it applies apply Nat.le.refl (every natural number is le itself) which unifies the metavariable (the value of the function) with the lower bound, then once that is assigned there is nothing else to prove.
This is one reason why people don't use tactics to make defs!
so your code really does this

import Mathlib.Data.Nat.Basic
def N (m : ℕ) := {n : ℕ // n ≥ m}

def incr_m {m : ℕ} (n : N m) : N (m+1) := by
  apply Subtype.mk
  apply Nat.le.refl

btw do you know the tactic show_term its very helpful for unpacking what tactics are doing under the hood (and often easier than reading the source code)

[Shreyas Srinivas]

Sorry about the imports. I wrote this inside a large file. About show_term thanks for recommending it. I tried to search the docs for it. It doesn't seem to be in the docs

[Shreyas Srinivas]

If I understand your explanation correctly, if the goal is a value (rather than a prop), then in tactic mode, there is a risk that it will be filled with the wrong hypothesis. In this case constructor found le.refl and an appropriate filler for the meta variable for the val goal.

[Patrick Massot]

https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/ShowTerm.html

[Shreyas Srinivas]

oh right. lean4 naming conventions.

[Alex J. Best]

Shreyas Srinivas said:

If I understand your explanation correctly, if the goal is a value (rather than a prop), then in tactic mode, there is a risk that it will be filled with the wrong hypothesis. In this case constructor found le.refl and an appropriate filler for the meta variable for the val goal.

Yeah the real issue is that tactics are very smart (sometimes) and fill in whatever they can, a goal whose type is a type is no different to most tactics. When proving things it doesn't matter most of the time if a tactic solves a goal in a way you weren't anticipating as any proof is just as good. But with defs/data there may be multiple ways to fill a goal that are distinct