module logic where

open import Level
open import Relation.Nullary
open import Relation.Binary hiding(_⇔_)
open import Data.Empty


data Bool : Set where
    true : Bool
    false : Bool

record  _!$\wedge$!_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n !$\sqcup$! m) where
   field
      proj1 : A
      proj2 : B

data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n !$\sqcup$! m) where
   case1 : A !$\rightarrow$! A ∨ B
   case2 : B !$\rightarrow$! A ∨ B

_⇔_ : {n m : Level } !$\rightarrow$! ( A : Set n ) ( B : Set m )  !$\rightarrow$! Set (n !$\sqcup$! m)
_⇔_ A B =  ( A !$\rightarrow$! B ) !$\wedge$! ( B !$\rightarrow$! A )

contra-position : {n m : Level } {A : Set n} {B : Set m} !$\rightarrow$! (A !$\rightarrow$! B) !$\rightarrow$! !$\neg$! B !$\rightarrow$! !$\neg$! A
contra-position {n} {m} {A} {B}  f !$\neg$!b a = !$\neg$!b ( f a )

double-neg : {n  : Level } {A : Set n} !$\rightarrow$! A !$\rightarrow$! !$\neg$! !$\neg$! A
double-neg A notnot = notnot A

double-neg2 : {n  : Level } {A : Set n} !$\rightarrow$! !$\neg$! !$\neg$! !$\neg$! A !$\rightarrow$! !$\neg$! A
double-neg2 notnot A = notnot ( double-neg A )

de-morgan : {n  : Level } {A B : Set n} !$\rightarrow$!  A !$\wedge$! B  !$\rightarrow$! !$\neg$! ( (!$\neg$! A ) ∨ (!$\neg$! B ) )
de-morgan {n} {A} {B} and (case1 !$\neg$!A) = !$\bot$!-elim ( !$\neg$!A ( _!$\wedge$!_.proj1 and ))
de-morgan {n} {A} {B} and (case2 !$\neg$!B) = !$\bot$!-elim ( !$\neg$!B ( _!$\wedge$!_.proj2 and ))

dont-or :　{n m : Level} {A  : Set n} { B : Set m } !$\rightarrow$!  A ∨ B !$\rightarrow$! !$\neg$! A !$\rightarrow$! B
dont-or {A} {B} (case1 a) !$\neg$!A = !$\bot$!-elim ( !$\neg$!A a )
dont-or {A} {B} (case2 b) !$\neg$!A = b

dont-orb :　{n m : Level} {A  : Set n} { B : Set m } !$\rightarrow$!  A ∨ B !$\rightarrow$! !$\neg$! B !$\rightarrow$! A
dont-orb {A} {B} (case2 b) !$\neg$!B = !$\bot$!-elim ( !$\neg$!B b )
dont-orb {A} {B} (case1 a) !$\neg$!B = a



infixr  130 _!$\wedge$!_
infixr  140 _∨_
infixr  150 _⇔_

_!$\wedge$!_ : Bool !$\rightarrow$! Bool !$\rightarrow$! Bool 
true !$\wedge$! true = true
_ !$\wedge$! _ = false

_\/_ : Bool !$\rightarrow$! Bool !$\rightarrow$! Bool 
false \/ false = false
_ \/ _ = true

not_ : Bool !$\rightarrow$! Bool 
not true = false
not false = true 

_<=>_ : Bool !$\rightarrow$! Bool !$\rightarrow$! Bool  
true <=> true = true
false <=> false = true
_ <=> _ = false

infixr  130 _\/_
infixr  140 _!$\wedge$!_

open import Relation.Binary.PropositionalEquality


!$\equiv$!-Bool-func : {A B : Bool } !$\rightarrow$! ( A !$\equiv$! true !$\rightarrow$! B !$\equiv$! true ) !$\rightarrow$! ( B !$\equiv$! true !$\rightarrow$! A !$\equiv$! true ) !$\rightarrow$! A !$\equiv$! B
!$\equiv$!-Bool-func {true} {true} a!$\rightarrow$!b b!$\rightarrow$!a = refl
!$\equiv$!-Bool-func {false} {true} a!$\rightarrow$!b b!$\rightarrow$!a with b!$\rightarrow$!a refl
... | ()
!$\equiv$!-Bool-func {true} {false} a!$\rightarrow$!b b!$\rightarrow$!a with a!$\rightarrow$!b refl
... | ()
!$\equiv$!-Bool-func {false} {false} a!$\rightarrow$!b b!$\rightarrow$!a = refl

bool-!$\equiv$!-? : (a b : Bool) !$\rightarrow$! Dec ( a !$\equiv$! b )
bool-!$\equiv$!-? true true = yes refl
bool-!$\equiv$!-? true false = no (!$\lambda$! ())
bool-!$\equiv$!-? false true = no (!$\lambda$! ())
bool-!$\equiv$!-? false false = yes refl

