fintype.card

Stream: general

[Reid Barton]

This works if I comment out the first, unneeded import.

import data.set.finite
import data.fintype

local attribute [instance, priority 1] classical.prop_decidable

-- set_option trace.class_instances true
variables {n : ℕ} {H : set (fin n)} (hH : fintype.card H > 3)
-- maximum class-instance resolution depth has been reached ...

[Reid Barton]

Anyone know what's going on? Or is there a better way to state the hypothesis?

[Chris Hughes]

Is it decidable_mem_of_fintype and subtype.fintype cycling? That's a guess without Lean in front of me.

[Reid Barton]

Yeah it looks like it

[Reid Barton]

At least, decidable_mem_of_fintype is definitely involved

[Reid Barton]

Can I locally make it not an instance?

[Reid Barton]

Well I locally gave it priority 0 and that seems to have fixed it

[Violeta Hernández]

As of recent, we have a new docs#finite typeclass, meant to be a version of fintype without computability. So I'm wondering, shouldn't we move the existing docs#fintype.card to finite.card, or at least create that alternate definition?

[Violeta Hernández]

We have many theorems relating docs#fintype.card and docs#cardinal.mk, and the cardinal API is already overwhelmingly noncomputable, so doing the same for the finite portion of the API would be nice..

[Violeta Hernández]

@Yury G. Kudryashov I suppose you've thought about this?

[Kyle Miller]

You can use docs#nat.card, which is better than a finite.card since it doesn't need a typeclass argument so has no dependent type issues.

[Kyle Miller]

I think it would be nice to change nat.card to be defined directly in terms of the existence of a finite instance, since that way it can be defined on Sort and would have fewer dependencies (no need for cardinals)

[Kyle Miller]

Violeta Hernández said:

shouldn't we move the existing docs#fintype.card to finite.card

There's still use for fintype.card -- it's the way to actually compute a cardinality, if that's something you want to do.

[Violeta Hernández]

Wait, there's two different suggestions here: use nat.card which doesn't have a typeclass argument, and redefine nat.card so that it has finite as a typeclass argument. What's the play then?

[Violeta Hernández]

I would rather prefer the latter approach. First because finite is a Prop, which means we seldom have dependent type issues to begin with, and second because I can't personally see much use in the junk values of nat.card.

[Kyle Miller]

@Violeta Hernández Are you referring to my "I think it would be nice" comment? I mean use docs#nat.card_eq as the definition.

[Violeta Hernández]

Oh I see

[Violeta Hernández]

My point stands, I'd rather ditch that in favor of finite.card

[Kyle Miller]

Violeta Hernández said:

First because finite is a Prop, which means we seldom have dependent type issues to begin with

Hold on, I'll pull up our last discussion about this

[Violeta Hernández]

Seems annoying to not have theorems like card α = 0 ↔ is_empty α

[Violeta Hernández]

If you really insist on not having the finite typeclass argument, then I believe the correct approach is to have an enat-valued function instead

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2314373.20.60finite.60.20predicate/near/283930474

[Kyle Miller]

The point is that you don't use nat.card unless you know it's finite. So long as you have a finite instance around, you can apply lemmas about nat.card just fine without worrying about junk values. The function itself doesn't need to have the typeclass argument.

[Violeta Hernández]

Ah, I get your point now

[Violeta Hernández]

Then I agree, this is the approach we should be taking

[Yury G. Kudryashov]

BTW, enat.card is a nice function too.

[Yury G. Kudryashov]

(especially once we redefine enat as with_top nat and establish all the relevant instances)

[Kyle Miller]

(It's true that there are some lemmas that take advantage of the fact that 0 is the junk value, like docs#nat.card_prod, but that's just for convenience to make it easier to apply.)

[Yury G. Kudryashov]

We can define

def enat.card (α : Sort*) : enat :=
if h : finite α then (@finite.exists_equiv_fin α h).some else top

[Violeta Hernández]

I think the plan of action should be to completely redo data/finite/card.lean in terms of a new definition nat.card which depends only on the finite API and not on cardinals, then change the theorems on cardinals that are stated in terms of fintype.card to use nat.card

[Violeta Hernández]

And we can also go ahead and define enat.card in this same file, can't hurt

[Yury G. Kudryashov]

nat.card α = (enat.card α).to_nat

[Violeta Hernández]

Oh that's great

[Yury G. Kudryashov]

Where to_nat n = n.untop' 0

[Yury G. Kudryashov]

See recently merged docs#with_top.untop'

[Yury G. Kudryashov]

(I don't know if the link works because half of websites don't work for me and many other people in Canada today)

[Violeta Hernández]

It does, don't worry

[Violeta Hernández]

