Mercurial > hg > Members > kono > Proof > automaton

changeset 178:27dbee9c292c

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, 17 Mar 2021 10:24:49 +0900
parents 375e1dcba6aa
children f226c21d61bf
files agda/halt.agda agda/regular-concat.agda
diffstat 2 files changed, 15 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/agda/halt.agda	Tue Mar 16 14:02:45 2021 +0900
+++ b/agda/halt.agda	Wed Mar 17 10:24:49 2021 +0900
@@ -82,13 +82,19 @@
 TNL : (halt : Halt ) → (utm : UTM) → HaltIsTM halt utm → HBijection (List Bool → Bool) (List Bool)
 TNL halt utm halt-is-tm = record {
        fun←  = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
-     ; fun→  = λ h  → encode utm record { tm = λ x → just (h x) } 
-     ; fiso← = TN1
+     ; fun→  = λ h  → encode utm record { tm = h1 h } 
+     ; fiso← = λ h →  f-extensionality (λ y → TN1 h y )
   } where
-     TN1 :  (h : List Bool → Bool) → (λ y → Halt.halt halt (UTM.utm utm) (encode utm (record { tm = λ x → just (h x) }) ++ y)) ≡ h
-     TN1 h =  f-extensionality (λ y →
-        Halt.halt halt (UTM.utm utm)  (encode utm (record { tm = λ x → just (h x) }) ++ y) ≡⟨ {!!} ⟩
-        h y ∎ ) where open ≡-Reasoning
+     h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool
+     h1 h x with h x
+     ... | true =  just true
+     ... | false = nothing
+     TN1 :  (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (encode utm (record { tm = h1 h }) ++ y) ≡ h y
+     TN1 h y with h y | inspect h y
+     ... | true  | record { eq = eq1 } = {!!}
+     ... | false | record { eq = eq1 } = begin
+        Halt.halt halt (UTM.utm utm)  (encode utm (record { tm = λ x → h1 h x }) ++ y) ≡⟨ {!!} ⟩
+        false ∎  where open ≡-Reasoning
 
 
 -- TNℕ : (halt : Halt ) → (utm : UTM) → HaltIsTM halt utm → HBijection (TM → Bool) TM
--- a/agda/regular-concat.agda	Tue Mar 16 14:02:45 2021 +0900
+++ b/agda/regular-concat.agda	Wed Mar 17 10:24:49 2021 +0900
@@ -153,8 +153,8 @@
     abmove (case1 q) h = case1 (δ (automaton A) q h)
     abmove (case2 q) h = case2 (δ (automaton B) q h)
     lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true
-    lemma-nmove-ab (case1 q) _ = equal?-refl (afin A)
-    lemma-nmove-ab (case2 q) _ = equal?-refl (afin B)
+    lemma-nmove-ab (case1 q) _ = ? -- equal?-refl (afin A)
+    lemma-nmove-ab (case2 q) _ = ? -- equal?-refl (afin B)
     nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
        exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
     nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )  
@@ -180,7 +180,7 @@
     acceptAB : Split (contain A) (contain B) x
         → Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true
     acceptAB S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
-        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) )
+        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) ? (prop0 S) (prop1 S) )
 
     closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
     closed-in-concat→ concat with split→AB (contain A) (contain B) x concat