wip

Without this change, we would not inline anything inside
let x_42 := casesOn x_3 fun .. => ... here ...

doc/BoolExpr.lean

@@ -6,7 +6,7 @@ inductive BoolExpr where
   | val (b : Bool)
   | or  (p q : BoolExpr)
   | not (p : BoolExpr)
-  deriving Repr, BEq, DecidableEq
+  deriving Repr, DecidableEq
 
 def BoolExpr.isValue : BoolExpr → Bool
   | val _ => true

src/Init/Classical.lean

@@ -74,8 +74,9 @@ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decid
 noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
   default := inferInstance
 
-noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
-  fun _ _ => inferInstance
+noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α where
+  beq a b := decide (a = b)
+  beq_iff_eq := ⟨of_decide_eq_true, decide_eq_true⟩
 
 noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
   match (propDecidable (Nonempty α)) with

src/Init/Coe.lean

@@ -290,7 +290,7 @@ syntax:1024 (name := coeNotation) "↑" term:1024 : term
 /-! # Basic instances -/
 
 instance boolToProp : Coe Bool Prop where
-  coe b := Eq b true
+  coe := Bool.asProp
 
 instance boolToSort : CoeSort Bool Prop where
   coe b := b

src/Init/Core.lean

@@ -78,19 +78,6 @@ instance thunkCoe : CoeTail α (Thunk α) where
 abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
   Eq.ndrec m h
 
