Rehoming contest

Stream: general

[Eric Wieser]

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

[Yury G. Kudryashov]

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

[Eric Wieser]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

In which file do you need pi.single?

[Johan Commelin]

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

[Eric Wieser]

I need pi.single for a pi instance of nontrivial

[Eric Wieser]

Which I need for a pi instance of group_with_zero

[Yury G. Kudryashov]

a pi instance of group_with_zero

But bool → G₀ is not a group_with_zero

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

BTW, we have docs#function.nontrivial

[Eric Wieser]

#4766

[Eric Wieser]

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

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

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

[Yury G. Kudryashov]

Yes, I meant [has_zero]

[Eric Wieser]

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?

[Kevin Buzzard]

docs#classical.indefinite_description

[Kevin Buzzard]

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

[Eric Wieser]

Shouldn't indefinite_description be a def not a lemma?

[Yury G. Kudryashov]

I guess it should. PR?

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Reid Barton]

That's definitely not true.

[Kevin Buzzard]

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...

[Kevin Buzzard]

def a : ℕ := 4

theorem b : ℕ := 4

example : a = b := rfl -- fails

[Reid Barton]

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).

[Reid Barton]

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

[Bryan Gin-ge Chen]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Yury G. Kudryashov]

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

[Reid Barton]

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

[Reid Barton]

e.g. theorem reals_as_complete_ordered_field := ...

[Bryan Gin-ge Chen]

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

[Reid Barton]

Because Mario said it's intentional

[Reid Barton]

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

[Kyle Miller]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

yeah, same as irreducible