open import NeilPrelude1

module BoolProps1 where


∨assoc : {b c : Bool} → (a : Bool) → (a ∨ b) ∨ c ≡ a ∨ b ∨ c
∨assoc false = refl
∨assoc true = refl

∨comm : {b : Bool} → (a : Bool) → a ∨ b ≡ b ∨ a
∨comm {false} false = refl
∨comm {true} false = refl
∨comm {false} true = refl
∨comm {true} true = refl

∨idem : {b : Bool} → b ∨ b ≡ b
∨idem {false} = refl
∨idem {true} = refl

∨split : {a b : Bool} → a ∨ b ≡ false → a ≡ false × b ≡ false
∨split {false} eq = refl & eq
∨split {true} ()

∧assoc : {b c : Bool} → (a : Bool) → (a ∧ b) ∧ c ≡ a ∧ b ∧ c
∧assoc false = refl
∧assoc true = refl

∧comm : {b : Bool} → (a : Bool) → a ∧ b ≡ b ∧ a
∧comm {false} false = refl
∧comm {true} false = refl
∧comm {false} true = refl
∧comm {true} true = refl 

∧idem : {b : Bool} → b ∧ b ≡ b
∧idem {false} = refl
∧idem {true} = refl

∧split : {a b : Bool} → a ∧ b ≡ true → a ≡ true × b ≡ true
∧split {false} ()
∧split {true} eq = refl & eq

∧∨distr : {b c : Bool} → (a : Bool) → a ∧ (b ∨ c) ≡ a ∧ b ∨ a ∧ c
∧∨distr false = refl
∧∨distr true = refl

{-
import CommSemiRing
open module CommSR = CommSemiRing _∨_ ∨assoc ∨comm false refl _∧_ ∧assoc ∧comm refl true refl ∧∨distr public
-}