Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/agda/halt.agda @ 182:567754463810

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganization
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Jun 2021 18:48:57 +0900
parents agda/halt.agda@4c5d26c149fa
children
comparison
equal deleted inserted replaced
181:9c63284d7695 182:567754463810
1 module halt where
2
3 open import Level renaming ( zero to Zero ; suc to Suc )
4 open import Data.Nat
5 open import Data.Maybe
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
11 open import Relation.Binary.Core hiding (_⇔_)
12 open import Relation.Binary.Definitions
13 open import Relation.Binary.PropositionalEquality
14
15 open import logic
16
17 record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
18 field
19 fun← : S → R
20 fun→ : R → S
21 fiso← : (x : R) → fun← ( fun→ x ) ≡ x
22 -- normal bijection required below, but we don't need this to show the inconsistency
23 -- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x
24
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
27
28 open HBijection
29
30 diag : {S : Set } (b : HBijection ( S → Bool ) S) → S → Bool
31 diag b n = not (fun← b n n)
32
33 diagonal : { S : Set } → ¬ HBijection ( S → Bool ) S
34 diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
35 diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n )
36 diagn1 n dn = ¬t=f (diag b n ) ( begin
37 not (diag b n)
38 ≡⟨⟩
39 not (not fun← b n n)
40 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩
41 not (fun← b (fun→ b (diag b)) n)
42 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
43 not (fun← b n n)
44 ≡⟨⟩
45 diag b n
46 ∎ ) where open ≡-Reasoning
47
48 record TM : Set where
49 field
50 tm : List Bool → Maybe Bool
51
52 open TM
53
54 record UTM : Set where
55 field
56 utm : TM
57 encode : TM → List Bool
58 is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x
59
60 open UTM
61
62 open _∧_
63
64 open import Axiom.Extensionality.Propositional
65 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n
66
67 record Halt : Set where
68 field
69 halt : (t : TM ) → (x : List Bool ) → Bool
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 )
72
73 open Halt
74
75 TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
76 TNL halt utm = record {
77 fun← = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
78 ; fun→ = λ h → encode utm record { tm = h1 h }
79 ; fiso← = λ h → f-extensionality (λ y → TN1 h y )
80 } where
81 open ≡-Reasoning
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
86 tenc : (h : List Bool → Bool) → (y : List Bool) → List Bool
87 tenc h y = encode utm (record { tm = λ x → h1 h x }) ++ y
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
94 TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y
95 TN1 h y with h y | inspect h y
96 ... | true | record { eq = eq1 } = begin
97 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩
98 true ∎ where
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 ⟩
102 h1 h y ≡⟨ h-just h y eq1 ⟩
103 just true ∎
104 ... | false | record { eq = eq1 } = begin
105 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩
106 false ∎ where
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 ⟩
110 h1 h y ≡⟨ h-nothing h y eq1 ⟩
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
114