# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574247090 -32400
# Node ID eddc4ad8e99a5b03c457761bb8d3ceeb474033b1
# Parent  37c919cec9acdba3a3dd764346f97a216c767b2c
...

diff -r 37c919cec9ac -r eddc4ad8e99a agda/finiteSet.agda
--- a/agda/finiteSet.agda	Wed Nov 20 13:34:34 2019 +0900
+++ b/agda/finiteSet.agda	Wed Nov 20 19:51:30 2019 +0900
@@ -130,6 +130,81 @@
      not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
      not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) )
 
+record ISO (A B : Set) : Set where
+   field
+       A←B : B → A
+       B←A : A → B
+       iso← : (q : A) → A←B ( B←A q ) ≡ q
+       iso→ : (f : B) → B←A ( A←B f ) ≡ f
+
+iso-fin : {A B : Set} → {n : ℕ } → FiniteSet A {n} → ISO A B → FiniteSet B {n}
+iso-fin {A} {B} {n} fin iso = record {
+        Q←F = λ f → ISO.B←A iso ( FiniteSet.Q←F fin f )
+      ; F←Q = λ b → FiniteSet.F←Q fin ( ISO.A←B iso b )
+      ; finiso→ = finiso→ 
+      ; finiso← = finiso← 
+   } where
+        finiso→ : (q : B) → ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) ≡ q
+        finiso→ q = begin
+                   ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) 
+                ≡⟨ cong (λ k → ISO.B←A iso k ) (FiniteSet.finiso→ fin _ ) ⟩
+                   ISO.B←A iso (ISO.A←B iso q)
+                ≡⟨ ISO.iso→ iso _ ⟩
+                   q
+                ∎  where
+                open ≡-Reasoning
+        finiso← : (f : Fin n) → FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) ≡ f
+        finiso← f = begin
+                   FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) 
+                ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (ISO.iso← iso _) ⟩
+                   FiniteSet.F←Q fin (FiniteSet.Q←F fin f) 
+                ≡⟨ FiniteSet.finiso← fin _  ⟩
+                   f
+                ∎  where
+                open ≡-Reasoning
+
+
+fin-∨2 : {B : Set} → { a b : ℕ } → FiniteSet B {b} → FiniteSet (Fin a ∨ B) {a Data.Nat.+ b}
+fin-∨2 {B} {zero} {b} fb = iso-fin fb iso where
+   iso : ISO B (Fin zero ∨ B)
+   iso =  record {
+          A←B = A←B
+        ; B←A = λ b → case2 b
+        ; iso→ = iso→
+        ; iso← = λ _ → refl
+      } where
+          A←B : Fin zero ∨ B → B
+          A←B (case2 x) = x 
+          iso→ : (f : Fin zero ∨ B ) → case2 (A←B f) ≡ f
+          iso→ (case2 x)  = refl
+fin-∨2 {B} {suc a} {b} fb =  record {
+        Q←F = Q←F
+      ; F←Q = F←Q
+      ; finiso→ = {!!} -- finiso→
+      ; finiso← = {!!} -- finiso←
+   } where
+       fin : FiniteSet (Fin a ∨ B) {a Data.Nat.+ b}
+       fin = fin-∨2 fb
+       Q←F : Fin (suc a Data.Nat.+ b) → Fin (suc a) ∨ B
+       Q←F f with  Data.Nat.Properties.<-cmp (toℕ f) (a Data.Nat.+ b)
+       Q←F f | tri≈ _ eq ¬c = case1 (fromℕ a)
+       Q←F f | tri> ¬a ¬b c = ⊥-elim (nat-≤> c (toℕ<n f) )
+       Q←F f | tri< lt ¬b ¬c  with FiniteSet.Q←F fin ( fromℕ≤ lt )
+       ... | case1 x = case1 (raise 1 x)
+       ... | case2 b = case2 b
+       F←Q : Fin (suc a) ∨ B → Fin (suc a Data.Nat.+ b)
+       F←Q (case1 f) = inject+ b f
+       F←Q (case2 b) = raise 1 (FiniteSet.F←Q fin (case2 b) )
+       finiso→ : (q : Fin (suc a) ∨ B) → Q←F (F←Q q) ≡ q
+       finiso→ (case1 f ) with Data.Nat.Properties.<-cmp (toℕ f) (a Data.Nat.+ b)
+       finiso→ (case1 f ) | tri≈ _ eq ¬c = {!!} -- case1 (fromℕ a)
+       finiso→ (case1 f ) | tri> ¬a ¬b c = ⊥-elim (nat-≤> c {!!} ) -- (toℕ<n f) )
+       finiso→ (case1 f ) | tri< lt ¬b ¬c  with FiniteSet.Q←F fin ( fromℕ≤ lt )
+       ... | case1 x = {!!} -- case1 (raise 1 x)
+       ... | case2 b = {!!} -- case2 b
+       finiso→ (case2 b ) = {!!}
+
+
 fin-∨' : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a Data.Nat.+ b}
 fin-∨' {A} {B} {a} {b} fa fb = record {
         Q←F = Q←F  
diff -r 37c919cec9ac -r eddc4ad8e99a agda/flcagl.agda
--- a/agda/flcagl.agda	Wed Nov 20 13:34:34 2019 +0900
+++ b/agda/flcagl.agda	Wed Nov 20 19:51:30 2019 +0900
@@ -471,6 +471,10 @@
 Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x ))
 Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) 
 
+nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
+Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa  {!!}
+Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) 
+
 -- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i
 -- Lang.ν (nlang' nfa s) = DA.ν nfa  s
 -- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a)