|
52
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 module practice-logic where
|
|
|
3
|
|
|
4 postulate A : Set
|
|
|
5 postulate B : Set
|
|
|
6
|
|
53
|
7 postulate b : B
|
|
|
8
|
|
|
9 lemma0 : A -> B
|
|
141
|
10 lemma0 a = {!!}
|
|
53
|
11
|
|
|
12 id : { A : Set } → ( A → A )
|
|
|
13 id = {!!}
|
|
|
14
|
|
|
15 id' : { A : Set } → ( A → A )
|
|
|
16 id' x = {!!}
|
|
|
17
|
|
|
18 _・_ : {A B C : Set } → {!!}
|
|
|
19 f ・ g = λ x → f ( g x )
|
|
|
20
|
|
|
21
|
|
52
|
22 Lemma1 : Set
|
|
|
23 Lemma1 = A -> ( A -> B ) -> B
|
|
|
24
|
|
|
25 lemma1 : Lemma1
|
|
139
|
26 lemma1 a f = f a
|
|
52
|
27
|
|
|
28 -- lemma1 a a-b = a-b a
|
|
|
29
|
|
141
|
30 lemma2 : Lemma1 -- π
|
|
52
|
31 lemma2 = \a b -> {!!}
|
|
|
32
|
|
|
33 -- lemma1 = \a a-b -> a-b a
|
|
|
34 -- lemma1 = \a b -> b a
|
|
|
35 -- lemma1 a b = b a
|
|
|
36
|
|
|
37 lemma3 : Lemma1
|
|
|
38 lemma3 = \a -> ( \b -> {!!} )
|
|
|
39
|
|
|
40 record _∧_ (A B : Set) : Set where
|
|
141
|
41 constructor _,_
|
|
52
|
42 field
|
|
141
|
43 π1 : A
|
|
|
44 π2 : B
|
|
52
|
45
|
|
|
46 data _∧d_ ( A B : Set ) : Set where
|
|
|
47 and : A -> B -> A ∧d B
|
|
|
48
|
|
|
49 Lemma4 : Set
|
|
|
50 Lemma4 = B -> A -> (B ∧ A)
|
|
|
51 lemma4 : Lemma4
|
|
|
52 lemma4 = \b -> \a -> {!!}
|
|
|
53
|
|
|
54 Lemma5 : Set
|
|
|
55 Lemma5 = (A ∧ B) -> B
|
|
|
56
|
|
|
57 lemma5 : Lemma5
|
|
|
58 lemma5 = \a -> {!!}
|
|
|
59
|
|
|
60 data _∨_ (A B : Set) : Set where
|
|
141
|
61 case1 : A -> A ∨ B
|
|
|
62 case2 : B -> A ∨ B
|
|
52
|
63
|
|
|
64 Lemma6 : Set
|
|
|
65 Lemma6 = B -> ( A ∨ B )
|
|
|
66
|
|
|
67 lemma6 : Lemma6
|
|
55
|
68 lemma6 = \b -> {!!}
|
|
|
69
|
|
|
70 open _∧_
|
|
52
|
71
|
|
53
|
72 ex1 : {A B : Set} → ( A ∧ B ) → A
|
|
|
73 ex1 a∧b = {!!}
|
|
|
74
|
|
|
75 ex2 : {A B : Set} → ( A ∧ B ) → B
|
|
|
76 ex2 a∧b = {!!}
|
|
|
77
|
|
|
78 ex3 : {A B : Set} → A → B → ( A ∧ B )
|
|
|
79 ex3 a b = {!!}
|
|
|
80
|
|
55
|
81 ex4 : {A : Set} → A → ( A ∧ A )
|
|
141
|
82 ex4 a = record { π1 = {!!} ; π2 = {!!} }
|
|
53
|
83
|
|
|
84 ex5 : {A B C : Set} → ( A ∧ B ) ∧ C → A ∧ (B ∧ C)
|
|
55
|
85 ex5 a∧b∧c = {!!}
|
|
53
|
86
|
|
|
87 ex6 : {A B C : Set} → ( (A → B ) ∧ ( B → C) ) → A → C
|
|
55
|
88 ex6 p a = {!!}
|
|
53
|
89
|
|
|
90 ex7 : {A : Set} → ( A ∨ A ) → A
|
|
141
|
91 ex7 (case1 a) = a
|
|
|
92 ex7 (case2 a) = a
|
|
53
|
93
|
|
|
94 ex8 : {A B : Set} → B → ( A ∨ ( B → A ) ) → A
|
|
55
|
95 ex8 = {!!}
|
|
53
|
96
|
|
52
|
97 open import Relation.Nullary
|
|
|
98 open import Relation.Binary
|
|
|
99 open import Data.Empty
|
|
|
100
|
|
|
101 contra-position : {A : Set } {B : Set } → (A → B) → ¬ B → ¬ A
|
|
|
102 contra-position {A} {B} f ¬b a = {!!}
|
|
|
103
|
|
141
|
104 contra-position' : {A : Set } {B : Set } → (A → B) → (B → ⊥) → A → ⊥
|
|
|
105 contra-position' f ¬b a = {!!}
|
|
|
106
|
|
|
107 contra-position1 : {A : Set } {B : Set } → (B ∨ ( ¬ B )) → (¬ B → ¬ A )→ (A → B)
|
|
|
108 contra-position1 {A} {B} = {!!}
|
|
|
109
|
|
|
110 double-neg : {A : Set } → A → ¬ (¬ A)
|
|
|
111 double-neg = {!!}
|
|
55
|
112
|
|
141
|
113 double-neg' : {A : Set } → A → ( A → ⊥ ) → ⊥
|
|
|
114 double-neg' = {!!}
|
|
|
115
|
|
|
116 double-neg1 : {A : Set } → ¬ (¬ A) → A
|
|
|
117 double-neg1 x = {!!}
|
|
|
118
|
|
|
119 lem : {A : Set } → A ∨ ( ¬ A ) -- 排中律 law of exclude middle LEM
|
|
|
120 lem = {!!}
|
|
55
|
121
|
|
|
122 lemma : {A : Set } → A ∨ ( ¬ A ) → ¬ ¬ A → A
|
|
|
123 lemma = {!!}
|
|
52
|
124
|
|
|
125 double-neg2 : {A : Set } → ¬ ¬ ¬ A → ¬ A
|
|
|
126 double-neg2 = {!!}
|
|
|
127
|
|
141
|
128 de-mcasegan : {A B : Set } → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) )
|
|
|
129 de-mcasegan {A} {B} = {!!}
|
|
52
|
130
|
|
141
|
131 dont-case : {A : Set } { B : Set } → A ∨ B → ¬ A → B
|
|
|
132 dont-case {A} {B} = {!!}
|
|
52
|
133
|
|
|
134
|
