2
$\begingroup$

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?

$\endgroup$
5
  • $\begingroup$ Please provide a MWE. $\endgroup$
    – Jason Rute
    Dec 4, 2023 at 2:24
  • $\begingroup$ @JasonRute Okay done $\endgroup$ Dec 4, 2023 at 3:06
  • $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Dec 4, 2023 at 3:10
  • $\begingroup$ @JasonRute Should we write a meta post for MWE (with non-Lean specific language) and link to that instead? $\endgroup$
    – Trebor
    Dec 4, 2023 at 12:45
  • $\begingroup$ @Trebor Feel free to go ahead. I’d be happy to link to that instead. $\endgroup$
    – Jason Rute
    Dec 4, 2023 at 13:36

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thanks, that worked. $\endgroup$ Dec 4, 2023 at 4:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.