Would be nice to have mul defined on enat so that 0 * ⊤ = 0

[Violeta Hernández]

That way we'd have enat.card (α × β) = enat.card α * enat.card β

[Yury G. Kudryashov]

Multiplication on with_top is defined this way.

[Violeta Hernández]

Darn

[Violeta Hernández]

This is the third inconvenience I come across regarding enat while working on this

[Violeta Hernández]

The first was the lack of with_top.unbot' and the second was some very simple missing simp lemmas

[Violeta Hernández]

I think I'm going to do the enat refactor first

[Violeta Hernández]

Nobody planned on doing that just yet, right?

[Yury G. Kudryashov]

Note that some parts of the library use with_top nat, some parts use enat. In particular, there is some theory about with_top nat before enat is defined.

[Violeta Hernández]

Are there any reasons for having enat := with_top nat instead of just using with_top nat?

[Kevin Buzzard]

This is probably historical. enat is (or was, I've not been paying attention) some weird constructive version of with_top nat which constructively has a different "topology" and is much harder to use if you don't understand get_or_else but makes more things computable. Or something.

[Yury G. Kudryashov]

It makes other things computable.

[Eric Rodriguez]

can someone explain how enat actually works? I'm still very confused about it

[Yury G. Kudryashov]

I don't know whether we should have defs or notations for things like nnreal, ennreal, enat.

[Yury G. Kudryashov]

Currently, enat = part nat, see docs#enat docs#part

[Yury G. Kudryashov]

So, it has two fields dom : Prop and get : dom → nat`.

[Yury G. Kudryashov]

E.g., it can be a pair ∃ n, p n and nat.find_min. If p is a decidable predicate, then this is a computable enat.

[Eric Rodriguez]

right, but how does this allow different things than with_top nat? Does it allow you to "defer" whether something is computable/noncomputable till later?

[Kevin Buzzard]

It allows you to not be able to use the equation compiler any more, that's one thing it allows for sure.

[Wrenna Robson]

Why is with_top nat not computable?

[Yury G. Kudryashov]

Other things are computable in with_top nat.

[Yury G. Kudryashov]

In order to create a computable value of type with_top nat, you need to know if it is equal to top or not.

[Yury G. Kudryashov]

In case of part nat, you postpone this decision.

[Yury G. Kudryashov]

So, e.g., if p : nat -> Prop is a decidable predicate, then you can define a computable value find_min p : enat. In order to actually get a value, you'll need to provide a proof of the fact that p n is true for some n.

[Violeta Hernández]

What sorts of computability does enat make possible that with_top ℕ does not, and viceversa?

[Violeta Hernández]

And are there any actual circumstances in mathlib where we care about this?

[Violeta Hernández]

The current state of affairs, where we use enat := part ℕ to mean with_top ℕ is clearly undesirable. I see various possible approaches:

• make enat := with_top ℕ, use it instead of with_top ℕ
• ditch enat entirely in favor of with_top ℕ
• use with_top ℕ everywhere unless whatever computability enat provides is a concern, in which case we use enat

[Violeta Hernández]

The first two solutions are undesirable if there's any circumstances where we actually care about the computability enat provides. The third one is the most conservative but will either leave us with lots of duplicate API, or a still annoyingly limited API for enat (though we wouldn't care much for this anymore).

[Eric Wieser]

Really the choice is about whether constructing enats is usually computable (part) or whether destructing them in the "obvious" way is always computable (with_top)

[Eric Wieser]

There's the same choice at play between docs#free_abelian_group and docs#dfinsupp I think (finsupp cheats and makes nothing computable)

[Eric Wieser]

free_abelian_group.lift $ pi.single i 1 can only extract a coefficient computably if the indices have decidable equality, while free_abelian_group.of doesn't need decidable equality; dfinsupp is the reverse

[Violeta Hernández]

Hmm... so maybe the conservative approach is the correct one

[Eric Wieser]

I think this is one of the arguments against being constructive; it makes classically equivalent constructions non-equivalent, and people who don't care about constructivity will see only downsides to having two ways to spell the "same" thing

[Kevin Buzzard]

@Violeta Hernández one point of view which has occasionally helped me in the past is this: constructively all functions are continuous, and these constructions we make in type theory for some reason come with some kind of internal topology which I don't really understand but I think might even be half the point of homotopy type theory. With this viewpoint, if I remember correctly (and I may well not!) then with_top nat is just naturals (discrete) disjoint union infinity (more discrete stuff) whereas I think enat is more like {1/(n+1) : n in nat} union {0}, so it has a different topology to with_top nat` and thus different functions to and from these different topological spaces are continuous.

[Kevin Buzzard]

I think I might have it the right way around because you can use the equation compiler to define a function on with_top nat which is X for top and Y for everything else, whereas this would not be continuous as a function from {1/(n+1)} union {0}. I think my dislike of with_top nat came precisely because I was using it in a situation where I wanted to precisely define lots of functions of this X Y form above and it was a kerfuffle.

[Violeta Hernández]

I see...

[Violeta Hernández]

I do think we should evaluate whether we're doing anything constructive that warrants enat and not with_top nat

[Violeta Hernández]

But in the meanwhile, we should port anything that isn't constructive to use with_top nat

[Violeta Hernández]

And specify in the enat documentation that unless computability is a concern, you should be using with_top nat

[Violeta Hernández]

...is this a good plan of action?

[Mario Carneiro]

I don't think any decision or refactor needs to be done on enat / with_top nat at this time, but the discussed extended nat.card function should have codomain with_top nat

[Yury G. Kudryashov]

Note that we have ennreal = with_top nnreal. @Mario Carneiro What do you think about "rename enat, use enat name for with_top nat"?

[Eric Wieser]

Maybe rename enat to part_nat?

[Yury G. Kudryashov]

part_enat?

[Mario Carneiro]

if it's going to be called part_nat, there's probably no point in the definition? Or does it have additional instances beyond what part nat would have?

[Mario Carneiro]

The usual notation for this type is something like $\mathbb{N}^\infty$, not sure if that helps

[Violeta Hernández]

How should we name the functions for cardinality returning ℕ and with_top ℕ?

[Violeta Hernández]

Maybe nat.card and nat.card_top?

[Violeta Hernández]

Also, is there any place where we have specialized lemmas for with_top ℕ?

[Violeta Hernández]

My imports must be really weak, since simp isn't being able to prove ↑(x + y) = ↑x + ↑y

[Violeta Hernández]

Oh wait, it's docs#with_top.coe_add

[Violeta Hernández]

Shouldn't this be marked simp?

[Violeta Hernández]

Apparently the answer is "no", since doing this change breaks a bunch of proofs in nontrivial ways

[Violeta Hernández]

I guess ↑(a + b) is useful in that it's structurally obvious that it's a coercion, while ↑a + ↑b doesn't quite have this same feature

[Violeta Hernández]

#15226

[Eric Rodriguez]

docs#enat.card exists, btw

[Eric Rodriguez]

I understand that enat is bad but at least worth linkign

[Violeta Hernández]

I think the solution here is to remove that in this same PR

[Violeta Hernández]

nat.card_top now does this but better

[Yaël Dillies]

I'm not a huge fan of changing the API from enat to with_top ℕ whimsically.

[Yaël Dillies]

Don't you have theorems to prove, Violeta? :-)

[Violeta Hernández]

I'm joining a larger effort to move away from fintype and into finite in noncomputable contexts, and this is a necessary step to do so

[Violeta Hernández]

Well, not the enat to with_top ℕ part, but the nat.card part

[Violeta Hernández]

Also, moving away from enat isn't a "just because" move, the idea is that we shouldn't have been using enat to begin with because we didn't care about the weird computability enat provided

[Violeta Hernández]

Also also, I am proving theorems! This refactor business is just a side thing.

[Violeta Hernández]

I decided to split off the enat.card → nat.card_top refactor: #15233

[Violeta Hernández]

Fortunately it seems like enat.card wasn't used much to begin with

[Violeta Hernández]

Not sure if we have a consensus on whether this is a good idea, but now would be a good time to discuss

[Yury G. Kudryashov]

I suggest that we rename first, #15235

[Yury G. Kudryashov]

Then we add lemmas about enat (defined as with_top nat) and redefine enat.card

[Yury G. Kudryashov]

I have a branch with new enat but it's not ready yet.

[Violeta Hernández]

Alright, I'll put these PRs on hold then

[Yury G. Kudryashov]

@Mario Carneiro I suggest that we use this notation for enat := with_top nat and use part_enat := part nat as a "enat implementation for a few cases where we care about that kind of computability".

[Violeta Hernández]

I just want to reiterate that I'm in favor of this

[Yury G. Kudryashov]

UPD: probably, it was you who suggested this. Sorry for incorrectly claiming credit for this.

[Violeta Hernández]

I really only got the idea after discussing it with you, so I'd say it was a joint effort

[Wrenna Robson]

Where's "new enat" at?

[Violeta Hernández]

^

[Wrenna Robson]

Aye, I meant "since this conversation last month"..

[Violeta Hernández]

Oh no, I'm repeating your question

[Yury G. Kudryashov]

Hi, I'm going over 2 months of backlog. We have enat = with_top nat now.