nth_unfold

Stream: general

[loooong]

I want to know is there a tactic like "nth_unfold". If a function appears in many places of a equation, I want to unfold it at a special place, what can I do?
I think a good way is using "nth_rw", but I do not know how to get the definition equation of a function.
For example,

def id₁ : ℕ → ℕ
  | 0 => 0
  | n + 1 => id₁ n + 1

example {n : ℕ} : id₁ n = match n with
  | 0 => 0
  | n + 1 => id₁ n + 1 := by
  induction' n with n h
  unfold id₁
  simp
  unfold id₁
  simp
  exact h

how to prove the example directly?

[Kevin Buzzard]

Your code doesn't compile for me as it stands. Can you please edit your post to make it a #mwe ?

[Arthur Adjedj]

loooong said:

I want to know is there a tactic like "nth_unfold". If a function appears in many places of a equation, I want to unfold it at a special place, what can I do?
I think a good way is using "nth_rw", but I do not know how to get the definition equation of a function.
For example,

def id₁ : ℕ → ℕ
  | 0 => 0
  | n + 1 => id₁ n + 1

example {n : ℕ} : id₁ n = match n with
  | 0 => 0
  | n + 1 => id₁ n + 1 := by
  induction' n with n h
  unfold id₁
  simp
  unfold id₁
  simp
  exact h

how to prove the example directly?

you can use the conv tactic to modify/unfold particular parts of your code:

example {n : Nat} : id₁ n = match n with
  | 0 => 0
  | n + 1 => id₁ n + 1 := by
  conv =>
    lhs
    unfold id₁

Your particular example can also be proved by trivial induction:

example {n : Nat} : id₁ n = match n with
  | 0 => 0
  | n + 1 => id₁ n + 1 := by induction n <;> rfl

[loooong]

Kevin Buzzard said:

Your code doesn't compile for me as it stands. Can you please edit your post to make it a #mwe ?

I think import something from Mathlib4 is okay to check this code. Since the below chat suggests on using conv mode or induction can both work as expected so I will not make the mwe. Thank you anyway!

[loooong]

Arthur Adjedj said:

loooong said:

I want to know is there a tactic like "nth_unfold". If a function appears in many places of a equation, I want to unfold it at a special place, what can I do?
I think a good way is using "nth_rw", but I do not know how to get the definition equation of a function.
For example,

def id₁ : ℕ → ℕ
  | 0 => 0
  | n + 1 => id₁ n + 1

example {n : ℕ} : id₁ n = match n with
  | 0 => 0
  | n + 1 => id₁ n + 1 := by
  induction' n with n h
  unfold id₁
  simp
  unfold id₁
  simp
  exact h

how to prove the example directly?

you can use the conv tactic to modify/unfold particular parts of your code:

example {n : Nat} : id₁ n = match n with
  | 0 => 0
  | n + 1 => id₁ n + 1 := by
  conv =>
    lhs
    unfold id₁

Your particular example can also be proved by trivial induction:

example {n : Nat} : id₁ n = match n with
  | 0 => 0
  | n + 1 => id₁ n + 1 := by induction n <;> rfl

Thank you! The conv mode can modify goal in a delicate style, which is what I want to find.
I also want to know is there a name for the definition equation of a function?

[Arthur Adjedj]

I'm also quite very surprised that this cannot be simply proven by rfl...

[Arthur Adjedj]

I don't know if there's a specific name for this, the fact that id₁ reduces to its definition is referred to as delta-reduction, if that's any help. I also believe Lean automatically generates these sorts of theorems, but I'm not capable of finding where to find them now

[Arthur Adjedj]

looking more into it, lean elaborates the definition of id₁ n to

(Nat.rec { fst := 0, snd := PUnit.unit }
        (fun n n_ih => { fst := Nat.succ n_ih.1, snd := { fst := n_ih, snd := PUnit.unit } }) n).1

whereas the right-hand side is elaborated to

Nat.rec 0
      (fun n n_ih =>
        Nat.succ
          (Nat.rec { fst := 0, snd := PUnit.unit }
              (fun n n_ih => { fst := Nat.succ n_ih.1, snd := { fst := n_ih, snd := PUnit.unit } }) n).1)
      n

The definitional equality breaks because the two terms are not elaborated the same way. Does anyone know if this an intended behaviour ?

[Arthur Adjedj]

For context, this also can't be proven by reflexivity in lean 3 and, more surprisingly, in coq.

[Trebor Huang]

If it were a judgemental equality then it can indefinitely unfold and there's a normalization problem iirc