annotate logic.agda @ 387:8b0715e28b33

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 Jul 2020 09:09:00 +0900
parents 22d435172d1a
children 44a484f17f26
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module logic where
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Relation.Nullary
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Relation.Binary
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.Empty
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
387
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
8 data One {n : Level } : Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
9 OneObj : One
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
10
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
11 data Two : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
12 i0 : Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
13 i1 : Two
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 data Bool : Set where
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 true : Bool
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 false : Bool
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 field
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 proj1 : A
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 proj2 : B
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 case1 : A → A ∨ B
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 case2 : B → A ∨ B
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m)
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 _⇔_ A B = ( A → B ) ∧ ( B → A )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 double-neg A notnot = notnot A
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 double-neg2 notnot A = notnot ( double-neg A )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 dont-or : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 dont-or {A} {B} (case2 b) ¬A = b
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 dont-orb : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 dont-orb {A} {B} (case1 a) ¬B = a
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 infixr 130 _∧_
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 infixr 140 _∨_
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 infixr 150 _⇔_
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56