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