mutual induction-recursion

Stream: Is there code for X?

[Allen Brown]

I am new to Lean and am starting by porting some existing Agda to Lean. I have just stumbled upon the fact that Lean mutual blocks are purely inductive or purely recursive. Unfortunately, I have several instances of the mixture in the Agda that I am porting. Is there an existing well-known solution to this problem in Lean?

[Aaron Liu]

can you share some of the code?

[Allen Brown]

I think that the following Agda snippet can be understood without its antecedent imports and opens:

data Multiplicity : Set where
#0 #1 #ω : Multiplicity

mutual
data Type : Set₁ where
Pure : Set → Type
Chan : Multiplicity → Multiplicity → Type → Type
Pair : (t : Type) → (f : ⟦ t ⟧ → Type) → Type

⟦_⟧ : Type → Set
⟦ Pure A ⟧ = A
⟦ Chan _ _ _ ⟧ = ⊤
⟦ Pair t f ⟧ = Σ ⟦ t ⟧ λ x → ⟦ f x ⟧

The definition of the inductive type, Type, exhibits one call to ⟦_⟧ while the definition of the recursive function, ⟦_⟧, matches on each of Type's constructors. Of course, my problem is that an analogous "mutual" construction using "inductive" and "def" is not available in L∃∀N.

[Kevin Buzzard]

(see #backticks and you can edit your post to make it look nicer)

[Allen Brown]

I should have added that the analogous (to the Agda) L∃∀N code that I wanted to write is:

mutual

inductive πType : Type 1 where

| Pure : Type → πType

| Chan : Multiplicity → Multiplicity → πType → πType

def blind : πType → Type 1

| Pure A => A

| Chan _ _ _ => Unit

end

In VS-Code this provokes the message

invalid mutual block: either all elements of the block must be inductive/structure declarations, or they must all be definitions/theorems/abbrevs

[Robin Arnez]

I suppose you mean this?

inductive Multiplicity where
  | zero | one | omega

mutual

inductive πType where
  | pure (α : Type)
  | chan (a b : Multiplicity) (t : πType)
  | pair (t : πType) (f : blind t → πType)

def blind : πType → Type
  | .pure α => α
  | .chan _ _ _ => Unit
  | .pair t f => (x : blind t) → blind (f x)

end

The problem is that Lean doesn't support inductive-recursive constructions, however there are some workarounds to this problem, e.g. using an index:

inductive Multiplicity where
  | zero | one | omega

inductive πType : (blind : Type) → Type 1 where
  | pure (α : Type) : πType α
  | chan (a b : Multiplicity) (t : πType α) : πType Unit
  | pair {α : Type} {β : α → Type} (t : πType α) (f : (a : α) → πType (β a)) : πType (Sigma β)

[Allen Brown]

Thank you for your suggestion. If I correctly understand your underlying insight, it is that rather than mutually defining an inductive type and a function by structural recursion on that type, instead define the graph of the function as an indexed inductive type. With that in mind, I believe that the following effectively reproduces the original Agda:

inductive Multiplicity : Type where

| ç0 | ç1 | çω

inductive πType : (filtered : Type) → Type 1 where

| pure (α : Type) : πType α

| chan {α : Type} (a b : Multiplicity) (t : πType α) : πType Unit

| pair {α : Type} {β : α → Type}

(t : πType α) (f : (a : α) →  πType (β a)) : πType (Σ a : α, β a)

def filter : πType α → Type

| _ => α

notation "⟦" t:arg "⟧" => filter t

[Kevin Buzzard]

#backticks