Add orBothFalse proof

idris-lang · Jun 30, 2023 · 721a83c · 721a83c
1 parent ecf4765
commit 721a83c
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/libs/base/Data/Bool.idr b/libs/base/Data/Bool.idr
@@ -71,6 +71,17 @@ orNotTrue : (x : Bool) -> x || not x = True
 orNotTrue False = Refl
 orNotTrue True = Refl
 
+export
+orBothFalse : {0 x, y : Bool} -> (0 prf : x || y = False) -> (x = False, y = False)
+orBothFalse prf = unerase $ orBothFalse' prf
+  where
+    unerase : (0 prf : (x = False, y = False)) -> (x = False, y = False)
+    unerase (p, q) = (irrelevantEq p, irrelevantEq q)
+
+    orBothFalse' : {x, y : Bool} -> x || y = False -> (x = False, y = False)
+    orBothFalse' {x = False} yFalse = (Refl, yFalse)
+    orBothFalse' {x = True} trueFalse = absurd trueFalse
+
 -- interaction & De Morgan's laws
 
 export