Stream: new members

Topic: inductives

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?

Mario Carneiro (Jun 12 2019 at 12:08):

nested inductives in lean 3 are kind of garbage

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

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?

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


Mario Carneiro (Jun 12 2019 at 12:12):

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

Keeley Hoek (Jun 12 2019 at 12:13):

Ok dreams restored maybe

Thanks!

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

ok.

Keeley Hoek (Jun 12 2019 at 12:16):

EVERYTHING IS BETTER AND DEFINITIONALLY EQUAL NOW AND I LOVE IT

sorry

:D

Keeley Hoek (Jun 12 2019 at 12:28):

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

Mario Carneiro (Jun 12 2019 at 12:30):

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

Mario Carneiro (Jun 12 2019 at 12:32):

the .recs look alright to me

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


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


Mario Carneiro (Jun 12 2019 at 12:56):

the parameters are mashed together

Last updated: May 10 2021 at 17:39 UTC