!$\neg$!-bool-t : {a : Bool} !$\rightarrow$!  !$\neg$! ( a !$\equiv$! true ) !$\rightarrow$! a !$\equiv$! false
!$\neg$!-bool-t {true} ne = !$\bot$!-elim ( ne refl )
!$\neg$!-bool-t {false} ne = refl

!$\neg$!-bool-f : {a : Bool} !$\rightarrow$!  !$\neg$! ( a !$\equiv$! false ) !$\rightarrow$! a !$\equiv$! true
!$\neg$!-bool-f {true} ne = refl
!$\neg$!-bool-f {false} ne = !$\bot$!-elim ( ne refl )

!$\neg$!-bool : {a : Bool} !$\rightarrow$!  a !$\equiv$! false  !$\rightarrow$! a !$\equiv$! true !$\rightarrow$! !$\bot$!
!$\neg$!-bool refl ()

lemma-!$\wedge$!-0 : {a b : Bool} !$\rightarrow$! a !$\wedge$! b !$\equiv$! true !$\rightarrow$! a !$\equiv$! false !$\rightarrow$! !$\bot$!
lemma-!$\wedge$!-0 {true} {true} refl ()
lemma-!$\wedge$!-0 {true} {false} ()
lemma-!$\wedge$!-0 {false} {true} ()
lemma-!$\wedge$!-0 {false} {false} ()

lemma-!$\wedge$!-1 : {a b : Bool} !$\rightarrow$! a !$\wedge$! b !$\equiv$! true !$\rightarrow$! b !$\equiv$! false !$\rightarrow$! !$\bot$!
lemma-!$\wedge$!-1 {true} {true} refl ()
lemma-!$\wedge$!-1 {true} {false} ()
lemma-!$\wedge$!-1 {false} {true} ()
lemma-!$\wedge$!-1 {false} {false} ()

bool-and-tt : {a b : Bool} !$\rightarrow$! a !$\equiv$! true !$\rightarrow$! b !$\equiv$! true !$\rightarrow$! ( a !$\wedge$! b ) !$\equiv$! true
bool-and-tt refl refl = refl

bool-!$\wedge$!!$\rightarrow$!tt-0 : {a b : Bool} !$\rightarrow$! ( a !$\wedge$! b ) !$\equiv$! true !$\rightarrow$! a !$\equiv$! true 
bool-!$\wedge$!!$\rightarrow$!tt-0 {true} {true} refl = refl
bool-!$\wedge$!!$\rightarrow$!tt-0 {false} {_} ()

bool-!$\wedge$!!$\rightarrow$!tt-1 : {a b : Bool} !$\rightarrow$! ( a !$\wedge$! b ) !$\equiv$! true !$\rightarrow$! b !$\equiv$! true 
bool-!$\wedge$!!$\rightarrow$!tt-1 {true} {true} refl = refl
bool-!$\wedge$!!$\rightarrow$!tt-1 {true} {false} ()
bool-!$\wedge$!!$\rightarrow$!tt-1 {false} {false} ()

bool-or-1 : {a b : Bool} !$\rightarrow$! a !$\equiv$! false !$\rightarrow$! ( a \/ b ) !$\equiv$! b 
bool-or-1 {false} {true} refl = refl
bool-or-1 {false} {false} refl = refl
bool-or-2 : {a b : Bool} !$\rightarrow$! b !$\equiv$! false !$\rightarrow$! (a \/ b ) !$\equiv$! a 
bool-or-2 {true} {false} refl = refl
bool-or-2 {false} {false} refl = refl

bool-or-3 : {a : Bool} !$\rightarrow$! ( a \/ true ) !$\equiv$! true 
bool-or-3 {true} = refl
bool-or-3 {false} = refl

bool-or-31 : {a b : Bool} !$\rightarrow$! b !$\equiv$! true  !$\rightarrow$! ( a \/ b ) !$\equiv$! true 
bool-or-31 {true} {true} refl = refl
bool-or-31 {false} {true} refl = refl

bool-or-4 : {a : Bool} !$\rightarrow$! ( true \/ a ) !$\equiv$! true 
bool-or-4 {true} = refl
bool-or-4 {false} = refl

bool-or-41 : {a b : Bool} !$\rightarrow$! a !$\equiv$! true  !$\rightarrow$! ( a \/ b ) !$\equiv$! true 
bool-or-41 {true} {b} refl = refl

bool-and-1 : {a b : Bool} !$\rightarrow$!  a !$\equiv$! false !$\rightarrow$! (a !$\wedge$! b ) !$\equiv$! false
bool-and-1 {false} {b} refl = refl
bool-and-2 : {a b : Bool} !$\rightarrow$!  b !$\equiv$! false !$\rightarrow$! (a !$\wedge$! b ) !$\equiv$! false
bool-and-2 {true} {false} refl = refl
bool-and-2 {false} {false} refl = refl