|
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
|
|
5
|
13 record _!$\wedge$!_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n !$\sqcup$! m) where
|
|
2
|
14 field
|
|
|
15 proj1 : A
|
|
|
16 proj2 : B
|
|
|
17
|
|
5
|
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
|
|
2
|
21
|
|
5
|
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 )
|
|
2
|
24
|
|
5
|
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 )
|
|
2
|
27
|
|
5
|
28 double-neg : {n : Level } {A : Set n} !$\rightarrow$! A !$\rightarrow$! !$\neg$! !$\neg$! A
|
|
2
|
29 double-neg A notnot = notnot A
|
|
|
30
|
|
5
|
31 double-neg2 : {n : Level } {A : Set n} !$\rightarrow$! !$\neg$! !$\neg$! !$\neg$! A !$\rightarrow$! !$\neg$! A
|
|
2
|
32 double-neg2 notnot A = notnot ( double-neg A )
|
|
|
33
|
|
5
|
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 ))
|
|
2
|
37
|
|
5
|
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
|
|
2
|
41
|
|
5
|
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
|
|
2
|
45
|
|
|
46
|
|
|
47
|
|
5
|
48 infixr 130 _!$\wedge$!_
|
|
2
|
49 infixr 140 _∨_
|
|
|
50 infixr 150 _⇔_
|
|
|
51
|
|
5
|
52 _!$\wedge$!_ : Bool !$\rightarrow$! Bool !$\rightarrow$! Bool
|
|
|
53 true !$\wedge$! true = true
|
|
|
54 _ !$\wedge$! _ = false
|
|
2
|
55
|
|
5
|
56 _\/_ : Bool !$\rightarrow$! Bool !$\rightarrow$! Bool
|
|
2
|
57 false \/ false = false
|
|
|
58 _ \/ _ = true
|
|
|
59
|
|
5
|
60 not_ : Bool !$\rightarrow$! Bool
|
|
2
|
61 not true = false
|
|
|
62 not false = true
|
|
|
63
|
|
5
|
64 _<=>_ : Bool !$\rightarrow$! Bool !$\rightarrow$! Bool
|
|
2
|
65 true <=> true = true
|
|
|
66 false <=> false = true
|
|
|
67 _ <=> _ = false
|
|
|
68
|
|
|
69 infixr 130 _\/_
|
|
5
|
70 infixr 140 _!$\wedge$!_
|
|
2
|
71
|
|
|
72 open import Relation.Binary.PropositionalEquality
|
|
|
73
|
|
|
74
|
|
5
|
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
|
|
2
|
78 ... | ()
|
|
5
|
79 !$\equiv$!-Bool-func {true} {false} a!$\rightarrow$!b b!$\rightarrow$!a with a!$\rightarrow$!b refl
|
|
2
|
80 ... | ()
|
|
5
|
81 !$\equiv$!-Bool-func {false} {false} a!$\rightarrow$!b b!$\rightarrow$!a = refl
|
|
2
|
82
|
|
5
|
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
|
|
2
|
88
|
|
5
|
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
|
|
2
|
92
|
|
5
|
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 )
|
|
2
|
96
|
|
5
|
97 !$\neg$!-bool : {a : Bool} !$\rightarrow$! a !$\equiv$! false !$\rightarrow$! a !$\equiv$! true !$\rightarrow$! !$\bot$!
|
|
|
98 !$\neg$!-bool refl ()
|
|
2
|
99
|
|
5
|
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} ()
|
|
2
|
105
|
|
5
|
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} ()
|
|
2
|
111
|
|
5
|
112 bool-and-tt : {a b : Bool} !$\rightarrow$! a !$\equiv$! true !$\rightarrow$! b !$\equiv$! true !$\rightarrow$! ( a !$\wedge$! b ) !$\equiv$! true
|
|
2
|
113 bool-and-tt refl refl = refl
|
|
|
114
|
|
5
|
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} {_} ()
|
|
2
|
118
|
|
5
|
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} ()
|
|
2
|
123
|
|
5
|
124 bool-or-1 : {a b : Bool} !$\rightarrow$! a !$\equiv$! false !$\rightarrow$! ( a \/ b ) !$\equiv$! b
|
|
2
|
125 bool-or-1 {false} {true} refl = refl
|
|
|
126 bool-or-1 {false} {false} refl = refl
|
|
5
|
127 bool-or-2 : {a b : Bool} !$\rightarrow$! b !$\equiv$! false !$\rightarrow$! (a \/ b ) !$\equiv$! a
|
|
2
|
128 bool-or-2 {true} {false} refl = refl
|
|
|
129 bool-or-2 {false} {false} refl = refl
|
|
|
130
|
|
5
|
131 bool-or-3 : {a : Bool} !$\rightarrow$! ( a \/ true ) !$\equiv$! true
|
|
2
|
132 bool-or-3 {true} = refl
|
|
|
133 bool-or-3 {false} = refl
|
|
|
134
|
|
5
|
135 bool-or-31 : {a b : Bool} !$\rightarrow$! b !$\equiv$! true !$\rightarrow$! ( a \/ b ) !$\equiv$! true
|
|
2
|
136 bool-or-31 {true} {true} refl = refl
|
|
|
137 bool-or-31 {false} {true} refl = refl
|
|
|
138
|
|
5
|
139 bool-or-4 : {a : Bool} !$\rightarrow$! ( true \/ a ) !$\equiv$! true
|
|
2
|
140 bool-or-4 {true} = refl
|
|
|
141 bool-or-4 {false} = refl
|
|
|
142
|
|
5
|
143 bool-or-41 : {a b : Bool} !$\rightarrow$! a !$\equiv$! true !$\rightarrow$! ( a \/ b ) !$\equiv$! true
|
|
2
|
144 bool-or-41 {true} {b} refl = refl
|
|
|
145
|
|
5
|
146 bool-and-1 : {a b : Bool} !$\rightarrow$! a !$\equiv$! false !$\rightarrow$! (a !$\wedge$! b ) !$\equiv$! false
|
|
2
|
147 bool-and-1 {false} {b} refl = refl
|
|
5
|
148 bool-and-2 : {a b : Bool} !$\rightarrow$! b !$\equiv$! false !$\rightarrow$! (a !$\wedge$! b ) !$\equiv$! false
|
|
2
|
149 bool-and-2 {true} {false} refl = refl
|
|
|
150 bool-and-2 {false} {false} refl = refl
|
|
|
151
|
|
|
152
|
