Mercurial > hg > Gears > GearsAgda
annotate logic.agda @ 949:057d3309ed9d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 04 Aug 2024 13:05:12 +0900 |
| parents | e5288029f850 |
| children | 5c75fc6dfe59 |
| rev | line source |
|---|---|
| 949 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 2 | |
| 579 | 3 module logic where |
| 4 | |
| 949 | 5 open import Level |
| 579 | 6 open import Relation.Nullary |
| 949 | 7 open import Relation.Binary hiding (_⇔_ ) |
| 579 | 8 open import Data.Empty |
| 9 | |
| 10 | |
| 11 data Bool : Set where | |
| 12 true : Bool | |
| 13 false : Bool | |
| 14 | |
| 15 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where | |
|
609
79418701a283
add test and speciication
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
604
diff
changeset
|
16 constructor ⟪_,_⟫ |
| 579 | 17 field |
| 18 proj1 : A | |
| 19 proj2 : B | |
| 20 | |
| 21 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where | |
| 22 case1 : A → A ∨ B | |
| 23 case2 : B → A ∨ B | |
| 24 | |
| 25 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m) | |
| 26 _⇔_ A B = ( A → B ) ∧ ( B → A ) | |
| 27 | |
| 28 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A | |
| 29 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) | |
| 30 | |
| 31 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A | |
| 32 double-neg A notnot = notnot A | |
| 33 | |
| 34 double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A | |
| 35 double-neg2 notnot A = notnot ( double-neg A ) | |
| 36 | |
| 37 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) ) | |
| 38 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and )) | |
| 39 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and )) | |
| 40 | |
| 41 dont-or : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B | |
| 42 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a ) | |
| 43 dont-or {A} {B} (case2 b) ¬A = b | |
| 44 | |
| 45 dont-orb : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A | |
| 46 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b ) | |
| 47 dont-orb {A} {B} (case1 a) ¬B = a | |
| 48 | |
| 49 infixr 130 _∧_ | |
| 50 infixr 140 _∨_ | |
| 51 infixr 150 _⇔_ | |
| 52 | |
| 949 | 53 _/\_ : Bool → Bool → Bool |
| 579 | 54 true /\ true = true |
| 55 _ /\ _ = false | |
| 56 | |
| 949 | 57 _\/_ : Bool → Bool → Bool |
| 579 | 58 false \/ false = false |
| 59 _ \/ _ = true | |
| 60 | |
| 949 | 61 not : Bool → Bool |
| 579 | 62 not true = false |
| 949 | 63 not false = true |
| 579 | 64 |
| 949 | 65 _<=>_ : Bool → Bool → Bool |
| 579 | 66 true <=> true = true |
| 67 false <=> false = true | |
| 68 _ <=> _ = false | |
| 69 | |
| 70 infixr 130 _\/_ | |
| 71 infixr 140 _/\_ | |
| 949 | 72 |
| 73 open import Relation.Binary.PropositionalEquality | |
| 74 | |
| 75 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where | |
| 76 field | |
| 77 fun← : S → R | |
| 78 fun→ : R → S | |
| 79 fiso← : (x : R) → fun← ( fun→ x ) ≡ x | |
| 80 fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x | |
| 81 | |
| 82 injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m) | |
| 83 injection R S f = (x y : R) → f x ≡ f y → x ≡ y | |
| 84 | |
| 85 | |
| 86 -- Cubical Agda has trouble with std-lib's Dec | |
| 87 -- we sometimes use simpler version of Dec | |
| 88 | |
| 89 data Dec0 {n : Level} (A : Set n) : Set n where | |
| 90 yes0 : A → Dec0 A | |
| 91 no0 : (A → ⊥) → Dec0 A | |
| 92 | |
| 93 open _∧_ | |
| 94 ∧-injective : {n m : Level} {A : Set n} {B : Set m} → {a b : A ∧ B} → proj1 a ≡ proj1 b → proj2 a ≡ proj2 b → a ≡ b | |
| 95 ∧-injective refl refl = refl | |
| 96 | |
| 97 not-not-bool : { b : Bool } → not (not b) ≡ b | |
| 98 not-not-bool {true} = refl | |
| 99 not-not-bool {false} = refl | |
| 100 | |
| 101 ¬t=f : (t : Bool ) → ¬ ( not t ≡ t) | |
| 102 ¬t=f true () | |
| 103 ¬t=f false () | |
| 104 | |
| 105 ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B | |
| 106 ≡-Bool-func {true} {true} a→b b→a = refl | |
| 107 ≡-Bool-func {false} {true} a→b b→a with b→a refl | |
| 108 ... | () | |
| 109 ≡-Bool-func {true} {false} a→b b→a with a→b refl | |
| 110 ... | () | |
| 111 ≡-Bool-func {false} {false} a→b b→a = refl | |
| 112 | |
| 113 bool-≡-? : (a b : Bool) → Dec0 ( a ≡ b ) | |
| 114 bool-≡-? true true = yes0 refl | |
| 115 bool-≡-? true false = no0 (λ ()) | |
| 116 bool-≡-? false true = no0 (λ ()) | |
| 117 bool-≡-? false false = yes0 refl | |
| 118 | |
| 119 ¬-bool-t : {a : Bool} → ¬ ( a ≡ true ) → a ≡ false | |
| 120 ¬-bool-t {true} ne = ⊥-elim ( ne refl ) | |
| 121 ¬-bool-t {false} ne = refl | |
| 122 | |
| 123 ¬-bool-f : {a : Bool} → ¬ ( a ≡ false ) → a ≡ true | |
| 124 ¬-bool-f {true} ne = refl | |
| 125 ¬-bool-f {false} ne = ⊥-elim ( ne refl ) | |
| 126 | |
| 127 ¬-bool : {a : Bool} → a ≡ false → a ≡ true → ⊥ | |
| 128 ¬-bool refl () | |
| 129 | |
| 130 lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥ | |
| 131 lemma-∧-0 {true} {false} () | |
| 132 lemma-∧-0 {false} {true} () | |
| 133 lemma-∧-0 {false} {false} () | |
| 134 lemma-∧-0 {true} {true} eq1 () | |
| 135 | |
| 136 lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥ | |
| 137 lemma-∧-1 {true} {false} () | |
| 138 lemma-∧-1 {false} {true} () | |
| 139 lemma-∧-1 {false} {false} () | |
| 140 lemma-∧-1 {true} {true} eq1 () | |
| 141 | |
| 142 bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true | |
| 143 bool-and-tt refl refl = refl | |
| 144 | |
| 145 bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true | |
| 146 bool-∧→tt-0 {true} {true} eq = refl | |
| 147 bool-∧→tt-0 {false} {_} () | |
| 148 | |
| 149 bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true | |
| 150 bool-∧→tt-1 {true} {true} eq = refl | |
| 151 bool-∧→tt-1 {true} {false} () | |
| 152 bool-∧→tt-1 {false} {false} () | |
| 153 | |
| 154 bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b | |
| 155 bool-or-1 {false} {true} eq = refl | |
| 156 bool-or-1 {false} {false} eq = refl | |
| 157 bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a | |
| 158 bool-or-2 {true} {false} eq = refl | |
| 159 bool-or-2 {false} {false} eq = refl | |
| 160 | |
| 161 bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true | |
| 162 bool-or-3 {true} = refl | |
| 163 bool-or-3 {false} = refl | |
| 164 | |
| 165 bool-or-31 : {a b : Bool} → b ≡ true → ( a \/ b ) ≡ true | |
| 166 bool-or-31 {true} {true} eq = refl | |
| 167 bool-or-31 {false} {true} eq = refl | |
| 168 | |
| 169 bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true | |
| 170 bool-or-4 {true} = refl | |
| 171 bool-or-4 {false} = refl | |
| 172 | |
| 173 bool-or-41 : {a b : Bool} → a ≡ true → ( a \/ b ) ≡ true | |
| 174 bool-or-41 {true} {b} eq = refl | |
| 175 | |
| 176 bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false | |
| 177 bool-and-1 {false} {b} eq = refl | |
| 178 bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false | |
| 179 bool-and-2 {true} {false} eq = refl | |
| 180 bool-and-2 {false} {false} eq = refl | |
| 181 bool-and-2 {true} {true} () | |
| 182 bool-and-2 {false} {true} () | |
| 183 | |
| 184 |