-/--
-If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
-By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
-is equivalent to the corresponding expression with `b` instead.
--/
-structure Iff (a b : Prop) : Prop where
-  /-- If `a → b` and `b → a` then `a` and `b` are equivalent. -/
-  intro ::
-  /-- Modus ponens for if and only if. If `a ↔ b` and `a`, then `b`. -/
-  mp : a → b
-  /-- Modus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`. -/
-  mpr : b → a
-
 @[inherit_doc] infix:20 " <-> " => Iff
 @[inherit_doc] infix:20 " ↔ "   => Iff
 
@@ -484,30 +471,12 @@ Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead
 
 @[inherit_doc] infix:50 " != " => bne
 
-/--
-`LawfulBEq α` is a typeclass which asserts that the `BEq α` implementation
-(which supplies the `a == b` notation) coincides with logical equality `a = b`.
-In other words, `a == b` implies `a = b`, and `a == a` is true.
--/
-class LawfulBEq (α : Type u) [BEq α] : Prop where
-  /-- If `a == b` evaluates to `true`, then `a` and `b` are equal in the logic. -/
-  eq_of_beq : {a b : α} → a == b → a = b
-  /-- `==` is reflexive, that is, `(a == a) = true`. -/
-  protected rfl : {a : α} → a == a
+/-- If `a == b` evaluates to `true`, then `a` and `b` are equal in the logic. -/
+theorem eq_of_beq [DecidableEq α] {a b : α} : a == b → a = b :=
+  beq_iff_eq.1
 
-export LawfulBEq (eq_of_beq)
-
-instance : LawfulBEq Bool where
-  eq_of_beq {a b} h := by cases a <;> cases b <;> first | rfl | contradiction
-  rfl {a} := by cases a <;> decide
-
-instance [DecidableEq α] : LawfulBEq α where
-  eq_of_beq := of_decide_eq_true
-  rfl := of_decide_eq_self_eq_true _
-
-instance : LawfulBEq Char := inferInstance
-
-instance : LawfulBEq String := inferInstance
+@[simp] theorem beq_self [DecidableEq α] {a : α} : (a == a) = true :=
+  beq_iff_eq.2 rfl
 
 /-! # Logical connectives and equality -/
 
@@ -598,13 +567,15 @@ theorem Bool.of_not_eq_false : {b : Bool} → ¬ (b = false) → b = true
   | true,  _ => rfl
   | false, h => absurd rfl h
 
-theorem ne_of_beq_false [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = false) : a ≠ b := by
-  intro h'; subst h'; have : true = false := Eq.trans LawfulBEq.rfl.symm h; contradiction
+theorem Bool.of_not_asProp : ¬ b.asProp → b = false := of_not_eq_true
 
-theorem beq_false_of_ne [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a == b) = false :=
-  have : ¬ (a == b) = true := by
-    intro h'; rw [eq_of_beq h'] at h; contradiction
-  Bool.of_not_eq_true this
+theorem Bool.of_asProp : b.asProp → b = true := id
+
+theorem ne_of_beq_false [DecidableEq α] {a b : α} (h : (a == b) = false) : a ≠ b :=
+  fun h' => nomatch (beq_iff_eq.2 h' ▸ h :)
+
+theorem beq_false_of_ne [DecidableEq α] {a b : α} (h : a ≠ b) : (a == b) = false :=
+  eq_false_of_ne_true (h ∘ beq_iff_eq.1)
 
 section
 variable {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
@@ -657,23 +628,6 @@ variable {a b c d : Prop}
 theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
   Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)
 
-theorem Iff.refl (a : Prop) : a ↔ a :=
-  Iff.intro (fun h => h) (fun h => h)
-
-protected theorem Iff.rfl {a : Prop} : a ↔ a :=
-  Iff.refl a
-
-theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
-  Iff.intro
-    (fun ha => Iff.mp h₂ (Iff.mp h₁ ha))
-    (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc))
-
-theorem Iff.symm (h : a ↔ b) : b ↔ a :=
-  Iff.intro (Iff.mpr h) (Iff.mp h)
-
-theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
-  Iff.intro Iff.symm Iff.symm
-
 theorem Iff.of_eq (h : a = b) : a ↔ b :=
   h ▸ Iff.refl _
 
@@ -689,6 +643,12 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
 
 /-! # Decidable -/
 
+theorem decide_congr [Decidable p] [Decidable q] (h : p ↔ q) : decide p = decide q :=
+  if hp : p then
+    (decide_eq_true hp).trans (decide_eq_true (h.1 hp)).symm
+  else
+    (decide_eq_false hp).trans (decide_eq_false (hp ∘ h.2)).symm
+
 theorem decide_true_eq_true (h : Decidable True) : @decide True h = true :=
   match h with
   | isTrue _  => rfl
@@ -825,17 +785,18 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT :
 
 /-- Auxiliary definition for generating compact `noConfusion` for enumeration types -/
 abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w :=
-  (inst (f x) (f y)).casesOn
-    (fun _ => P)
-    (fun _ => P → P)
+  -- written explicitly so that it reduces reducibly
+  (inst.beq (f x) (f y)).casesOn P (P → P)
 
 /-- Auxiliary definition for generating compact `noConfusion` for enumeration types -/
 abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w} {x y : α} (h : x = y) : noConfusionTypeEnum f P x y :=
-  Decidable.casesOn
-    (motive := fun (inst : Decidable (f x = f y)) => Decidable.casesOn (motive := fun _ => Sort w) inst (fun _ => P) (fun _ => P → P))
-    (inst (f x) (f y))
-    (fun h' => False.elim (h' (congrArg f h)))
-    (fun _ => fun x => x)
+  -- written explicitly so that it reduces reducibly
+  Bool.casesOn
+    (motive := fun b => (b ↔ f x = f y) → b.casesOn P (P → P))
+    (inst.beq (f x) (f y))
+    (nomatch ·.2 (h ▸ rfl))
+    (fun _ x => x)
+    beq_iff_eq
 
 /-! # Inhabited -/
 
@@ -960,10 +921,11 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
 instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} where
   default := ⟨a, h⟩
 
-instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
-  fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
-    if h : a = b then isTrue (by subst h; exact rfl)
-    else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
+instance [BEq α] : BEq {x // p x} where
+  beq a b := a.val == b.val
+
+instance [DecidableEq α] : DecidableEq {x : α // p x} :=
+  .ofInj (·.val) Subtype.eq
 
 end Subtype
 
@@ -978,16 +940,17 @@ instance Sum.inhabitedLeft [Inhabited α] : Inhabited (Sum α β) where
 instance Sum.inhabitedRight [Inhabited β] : Inhabited (Sum α β) where
   default := Sum.inr default
 
-instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
-  match a, b with
-  | Sum.inl a, Sum.inl b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr a, Sum.inr b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
-  | Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h
+/-- Boolean equality for sum types. -/
+protected def Sum.beq [BEq α] [BEq β] : Sum α β → Sum α β → Bool
+  | inl a, inl b | inr a, inr b => a == b
+  | _, _ => false
+
+instance [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) where
+  beq := Sum.beq
+  beq_iff_eq := @fun
+    | .inl _, .inl _ => (beq_iff_eq (α := α)).trans ⟨(· ▸ rfl), (Sum.noConfusion · id)⟩
+    | .inr _, .inr _ => (beq_iff_eq (α := β)).trans ⟨(· ▸ rfl), (Sum.noConfusion · id)⟩
+    | .inr _, .inl _ | .inl _, .inr _ => ⟨(nomatch ·), (nomatch ·)⟩
 
 end
 
@@ -1002,18 +965,17 @@ instance [Inhabited α] [Inhabited β] : Inhabited (MProd α β) where
 instance [Inhabited α] [Inhabited β] : Inhabited (PProd α β) where
   default := ⟨default, default⟩
 
-instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
-  fun (a, b) (a', b') =>
-    match decEq a a' with
-    | isTrue e₁ =>
-      match decEq b b' with
-      | isTrue e₂  => isTrue (e₁ ▸ e₂ ▸ rfl)
-      | isFalse n₂ => isFalse fun h => Prod.noConfusion h fun _   e₂' => absurd e₂' n₂
-    | isFalse n₁ => isFalse fun h => Prod.noConfusion h fun e₁' _   => absurd e₁' n₁
-
 instance [BEq α] [BEq β] : BEq (α × β) where
   beq := fun (a₁, b₁) (a₂, b₂) => a₁ == a₂ && b₁ == b₂
 
+instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) where
+  beq_iff_eq := @fun (a, b) (a', b') =>
+    show (and _ _).asProp ↔ _ from
+    match ha : a == a', hb : b == b' with
+    | true, true => ⟨fun _ => beq_iff_eq.1 ha ▸ beq_iff_eq.1 hb ▸ rfl, fun _ => rfl⟩
+    | false, _ => ⟨(nomatch ·), (Prod.noConfusion · fun h _ => nomatch ha.symm.trans (beq_iff_eq.2 h))⟩
+    | true, false => ⟨(nomatch ·), (Prod.noConfusion · fun _ h => nomatch hb.symm.trans (beq_iff_eq.2 h))⟩
+
 /-- Lexicographical order for products -/
 def Prod.lexLt [LT α] [LT β] (s : α × β) (t : α × β) : Prop :=
   s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
@@ -1062,8 +1024,9 @@ instance : Subsingleton PUnit :=
 instance : Inhabited PUnit where
   default := ⟨⟩
 
-instance : DecidableEq PUnit :=
-  fun a b => isTrue (PUnit.subsingleton a b)
+instance : DecidableEq PUnit where
+  beq _ _ := true
+  beq_iff_eq := ⟨fun _ => rfl, fun _ => rfl⟩
 
 /-! # Setoid -/
 
@@ -1093,6 +1056,9 @@ theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
 theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
   iseqv.trans hab hbc
 
+protected theorem congr {a b c d : α} (hab : a ≈ b) (hcd : c ≈ d) : a ≈ c ↔ b ≈ d :=
+  ⟨fun h => trans (symm hab) (trans h hcd), fun h => trans hab (trans h (symm hcd))⟩
+
 end Setoid
 
 
@@ -1159,8 +1125,7 @@ gen_injective_theorems% EStateM.Result
 gen_injective_theorems% Lean.Name
 gen_injective_theorems% Lean.Syntax
 
-@[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b :=
-  ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
+attribute [simp] beq_iff_eq
 
 /-! # Quotients -/
 
@@ -1521,13 +1486,9 @@ section
 variable {α : Type u}
 variable (r : α → α → Prop)
 
-instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) :=
-  fun (q₁ q₂ : Quotient s) =>
-    Quotient.recOnSubsingleton₂ q₁ q₂
-      fun a₁ a₂ =>
-        match d a₁ a₂ with
-        | isTrue h₁  => isTrue (Quotient.sound h₁)
-        | isFalse h₂ => isFalse fun h => absurd (Quotient.exact h) h₂
+instance {α : Sort u} {s : Setoid α} [∀ (a b : α), Decidable (a ≈ b)] : DecidableEq (Quotient s) where
+  beq := Quotient.lift₂ (decide <| · ≈ ·) fun _ _ _ _ h₁ h₂ => decide_congr (Setoid.congr h₁ h₂)
+  beq_iff_eq := @(Quotient.ind₂ fun _ _ => decide_iff.trans ⟨Quotient.sound, Quotient.exact⟩)
 
 /-! # Function extensionality -/
 

src/Init/Data/Array/DecidableEq.lean

@@ -31,20 +31,19 @@ theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y
    have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h
    exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _
 
-theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i = true := by
+theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i := by
   unfold Array.isEqvAux
   split
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
 termination_by _ => a.size - i
 
-theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
+theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) := by
   simp [isEqv, isEqvAux_self]
 
-instance [DecidableEq α] : DecidableEq (Array α) :=
-  fun a b =>
-    match h:isEqv a b (fun a b => a = b) with
-    | true  => isTrue (eq_of_isEqv a b h)
-    | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
+instance [DecidableEq α] : DecidableEq (Array α) where
+  beq_iff_eq {a b} :=
+    have : isEqv a b (fun x y => x = y) ↔ a = b := ⟨eq_of_isEqv a b, (· ▸ isEqv_self a)⟩
+    show isEqv a b (fun x y => x == y) ↔ _ by simp only [decide_eq] at this; exact this
 
 end Array

src/Init/Data/Array/Mem.lean

@@ -31,7 +31,7 @@ theorem sizeOf_get_lt [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as
 
 theorem sizeOf_lt_of_mem [DecidableEq α] [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
-  let rec aux (j : Nat) (h : 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) (h : anyM.loop (m := Id) (fun b => a == b) as as.size (Nat.le_refl ..) j = true) : sizeOf a < sizeOf as := by
     unfold anyM.loop at h
     split at h
     · simp [Bind.bind, pure] at h; split at h

src/Init/Data/Int/Basic.lean

@@ -99,18 +99,18 @@ instance : LT Int where
 
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_int_dec_eq"]
-protected def decEq (a b : @& Int) : Decidable (a = b) :=
+protected def beq (a b : @& Int) : Bool :=
   match a, b with
-  | ofNat a, ofNat b => match decEq a b with
-    | isTrue h  => isTrue  <| h ▸ rfl
-    | isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
-  | negSucc a, negSucc b => match decEq a b with
-    | isTrue h  => isTrue  <| h ▸ rfl
-    | isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
-  | ofNat _, negSucc _ => isFalse <| fun h => Int.noConfusion h
-  | negSucc _, ofNat _ => isFalse <| fun h => Int.noConfusion h
+  | ofNat a, ofNat b | negSucc a, negSucc b => a == b
+  | _, _ => false
 
-instance : DecidableEq Int := Int.decEq
+instance : BEq Int where
+  beq := Int.beq
+
+instance : DecidableEq Int where
+  beq_iff_eq {a b} := by
+    show Int.beq _ _ ↔ _
+    cases a <;> cases b <;> simp [Int.beq]
 
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_int_dec_nonneg"]
@@ -165,10 +165,6 @@ protected def pow (m : Int) : Nat → Int
 instance : HPow Int Nat Int where
   hPow := Int.pow
 
-instance : LawfulBEq Int where
-  eq_of_beq h := by simp [BEq.beq] at h; assumption
-  rfl := by simp [BEq.beq]
-
 instance : Min Int := minOfLe
 
 instance : Max Int := maxOfLe

src/Init/Data/List/Basic.lean

@@ -331,9 +331,7 @@ def replace [BEq α] : List α → α → α → List α
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false
-  | b::bs => match a == b with
-    | true  => true
-    | false => elem a bs
+  | b::bs => a == b || elem a bs
 
 /-- `notElem a l` is `!(elem a l)`. -/
 def notElem [BEq α] (a : α) (as : List α) : Bool :=
@@ -356,22 +354,21 @@ inductive Mem (a : α) : List α → Prop
 instance : Membership α (List α) where
   mem := Mem
 
-theorem mem_of_elem_eq_true [DecidableEq α] {a : α} {as : List α} : elem a as = true → a ∈ as := by
-  match as with
-  | [] => simp [elem]
-  | a'::as =>
-    simp [elem]
-    split
-    next h => intros; simp [BEq.beq] at h; subst h; apply Mem.head
-    next _ => intro h; exact Mem.tail _ (mem_of_elem_eq_true h)
+theorem elem_iff_mem [DecidableEq α] {a : α} {as : List α} : elem a as ↔ a ∈ as := by
+  show _ ↔ Mem a as
+  have not_mem_nil : ∀ {a : α}, ¬ Mem a nil := by intro _ h; cases h
+  have mem_cons_iff : ∀ {a b : α} {bs}, Mem a (b::bs) ↔ (a = b ∨ Mem a bs) := by
+    intros; constructor <;> intro h <;> cases h <;> simp [*, Mem.head, Mem.tail]
+  induction as <;> simp [elem, *]
 
-theorem elem_eq_true_of_mem [DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : elem a as = true := by
-  induction h with
-  | head _ => simp [elem]
-  | tail _ _ ih => simp [elem]; split; rfl; assumption
+theorem mem_of_elem [DecidableEq α] {a : α} {as : List α} : elem a as → a ∈ as :=
+  elem_iff_mem.1
+
+theorem elem_of_mem [DecidableEq α] {a : α} {as : List α} (h : a ∈ as) : elem a as :=
+  elem_iff_mem.2 h
 
 instance [DecidableEq α] (a : α) (as : List α) : Decidable (a ∈ as) :=
-  decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
+  decidable_of_decidable_of_iff elem_iff_mem
 
 theorem mem_append_of_mem_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
   intro h
@@ -718,17 +715,6 @@ and they are pairwise related by `eqv`.
   | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv
   | _,     _,     _   => false
 
-/--
-The equality relation on lists asserts that they have the same length
-and they are pairwise `BEq`.
--/
-protected def beq [BEq α] : List α → List α → Bool
-  | [],    []    => true
-  | a::as, b::bs => a == b && List.beq as bs
-  | _,     _     => false
-
-instance [BEq α] : BEq (List α) := ⟨List.beq⟩
-
 /--
 `replicate n a` is `n` copies of `a`:
 * `replicate 5 a = [a, a, a, a, a]`
@@ -822,22 +808,6 @@ def minimum? [Min α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl min a
 
-instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
-  eq_of_beq {as bs} := by
-    induction as generalizing bs with
-    | nil => intro h; cases bs <;> first | rfl | contradiction
-    | cons a as ih =>
-      cases bs with
-      | nil => intro h; contradiction
-      | cons b bs =>
-        simp [show (a::as == b::bs) = (a == b && as == bs) from rfl]
-        intro ⟨h₁, h₂⟩
-        exact ⟨h₁, ih h₂⟩
-  rfl {as} := by
-    induction as with
-    | nil => rfl
-    | cons a as ih => simp [BEq.beq, List.beq, LawfulBEq.rfl]; exact ih
-
 theorem of_concat_eq_concat {as bs : List α} {a b : α} (h : as.concat a = bs.concat b) : as = bs ∧ a = b := by
   match as, bs with
   | [], [] => simp [concat] at h; simp [h]

src/Init/Data/Nat/Basic.lean

@@ -89,25 +89,13 @@ attribute [simp] Nat.zero_le
 
 /-! # Helper Bool relation theorems -/
 
-@[simp] theorem beq_refl (a : Nat) : Nat.beq a a = true := by
+@[simp] theorem beq_refl (a : Nat) : (Nat.beq a a).asProp := by
   induction a with simp [Nat.beq]
   | succ a ih => simp [ih]
 
-@[simp] theorem beq_eq : (Nat.beq x y = true) = (x = y) := propext <| Iff.intro Nat.eq_of_beq_eq_true (fun h => h ▸ (Nat.beq_refl x))
-@[simp] theorem ble_eq : (Nat.ble x y = true) = (x ≤ y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
-@[simp] theorem blt_eq : (Nat.blt x y = true) = (x < y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
-
-instance : LawfulBEq Nat where
-  eq_of_beq h := Nat.eq_of_beq_eq_true h
-  rfl := by simp [BEq.beq]
-
-@[simp] theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := propext <| Iff.intro eq_of_beq (fun h => by subst h; apply LawfulBEq.rfl)
-@[simp] theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) :=
-  propext <| Iff.intro
-    (fun h₁ h₂ => by subst h₂; rw [LawfulBEq.rfl] at h₁; contradiction)
-    (fun h =>
-      have : ¬ ((a == b) = true) := fun h' => absurd (eq_of_beq h') h
-      by simp [this])
+@[simp] theorem beq_eq : (Nat.beq x y).asProp = (x = y) := propext (beq_iff_eq (α := Nat))
+@[simp] theorem ble_eq : (Nat.ble x y).asProp = (x ≤ y) := propext <| Iff.intro Nat.le_of_ble Nat.ble_of_le
+@[simp] theorem blt_eq : (Nat.blt x y).asProp = (x < y) := propext <| Iff.intro Nat.le_of_ble Nat.ble_of_le
 
 /-! # Nat.add theorems -/
 

src/Init/Data/Nat/Linear.lean

@@ -170,21 +170,7 @@ structure PolyCnstr  where
   eq  : Bool
   lhs : Poly
   rhs : Poly
-  deriving BEq
-
--- TODO: implement LawfulBEq generator companion for BEq
-instance : LawfulBEq PolyCnstr where
-  eq_of_beq {a b} h := by
-    cases a; rename_i eq₁ lhs₁ rhs₁
-    cases b; rename_i eq₂ lhs₂ rhs₂
-    have h : eq₁ == eq₂ && lhs₁ == lhs₂ && rhs₁ == rhs₂ := h
-    simp at h
-    have ⟨⟨h₁, h₂⟩, h₃⟩ := h
-    rw [h₁, h₂, h₃]
-  rfl {a} := by
-    cases a; rename_i eq lhs rhs
-    show (eq == eq && lhs == lhs && rhs == rhs) = true
-    simp [LawfulBEq.rfl]
+  deriving DecidableEq
 
 def PolyCnstr.mul (k : Nat) (c : PolyCnstr) : PolyCnstr :=
   { c with lhs := c.lhs.mul k, rhs := c.rhs.mul k }
@@ -274,11 +260,12 @@ def PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr :=
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.right_distrib Nat.left_distrib Nat.mul_assoc Nat.mul_comm
 attribute [local simp] Poly.denote Expr.denote Poly.insertSorted Poly.sort Poly.sort.go Poly.fuse Poly.cancelAux
 attribute [local simp] Poly.mul Poly.mul.go
+attribute [local simp] cond_eq_ite
 
 theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (v : Var) (p : Poly) : (p.insertSorted k v).denote ctx = p.denote ctx + k * v.denote ctx := by
   match p with
   | [] => simp
-  | (k', v') :: p => by_cases h : Nat.blt v v' <;> simp [h, denote_insertSorted]
+  | (k', v') :: p => by_cases h : v < v' <;> simp [h, denote_insertSorted]
 
 attribute [local simp] Poly.denote_insertSorted
 
@@ -328,22 +315,22 @@ theorem Poly.denote_fuse (ctx : Context) (p : Poly) : p.fuse.denote ctx = p.deno
     simp
     split
     case _ h => simp [← ih, h]
-    case _ k' v' p' h => by_cases he : v == v' <;> simp [he, ← ih, h]; rw [eq_of_beq he]
+    case _ k' v' p' h => by_cases he : v = v' <;> simp_all [he, ← ih, h]
 
 attribute [local simp] Poly.denote_fuse
 
-theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx := by
-  simp
-  by_cases h : k == 0 <;> simp [h]; simp [eq_of_beq h]
-  by_cases h : k == 1 <;> simp [h]; simp [eq_of_beq h]
-  induction p with
-  | nil  => simp
-  | cons kv m ih => cases kv with | _ k' v => simp [ih]
+theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx :=
+  match k with
+  | 0 | 1 => by simp
+  | k+2 => by
+    induction p with
+    | nil  => simp
+    | cons kv m ih => cases kv with | _ k' v =>
+      simp_all [ih, show k + 1 ≠ 0 from (nomatch ·), show k + 2 ≠ 0 from (nomatch ·)]
+      simp only [Nat.mul_left_comm]
 
-private theorem eq_of_not_blt_eq_true (h₁ : ¬ (Nat.blt x y = true)) (h₂ : ¬ (Nat.blt y x = true)) : x = y :=
-  have h₁ : ¬ x < y := fun h => h₁ (Nat.blt_eq.mpr h)
-  have h₂ : ¬ y < x := fun h => h₂ (Nat.blt_eq.mpr h)
-  Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
+private theorem eq_of_not_lt {x y : Nat} (hxy : ¬ x < y) (hyx : ¬ y < x) : x = y :=
+  Nat.le_antisymm (Nat.ge_of_not_lt hyx) (Nat.ge_of_not_lt hxy)
 
 attribute [local simp] Poly.denote_mul
 
@@ -355,27 +342,27 @@ theorem Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
     simp
     split <;> simp at h <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
+    by_cases hltv : v₁ < v₂ <;> simp [hltv]
     · apply ih; simp [denote_eq] at h |-; assumption
-    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
+    · by_cases hgtv : v₂ < v₁ <;> simp [hgtv]
       · apply ih; simp [denote_eq] at h |-; assumption
-      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
-        by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk]
+      · cases eq_of_not_lt hltv hgtv
+        by_cases hltk : k₁ < k₂ <;> simp [hltk]
         · apply ih
           simp [denote_eq] at h |-
-          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
+          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hltk)
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
           apply Eq.symm
           apply Nat.sub_eq_of_eq_add
           simp [h]
-        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
+        · by_cases hgtk : k₂ < k₁ <;> simp [hgtk]
           · apply ih
             simp [denote_eq] at h |-
-            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
+            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hgtk)
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
             apply Nat.sub_eq_of_eq_add
             simp [h]
-          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · cases eq_of_not_lt hltk hgtk
             apply ih
             simp [denote_eq] at h |-
             rw [← Nat.add_assoc, ← Nat.add_assoc] at h
@@ -389,26 +376,26 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
     simp at h
     split at h <;> simp <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
+    by_cases hltv : v₁ < v₂ <;> simp [hltv] at h
     · have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
-    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
+    · by_cases hgtv : v₂ < v₁ <;> simp [hgtv] at h
       · have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
-      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
-        by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk] at h
+      · cases eq_of_not_lt hltv hgtv
+        by_cases hltk : k₁ < k₂ <;> simp [hltk] at h
         · have ih := ih (h := h); simp [denote_eq] at ih ⊢
-          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
+          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hltk)
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
           have ih := Nat.eq_add_of_sub_eq (Nat.le_trans haux (Nat.le_add_left ..)) ih.symm
           simp at ih
           rw [ih]
-        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
+        · by_cases hgtk : k₂ < k₁ <;> simp [hgtk] at h
           · have ih := ih (h := h); simp [denote_eq] at ih ⊢
-            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
+            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hgtk)
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
             have ih := Nat.eq_add_of_sub_eq (Nat.le_trans haux (Nat.le_add_left ..)) ih
             simp at ih
             rw [ih]
-          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · cases eq_of_not_lt hltk hgtk
             have ih := ih (h := h); simp [denote_eq] at ih ⊢
             rw [← Nat.add_assoc, ih, Nat.add_assoc]
 
@@ -434,26 +421,26 @@ theorem Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
     simp
     split <;> simp at h <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
+    by_cases hltv : v₁ < v₂ <;> simp [hltv]
     · apply ih; simp [denote_le] at h |-; assumption
-    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv]
+    · by_cases hgtv : v₂ < v₁ <;> simp [hgtv]
       · apply ih; simp [denote_le] at h |-; assumption
-      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
-        by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk]
+      · have heqv : v₁ = v₂ := eq_of_not_lt hltv hgtv; subst heqv
+        by_cases hltk : k₁ < k₂ <;> simp [hltk]
         · apply ih
           simp [denote_le] at h |-
-          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
+          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hltk)
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
           apply Nat.le_sub_of_add_le
           simp [h]
-        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk]
+        · by_cases hgtk : k₂ < k₁ <;> simp [hgtk]
           · apply ih
             simp [denote_le] at h |-
-            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
+            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hgtk)
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
             apply Nat.sub_le_of_le_add
             simp [h]
-          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · have heqk : k₁ = k₂ := eq_of_not_lt hltk hgtk; subst heqk
             apply ih
             simp [denote_le] at h |-
             rw [← Nat.add_assoc, ← Nat.add_assoc] at h
@@ -468,26 +455,26 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
     simp at h
     split at h <;> simp <;> try assumption
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
+    by_cases hltv : v₁ < v₂ <;> simp [hltv] at h
     · have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
-    · by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv] at h
+    · by_cases hgtv : v₂ < v₁ <;> simp [hgtv] at h
       · have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
-      · have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv; subst heqv
-        by_cases hltk : Nat.blt k₁ k₂ <;> simp [hltk] at h
+      · have heqv : v₁ = v₂ := eq_of_not_lt hltv hgtv; subst heqv
+        by_cases hltk : k₁ < k₂ <;> simp [hltk] at h
         · have ih := ih (h := h); simp [denote_le] at ih ⊢
-          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))
+          have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hltk)
           rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
           have := Nat.add_le_of_le_sub (Nat.le_trans haux (Nat.le_add_left ..)) ih
           simp at this
           exact this
-        · by_cases hgtk : Nat.blt k₂ k₁ <;> simp [hgtk] at h
+        · by_cases hgtk : k₂ < k₁ <;> simp [hgtk] at h
           · have ih := ih (h := h); simp [denote_le] at ih ⊢
-            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
+            have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt hgtk)
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
             have := Nat.le_add_of_sub_le ih
             simp at this
             exact this
-          · have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
+          · have heqk : k₁ = k₂ := eq_of_not_lt hltk hgtk; subst heqk
             have ih := ih (h := h); simp [denote_le] at ih ⊢
             have := Nat.add_le_add_right ih (k₁ * Var.denote ctx v₁)
             simp at this
@@ -512,10 +499,9 @@ theorem Poly.denote_combineAux (ctx : Context) (fuel : Nat) (p₁ p₂ : Poly) :
   | succ fuel ih =>
     split <;> simp
     rename_i k₁ v₁ p₁ k₂ v₂ p₂
-    by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv, ih]
-    by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv, ih]
-    have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv
-    simp [heqv]
+    by_cases hltv : v₁ < v₂ <;> simp [hltv, ih]
+    by_cases hgtv : v₂ < v₁ <;> simp [hgtv, ih]
+    simp [eq_of_not_lt hgtv hltv]
 
 theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   simp [combine, denote_combineAux]
@@ -524,7 +510,7 @@ attribute [local simp] Poly.denote_combine
 
 theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
   induction e with
-  | num k => by_cases h : k == 0 <;> simp [toPoly, h, Var.denote]; simp [eq_of_beq h]
+  | num k => by_cases h : k = 0 <;> simp [toPoly, h, Var.denote]
   | var i => simp [toPoly]
   | add a b iha ihb => simp [toPoly, iha, ihb]
   | mulL k a ih => simp [toPoly, ih, -Poly.mul]
@@ -559,7 +545,7 @@ theorem ExprCnstr.toPoly_norm_eq (c : ExprCnstr) : c.toPoly.norm = c.toNormPoly
 theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
-  by_cases h : eq = true <;> simp [h]
+  by_cases h : eq <;> simp [h]
   · simp [Poly.denote_eq, Expr.toPoly]
   · simp [Poly.denote_le, Expr.toPoly]
 
@@ -568,7 +554,7 @@ attribute [local simp] ExprCnstr.denote_toPoly
 theorem ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) : c.toNormPoly.denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toNormPoly]
-  by_cases h : eq = true <;> simp [h]
+  by_cases h : eq <;> simp [h]
   · rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq, Expr.toNormPoly, Poly.norm]
   · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_le, Expr.toNormPoly, Poly.norm]
 
@@ -586,13 +572,9 @@ attribute [-simp] Nat.right_distrib Nat.left_distrib
 
 theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul (k+1)).denote ctx = c.denote ctx := by
   cases c; rename_i eq lhs rhs
-  have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp; apply Nat.succ_ne_zero
-  have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
-  have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
-  have : (1 == (0 : Nat)) = false := rfl
-  have : (1 == (1 : Nat)) = true  := rfl
-  by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
-     <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
+  have : k + 1 ≠ 0 := (nomatch ·)
+  by_cases he : eq <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
+     <;> by_cases hk : k = 0 <;> (try simp [hk]) <;> simp [*] <;> apply propext <;> apply Iff.intro <;> intro h
   · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
   · rw [h]
   · exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
@@ -606,7 +588,7 @@ theorem PolyCnstr.denote_combine {ctx : Context} {c₁ c₂ : PolyCnstr} (h₁ :
   cases c₁; cases c₂; rename_i eq₁ lhs₁ rhs₁ eq₂ lhs₂ rhs₂
   simp [denote] at h₁ h₂
   simp [PolyCnstr.combine, denote]
-  by_cases he₁ : eq₁ = true <;> by_cases he₂ : eq₂ = true <;> simp [he₁, he₂] at h₁ h₂ |-
+  by_cases he₁ : eq₁ <;> by_cases he₂ : eq₂ <;> simp [he₁, he₂] at h₁ h₂ |-
   · rw [Poly.denote_eq_cancel_eq]; simp [Poly.denote_eq] at h₁ h₂ |-; simp [h₁, h₂]
   · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₁]; apply Nat.add_le_add_left h₂
   · rw [Poly.denote_le_cancel_eq]; simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-; rw [h₂]; apply Nat.add_le_add_right h₁
@@ -618,28 +600,28 @@ theorem Poly.isNum?_eq_some (ctx : Context) {p : Poly} {k : Nat} : p.isNum? = so
   simp [isNum?]
   split
   next => intro h; injection h
-  next k v => by_cases h : v == fixedVar <;> simp [h]; intros; simp [Var.denote, eq_of_beq h]; assumption
+  next k v => by_cases h : v = fixedVar <;> simp [h]; intros; simp [Var.denote, h]; assumption
   next => intros; contradiction
 
-theorem Poly.of_isZero (ctx : Context) {p : Poly} (h : isZero p = true) : p.denote ctx = 0 := by
+theorem Poly.of_isZero (ctx : Context) {p : Poly} (h : isZero p) : p.denote ctx = 0 := by
   simp [isZero] at h
   split at h
   · simp
   · contradiction
 
-theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p = true) : p.denote ctx > 0 := by
+theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p) : p.denote ctx > 0 := by
   match p with
   | [] => contradiction
   | (k, v) :: p =>
-    by_cases he : v == fixedVar <;> simp [he, isNonZero] at h ⊢
-    · simp [eq_of_beq he, Var.denote]; apply Nat.lt_of_succ_le; exact Nat.le_trans h (Nat.le_add_right ..)
+    by_cases he : v = fixedVar <;> simp [he, isNonZero] at h ⊢
+    · simp [he, Var.denote]; apply Nat.lt_of_succ_le; exact Nat.le_trans h (Nat.le_add_right ..)
     · have ih := of_isNonZero ctx h
       exact Nat.le_trans ih (Nat.le_add_right ..)
 
 theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat → c.denote ctx = False := by
   cases c; rename_i eq lhs rhs
   simp [isUnsat]
-  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
+  by_cases he : eq <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
   · intro
       | Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
       | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
@@ -652,7 +634,7 @@ theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsa
 theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid → c.denote ctx = True := by
   cases c; rename_i eq lhs rhs
   simp [isValid]
-  by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
+  by_cases he : eq <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
   · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₁, h₂]
   · intro h
@@ -694,9 +676,9 @@ theorem Certificate.of_combine_isUnsat (ctx : Context) (cs : Certificate) (h : c
 
 theorem denote_monomialToExpr (ctx : Context) (k : Nat) (v : Var) : (monomialToExpr k v).denote ctx = k * v.denote ctx := by
   simp [monomialToExpr]
-  by_cases h : v == fixedVar <;> simp [h, Expr.denote]
-  · simp [eq_of_beq h, Var.denote]
-  · by_cases h : k == 1 <;> simp [h, Expr.denote]; simp [eq_of_beq h]
+  by_cases h : v = fixedVar <;> simp [h, Expr.denote]
+  · simp [h, Var.denote]
+  · by_cases h : k = 1 <;> simp [h, Expr.denote]
 
 attribute [local simp] denote_monomialToExpr
 

src/Init/Data/Nat/SOM.lean

@@ -113,11 +113,11 @@ where
     induction fuel generalizing m₁ m₂ with
     | zero => simp! [append_denote]
     | succ _ ih =>
-      simp!
+      simp! [cond_eq_ite]
       split <;> simp!
       next v₁ m₁ v₂ m₂ =>
-        by_cases hlt : Nat.blt v₁ v₂ <;> simp! [hlt, Nat.mul_assoc, ih]
-        by_cases hgt : Nat.blt v₂ v₁ <;> simp! [hgt, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, ih]
+        by_cases hlt : v₁ < v₂ <;> simp! [hlt, Nat.mul_assoc, ih]
+        by_cases hgt : v₂ < v₁ <;> simp! [hgt, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, ih]
 
 theorem Poly.append_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁ ++ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   match p₁ with
@@ -135,11 +135,11 @@ where
       split <;> simp!
       next k₁ m₁ p₁ k₂ m₂ p₂ =>
         by_cases hlt : m₁ < m₂ <;> simp! [hlt, Nat.add_assoc, ih]
-        by_cases hgt : m₂ < m₁ <;> simp! [hgt, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, ih]
+        by_cases hgt : m₂ < m₁ <;> simp! [hgt, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, ih, cond_eq_ite]
         have : m₁ = m₂ := List.le_antisymm hgt hlt
         subst m₂
-        by_cases heq : k₁ + k₂ == 0 <;> simp! [heq, ih]
-        · simp [← Nat.add_assoc, ← Nat.right_distrib, eq_of_beq heq]
+        by_cases heq : k₁ + k₂ = 0 <;> simp! [heq, ih, if_pos, if_neg]
+        · simp [← Nat.add_assoc, ← Nat.right_distrib, heq]
         · simp [Nat.right_distrib, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
 
 theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (m : Mon) (p : Poly) : (p.insertSorted k m).denote ctx = p.denote ctx + k * m.denote ctx := by
@@ -171,8 +171,7 @@ where
 theorem Expr.toPoly_denote (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
   induction e with
   | num k =>
-    simp!; by_cases h : k == 0 <;> simp! [*]
-    simp [eq_of_beq h]
+    simp!; by_cases h : k = 0 <;> simp! [*, cond_eq_ite]
   | var v => simp!
   | add a b => simp! [Poly.add_denote, *]
   | mul a b => simp! [Poly.mul_denote, *]

src/Init/Data/Option/Basic.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Core
 import Init.Control.Basic
 import Init.Coe
+import Init.SimpLemmas
 
 namespace Option
 
@@ -83,9 +84,14 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
 
 end Option
 
-deriving instance DecidableEq for Option
 deriving instance BEq for Option
 
+instance [DecidableEq α] : DecidableEq (Option α) where
+  beq_iff_eq := @fun
+    | some a, some b => show (true && a == b) ↔ some a = some b by simp
+    | none, none => ⟨fun _ => rfl, fun _ => rfl⟩
+    | none, some _ | some _, none => ⟨(nomatch ·), (nomatch ·)⟩
+
 instance [LT α] : LT (Option α) where
   lt := Option.lt (· < ·)
 

src/Init/Data/Prod.lean

@@ -4,10 +4,3 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.SimpLemmas
-
-instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
-  eq_of_beq {a b} (h : a.1 == b.1 && a.2 == b.2) := by
-    cases a; cases b
-    refine congr (congrArg _ (eq_of_beq ?_)) (eq_of_beq ?_) <;> simp_all
-  rfl {a} := by cases a; simp [BEq.beq, LawfulBEq.rfl]

src/Init/Data/Range.lean

@@ -62,6 +62,12 @@ instance : ForIn' m Range Nat inferInstance where
 instance : ForM m Range Nat where
   forM := Range.forM
 
+def toArray (range : Range) : Array Nat := Id.run do
+  let mut out := #[]
+  for i in range do
+    out := out.push i
+  return out
+
 syntax:max "[" withoutPosition(":" term) "]" : term
 syntax:max "[" withoutPosition(term ":" term) "]" : term
 syntax:max "[" withoutPosition(":" term ":" term) "]" : term

src/Init/Data/String/Basic.lean

@@ -244,7 +244,12 @@ where go (acc : String) (s : String) : List String → String
 structure Iterator where
   s : String
   i : Pos
-  deriving DecidableEq
+  deriving BEq
+
+instance : DecidableEq Iterator where
+  beq_iff_eq := @fun {..} {..} =>
+    .trans (Bool.and_iff_congr (Bool.and_iff_congr Bool.true_iff beq_iff_eq) beq_iff_eq)
+      (by simp)
 
 def mkIterator (s : String) : Iterator :=
   ⟨s, 0⟩

src/Init/Meta.lean

@@ -208,12 +208,8 @@ protected theorem beq_iff_eq {m n : Name} : m == n ↔ m = n := by
   show m.beq n ↔ _
   induction m generalizing n <;> cases n <;> simp_all [Name.beq, And.comm]
 
-instance : LawfulBEq Name where
-  eq_of_beq := Name.beq_iff_eq.1
-  rfl := Name.beq_iff_eq.2 rfl
-
-instance : DecidableEq Name :=
-  fun a b => if h : a == b then .isTrue (by simp_all) else .isFalse (by simp_all)
+instance : DecidableEq Name where
+  beq_iff_eq := Name.beq_iff_eq
 
 end Name
 

src/Init/Prelude.lean

@@ -506,6 +506,34 @@ structure And (a b : Prop) : Prop where
   `h.right`, also notated as `h.2`, is a proof of `b`. -/
   right : b
 
+/--
+If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
+By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
+is equivalent to the corresponding expression with `b` instead.
+-/
+structure Iff (a b : Prop) : Prop where
+  /-- If `a → b` and `b → a` then `a` and `b` are equivalent. -/
+  intro ::
+  /-- Modus ponens for if and only if. If `a ↔ b` and `a`, then `b`. -/
+  mp : a → b
+  /-- Modus ponens for if and only if, reversed. If `a ↔ b` and `b`, then `a`. -/
+  mpr : b → a
+
+protected theorem Iff.refl (a : Prop) : Iff a a := ⟨(·), (·)⟩
+
+protected theorem Iff.rfl : Iff a a := Iff.refl a
+
+theorem Iff.trans (h₁ : Iff a b) (h₂ : Iff b c) : Iff a c :=
+  Iff.intro
+    (fun ha => Iff.mp h₂ (Iff.mp h₁ ha))
+    (fun hc => Iff.mpr h₁ (Iff.mpr h₂ hc))
+
+theorem Iff.symm (h : Iff a b) : Iff b a :=
+  Iff.intro (Iff.mpr h) (Iff.mp h)
+
+theorem Iff.comm : Iff (Iff a b) (Iff b a) :=
+  Iff.intro Iff.symm Iff.symm
+
 /--
 `Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
 constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
