annotate agda/logic.agda @ 89:e919e82e95a2

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