nested inductive equational lemmas?

Stream: lean4

[James Gallicchio]

an MWE:

import Std.Data.Array.Basic

inductive ReducedForm (L : Type u) : Type u
| and (fs : Array (ReducedForm L)) : ReducedForm L
| or  (fs : Array (ReducedForm L)) : ReducedForm L
| lit (l : L) : ReducedForm L

theorem ReducedForm.toPropFun (r : ReducedForm L) : Nat :=
  match r with
  | and fs =>
    let fs' := fs.attach.map (fun ⟨x,_⟩ => ReducedForm.toPropFun x)
    Array.size fs'
  | or fs  =>
    let fs' := fs.attach.map (fun ⟨x,_⟩ => ReducedForm.toPropFun x)
    Array.size fs'
  | lit _ => 0

example : ReducedForm.toPropFun (.lit l : ReducedForm L) = 0 := by
  simp [ReducedForm.toPropFun]

example : ReducedForm.toPropFun (.lit l : ReducedForm L) = 0 := by
  unfold ReducedForm.toPropFun
  rw [WellFounded.fix_eq]

I expected the first example to prove by its equational lemmas, but it doesn't. is this expected?

[Mario Carneiro]

you made it a theorem, this is like opaque

[James Gallicchio]

:man_facepalming:

[James Gallicchio]

forgot that turns off the equational lemma generation :sob: then this is a feature request for a warning when you try to simp a theorem

[Mario Carneiro]

um...

[Mario Carneiro]

people use theorems in simp all the time

[James Gallicchio]

err, you are right :stuck_out_tongue: i have no clue what this request is then

[Mario Carneiro]

probably to make defTheorem a lean linter

[James Gallicchio]

I think mathlib also has a linter for theorems with return type not in Prop right?

[James Gallicchio]

yeah

[Mario Carneiro]

you can run #lint but it's not as obvious

[James Gallicchio]

thanks for the fast response :racecar: my proofing is once again proceeding