Zulip Chat Archive

Stream: mathlib4

Topic: Data.Finset.Basic mathlib4#1555

Johan Commelin (Jan 13 2023 at 20:24):

I started a PR for this milestone.

Eric Wieser (Jan 13 2023 at 20:29):

Can we throw out the adhoc one entirely this time? I feel it just got in the way for Fin.Basic

Johan Commelin (Jan 13 2023 at 20:30):

I did

Johan Commelin (Jan 13 2023 at 20:31):

For Fin.Basic we also tried that. But Data/UInt (a new file) relied on it.

Johan Commelin (Jan 13 2023 at 20:32):

A promising start:

-- import Mathlib.Tactic.Apply
-- import Mathlib.Tactic.NthRewrite.Default
-- import Mathlib.Tactic.Monotonicity.Default

Johan Commelin (Jan 13 2023 at 21:04):

I need to do some other stuff. So please feel free to take over.

Johan Commelin (Jan 14 2023 at 05:16):

finset.disj_union and finset.disj_Union both exist.
What should their Lean 4 names become?

Johan Commelin (Jan 14 2023 at 05:18):

Currently they both translate to Finset.disjUnion. Lean 4 doesn't like that. And I can't really blame it :grinning:

Johan Commelin (Jan 14 2023 at 05:20):

Should the latter translate to Finset.disj⋃nion instead? :rofl:

Johan Commelin (Jan 14 2023 at 06:22):

Or maybe we should call the former disjunion?

Eric Wieser (Jan 14 2023 at 07:23):

This is just union vs Union again

Eric Wieser (Jan 14 2023 at 07:23):

So it should be disjUnionᵢ

Yaël Dillies (Jan 14 2023 at 08:47):

Johan Commelin said:

Should the latter translate to Finset.disj⋃nion instead? :rofl:

That would be such a trap :laughing:

Alistair Tucker (Jan 14 2023 at 13:55):

My naive reading of the naming convention suggests that the structure field Nodup : Nodup should be noDup : NoDup?

Eric Wieser (Jan 14 2023 at 13:56):

What did we do for Iist?

Chris Hughes (Jan 14 2023 at 13:57):

The convention that seems to be done in practice is that anything that was one word in Lean3 is also one word in Lean4, without underscores or upper case in the middle

Mario Carneiro (Jan 14 2023 at 13:59):

on list it's Nodup

Mario Carneiro (Jan 14 2023 at 13:59):

Data.AList even has Nodupkeys

Alistair Tucker (Jan 14 2023 at 14:00):

Ok that would be nodup : Nodup then

Chris Hughes (Jan 14 2023 at 14:00):

Mario Carneiro said:

Data.AList even has Nodupkeys

Zero thought went into this decision

Mario Carneiro (Jan 14 2023 at 14:01):

my preference is for Nodup and NodupKeys

Alistair Tucker (Jan 14 2023 at 14:04):

If someone would like to give me the rights, I can commit this very minor change to make it nodup : Nodup

Chris Hughes (Jan 14 2023 at 14:05):

What is your github username?

Alistair Tucker (Jan 14 2023 at 14:06):

agjftucker

Johan Commelin (Jan 16 2023 at 06:54):

Great job at cleaning up the errors in this file!

Johan Commelin (Jan 16 2023 at 06:55):

There are two linter errors left, of the form

@[simp, norm_cast]
theorem coe_filter (s : Finset α) : ↑(s.filter p) = ({ x ∈ ↑s | p x } : Set α) :=
  Set.ext fun _ => mem_filter
/- simplify fails on left-hand side:
tactic 'simp' failed, nested error:
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit) -/