@@ -550,6 +578,10 @@ inductive Bool : Type where
 
 export Bool (false true)
 
+/-- Interprets a Boolean value as a proposition. -/
+def Bool.asProp (b : Bool) : Prop :=
+  Eq b true
+
 /--
 `Subtype p`, usually written as `{x : α // p x}`, is a type which
 represents all the elements `x : α` for which `p x` is true. It is structurally
@@ -810,15 +842,47 @@ abbrev DecidableRel {α : Sort u} (r : α → α → Prop) :=
   (a b : α) → Decidable (r a b)
 
 /--
-Asserts that `α` has decidable equality, that is, `a = b` is decidable
+`BEq α` is a typeclass for supplying a boolean-valued equality relation on
+`α`, notated as `a == b`. Unlike `DecidableEq α` (which uses `a = b`), this
+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 `DecidableEq` for a version that requires that
+`==` and `=` coincide.
+-/
+class BEq (α : Sort u) where
+  /-- Boolean equality, notated as `a == b`. -/
+  beq : α → α → Bool
+
+open BEq (beq)
+
+/--
+Asserts that `α` has decidable equality.
+This is equivalent to `a = b` being decidable
 for all `a b : α`. See `Decidable`.
 -/
-abbrev DecidableEq (α : Sort u) :=
-  (a b : α) → Decidable (Eq a b)
+class DecidableEq (α : Sort u) extends BEq α where
+  /-- `==` and `=` coincide. -/
+  beq_iff_eq {a b : α} : Iff (beq a b).asProp (Eq a b)
+
+theorem beq_iff_eq [DecidableEq α] {a b : α} : Iff (beq a b).asProp (Eq a b) :=
+  DecidableEq.beq_iff_eq
+
+theorem beq_iff_eq' [DecidableEq α] (a b : α) : Iff (beq a b).asProp (Eq a b) := beq_iff_eq ..
+
+/--
+Constructs a decidable equality equality instance on `α` given an injective
+function to another type that already has a decidable equality instance.
+-/
+abbrev DecidableEq.ofInj [DecidableEq β] (f : α → β)
+    (finj : ∀ {a b : α}, Eq (f a) (f b) → Eq a b) : DecidableEq α where
+  beq a b := beq (f a) (f b)
+  beq_iff_eq := (beq_iff_eq (α := β)).trans ⟨finj, (· ▸ rfl)⟩
 
 /-- Proves that `a = b` is decidable given `DecidableEq α`. -/
