From 2cf478cbbe1c0041cdac876d5889dbedfbd1077a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 14 Jun 2024 05:08:45 +0100 Subject: [PATCH] =?UTF-8?q?chore:=20prefer=20`=C2=B7=20=3D=3D=20a`=20over?= =?UTF-8?q?=20`a=20=3D=3D=20=C2=B7`=20(#3056)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We recently discovered inconsistencies in Mathlib and Std over the ordering of the arguments for `==`. The most common usage puts the "more variable" term on the LHS, and the "more constant" term on the RHS, however there are plenty of exceptions, and they cause unnecessary pain when switching (particularly, sometimes requiring otherwise unneeded `LawfulBEq` hypotheses). This convention is consistent with the (obvious) preference for `x == 0` over `0 == x` when one term is a literal. We recently updated Std to use this convention https://github.com/leanprover/std4/pull/430 This PR changes the two major places in Lean that use the opposite convention, and adds a suggestion to the docstring for `BEq` about the preferred convention. --- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/List/Basic.lean | 2 +- src/Init/Data/List/Lemmas.lean | 9 ++++----- src/Init/Prelude.lean | 3 +++ tests/lean/run/wfOverapplicationIssue.lean | 2 +- 5 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 8a6e6f40eb..f828392293 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -481,7 +481,7 @@ def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool Id.run <| as.allM p start stop def contains [BEq α] (as : Array α) (a : α) : Bool := - as.any fun b => a == b + as.any (· == a) def elem [BEq α] (a : α) (as : Array α) : Bool := as.contains a diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 2393175685..2c10d67406 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -369,7 +369,7 @@ def replace [BEq α] : List α → α → α → List α -/ def elem [BEq α] (a : α) : List α → Bool | [] => false - | b::bs => match a == b with + | b::bs => match b == a with | true => true | false => elem a bs diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 94bc391e93..c6e6a4b373 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -501,8 +501,7 @@ theorem replace_cons [BEq α] {a : α} : @[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl theorem elem_cons [BEq α] {a : α} : - (a::as).elem b = match b == a with | true => true | false => as.elem b := - rfl + (a::as).elem b = match a == b with | true => true | false => as.elem b := rfl @[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp [elem_cons] @@ -1338,12 +1337,12 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s @[simp] theorem contains_nil [BEq α] : ([] : List α).contains a = false := rfl @[simp] theorem contains_cons [BEq α] : - (a :: as : List α).contains x = (x == a || as.contains x) := by + (a :: as : List α).contains x = (a == x || as.contains x) := by simp only [contains, elem] split <;> simp_all -theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by - induction l with simp | cons b l => cases a == b <;> simp [*] +theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (· == a) := by + induction l with simp | cons b l => cases b == a <;> simp [*] theorem not_all_eq_any_not (l : List α) (p : α → Bool) : (!l.all p) = l.any fun a => !p a := by induction l with simp | cons _ _ ih => rw [ih] diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index b68b2f6c91..fd2d08aa2e 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -914,6 +914,9 @@ is `Bool` valued instead of `Prop` valued, and it also does not have any axioms like being reflexive or agreeing with `=`. It is mainly intended for programming applications. See `LawfulBEq` for a version that requires that `==` and `=` coincide. + +Typically we prefer to put the "more variable" term on the left, +and the "more constant" term on the right. -/ class BEq (α : Type u) where /-- Boolean equality, notated as `a == b`. -/ diff --git a/tests/lean/run/wfOverapplicationIssue.lean b/tests/lean/run/wfOverapplicationIssue.lean index 55dda3ae00..cacefc89be 100644 --- a/tests/lean/run/wfOverapplicationIssue.lean +++ b/tests/lean/run/wfOverapplicationIssue.lean @@ -1,6 +1,6 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : as.contains a) : sizeOf a < sizeOf as := by simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h - let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by + let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (b = a)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by unfold anyM.loop intro h split at h