feat: EquivBEq and LawfulHashable classes (#4607)

Split from #4583

There are two open questions, opinions appreciated:

- Should this material be part of `Init` or `Std`?
- Should the typeclasses be in the `Std` namespace?

src/Init/Data/BEq.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Markus Himmel
+-/
+prelude
+import Init.Data.Bool
+
+set_option linter.missingDocs true
+
+/-- `PartialEquivBEq α` says that the `BEq` implementation is a
+partial equivalence relation, that is:
+* it is symmetric: `a == b → b == a`
+* it is transitive: `a == b → b == c → a == c`.
+-/
+class PartialEquivBEq (α) [BEq α] : Prop where
+  /-- Symmetry for `BEq`. If `a == b` then `b == a`. -/
+  symm : (a : α) == b → b == a
+  /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
+  trans : (a : α) == b → b == c → a == c
+
+/-- `ReflBEq α` says that the `BEq` implementation is reflexive. -/
+class ReflBEq (α) [BEq α] : Prop where
+  /-- Reflexivity for `BEq`. -/
+  refl : (a : α) == a
+
+/-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
+class EquivBEq (α) [BEq α] extends PartialEquivBEq α, ReflBEq α : Prop
+
+@[simp]
+theorem BEq.refl [BEq α] [ReflBEq α] {a : α} : a == a :=
+  ReflBEq.refl
+
+theorem beq_of_eq [BEq α] [ReflBEq α] {a b : α} : a = b → a == b
+  | rfl => BEq.refl
+
+theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
+  PartialEquivBEq.symm
+
+theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
+  Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
+
+theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false :=
+  BEq.comm (α := α) ▸ id
+
+theorem BEq.trans [BEq α] [PartialEquivBEq α] {a b c : α} : a == b → b == c → a == c :=
+  PartialEquivBEq.trans
+
+theorem BEq.neq_of_neq_of_beq [BEq α] [PartialEquivBEq α] {a b c : α} :
+    (a == b) = false → b == c → (a == c) = false :=
+  fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₁ (BEq.trans h₃ (BEq.symm h₂))
+
+theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
+    a == b → (b == c) = false → (a == c) = false :=
+  fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₂ (BEq.trans (BEq.symm h₁) h₃)
+
+instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
+  refl := LawfulBEq.rfl
+  symm h := (beq_iff_eq _ _).2 <| Eq.symm <| (beq_iff_eq _ _).1 h
+  trans hab hbc := (beq_iff_eq _ _).2 <| ((beq_iff_eq _ _).1 hab).trans <| (beq_iff_eq _ _).1 hbc

src/Init/Data/Hashable.lean

@@ -62,3 +62,16 @@ instance (P : Prop) : Hashable P where
 /-- An opaque (low-level) hash operation used to implement hashing for pointers. -/
 @[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
   mixHash u 11
+
+/-- `LawfulHashable α` says that the `BEq α` and `Hashable α` instances on `α` are compatible, i.e.,
+that `a == b` implies `hash a = hash b`. This is automatic if the `BEq` instance is lawful.
+-/
+class LawfulHashable (α : Type u) [BEq α] [Hashable α] where
+  /-- If `a == b`, then `hash a = hash b`. -/
+  hash_eq (a b : α) : a == b → hash a = hash b
+
+theorem hash_eq [BEq α] [Hashable α] [LawfulHashable α] {a b : α} : a == b → hash a = hash b :=
+  LawfulHashable.hash_eq a b
+
+instance (priority := low) [BEq α] [Hashable α] [LawfulBEq α] : LawfulHashable α where
+  hash_eq _ _ h := eq_of_beq h ▸ rfl