-def decEq {α : Sort u} [inst : DecidableEq α] (a b : α) : Decidable (Eq a b) :=
-  inst a b
+instance decEq [DecidableEq α] (a b : α) : Decidable (Eq a b) :=
+  match h : beq a b with
+  | true => isTrue (beq_iff_eq.1 h)
+  | false => isFalse fun h' => nomatch h.symm.trans (beq_iff_eq.2 h')
 
 set_option linter.unusedVariables false in
 theorem decide_eq_true : [inst : Decidable p] → p → Eq (decide p) true
@@ -839,39 +903,35 @@ theorem of_decide_eq_false [inst : Decidable p] : Eq (decide p) false → Not p
   | isTrue  h₁ => absurd h (ne_false_of_eq_true (decide_eq_true h₁))
   | isFalse h₁ => h₁
 
-theorem of_decide_eq_self_eq_true [inst : DecidableEq α] (a : α) : Eq (decide (Eq a a)) true :=
-  match (generalizing := false) inst a a with
-  | isTrue  _  => rfl
-  | isFalse h₁ => absurd rfl h₁
+theorem decide_eq [DecidableEq α] {a b : α} : Eq (decide (Eq a b)) (beq a b) :=
+  match h : beq a b with
+  | true => decide_eq_true (beq_iff_eq.1 h) ▸ rfl
+  | false => decide_eq_false (fun h' => nomatch h.symm.trans (beq_iff_eq.2 h')) ▸ rfl
 
-/-- Decidable equality for Bool -/
-@[inline] def Bool.decEq (a b : Bool) : Decidable (Eq a b) :=
-   match a, b with
-   | false, false => isTrue rfl
-   | false, true  => isFalse (fun h => Bool.noConfusion h)
-   | true, false  => isFalse (fun h => Bool.noConfusion h)
-   | true, true   => isTrue rfl
+theorem of_decide_eq_self_eq_true [DecidableEq α] (a : α) : Eq (decide (Eq a a)) true :=
+  decide_eq_true (Eq.refl a) ▸ rfl
 
-@[inline] instance : DecidableEq Bool :=
-   Bool.decEq
+theorem decide_iff [Decidable p] : Iff (decide p).asProp p :=
+  ⟨of_decide_eq_true, decide_eq_true⟩
 
-/--
-`BEq α` is a typeclass for supplying a boolean-valued equality relation on
-`α`, notated as `a == b`. Unlike `DecidableEq α` (which uses `a = b`), this
-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.
--/
-class BEq (α : Type u) where
-  /-- Boolean equality, notated as `a == b`. -/
-  beq : α → α → Bool
+theorem decide_asProp_of [Decidable p] : p → (decide p).asProp := decide_iff.2
 
-open BEq (beq)
+instance : Decidable (Bool.asProp b) :=
+  match b with
+  | true => isTrue rfl
+  | false => isFalse (nomatch ·)
 
-instance [DecidableEq α] : BEq α where
-  beq a b := decide (Eq a b)
+/-- Boolean equality for Bool -/
+@[inline] protected def Bool.beq : Bool → Bool → Bool
+  | false, false | true, true => true
+  | _, _ => false
 
+@[inline] instance : DecidableEq Bool where
+  beq := Bool.beq
+  beq_iff_eq := @fun
+    | true, true | false, true => .rfl
+    | false, false => ⟨fun _ => rfl, fun _ => rfl⟩
+    | true, false => ⟨.symm, .symm⟩
 
 /--
 "Dependent" if-then-else, normally written via the notation `if h : c then t(h) else e(h)`,
@@ -1469,46 +1529,22 @@ evaluate using the "bignum" representation (see `Nat`). The definition provided
 here is the logical model (and it is soundness-critical that they coincide).
 -/
 @[extern "lean_nat_dec_eq"]
-def Nat.beq : (@& Nat) → (@& Nat) → Bool
+protected def Nat.beq : (@& Nat) → (@& Nat) → Bool
   | zero,   zero   => true
   | zero,   succ _ => false
   | succ _, zero   => false
-  | succ n, succ m => beq n m
+  | succ n, succ m => Nat.beq n m
 
-instance : BEq Nat where
+@[inline] instance : BEq Nat where
   beq := Nat.beq
 
-theorem Nat.eq_of_beq_eq_true : {n m : Nat} → Eq (beq n m) true → Eq n m
-  | zero,   zero,   _ => rfl
-  | zero,   succ _, h => Bool.noConfusion h
-  | succ _, zero,   h => Bool.noConfusion h
-  | succ n, succ m, h =>
-    have : Eq (beq n m) true := h
-    have : Eq n m := eq_of_beq_eq_true this
-    this ▸ rfl
+protected theorem Nat.beq_iff_eq : {n m : Nat} → Iff (beq n m).asProp (Eq n m)
+  | zero, zero => ⟨fun _ => rfl, fun _ => rfl⟩
+  | zero, succ _ | succ _, zero => ⟨(nomatch ·), (nomatch ·)⟩
+  | succ n, succ m => (@Nat.beq_iff_eq n m).trans ⟨(· ▸ rfl), (Nat.noConfusion · (·))⟩
 
-theorem Nat.ne_of_beq_eq_false : {n m : Nat} → Eq (beq n m) false → Not (Eq n m)
-  | zero,   zero,   h₁, _  => Bool.noConfusion h₁
-  | zero,   succ _, _,  h₂ => Nat.noConfusion h₂
-  | succ _, zero,   _,  h₂ => Nat.noConfusion h₂
-  | succ n, succ m, h₁, h₂ =>
-    have : Eq (beq n m) false := h₁
-    Nat.noConfusion h₂ (fun h₂ => absurd h₂ (ne_of_beq_eq_false this))
-
-/--
-A decision procedure for equality of natural numbers.
-
-This definition is overridden in the compiler to efficiently
-evaluate using the "bignum" representation (see `Nat`). The definition provided
-here is the logical model.
--/
-@[reducible, extern "lean_nat_dec_eq"]
-protected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) :=
-  match h:beq n m with
-  | true  => isTrue (eq_of_beq_eq_true h)
-  | false => isFalse (ne_of_beq_eq_false h)
-
-@[inline] instance : DecidableEq Nat := Nat.decEq
+@[inline] instance : DecidableEq Nat where
+  beq_iff_eq := Nat.beq_iff_eq
 
 set_option bootstrap.genMatcherCode false in
 /--
@@ -1649,30 +1685,30 @@ protected theorem Nat.lt_of_le_of_ne {n m : Nat} (h₁ : LE.le n m) (h₂ : Not
   | Or.inl h₃ => h₃
   | Or.inr h₃ => absurd (Nat.le_antisymm h₁ h₃) h₂
 
-theorem Nat.le_of_ble_eq_true (h : Eq (Nat.ble n m) true) : LE.le n m :=
+theorem Nat.le_of_ble (h : (Nat.ble n m).asProp) : LE.le n m :=
   match n, m with
   | 0,      _      => Nat.zero_le _
-  | succ _, succ _ => Nat.succ_le_succ (le_of_ble_eq_true h)
+  | succ _, succ _ => Nat.succ_le_succ (le_of_ble h)
 
-theorem Nat.ble_self_eq_true : (n : Nat) → Eq (Nat.ble n n) true
+theorem Nat.ble_self : (n : Nat) → (Nat.ble n n).asProp
   | 0      => rfl
-  | succ n => ble_self_eq_true n
+  | succ n => ble_self n
 
-theorem Nat.ble_succ_eq_true : {n m : Nat} → Eq (Nat.ble n m) true → Eq (Nat.ble n (succ m)) true
+theorem Nat.ble_succ : {n m : Nat} → (Nat.ble n m).asProp → (Nat.ble n (succ m)).asProp
   | 0,      _,      _ => rfl
-  | succ n, succ _, h => ble_succ_eq_true (n := n) h
+  | succ n, succ _, h => ble_succ (n := n) h
 
-theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true :=
+theorem Nat.ble_of_le (h : LE.le n m) : (Nat.ble n m).asProp :=
   match h with
-  | Nat.le.refl   => Nat.ble_self_eq_true n
-  | Nat.le.step h => Nat.ble_succ_eq_true (ble_eq_true_of_le h)
+  | Nat.le.refl   => Nat.ble_self n
+  | Nat.le.step h => Nat.ble_succ (ble_of_le h)
 
-theorem Nat.not_le_of_not_ble_eq_true (h : Not (Eq (Nat.ble n m) true)) : Not (LE.le n m) :=
-  fun h' => absurd (Nat.ble_eq_true_of_le h') h
+theorem Nat.not_le_of_not_ble (h : Not (Nat.ble n m).asProp) : Not (LE.le n m) :=
+  fun h' => absurd (Nat.ble_of_le h') h
 
 @[extern "lean_nat_dec_le"]
 instance Nat.decLe (n m : @& Nat) : Decidable (LE.le n m) :=
-  dite (Eq (Nat.ble n m) true) (fun h => isTrue (Nat.le_of_ble_eq_true h)) (fun h => isFalse (Nat.not_le_of_not_ble_eq_true h))
+  dite (Nat.ble n m).asProp (fun h => isTrue (Nat.le_of_ble h)) (fun h => isFalse (Nat.not_le_of_not_ble h))
 
 @[extern "lean_nat_dec_lt"]
 instance Nat.decLt (n m : @& Nat) : Decidable (LT.lt n m) :=
