Add Haskell.Reasoning.Bool (#32)

This pull request adds a module `Haskell.Reasoning.Bool`.

This modules adds lemmas that relate the operations `&&`, `||` and `not`
on the `Bool` data type to the logical connectives `⋀`, `⋁`, and `¬`
from the metatheory. This simplifies reasoning with predicates of the
form `b ≡ True`, enabling proofs about Haskell functions such as
`filter` or `any`.

This pull request removes a couple of ad-hoc lemmas about logical
connectives that are either obsolete or subsumed by the new module.

lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure.agda

@@ -337,17 +337,6 @@ prop-createPayment-success = λ s destinations x → {!   !}
     Proposition: Never sends funds to known address
 ------------------------------------------------------------------------------}
 
-lemma-neg-or
-  : ∀ {A B : Set}
-  → (A ⋁ B) → (¬ B) → A
-lemma-neg-or (inl a) _ = a
-lemma-neg-or (inr b) ¬b = magic (¬b b)
-
-lemma-neg-impl
-  : ∀ {A B : Set}
-  → (A → B) → ¬ B → ¬ A
-lemma-neg-impl = λ f ¬b a → ¬b (f a)
-
 --
 @0 prop-createPayment-not-known
   : ∀ (s : WalletState)
@@ -360,9 +349,13 @@ lemma-neg-impl = λ f ¬b a → ¬b (f a)
     → ¬ (address ∈ map TxOut.address (TxBody.outputs tx))
 --
 prop-createPayment-not-known s destinations tx created addr known ¬dest =
-    lemma-neg-impl
-        (λ outs → lemma-neg-or (changeOrPartial outs) lem2)
-        (prop-changeAddress-not-Customer s addr known)
+  λ outs →
+    case changeOrPartial outs of λ
+      { (inl caseChange) →
+          magic (prop-changeAddress-not-Customer s addr known caseChange)
+      ; (inr casePartial) →
+          magic (lem2 casePartial)
+      }
   where
     new = newChangeAddress s
     partialTx = record { outputs = map txOutFromPair destinations }

lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/Address.agda

@@ -303,13 +303,6 @@ getBIP32Path s = fmap toBIP32Path ∘ getDerivationPath s
 
 {-# COMPILE AGDA2HS getBIP32Path #-}
 
-lemma-||-⋁
-  : ∀ (b b' : Bool)
-  → (b || b') ≡ True
-  → (b ≡ True) ⋁ (b' ≡ True)
-lemma-||-⋁ True b' refl = inl refl
-lemma-||-⋁ False True refl = inr refl
-
 --
 @0 lemma-getDerivationPath-Just
   : ∀ (s : AddressState)
@@ -333,7 +326,7 @@ lemma-getDerivationPath-Just s addr eq =
               Just DerivationChange
             ∎
           )
-        ; False {{eq2}} → case (lemma-||-⋁ _ (isCustomerAddress s addr) eq) of λ
+        ; False {{eq2}} → case (prop-||-⋁ eq) of λ
           { (inl eqChange) →
             case trans (sym eqChange) eq2 of λ ()
           ; (inr eqCustomer) →

lib/customer-deposit-wallet-pure/agda/Cardano/Write/Tx/Balance.agda

@@ -150,13 +150,6 @@ lemma-isChange-c0
   → isChange new addr
 lemma-isChange-c0 = λ new c0 addr x → c0 `witness` (sym x)
 
-lemma-||-equal
-  : ∀ (b b' : Bool)
-  → (b || b') ≡ True
-  → (b ≡ True) ⋁ (b' ≡ True)
-lemma-||-equal True b' refl = inl refl
-lemma-||-equal False True refl = inr refl
-
 onLeft
   : ∀ {p p' q : Set} → (p → p') → p ⋁ q → p' ⋁ q
 onLeft f (inl p) = inl (f p)
@@ -179,7 +172,7 @@ prop-balanceTransaction-addresses
         ⋁ addr ∈ map TxOut.address (PartialTx.outputs partialTx)
 
 prop-balanceTransaction-addresses u partialTx new c0 tx balance addr el
-    = onLeft lemma2 (lemma-||-equal b1 b2 (sym lemma1))
+    = onLeft lemma2 (prop-||-⋁ (sym lemma1))
   where
     lemma1 =
       begin

lib/customer-deposit-wallet-pure/agda/Haskell/Data/Map.agda

@@ -19,25 +19,6 @@ open import Haskell.Data.Maybe using
 import Haskell.Prelude as List using (map)
 import Haskell.Data.Set as Set
 
-{-----------------------------------------------------------------------------
-    Helpers
-------------------------------------------------------------------------------}
-
--- These lemmas are obvious substitutions,
--- but substitution in a subterm is sometimes cumbersome
--- with equational reasoning.
-lemma-if-True
-  : ∀ {A B : Set} {{_ : Eq A}} (x x' : A) {t f : B}
-  → (x == x') ≡ True
-  → (if (x == x') then t else f) ≡ t
-lemma-if-True _ _ eq1 rewrite eq1 = refl
-
-lemma-if-False
-  : ∀ {A B : Set} {{_ : Eq A}} (x x' : A) {t f : B}
-  → (x == x') ≡ False
-  → (if (x == x') then t else f) ≡ f
-lemma-if-False _ _ eq1 rewrite eq1 = refl
-
 {-----------------------------------------------------------------------------
     Data.Maybe
 ------------------------------------------------------------------------------}

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][].