|
431
|
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 data One {n : Level } : Set n where
|
|
|
9 OneObj : One
|
|
|
10
|
|
|
11 data Two : Set where
|
|
|
12 i0 : Two
|
|
|
13 i1 : Two
|
|
|
14
|
|
|
15 data Bool : Set where
|
|
|
16 true : Bool
|
|
|
17 false : Bool
|
|
|
18
|
|
|
19 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
|
|
|
20 constructor ⟪_,_⟫
|
|
|
21 field
|
|
|
22 proj1 : A
|
|
|
23 proj2 : B
|
|
|
24
|
|
|
25 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
|
|
|
26 case1 : A → A ∨ B
|
|
|
27 case2 : B → A ∨ B
|
|
|
28
|
|
|
29 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m)
|
|
|
30 _⇔_ A B = ( A → B ) ∧ ( B → A )
|
|
|
31
|
|
|
32 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
|
|
|
33 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
|
|
|
34
|
|
|
35 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A
|
|
|
36 double-neg A notnot = notnot A
|
|
|
37
|
|
|
38 double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
|
|
|
39 double-neg2 notnot A = notnot ( double-neg A )
|
|
|
40
|
|
|
41 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) )
|
|
|
42 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
|
|
|
43 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
|
|
|
44
|
|
|
45 dont-or : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B
|
|
|
46 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
|
|
|
47 dont-or {A} {B} (case2 b) ¬A = b
|
|
|
48
|
|
|
49 dont-orb : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A
|
|
|
50 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
|
|
|
51 dont-orb {A} {B} (case1 a) ¬B = a
|
|
|
52
|
|
1174
|
53 open import Relation.Binary.PropositionalEquality
|
|
|
54
|
|
|
55 ¬i0≡i1 : ¬ ( i0 ≡ i1 )
|
|
|
56 ¬i0≡i1 ()
|
|
|
57
|
|
|
58 ¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1
|
|
|
59 ¬i0→i1 {i0} ne = ⊥-elim ( ne refl )
|
|
|
60 ¬i0→i1 {i1} ne = refl
|
|
|
61
|
|
|
62 ¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0
|
|
|
63 ¬i1→i0 {i0} ne = refl
|
|
|
64 ¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
|
|
|
65
|
|
431
|
66
|
|
|
67 infixr 130 _∧_
|
|
|
68 infixr 140 _∨_
|
|
|
69 infixr 150 _⇔_
|
|
|
70
|
