induction for mutually inductive types

Stream: new members

[Malvin Gattinger]

I get 'induction' tactic does not support mutually inductive types, the eliminator 'MyType.rec' has multiple motives. If needed I can try to make an mwe, but maybe someone has a hint how to deal with this in general? Is induction in Lean 4 less powerful than in Lean 3? I saw this discussion from 2021 but I am such a user that does not know what "motives" are. Do I need to understand it if I want to work with mutually inductive types in Lean 4?

[Kevin Buzzard]

the motive is just the thing you're trying to prove.

[Malvin Gattinger]

Ah, then I guess I do not really know what the eliminator of my type is. I guess to do induction on a mutually inductive type I have to show two motives, one for each of the types?

[Malvin Gattinger]

I'll see if I can make an MWE tomorrow. thanks for now!

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Malvin Gattinger]

Here comes my example. I actually have three questions, and the second to me feels like a bug :thinking:

-- MWE about Mutually Inductive Types
-- A bag is a thing that contains an object.
-- A box is an object that contains two things.

import Mathlib.Data.Finset.Basic -- comment this and sizeOfThing no longer errors O.o

-- Question 1: How do I get DecidableEq for these types?
mutual
  inductive Thing : Type
    | Pizza : Thing
    | round : Thing → Thing
    | Bag : Object → Thing
    deriving Repr -- , DecidableEq -- error "default handlers have not been implemented yet"
  inductive Object : Type
    | Bike : Object
    | Box : Thing -> Thing -> Object
    deriving Repr -- , DecidableEq
end
-- if deriving is not possible, how would I write these manually?
mutual
  instance decEqThing : DecidableEq Thing := sorry
  instance decEqObject : DecidableEq Object := sorry
end


-- Question 2: When I "import Mathlib.Data.Finset.Basic" above, then this here
-- fails with: "structural recursion does not handle mutually recursive functions".

open Thing Object

mutual
  def sizeOfThing : Thing → Nat
    | Pizza => 13
    | round s => sizeOfThing s
    | Bag o => 1 + sizeOfObject o
  def sizeOfObject : Object → Nat
    | Bike => 42
    | Box t1 t2 => 10 + sizeOfThing t1 + sizeOfThing t2
end
-- decreasing_by sorry -- would this help?
-- Should I be doing it, or just avoiding the (unrelated) import above?



-- Question 3: How do I prove things about mutually inductive types?

theorem aboutThings : ∀ t, sizeOfThing t * 2 = sizeOfObject (Box t t) - 10 :=
  by
  intro t
  -- induction t
  -- "induction t" here gives me the error:
  --      'induction' tactic does not support mutually inductive types,
  --      the eliminator 'Thing.rec' has multiple motives
  -- What can I use instead?
  -- "cases t" will not give me an induction hypothesis, right?
  sorry

[Joachim Breitner]

You meant Thing and Object, not Formula and Program, right?

[Malvin Gattinger]

Ah, yes, sorry, that was copypasta leftover from my original code.

[Joachim Breitner]

The unrelated import seems to be caused by

import Mathlib.Data.Nat.Order.Basic

at least I can observe your issue with that, but not if I replace it with that module’s imports.

[Joachim Breitner]

And if I change the result type of sizeOfThing from Nat to Unit the problem also goes away.

[Malvin Gattinger]

Ah, thanks for tracking that down. I also noticed that my code behaves differently when I used $\mathbb{N}$ instead of Nat, resulting in failed to synthesize instance OfNat ℕ 13 etc. Is that related?

[Malvin Gattinger]

Could it be that importing something brings extra lemmas or simp rules in scope which make the thing that tries to prove the termination / decreasing fail?

[Joachim Breitner]

This seems to work (although I wonder how that differs from the default):

mutual
  def sizeOfThing : Thing → Nat
    | Pizza => 13
    | round s => sizeOfThing s
    | Bag o => 1 + sizeOfObject o
  def sizeOfObject : Object → Nat
    | Bike => 42
    | Box t1 t2 => 10 + sizeOfThing t1 + sizeOfThing t2
end
termination_by
  sizeOfThing t => sizeOf t
  sizeOfObject o => sizeOf o

[Malvin Gattinger]

Oh, what is sizeOf here then? A default method counting levels of nested constructors?

[Joachim Breitner]

Yes, I think it is generated automatically whenever you define an inductive

[Joachim Breitner]

And here is how you can proof your theorem:

theorem aboutThings : ∀ t, sizeOfThing t * 2 = sizeOfObject (Box t t) - 10 :=  by
  unfold sizeOfObject
  intro t
  rw [add_assoc, ← Nat.mul_two, Nat.add_sub_self_left]

;-)

[Joachim Breitner]

Your comment “ -- "cases t" will not give me an induction hypothesis, right?” is actually going into a possibly right direction: You can use aboutThings inside aboutThings, it’ll be like a recursive function definition, and the system (or you) can prove termination, that works as a recursive proof.

[Joachim Breitner]

Like this (the lemma is not a good example, I guess):

theorem aboutThings : ∀ t, sizeOfThing t * 2 = sizeOfObject (Box t t) - 10 := by
  intro t
  cases t with
  | Pizza => sorry
  | round t =>
    have := aboutThings t
    sorry
  | Bag _ => sorry

[Joachim Breitner]

I was expecting this to work:

mutual
theorem aboutThings : ∀ t, sizeOfThing t % 2 = 1 := by
  intro t
  cases t with
  | Pizza => simp
  | round t =>
    have := aboutThings t
    unfold sizeOfThing
    exact this
  | Bag o =>
    unfold sizeOfThing
    rw [Nat.add_mod, aboutObjects]
    simp

theorem aboutObjects : ∀ o, sizeOfObject o % 2 = 0 := by
  intro o
  cases o with
  | Bike => simp
  | Box t1 t2 =>
    unfold sizeOfObject
    rw [Nat.add_mod, aboutThings]
    rw [Nat.add_mod (a := 10), aboutThings]
    simp
end
termination_by
  aboutThings t => sizeOf t
  aboutObjects o => sizeOf o

but I get

(kernel) unknown constant 'aboutObjects'

[Joachim Breitner]

Ok, avoiding putting the recursive call inside rw avoids that bug:

mutual
theorem aboutThings : ∀ t, sizeOfThing t % 2 = 1
  | Pizza => by simp
  | round t => by
    have := aboutThings t
    unfold sizeOfThing
    exact this
  | Bag o => by
    unfold sizeOfThing
    have := aboutObjects o
    rw [Nat.add_mod, this]
    simp

theorem aboutObjects : ∀ o, sizeOfObject o % 2 = 0
  | Bike => by simp
  | Box t1 t2 => by
    unfold sizeOfObject
    have h1 := aboutThings t1
    have h2 := aboutThings t2
    rw [Nat.add_mod, h2]
    rw [Nat.add_mod (a := 10), h1]
    simp
end
termination_by
  aboutThings t => sizeOf t
  aboutObjects o => sizeOf o

[Malvin Gattinger]

Nice, thank you! Indeed the lemma was a silly example, as it can also be proven without induction.

[Joachim Breitner]

You can also write

    rw [Nat.add_mod, aboutThings t2]
    rw [Nat.add_mod (a := 10), aboutThings t1

as long as you pass the parameter explicitly.

[Joachim Breitner]

Reported the kernel error at https://github.com/leanprover/lean4/issues/2628

[Joachim Breitner]

And back to your original question: As far as I know, support for structural mutual recursion is planned, but not present. At the moment, it generates the sizeOf function structurally recursively, thus enabling you to define stuff using well-founded recursion (and even if your definition looks structurally recursive and gets accepted without further ado, the system uses well-founded recursion internally).
sizeOf is defined by way of Object.rec, and I assume you can use that directly, if you want to.

[Malvin Gattinger]

Note to self: DecidableEq for mutual inductives is apparently not yet doable but coming up in the next Lean version: https://github.com/leanprover/lean4/pull/2591

[Joachim Breitner]

Here is a proof using the recursor directly:

theorem aboutThings : ∀ t, sizeOfThing t % 2 = 1 :=
  Thing.rec
    (motive_1 := fun t => sizeOfThing t % 2 = 1)
    (motive_2 := fun o => sizeOfObject o % 2 = 0)
    (Bag := fun o h => by
      dsimp
      unfold sizeOfThing
      rw [Nat.add_mod, h]
      rfl)
    (Bike := rfl)
    (Box := fun t h => by
      dsimp
      unfold sizeOfObject
      rw [Nat.add_mod, h]
      rfl)

[Malvin Gattinger]

Late thanks again for this. This example using a recuror direclty helped me in anoher case just now :smiley_cat:

[Malvin Gattinger]

Is it bad pratice to do something like apply Thing.rec in a tactic proof?