@@ -1724,20 +1760,19 @@ structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.2` is a proof that `i.1 < n`. -/
   isLt : LT.lt val n
 
-theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j
-  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+theorem Fin.eq_iff_val_eq {i j : Fin n} : Iff (Eq i j) (Eq i.1 j.1) :=
+  ⟨(· ▸ rfl), (match i, j, · with | .mk .., .mk .., rfl => rfl)⟩
 
-theorem Fin.val_eq_of_eq {n} {i j : Fin n} (h : Eq i j) : Eq i.val j.val :=
-  h ▸ rfl
+theorem Fin.eq_of_val_eq {i j : Fin n} : Eq i.val j.val → Eq i j := Fin.eq_iff_val_eq.2
 
-theorem Fin.ne_of_val_ne {n} {i j : Fin n} (h : Not (Eq i.val j.val)) : Not (Eq i j) :=
+theorem Fin.val_eq_of_eq {i j : Fin n} : Eq i j → Eq i.val j.val := Fin.eq_iff_val_eq.1
+
+theorem Fin.ne_of_val_ne {i j : Fin n} (h : Not (Eq i.val j.val)) : Not (Eq i j) :=
   fun h' => absurd (val_eq_of_eq h') h
 
-instance (n : Nat) : DecidableEq (Fin n) :=
-  fun i j =>
-    match decEq i.val j.val with
-    | isTrue h  => isTrue (Fin.eq_of_val_eq h)
-    | isFalse h => isFalse (Fin.ne_of_val_ne h)
+instance (n : Nat) : DecidableEq (Fin n) where
+  beq i j := beq i.1 j.1
+  beq_iff_eq := .trans (beq_iff_eq (α := Nat)) Fin.eq_iff_val_eq.symm
 
 instance {n} : LT (Fin n) where
   lt a b := LT.lt a.val b.val
@@ -1771,18 +1806,18 @@ This function is overridden with a native implementation.
 def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
   val := { val := n, isLt := h }
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides equality on `UInt8`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint8_dec_eq"]
-def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h)))
+protected def UInt8.beq (a b : UInt8) : Bool :=
+  beq a.1 b.1
 
-instance : DecidableEq UInt8 := UInt8.decEq
+instance : DecidableEq UInt8 where
+  beq := UInt8.beq
+  beq_iff_eq {a b} := (beq_iff_eq (α := Fin _)).trans
+    ⟨(match a, b, · with | {..}, {..}, rfl => rfl), (· ▸ rfl)⟩
 
 instance : Inhabited UInt8 where
   default := UInt8.ofNatCore 0 (by decide)
@@ -1810,18 +1845,18 @@ This function is overridden with a native implementation.
 def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
   val := { val := n, isLt := h }
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides equality on `UInt16`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint16_dec_eq"]
-def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h)))
+protected def UInt16.beq (a b : UInt16) : Bool :=
+  beq a.1 b.1
 
-instance : DecidableEq UInt16 := UInt16.decEq
+instance : DecidableEq UInt16 where
+  beq := UInt16.beq
+  beq_iff_eq {a b} := (beq_iff_eq (α := Fin _)).trans
+    ⟨(match a, b, · with | {..}, {..}, rfl => rfl), (· ▸ rfl)⟩
 
 instance : Inhabited UInt16 where
   default := UInt16.ofNatCore 0 (by decide)
@@ -1856,18 +1891,18 @@ This function is overridden with a native implementation.
 @[extern "lean_uint32_to_nat"]
 def UInt32.toNat (n : UInt32) : Nat := n.val.val
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides equality on `UInt32`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint32_dec_eq"]
-def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt32.noConfusion h' (fun h' => absurd h' h)))
+protected def UInt32.beq (a b : UInt32) : Bool :=
+  beq a.1 b.1
 
-instance : DecidableEq UInt32 := UInt32.decEq
+instance : DecidableEq UInt32 where
+  beq := UInt32.beq
+  beq_iff_eq {a b} := (beq_iff_eq (α := Fin _)).trans
+    ⟨(match a, b, · with | {..}, {..}, rfl => rfl), (· ▸ rfl)⟩
 
 instance : Inhabited UInt32 where
   default := UInt32.ofNatCore 0 (by decide)
@@ -1925,18 +1960,18 @@ This function is overridden with a native implementation.
 def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
   val := { val := n, isLt := h }
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides equality on `UInt64`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_uint64_dec_eq"]
-def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h => isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h)))
+protected def UInt64.beq (a b : UInt64) : Bool :=
+  beq a.1 b.1
 
-instance : DecidableEq UInt64 := UInt64.decEq
+instance : DecidableEq UInt64 where
+  beq := UInt64.beq
+  beq_iff_eq {a b} := (beq_iff_eq (α := Fin _)).trans
+    ⟨(match a, b, · with | {..}, {..}, rfl => rfl), (· ▸ rfl)⟩
 
 instance : Inhabited UInt64 where
   default := UInt64.ofNatCore 0 (by decide)
@@ -1977,18 +2012,18 @@ def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize := {
   val := { val := n, isLt := h }
 }
 
-set_option bootstrap.genMatcherCode false in
 /--
 Decides equality on `USize`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_dec_eq"]
-def USize.decEq (a b : USize) : Decidable (Eq a b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ =>
-    dite (Eq n m) (fun h =>isTrue (h ▸ rfl)) (fun h => isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h)))
+protected def USize.beq (a b : USize) : Bool :=
+  beq a.1 b.1
 
-instance : DecidableEq USize := USize.decEq
+instance : DecidableEq USize where
+  beq := USize.beq
+  beq_iff_eq {a b} := (beq_iff_eq (α := Fin _)).trans
+    ⟨(match a, b, · with | {..}, {..}, rfl => rfl), (· ▸ rfl)⟩
 
 instance : Inhabited USize where
   default := USize.ofNatCore 0 (match USize.size, usize_size_eq with
@@ -2067,10 +2102,7 @@ theorem Char.val_ne_of_ne {c d : Char} (h : Not (Eq c d)) : Not (Eq c.val d.val)
   fun h' => absurd (eq_of_val_eq h') h
 
 instance : DecidableEq Char :=
-  fun c d =>
-    match decEq c.val d.val with
-    | isTrue h  => isTrue (Char.eq_of_val_eq h)
-    | isFalse h => isFalse (Char.ne_of_val_ne h)
+  .ofInj (·.val) @fun | {..}, {..}, rfl => rfl
 
 /-- Returns the number of bytes required to encode this `Char` in UTF-8. -/
 def Char.utf8Size (c : Char) : UInt32 :=
@@ -2164,20 +2196,29 @@ inductive List (α : Type u) where
 instance {α} : Inhabited (List α) where
   default := List.nil
 
-/-- Implements decidable equality for `List α`, assuming `α` has decidable equality. -/
-protected def List.hasDecEq {α : Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b)
-  | nil,       nil       => isTrue rfl
-  | cons _ _, nil        => isFalse (fun h => List.noConfusion h)
-  | nil,       cons _ _  => isFalse (fun h => List.noConfusion h)
-  | cons a as, cons b bs =>
-    match decEq a b with
-    | isTrue hab  =>
-      match List.hasDecEq as bs with
-      | isTrue habs  => isTrue (hab ▸ habs ▸ rfl)
-      | isFalse nabs => isFalse (fun h => List.noConfusion h (fun _ habs => absurd habs nabs))
-    | isFalse nab => isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab))
+/--
+The equality relation on lists asserts that they have the same length
+and they are pairwise `BEq`.
+-/
+protected def List.beq [BEq α] : List α → List α → Bool
+  | nil, nil => true
+  | cons a as, cons b bs => and (beq a b) (List.beq as bs)
+  | _, _ => false
 
-instance {α : Type u} [DecidableEq α] : DecidableEq (List α) := List.hasDecEq
+instance [BEq α] : BEq (List α) := ⟨List.beq⟩
+
+protected theorem List.beq_iff_eq [DecidableEq α] : {a b : List α} → Iff (beq a b).asProp (Eq a b)
+  | nil, nil => ⟨fun _ => rfl, fun _ => rfl⟩
+  | nil, cons _ _ | cons _ _, nil => ⟨(nomatch ·), (nomatch ·)⟩
+  | cons a as, cons b bs =>
+    show Iff (and _ _).asProp _ from
+    match ha : beq a b, has : List.beq as bs with
+    | true, true => ⟨fun _ => beq_iff_eq.1 ha ▸ List.beq_iff_eq.1 has ▸ rfl, fun _ => rfl⟩
+    | false, _ => ⟨(nomatch ·), (List.noConfusion · fun h _ => nomatch ha.symm.trans (beq_iff_eq.2 h))⟩
+    | true, false => ⟨(nomatch ·), (List.noConfusion · fun _ h => nomatch has.symm.trans (List.beq_iff_eq.2 h))⟩
+
+instance [DecidableEq α] : DecidableEq (List α) where
+  beq_iff_eq := List.beq_iff_eq
 
 /--
 Folds a function over a list from the left:
@@ -2259,12 +2300,13 @@ Decides equality on `String`.
 This function is overridden with a native implementation.
 -/
 @[extern "lean_string_dec_eq"]
-def String.decEq (s₁ s₂ : @& String) : Decidable (Eq s₁ s₂) :=
-  match s₁, s₂ with
-  | ⟨s₁⟩, ⟨s₂⟩ =>
-    dite (Eq s₁ s₂) (fun h => isTrue (congrArg _ h)) (fun h => isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h)))
+protected def String.beq (s₁ s₂ : @& String) : Bool :=
+  beq s₁.data s₂.data
 
-instance : DecidableEq String := String.decEq
+instance : DecidableEq String where
+  beq := String.beq
+  beq_iff_eq {a b} := (beq_iff_eq (α := List Char)).trans
+    ⟨(match a, b, · with | {..}, {..}, rfl => rfl), (· ▸ rfl)⟩
 
 /--
 A byte position in a `String`. Internally, `String`s are UTF-8 encoded.
@@ -2281,9 +2323,7 @@ instance : Inhabited String.Pos where
   default := {}
 
 instance : DecidableEq String.Pos :=
-  fun ⟨a⟩ ⟨b⟩ => match decEq a b with
-    | isTrue h => isTrue (h ▸ rfl)
-    | isFalse h => isFalse (fun he => String.Pos.noConfusion he fun he => absurd he h)
+  .ofInj (·.byteIdx) @fun | {..}, {..}, rfl => rfl
 
 /--
 A `Substring` is a view into some subslice of a `String`.
@@ -3452,8 +3492,8 @@ abbrev mkSimple (s : String) : Name :=
 @[extern "lean_name_eq"]
 protected def beq : (@& Name) → (@& Name) → Bool
   | anonymous, anonymous => true
-  | str p₁ s₁, str p₂ s₂ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
-  | num p₁ n₁, num p₂ n₂ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
+  | str p₁ s₁, str p₂ s₂ => and (beq s₁ s₂) (Name.beq p₁ p₂)
+  | num p₁ n₁, num p₂ n₂ => and (beq n₁ n₂) (Name.beq p₁ p₂)
   | _,         _         => false
 
 instance : BEq Name where

src/Init/SimpLemmas.lean

@@ -127,16 +127,15 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
 @[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
 
-@[simp] theorem Bool.beq_to_eq (a b : Bool) :
+theorem Bool.beq_to_eq (a b : Bool) :
   (a == b) = (a = b) := by cases a <;> cases b <;> decide
-@[simp] theorem Bool.not_beq_to_not_eq (a b : Bool) :
+theorem Bool.not_beq_to_not_eq (a b : Bool) :
   (!(a == b)) = ¬(a = b) := by cases a <;> cases b <;> decide
 
 @[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
 @[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide
 
 @[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p := propext <| Iff.intro of_decide_eq_true decide_eq_true
-@[simp] theorem decide_not [h : Decidable p] : decide (¬ p) = !decide p := by cases h <;> rfl
 @[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *]
 
 @[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
@@ -144,14 +143,34 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
 @[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
 
-@[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl
-@[simp] theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp [BEq.beq]
+theorem cond_eq_ite : cond c a b = ite c a b := by cases c <;> simp
+theorem cond_pos : c.asProp → cond c a b = a := by cases c <;> simp
+theorem cond_neg : ¬ c.asProp → cond c a b = b := by cases c <;> simp
 
-@[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]
-@[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
+@[simp] theorem beq_self_eq_true [DecidableEq α] (a : α) : (a == a) = true := by simp [BEq.beq]
+@[simp] theorem bne_self_eq_false [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
 
 @[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
   propext ⟨fun h => Nat.le_antisymm h (Nat.zero_le ..), fun h => by simp [h]⟩
 
+attribute [simp] decide_iff
+@[simp] theorem Bool.asProp_false : false.asProp = False := by simp [asProp]
+@[simp] theorem Bool.asProp_true : true.asProp = True := by simp [asProp]
+@[simp] theorem Bool.asProp_and : (b && c).asProp = (b ∧ c) := by simp [asProp]
+@[simp] theorem Bool.asProp_or : (b || c).asProp = (b ∨ c) := by simp [asProp]
+@[simp] theorem Bool.asProp_not : (!b).asProp = (¬ b) := by simp [asProp]
+@[simp] theorem Bool.asProp_beq [DecidableEq α] (a b : α) : (a == b).asProp = (a = b) := propext beq_iff_eq
+
+theorem Bool.eq_of_asProp_eq {b c : Bool} : b.asProp = c.asProp → b = c := by
+  cases b <;> cases c <;> simp
+
+@[simp] theorem decide_asProp : decide (Bool.asProp b) = b := by cases b <;> simp
 @[simp] theorem decide_False : decide False = false := rfl
 @[simp] theorem decide_True : decide True = true := rfl
+@[simp] theorem decide_and [Decidable p] [Decidable q] : decide (p ∧ q) = (decide p && decide q) := Bool.eq_of_asProp_eq (by simp)
+@[simp] theorem decide_or [Decidable p] [Decidable q] : decide (p ∨ q) = (decide p || decide q) := Bool.eq_of_asProp_eq (by simp)
+@[simp] theorem decide_not [Decidable p] : decide (¬ p) = !decide p := Bool.eq_of_asProp_eq (by simp)
+
+-- Required for the DecidableEq derive handler.
+theorem Bool.true_iff : true ↔ True := by simp [Bool.asProp_true]
+theorem Bool.and_iff_congr {a b : Bool} (ha : a ↔ a') (hb : b ↔ b') : (a && b) ↔ (a' ∧ b') := by simp_all

src/Init/System/FilePath.lean

@@ -8,6 +8,7 @@ import Init.System.Platform
 import Init.Data.String.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
+import Init.NotationExtra
 
 namespace System
 open Platform

src/Init/Util.lean

@@ -57,11 +57,11 @@ unsafe def ptrEqList : (as bs : List α) → Bool
   | _, _ => false
 
 set_option linter.unusedVariables.funArgs false in
-@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
+@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k ()) : Bool :=
   if ptrEq a b then true else k ()
 
 @[implemented_by withPtrEqUnsafe]
-def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool := k ()
+def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k ()) : Bool := k ()
 
 /-- `withPtrEq` for `DecidableEq` -/
 @[inline] def withPtrEqDecEq {α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b) :=

src/Lean/Compiler/ConstFolding.lean

@@ -119,7 +119,6 @@ def foldNatBinPred (mkPred : Expr → Expr → Expr) (fn : Nat → Nat → Bool)
   let n₂   ← getNumLit a₂
   return toDecidableExpr beforeErasure (mkPred a₁ a₂) (fn n₁ n₂)
 
-def foldNatDecEq := foldNatBinPred mkNatEq (fun a b => a = b)
 def foldNatDecLt := foldNatBinPred mkNatLt (fun a b => a < b)
 def foldNatDecLe := foldNatBinPred mkNatLe (fun a b => a ≤ b)
 
@@ -141,7 +140,6 @@ def natFoldFns : List (Name × BinFoldFn) :=
    (``Nat.div, foldNatDiv),
    (``Nat.mod, foldNatMod),
    (``Nat.pow, foldNatPow),
-   (``Nat.decEq, foldNatDecEq),
    (``Nat.decLt, foldNatDecLt),
    (``Nat.decLe, foldNatDecLe),
    (``Nat.beq,   foldNatBeq),

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -334,23 +334,16 @@ def arithmeticFolders : List (Name × Folder) := [
 ]
 
 def relationFolders : List (Name × Folder) := [
-  (``Nat.decEq, Folder.mkBinaryDecisionProcedure Nat.decEq),
   (``Nat.decLt, Folder.mkBinaryDecisionProcedure Nat.decLt),
   (``Nat.decLe, Folder.mkBinaryDecisionProcedure Nat.decLe),
-  (``UInt8.decEq, Folder.mkBinaryDecisionProcedure UInt8.decEq),
   (``UInt8.decLt, Folder.mkBinaryDecisionProcedure UInt8.decLt),
   (``UInt8.decLe, Folder.mkBinaryDecisionProcedure UInt8.decLe),
-  (``UInt16.decEq, Folder.mkBinaryDecisionProcedure UInt16.decEq),
   (``UInt16.decLt, Folder.mkBinaryDecisionProcedure UInt16.decLt),
   (``UInt16.decLe, Folder.mkBinaryDecisionProcedure UInt16.decLe),
-  (``UInt32.decEq, Folder.mkBinaryDecisionProcedure UInt32.decEq),
   (``UInt32.decLt, Folder.mkBinaryDecisionProcedure UInt32.decLt),
   (``UInt32.decLe, Folder.mkBinaryDecisionProcedure UInt32.decLe),
-  (``UInt64.decEq, Folder.mkBinaryDecisionProcedure UInt64.decEq),
   (``UInt64.decLt, Folder.mkBinaryDecisionProcedure UInt64.decLt),
-  (``UInt64.decLe, Folder.mkBinaryDecisionProcedure UInt64.decLe),
-  (``Bool.decEq, Folder.mkBinaryDecisionProcedure Bool.decEq),
-  (``Bool.decEq, Folder.mkBinaryDecisionProcedure String.decEq)
+  (``UInt64.decLe, Folder.mkBinaryDecisionProcedure UInt64.decLe)
 ]
 
 /--

src/Lean/Data/Rat.lean

@@ -14,7 +14,7 @@ structure Rat where
   private mk ::
     num : Int
     den : Nat := 1
-  deriving Inhabited, BEq, DecidableEq
+  deriving Inhabited, DecidableEq
 
 instance : ToString Rat where
   toString a := if a.den == 1 then toString a.num else s!"{a.num}/{a.den}"

src/Lean/Elab/Deriving.lean

@@ -8,8 +8,7 @@ import Lean.Elab.Deriving.Util
 import Lean.Elab.Deriving.Inhabited
 import Lean.Elab.Deriving.Nonempty
 import Lean.Elab.Deriving.TypeName
-import Lean.Elab.Deriving.BEq
-import Lean.Elab.Deriving.DecEq
+import Lean.Elab.Deriving.Eq
 import Lean.Elab.Deriving.Repr
 import Lean.Elab.Deriving.FromToJson
 import Lean.Elab.Deriving.SizeOf

src/Lean/Elab/Deriving/DecEq.lean

@@ -7,35 +7,20 @@ import Lean.Meta.Transform
 import Lean.Meta.Inductive
 import Lean.Elab.Deriving.Basic
 import Lean.Elab.Deriving.Util
+import Lean.Elab.Deriving.BEq
 
 namespace Lean.Elab.Deriving.DecEq
 open Lean.Parser.Term
 open Meta
 
 def mkDecEqHeader (indVal : InductiveVal) : TermElabM Header := do
-  mkHeader `DecidableEq 2 indVal
+  mkHeader `DecidableEq 0 indVal
 
 def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do
-  let discrs ← mkDiscrs header indVal
+  let discrs := (← mkDiscrs header indVal) ++ #[← `(matchDiscr| lhs), ← `(matchDiscr| rhs)]
   let alts ← mkAlts
   `(match $[$discrs],* with $alts:matchAlt*)
 where
