feat: add SemiDeciable and withPtrEqSubsingleton

src/Init/Core.lean

@@ -306,6 +306,18 @@ abbrev DecidableEq (α : Sort u) :=
 def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) :=
 s a b
 
+class inductive SemiDeciable (p : Prop)
+| unknown {}     : SemiDeciable
+| isTrue (h : p) : SemiDeciable
+
+def Decidable.toSemiDecidable {p : Prop} (d : Decidable p) : SemiDeciable p :=
+match d with
+| Decidable.isTrue h => SemiDeciable.isTrue h
+| _                  => SemiDeciable.unknown
+
+instance SemiDeciable.ofDecidable {p : Prop} [d : Decidable p] : SemiDeciable p :=
+d.toSemiDecidable
+
 inductive Option (α : Type u)
 | none {} : Option
 | some (val : α) : Option

src/Init/Util.lean

@@ -47,18 +47,24 @@ k (ptrAddrUnsafe a)
 @[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
 if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()
 
+@[inline] unsafe def withPtrEqSubsingletonUnsafe {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : SemiDeciable (a = b) → β) : β :=
+if ptrAddrUnsafe a == ptrAddrUnsafe b then k (SemiDeciable.isTrue lcProof) else k SemiDeciable.unknown
+
 @[implementedBy withPtrEqUnsafe]
 def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
 k ()
 
--- `withPtrEq` for `DecidableEq`
-
+/-- `withPtrEq` for `DecidableEq` -/
 @[inline] def withPtrEqDecEq {α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b) :=
 let b := withPtrEq a b (fun _ => toBoolUsing (k ())) (toBoolUsingEqTrue (k ()));
 condEq b
   (fun h => isTrue (ofBoolUsingEqTrue h))
   (fun h => isFalse (ofBoolUsingEqFalse h))
 
+@[implementedBy withPtrEqSubsingletonUnsafe]
+def withPtrEqSubsingleton {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : SemiDeciable (a = b) → β) : β :=
+k SemiDeciable.unknown
+
 @[implementedBy withPtrAddrUnsafe]
 def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
 k 0