Zulip Chat Archive

Stream: general

Topic: Another non-transitivity


view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:24):

While trying to prove that lean doesn't have any other sources of definitional non-transitivity besides K-like eliminators, I discovered another one, quotients of propositions:

variables (α : Prop) (r : α → α → Prop) (β : Sort*)
  (f : α → β) (H : Π (a b : α), r a b → f a = f b) (a : α)
example : quot.lift f H (quot.mk r a) = f a := rfl
example (h : quot r) : quot.lift f H h = quot.lift f H (quot.mk r a) := congr rfl rfl
example (h : quot r) : quot.lift f H h = f a := sorry

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:27):

Note that a quotient of a proposition is always useless, because propositions are already subsingletons. Maybe we should just make quot always live in Type, even if the input is a Prop?

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:37):

What do we gain by doing that?

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:37):

doing what

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:38):

Putting quot in Type even when the input is a Prop

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:39):

The source of non-transitivity is when the major premise of an iota rule is a proof, while the resulting type is a Type

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:39):

This happens exactly when the inductive type is a Prop but it "large eliminates"

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:40):

Is the kind of price that you pay only when you're in that situation?

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:40):

And quot p acts like a large eliminator in this case because lift has target Type

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:41):

The issue is that you can arbitrarily muck with the major premise and extract data from it even though it's a prop

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:42):

A bit as if your the quot framework acted as an axiom of choice?

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:42):

Any other time it's not a problem - if the type itself is in Type then the major premise is not subject to proof irrelevance, and if it is a small eliminator then anything that results will also be subject to proof irrelevance

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:43):

It's not quite axiom of choice level, because large elimination is only sound in the first place when there is exactly one thing that can be in the major premise... but that's only up to definitional equality and there are potentially many ways to write it

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:43):

This is where undecidability of defeq arises

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:44):

The thing I'm worried about is if you build something on top of quot and you need functions of type Sort u -> Sort u, putting quot in Type may require you to have complicated universe expressions and force you to deal with types that live in different universes.

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:45):

For example, consider the definitional equality quot.lift f H h = f a in the example above. Where would it get a from to perform that reduction?

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:45):

It's a proof, so it is "unique"... but that doesn't make the problem easier

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:46):

The other alternative, which was actually in use for a while, is to have quot : Type u -> Type u like so many other things

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:46):

I think it was generalized to Sort because no one saw any harm in it

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:48):

Yeah I see. I find myself siding with Type u -> Type u. I wonder if that rules out anything useful

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:48):

You can recover quot on Sort, without quite as many definitional rules, by simply using quot (plift p)

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:50):

Oh nice! I like that. In the general case, quot is cheap (from a design perspective) and you only pay a price for exotic uses

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:51):

I think I would prefer quot : Sort u -> Sort (max 1 u) since it is the axiomatic one, and quotient : Type u -> Type u. This should avoid most universe unification problems

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:51):

Yeah, you're right

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:52):

Just to be sure. You're saying that this example demonstrate undecidability of defeq. Does that mean that the current type checker does not terminate on this example?

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:53):

No, the current typechecker does not accept those definitional equalities

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:53):

even though they are composed from acceptable definitional equalities

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:55):

Right but it is a known state of affair that definitional equalities are not transitive, no?

view this post on Zulip Mario Carneiro (Mar 02 2018 at 01:55):

Right, hence "another non-transitivity"

view this post on Zulip Simon Hudon (Mar 02 2018 at 01:56):

What I'm asking is why do we need to avoid this one?

view this post on Zulip Mario Carneiro (Mar 02 2018 at 02:01):

Because it is preferable to have a reasonable story for how defeq works and to only break it with good reason. (Full disclosure: this is also going to add another page to my paper, for a dumb edge case that I am positive is currently completely unused)

view this post on Zulip Mario Carneiro (Mar 02 2018 at 02:02):

In fact, I've even had conversations discussing putting acc in Type to avoid exactly this problem, and that's a much bigger deal

view this post on Zulip Simon Hudon (Mar 02 2018 at 02:02):

