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