Zulip Chat Archive

Stream: new members

Topic: Inductive decls


view this post on Zulip Keeley Hoek (May 31 2019 at 08:00):

Why is it illegal to declare

inductive foo
| mk (f : foo → ℕ)

view this post on Zulip Keeley Hoek (May 31 2019 at 08:01):

whereas

inductive foo'
| mk (f : ℕ → foo')

is fine?

view this post on Zulip Keeley Hoek (May 31 2019 at 08:01):

Is there an (easy?) proof of false?

view this post on Zulip Edward Ayers (May 31 2019 at 08:23):

I think the first problem is that it's not clear what the recursor should be.

view this post on Zulip Kenny Lau (May 31 2019 at 08:24):

yeah I was thinking about that.

view this post on Zulip Edward Ayers (May 31 2019 at 08:25):

And then all of the sensible definitions of rec let you make infinite descending terms. edit: or derive false or something.

view this post on Zulip Edward Ayers (May 31 2019 at 08:27):

The thing to look up is called "strict positivity"

view this post on Zulip Rob Lewis (May 31 2019 at 08:32):

It's easy enough to adapt examples like this one: https://cstheory.stackexchange.com/questions/14415/guarded-negative-occurrences-in-definition-of-inductive-types-always-bad

constant foo : Type
constant mk {α} (f : foo  α) : foo
constant inj {α} : Π x : foo, {f : foo  α // x = mk f}

noncomputable def self_app {α} (a : foo) : α :=
let f, hf := inj a in f a

noncomputable def ta {α} (nf : α  α) : α := self_app $ mk $ λ a, nf $ self_app a

example : false := ta id

view this post on Zulip Keeley Hoek (May 31 2019 at 08:42):

Awesome! Thanks for the demo.
If I make mk increase universe level by one the demo fails;

universe u

constant foo : Type u
constant mk {α} (f : foo.{u}  α) : foo.{u + 1}
constant inj {α} : Π x : foo, {f : foo  α // x = mk f}

noncomputable def self_app {α} (a : foo) : α :=
let f, hf := inj a in f a

noncomputable def ta {α} (nf : α  α) : α := self_app $ mk $ λ a, nf $ self_app a

example : false := ta id

Am I safe now? If so, is there any way to make lean build this?

view this post on Zulip Rob Lewis (May 31 2019 at 08:58):

universe u

constant foo : Type u
constant mk {α} (f : foo.{u}  α) : foo.{u + 1}
constant inj {α} : Π x : foo, {f : foo  α // x = mk f}

noncomputable def self_app {α} (a : foo) : α :=
let f, hf := inj (mk $ λ _, trivial) in f a

noncomputable def ta {α} (nf : α  α) : α := self_app $ mk $ λ a, nf $ self_app a

example : false := ta id

view this post on Zulip Keeley Hoek (May 31 2019 at 09:27):

Actually, I'm not quite sure I understand---why is \alpha free to vary in those axioms? If I force \alpha to be \nat, can it work?

view this post on Zulip Mario Carneiro (May 31 2019 at 09:30):

the short answer is "no, this type violates cantor's theorem"

view this post on Zulip Mario Carneiro (May 31 2019 at 09:35):

I agree that something is funny in Rob's example. We don't need ta, it's already a contradiction in self_app if we instantiate alpha as false

view this post on Zulip Mario Carneiro (May 31 2019 at 09:36):

and also self_app isn't diagonalizing in the second version

view this post on Zulip Rob Lewis (May 31 2019 at 09:37):

Yeah, I just copied it from the StackOverflow answer, I'm sure there are shorter ways.

view this post on Zulip Mario Carneiro (May 31 2019 at 09:38):

I would guess that you are actually safe if mk bumps the universe, but this is not the sort of definition lean can handle. It's recursive in a weird way - foo.{n+1} is defined in terms of foo.{n}

view this post on Zulip Mario Carneiro (May 31 2019 at 09:41):

Rob, I think that inj is not a reasonable axiom - if you just look at inj it says foo -> foo -> A for all A

view this post on Zulip Rob Lewis (May 31 2019 at 09:41):

Oh, wait, I see what you're saying.

view this post on Zulip Rob Lewis (May 31 2019 at 09:41):

Heh, we just had our coffee break and it's kicking in now.

view this post on Zulip Rob Lewis (May 31 2019 at 09:43):

You're right, that's too strong. But I'm not convinced that bumping the universe saves you, could you explain?

view this post on Zulip Mario Carneiro (May 31 2019 at 09:44):

you have to have a fixed alpha, like Keeley says

view this post on Zulip Mario Carneiro (May 31 2019 at 09:44):

right now you can use mk with one alpha and inj with another - and that's actually what you are doing in the proof, you use mk with true and inj with false

view this post on Zulip Mario Carneiro (May 31 2019 at 09:45):

Imagine you could just define foo.{u+1} := foo.{u} -> nat, that would satisfy all the axioms

view this post on Zulip Mario Carneiro (May 31 2019 at 09:46):

it's not really recursive, since for each fixed u it's a finite number of arrows

view this post on Zulip Mario Carneiro (May 31 2019 at 09:47):

in fact such a type probably even exists, since Set.{u} grows faster than foo.{u}

view this post on Zulip Mario Carneiro (May 31 2019 at 09:54):

Thinking about it more carefully, I think this is not definable. If it was, then we could define level.{u} : nat which is equal to u as a nat

view this post on Zulip Mario Carneiro (May 31 2019 at 09:56):

Set.{u} almost lets you define level, but you can only guarantee u or more inaccessible cardinals in it. There is a sort of cardinal collapsing property here - the theory can't tell if you just take one of the Type u universes out and shift the indexes of everything else down

view this post on Zulip Keeley Hoek (May 31 2019 at 09:57):

Looking at Set more than I have before, it seems like the way to get around having a foo -> Prop is choosing an indexing type \alpha and looking at maps \alpha -> foo instead. Since you can choose the indexing type as large as you want, isn't there some sort of bijection between these two pieces of data?

view this post on Zulip Mario Carneiro (May 31 2019 at 09:58):

that's why Set lives in a higher universe

view this post on Zulip Keeley Hoek (May 31 2019 at 09:58):

(modulo a quotient of such maps by permutations of the indexing type and change of indexing type)

view this post on Zulip Mario Carneiro (May 31 2019 at 09:58):

you can't instantiate Set.{u} with Set.{u} as the index type

view this post on Zulip Keeley Hoek (May 31 2019 at 10:00):

For sure

view this post on Zulip Mario Carneiro (May 31 2019 at 10:01):

so you don't get a cantor contradiction, instead you just end up proving that Set.{u} is (a lot) smaller than Set.{u+1}

view this post on Zulip Keeley Hoek (May 31 2019 at 12:21):

Regarding your comments on level, why would it be bad if level.{u} : nat existed?

view this post on Zulip Keeley Hoek (May 31 2019 at 12:21):

(Sorry for using you to learn about type theory)

view this post on Zulip Floris van Doorn (May 31 2019 at 19:05):

(deleted)

view this post on Zulip Mario Carneiro (May 31 2019 at 19:09):

@Keeley Hoek It wouldn't necessarily be bad if level.{u} existed, but I'm pretty sure it's independent

view this post on Zulip Floris van Doorn (May 31 2019 at 19:10):

(oops, I replied to the wrong thread)


Last updated: May 14 2021 at 07:19 UTC