Zulip Chat Archive

Stream: general

Topic: mutually inductive type and function


view this post on Zulip 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!)

view this post on Zulip Scott Morrison (Apr 12 2020 at 06:01):

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

view this post on Zulip 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"?

view this post on Zulip Scott Morrison (Apr 12 2020 at 06:02):

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

view this post on Zulip Bryan Gin-ge Chen (Apr 12 2020 at 06:03):

Oh, now I think I know. :joy:

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 06:29):

do you have a MWE?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?)

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:17):

lean doesn't like dependent args after recursive args

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:17):

Is it something to do with dots and boxes?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:17):

except it's a bit annoying to reorder arguments

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 12 2020 at 09:47):

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

view this post on Zulip 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.

view this post on Zulip 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