Good recursors for mutually inductive types

recover.lean

import logic.equiv.basic

universes u v

section

parameters {l r : Type u}

mutual inductive P₁, P₂ (l r : Type u)
with P₁ : Type u
| zero : P₁
| left₁ : r → P₁ → P₁
| left₂ : l → P₂ → P₁
with P₂ : Type u
| right₁ : l → P₁ → P₂
| right₂ : r → P₂ → P₂

def P : bool → Type u
| ff := P₁
| tt := P₂

def P.sizeof : (Σ' b, P b) → ℕ
| ⟨ff, x⟩ := @sizeof P₁ _ x
| ⟨tt, x⟩ := @sizeof P₂ _ x

meta def P.rel_tac : expr → list expr → tactic unit :=
λ _ _, `[exact ⟨_, measure_wf P.sizeof⟩]

@[simp] def P.rec {C : Π b, P b → Sort v}
  (hz : C ff P₁.zero)
  (hl₁ : Π {j x}, C ff x → C ff (P₁.left₁ j x))
  (hl₂ : Π {i x}, C tt x → C ff (P₁.left₂ i x))
  (hr₁ : Π {i x}, C ff x → C tt (P₂.right₁ i x))
  (hr₂ : Π {j x}, C tt x → C tt (P₂.right₂ j x))
  : Π {b} x, C b x
| ff P₁.zero := hz
| ff (P₁.left₁ _ x) := hl₁ (@P.rec ff x)
| ff (P₁.left₂ _ x) := hl₂ (@P.rec tt x)
| tt (P₂.right₁ _ x) := hr₁ (@P.rec ff x)
| tt (P₂.right₂ _ x) := hr₂ (@P.rec tt x)
using_well_founded { rel_tac := P.rel_tac }

@[simp] def P₁.rec' {C₁ : P₁ → Sort v} {C₂ : P₂ → Sort v}
  (hz : C₁ P₁.zero)
  (hl₁ : Π {j x}, C₁ x → C₁ (P₁.left₁ j x))
  (hl₂ : Π {i x}, C₂ x → C₁ (P₁.left₂ i x))
  (hr₁ : Π {i x}, C₁ x → C₂ (P₂.right₁ i x))
  (hr₂ : Π {j x}, C₂ x → C₂ (P₂.right₂ j x))
  : Π x, C₁ x :=
let C : Π b, P b → Sort v := λ b, bool.rec C₁ C₂ b in
@P.rec C hz @hl₁ @hl₂ @hr₁ @hr₂ ff

@[simp] def P₂.rec' {C₁ : P₁ → Sort v} {C₂ : P₂ → Sort v}
  (hz : C₁ P₁.zero)
  (hl₁ : Π {j x}, C₁ x → C₁ (P₁.left₁ j x))
  (hl₂ : Π {i x}, C₂ x → C₁ (P₁.left₂ i x))
  (hr₁ : Π {i x}, C₁ x → C₂ (P₂.right₁ i x))
  (hr₂ : Π {j x}, C₂ x → C₂ (P₂.right₂ j x))
  : Π x, C₂ x :=
let C : Π b, P b → Sort v := λ b, bool.rec C₁ C₂ b in
@P.rec C hz @hl₁ @hl₂ @hr₁ @hr₂ tt

end