Mercurial > hg > Members > Moririn
comparison logic.agda @ 579:821d04c0770b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 02 Nov 2019 17:34:46 +0900 |
| parents | |
| children | 0ddfa505d612 |
comparison
equal
deleted
inserted
replaced
| 578:7bacba816277 | 579:821d04c0770b |
|---|---|
| 1 module logic where | |
| 2 | |
| 3 open import Level | |
| 4 open import Relation.Nullary | |
| 5 open import Relation.Binary | |
| 6 open import Data.Empty | |
| 7 | |
| 8 | |
| 9 data Bool : Set where | |
| 10 true : Bool | |
| 11 false : Bool | |
| 12 | |
| 13 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where | |
| 14 field | |
| 15 proj1 : A | |
| 16 proj2 : B | |
| 17 | |
| 18 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where | |
| 19 case1 : A → A ∨ B | |
| 20 case2 : B → A ∨ B | |
| 21 | |
| 22 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m) | |
| 23 _⇔_ A B = ( A → B ) ∧ ( B → A ) | |
| 24 | |
| 25 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A | |
| 26 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) | |
| 27 | |
| 28 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A | |
| 29 double-neg A notnot = notnot A | |
| 30 | |
| 31 double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A | |
| 32 double-neg2 notnot A = notnot ( double-neg A ) | |
| 33 | |
| 34 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) ) | |
| 35 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and )) | |
| 36 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and )) | |
| 37 | |
| 38 dont-or : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B | |
| 39 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a ) | |
| 40 dont-or {A} {B} (case2 b) ¬A = b | |
| 41 | |
| 42 dont-orb : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A | |
| 43 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b ) | |
| 44 dont-orb {A} {B} (case1 a) ¬B = a | |
| 45 | |
| 46 | |
| 47 infixr 130 _∧_ | |
| 48 infixr 140 _∨_ | |
| 49 infixr 150 _⇔_ | |
| 50 | |
| 51 _/\_ : Bool → Bool → Bool | |
| 52 true /\ true = true | |
| 53 _ /\ _ = false | |
| 54 | |
| 55 _\/_ : Bool → Bool → Bool | |
| 56 false \/ false = false | |
| 57 _ \/ _ = true | |
| 58 | |
| 59 not_ : Bool → Bool | |
| 60 not true = false | |
| 61 not false = true | |
| 62 | |
| 63 _<=>_ : Bool → Bool → Bool | |
| 64 true <=> true = true | |
| 65 false <=> false = true | |
| 66 _ <=> _ = false | |
| 67 | |
| 68 infixr 130 _\/_ | |
| 69 infixr 140 _/\_ |