Mercurial > hg > Members > kono > Proof > category
annotate src/negnat.agda @ 1124:f683d96fbc93 default tip
safe fix done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jul 2024 22:28:50 +0900 |
| parents | ac53803b3b2a |
| children |
| rev | line source |
|---|---|
| 1124 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 451 | 2 module negnat where |
| 3 | |
| 4 | |
| 5 open import Data.Nat | |
| 1124 | 6 open import Relation.Nullary hiding (proof) |
| 451 | 7 open import Data.Empty |
| 8 open import Data.Unit | |
| 9 open import Data.Fin renaming ( suc to fsuc ; zero to fzero ; _+_ to _++_ ) | |
| 10 open import Relation.Binary.Core | |
| 1124 | 11 open import Relation.Binary.PropositionalEquality hiding (J) |
| 451 | 12 |
| 13 | |
| 14 -- http://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda | |
| 15 | |
| 16 | |
| 17 ℕ-elim : ∀ {p} (P : ℕ → Set p) | |
| 18 (s : ∀ {n} → P n → P (suc n)) | |
| 19 (z : P 0) → ∀ n → P n | |
| 20 ℕ-elim P s z zero = z | |
| 21 ℕ-elim P s z (suc n) = s (ℕ-elim P s z n) | |
| 22 | |
| 452 | 23 -- data ⊥ : Set where |
| 24 | |
| 25 -- record ⊤ : Set where | |
| 26 -- constructor tt | |
| 27 | |
| 451 | 28 -- peano : ∀ n → suc n ≡ zero → ⊥ |
| 29 | |
| 30 Nope : (m n : ℕ) → Set | |
| 31 Nope (suc _) zero = ⊥ | |
| 32 Nope _ _ = ⊤ | |
| 33 | |
| 34 nope : ∀ m n → m ≡ n → Nope m n | |
| 35 nope zero ._ refl = _ | |
| 36 nope (suc m) ._ refl = _ | |
| 37 | |
| 38 peano : ∀ n → suc n ≡ zero → ⊥ | |
| 39 peano _ p = nope _ _ p | |
| 40 | |
| 41 | |
| 42 J : ∀ {a p} {A : Set a} (P : ∀ (x : A) y → x ≡ y → Set p) | |
| 43 (f : ∀ x → P x x refl) → ∀ x y → (p : x ≡ y) → P x y p | |
| 44 J P f x .x refl = f x | |
| 45 | |
| 46 Fin-elim : ∀ {p} (P : ∀ n → Fin n → Set p) | |
| 47 (s : ∀ {n} {fn : Fin n} → P n fn → P (suc n) (fsuc fn)) | |
| 48 (z : ∀ {n} → P (suc n) fzero) → | |
| 49 ∀ {n} (fn : Fin n) → P n fn | |
| 50 Fin-elim P s z fzero = z | |
| 51 Fin-elim P s z (fsuc x) = s (Fin-elim P s z x) | |
| 52 | |
| 452 | 53 Nope1 : ℕ -> Set |
| 54 Nope1 zero = ⊥ | |
| 55 Nope1 (suc _) = ⊤ | |
| 451 | 56 |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
57 Nope0 : ℕ → Set |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
58 Nope0 = ℕ-elim (λ _ → Set) (λ _ → ⊤) ⊥ |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
59 |
| 451 | 60 bad : Fin 0 → ⊥ |
| 61 bad = Fin-elim (λ n _ → Nope0 n) (λ _ → _) _ | |
| 62 | |
| 63 | |
| 64 -- http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type | |
| 65 even : ℕ -> Set | |
| 66 even zero = ⊤ | |
| 67 even (suc zero) = ⊥ | |
| 68 even (suc (suc n)) = even n | |
| 69 | |
| 70 div : (n : ℕ) -> even n -> ℕ | |
| 71 div zero p = zero | |
| 72 div (suc (suc n)) p = suc (div n p) | |
| 73 div (suc zero) () | |
| 74 | |
| 452 | 75 proof : 2 + 3 ≡ suc (suc (suc (suc (suc zero)))) |
| 451 | 76 proof = refl |
| 77 | |
| 78 -- | |
| 79 -- ¬_ : Set → Set | |
| 80 -- ¬ A = A → ⊥ | |
| 81 -- | |
| 82 -- data Dec (P : Set) : Set where | |
| 83 -- yes : P → Dec P | |
| 84 -- no : ¬ P → Dec P | |
| 85 | |
| 86 EvenDecidable : Set | |
| 87 EvenDecidable = ∀ n → Dec (even n) | |
| 88 | |
| 89 isEven : EvenDecidable | |
| 90 isEven zero = yes _ | |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
91 isEven (suc zero) = no (λ ()) |
| 451 | 92 isEven (suc (suc n)) = isEven n |
| 93 | |
| 94 data Bool : Set where | |
| 95 true false : Bool | |
| 96 | |
| 97 if_then_else_ : {A : Set} → Bool → A → A → A | |
| 98 if true then t else _ = t | |
| 99 if false then _ else f = f | |
| 100 | |
| 101 ⌊_⌋ : {P : Set} → Dec P → Bool | |
| 102 ⌊ yes _ ⌋ = true | |
| 103 ⌊ no _ ⌋ = false | |
| 104 | |
| 105 bad1 : ∀ n → even n → even (suc n) → ⊥ | |
| 106 bad1 zero p q = q | |
| 107 bad1 (suc zero) p q = p | |
| 108 bad1 (suc (suc n)) p q = bad1 n p q | |
| 109 | |
| 110 odd : ∀ n → ¬ even n → even (suc n) | |
| 111 odd zero p = p _ | |
| 112 odd (suc zero) p = _ | |
| 113 odd (suc (suc n)) p = odd n p | |
| 114 | |
| 115 g : ℕ → ℕ | |
| 116 g n with isEven n | |
| 117 ... | yes e = div n e | |
| 118 ... | no o = div (suc n) (odd n o) | |
| 119 | |
| 120 -- g-bad : ℕ → ℕ | |
| 121 -- g-bad n = if ⌊ isEven n ⌋ | |
| 122 -- then (div n {!!}) | |
| 123 -- else (div (suc n) (odd n {!!})) | |
| 124 | |
| 125 | |
| 126 if-dec_then_else_ : {P A : Set} → Dec P → (P → A) → (¬ P → A) → A | |
| 127 if-dec yes p then t else _ = t p | |
| 128 if-dec no ¬p then _ else f = f ¬p | |
| 129 | |
| 130 g' : ℕ → ℕ | |
| 131 g' n = if-dec isEven n | |
| 132 then (λ e → div n e) | |
| 133 else (λ o → div (suc n) (odd n o)) | |
| 134 | |
| 135 if-syntax = if-dec_then_else_ | |
| 136 | |
| 137 syntax if-syntax dec (λ yup → yupCase) (λ nope → nopeCase) | |
| 138 = if-dec dec then[ yup ] yupCase else[ nope ] nopeCase | |
| 139 | |
| 140 g'' : ℕ → ℕ | |
| 141 g'' n = if-dec isEven n | |
| 142 then[ e ] div n e | |
| 143 else[ o ] div (suc n) (odd n o) | |
| 144 | |
| 145 | |
| 146 mod : ℕ -> ℕ | |
| 147 mod zero = zero | |
| 148 mod (suc zero) = suc zero | |
| 149 mod (suc (suc N)) = mod N | |
| 150 | |
| 151 proof1 : (n : ℕ ) -> ( if ⌊ isEven n ⌋ then zero else (suc zero) ) ≡ ( mod n ) | |
| 152 proof1 zero = refl | |
| 153 proof1 (suc zero) = refl | |
| 154 proof1 (suc (suc n)) = let open ≡-Reasoning in | |
| 155 begin | |
| 156 if ⌊ isEven (suc (suc n)) ⌋ then zero else suc zero | |
| 157 ≡⟨ cong ( \x -> (if ⌊ x ⌋ then zero else suc zero)) (lemma2 {n} )⟩ | |
| 158 if ⌊ isEven n ⌋ then zero else suc zero | |
| 159 ≡⟨ proof1 n ⟩ | |
| 160 mod n | |
| 161 ≡⟨ sym (lemma1 {n}) ⟩ | |
| 162 mod (suc (suc n)) | |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
163 ∎ where |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
164 lemma1 : { n : ℕ } -> mod (suc (suc n )) ≡ mod n |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
165 lemma1 = refl |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
166 lemma2 : { n : ℕ } -> isEven (suc (suc n )) ≡ isEven n |
|
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
167 lemma2 = refl |
| 451 | 168 |
|
822
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
169 data One : Set where |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
170 * : One |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
171 |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
172 lemma1 : ( x y : One ) → x ≡ y |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
173 lemma1 * * = refl |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
174 |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
175 lemma2 : {A : Set} ( x : A) → x ≡ x |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
176 lemma2 x = refl |
| 451 | 177 |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
178 |
|
822
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
179 open import Data.Empty |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
180 open import Relation.Nullary |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
181 open import Level |
|
453
3c2ce4474d92
try incomplete pattern for discrete
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
452
diff
changeset
|
182 |
|
822
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
183 lemma4 : Set (Level.suc Level.zero) |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
184 lemma4 = {A : Set} ( x y : A) → ¬ ( ¬ x ≡ y ) |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
185 |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
186 data A : Set where |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
187 x y z : A |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
188 |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
189 data _==_ : ( a b : A ) → Set where |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
190 x=y : x == y |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
191 |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
192 lemma3 : ( a b : A ) → a == b → ¬ a ≡ b |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
193 lemma3 _ _ x=y = λ () |
|
4c0580d9dda4
from cart to graph, hom equality to set equality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
454
diff
changeset
|
194 |