Zulip Chat Archive

Stream: general

Topic: more than one ext lemma


view this post on Zulip Kevin Buzzard (Jul 18 2020 at 10:54):

I thought I had this nailed, until test3. What is the preferred way of telling ext how to work? Or should every structure have at most one lemma tagged @[ext]?

import tactic

universe u

@[ext] structure submonoid (G : Type u) [monoid G] :=
(carrier : set G)
(mul_mem' :  {a b : G}, a  carrier  b  carrier  a * b  carrier)
(one_mem' : (1 : G)  carrier)

namespace submonoid

#check ext -- ∀ (x y : submonoid ?M_1), x.carrier = y.carrier → x = y

variables {G : Type u} [monoid G]

instance : has_mem G (submonoid G) := ⟨λ g H, g  H.carrier

variables {H J : submonoid G}

@[ext] lemma ext' (h :  x : G, x  H  x  J) : H = J :=
begin
  ext x,
  -- ⊢ x ∈ H.carrier ↔ x ∈ J.carrier
  exact h x,
end

-- I have no idea what the default priorities are

#print ext -- @[_ext_lemma_core] blah
#print ext' -- @[_ext_lemma_core, ext list.nil.{0} ext_param_type] blah


-- check that ext' beats ext
lemma test (H J : submonoid G) : H = J :=
begin
  ext x, -- ⊢ x ∈ H ↔ x ∈ J
  sorry
end

attribute [ext, priority 10] ext'
attribute [ext, priority 10000] ext

-- check that ext beats ext' now
lemma test2 (H J : submonoid G) : H = J :=
begin
  ext x, -- ⊢ x ∈ H.carrier ↔ x ∈ J.carrier
  sorry
end

#print ext -- @[_ext_lemma_core, priority 10000, ext list.nil.{0} ext_param_type, priority 10000] blah
#print ext' -- @[_ext_lemma_core, priority 10, ext list.nil.{0} ext_param_type, priority 10] blah

attribute [ext, priority 10000] ext'
attribute [ext, priority 10] ext

#print ext -- @[_ext_lemma_core, priority 10, ext list.nil.{0} ext_param_type, priority 10] blah
#print ext' -- @[_ext_lemma_core, priority 10000, ext list.nil.{0} ext_param_type, priority 10000] blah

-- Wait -- ext is still beating ext' ??
lemma test3 (H J : submonoid G) : H = J :=
begin
  ext x, -- ⊢ x ∈ H.carrier ↔ x ∈ J.carrier
  sorry
end

-- let's try those same commands again the other way around

attribute [ext, priority 10] ext
attribute [ext, priority 10000] ext'

-- no change in `#print` output

-- ext' now beating ext again
lemma test4 (H J : submonoid G) : H = J :=
begin
  ext x, -- ⊢ x ∈ H ↔ x ∈ J
  sorry
end

end submonoid

view this post on Zulip Chris Hughes (Jul 18 2020 at 11:32):

Looking at the code for the ext attribute, it looks like the priority number is not actually used.

view this post on Zulip Chris Hughes (Jul 18 2020 at 11:32):

Every attribute has a priority setting, but usually it doesn't do anything, and it look like ext is one of these attributes.

view this post on Zulip Chris Hughes (Jul 18 2020 at 11:34):

The attribute is here. The prio argument is used once, but only to pass it to another attribute which doesn't use it.

view this post on Zulip Scott Morrison (Jul 18 2020 at 11:35):

Yeah, I think it's just "most recent wins".

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 11:57):

But fortunately re-tagging makes you more recent -- this is consistent with what we see. Thanks!


Last updated: May 10 2021 at 00:31 UTC