From b54a9ec9b986f4833278caf750ab06c6352fdf7c Mon Sep 17 00:00:00 2001 From: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com> Date: Mon, 26 Aug 2024 08:35:47 -0400 Subject: [PATCH] feat: swap arguments to `Membership.mem` (#5020) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We swap the arguments for `Membership.mem` so that when proceeded by a `SetLike` coercion, as is often the case in Mathlib, the resulting expression is recognized as eta expanded and reduce for many computations. The most beneficial outcome is that the discrimination tree keys for instances and simp lemmas concerning subsets become more robust resulting in more efficient searches. Closes `RFC` #4932 --------- Co-authored-by: Kim Morrison Co-authored-by: Henrik Böving --- src/Init/Data/Array/Mem.lean | 4 +-- src/Init/Data/List/Basic.lean | 2 +- src/Init/Data/List/Sublist.lean | 8 ++--- src/Init/Data/Option/Instances.lean | 2 +- src/Init/Data/Range.lean | 2 +- src/Init/Notation.lean | 2 +- src/Init/Prelude.lean | 2 +- src/Std/Data/DHashMap/Basic.lean | 2 +- src/Std/Data/DHashMap/Raw.lean | 2 +- src/Std/Data/HashMap/Basic.lean | 2 +- src/Std/Data/HashMap/Raw.lean | 2 +- src/Std/Data/HashSet/Basic.lean | 2 +- src/Std/Data/HashSet/Raw.lean | 2 +- src/Std/Sat/AIG/Basic.lean | 2 +- .../LRAT/Internal/Formula/RupAddResult.lean | 6 ++-- tests/lean/run/1986.lean | 2 +- tests/lean/run/3807.lean | 31 ++++++++++++++----- tests/lean/run/3965_3.lean | 2 +- tests/lean/run/binop_binrel_perf_issue.lean | 6 ++-- tests/lean/run/elabAsElim.lean | 2 +- tests/lean/run/setStructInstNotation.lean | 2 +- tests/lean/run/subset.lean | 2 +- 22 files changed, 52 insertions(+), 37 deletions(-) diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean index cda31733b773..32b68e19f777 100644 --- a/src/Init/Data/Array/Mem.lean +++ b/src/Init/Data/Array/Mem.lean @@ -13,11 +13,11 @@ namespace Array /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/ -- NB: This is defined as a structure rather than a plain def so that a lemma -- like `sizeOf_lt_of_mem` will not apply with no actual arrays around. -structure Mem (a : α) (as : Array α) : Prop where +structure Mem (as : Array α) (a : α) : Prop where val : a ∈ as.data instance : Membership α (Array α) where - mem a as := Mem a as + mem := Mem theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by cases as with | _ as => diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index c60845772b99..ff1f9d55ad95 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -689,7 +689,7 @@ inductive Mem (a : α) : List α → Prop | tail (b : α) {as : List α} : Mem a as → Mem a (b::as) instance : Membership α (List α) where - mem := Mem + mem l a := Mem a l theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : List α} : elem a as = true → a ∈ as := by match as with diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 5147a9c2558a..332296e928b1 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -62,8 +62,8 @@ theorem subset_def {l₁ l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ theorem Subset.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ := fun _ i => h₂ (h₁ i) -instance : Trans (Membership.mem : α → List α → Prop) Subset Membership.mem := - ⟨fun h₁ h₂ => h₂ h₁⟩ +instance : Trans (fun l₁ l₂ => Subset l₂ l₁) (Membership.mem : List α → α → Prop) Membership.mem := + ⟨fun h₁ h₂ => h₁ h₂⟩ instance : Trans (Subset : List α → List α → Prop) Subset Subset := ⟨Subset.trans⟩ @@ -197,8 +197,8 @@ instance : Trans (@Sublist α) Subset Subset := instance : Trans Subset (@Sublist α) Subset := ⟨fun h₁ h₂ => trans h₁ h₂.subset⟩ -instance : Trans (Membership.mem : α → List α → Prop) Sublist Membership.mem := - ⟨fun h₁ h₂ => h₂.subset h₁⟩ +instance : Trans (fun l₁ l₂ => Sublist l₂ l₁) (Membership.mem : List α → α → Prop) Membership.mem := + ⟨fun h₁ h₂ => h₁.subset h₂⟩ theorem mem_of_cons_sublist {a : α} {l₁ l₂ : List α} (s : a :: l₁ <+ l₂) : a ∈ l₂ := (cons_subset.1 s.subset).1 diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean index 40c89064ed80..865a958474eb 100644 --- a/src/Init/Data/Option/Instances.lean +++ b/src/Init/Data/Option/Instances.lean @@ -19,7 +19,7 @@ theorem eq_of_eq_some {α : Type u} : ∀ {x y : Option α}, (∀z, x = some z theorem eq_none_of_isNone {α : Type u} : ∀ {o : Option α}, o.isNone → o = none | none, _ => rfl -instance : Membership α (Option α) := ⟨fun a b => b = some a⟩ +instance : Membership α (Option α) := ⟨fun b a => b = some a⟩ @[simp] theorem mem_def {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl diff --git a/src/Init/Data/Range.lean b/src/Init/Data/Range.lean index 6e11f5a14ab0..0de8c9222894 100644 --- a/src/Init/Data/Range.lean +++ b/src/Init/Data/Range.lean @@ -15,7 +15,7 @@ structure Range where step : Nat := 1 instance : Membership Nat Range where - mem i r := r.start ≤ i ∧ i < r.stop + mem r i := r.start ≤ i ∧ i < r.stop namespace Range universe u v diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index c521db2e0648..33967c63995a 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -336,7 +336,7 @@ macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y) @[inherit_doc] infixl:30 " || " => or @[inherit_doc] notation:max "!" b:40 => not b -@[inherit_doc] infix:50 " ∈ " => Membership.mem +@[inherit_doc] notation:50 a:50 " ∈ " b:50 => Membership.mem b a /-- `a ∉ b` is negated elementhood. It is notation for `¬ (a ∈ b)`. -/ notation:50 a:50 " ∉ " b:50 => ¬ (a ∈ b) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index d1d4f1627fd6..aa2a25ad5d0a 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1515,7 +1515,7 @@ of the elements of the container. -/ class Membership (α : outParam (Type u)) (γ : Type v) where /-- The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. -/ - mem : α → γ → Prop + mem : γ → α → Prop set_option bootstrap.genMatcherCode false in /-- diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index a1ec43e8cab2..236593356d75 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -103,7 +103,7 @@ instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where Raw₀.contains ⟨m.1, m.2.size_buckets_pos⟩ a instance [BEq α] [Hashable α] : Membership α (DHashMap α β) where - mem a m := m.contains a + mem m a := m.contains a instance [BEq α] [Hashable α] {m : DHashMap α β} {a : α} : Decidable (a ∈ m) := show Decidable (m.contains a) from inferInstance diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index a1092ae8afc5..b3264a6e059e 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -142,7 +142,7 @@ Observe that this is different behavior than for lists: for lists, `∈` uses `= else false -- will never happen for well-formed inputs instance [BEq α] [Hashable α] : Membership α (Raw α β) where - mem a m := m.contains a + mem m a := m.contains a instance [BEq α] [Hashable α] {m : Raw α β} {a : α} : Decidable (a ∈ m) := inferInstanceAs (Decidable (m.contains a)) diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index 210436a1aeaf..4841318556e7 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -121,7 +121,7 @@ def find? (m : HashMap α β) (a : α) : Option β := m.inner.contains a instance [BEq α] [Hashable α] : Membership α (HashMap α β) where - mem a m := a ∈ m.inner + mem m a := a ∈ m.inner instance [BEq α] [Hashable α] {m : HashMap α β} {a : α} : Decidable (a ∈ m) := inferInstanceAs (Decidable (a ∈ m.inner)) diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index f63bfc68c3a0..5691a5e751a9 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -108,7 +108,7 @@ Tries to retrieve the mapping for the given key, returning `none` if no such map m.inner.contains a instance [BEq α] [Hashable α] : Membership α (Raw α β) where - mem a m := a ∈ m.inner + mem m a := a ∈ m.inner instance [BEq α] [Hashable α] {m : Raw α β} {a : α} : Decidable (a ∈ m) := inferInstanceAs (Decidable (a ∈ m.inner)) diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index 2feab9be33a1..b741c644a261 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean @@ -99,7 +99,7 @@ Observe that this is different behavior than for lists: for lists, `∈` uses `= m.inner.contains a instance [BEq α] [Hashable α] : Membership α (HashSet α) where - mem a m := a ∈ m.inner + mem m a := a ∈ m.inner instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m) := inferInstanceAs (Decidable (a ∈ m.inner)) diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean index 1155b521754c..c5687f67cc90 100644 --- a/src/Std/Data/HashSet/Raw.lean +++ b/src/Std/Data/HashSet/Raw.lean @@ -100,7 +100,7 @@ Observe that this is different behavior than for lists: for lists, `∈` uses `= m.inner.contains a instance [BEq α] [Hashable α] : Membership α (Raw α) where - mem a m := a ∈ m.inner + mem m a := a ∈ m.inner instance [BEq α] [Hashable α] {m : Raw α} {a : α} : Decidable (a ∈ m) := inferInstanceAs (Decidable (a ∈ m.inner)) diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean index 0c6ca9221713..2cdcbb2d9747 100644 --- a/src/Std/Sat/AIG/Basic.lean +++ b/src/Std/Sat/AIG/Basic.lean @@ -223,7 +223,7 @@ def empty : AIG α := { decls := #[], cache := Cache.empty #[], invariant := IsD /-- The atom `a` occurs in `aig`. -/ -def Mem (a : α) (aig : AIG α) : Prop := (.atom a) ∈ aig.decls +def Mem (aig : AIG α) (a : α) : Prop := (.atom a) ∈ aig.decls instance : Membership α (AIG α) where mem := Mem diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index bebb0d5c6385..bb8d49c79ab0 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -1118,10 +1118,8 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) intro li_eq_lj let li := derivedLits_arr[i] have li_in_derivedLits : li ∈ derivedLits := by - have derivedLits_rw : derivedLits = (Array.mk derivedLits).data := by simp only - simp only [derivedLits_arr_def, li] - conv => rhs; rw [derivedLits_rw] - apply Array.getElem_mem_data + rw [Array.mem_data, ← derivedLits_arr_def] + simp only [li, Array.getElem?_mem] have i_in_bounds : i.1 < derivedLits.length := by have i_property := i.2 simp only [derivedLits_arr_def, Array.size_mk] at i_property diff --git a/tests/lean/run/1986.lean b/tests/lean/run/1986.lean index 04e5f6520c44..821b3d75ac5a 100644 --- a/tests/lean/run/1986.lean +++ b/tests/lean/run/1986.lean @@ -27,7 +27,7 @@ p namespace Set -protected def Mem (a : α) (s : Set α) : Prop := +protected def Mem (s : Set α) (a : α) : Prop := s a instance : Membership α (Set α) := diff --git a/tests/lean/run/3807.lean b/tests/lean/run/3807.lean index d064fba38cec..d0ef82b39351 100644 --- a/tests/lean/run/3807.lean +++ b/tests/lean/run/3807.lean @@ -138,7 +138,7 @@ def setOf {α : Type u} (p : α → Prop) : Set α := p namespace Set -protected def Mem (a : α) (s : Set α) : Prop := s a +protected def Mem (s : Set α) (a : α) : Prop := s a instance : Membership α (Set α) := ⟨Set.Mem⟩ @@ -747,7 +747,7 @@ variable {A : Type _} {B : Type _} [i : SetLike A B] instance : CoeTC A (Set B) where coe := SetLike.coe instance (priority := 100) instMembership : Membership B A := - ⟨fun x p => x ∈ (p : Set B)⟩ + ⟨fun p x => x ∈ (p : Set B)⟩ instance (priority := 100) : CoeSort A (Type _) := ⟨fun p => { x : B // x ∈ p }⟩ @@ -2050,6 +2050,8 @@ instance id : Algebra R R where map_zero' := sorry map_add' := sorry +instance (S : Subsemiring R) : SMul S A := Submonoid.smul .. + instance ofSubsemiring (S : Subsemiring R) : Algebra S A where toRingHom := (algebraMap R A).comp S.subtype smul := (· • ·) @@ -2274,6 +2276,8 @@ def inclusion {S T : Subalgebra R A} (h : S ≤ T) : S →ₐ[R] T where map_zero' := sorry commutes' _ := sorry +instance Subalgebra.instSMul [Semiring S] [Algebra R S] [SMul S T] (S' : Subalgebra R S) : SMul S' T := S'.smul + instance isScalarTower_mid {R S T : Type _} [Semiring R] [Semiring S] [AddMonoid T] [Algebra R S] [MulAction R T] [MulAction S T] [IsScalarTower R S T] (S' : Subalgebra R S) : IsScalarTower R S' T := sorry @@ -2420,14 +2424,18 @@ def toSubfield : Subfield L := instance : SubfieldClass (IntermediateField K L) L where +instance toAlgebra : Algebra S L := + inferInstanceAs (Algebra S.toSubsemiring L) + +instance algebra' {R' K L : Type _} [Field K] [Field L] [Algebra K L] (S : IntermediateField K L) + [Semiring R'] [SMul R' K] [Algebra R' L] [IsScalarTower R' K L] : Algebra R' S := + inferInstanceAs (Algebra R' S.toSubalgebra) + +instance {E} [Field E] [Algebra L E] : Algebra S E := Algebra.ofSubsemiring S.toSubsemiring + instance isScalarTower {R} [Semiring R] [SMul R K] [SMul R L] [SMul R S] [IsScalarTower R K L] : IsScalarTower R K S := sorry -variable {E} [Field E] [Algebra L E] (T : IntermediateField S E) {S} -instance : Algebra S T := T.algebra -instance : SMul S T := Algebra.toSMul -instance [Algebra K E] [IsScalarTower K L E] : IsScalarTower K S T := T.isScalarTower - end IntermediateField namespace AlgHom @@ -2483,6 +2491,8 @@ def adjoin : IntermediateField F E := variable [Field F] [Algebra F E] in theorem subset_adjoin : S ⊆ adjoin F S := sorry +instance (F : Subfield E) : Algebra F E := inferInstanceAs (Algebra F.toSubsemiring E) + theorem subset_adjoin_of_subset_left {F : Subfield E} {T : Set E} (HT : T ⊆ F) : T ⊆ adjoin F S := sorry @@ -2503,6 +2513,11 @@ namespace IntermediateField variable {F E K : Type _} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} +instance (L : IntermediateField F E) : IsScalarTower F L E := sorry + +instance (L : IntermediateField F E) : Algebra F (adjoin L S) := + (IntermediateField.adjoin { x // x ∈ L } S).algebra' + private theorem exists_algHom_adjoin_of_splits'' {L : IntermediateField F E} (f : L →ₐ[F] K) : ∃ φ : adjoin L S →ₐ[F] K, φ.comp (IsScalarTower.toAlgHom F L _) = f := by @@ -2512,7 +2527,7 @@ variable {L : Type _} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E (f : L →ₐ[F] K) -- This only required 16,000 heartbeats prior to #3807, and now takes ~210,000. -set_option maxHeartbeats 30000 +set_option maxHeartbeats 20000 theorem exists_algHom_adjoin_of_splits''' : ∃ φ : adjoin L S →ₐ[F] K, φ.comp (IsScalarTower.toAlgHom F L _) = f := by let L' := (IsScalarTower.toAlgHom F L E).fieldRange diff --git a/tests/lean/run/3965_3.lean b/tests/lean/run/3965_3.lean index e1b46e10c54c..67fc62921913 100644 --- a/tests/lean/run/3965_3.lean +++ b/tests/lean/run/3965_3.lean @@ -20,7 +20,7 @@ def Set (α : Type u) := α → Prop namespace Set -protected def Mem (a : α) (s : Set α) : Prop := +protected def Mem (s : Set α) (a : α) : Prop := s a instance : Membership α (Set α) := diff --git a/tests/lean/run/binop_binrel_perf_issue.lean b/tests/lean/run/binop_binrel_perf_issue.lean index d426fec52e7c..baacef00b0d8 100644 --- a/tests/lean/run/binop_binrel_perf_issue.lean +++ b/tests/lean/run/binop_binrel_perf_issue.lean @@ -14,7 +14,7 @@ def setOf {α : Type u} (p : α → Prop) : Set α := p namespace Set -protected def Mem (a : α) (s : Set α) : Prop := s a +protected def Mem (s : Set α) (a : α) : Prop := s a instance : Membership α (Set α) := ⟨Set.Mem⟩ @@ -155,7 +155,7 @@ variable {A : Type _} {B : Type _} [i : SetLike A B] instance : CoeTC A (Set B) where coe := SetLike.coe instance (priority := 100) instMembership : Membership B A := - ⟨fun x p => x ∈ (p : Set B)⟩ + ⟨fun p x => x ∈ (p : Set B)⟩ instance (priority := 100) : CoeSort A (Type _) := ⟨fun p => { x : B // x ∈ p }⟩ @@ -747,6 +747,8 @@ namespace QuotientAddGroup variable [AddGroup α] (s : AddSubgroup α) +instance : VAdd s.op α := Submonoid.vadd s.op.toAddSubmonoid + def leftRel : Setoid α := VAdd.orbitRel s.op α diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean index d3585e37505f..80347f79c22e 100644 --- a/tests/lean/run/elabAsElim.lean +++ b/tests/lean/run/elabAsElim.lean @@ -153,7 +153,7 @@ def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := def Set (α : Type u) := α → Prop def Set.univ {α : Type _} : Set α := fun _ => True -instance : Membership α (Set α) := ⟨fun x s => s x⟩ +instance : Membership α (Set α) := ⟨fun s x => s x⟩ def Set.pi {α : ι → Type _} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i) := fun f => ∀ i ∈ s, f i ∈ t i example {α : Type u} [IsEmpty α] {β : α → Type v} (x : (a : α) → β a) (s : (i : α) → Set (β i)) : diff --git a/tests/lean/run/setStructInstNotation.lean b/tests/lean/run/setStructInstNotation.lean index 8f58e358a277..3b3a149de659 100644 --- a/tests/lean/run/setStructInstNotation.lean +++ b/tests/lean/run/setStructInstNotation.lean @@ -12,7 +12,7 @@ def setOf {α : Type u} (p : α → Prop) : Set α := namespace Set -protected def mem (a : α) (s : Set α) := +protected def mem (s : Set α) (a : α) := s a instance : Membership α (Set α) := diff --git a/tests/lean/run/subset.lean b/tests/lean/run/subset.lean index adaa063de208..69736abe1b3c 100644 --- a/tests/lean/run/subset.lean +++ b/tests/lean/run/subset.lean @@ -5,7 +5,7 @@ p namespace Set -protected def mem (a : α) (s : Set α) := +protected def mem (s : Set α) (a : α) := s a instance : Membership α (Set α) :=