|
2
|
1 module logic where
|
|
|
2
|
|
|
3 open import Level
|
|
|
4 open import Relation.Nullary
|
|
|
5 open import Relation.Binary hiding(_⇔_)
|
|
|
6 open import Data.Empty
|
|
|
7
|
|
|
8
|
|
|
9 data Bool : Set where
|
|
|
10 true : Bool
|
|
|
11 false : Bool
|
|
|
12
|
|
|
13 record _@$\wedge$@_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where
|
|
|
14 field
|
|
|
15 proj1 : A
|
|
|
16 proj2 : B
|
|
|
17
|
|
|
18 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where
|
|
|
19 case1 : A @$\rightarrow$@ A ∨ B
|
|
|
20 case2 : B @$\rightarrow$@ A ∨ B
|
|
|
21
|
|
|
22 _⇔_ : {n m : Level } @$\rightarrow$@ ( A : Set n ) ( B : Set m ) @$\rightarrow$@ Set (n @$\sqcup$@ m)
|
|
|
23 _⇔_ A B = ( A @$\rightarrow$@ B ) @$\wedge$@ ( B @$\rightarrow$@ A )
|
|
|
24
|
|
|
25 contra-position : {n m : Level } {A : Set n} {B : Set m} @$\rightarrow$@ (A @$\rightarrow$@ B) @$\rightarrow$@ @$\neg$@ B @$\rightarrow$@ @$\neg$@ A
|
|
|
26 contra-position {n} {m} {A} {B} f @$\neg$@b a = @$\neg$@b ( f a )
|
|
|
27
|
|
|
28 double-neg : {n : Level } {A : Set n} @$\rightarrow$@ A @$\rightarrow$@ @$\neg$@ @$\neg$@ A
|
|
|
29 double-neg A notnot = notnot A
|
|
|
30
|
|
|
31 double-neg2 : {n : Level } {A : Set n} @$\rightarrow$@ @$\neg$@ @$\neg$@ @$\neg$@ A @$\rightarrow$@ @$\neg$@ A
|
|
|
32 double-neg2 notnot A = notnot ( double-neg A )
|
|
|
33
|
|
|
34 de-morgan : {n : Level } {A B : Set n} @$\rightarrow$@ A @$\wedge$@ B @$\rightarrow$@ @$\neg$@ ( (@$\neg$@ A ) ∨ (@$\neg$@ B ) )
|
|
|
35 de-morgan {n} {A} {B} and (case1 @$\neg$@A) = @$\bot$@-elim ( @$\neg$@A ( _@$\wedge$@_.proj1 and ))
|
|
|
36 de-morgan {n} {A} {B} and (case2 @$\neg$@B) = @$\bot$@-elim ( @$\neg$@B ( _@$\wedge$@_.proj2 and ))
|
|
|
37
|
|
|
38 dont-or : {n m : Level} {A : Set n} { B : Set m } @$\rightarrow$@ A ∨ B @$\rightarrow$@ @$\neg$@ A @$\rightarrow$@ B
|
|
|
39 dont-or {A} {B} (case1 a) @$\neg$@A = @$\bot$@-elim ( @$\neg$@A a )
|
|
|
40 dont-or {A} {B} (case2 b) @$\neg$@A = b
|
|
|
41
|
|
|
42 dont-orb : {n m : Level} {A : Set n} { B : Set m } @$\rightarrow$@ A ∨ B @$\rightarrow$@ @$\neg$@ B @$\rightarrow$@ A
|
|
|
43 dont-orb {A} {B} (case2 b) @$\neg$@B = @$\bot$@-elim ( @$\neg$@B b )
|
|
|
44 dont-orb {A} {B} (case1 a) @$\neg$@B = a
|
|
|
45
|
|
|
46
|
|
|
47
|
|
|
48 infixr 130 _@$\wedge$@_
|
|
|
49 infixr 140 _∨_
|
|
|
50 infixr 150 _⇔_
|
|
|
51
|
|
|
52 _@$\wedge$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool
|
|
|
53 true @$\wedge$@ true = true
|
|
|
54 _ @$\wedge$@ _ = false
|
|
|
55
|
|
|
56 _\/_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool
|
|
|
57 false \/ false = false
|
|
|
58 _ \/ _ = true
|
|
|
59
|
|
|
60 not_ : Bool @$\rightarrow$@ Bool
|
|
|
61 not true = false
|
|
|
62 not false = true
|
|
|
63
|
|
|
64 _<=>_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool
|
|
|
65 true <=> true = true
|
|
|
66 false <=> false = true
|
|
|
67 _ <=> _ = false
|
|
|
68
|
|
|
69 infixr 130 _\/_
|
|
|
70 infixr 140 _@$\wedge$@_
|
|
|
71
|
|
|
72 open import Relation.Binary.PropositionalEquality
|
|
|
73
|
|
|
74
|
|
|
75 @$\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
|
|
|
76 @$\equiv$@-Bool-func {true} {true} a@$\rightarrow$@b b@$\rightarrow$@a = refl
|
|
|
77 @$\equiv$@-Bool-func {false} {true} a@$\rightarrow$@b b@$\rightarrow$@a with b@$\rightarrow$@a refl
|
|
|
78 ... | ()
|
|
|
79 @$\equiv$@-Bool-func {true} {false} a@$\rightarrow$@b b@$\rightarrow$@a with a@$\rightarrow$@b refl
|
|
|
80 ... | ()
|
|
|
81 @$\equiv$@-Bool-func {false} {false} a@$\rightarrow$@b b@$\rightarrow$@a = refl
|
|
|
82
|
|
|
83 bool-@$\equiv$@-? : (a b : Bool) @$\rightarrow$@ Dec ( a @$\equiv$@ b )
|
|
|
84 bool-@$\equiv$@-? true true = yes refl
|
|
|
85 bool-@$\equiv$@-? true false = no (@$\lambda$@ ())
|
|
|
86 bool-@$\equiv$@-? false true = no (@$\lambda$@ ())
|
|
|
87 bool-@$\equiv$@-? false false = yes refl
|
|
|
88
|
|
|
89 @$\neg$@-bool-t : {a : Bool} @$\rightarrow$@ @$\neg$@ ( a @$\equiv$@ true ) @$\rightarrow$@ a @$\equiv$@ false
|
|
|
90 @$\neg$@-bool-t {true} ne = @$\bot$@-elim ( ne refl )
|
|
|
91 @$\neg$@-bool-t {false} ne = refl
|
|
|
92
|
|
|
93 @$\neg$@-bool-f : {a : Bool} @$\rightarrow$@ @$\neg$@ ( a @$\equiv$@ false ) @$\rightarrow$@ a @$\equiv$@ true
|
|
|
94 @$\neg$@-bool-f {true} ne = refl
|
|
|
95 @$\neg$@-bool-f {false} ne = @$\bot$@-elim ( ne refl )
|
|
|
96
|
|
|
97 @$\neg$@-bool : {a : Bool} @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ @$\bot$@
|
|
|
98 @$\neg$@-bool refl ()
|
|
|
99
|
|
|
100 lemma-@$\wedge$@-0 : {a b : Bool} @$\rightarrow$@ a @$\wedge$@ b @$\equiv$@ true @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ @$\bot$@
|
|
|
101 lemma-@$\wedge$@-0 {true} {true} refl ()
|
|
|
102 lemma-@$\wedge$@-0 {true} {false} ()
|
|
|
103 lemma-@$\wedge$@-0 {false} {true} ()
|
|
|
104 lemma-@$\wedge$@-0 {false} {false} ()
|
|
|
105
|
|
|
106 lemma-@$\wedge$@-1 : {a b : Bool} @$\rightarrow$@ a @$\wedge$@ b @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ @$\bot$@
|
|
|
107 lemma-@$\wedge$@-1 {true} {true} refl ()
|
|
|
108 lemma-@$\wedge$@-1 {true} {false} ()
|
|
|
109 lemma-@$\wedge$@-1 {false} {true} ()
|
|
|
110 lemma-@$\wedge$@-1 {false} {false} ()
|
|
|
111
|
|
|
112 bool-and-tt : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ true @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true
|
|
|
113 bool-and-tt refl refl = refl
|
|
|
114
|
|
|
115 bool-@$\wedge$@@$\rightarrow$@tt-0 : {a b : Bool} @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true @$\rightarrow$@ a @$\equiv$@ true
|
|
|
116 bool-@$\wedge$@@$\rightarrow$@tt-0 {true} {true} refl = refl
|
|
|
117 bool-@$\wedge$@@$\rightarrow$@tt-0 {false} {_} ()
|
|
|
118
|
|
|
119 bool-@$\wedge$@@$\rightarrow$@tt-1 : {a b : Bool} @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ true
|
|
|
120 bool-@$\wedge$@@$\rightarrow$@tt-1 {true} {true} refl = refl
|
|
|
121 bool-@$\wedge$@@$\rightarrow$@tt-1 {true} {false} ()
|
|
|
122 bool-@$\wedge$@@$\rightarrow$@tt-1 {false} {false} ()
|
|
|
123
|
|
|
124 bool-or-1 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ ( a \/ b ) @$\equiv$@ b
|
|
|
125 bool-or-1 {false} {true} refl = refl
|
|
|
126 bool-or-1 {false} {false} refl = refl
|
|
|
127 bool-or-2 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ (a \/ b ) @$\equiv$@ a
|
|
|
128 bool-or-2 {true} {false} refl = refl
|
|
|
129 bool-or-2 {false} {false} refl = refl
|
|
|
130
|
|
|
131 bool-or-3 : {a : Bool} @$\rightarrow$@ ( a \/ true ) @$\equiv$@ true
|
|
|
132 bool-or-3 {true} = refl
|
|
|
133 bool-or-3 {false} = refl
|
|
|
134
|
|
|
135 bool-or-31 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ true @$\rightarrow$@ ( a \/ b ) @$\equiv$@ true
|
|
|
136 bool-or-31 {true} {true} refl = refl
|
|
|
137 bool-or-31 {false} {true} refl = refl
|
|
|
138
|
|
|
139 bool-or-4 : {a : Bool} @$\rightarrow$@ ( true \/ a ) @$\equiv$@ true
|
|
|
140 bool-or-4 {true} = refl
|
|
|
141 bool-or-4 {false} = refl
|
|
|
142
|
|
|
143 bool-or-41 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ ( a \/ b ) @$\equiv$@ true
|
|
|
144 bool-or-41 {true} {b} refl = refl
|
|
|
145
|
|
|
146 bool-and-1 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ (a @$\wedge$@ b ) @$\equiv$@ false
|
|
|
147 bool-and-1 {false} {b} refl = refl
|
|
|
148 bool-and-2 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ (a @$\wedge$@ b ) @$\equiv$@ false
|
|
|
149 bool-and-2 {true} {false} refl = refl
|
|
|
150 bool-and-2 {false} {false} refl = refl
|
|
|
151
|
|
|
152
|
