open import NeilPrelude1
open import BoolProps1
open import Ord1

module BoolOrd1 where

infix  _<₂_ -- _>₂_

≤false : {b : Bool} → false ≤ b
≤false {false} = refl
≤false {true}  = f≤t

≤true : {b : Bool} → b ≤ true
≤true {false} = f≤t
≤true {true}  = refl

≤antisym : {a b : Bool} → a ≤ b → b ≤ a → a ≡ b
≤antisym refl _ = refl
≤antisym f≤t ()

≤trans : {a b c : Bool} → a ≤ b → b ≤ c → a ≤ c
≤trans refl lt2 = lt2
≤trans f≤t lt2 = ≤false

≤total : {a b : Bool} → Either (a ≤ b) (b ≤ a)
≤total {false} = left ≤false
≤total {true} = right ≤true
{-
import TotalOrder
open module ℕTO = TotalOrder _≤_ ≤antisym ≤trans ≤total public
-}

----------------------------------------------------------------

data _<₂_ : Bool → Bool → Set where
  f<t : false <₂ true

<trans : {a b c : Bool} → a <₂ b → b <₂ c → a <₂ c
<trans f<t ()

<trich : {a b : Bool} → Either (a ≡ b × Not (a <₂ b) × Not (b <₂ a))
                        (Either (Not (a ≡ b) × a <₂ b × Not (b <₂ a))
                                (Not (a ≡ b) × Not (a <₂ b) × b <₂ a))
<trich {false} {false} = left (refl & fork (\ ()))
<trich {false} {true} = right (left ((\ ()) & f<t & \ ()))
<trich {true} {false} = right (right ( (\ ()) & (\ ()) & f<t))
<trich {true} {true} = left (refl & fork (\ ()))
{-
import StrictTotalOrder
open module ℕSPO = StrictTotalOrder _<₂_ <trans <trich public

_>₂_ : Bool → Bool → Set
_>₂_ = _>'_ 
-}
-----------------------------------------------------------------

∨max : {a b : Bool} → a ≤ a ∨ b
∨max {false} = ≤false
∨max {true} = refl

∨maxR : {b : Bool} → (a : Bool) → b ≤ a ∨ b
∨maxR false = refl
∨maxR true  = ≤true

∧min : {a b : Bool} → a ∧ b ≤ a
∧min {false} = refl
∧min {true} = ≤true

∧minR : {b : Bool} → (a : Bool) → a ∧ b ≤ b
∧minR true = refl
∧minR false = ≤false

-----------------------------------

≤resp∧ : {a b c d : Bool} → a ≤ c → b ≤ d → (a ∧ b) ≤ (c ∧ d)
≤resp∧ refl refl = refl
≤resp∧ {a} refl f≤t = ≤trans (∧minR a) ≤false
≤resp∧ f≤t refl = ≤false
≤resp∧ f≤t f≤t = f≤t

≤resp∧L : {a b c : Bool} → a ≤ c → (a ∧ b) ≤ (c ∧ b)
≤resp∧L = flip ≤resp∧ refl

≤resp∧R : {b c : Bool} → (a : Bool) → b ≤ c → (a ∧ b) ≤ (a ∧ c)
≤resp∧R a = ≤resp∧ {a} refl
{-
≤resp∨ : {a b c d : Bool} →  a ≤ c → b ≤ d → (a ∨ b) ≤ (c ∨ d)
≤resp∨ refl refl = refl
≤resp∨ .{_} .{_} {c} refl f≤t = {!!} -- ≤substL ? (∨max {c})
≤resp∨ f≤t refl = ≤true
≤resp∨ f≤t f≤t = f≤t

≤resp∨L : {a b c : Bool} →  a ≤ c → (a ∨ b) ≤ (c ∨ b)
≤resp∨L = flip ≤resp∨ refl

≤resp∨R : {b c : Bool} → (a : Bool) → b ≤ c → (a ∨ b) ≤ (a ∨ c)
≤resp∨R a = ≤resp∨ {a} refl 
-}
≤false≡min : {b : Bool} → b ≤ false → b ≡ false
≤false≡min refl = refl

≥max≡max : {b : Bool} → b ≥ true → b ≡ true
≥max≡max refl = refl

≤∧L : {a b c : Bool} → a ≤ c → a ∧ b ≤ c
≤∧L = ≤trans ∧min 

≤∧R : {b c : Bool} → (a : Bool) → b ≤ c → a ∧ b ≤ c
≤∧R a = ≤trans (∧minR a)

≤∨L : {a b c : Bool} → a ≤ b → a ≤ b ∨ c
≤∨L = flip ≤trans ∨max

≤∨R : {a c : Bool} → (b : Bool) → a ≤ c → a ≤ b ∨ c
≤∨R b = flip ≤trans (∨maxR b)