Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/halt.agda @ 319:cd91a9f313dd
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 12 Jan 2022 21:20:16 +0900 |
| parents | 3fa72793620b |
| children | 6f3636fbc481 |
| rev | line source |
|---|---|
| 141 | 1 module halt where |
| 2 | |
| 3 open import Level renaming ( zero to Zero ; suc to Suc ) | |
| 4 open import Data.Nat | |
| 142 | 5 open import Data.Maybe |
| 141 | 6 open import Data.List hiding ([_]) |
| 7 open import Data.Nat.Properties | |
| 8 open import Relation.Nullary | |
| 9 open import Data.Empty | |
| 10 open import Data.Unit | |
| 142 | 11 open import Relation.Binary.Core hiding (_⇔_) |
| 141 | 12 open import Relation.Binary.Definitions |
| 13 open import Relation.Binary.PropositionalEquality | |
| 14 | |
| 15 open import logic | |
| 16 | |
| 176 | 17 record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where |
| 141 | 18 field |
| 19 fun← : S → R | |
| 20 fun→ : R → S | |
| 21 fiso← : (x : R) → fun← ( fun→ x ) ≡ x | |
| 176 | 22 -- normal bijection required below, but we don't need this to show the inconsistency |
| 23 -- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x | |
| 141 | 24 |
| 319 | 25 injection' : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m) |
| 26 injection' R S f = (x y : R) → f x ≡ f y → x ≡ y | |
| 164 | 27 |
| 176 | 28 open HBijection |
| 141 | 29 |
| 176 | 30 diag : {S : Set } (b : HBijection ( S → Bool ) S) → S → Bool |
| 164 | 31 diag b n = not (fun← b n n) |
| 32 | |
| 176 | 33 diagonal : { S : Set } → ¬ HBijection ( S → Bool ) S |
| 174 | 34 diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where |
| 35 diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) | |
| 164 | 36 diagn1 n dn = ¬t=f (diag b n ) ( begin |
| 37 not (diag b n) | |
| 141 | 38 ≡⟨⟩ |
| 39 not (not fun← b n n) | |
| 40 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩ | |
| 164 | 41 not (fun← b (fun→ b (diag b)) n) |
| 141 | 42 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩ |
| 43 not (fun← b n n) | |
| 44 ≡⟨⟩ | |
| 164 | 45 diag b n |
| 141 | 46 ∎ ) where open ≡-Reasoning |
| 47 | |
| 164 | 48 record TM : Set where |
| 49 field | |
| 50 tm : List Bool → Maybe Bool | |
| 51 | |
| 52 open TM | |
| 53 | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
54 record UTM : Set where |
| 164 | 55 field |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
56 utm : TM |
|
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
57 encode : TM → List Bool |
|
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
58 is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x |
| 164 | 59 |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
60 open UTM |
| 164 | 61 |
| 141 | 62 open _∧_ |
| 173 | 63 |
| 141 | 64 open import Axiom.Extensionality.Propositional |
| 65 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n | |
| 66 | |
| 142 | 67 record Halt : Set where |
| 68 field | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
69 halt : (t : TM ) → (x : List Bool ) → Bool |
| 179 | 70 is-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ true ) ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) ) |
| 71 is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x ) | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
72 |
| 142 | 73 open Halt |
| 74 | |
| 180 | 75 TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool) |
| 76 TNL halt utm = record { | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
77 fun← = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x) |
| 178 | 78 ; fun→ = λ h → encode utm record { tm = h1 h } |
| 79 ; fiso← = λ h → f-extensionality (λ y → TN1 h y ) | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
80 } where |
| 180 | 81 open ≡-Reasoning |
| 178 | 82 h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool |
| 83 h1 h x with h x | |
| 84 ... | true = just true | |
| 85 ... | false = nothing | |
| 180 | 86 tenc : (h : List Bool → Bool) → (y : List Bool) → List Bool |
| 87 tenc h y = encode utm (record { tm = λ x → h1 h x }) ++ y | |
| 179 | 88 h-nothing : (h : List Bool → Bool) → (y : List Bool) → h y ≡ false → h1 h y ≡ nothing |
| 89 h-nothing h y eq with h y | |
| 90 h-nothing h y refl | false = refl | |
| 91 h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true | |
| 92 h-just h y eq with h y | |
| 93 h-just h y refl | true = refl | |
| 180 | 94 TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y |
| 178 | 95 TN1 h y with h y | inspect h y |
| 179 | 96 ... | true | record { eq = eq1 } = begin |
| 180 | 97 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩ |
| 179 | 98 true ∎ where |
| 180 | 99 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ just true |
| 100 tm-tenc = begin | |
| 101 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩ | |
| 179 | 102 h1 h y ≡⟨ h-just h y eq1 ⟩ |
| 180 | 103 just true ∎ |
| 178 | 104 ... | false | record { eq = eq1 } = begin |
| 180 | 105 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩ |
| 179 | 106 false ∎ where |
| 180 | 107 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ nothing |
| 108 tm-tenc = begin | |
| 109 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩ | |
| 179 | 110 h1 h y ≡⟨ h-nothing h y eq1 ⟩ |
| 180 | 111 nothing ∎ |
| 112 -- the rest of bijection means encoding is unique | |
| 113 -- fiso→ : (y : List Bool ) → encode utm record { tm = λ x → h1 (λ tm → Halt.halt halt (UTM.utm utm) tm ) x } ≡ y | |
| 179 | 114 |
| 319 | 115 TNL1 : UTM → ¬ Halt |
| 116 TNL1 utm halt = diagonal ( TNL halt utm ) |