Expand using a definition

Stream: new members

[Mark Fischer]

Here's an example of a simple proof:

def exSmallNat : ∃n, n < 5 := by
  use 3
  apply Nat.le.step
  apply Nat.le.refl

When I step through this proof in vscode, the fact that a proof of 3 < 5 is defined as proof of 4 ≤ 5 is obscured by step. Is there a tactic that expands that for me?

[Ruben Van de Velde]

How did you come up with that proof?

[Ruben Van de Velde]

Because I can think of no reason to have either of those in a finished proof

[Mark Fischer]

I'm not sure what you mean? I was just playing around with Nat and logical predicates to wrap my head around what's happening. I don't have any real purpose in mind.

[Kyle Miller]

Here are some tactics for exploration:

def exSmallNat : ∃n, n < 5 := by
  use 3
  whnf
  -- Nat.le (Nat.succ 3) 5
  reduce
  -- Nat.le 4 5

[Kyle Miller]

whnf is "weak-head normal form", and it's for reducing just the head of an expression, unfolding definitions as they come. reduce does this to everything in the entire expression.

[Kyle Miller]

Those are mathlib tactics.

[Mark Fischer]

Ah! Nice. That works!

[Mark Fischer]

I suppose this is a follow up question in the same line. Is there some deeper reason that definitional equality isn't recognized by the rw tactic?

def smallNat : {n : Nat // n < 5 } :=
  let n := 2
  have h: n < 5 := by
    rw [n] -- this line doesn't compile as it's not a proof of `n = 2` or `n ↔ 2`
    trivial
  ⟨n, h⟩

[Kyle Miller]

rw isn't what you use for substituting local variables, it's for rewriting using equalities or iffs. You could try simp only [n] or the mathlib tactic unfold_let n

[Winston Yin (尹維晨)]

If you must use rw, you can wrap the whole thing in tactic mode and use set ... with:

def smallNat : {n : Nat // n < 5 } := by
  set n := 2 with hn
  have h: n < 5 := by
    rw [hn]
...