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 α) :=