(About the disclosure: are you telling me that you're being paid by the big definitional equality industry?)

view this post on Zulip Mario Carneiro (Mar 02 2018 at 02:03):

I guess I am, in a way...

view this post on Zulip Simon Hudon (Mar 02 2018 at 02:03):

What's the consequence of putting acc in Type?

view this post on Zulip Mario Carneiro (Mar 02 2018 at 05:04):

Again, it eliminates issues caused by large elimination. If acc was in Type and quot was in type, then definitional equality would be decidable, transitive, all that good stuff

view this post on Zulip Gabriel Ebner (Mar 02 2018 at 08:09):

I had already submitted a PR to move acc into Type once: https://github.com/leanprover/lean/pull/1803 But of course it got rejected. The comments on the PR are an interesting read, though.

view this post on Zulip Gabriel Ebner (Mar 02 2018 at 08:23):

Just if anybody else wondered, congr rfl rfl in the original post is definitionally equal to rfl. And if I see this correctly, my PR would not fix this issue.

view this post on Zulip Sean Leather (Mar 02 2018 at 08:51):

https://github.com/leanprover/lean/pull/1803#issuecomment-325014390 :

If "several people" == @digama0, then it doesn't count :)

Ouch! :open_mouth:

view this post on Zulip Patrick Massot (Mar 02 2018 at 09:05):

Yes, I'm very worried by that paper @Mario Carneiro is writing. I don't understand anything about type theory but, to me, it sounds like Mario is scientifically documenting some weakness of Lean (which is irrelevant to end users and doesn't allow to prove false). In principle this is fair. But is it a smart diplomatic move? How could that improve the little "communication issue"?

view this post on Zulip Patrick Massot (Mar 02 2018 at 09:10):

I have a recurrent question: should I learn what "subsingleton" means? If yes, where?

view this post on Zulip Chris Hughes (Mar 02 2018 at 09:11):

Subsingleton just means a type with 0 or 1 elements

view this post on Zulip Patrick Massot (Mar 02 2018 at 09:11):

I understand that bit. It doesn't explain why it comes up all the time, always with "elimination" in the same neighborhood

view this post on Zulip Simon Hudon (Mar 02 2018 at 09:12):

In the context of Lean, that includes any Prop. I believe it's a generalization of proof irrelevance.

view this post on Zulip Simon Hudon (Mar 02 2018 at 09:13):

When checking if two terms are the same, you ignore proof terms and you can ignore subsingleton types.

view this post on Zulip Patrick Massot (Mar 02 2018 at 09:14):

I see

view this post on Zulip Patrick Massot (Mar 02 2018 at 09:14):

Thanks

view this post on Zulip Gabriel Ebner (Mar 02 2018 at 10:31):

@Simon Hudon That's just proof irrelevance. @Patrick Massot Subsingleton is a type with at most one element (we have the subsingleton type class for that). Subsingleton elimination is something slightly different: usually, inductive data types in Prop only allow you to eliminate into Prop. For example, the recursor for ∃ only allows you to obtain propositions, if you could eliminate into Type, then you could extract the witness and thereby prove choice. Subsingleton elimination is now a relaxation of this restriction: in some cases it is perfectly sound for the recursor of an inductive proposition to eliminate into Type: intuitively, if you don't get any additional "data" when eliminating (such as constructor arguments that are in Type, or which constructor of the inductive proposition is used). For example, ∧, false, true, all eliminate into Type.

view this post on Zulip Patrick Massot (Mar 02 2018 at 10:45):

Thanks for your explanation but I'm afraid I'm missing too much background. Can you explain what "∧ eliminate into Type" means? Maybe with an example? I know about and.elim but I don't see any Type here, only Prop.

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:47):

Thanks for your explanation but I'm afraid I'm missing too much background. Can you explain what "∧ eliminate into Type" means? Maybe with an example? I know about and.elim but I don't see any Type here, only Prop.

look at and.rec

view this post on Zulip Kevin Buzzard (Mar 02 2018 at 10:49):

Compare with Exists.rec [sorry, typo fixed]

view this post on Zulip Gabriel Ebner (Mar 02 2018 at 10:59):

Example:

-- and eliminates into Type, this means that in the
-- recursor we can return values e.g. of type nat : Type
#check @and.rec true true  (λ h₁ h₂, 5) ⟨⟨⟩,⟨⟩⟩

-- however Exists does not eliminate into Type (just
-- into Prop), we cannot return values of type nat : Type,
-- just propositions
#check @Exists.rec _ (λ x : , true)  (λ witness h, 5) 1, trivial
             -- could use witness here, so forbidden ^

The second example fails, since nat is not in Prop.

view this post on Zulip Patrick Massot (Mar 02 2018 at 11:50):

Thank you very much. I was confused by the type of and.elim. Since it only wraps and.rec, why do we have a different type here?

view this post on Zulip Gabriel Ebner (Mar 02 2018 at 12:39):

The .rec one is the one generated by the kernel, and is the only one that matters (for foundational purposes). I don't know the reason behind the .elim redefinitions, my best guess is that they correspond to the inference rules in natural deduction (which obviously only talk about Prop).

view this post on Zulip Simon Hudon (Mar 02 2018 at 18:35):

Thanks for correcting my mistake


Last updated: May 11 2021 at 22:14 UTC