help with `unfold`

Stream: lean4

[Shreyas Srinivas]

Is there a way to unfold only one occurrence of a definition. unfold unfolds all occurrences. This affects proofs by induction

[Shreyas Srinivas]

I am referring to the first occurrence in the goal, so I don't see a way to separately call this occurrence by a name

[Ruben Van de Velde]

Maybe with conv?

[Kevin Buzzard]

If unfold is doing definitional unfolding then you might be able to use change with some _ .

[Shreyas Srinivas]

It did not work. I am at my wits end with some of these proofs

[Kevin Buzzard]

Can you post a #mwe ?

[Shreyas Srinivas]

It is the same as last time.

import Mathlib.Init.Data.Nat.Lemmas
import Init.WFTactics

-- Imported for Boolean `xor`
import Mathlib.Data.Bool.Basic
import Mathlib.Init.Data.Bool.Lemmas

-- Imported for `bit0` and `bit1`
import Mathlib.Init.ZeroOne

-- Imported for cases'
import Mathlib.Tactic.Cases

universe u

-- The following line helps override the default behaviour, wherein
-- lean equates xor with Nat.xor
-- bxor points to Mathlib.Data.Bool.Basic.xor
--- Author : Shreyas Srinivas
abbrev bxor := xor

namespace Nat
def boddDiv2 : ℕ → Bool × ℕ
  | 0 => (false, 0)
  | succ n =>
    match boddDiv2 n with
    | (false, m) => (true, m)
    | (true, m) => (false, succ m)
#align nat.bodd_div2 Nat.boddDiv2

def div2 (n : ℕ) : ℕ :=
  (boddDiv2 n).2


def bodd (n : ℕ) : Bool :=
  (boddDiv2 n).1


@[simp]
theorem bodd_zero : bodd 0 = false :=
  rfl


theorem bodd_one : bodd 1 = true :=
  rfl


theorem bodd_two : bodd 2 = false :=
  rfl
#align nat.bodd_two Nat.bodd_two

@[simp]
theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
/-  unfold bodd boddDiv2 <;> cases boddDiv2 n <;> rename_i fst snd <;> cases fst <;>
  simp <;>
  cases n <;> simp [add_succ, ]
-/
    unfold bodd
    unfold boddDiv2
    induction' n with n IH
    case zero =>
      simp
    case succ =>
      simp[IH]

[Kevin Buzzard]

This doesn't compile for me. Can you make it a #mwe ?

[Shreyas Srinivas]

I edited it and checked on the lean playground. It works. At the end of case succ, it seems unfolding boddDiv2 (succ n) would be useful. unfold boddDiv2 unfolds all occurrences of boddDiv2

[Shreyas Srinivas]

So far I have worked around this and fixed a number of other errors in the file (Down from 70 odd messages to 19 messages). But I can't overlook this one anymore

[Siddhartha Gadgil]

A workaround is to introduce a statement have l : boddDiv2 (succ n) = ... := by unfold boddDiv2 and then rw [l].

[Siddhartha Gadgil]

I mean you can see what boddDiv2 (succ n) unfolds to, copy-paste that (in place of ... above) to make the claim l and proceed as above.

[Kevin Buzzard]

theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
  simp only [bodd, boddDiv2]
  let ⟨b,m⟩ := boddDiv2 n
  cases b <;> rfl

[Kevin Buzzard]

unfold was unfolding too far; simp only gets it right.

[Marcus Rossel]

I've also had the general experience that rw can be useful for performing a single unfold.

[Kevin Buzzard]

Ruben's suggestion also works:

theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
  unfold bodd
  conv =>
    lhs
    unfold boddDiv2
  let ⟨b,m⟩ := boddDiv2 n
  cases b <;> rfl

[Kevin Buzzard]

change works too:

theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
  unfold bodd
  change (match boddDiv2 n with
    | (false, m) => (true, m)
    | (true, m) => (false, succ m)).fst =
  !(boddDiv2 n).fst
  let ⟨b,m⟩ := boddDiv2 n
  cases b <;> rfl

[Shreyas Srinivas]

Kevin Buzzard said:

theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
  simp only [bodd, boddDiv2]
  let ⟨b,m⟩ := boddDiv2 n
  cases b <;> rfl

Yeah this worked. Using simp only also helped with another error. Thanks