Zulip Chat Archive

Stream: general

Topic: Rehoming contest


view this post on Zulip Eric Wieser (Oct 24 2020 at 15:42):

I need docs#pi.single before its definition in algebra.group.pi. Where can I move it to? data.pi?

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:09):

BTW, why is it not defined in terms of function.update?

view this post on Zulip Eric Wieser (Oct 24 2020 at 16:09):

No idea. You could also ask why all of the other singles aren't defined that way either

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:13):

I understand the answer in the case of a non-dependent function: don't deal with rewriting in the domain.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:13):

In which file do you need pi.single?

view this post on Zulip Johan Commelin (Oct 24 2020 at 16:15):

function.update was introduced after many of the singles already existed, I think

view this post on Zulip Eric Wieser (Oct 24 2020 at 16:16):

I need pi.single for a pi instance of nontrivial

view this post on Zulip Eric Wieser (Oct 24 2020 at 16:16):

Which I need for a pi instance of group_with_zero

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:54):

a pi instance of group_with_zero

But bool → G₀ is not a group_with_zero

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:54):

You don't need pi.single for a pi instance of nontrivial because the pi instance of nontrivial shouldn't use any algebra.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:56):

BTW, we have docs#function.nontrivial

view this post on Zulip Eric Wieser (Oct 24 2020 at 17:07):

#4766

view this post on Zulip Eric Wieser (Oct 24 2020 at 17:10):

I'm not really sure what you by "algebra" there do you mean presence of a zero? I suppose inhabited would suffice instead of has_zero

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 17:21):

Yury G. Kudryashov said:

a pi instance of group_with_zero

But bool → G₀ is not a group_with_zero

It might be a monoid with zero though.

view this post on Zulip Eric Wieser (Oct 24 2020 at 17:23):

Yeah, that was what I concluded in the PR - I can build the monoid_with_zero typeclases, but I can't satisfy the inv 0 = 0 requirements of group_with_zero

view this post on Zulip Eric Wieser (Oct 24 2020 at 17:26):

I'm also unsure whether [∃ i, nontrivial (f i)] is a sane typeclass argument

view this post on Zulip Reid Barton (Oct 24 2020 at 17:27):

In the nondependent case nontrivial (A -> B) the right hypothesis is inhabited A (or nonempty A) and nontrivial B.

view this post on Zulip Reid Barton (Oct 24 2020 at 17:27):

In the dependent case I guess the most sensible option is to use inhabited A and nontrivial (B default)

view this post on Zulip Reid Barton (Oct 24 2020 at 17:39):

Even if you could tell Lean "go try to find some i : A and [nontrivial (B i)], which sounds like a wild goose chase waiting to happen, I can't think of a realistic scenario where that would actually be useful.

view this post on Zulip Reid Barton (Oct 24 2020 at 17:41):

If you really need to use some specific i then that's what haveI is for.

view this post on Zulip Reid Barton (Oct 24 2020 at 17:50):

Oh right, in the dependent case you also need everything to be nonempty too.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 17:52):

Yes, I meant [has_zero]

view this post on Zulip Eric Wieser (Oct 24 2020 at 17:58):

On a related note, is there a shorthand for (classical.some p, classical.some_spec p) so that I can get both in a single let statement with unpacking?

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 17:59):

docs#classical.indefinite_description

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:01):

Indeed, in core Lean we have

noncomputable def some {α : Sort u} {p : α  Prop} (h :  x, p x) : α :=
(indefinite_description p h).val

theorem some_spec {α : Sort u} {p : α  Prop} (h :  x, p x) : p (some h) :=
(indefinite_description p h).property

:D

view this post on Zulip Eric Wieser (Oct 24 2020 at 18:03):

Shouldn't indefinite_description be a def not a lemma?

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:06):

I guess it should. PR?

view this post on Zulip Reid Barton (Oct 24 2020 at 18:09):

I know there's some super obscure reason for something like this but I don't remember if it's this specifically.

view this post on Zulip Reid Barton (Oct 24 2020 at 18:10):

But of course it would be good to PR either a change to make it use def or a comment explaining why it cannot.

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:11):

Yes I have it in my head that this has come up before. In fact I am a bit confused -- I'm surprised that the definition of some doesn't make Lean complain that it has forgotten what the choice is.

view this post on Zulip Eric Wieser (Oct 24 2020 at 18:11):

My understanding is the distinction between def and lemma is totally meaningless, and it just comes down to convention

view this post on Zulip Reid Barton (Oct 24 2020 at 18:12):

That's definitely not true.

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:12):

Theorems and definitions are a bit different, I thought? Theorems don't create code in the VM or something? No idea what I'm talking about...

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:13):

def a :  := 4

theorem b :  := 4

example : a = b := rfl -- fails

view this post on Zulip Reid Barton (Oct 24 2020 at 18:13):

One difference is that the type of a lemma is elaborated without looking at the body (so that the body can be type checked on a separate thread).

view this post on Zulip Reid Barton (Oct 24 2020 at 18:15):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/noncomputable.20theorem/near/136143755

view this post on Zulip Bryan Gin-ge Chen (Oct 24 2020 at 18:17):

Here's an old gist showing that the linter agrees that classical.indefinite_description should be a def. See also this issue on linting the core library: lean#200

view this post on Zulip Reid Barton (Oct 24 2020 at 18:19):

So in this case, the linter is wrong; but I assume we can't put nolints in the core library?

view this post on Zulip Reid Barton (Oct 24 2020 at 18:19):

Presumably, the linter will be wrong more often for stuff in core...

view this post on Zulip Reid Barton (Oct 24 2020 at 18:20):

The link above explains Kevin's example--I had forgotten about this "definition irrelevance".

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:22):

I don't see what's wrong with unfolding classical.some to classical.choice.

view this post on Zulip Reid Barton (Oct 24 2020 at 18:24):

actually, this is a pretty interesting feature--couldn't you use it to provide opaque ML-style modules?

view this post on Zulip Reid Barton (Oct 24 2020 at 18:24):

e.g. theorem reals_as_complete_ordered_field := ...

view this post on Zulip Bryan Gin-ge Chen (Oct 24 2020 at 18:26):

Sorry if I'm missing something - why is the linter wrong in this case?

view this post on Zulip Reid Barton (Oct 24 2020 at 18:26):

Because Mario said it's intentional

view this post on Zulip Reid Barton (Oct 24 2020 at 18:28):

Yury G. Kudryashov said:

I don't see what's wrong with unfolding classical.some to classical.choice.

My understanding is that there's nothing particularly wrong with doing it except that it will never be useful, so we might as well not

view this post on Zulip Kyle Miller (Oct 24 2020 at 18:51):

If it's about unfolding, would it be the same if indefinite_description were an @[irreducible] noncomputable def?

view this post on Zulip Reid Barton (Oct 24 2020 at 18:52):

I don't know for sure, or how to test, but my impression from the earlier discussion is that theorems don't even have a definitional delta rule in the kernel

view this post on Zulip Mario Carneiro (Oct 25 2020 at 05:06):

You can use delta on theorems, although it requires joining on that thread's task

view this post on Zulip Reid Barton (Oct 25 2020 at 16:44):

I see, so... the elaborator just pretends there is no delta rule unless you ask it specifically?

view this post on Zulip Mario Carneiro (Oct 25 2020 at 18:11):

yeah, same as irreducible


Last updated: May 06 2021 at 20:13 UTC