Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/halt.agda @ 408:3d0aa205edf9

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 Wed, 15 Nov 2023 16:24:07 +0900
parents c7ad8d2dc157
children b85402051cdb
comparison
equal deleted inserted replaced
407:c7ad8d2dc157 408:3d0aa205edf9
14 open import Relation.Binary.Definitions 14 open import Relation.Binary.Definitions
15 open import Relation.Binary.PropositionalEquality 15 open import Relation.Binary.PropositionalEquality
16 16
17 open import logic 17 open import logic
18 18
19 --
20 -- (R → Bool) <-> S
21 --
19 record FBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where 22 record FBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
20 field 23 field
21 ffun← : S → R → Bool 24 ffun← : S → R → Bool
22 ffun→ : (R → Bool) → S 25 ffun→ : (R → Bool) → S
23 ffiso← : (f : R → Bool ) → (x : R) → ffun← ( ffun→ f ) x ≡ f x 26 ffiso← : (f : R → Bool ) → (x : R) → ffun← ( ffun→ f ) x ≡ f x
24 27
25 -- ffun← ( ffun→ f ) ≡ f , if we have functional extensionality but it is unsafe 28 -- ffun← ( ffun→ f ) ≡ f , if we have functional extensionality but it is unsafe
26 29
27 open FBijection 30 open FBijection
28 31
32 -- S <-> S → Bool
33 --
34 -- S 0 1 2 3 ....
35 -- 0 t f t f ....
36 -- 1 t f t f ....
37 -- 2 t f t f ....
38 -- 3 t t t t .....
39 -- ..
40 -- counter exmpple
41 -- f t f f ...
42
29 fdiag : {S : Set } (b : FBijection S S) → S → Bool 43 fdiag : {S : Set } (b : FBijection S S) → S → Bool
30 fdiag b n = not (ffun← b n n) 44 fdiag b n = not (ffun← b n n)
31 45
32 -- 46 --
33 -- ffun→ b (fiag b) is some S 47 -- ffun→ b (fiag b) is some S
34 -- ffun← b (ffun→ b (fdiag b) ) is a function S → Bool 48 -- ffun← b (ffun→ b (fdiag b) ) is a function S → Bool
35 -- is pointwise equal to fdiag b , which means not (ffun← b (ffun→ b (fdiag b) ) x ≡ (fdiag b) x ) 49 -- is pointwise equal to fdiag b , which means not (ffun← b (ffun→ b (fdiag b) ) x ≡ (fdiag b) x )
36 -- but is also means not (fdiag b) x ≡ (fdiag b) x , contradiction 50 -- but is also means not (fdiag b) x ≡ (fdiag b) x , contradiction
37 51
52 -- ¬ (S → Bool) <-> S
53 --
38 fdiagonal : { S : Set } → ¬ FBijection S S 54 fdiagonal : { S : Set } → ¬ FBijection S S
39 fdiagonal {S} b = ¬t=f _ (trans ff4 (sym (ff3 _) ) ) where 55 fdiagonal {S} b = ¬t=f _ (trans ff4 (sym (ff3 _) ) ) where
40 ff1 : S 56 ff1 : S
41 ff1 = ffun→ b (fdiag b) 57 ff1 = ffun→ b (fdiag b)
42 ff2 : S → Bool 58 ff2 : S → Bool