Zulip Chat Archive

One thing I'm noticing here is that in the order-dualled proofs, putting on (α := αᵒᵈ) speeds things up massively, so it's probably worth doing in all proofs of this form, even if they already typecheck. Named arguments is an amazing feature!

Heather Macbeth (Jan 20 2023 at 22:00):

Another point of view: this used not to be slow; hopefully we can figure out why it has become slow :-(

Eric Rodriguez (Jan 20 2023 at 22:01):

from my completely uneducated guess, Lean4 really doesn't want to modify its guesses about the metavars, whilst lean3 was a bit more free

Eric Rodriguez (Jan 20 2023 at 22:02):

this again just comes from my experience with it and isn't backed by any sentiment but stuff like https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/sensible.20constructor.20for.20.60add_comm_group.60/near/322621160 doesn't help

Heather Macbeth (Jan 20 2023 at 22:04):

It'd be interesting to find out if this is one of the many things improved by lean4#2003

Eric Rodriguez (Jan 20 2023 at 22:06):

is there an easy way to get some code with that branch and toy with it?

Yury G. Kudryashov (Jan 20 2023 at 22:29):

I'm going to work on Data.Set.Finite.

Eric Rodriguez (Jan 20 2023 at 22:31):

I've just done working on it, sorry for the weird merge commits. There's only few things left.

Yury G. Kudryashov (Jan 20 2023 at 22:42):

Did you push?

Yury G. Kudryashov (Jan 20 2023 at 22:45):

About fintypeBUnionᵢ: it seems that simp fails to use Set.mem_toFinset because [Fintype (t _)] is not a local instance. I'm going to add Set.mem_toFinset' that takes {_ : Fintype s} instead of [Fintype s].

Yury G. Kudryashov (Jan 20 2023 at 22:46):

I can't just replace the old lemma because it breaks rewrites right-to-left.

Yury G. Kudryashov (Jan 20 2023 at 22:47):

@Mario Carneiro @Gabriel Ebner What is the correct way to fix this?

Yury G. Kudryashov (Jan 20 2023 at 22:47):

(BTW, should I tag someone else for questions like "how does Lean work?")

Yury G. Kudryashov (Jan 20 2023 at 22:54):

I'm fixing the rest (unused args etc)

Gabriel Ebner (Jan 20 2023 at 22:56):

Indeed, this used to work in Lean 3 because we didn't try to synthesize instances in simp if they were already filled in by unification. https://github.com/leanprover-community/lean/blob/34f41e59146bbda3b58adb23dff350c30093e02b/src/library/tactic/simp_lemmas.cpp#L1368

Yury G. Kudryashov (Jan 20 2023 at 23:03):

What should we do in Lean 4?

Yury G. Kudryashov (Jan 20 2023 at 23:04):

Add lemmas with {} arguments or change something where we want to use this lemma in simp?

Gabriel Ebner (Jan 20 2023 at 23:05):

I'm not a fan of changing things to {} just to make simp happy (and break rw [← ..] in the process).

Yury G. Kudryashov (Jan 20 2023 at 23:07):

As a temporary workaround, I've duplicated a lemma.

Eric Rodriguez (Jan 20 2023 at 23:08):

Yury G. Kudryashov said:

About fintypeBUnionᵢ: it seems that simp fails to use Set.mem_toFinset because [Fintype (t _)] is not a local instance. I'm going to add Set.mem_toFinset' that takes {_ : Fintype s} instead of [Fintype s].

are these Fintype (t _)s only in the term, and they're not getting matched via unification as the hope was that in lean4 that's never necessary? what is the workaround, I agree

Yury G. Kudryashov (Jan 20 2023 at 23:10):

These Fintype (t _) are deduced from h guarded by ∃.

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

Gabriel Ebner said:

Indeed, this used to work in Lean 3 because we didn't try to synthesize instances in simp if they were already filled in by unification.

I think this property extends far beyond simp; there are many cases in Lean 3 where we were happy to use unification instead of typeclass search. There was the thread I made a while back where { foo := 1, bar := 2} used to use unification to find typeclass arguments for my_structure.mk, but now the notation only works if the unification matches inference

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

IIRC it's not that Lean 4 can't do the unification, it's that it makes the conscious decision to discard it unless it can solve the typeclass problem and the solution it finds is the same

Gabriel Ebner (Jan 20 2023 at 23:14):

Here's a different approach that works out-of-the-box:

def fintypeBUnionᵢ [DecidableEq α] {ι : Type _} (s : Set ι) [Fintype s] (t : ι → Set α)
    (H : ∀ i ∈ s, Fintype (t i)) : Fintype (⋃ x ∈ s, t x) :=
  haveI : ∀ i : toFinset s, Fintype (t i) := fun i => H i (by simpa using i.2)
  Fintype.ofFinset (s.toFinset.attach.bunionᵢ fun x => (t x).toFinset) (by simp)

Gabriel Ebner (Jan 20 2023 at 23:16):

IIRC it's not that Lean 4 can't do the unification, it's that it makes the conscious decision to discard it unless it can solve the typeclass problem and the solution it finds is the same

Yes, this is definitely not the only such case. In general it's probably best to arrange things so that instances can always be resynthesized in the same (defeq) way.

Eric Wieser (Jan 20 2023 at 23:33):

That's certainly a nice property to have, but I don't yet see the argument for why the elaborator should force things to always have that property.

Gabriel Ebner (Jan 20 2023 at 23:40):

Because finding instances by unification doesn't mesh well with inheritance, or really any situation where the instances don't match up perfectly. If mem_toFinset required NonemptyFinLinOrd (first child class I could find in the docs) instead of Fintype, then unification alone wouldn't be able to fill that in.