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