Mercurial > hg > Papers > 2022 > soto-sigos

comparison DPP/logic.agda @ 1:9f6cb9166d06

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
WIP dpp
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 01 May 2022 15:17:52 +0900
parents
children
comparison
equal deleted inserted replaced
0:14a0e409d574 1:9f6cb9166d06
1 module logic where
2
3 open import Level
4 open import Relation.Nullary
5 open import Relation.Binary hiding (_⇔_)
6 open import Relation.Binary.PropositionalEquality
7
8 open import Data.Empty
9 open import Data.Nat hiding (_⊔_)
10
11
12 data Bool : Set where
13 true : Bool
14 false : Bool
15
16 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
17 constructor ⟪_,_⟫
18 field
19 proj1 : A
20 proj2 : B
21
22 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
23 case1 : A → A ∨ B
24 case2 : B → A ∨ B
25
26 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m)
27 _⇔_ A B = ( A → B ) ∧ ( B → A )
28
29 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
30 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
31
32 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A
33 double-neg A notnot = notnot A
34
35 double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
36 double-neg2 notnot A = notnot ( double-neg A )
37
38 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) )
39 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
40 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
41
42 dont-or :　{n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B
43 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
44 dont-or {A} {B} (case2 b) ¬A = b
45
46 dont-orb :　{n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A
47 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
48 dont-orb {A} {B} (case1 a) ¬B = a
49
50
51 infixr 130 _∧_
52 infixr 140 _∨_
53 infixr 150 _⇔_
54
55 _/\_ : Bool → Bool → Bool
56 true /\ true = true
57 _ /\ _ = false
58
59 _<B?_ : ℕ → ℕ → Bool
60 ℕ.zero <B? x = true
61 ℕ.suc x <B? ℕ.zero = false
62 ℕ.suc x <B? ℕ.suc xx = x <B? xx
63
64 -- _<BT_ : ℕ → ℕ → Set
65 -- ℕ.zero <BT ℕ.zero = ⊤
66 -- ℕ.zero <BT ℕ.suc b = ⊤
67 -- ℕ.suc a <BT ℕ.zero = ⊥
68 -- ℕ.suc a <BT ℕ.suc b = a <BT b
69
70
71 _≟B_ : Decidable {A = Bool} _≡_
72 true ≟B true = yes refl
73 false ≟B false = yes refl
74 true ≟B false = no λ()
75 false ≟B true = no λ()
76
77 _\/_ : Bool → Bool → Bool
78 false \/ false = false
79 _ \/ _ = true
80
81 not_ : Bool → Bool
82 not true = false
83 not false = true
84
85 _<=>_ : Bool → Bool → Bool
86 true <=> true = true
87 false <=> false = true
88 _ <=> _ = false
89
90 infixr 130 _\/_
91 infixr 140 _/\_