feat: Decidable as subtype of Bool (leanprover#8309)

This PR changes the definition of `Decidable p` to a structure
containing a `Bool` and a proof of either `p` or `¬p`.

This is basically the approach proposed by @kmill in leanprover#2038.

Due to bugs in the old compiler, this was previously not possible;
however, now that the new compiler is enabled, this works perfectly
fine.

Using `Bool` in the definition of `Decidable` has several advantages, in
particular
- There are many more definitional equalities, e.g.
  ```lean
  variable (a b : Bool)

  #check (rfl : decide (a = true) = a)
  #check (rfl : decide (a = false) = !a)
  #check (rfl : decide (a = true ∧ b = true) = a && b)
  #check (rfl : decide (a = true ∨ b = true) = a || b)
  #check (rfl : decide (¬a) = !a)
  #check (rfl : decide (a = true ↔ b = true) = (a == b))
  ```
- The `decide` tactic no longer needs to carry proofs with it, improving
performance for well-written `Decidable` instances.
- `LawfulBEq` and `DecidableEq` are now compatible: When using the
`DecidableEq` instance provided by `LawfulBEq`, `decide (a = b)` is
definitionally equivalent to `a == b`.
- `Decidable` no longer needs special casing in the compiler.

In order to take full advantage from these changes, it is recommended to
use the `decidable_of_bool` and `decidable_of_iff` functions to
construct `Decidable` instances.

This is a breaking change, but in part due to `Decidable.isTrue` and
`Decidable.isFalse` remaining as `match_pattern`s, surprisingly few
(meta-)programs break.

---------

Co-authored-by: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>

Author: Rob23oba

src/Init/Classical.lean

@@ -147,9 +147,7 @@ is classically true but not constructively. -/
 -- This can not be an instance as it would be tried everywhere.
 @[instance_reducible]
 def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
-  match h with
-  | isFalse h => isTrue (Classical.not_not.mp h)
-  | isTrue h => isFalse h
+  decidable_of_decidable_of_iff not_not
 
 attribute [local instance] decidable_of_decidable_not in
 /-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/

src/Init/Core.lean

@@ -817,10 +817,12 @@ instance [DecidableEq α] : LawfulBEq α where
 Non-instance for `DecidableEq` from `LawfulBEq`.
 To use this, add `attribute [local instance 5] instDecidableEqOfLawfulBEq` at the top of a file.
 -/
+@[instance_reducible]
 def instDecidableEqOfLawfulBEq [BEq α] [LawfulBEq α] : DecidableEq α := fun x y =>
-  match h : x == y with
-  | false => .isFalse (not_eq_of_beq_eq_false h)
-  | true => .isTrue (eq_of_beq h)
+  Decidable.intro (x == y)
+    (match h : x == y with
+    | false => not_eq_of_beq_eq_false h
+    | true => eq_of_beq h)
 
 instance : LawfulBEq Char := inferInstance
 
@@ -1087,7 +1089,7 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
 
 /-- Similar to `decide`, but uses an explicit instance -/
 @[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool :=
-  decide (h := d)
+  d.decide
 
 theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true :=
   decide_eq_true (inst := d) h
@@ -1143,14 +1145,15 @@ end Decidable
 section
 variable {p q : Prop}
 /-- Transfer a decidability proof across an equivalence of propositions. -/
-@[inline] def decidable_of_decidable_of_iff [Decidable p] (h : p ↔ q) : Decidable q :=
-  if hp : p then
-    isTrue (Iff.mp h hp)
-  else
-    isFalse fun hq => absurd (Iff.mpr h hq) hp
+abbrev decidable_of_decidable_of_iff [dp : Decidable p] (h : p ↔ q) : Decidable q where
+  decide := decide p
+  reflects_decide :=
+    match dp with
+    | isTrue hp => Iff.mp h hp
+    | isFalse hp => fun hq => absurd (Iff.mpr h hq) hp
 
 /-- Transfer a decidability proof across an equality of propositions. -/
-@[inline] def decidable_of_decidable_of_eq [Decidable p] (h : p = q) : Decidable q :=
+abbrev decidable_of_decidable_of_eq [Decidable p] (h : p = q) : Decidable q :=
   decidable_of_decidable_of_iff (p := p) (h ▸ Iff.rfl)
 end
 
@@ -1161,17 +1164,14 @@ end
   else isTrue (fun h => absurd h hp)
 
 @[inline]
-instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
-  if hp : p then
-    if hq : q then
-      isTrue ⟨fun _ => hq, fun _ => hp⟩
-    else
-      isFalse fun h => hq (h.1 hp)
-  else
-    if hq : q then
-      isFalse fun h => hp (h.2 hq)
-    else
-      isTrue ⟨fun h => absurd h hp, fun h => absurd h hq⟩
+instance {p q} [dp : Decidable p] [dq : Decidable q] : Decidable (p ↔ q) where
+  decide := decide p == decide q
+  reflects_decide :=
+    match dp, dq with
+    | isTrue  hp, isTrue  hq => ⟨fun _ => hq, fun _ => hp⟩
+    | isTrue  hp, isFalse hq => fun h => hq (h.1 hp)
+    | isFalse hp, isTrue  hq => fun h => hp (h.2 hq)
+    | isFalse hp, isFalse hq => ⟨fun h => absurd h hp, fun h => absurd h hq⟩
 
 /-! # if-then-else expression theorems -/
 
@@ -1231,18 +1231,16 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT :
   | isFalse hc => dE hc
 
 /-- 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)
+abbrev noConfusionTypeEnum {α : Sort u} (f : α → Nat) (P : Sort w) (x y : α) : Sort w :=
+  ((f x).beq (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)
+abbrev noConfusionEnum {α : Sort u} (f : α → Nat) {P : Sort w} {x y : α} (h : x = y) : noConfusionTypeEnum f P x y :=
+  ((f x).beq (f y)).casesOn
+    (motive := fun b => (f x).beq (f y) = b → b.casesOn P (P → P))
+    (fun h' => False.elim (Nat.ne_of_beq_eq_false h' (congrArg f h)))
+    (fun _ a => a)
+    rfl
 
 /-! # Inhabited -/
 
@@ -1307,7 +1305,7 @@ theorem recSubsingleton
      {h₂ : ¬p → Sort u}
      [h₃ : ∀ (h : p), Subsingleton (h₁ h)]
      [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)]
