module logic where

open import Level 

open import Relation.Nullary
open import Relation.Binary hiding (_⇔_) 
open import Relation.Binary.PropositionalEquality

open import Data.Empty
open import Data.Nat hiding (_⊔_)


data Bool : Set where
    true : Bool
    false : Bool

record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   constructor ⟪_,_⟫
   field
      proj1 : A
      proj2 : B

data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   case1 : A → A ∨ B
   case2 : B → A ∨ B

_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
_⇔_ A B =  ( A → B ) ∧ ( B → A )

contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )

double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
double-neg A notnot = notnot A

double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
double-neg2 notnot A = notnot ( double-neg A )

de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))

dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
dont-or {A} {B} (case2 b) ¬A = b

dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
dont-orb {A} {B} (case1 a) ¬B = a


infixr  130 _∧_
infixr  140 _∨_
infixr  150 _⇔_

_/\_ : Bool → Bool → Bool 
true /\ true = true
_ /\ _ = false

_<B?_ : ℕ → ℕ → Bool
ℕ.zero <B? x = true
ℕ.suc x <B? ℕ.zero = false
ℕ.suc x <B? ℕ.suc xx = x <B? xx

-- _<BT_ : ℕ → ℕ → Set
-- ℕ.zero <BT ℕ.zero = ⊤
-- ℕ.zero <BT ℕ.suc b = ⊤
-- ℕ.suc a <BT ℕ.zero = ⊥
-- ℕ.suc a <BT ℕ.suc b = a <BT b


_≟B_ : Decidable {A = Bool} _≡_
true  ≟B true  = yes refl
false ≟B false = yes refl
true  ≟B false = no λ()
false ≟B true  = no λ()

_\/_ : Bool → Bool → Bool 
false \/ false = false
_ \/ _ = true

not_ : Bool → Bool 
not true = false
not false = true 

_<=>_ : Bool → Bool → Bool  
true <=> true = true
false <=> false = true
_ <=> _ = false

infixr  130 _\/_
infixr  140 _/\_