inductives

Stream: new members

[Keeley Hoek]

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]

nested inductives in lean 3 are kind of garbage

[Mario Carneiro]

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]

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]

the correct equivalent of foo is

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

[Mario Carneiro]

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

[Keeley Hoek]

Ok dreams restored maybe

[Keeley Hoek]

Thanks!

[Mario Carneiro]

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

[Keeley Hoek]

ok.

[Keeley Hoek]

EVERYTHING IS BETTER AND DEFINITIONALLY EQUAL NOW AND I LOVE IT

[Keeley Hoek]

sorry

[Keeley Hoek]

:D

[Keeley Hoek]

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

[Mario Carneiro]

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

[Mario Carneiro]

the .recs look alright to me

[Keeley Hoek]

@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]

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]

the parameters are mashed together