## Stream: general

### Topic: Rehoming contest

#### 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?

#### Yury G. Kudryashov (Oct 24 2020 at 16:09):

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

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

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

#### Yury G. Kudryashov (Oct 24 2020 at 16:13):

In which file do you need pi.single?

#### Johan Commelin (Oct 24 2020 at 16:15):

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

#### Eric Wieser (Oct 24 2020 at 16:16):

I need pi.single for a pi instance of nontrivial

#### Eric Wieser (Oct 24 2020 at 16:16):

Which I need for a pi instance of group_with_zero

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

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

#### Yury G. Kudryashov (Oct 24 2020 at 16:56):

BTW, we have docs#function.nontrivial

#4766

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

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

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

#### Eric Wieser (Oct 24 2020 at 17:26):

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

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

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

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

#### Reid Barton (Oct 24 2020 at 17:41):

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

#### Reid Barton (Oct 24 2020 at 17:50):

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

#### Yury G. Kudryashov (Oct 24 2020 at 17:52):

Yes, I meant [has_zero]

#### 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?

#### Kevin Buzzard (Oct 24 2020 at 17:59):

docs#classical.indefinite_description

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

#### Eric Wieser (Oct 24 2020 at 18:03):

Shouldn't indefinite_description be a def not a lemma?

#### Yury G. Kudryashov (Oct 24 2020 at 18:06):

I guess it should. PR?

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

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

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

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

#### Reid Barton (Oct 24 2020 at 18:12):

That's definitely not true.

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

#### Kevin Buzzard (Oct 24 2020 at 18:13):

def a : ℕ := 4

theorem b : ℕ := 4

example : a = b := rfl -- fails


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

#### Reid Barton (Oct 24 2020 at 18:15):

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

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

#### 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?

#### Reid Barton (Oct 24 2020 at 18:19):

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

#### Yury G. Kudryashov (Oct 24 2020 at 18:22):

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

#### 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?

#### Reid Barton (Oct 24 2020 at 18:24):

e.g. theorem reals_as_complete_ordered_field := ...

#### Bryan Gin-ge Chen (Oct 24 2020 at 18:26):

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

#### Reid Barton (Oct 24 2020 at 18:26):

Because Mario said it's intentional

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

#### 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?

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

#### Mario Carneiro (Oct 25 2020 at 05:06):

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

#### 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?

#### Mario Carneiro (Oct 25 2020 at 18:11):

yeah, same as irreducible

Last updated: May 06 2021 at 20:13 UTC