-     : Subsingleton (h.casesOn h₂ h₁) :=
+     : Subsingleton (h.falseTrueCases h₂ h₁) :=
   match h with
   | isTrue h  => h₃ h
   | isFalse h => h₄ h
@@ -1453,14 +1451,15 @@ instance [Inhabited α] [Inhabited β] : Inhabited (MProd α β) where
 instance [Inhabited α] [Inhabited β] : Inhabited (PProd α β) where
   default := ⟨default, default⟩
 
-instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
+instance [h : DecidableEq α] [h' : 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 rfl rfl (heq_of_eq h) fun _   e₂' => absurd (eq_of_heq e₂') n₂
-    | isFalse n₁ => isFalse fun h => Prod.noConfusion rfl rfl (heq_of_eq h) fun e₁' _   => absurd (eq_of_heq e₁') n₁
+    Decidable.intro (decide (a = a') && decide (b = b'))
+      (match h a a' with
+      | isTrue e₁ =>
+        match h' b b' with
+        | isTrue e₂  => (e₁ ▸ e₂ ▸ rfl : (a, b) = (a', b'))
+        | isFalse n₂ => fun h => Prod.noConfusion rfl rfl (heq_of_eq h) fun _ e₂' => absurd (eq_of_heq e₂') n₂
+      | isFalse n₁ => fun h => Prod.noConfusion rfl rfl (heq_of_eq h) fun e₁' _   => absurd (eq_of_heq e₁') n₁)
 
 instance [BEq α] [BEq β] : BEq (α × β) where
   beq := fun (a₁, b₁) (a₂, b₂) => a₁ == a₂ && b₁ == b₂
@@ -1611,9 +1610,7 @@ theorem Eq.propIntro {a b : Prop} (h₁ : a → b) (h₂ : b → a) : a = b :=
 
 -- Eq for Prop is now decidable if the equivalent Iff is decidable
 instance {p q : Prop} [d : Decidable (p ↔ q)] : Decidable (p = q) :=
