# Apply unfold once, instead of many times, in lean4

I have code that is similar in spirit to this:

inductive
RS where
| leaf (value : Nat)
| node (left : RS) (right : RS)

def count (a : Nat) (br : RS) : Nat :=
match br with
| RS.leaf v => a * v
| RS.node leftB rightB => ((count a leftB) + (count a rightB))

example
(a : Nat)
(b : RS)
(h : b = (RS.node l r))
: (count a b) ≤ (2 * max (count a l) (count a r)) := by
unfold count
sorry


The problem I'm running into is that, when I use unfold, the goal goes from this:

count a b ≤ 2 * max (count a left) (count a right)

to this:

(match b with
| RS.leaf v => a * v
| RS.node leftB rightB => count a leftB + count a rightB) ≤
2 *
max
(match l with
| RS.leaf v => a * v
| RS.node leftB rightB => count a leftB + count a rightB)
(match r with
| RS.leaf v => a * v
| RS.node leftB rightB => count a leftB + count a rightB)


but I wanted this much more succinct state:

(match b with
| RS.leaf v => a * v
| RS.node leftB rightB => count a leftB + count a rightB
) ≤ 2 * max (count a l) (count a r)


How do I only unfold the part on the left hand side, leaving the right hand side alone?

• Please provide a MWE. Dec 4, 2023 at 2:24
• @JasonRute Okay done Dec 4, 2023 at 3:06
• There may be a better approach, but you could just rewrite all but one of them (as per proofassistants.stackexchange.com/questions/2568/…) as count' (where count' := count), unfold, and then change it back after the unfold. Dec 4, 2023 at 3:10
• @JasonRute Should we write a meta post for MWE (with non-Lean specific language) and link to that instead?
– Trebor
Dec 4, 2023 at 12:45
• @Trebor Feel free to go ahead. I’d be happy to link to that instead. Dec 4, 2023 at 13:36

## 1 Answer

I personally don't know of a setting for this, but actually for what you are trying to do, simp [count] works fine in place of unfold count. The key is to realize you know you can only simplify your expression when you know the structure of the recursive parameter, in this case b:

example
(a : Nat)
(b : RS)
(h : b = (RS.node l r))
: (count a b) ≤ (2 * max (count a l) (count a r)) := by
rw [h]
simp [count]
/-
l r : RS
a : Nat
b : RS
h : b = RS.node l r
⊢ count a l + count a r ≤ 2 * max (count a l) (count a r)
-/
sorry


If you didn't have h : b = (RS.node l r), then you could have done induction b and both branches would have let you use simp [count] to simplify the LHS while leaving the RHS the same. This is a common pattern for recursive definitions. You don't have to unfold. Just do induction followed by simp.

• Thanks, that worked. Dec 4, 2023 at 4:49