open import NeilPrelude1
open import BoolProps1
open import Ord1

module BoolOrd1 where

infix 3 _<₂_ -- _>₂_

≤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)