Add Haskell.Reasoning.Bool

lib/customer-deposit-wallet-pure/agda/Haskell/Reasoning.agda

@@ -0,0 +1,13 @@
+{-# OPTIONS --erasure #-}
+
+module Haskell.Reasoning where
+
+{- About
+
+See the Haskell.Reasoning.Core module
+for an extended description of how to use these modules.
+
+-}
+
+open import Haskell.Reasoning.Core public
+open import Haskell.Reasoning.Bool public

lib/customer-deposit-wallet-pure/agda/Haskell/Reasoning/Bool.agda

@@ -0,0 +1,61 @@
+{-# OPTIONS --erasure #-}
+
+module Haskell.Reasoning.Bool where
+
+open import Haskell.Prelude
+open import Haskell.Reasoning.Core
+
+{-----------------------------------------------------------------------------
+    Relate (≡ True) to logical connectives
+------------------------------------------------------------------------------}
+
+-- Logical conjunction
+prop-&&-⋀
+  : ∀ {x y : Bool}
+  → (x && y) ≡ True
+  → (x ≡ True) ⋀ (y ≡ True)
+--
+prop-&&-⋀ {True} {True} refl = refl `and` refl
+
+--
+prop-⋀-&&
+  : ∀ {x y : Bool}
+  → (x ≡ True) ⋀ (y ≡ True)
+  → (x && y) ≡ True
+--
+prop-⋀-&& {True} {True} (refl `and` refl) = refl
+
+-- Logical disjunction
+prop-||-⋁
+  : ∀ {x y : Bool}
+  → (x || y) ≡ True
+  → (x ≡ True) ⋁ (y ≡ True)
+--
+prop-||-⋁ {True} {y} refl = inl refl
+prop-||-⋁ {False} {True} refl = inr refl
+
+--
+prop-⋁-||
+  : ∀ {x y : Bool}
+  → (x ≡ True) ⋁ (y ≡ True)
+  → (x || y) ≡ True
+--
+prop-⋁-|| {True} (inl refl) = refl
+prop-⋁-|| {True} (inr refl) = refl
+prop-⋁-|| {False} (inr refl) = refl
+
+-- Logical negation
+prop-not-¬
+  : ∀ {x : Bool}
+  → (not x ≡ True)
+  → ¬ (x ≡ True)
+--
+prop-not-¬ {True} ()
+
+prop-¬-not
+  : ∀ {x : Bool}
+  → ¬ (x ≡ True)
+  → (not x ≡ True)
+--
+prop-¬-not {False} contra = refl
+prop-¬-not {True} contra = case contra refl of λ ()

lib/customer-deposit-wallet-pure/agda/Haskell/Reasoning.lagda.md → lib/customer-deposit-wallet-pure/agda/Haskell/Reasoning/Core.lagda.md

@@ -4,7 +4,7 @@
 
 ```agda
 {-# OPTIONS --erasure #-}
-module Haskell.Reasoning where
+module Haskell.Reasoning.Core where
 ```
 
 This module bundles tools for reasoning about Haskell programs in [Agda][] and [Agda2hs][].