Mercurial > hg > Members > kono > Proof > automaton

comparison agda/halt.agda @ 174:0e87089e5de4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
..`
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Mar 2021 15:31:56 +0900
parents 6835096cfa3a
children bf50676c77af
comparison
equal deleted inserted replaced
173:6835096cfa3a 174:0e87089e5de4
40 b→injection1 : {n m : Level} (R : Set n) (S : Set m) → (b : Bijection R S) → injection S R (fun← b) 40 b→injection1 : {n m : Level} (R : Set n) (S : Set m) → (b : Bijection R S) → injection S R (fun← b)
41 b→injection1 R S b x y eq = trans ( sym ( fiso→ b x ) ) (trans ( cong (λ k → fun→ b k ) eq ) ( fiso→ b y )) 41 b→injection1 R S b x y eq = trans ( sym ( fiso→ b x ) ) (trans ( cong (λ k → fun→ b k ) eq ) ( fiso→ b y ))
42 42
43 -- ¬ A = A → ⊥ 43 -- ¬ A = A → ⊥
44 44
45 diag : (b : Bijection ( ℕ → Bool ) ℕ) → ℕ → Bool 45 diag : {S : Set } (b : Bijection ( S → Bool ) S) → S → Bool
46 diag b n = not (fun← b n n) 46 diag b n = not (fun← b n n)
47 47
48 diagonal : ¬ Bijection ( ℕ → Bool ) ℕ 48 diagonal : { S : Set } → ¬ Bijection ( S → Bool ) S
49 diagonal b = diagn1 (fun→ b (diag b) ) refl where 49 diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
50 diagn1 : (n : ℕ ) → ¬ (fun→ b (diag b) ≡ n ) 50 diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n )
51 diagn1 n dn = ¬t=f (diag b n ) ( begin 51 diagn1 n dn = ¬t=f (diag b n ) ( begin
52 not (diag b n) 52 not (diag b n)
53 ≡⟨⟩ 53 ≡⟨⟩
54 not (not fun← b n n) 54 not (not fun← b n n)
55 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩ 55 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩
170 ... | ⟪ proj3 , false ⟫ = refl 170 ... | ⟪ proj3 , false ⟫ = refl
171 lbisor : (x : List Bool) → ntol (lton x) ≡ x 171 lbisor : (x : List Bool) → ntol (lton x) ≡ x
172 lbisor [] = refl 172 lbisor [] = refl
173 lbisor (false ∷ []) = refl 173 lbisor (false ∷ []) = refl
174 lbisor (true ∷ []) = refl 174 lbisor (true ∷ []) = refl
175 lbisor (false ∷ true ∷ t) = ? 175 lbisor (false ∷ true ∷ t) = {!!}
176 lbisor (false ∷ false ∷ t) = ? 176 lbisor (false ∷ false ∷ t) = {!!}
177 lbisor (true ∷ x ∷ t) = {!!} 177 lbisor (true ∷ x ∷ t) = {!!}
178 178
179 179
180 open import Axiom.Extensionality.Propositional 180 open import Axiom.Extensionality.Propositional
181 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n 181 postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n
202 } where 202 } where
203 tmb1 : (x : TM ) → record { tm = utm (encode x) ; encode = encode x ; is-tm = refl } ≡ x 203 tmb1 : (x : TM ) → record { tm = utm (encode x) ; encode = encode x ; is-tm = refl } ≡ x
204 tmb1 x with is-tm x | inspect is-tm x 204 tmb1 x with is-tm x | inspect is-tm x
205 ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl 205 ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
206 206
207 TNℕ : Bijection TM ℕ 207 TNℕ : Halt → Bijection (TM → Bool) TM
208 TNℕ = {!!} 208 TNℕ = {!!}
209 209
210 -- Halt1 (Halt2 x) ≡ x 210 -- Halt1 (Halt2 x) ≡ x
211 -- Halt2 (Halt2 y) ≡ y 211 -- Halt2 (Halt2 y) ≡ y
212 212