more than one ext lemma

Stream: general

[Kevin Buzzard]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Scott Morrison]

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

[Kevin Buzzard]

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