|
52
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 module practice-logic where
|
|
|
3
|
|
|
4 postulate A : Set
|
|
|
5 postulate B : Set
|
|
|
6
|
|
|
7 Lemma1 : Set
|
|
|
8 Lemma1 = A -> ( A -> B ) -> B
|
|
|
9
|
|
|
10 lemma1 : Lemma1
|
|
|
11 lemma1 a b = {!!}
|
|
|
12
|
|
|
13 -- lemma1 a a-b = a-b a
|
|
|
14
|
|
|
15 lemma2 : Lemma1
|
|
|
16 lemma2 = \a b -> {!!}
|
|
|
17
|
|
|
18 -- lemma1 = \a a-b -> a-b a
|
|
|
19 -- lemma1 = \a b -> b a
|
|
|
20 -- lemma1 a b = b a
|
|
|
21
|
|
|
22 lemma3 : Lemma1
|
|
|
23 lemma3 = \a -> ( \b -> {!!} )
|
|
|
24
|
|
|
25 record _∧_ (A B : Set) : Set where
|
|
|
26 field
|
|
|
27 and1 : A
|
|
|
28 and2 : B
|
|
|
29
|
|
|
30 data _∧d_ ( A B : Set ) : Set where
|
|
|
31 and : A -> B -> A ∧d B
|
|
|
32
|
|
|
33 Lemma4 : Set
|
|
|
34 Lemma4 = B -> A -> (B ∧ A)
|
|
|
35
|
|
|
36 lemma4 : Lemma4
|
|
|
37 lemma4 = \b -> \a -> {!!}
|
|
|
38
|
|
|
39 Lemma5 : Set
|
|
|
40 Lemma5 = (A ∧ B) -> B
|
|
|
41
|
|
|
42 lemma5 : Lemma5
|
|
|
43 lemma5 = \a -> {!!}
|
|
|
44
|
|
|
45 data _∨_ (A B : Set) : Set where
|
|
|
46 or1 : A -> A ∨ B
|
|
|
47 or2 : B -> A ∨ B
|
|
|
48
|
|
|
49 Lemma6 : Set
|
|
|
50 Lemma6 = B -> ( A ∨ B )
|
|
|
51
|
|
|
52 lemma6 : Lemma6
|
|
|
53 lemma6 = \b -> {!!}
|
|
|
54
|
|
|
55 open import Relation.Nullary
|
|
|
56 open import Relation.Binary
|
|
|
57 open import Data.Empty
|
|
|
58
|
|
|
59 contra-position : {A : Set } {B : Set } → (A → B) → ¬ B → ¬ A
|
|
|
60 contra-position {A} {B} f ¬b a = {!!}
|
|
|
61
|
|
|
62 double-neg : {A : Set } → A → ¬ ¬ A
|
|
|
63 double-neg = {!!}
|
|
|
64
|
|
|
65 double-neg2 : {A : Set } → ¬ ¬ ¬ A → ¬ A
|
|
|
66 double-neg2 = {!!}
|
|
|
67
|
|
|
68 de-morgan : {A B : Set } → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) )
|
|
|
69 de-morgan {A} {B} = {!!}
|
|
|
70
|
|
|
71 dont-or : {A : Set } { B : Set } → A ∨ B → ¬ A → B
|
|
|
72 dont-or {A} {B} = {!!}
|
|
|
73
|
|
|
74
|
