chore: prefer · == a over a == · (#3056)

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

@@ -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

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
 

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]

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`. -/

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