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