inductive type equation lemma

Stream: general

[Kevin Buzzard]

I'm struggling to make an equation lemma for an inductive type. What am I missing?

def Even : Nat → Prop := sorry

instance (n : Nat) : Decidable (Even n) := sorry

def EDS_aux : Nat → Nat
| 0       => 0
| 1       => 1
| 2       => 1
| 3       => 2
| 4       => 2
| (n + 5) =>
if hn : Even n then
  have h4 : n / 2 + 4 < n + 5 := sorry
  have h3 : n / 2 + 3 < n + 5 := sorry
  have h2 : n / 2 + 2 < n + 5 := sorry
  have h1 : n / 2 + 1 < n + 5 := sorry
  (EDS_aux (n / 2 + 4) * EDS_aux (n / 2 + 2) ^ 3) * (if Even (n / 2) then 2^4 else 1)
    - (EDS_aux (n / 2 + 1) * EDS_aux (n / 2 + 3) ^ 3) * (if Even (n / 2) then 1 else 2^4)
else
  have h5 : n / 2 + 5 < n + 5 := sorry
  have h4 : n / 2 + 4 < n + 5 := sorry
  have h3 : n / 2 + 3 < n + 5 := sorry
  have h2 : n / 2 + 2 < n + 5 := sorry
  have h1 : n / 2 + 1 < n + 5 := sorry
  (EDS_aux (n / 2 + 2) ^ 2 * EDS_aux (n / 2 + 3) * EDS_aux (n / 2 + 5)
      - EDS_aux (n / 2 + 1) * EDS_aux (n / 2 + 3) * EDS_aux (n / 2 + 4) ^ 2)

theorem EDS_aux_eqn_lemma (n : Nat) : EDS_aux (n + 5) =
if hn : Even n then
  (EDS_aux (n / 2 + 4) * EDS_aux (n / 2 + 2) ^ 3) * (if Even (n / 2) then 2^4 else 1)
    - (EDS_aux (n / 2 + 1) * EDS_aux (n / 2 + 3) ^ 3) * (if Even (n / 2) then 1 else 2^4)
else
  (EDS_aux (n / 2 + 2) ^ 2 * EDS_aux (n / 2 + 3) * EDS_aux (n / 2 + 5)
      - EDS_aux (n / 2 + 1) * EDS_aux (n / 2 + 3) * EDS_aux (n / 2 + 4) ^ 2) := by
  -- simp -- `simp made no progress`
  -- simp [EDS_aux] -- `max recursion depth`
  sorry

[Alex J. Best]

looks like

  rw [EDS_aux]

works fine, which makes sense I think, you just want to unfold one step of the recursion not iteratively do so

[Kevin Buzzard]

I had it hard-wired in my head that nowadays you prove equation lemmas using simp. Thanks!

[Mario Carneiro]

you should be able to do it using simp (config := {singlePass := true})