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