Zulip Chat Archive

Stream: general

Topic: Specialized `ext` lemmas


view this post on Zulip Yury G. Kudryashov (May 01 2020 at 20:04):

Would it be hard to make ext use more information to match lemmas? There are (in mathlib or not yet) specialized ext lemmas for (additive/multiplicative/linear/ring/algebra) homomorphisms from nat, int, submodule.quotient, monoid_algebra, finsupp=direct_sum, multiset, free_*.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 20:04):

Now I'm adding *hom_ext lemmas and applying them explicitly.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 20:07):

I'm talking about, e.g., (f g : free_group α →* G) (h : ∀ x : α, f (of x) = g (of x)) : f = g or (f g : nat →+ A) (h : f 1 = g 1) : f = g, or (p : submodule R M) (f g : p.quotient →ₗ[R] M₂) (h : ∀ x : M, f (quotient.mk x) = g (quotient.mk x)) : f = g.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 20:08):

We can use ext ⟨x⟩ instead of the last one but not for the other lemmas.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 20:09):

A few more: (f g : (α →₀ A) →+ B) (h : ∀ a b, f (single a b) = g (single a b)) : f = g, (f g : monoid_algebra k G →ₐ[k] A) (h : ∀ a, f (single a 1) = g (single a 1)) : f = g.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 20:13):

Another possibility: make ext aware of priority and make all these lemmas have higher priority than generic ones. If the top-priority lemma fails, ext should try the next one.

view this post on Zulip Kevin Buzzard (May 01 2020 at 20:38):

Is it clear what someone wants ext to do in practice? Do they always want the most aggressive one?

view this post on Zulip Reid Barton (May 01 2020 at 20:40):

I wouldn't be surprised if ext was automatically aware of priority; did you try it?

view this post on Zulip Reid Barton (May 01 2020 at 20:41):

I think I remember @Floris van Doorn saying that some kind of enumerating over declarations with a given tag orders by priority by default

view this post on Zulip Floris van Doorn (May 11 2020 at 19:02):

The tactic attribute.get_instances returns a list ordered by priority, the first element has the highest priority. If priorities are tied then it depends on when a declaration is given (and probably the order in which you import files).

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 19:06):

Thank you. I forgot to post here that I've tried adding extra @[ext] attributes and it worked. I'll PR some of those @[ext]s.


Last updated: May 12 2021 at 23:13 UTC