## Stream: general

### Topic: mutually inductive type and function

#### Scott Morrison (Apr 12 2020 at 06:00):

I would like to define a mutually inductive type and function out of it. Is this possible? My example which I'd hoped might be accepted is:

mutual inductive edge_sequence, add_edge_sequence
with edge_sequence : layout G → Type
| single {L : layout G} {e : G.edges} (h : e ∈ L.remaining_edges) : edge_sequence L
| cons {L : layout G} (S : edge_sequence L) {e : G.edges} (h : e ∈ (add_edge_sequence S).1.remaining_edges) : edge_sequence L
with add_edge_sequence : Π {L : layout G}, edge_sequence L → layout G × finset G.boxes
| L (single h) := L.add_edge h
| L (cons S h) := let ⟨L', B⟩ := L.add_edge_sequence S in let ⟨L'', B'⟩ := L.1.add_edge h in ⟨L'', B ∪ B'⟩


(I can try to come up with a MWE if it's completely unclear what I'm going for here!)

#### Scott Morrison (Apr 12 2020 at 06:01):

From this I only get the helpful: unknown declaration '4._.0'

#### Scott Morrison (Apr 12 2020 at 06:01):

Presuming Lean doesn't support this, does anyone who is good at induction know how to "roll it by hand"?

#### Scott Morrison (Apr 12 2020 at 06:02):

(@Kevin Buzzard, points if you can guess what I'm doing)

#### Bryan Gin-ge Chen (Apr 12 2020 at 06:03):

Oh, now I think I know. :joy:

#### Mario Carneiro (Apr 12 2020 at 06:28):

The general scheme is called "induction-recursion" and it's stronger than lean's axiomatics, so this isn't always possible

#### Mario Carneiro (Apr 12 2020 at 06:29):

do you have a MWE?

#### Mario Carneiro (Apr 12 2020 at 06:36):

Is there a typo on the last line, where L.1.add_edge should be L'.1.add_edge?

#### Mario Carneiro (Apr 12 2020 at 06:44):

I can't type check this because of the lack of MWE, but something like this should work

inductive with_edge_sequence : layout G → layout G → Type
| single {L : layout G} {e : G.edges} (h : e ∈ L.remaining_edges) : with_edge_sequence L (L.add_edge h).1
| cons {L L' : layout G} (S : with_edge_sequence L L')
{e : G.edges} (h : e ∈ L'.remaining_edges) : with_edge_sequence L (L'.add_edge h).1

def edge_sequence (L : layout G) : Type := Σ L', with_edge_sequence L L'

def add_edge_sequence_boxes : ∀ {L L' : layout G}, with_edge_sequence L L' → finset G.boxes
| L _ (with_edge_sequence.single h) := (L.add_edge h).2
| _ _ (@with_edge_sequence.cons L L' S e h) := add_edge_sequence_boxes S ∪ (L'.add_edge h).2

def add_edge_sequence {L : layout G} : edge_sequence L → layout G × finset G.boxes
| ⟨L', S⟩ := ⟨L', add_edge_sequence_boxes S⟩


#### Scott Morrison (Apr 12 2020 at 08:15):

Lovely. Needed one minor tweak: in the cons constructor, I needed to move the S argument last or I get

invalid occurrence of recursive arg#5 of 'layout.with_edge_sequence.cons', the body of the functional type depends on it.


which we've seen many times before (and is possibly a Lean bug?)

#### Mario Carneiro (Apr 12 2020 at 08:17):

lean doesn't like dependent args after recursive args

#### Mario Carneiro (Apr 12 2020 at 08:17):

in the formal presentation we assume the two are partitioned but it doesn't make a practical difference

#### Kevin Buzzard (Apr 12 2020 at 08:17):

Is it something to do with dots and boxes?

#### Mario Carneiro (Apr 12 2020 at 08:17):

except it's a bit annoying to reorder arguments

#### Mario Carneiro (Apr 12 2020 at 08:18):

I recall this coming up during cyril's work on parametricity since the natural inductive type produced by the algorithm has this kind of out of order problem

#### Scott Morrison (Apr 12 2020 at 09:47):

It's actually going surprisingly well... Down to a few sorries (some easy, some less so :-)

#### Reid Barton (Apr 12 2020 at 12:56):

I think more or less this is one of the examples in one paper on induction-recursion, even.

#### Reid Barton (Apr 12 2020 at 12:57):

Probably not useful any more but: https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.6.4575&rep=rep1&type=pdf Fresh, bottom of page 4

Last updated: May 14 2021 at 13:24 UTC