mutually inductive type and function

Stream: general

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Bryan Gin-ge Chen]

Oh, now I think I know. :joy:

[Mario Carneiro]

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

[Mario Carneiro]

do you have a MWE?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

lean doesn't like dependent args after recursive args

[Mario Carneiro]

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

[Kevin Buzzard]

Is it something to do with dots and boxes?

[Mario Carneiro]

except it's a bit annoying to reorder arguments

[Mario Carneiro]

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]

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

[Reid Barton]

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

[Reid Barton]

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