Induction over mutually inductive predicates

Stream: lean4

[Jannis Limperg]

A student of mine is currently struggling with induction over mutually inductive predicates (in Prop) because

• induction doesn't support mutual inductive types;
• mutual recursion is implemented via well-founded recursion, but inductive predicates don't have (and can't have) a useful SizeOf instance.

As far as I can tell, he has the following options, none of which are particularly pleasing:

• Recurse over the data rather than the predicates.
• Put the predicates into Type.
• Use the recursor directly.
• Give up on mutual types and define the union of the predicates as a single inductive predicate, essentially doing the elaborator's job by hand.

Is there a more idiomatic way?

[Mario Carneiro]

Nope, this is currently not really supported. The best option for now is just using the recursor directly

[Mario Carneiro]

Probably using an inductive family is the path of least resistance

[Jannis Limperg]

Okay, thanks!

[Max Nowak 🐉]

You can use a mutual block of two definitions to consume the mutually inductive type. Then you won’t use the induction tactic, but simply obtain the IH by invoking the other definition recursively. It actually works quite nice.

[Jannis Limperg]

I think back when I made this thread, your suggestion didn't work for Prop-valued(!) inductive types because mutual rec went via wfrec, which went via SizeOf and Prop-valued types can't have a useful SizeOf instance. Maybe that has changed in the meantime.

[Jonathan Chan]

I noticed that there's structural mutual recursion now: https://github.com/leanprover/lean4/pull/4575
Is there some way of doing mutual induction over inductive predicates with this instead of encoding a mutual predicate as a single inductive family? I've run into an error saying my mutual inductive type

does not have a .brecOn recursor

and I'm not sure if there's a trick I'm missing or if indexed predicates are inherently different from propositions

[Edward van de Meent]

Afaik using induction on mutual inductives should be possible... Can you post a #mwe?

[Jonathan Chan]

okay not so minimal but this is demonstrating the kind of proof I'm trying to do, I'm mechanizing typing judgements and proving syntactic properties:

set_option autoImplicit false
set_option pp.fieldNotation false

inductive Term : Type where
  | 𝒰 : Nat → Term
open Term

inductive Ctxt : Type where
  | nil : Ctxt
  | cons : Ctxt → Term → Ctxt
notation:50 "⬝" => Ctxt.nil
infixl:50 "∷" => Ctxt.cons

inductive Eqv : Term → Term → Prop where
  | trans {a b c} :
    Eqv a b →
    Eqv b c →
    ---------
    Eqv a c
  | 𝒰 {a b} :
    a = b →
    ----------------
    Eqv (𝒰 a) (𝒰 b)
infix:40 (priority := 1001) "≈" => Eqv

mutual
inductive Wf : Ctxt → Prop where
  | nil : Wf (⬝)
  | cons {Γ A k} :
    Wf Γ →
    Wt Γ A (𝒰 k) →
    --------------
    Wf (Γ ∷ A)

inductive Wt : Ctxt → Term → Term → Prop where
  | 𝒰 {Γ j k} :
    j < k →
    -----------------
    Wt Γ (𝒰 j) (𝒰 k)
  | conv {Γ A B a k} :
    A ≈ B →
    Wt Γ a A →
    Wt Γ B (𝒰 k) →
    --------------
    Wt Γ a B
end

notation:40 "⊢" Γ:40 => Wf Γ
notation:40 Γ:41 "⊢" a:41 "∶" A:41 => Wt Γ a A

theorem wt𝒰Inv {Γ j A 𝒰'} : Γ ⊢ A ∶ 𝒰' → A = 𝒰 j → ∃ k, 𝒰 k ≈ 𝒰' := by
  intro h e; subst e
  -- induction h
  /- 'induction' tactic does not support mutually inductive types,
     the eliminator 'Wt.rec' has multiple motives -/
  cases h with
  | 𝒰 lt => exact ⟨_, Eqv.𝒰 rfl⟩
  | conv e₁ h _ =>
    let ⟨_, e₂⟩ := wt𝒰Inv h rfl
    exact ⟨_, Eqv.trans e₂ e₁⟩
  termination_by structural h => h
  /- failed to infer structural recursion:
     Cannot use parameter h:
       unknown constant 'Wt.brecOn' -/

[Jannis Limperg]

Induction on mutually defined predicates (in Prop) still seems to be effectively unsupported. A student of mine is currently struggling with this. The best solution we came up with is to manually define an induction principle for all the mutual types together, using the induction principles for each individual type that Lean generates. But it's a big pain.

[Max Nowak 🐉]

I have done mutual theorem (or mutual def) before and it works just fine. That is what the induction tactic does under the hood anyway, right? The induction hypothesis is just the result obtained via a recursive call.

[Jonathan Chan]

Yeah, my current solution is also to manually define the induction principles I need for the mutual predicate that I've encoded as a single predicate

[Jannis Limperg]

Max Nowak 🐉 said:

I have done mutual theorem (or mutual def) before and it works just fine. That is what the induction tactic does under the hood anyway, right? The induction hypothesis is just the result obtained via a recursive call.

This does seem to work. I might have to apologise to my student. It seems to do recursion on the mutual types over which the mutual predicates are presumably defined, so no rule induction. But this is probably fine for most use cases.

[Jannis Limperg]

A toy example:

mutual
  inductive A : Type
    | base : A
    | good : B → A
    | evil : B → A

  inductive B : Type
    | good : A → B
    | evil : A → B
end

mutual
  inductive AGood : A → Prop
    | base : AGood .base
    | good : BGood b → AGood (.good b)

  inductive BGood : B → Prop
    | good : AGood a → BGood (.good a)
end

mutual
  inductive AEvil : A → Prop
    | here : AEvil (.evil b)
    | there : BEvil b → AEvil (.good b)

  inductive BEvil : B → Prop
    | here : BEvil (.evil a)
    | there : AEvil a → BEvil (.good a)
end

mutual
  theorem AGood_not_AEvil : AGood a → ¬ AEvil a := by
    intro h contra
    cases h
    case base => cases contra
    case good p =>
      cases contra
      apply BGood_not_BEvil <;> assumption

  theorem BGood_not_BEvil : BGood b → ¬ BEvil b := by
    intro h contra
    cases h
    cases contra
    case there p => apply AGood_not_AEvil <;> assumption
end

[Jannis Limperg]

Thanks @Max Nowak 🐉!

[Edward van de Meent]

you can also explicitly invoke .rec, which i think should work too

[Jannis Limperg]

Yes, that also works. But the recursors that Lean generates have a bit of an awkward shape (they ask you to prove one property per mutual type, but then conclude only the property for one of the types). So if you want to go down that route, it's better to first define a more natural recursor/induction principle.