inductive-inductive types

Stream: general

[Adam Topaz]

Hi everyone. Sorry in advance for the vague question. I'm trying to define what I understand to be an example of an inductive-inductive type in lean (see e.g. https://ncatlab.org/nlab/show/inductive-inductive+type ).

In my specific case, I'm trying to define a type $A$ and a relation on $A$, say $r : A \to A \to Prop$, with both $A$ and $r$ defined inductively, while using $r$ in the definition of $A$.

I tried coming up with some minimized pseudocode (replacing a relation with a predicate for simplicity), and here is an example along the same lines for what I actually want to accomplish.

mutual inductive foo, bar
with foo : Type
| a : foo
| b : Π x, bar x → foo
with bar : foo → Prop
| c : bar foo.a

I don't see any simple way to simulate this using a single inductive definition. Does anyone have any ideas?

[Floris van Doorn]

It's not easy, but there are methods which will work in general. I believe that these methods do not give you definitional computation rules, if that is something you care about.
The idea in general is to first forget about the indexing that bar has, and then define a predicate that specifies the well-formed expressions of foo and the well-formed expressions of bar x.
In this case, the encoding would look something like this:

mutual inductive foo', bar'
with foo' : Type
| a : foo'
| b : foo' → bar' → foo'
with bar' : Type
| c : bar'

open foo' bar'

mutual inductive good_foo, good_bar
-- `good_foo x` means that `x` is well-formed
with good_foo : foo' → Prop
| a_good : good_foo a
| b_good : ∀ {x : foo'} {y : bar'}, good_foo x → good_bar y x → good_foo (b x y)
-- `good_bar y x` means that `y` is well-formed with index `x`
with good_bar : bar' → foo' → Prop
| c_good : good_bar c a


def foo : Type := { x : foo' // good_foo x }
instance : has_coe foo (foo') := ⟨subtype.val⟩
def bar (x : foo) : Type := { y : bar' // good_bar y x }

-- now we have to define/prove constructors, recursors and computation rules

[Floris van Doorn]

For more information, see for example Fredrik Nordvall Forsberg's PhD thesis (link) section 5.3 (which might be in a different type theory with equality reflection, I'm not sure)

[Adam Topaz]

Thanks Floris. I'll need some time to digest this (which means that it will have to happen later). I'll probably have some more questions later

[Floris van Doorn]

I thought it was a good exercise for myself, so here are the constructors, one way of formulating the recursor and the computation rules.
I made two changes:

• I used the standard encoding of mutual inductives into an indexed inductive, because I don't know how to induct on a mutual inductive in tactic mode
• I had to make the type of good a Type instead of a Prop, in order to make the recursor work for Sort u.

import tactic.basic

inductive foo_bar : bool → Type
| a : foo_bar tt
| b : foo_bar tt → foo_bar ff → foo_bar tt
| c : foo_bar ff

open sum
section
open foo_bar

-- `good (inl x)` means that `x` is well-formed
-- `good (inr (y, x))` means that `y` is well-formed with index `x`
inductive good : foo_bar tt ⊕ (foo_bar ff × foo_bar tt) → Type
| a : good (inl a)
| b : ∀ {x : foo_bar tt} {y : foo_bar ff}, good (inl x) → good (inr (y, x)) → good (inl (b x y))
| c : good (inr (c, a))

/-! Type formation -/
def foo : Type := Σ x : foo_bar tt, good (inl x)
instance foo.has_coe : has_coe foo (foo_bar tt) := ⟨sigma.fst⟩
def bar (x : foo) : Type := Σ y : foo_bar ff, good (inr (y, x))
instance bar.has_coe (x : foo) : has_coe (bar x) (foo_bar ff) := ⟨sigma.fst⟩
end

/-! Constructors -/
def foo.a : foo := ⟨foo_bar.a, good.a⟩
def foo.b (x : foo) (y : bar x) : foo := ⟨foo_bar.b x y, good.b x.2 y.2⟩
def bar.c : bar foo.a := ⟨foo_bar.c, good.c⟩

/-! Auxilliary definitions for the recursor -/
def data : ∀ {b}, foo_bar b → Type
| tt x := good (inl x)
| ff y := Σ x : foo, good (inr (y, x))

def val : ∀ {b} {x : foo_bar b}, data x → foo ⊕ Σ x, bar x
| tt x hx := inl ⟨x, hx⟩
| ff y hy := inr ⟨hy.1, ⟨y, hy.2⟩⟩

/-! One way to formulate the recursor -/
universe variable u
def rec {P : (foo ⊕ Σ x, bar x) → Sort u}
  (ha : P (inl foo.a)) (hb : ∀ x (y : bar x), P (inl x) → P (inr ⟨x, y⟩) → P (inl $ foo.b x y))
  (hc : P (inr ⟨foo.a, bar.c⟩)) :
  ∀ x, P x :=
begin
  suffices : ∀ b (x : foo_bar b) (hx : data x), P (val hx),
  { rintro (⟨x, hx⟩|⟨⟨x, hx⟩, ⟨y, hy⟩⟩),
    { exact this tt x hx },
    { exact this ff y ⟨⟨x, hx⟩, hy⟩ } },
  intros b x hx,
  induction x with x y ihx ihy,
  { cases hx, exact ha },
  { cases hx with _ _ hx hy, exact hb ⟨x, hx⟩ ⟨y, hy⟩ (ihx hx) (ihy ⟨⟨x, hx⟩, hy⟩) },
  { rcases hx with ⟨⟨x, ⟨⟩⟩,⟨⟩⟩, exact hc }
end

/-! Computation rules -/

lemma rec_a {P : (foo ⊕ Σ x, bar x) → Sort u}
  (ha : P (inl foo.a)) (hb : ∀ x (y : bar x), P (inl x) → P (inr ⟨x, y⟩) → P (inl $ foo.b x y))
  (hc : P (inr ⟨foo.a, bar.c⟩)) : rec ha hb hc (inl foo.a) = ha :=
rfl

lemma rec_b {P : (foo ⊕ Σ x, bar x) → Sort u}
  (ha : P (inl foo.a)) (hb : ∀ x (y : bar x), P (inl x) → P (inr ⟨x, y⟩) → P (inl $ foo.b x y))
  (hc : P (inr ⟨foo.a, bar.c⟩)) (x : foo) (y : bar x) :
    rec ha hb hc (inl (foo.b x y)) = hb x y (rec ha hb hc (inl x)) (rec ha hb hc (inr ⟨x, y⟩)) :=
by { cases x with x hx, cases y with y hy, refl }

lemma rec_c {P : (foo ⊕ Σ x, bar x) → Sort u}
  (ha : P (inl foo.a)) (hb : ∀ x (y : bar x), P (inl x) → P (inr ⟨x, y⟩) → P (inl $ foo.b x y))
  (hc : P (inr ⟨foo.a, bar.c⟩)) : rec ha hb hc (inr ⟨foo.a, bar.c⟩) = hc :=
rfl