Missing inductive hypothesis in constr w/ different type

Stream: lean4

[Andrés Goens]

I'm missing an inductive hypothesis when trying to use induction on a constructor that has a different type for the recusion. Here's an MWE:

inductive Foo
| base : Foo
| reccase : Foo → Foo
| natcase : Nat → Foo

def decFoo : Foo → Foo
  | .base => .base
  | .reccase f => f
  | .natcase .zero => .base
  | .natcase (.succ n) => .natcase n

theorem decFoo_decrease (f : Foo) : sizeOf (decFoo f) ≤ sizeOf f :=
  by induction f --<;> simp [decFoo]
 /-
 3 goals
case base
⊢ sizeOf (decFoo Foo.base) ≤ sizeOf Foo.base
case reccase
a✝ : Foo
a_ih✝ : sizeOf (decFoo a✝) ≤ sizeOf a✝
⊢ sizeOf (decFoo a✝.reccase) ≤ sizeOf a✝.reccase
case natcase
a✝ : Nat
⊢ sizeOf (decFoo (Foo.natcase a✝)) ≤ sizeOf (Foo.natcase a✝)
 -/

On the regular recursive case .reccase we get the induction hypothesis a_ih✝ : sizeOf (decFoo a✝) ≤ sizeOf a✝, but on the other recursive case that uses another inductive type (Nat in this case), it's missing. If I look at the recursor, it's there though:

#check Foo.rec
/-
Foo.rec.{u} {motive : Foo → Sort u}
(base : motive Foo.base)
(reccase : (a : Foo) → motive a → motive a.reccase)
(natcase : (a : Nat) → motive (Foo.natcase a))
(t : Foo) : motive t
-/

Is that a bug/missing feature in the induction tactic? (Maybe @Joachim Breitner is the person to ask here?)

[Henrik Böving]

The recursor is not giving you an IH here?

[Henrik Böving]

There is also no induction to be done in that case, natcase only contains a Nat, your induction goes over a Foo.

[Andrés Goens]

hm, you're right @Henrik Böving maybe this was too minimal, I have to think a bit more about why it's not working in my actual case

[Henrik Böving]

theorem decFoo_decrease (f : Foo) : sizeOf (decFoo f) ≤ sizeOf f := by
  induction f with
  | base => simp [decFoo]
  | reccase f ih => simp [decFoo, ih]
  | natcase n =>
    cases n with
    | zero => simp [decFoo]
    | succ n => simp [decFoo]

[Andrés Goens]

yep, that was quite silly! My actual case was just a more complicated version of the same. I needed to do an induction in the other type, but the reasoning from @Henrik Böving still applied. Thanks!

[Henrik Böving]

Note that you can also use functional induction here (don't know if that applies to your real world problem)

[Andrés Goens]

(functional induction works better in my actual use case too, thanks!)

[Andrés Goens]

wanted to write it up for the MWE for completeness here, but interestingly I can't get it to work :sweat_smile:

inductive Foo
| base : Foo
| reccase : Foo → Foo
| natcase : Nat → Foo

def decFoo : Foo → Foo
  | .base => .base
  | .reccase f => f
  | .natcase .zero => .base
  | .natcase (.succ n) => .natcase n

#check decFoo -- decFoo : Foo → Foo
#check decFoo.induct -- unknown constant 'decFoo.induct'

[Joachim Breitner]

You only get functional induction for recursive functions (at the moment, at least), so it’s not applicable to your proof. But it is also an induction that you don't need induction, merely case

[Joachim Breitner]

Or even just

theorem decFoo_decrease (f : Foo) : sizeOf (decFoo f) ≤ sizeOf f := by
  unfold decFoo; split <;> simp

[Andrés Goens]

makes sense, thanks! (FWIW, in the non-minimal case it is recursive and functional induction worked like a charm)

[Joachim Breitner]

Ah, the danger of mwe-ification. Glad to hear it works for you!