Zulip Chat Archive

Stream: new members

Topic: inductives


view this post on Zulip Keeley Hoek (Jun 12 2019 at 11:06):

Here are two attempts at the same idea:

structure pairing (β : Type 1) :=
(α : Type)
(f : α  β)

inductive foo (γ : Type) : Type 1
| intro (m : γ  pairing foo) : foo

and

inductive bar : Type 1
| intro : Π (α β : Type) (v : α  bar) (v2 : β  bar), bar

called foo and bar, where bar is evidently isomorphic to foo (fin 2). It seems like the <...>.rec generated for the former is considerably weaker than that for the latter. I think this has something to do with the way nesting inductives is done. Can anyone comment on whether that's what's going on. Is there a way to fix things, while keeping my gamma parameter?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:08):

nested inductives in lean 3 are kind of garbage

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:09):

nested meta inductives aren't bad because lean just rolls with whatever you say, but regular nested inductives have a complicated and buggy compilation

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:11):

Yeah okay damn. This is really depressing. Since I suddenly care about them and haven't been listening prior, are they getting better in lean 4?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:12):

the correct equivalent of foo is

inductive foo (γ : Type) : Type 1
| intro (α : γ  Type) (f :  x, α x  foo) : foo

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:12):

I recommend just hand-unrolling any nested/mutual inductives you need into plain inductives

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:13):

Ok dreams restored maybe

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:13):

Thanks!

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:13):

I think they are being addressed in lean 4, but I don't know how successful it will be, we will see

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:16):

ok.

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:16):

EVERYTHING IS BETTER AND DEFINITIONALLY EQUAL NOW AND I LOVE IT

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:16):

sorry

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:17):

:D

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:28):

Oooh, interesting, I still don't get that more powerful recursor using the unwrapped definition!...

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:30):

is the claim that bar is isomorphic to foo (fin 2)?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:32):

the .recs look alright to me

view this post on Zulip Keeley Hoek (Jun 12 2019 at 12:54):

@Mario Carneiro compare the following:

def test2 (b : bar) : bar :=
begin
  induction b with α β v v2 Ihv Ihv2,
  -- I have Ihv and Ihv2
end

def test (b : foo (fin 2)) : foo (fin 2) :=
begin
  induction b with α β v v2 Ihv Ihv2,
  -- I don't have Ihv and Ihv2
end

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:56):

here are some improved names in the second case:

def test (b : foo bool) : foo bool :=
begin
  induction b with αβ vv2 IhvIhv2,
  let α := αβ ff, let β := αβ tt,
  let v : α  foo bool := vv2 ff,
  let v2 : β  foo bool := vv2 tt,
  have Ihv : α  foo bool := IhvIhv2 ff,
  have Ihv2 : β  foo bool := IhvIhv2 tt,
end

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:56):

the parameters are mashed together


Last updated: May 10 2021 at 17:39 UTC