-  match d with
-  | isTrue h => isTrue (propext h)
-  | isFalse h => isFalse fun heq => h (heq ▸ Iff.rfl)
+  decidable_of_decidable_of_iff ⟨propext, Iff.of_eq⟩
 
 /-- Helper theorem for proving injectivity theorems -/
 theorem Lean.injEq_helper {P Q R : Prop} :
@@ -2243,9 +2240,10 @@ instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : ∀ (a b : α),
   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₂
+        Decidable.intro (decide (a₁ ≈ a₂))
+          (match d a₁ a₂ with
+          | isTrue h₁  => Quotient.sound h₁
+          | isFalse h₂ => fun h => absurd (Quotient.exact h) h₂)
 
 /--
 Like `Quot.liftOn q f h` but allows `f a` to "know" that `q = Quot.mk r a`.

src/Init/Data/Bool.lean

@@ -32,16 +32,18 @@ abbrev xor : Bool → Bool → Bool := bne
 recommended_spelling "xor" for "^^" in [xor, «term_^^_»]
 
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
-  match inst true, inst false with
-  | isFalse ht, _ => isFalse fun h => absurd (h _) ht
-  | _, isFalse hf => isFalse fun h => absurd (h _) hf
-  | isTrue ht, isTrue hf => isTrue fun | true => ht | false => hf
+  Decidable.intro (p true && p false)
+    (match inst true, inst false with
+    | isFalse ht, _ => fun h => absurd (h _) ht
+    | isTrue _, isFalse hf => fun h => absurd (h _) hf
+    | isTrue ht, isTrue hf => fun | true => ht | false => hf)
 
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∃ x, p x) :=
-  match inst true, inst false with
-  | isTrue ht, _ => isTrue ⟨_, ht⟩
-  | _, isTrue hf => isTrue ⟨_, hf⟩
-  | isFalse ht, isFalse hf => isFalse fun | ⟨true, h⟩ => absurd h ht | ⟨false, h⟩ => absurd h hf
+  Decidable.intro (p true || p false)
+    (match inst true, inst false with
+    | isTrue ht, _ => ⟨_, ht⟩
+    | isFalse _, isTrue hf => ⟨_, hf⟩
+    | isFalse ht, isFalse hf => fun | ⟨true, h⟩ => absurd h ht | ⟨false, h⟩ => absurd h hf)
 
 @[simp] theorem default_bool : default = false := rfl
 
@@ -636,15 +638,15 @@ protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = tru
   cases dp with | _ p => simp [p]
 
 @[bool_to_prop]
-theorem and_eq_decide (p q : Bool) : (p && q) = decide (p ∧ q) := by simp
+theorem and_eq_decide (p q : Bool) : (p && q) = decide (p ∧ q) := rfl
 
 @[bool_to_prop]
-theorem or_eq_decide (p q : Bool) : (p || q) = decide (p ∨ q) := by simp
+theorem or_eq_decide (p q : Bool) : (p || q) = decide (p ∨ q) := rfl
 
 @[bool_to_prop]
-theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] :
-    (decide p == decide q) = decide (p ↔ q) := by
-  cases dp with | _ p => simp [p]
+theorem decide_beq_decide (p q : Prop) [dp : Decidable p] [dq : Decidable q] :
+    (decide p == decide q) = decide (p ↔ q) :=
+  rfl
 
 end Bool
 

src/Init/Data/List/Basic.lean

@@ -123,15 +123,6 @@ theorem of_concat_eq_concat {as bs : List α} {a b : α} (h : as.concat a = bs.c
 
 /-! ## Equality -/
 
-/--
-Checks whether two lists have the same length and their elements are pairwise `BEq`. Normally used
-via the `==` operator.
--/
-protected def beq [BEq α] : List α → List α → Bool
-  | [],    []    => true
-  | a::as, b::bs => a == b && List.beq as bs
-  | _,     _     => false
-
 @[simp] theorem beq_nil_nil [BEq α] : List.beq ([] : List α) ([] : List α) = true := rfl
 @[simp] theorem beq_cons_nil [BEq α] {a : α} {as : List α} : List.beq (a::as) [] = false := rfl
 @[simp] theorem beq_nil_cons [BEq α] {a : α} {as : List α} : List.beq [] (a::as) = false := rfl