Zulip Chat Archive

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: Aug 03 2023 at 10:10 UTC