-  mkSameCtorRhs : List (Ident × Ident × Bool × Bool) → TermElabM Term
-    | [] => ``(isTrue rfl)
-    | (a, b, recField, isProof) :: todo => withFreshMacroScope do
-      let rhs ← if isProof then
-        `(have h : $a = $b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
-      else
-        `(if h : $a = $b then
-           by subst h; exact $(← mkSameCtorRhs todo):term
-          else
-           isFalse (by intro n; injection n; apply h _; assumption))
-      if recField then
-        -- add local instance for `a = b` using the function being defined `auxFunName`
-        `(let inst := $(mkIdent auxFunName) $a $b; $rhs)
-      else
-        return rhs
-
   mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do
     let mut alts := #[]
     for ctorName₁ in indVal.ctors do
@@ -55,7 +40,7 @@ where
             for _ in [:indVal.numParams] do
               ctorArgs1 := ctorArgs1.push (← `(_))
               ctorArgs2 := ctorArgs2.push (← `(_))
-            let mut todo := #[]
+            let mut rhs ← `(Bool.true_iff)
             for i in [:ctorInfo.numFields] do
               let x := xs[indVal.numParams + i]!
               if type.containsFVar x.fvarId! then
@@ -69,15 +54,23 @@ where
                 ctorArgs2 := ctorArgs2.push b
                 let recField  := (← inferType x).isAppOf indVal.name
                 let isProof := (← inferType (← inferType x)).isProp
-                todo := todo.push (a, b, recField, isProof)
+                if isProof then
+                  pure () -- skip
+                else if recField then
+                  rhs ← `(Bool.and_iff_congr $rhs ($(mkIdent auxFunName) $a $b))
+                else
+                  rhs ← `(Bool.and_iff_congr $rhs (@beq_iff_eq _ _ $a $b))
             patterns := patterns.push (← `(@$(mkIdent ctorName₁):ident $ctorArgs1:term*))
             patterns := patterns.push (← `(@$(mkIdent ctorName₁):ident $ctorArgs2:term*))
-            let rhs ← mkSameCtorRhs todo.toList
+            rhs ← `(by
+              refine .trans $rhs ⟨?_, ?_⟩
+              · intro h; simp only [h] -- solves True ∧ a=b ∧ c=d → ctor a c = ctor b d
+              · intro h; cases h; trivial) -- solves ctor a c = ctor b d → True ∧ a=b ∧ c=d
             `(matchAltExpr| | $[$patterns:term],* => $rhs:term)
           alts := alts.push alt
         else if (← compatibleCtors ctorName₁ ctorName₂) then
           patterns := patterns ++ #[(← `($(mkIdent ctorName₁) ..)), (← `($(mkIdent ctorName₂) ..))]
-          let rhs ← `(isFalse (by intro h; injection h))
+          let rhs ← `(⟨(nomatch ·), (nomatch ·)⟩)
           alts := alts.push (← `(matchAltExpr| | $[$patterns:term],* => $rhs:term))
     return alts
 
@@ -85,10 +78,12 @@ def mkAuxFunction (ctx : Context) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[0]!
   let indVal     :=ctx.typeInfos[0]!
   let header     ← mkDecEqHeader indVal
-  let mut body   ← mkMatch header indVal auxFunName
+  let mut body   ← mkMatch header indVal (← `(ident| deriving_beq_aux)).1.getId
   let binders    := header.binders
-  let type       ← `(Decidable ($(mkIdent header.targetNames[0]!) = $(mkIdent header.targetNames[1]!)))
-  `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term)
+  `(theorem deriving_beq_aux $binders:bracketedBinder* (lhs rhs : $(header.targetType)) :
+      lhs == rhs ↔ lhs = rhs := $body
+    abbrev $(mkIdent auxFunName):ident $binders:bracketedBinder* : DecidableEq $(header.targetType) where
+      beq_iff_eq := deriving_beq_aux ..)
 
 def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do
   let ctx ← mkContext "decEq" indVal.name
@@ -163,17 +158,15 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
   let auxThmIdent := mkIdent (Name.mkStr declName "ofNat_toCtorIdx")
   let cmd ← `(
     instance : DecidableEq $(mkIdent declName) :=
-      fun x y =>
-        if h : x.toCtorIdx = y.toCtorIdx then
-          -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct.
-          isTrue (by first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
-        else
-          isFalse fun h => by subst h; contradiction
-  )
+      .ofInj (·.toCtorIdx) @fun x y h => by
+        -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct.
+        first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
   trace[Elab.Deriving.decEq] "\n{cmd}"
   elabCommand cmd
 
 def mkDecEqInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  -- Call BEq derive handler first, as we require the automatically derived BEq instance.
+  _ ← BEq.mkBEqInstanceHandler declNames
   if declNames.size != 1 then
     return false -- mutually inductive types are not supported yet
   else if (← isEnumType declNames[0]!) then

src/Lean/Elab/Deriving/Eq.lean

@@ -0,0 +1,183 @@
+/-
+Copyright (c) 2023 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Gabriel Ebner
+-/
+import Lean.Meta.Transform
+import Lean.Meta.Inductive
+import Lean.Elab.Deriving.Basic
+
+namespace Lean.Elab.Deriving.Eq
+open Lean.Parser.Term
+open Meta
+
+structure SameCtorResult where
+  beqArm : TSyntax ``matchAlt
+  beqIffEqArm : TSyntax ``matchAlt
+
+def hasFwdDeps (i : Nat) (xs : Array Expr) : MetaM Bool := do
+  let x := xs[i]!
+  for j in [i+1:xs.size] do
+    let y := xs[j]!
+    if ← isProof y then continue
+    if (← inferType y).containsFVar x.fvarId! then
+      return true
+  return false
+
+def sameCtorArm (indVal : InductiveVal) (ctorInfo : ConstructorVal)
+    (beqFn beqIffEqFn : Syntax.Ident) : TermElabM SameCtorResult := do
+  forallTelescopeReducing ctorInfo.type fun xs type => do
+  let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
+  let mut beq ← `(true)
+  let mut proof ← `(⟨fun _ => rfl, fun _ => rfl⟩)
+  let mut ctorArgs1 : List Term := []
+  let mut ctorArgs2 : List Term := []
+  for i in [:ctorInfo.numFields].toArray.reverse do
+    let i := indVal.numParams + i
+    let x := xs[i]!
+    if type.containsFVar x.fvarId! then
+      -- If resulting type depends on this field, we don't need to compare
+      ctorArgs1 := (← `(_)) :: ctorArgs1
+      ctorArgs2 := (← `(_)) :: ctorArgs2
+      continue
+    let a := mkIdent (← mkFreshUserName `x)
+    let b := mkIdent (← mkFreshUserName `y)
+    ctorArgs1 := a :: ctorArgs1
+    ctorArgs2 := b :: ctorArgs2
+    if (← inferType (← inferType x)).isProp then
+      -- proofs are defeq
+      continue
+    let (beqTerm, spec) ←
+      if (← inferType x).isAppOf indVal.name then
+        beq ← `($beqFn $a $b && $beq)
+        pure (← `($beqFn $a $b), ← `($beqIffEqFn $a $b))
+      else if ← hasFwdDeps i xs then
+        beq ← `(
+          if h : $a == $b then
+            have := $(quote i)
+            have heq : $a = $b := (beq_iff_eq' $a $b).1 h
+            by subst heq; exact $beq
+          else
+            false)
+        pure (← `($a == $b), ← `(beq_iff_eq' $a $b))
+      else
+        beq ← `($a == $b && $beq)
+        pure (← `($a == $b), ← `(beq_iff_eq' $a $b))
+    proof ← withFreshMacroScope `(
+      if h : $beqTerm then
+        have heq : $a = $b := ($spec).1 h
+        by subst heq; simp only [Bool.true_and, dif_pos, h]; first | done | exact $proof
+      else
+        have : $a ≠ $b := h ∘ ($spec).2
+        ⟨by simp only [*, dif_neg, Bool.false_and, false_implies], (by injection ·; contradiction)⟩)
+  -- add `_` for inductive parameters, they are inaccessible
+  ctorArgs1 := .replicate indVal.numParams (← `(_)) ++ ctorArgs1
+  ctorArgs2 := .replicate indVal.numParams (← `(_)) ++ ctorArgs2
+  let patterns :=
+    -- add `_` pattern for indices
+    mkArray indVal.numIndices (← `(_)) ++
+    #[← `(@$(mkCIdent ctorInfo.name) $(ctorArgs1.toArray)*),
+      ← `(@$(mkCIdent ctorInfo.name) $(ctorArgs2.toArray)*)]
+  return {
+    beqArm := ← `(matchAltExpr| | $patterns,* => $beq)
+    beqIffEqArm := ← `(matchAltExpr| | $patterns,* =>
+      by simp only [$beqFn:ident]; first | done | exact $proof)
+  }
+
+def mkEqFuns (indVal : InductiveVal) (beqFn beqIffEqFn : Syntax.Ident)
+    (params indices : Array Syntax.Ident) :
+    TermElabM (Command × Command) := do
+  let ctors ← indVal.ctors.mapM fun ctorName => do
+    sameCtorArm indVal (← getConstInfoCtor ctorName) beqFn beqIffEqFn
+  let indPatterns := mkArray indVal.numIndices (← `(_)) -- add `_` pattern for indices
+  let beqArms := ctors.map (·.beqArm) ++ -- TODO: simplify after #2065
+    [(← `(matchAltExpr| | $[$(indPatterns ++ #[← `(_), ← `(_)])],* => false) : TSyntax ``matchAlt)]
+  let beqCmd ← `(
+    set_option match.ignoreUnusedAlts true
+    def $beqFn {$indices*} (lhs rhs : @$(mkCIdent indVal.name) $params* $indices*) : Bool :=
+      -- TODO: simplify after #2065
+      match $((← indices.mapM (`(matchDiscr| $(·):ident))) ++ #[← `(matchDiscr| lhs), ← `(matchDiscr| rhs)]):matchDiscr,* with
+      $(beqArms.toArray):matchAlt*
+  )
+  let mut proofArms : Array (TSyntax ``matchAlt) := ctors.map (·.beqIffEqArm) |>.toArray
+  for ctor1 in indVal.ctors do for ctor2 in indVal.ctors do
+    if ctor1 = ctor2 then continue
+    unless ← compatibleCtors ctor1 ctor2 do continue
+    proofArms := proofArms.push <| ← `(matchAltExpr|
+      -- TODO: simplify after #2065
+      | $[$(indPatterns ++ #[← `(@$(mkCIdent ctor1) ..), ← `($(mkCIdent ctor2) ..)])],* =>
+        ⟨(nomatch ·), (nomatch ·)⟩)
+  let beqIffEqCmd ← `(
+    theorem $beqIffEqFn {$indices*} (lhs rhs : @$(mkCIdent indVal.name) $params* $indices*) : $beqFn lhs rhs ↔ lhs = rhs :=
+      -- TODO: simplify after #2065
+      match $((← indices.mapM (`(matchDiscr| $(·):ident))) ++ #[← `(matchDiscr| lhs), ← `(matchDiscr| rhs)]):matchDiscr,* with
+      $proofArms:matchAlt*
+  )
+  return (beqCmd, beqIffEqCmd)
+
+def paramsWithFwdDeps (indVal : InductiveVal) : MetaM (HashSet Nat) := do
+  let mut ps := {}
+  for ctor in indVal.ctors do
+    ps ← forallTelescopeReducing (← getConstInfoCtor ctor).type fun xs _ => do
+      let mut ps := ps
+      for i in [indVal.numParams:xs.size] do
+        if ← hasFwdDeps i xs then
+          let xsiType ← inferType xs[i]!
+          for j in [:indVal.numParams], p in xs do
+            if xsiType.containsFVar p.fvarId! then
+              ps := ps.insert j
+      return ps
+  return ps
+
+open Lean.Elab.Command
+def mkInstancesDefault (indVal : InductiveVal) (decEq : Bool) : CommandElabM Unit := do
+  elabCommand <| ← liftTermElabM do
+    forallTelescopeReducing indVal.type fun paramsIndices _ => do
+    let paramsIndicesIdents ← paramsIndices.mapM fun p =>
+      return mkIdent (← mkFreshUserName (← p.fvarId!.getUserName).eraseMacroScopes)
+    let params := paramsIndicesIdents[:indVal.numParams].toArray
+    let indices := paramsIndicesIdents[indVal.numParams:].toArray
+    let decEqParams ← paramsWithFwdDeps indVal
+    let mut instsForBEq := #[]
+    let mut instsForDecEq := #[]
+    for i in [:indVal.numParams], p in paramsIndices, pn in params do
+      if let .sort u ← whnfD (← inferType p) then
+      if u.isEquiv .zero then continue
+      instsForBEq := instsForBEq.push <| ←
+        if decEqParams.contains i then
+          `(bracketedBinderF| [DecidableEq $pn])
+        else
+          `(bracketedBinderF| [BEq $pn])
+      instsForDecEq := instsForDecEq.push <| ← `(bracketedBinderF| [DecidableEq $pn])
+    let beqFn : Ident ← `(beq_fn)
+    let beqIffEqFn : Ident ← `(beq_iff_eq_fn)
+    let (beqCmd, beqIffEqCmd) ← withFreshMacroScope do
+      mkEqFuns indVal beqFn beqIffEqFn params indices
+    let beqInst ← `(section
+      variable $[{$params}]* $instsForBEq*
+      $beqCmd:command
+      instance {$indices*} : BEq (@$(mkCIdent indVal.name) $params* $indices*) where
+        beq := $beqFn
+      end)
+    let decEqInst ← `(section
+      variable $[{$params}]* $instsForDecEq*
+      $beqIffEqCmd:command
+      instance {$indices*} : DecidableEq (@$(mkCIdent indVal.name) $params* $indices*) where
+        beq_iff_eq := $beqIffEqFn _ _
+      end)
+    if decEq then `($beqInst $decEqInst:command) else return beqInst
+
+def mkInstanceHandler (decEq : Bool) (declNames : Array Name) : CommandElabM Bool := do
+  if declNames.size != 1 then
+    return false -- mutually inductive types are not supported yet
+  else if (← isEnumType declNames[0]!) then
+    throwError "todo"
+    -- mkDecEqEnum declNames[0]!
+    return true
+  else
+    mkInstancesDefault (← getConstInfoInduct declNames[0]!) decEq
+    return true
+
+builtin_initialize
+  registerDerivingHandler ``DecidableEq <| mkInstanceHandler (decEq := true)
+  registerDerivingHandler ``BEq <| mkInstanceHandler (decEq := false)

src/Lean/Meta/Tactic/LinearArith/Solver.lean

@@ -123,18 +123,18 @@ structure AssumptionId where
 inductive Justification where
   | combine (c₁ : Int) (j₁ : Justification) (c₂ : Int) (j₂ : Justification)
   | assumption (id : AssumptionId)
-  deriving Inhabited, DecidableEq, BEq, Repr
+  deriving Inhabited, DecidableEq, Repr
 
 inductive CnstrKind where
   | eq | div | lt | le
-  deriving Inhabited, DecidableEq, BEq, Repr
+  deriving Inhabited, DecidableEq, Repr
 
 structure Cnstr where
   kind : CnstrKind
   lhs  : Poly
   rhs  : Int
   jst  : Justification
-  deriving Inhabited, DecidableEq, BEq, Repr
+  deriving Inhabited, DecidableEq, Repr
 
 abbrev Cnstr.isStrict (c : Cnstr) : Bool :=
   c.kind matches CnstrKind.lt

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -263,21 +263,14 @@ where
   else if let some (_, lhs, rhs) := type.ne? then
     if inv then
       throwError "invalid '←' modifier in rewrite rule to 'False'"
-    if rhs.isConstOf ``Bool.true then
-      return [(← mkAppM ``Bool.of_not_eq_true #[e], ← mkEq lhs (mkConst ``Bool.false))]
-    else if rhs.isConstOf ``Bool.false then
-      return [(← mkAppM ``Bool.of_not_eq_false #[e], ← mkEq lhs (mkConst ``Bool.true))]
     let type ← mkEq (← mkEq lhs rhs) (mkConst ``False)
     let e    ← mkEqFalse e
     return [(e, type)]
   else if let some p := type.not? then
     if inv then
       throwError "invalid '←' modifier in rewrite rule to 'False'"
-    if let some (_, lhs, rhs) := p.eq? then
-      if rhs.isConstOf ``Bool.true then
-        return [(← mkAppM ``Bool.of_not_eq_true #[e], ← mkEq lhs (mkConst ``Bool.false))]
-      else if rhs.isConstOf ``Bool.false then
-        return [(← mkAppM ``Bool.of_not_eq_false #[e], ← mkEq lhs (mkConst ``Bool.true))]
+    if let some b := p.asProp? then
+      return [(← mkAppM ``Bool.of_not_asProp #[e], ← mkEq b (mkConst ``false))]
     let type ← mkEq p (mkConst ``False)
     let e    ← mkEqFalse e
     return [(e, type)]
@@ -285,6 +278,10 @@ where
     let e₁ := mkProj ``And 0 e
     let e₂ := mkProj ``And 1 e
     return (← go e₁ type₁) ++ (← go e₂ type₂)
+  else if let some b := type.asProp? then
+    if inv then
+      throwError "invalid '←' modifier in rewrite rule to 'true'"
+    return [(← mkAppM ``Bool.of_asProp #[e], ← mkEq b (mkConst ``true))]
   else
     if inv then
       throwError "invalid '←' modifier in rewrite rule to 'True'"

src/Lean/Meta/WHNF.lean

@@ -388,14 +388,12 @@ def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
       return info.name == ``ite
        || info.name == ``dite
        || info.name == ``decEq
-       || info.name == ``Nat.decEq
        || info.name == ``Char.ofNat   || info.name == ``Char.ofNatAux
-       || info.name == ``String.decEq || info.name == ``List.hasDecEq
        || info.name == ``Fin.ofNat
-       || info.name == ``UInt8.ofNat  || info.name == ``UInt8.decEq
-       || info.name == ``UInt16.ofNat || info.name == ``UInt16.decEq
-       || info.name == ``UInt32.ofNat || info.name == ``UInt32.decEq
-       || info.name == ``UInt64.ofNat || info.name == ``UInt64.decEq
+       || info.name == ``UInt8.ofNat
+       || info.name == ``UInt16.ofNat
+       || info.name == ``UInt32.ofNat
+       || info.name == ``UInt64.ofNat
        /- Remark: we need to unfold the following two definitions because they are used for `Fin`, and
           lazy unfolding at `isDefEq` does not unfold projections.  -/
        || info.name == ``HMod.hMod || info.name == ``Mod.mod

src/Lean/Util/Recognizers.lean

@@ -63,6 +63,9 @@ namespace Expr
 @[inline] def and? (p : Expr) : Option (Expr × Expr) :=
   p.app2? ``And
 
+@[inline] def asProp? (p : Expr) : Option Expr :=
+  p.app1? ``Bool.asProp
+
 @[inline] def heq? (p : Expr) : Option (Expr × Expr × Expr × Expr) :=
   p.app4? ``HEq
 

src/library/compiler/csimp.cpp

@@ -1606,10 +1606,8 @@ class csimp_fn {
 
         if (is_constructor_app(env(), major)) {
             return reduce_cases_cnstr(args, I_val, major, is_let_val);
-        } else if (!is_let_val) {
-            return visit_cases_default(e);
         } else {
-            return e;
+            return visit_cases_default(e);
         }
     }
 

src/library/compiler/erase_irrelevant.cpp

@@ -174,7 +174,7 @@ class erase_irrelevant_fn {
         expr zero        = mk_lit(literal(nat(0)));
         expr one         = mk_lit(literal(nat(1)));
         expr nat_type    = mk_constant(get_nat_name());
-        expr dec_eq      = mk_app(mk_constant(get_nat_dec_eq_name()), major, zero);
+        expr dec_eq      = mk_app(mk_constant(get_nat_beq_name()), major, zero);
         expr dec_eq_type = mk_bool();
         expr c           = mk_simple_decl(dec_eq, dec_eq_type);
         expr minor_z     = args[2];

src/library/constants.cpp

@@ -3,7 +3,6 @@
 // DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py
 #include "util/name.h"
 namespace lean{
-name const * g_absurd = nullptr;
 name const * g_and = nullptr;
 name const * g_and_left = nullptr;
 name const * g_and_right = nullptr;
@@ -11,7 +10,6 @@ name const * g_and_intro = nullptr;
 name const * g_and_rec = nullptr;
 name const * g_and_cases_on = nullptr;
 name const * g_array = nullptr;
-name const * g_array_sz = nullptr;
 name const * g_array_data = nullptr;
 name const * g_auto_param = nullptr;
 name const * g_bit0 = nullptr;
@@ -23,9 +21,7 @@ name const * g_bool = nullptr;
 name const * g_bool_false = nullptr;
 name const * g_bool_true = nullptr;
 name const * g_bool_cases_on = nullptr;
-name const * g_cast = nullptr;
 name const * g_char = nullptr;
-name const * g_congr_arg = nullptr;
 name const * g_decidable = nullptr;
 name const * g_decidable_is_true = nullptr;
 name const * g_decidable_is_false = nullptr;
@@ -40,9 +36,6 @@ name const * g_eq_rec_on = nullptr;
 name const * g_eq_rec = nullptr;
 name const * g_eq_ndrec = nullptr;
 name const * g_eq_refl = nullptr;
-name const * g_eq_subst = nullptr;
-name const * g_eq_symm = nullptr;
-name const * g_eq_trans = nullptr;
 name const * g_float = nullptr;
 name const * g_float_array = nullptr;
 name const * g_float_array_data = nullptr;
@@ -75,7 +68,7 @@ name const * g_nat_has_zero = nullptr;
 name const * g_nat_has_one = nullptr;
 name const * g_nat_has_add = nullptr;
 name const * g_nat_add = nullptr;
-name const * g_nat_dec_eq = nullptr;
+name const * g_nat_beq = nullptr;
 name const * g_nat_sub = nullptr;
 name const * g_ne = nullptr;
 name const * g_not = nullptr;
@@ -86,15 +79,11 @@ name const * g_punit = nullptr;
 name const * g_punit_unit = nullptr;
 name const * g_pprod = nullptr;
 name const * g_pprod_mk = nullptr;
-name const * g_pprod_fst = nullptr;
-name const * g_pprod_snd = nullptr;
 name const * g_propext = nullptr;
 name const * g_quot_mk = nullptr;
 name const * g_quot_lift = nullptr;
-name const * g_sorry_ax = nullptr;
 name const * g_string = nullptr;
 name const * g_string_data = nullptr;
-name const * g_subsingleton_elim = nullptr;
 name const * g_task = nullptr;
 name const * g_thunk = nullptr;
 name const * g_thunk_mk = nullptr;
@@ -109,8 +98,6 @@ name const * g_uint32 = nullptr;
 name const * g_uint64 = nullptr;
 name const * g_usize = nullptr;
 void initialize_constants() {
-    g_absurd = new name{"absurd"};
-    mark_persistent(g_absurd->raw());
     g_and = new name{"And"};
     mark_persistent(g_and->raw());
     g_and_left = new name{"And", "left"};
@@ -125,8 +112,6 @@ void initialize_constants() {
     mark_persistent(g_and_cases_on->raw());
     g_array = new name{"Array"};
     mark_persistent(g_array->raw());
-    g_array_sz = new name{"Array", "sz"};
-    mark_persistent(g_array_sz->raw());
     g_array_data = new name{"Array", "data"};
     mark_persistent(g_array_data->raw());
     g_auto_param = new name{"autoParam"};
@@ -149,12 +134,8 @@ void initialize_constants() {
     mark_persistent(g_bool_true->raw());
     g_bool_cases_on = new name{"Bool", "casesOn"};
     mark_persistent(g_bool_cases_on->raw());
-    g_cast = new name{"cast"};
-    mark_persistent(g_cast->raw());
     g_char = new name{"Char"};
     mark_persistent(g_char->raw());
-    g_congr_arg = new name{"congrArg"};
-    mark_persistent(g_congr_arg->raw());
     g_decidable = new name{"Decidable"};
     mark_persistent(g_decidable->raw());
     g_decidable_is_true = new name{"Decidable", "isTrue"};
@@ -183,12 +164,6 @@ void initialize_constants() {
     mark_persistent(g_eq_ndrec->raw());
     g_eq_refl = new name{"Eq", "refl"};
     mark_persistent(g_eq_refl->raw());
-    g_eq_subst = new name{"Eq", "subst"};
-    mark_persistent(g_eq_subst->raw());
-    g_eq_symm = new name{"Eq", "symm"};
-    mark_persistent(g_eq_symm->raw());
-    g_eq_trans = new name{"Eq", "trans"};
-    mark_persistent(g_eq_trans->raw());
     g_float = new name{"Float"};
     mark_persistent(g_float->raw());
     g_float_array = new name{"FloatArray"};
@@ -253,8 +228,8 @@ void initialize_constants() {
     mark_persistent(g_nat_has_add->raw());
     g_nat_add = new name{"Nat", "add"};
     mark_persistent(g_nat_add->raw());
-    g_nat_dec_eq = new name{"Nat", "decEq"};
-    mark_persistent(g_nat_dec_eq->raw());
+    g_nat_beq = new name{"Nat", "beq"};
+    mark_persistent(g_nat_beq->raw());
     g_nat_sub = new name{"Nat", "sub"};
     mark_persistent(g_nat_sub->raw());
     g_ne = new name{"ne"};
@@ -275,24 +250,16 @@ void initialize_constants() {
     mark_persistent(g_pprod->raw());
     g_pprod_mk = new name{"PProd", "mk"};
     mark_persistent(g_pprod_mk->raw());
-    g_pprod_fst = new name{"PProd", "fst"};
-    mark_persistent(g_pprod_fst->raw());
-    g_pprod_snd = new name{"PProd", "snd"};
-    mark_persistent(g_pprod_snd->raw());
     g_propext = new name{"propext"};
     mark_persistent(g_propext->raw());
     g_quot_mk = new name{"Quot", "mk"};
     mark_persistent(g_quot_mk->raw());
     g_quot_lift = new name{"Quot", "lift"};
     mark_persistent(g_quot_lift->raw());
-    g_sorry_ax = new name{"sorryAx"};
-    mark_persistent(g_sorry_ax->raw());
     g_string = new name{"String"};
     mark_persistent(g_string->raw());
     g_string_data = new name{"String", "data"};
     mark_persistent(g_string_data->raw());
-    g_subsingleton_elim = new name{"Subsingleton", "elim"};
-    mark_persistent(g_subsingleton_elim->raw());
     g_task = new name{"Task"};
     mark_persistent(g_task->raw());
     g_thunk = new name{"Thunk"};
@@ -321,7 +288,6 @@ void initialize_constants() {
     mark_persistent(g_usize->raw());
 }
 void finalize_constants() {
-    delete g_absurd;
     delete g_and;
     delete g_and_left;
     delete g_and_right;
@@ -329,7 +295,6 @@ void finalize_constants() {
     delete g_and_rec;
     delete g_and_cases_on;
     delete g_array;
-    delete g_array_sz;
     delete g_array_data;
     delete g_auto_param;
     delete g_bit0;
@@ -341,9 +306,7 @@ void finalize_constants() {
     delete g_bool_false;
     delete g_bool_true;
     delete g_bool_cases_on;
-    delete g_cast;
     delete g_char;
-    delete g_congr_arg;
     delete g_decidable;
     delete g_decidable_is_true;
     delete g_decidable_is_false;
@@ -358,9 +321,6 @@ void finalize_constants() {
     delete g_eq_rec;
     delete g_eq_ndrec;
     delete g_eq_refl;
-    delete g_eq_subst;
-    delete g_eq_symm;
-    delete g_eq_trans;
     delete g_float;
     delete g_float_array;
     delete g_float_array_data;
@@ -393,7 +353,7 @@ void finalize_constants() {
     delete g_nat_has_one;
     delete g_nat_has_add;
     delete g_nat_add;
-    delete g_nat_dec_eq;
+    delete g_nat_beq;
     delete g_nat_sub;
     delete g_ne;
     delete g_not;
@@ -404,15 +364,11 @@ void finalize_constants() {
     delete g_punit_unit;
     delete g_pprod;
     delete g_pprod_mk;
-    delete g_pprod_fst;
-    delete g_pprod_snd;
     delete g_propext;
     delete g_quot_mk;
     delete g_quot_lift;
-    delete g_sorry_ax;
     delete g_string;
     delete g_string_data;
-    delete g_subsingleton_elim;
     delete g_task;
     delete g_thunk;
     delete g_thunk_mk;
@@ -427,7 +383,6 @@ void finalize_constants() {
     delete g_uint64;
     delete g_usize;
 }
-name const & get_absurd_name() { return *g_absurd; }
 name const & get_and_name() { return *g_and; }
 name const & get_and_left_name() { return *g_and_left; }
 name const & get_and_right_name() { return *g_and_right; }
@@ -435,7 +390,6 @@ name const & get_and_intro_name() { return *g_and_intro; }
 name const & get_and_rec_name() { return *g_and_rec; }
 name const & get_and_cases_on_name() { return *g_and_cases_on; }
 name const & get_array_name() { return *g_array; }
-name const & get_array_sz_name() { return *g_array_sz; }
 name const & get_array_data_name() { return *g_array_data; }
 name const & get_auto_param_name() { return *g_auto_param; }
 name const & get_bit0_name() { return *g_bit0; }
@@ -447,9 +401,7 @@ name const & get_bool_name() { return *g_bool; }
 name const & get_bool_false_name() { return *g_bool_false; }
 name const & get_bool_true_name() { return *g_bool_true; }
 name const & get_bool_cases_on_name() { return *g_bool_cases_on; }
-name const & get_cast_name() { return *g_cast; }
 name const & get_char_name() { return *g_char; }
-name const & get_congr_arg_name() { return *g_congr_arg; }
 name const & get_decidable_name() { return *g_decidable; }
 name const & get_decidable_is_true_name() { return *g_decidable_is_true; }
 name const & get_decidable_is_false_name() { return *g_decidable_is_false; }
@@ -464,9 +416,6 @@ name const & get_eq_rec_on_name() { return *g_eq_rec_on; }
 name const & get_eq_rec_name() { return *g_eq_rec; }
 name const & get_eq_ndrec_name() { return *g_eq_ndrec; }
 name const & get_eq_refl_name() { return *g_eq_refl; }
-name const & get_eq_subst_name() { return *g_eq_subst; }
-name const & get_eq_symm_name() { return *g_eq_symm; }
-name const & get_eq_trans_name() { return *g_eq_trans; }
 name const & get_float_name() { return *g_float; }
 name const & get_float_array_name() { return *g_float_array; }
 name const & get_float_array_data_name() { return *g_float_array_data; }
@@ -499,7 +448,7 @@ name const & get_nat_has_zero_name() { return *g_nat_has_zero; }
 name const & get_nat_has_one_name() { return *g_nat_has_one; }
 name const & get_nat_has_add_name() { return *g_nat_has_add; }
 name const & get_nat_add_name() { return *g_nat_add; }
-name const & get_nat_dec_eq_name() { return *g_nat_dec_eq; }
+name const & get_nat_beq_name() { return *g_nat_beq; }
 name const & get_nat_sub_name() { return *g_nat_sub; }
 name const & get_ne_name() { return *g_ne; }
 name const & get_not_name() { return *g_not; }
@@ -510,15 +459,11 @@ name const & get_punit_name() { return *g_punit; }
 name const & get_punit_unit_name() { return *g_punit_unit; }
 name const & get_pprod_name() { return *g_pprod; }
 name const & get_pprod_mk_name() { return *g_pprod_mk; }
-name const & get_pprod_fst_name() { return *g_pprod_fst; }
-name const & get_pprod_snd_name() { return *g_pprod_snd; }
 name const & get_propext_name() { return *g_propext; }
 name const & get_quot_mk_name() { return *g_quot_mk; }
 name const & get_quot_lift_name() { return *g_quot_lift; }
-name const & get_sorry_ax_name() { return *g_sorry_ax; }
 name const & get_string_name() { return *g_string; }
 name const & get_string_data_name() { return *g_string_data; }
-name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; }
 name const & get_task_name() { return *g_task; }
 name const & get_thunk_name() { return *g_thunk; }
 name const & get_thunk_mk_name() { return *g_thunk_mk; }

src/library/constants.h

@@ -5,7 +5,6 @@
 namespace lean {
 void initialize_constants();
 void finalize_constants();
-name const & get_absurd_name();
 name const & get_and_name();
 name const & get_and_left_name();
 name const & get_and_right_name();
@@ -13,7 +12,6 @@ name const & get_and_intro_name();
 name const & get_and_rec_name();
 name const & get_and_cases_on_name();
 name const & get_array_name();
-name const & get_array_sz_name();
 name const & get_array_data_name();
 name const & get_auto_param_name();
 name const & get_bit0_name();
@@ -25,9 +23,7 @@ name const & get_bool_name();
 name const & get_bool_false_name();
 name const & get_bool_true_name();
 name const & get_bool_cases_on_name();
-name const & get_cast_name();
 name const & get_char_name();
-name const & get_congr_arg_name();
 name const & get_decidable_name();
 name const & get_decidable_is_true_name();
 name const & get_decidable_is_false_name();
@@ -42,9 +38,6 @@ name const & get_eq_rec_on_name();
 name const & get_eq_rec_name();
 name const & get_eq_ndrec_name();
 name const & get_eq_refl_name();
-name const & get_eq_subst_name();
-name const & get_eq_symm_name();
-name const & get_eq_trans_name();
 name const & get_float_name();
 name const & get_float_array_name();
 name const & get_float_array_data_name();
@@ -77,7 +70,7 @@ name const & get_nat_has_zero_name();
 name const & get_nat_has_one_name();
 name const & get_nat_has_add_name();
 name const & get_nat_add_name();
-name const & get_nat_dec_eq_name();
+name const & get_nat_beq_name();
 name const & get_nat_sub_name();
 name const & get_ne_name();
 name const & get_not_name();
@@ -88,15 +81,11 @@ name const & get_punit_name();
 name const & get_punit_unit_name();
 name const & get_pprod_name();
 name const & get_pprod_mk_name();
-name const & get_pprod_fst_name();
-name const & get_pprod_snd_name();
 name const & get_propext_name();
 name const & get_quot_mk_name();
 name const & get_quot_lift_name();
-name const & get_sorry_ax_name();
 name const & get_string_name();
 name const & get_string_data_name();
-name const & get_subsingleton_elim_name();
 name const & get_task_name();
 name const & get_thunk_name();
 name const & get_thunk_mk_name();

src/library/constants.txt

@@ -1,4 +1,3 @@
-absurd
 And
 And.left
 And.right
@@ -6,7 +5,6 @@ And.intro
 And.rec
 And.casesOn
 Array
-Array.sz
 Array.data
 autoParam
 bit0
@@ -18,9 +16,7 @@ Bool
 Bool.false
 Bool.true
 Bool.casesOn
-cast
 Char
-congrArg
 Decidable
 Decidable.isTrue
 Decidable.isFalse
@@ -35,9 +31,6 @@ Eq.recOn
 Eq.rec
 Eq.ndrec
 Eq.refl
-Eq.subst
-Eq.symm
-Eq.trans
 Float
 FloatArray
 FloatArray.data
@@ -70,7 +63,7 @@ Nat.HasZero
 Nat.HasOne
 Nat.HasAdd
 Nat.add
-Nat.decEq
+Nat.beq
 Nat.sub
 ne
 Not
@@ -81,15 +74,11 @@ PUnit
 PUnit.unit
 PProd
 PProd.mk
-PProd.fst
-PProd.snd
 propext
 Quot.mk
 Quot.lift
-sorryAx
 String
 String.data
-Subsingleton.elim
 Task
 Thunk
 Thunk.mk