Mercurial > hg > Members > kono > Proof > automaton

changeset 120:481691ffc710

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
finite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 20 Nov 2019 22:31:54 +0900
parents eddc4ad8e99a
children ee43fecd3f34
files agda/finiteSet.agda
diffstat 1 files changed, 75 insertions(+), 188 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Wed Nov 20 19:51:30 2019 +0900
+++ b/agda/finiteSet.agda	Wed Nov 20 22:31:54 2019 +0900
@@ -163,9 +163,32 @@
                 ∎  where
                 open ≡-Reasoning
 
+data One : Set where
+   one : One
 
-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
+fin-∨1 : {B : Set} → { b : ℕ } → FiniteSet B {b} → FiniteSet (One ∨ B) {suc b}
+fin-∨1 {B} {b} fb =  record {
+        Q←F = Q←F
+      ; F←Q =  F←Q
+      ; finiso→ = finiso→
+      ; finiso← = finiso←
+   }  where
+        Q←F : Fin (suc b) → One ∨ B
+        Q←F zero = case1 one
+        Q←F (suc f) = case2 (FiniteSet.Q←F fb f)
+        F←Q : One ∨ B → Fin (suc b)
+        F←Q (case1 one) = zero
+        F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) 
+        finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q
+        finiso→ (case1 one) = refl
+        finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b)
+        finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q
+        finiso← zero = refl
+        finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f)
+
+
+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
@@ -177,162 +200,44 @@
           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-∨2 {B} (suc a) {b} fb =  iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
+    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 = fin-∨2 a fb
+       iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B)
+       ISO.A←B iso (case1 zero) = case1 one
+       ISO.A←B iso (case1 (suc f)) = case2 (case1 f)
+       ISO.A←B iso (case2 b) = case2 (case2 b)
+       ISO.B←A iso (case1 one) = case1 zero
+       ISO.B←A iso (case2 (case1 f)) = case1 (suc f)
+       ISO.B←A iso (case2 (case2 b)) = case2 b
+       ISO.iso← iso (case1 one) = refl
+       ISO.iso← iso (case2 (case1 x)) = refl
+       ISO.iso← iso (case2 (case2 x)) = refl
+       ISO.iso→ iso (case1 zero) = refl
+       ISO.iso→ iso (case1 (suc x)) = refl
+       ISO.iso→ iso (case2 x) = refl
 
 
+FiniteSet→Fin : {A : Set} → { a : ℕ } → (fin : FiniteSet A {a} ) → ISO (Fin a) A
+ISO.A←B (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f
+ISO.B←A (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f
+ISO.iso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin
+ISO.iso→ (FiniteSet→Fin fin) =  FiniteSet.finiso→ fin
+   
+
 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  
-      ; F←Q =  F←Q  
-      ; finiso→ = finiso→ 
-      ; finiso← = finiso← 
-   } where
-        n : ℕ
-        n = a Data.Nat.+ b
-        Q : Set 
-        Q = A ∨ B
-        f-a : ∀{i b} → (f : Fin i ) → (a : ℕ ) → toℕ f > a  → toℕ f < a Data.Nat.+ b  → Fin b
-        f-a {i} {b} f zero lt lt2 = fromℕ≤ lt2 
-        f-a {suc i} {_} (suc f) (suc a) (s≤s lt) (s≤s lt2) = f-a f a lt lt2
-        f-a zero (suc x) () _
-        a<a+b :  {f : Fin n} → toℕ f ≡ a → a < a Data.Nat.+ b 
-        a<a+b  {f} eq = subst (λ k → k < a Data.Nat.+ b) eq ( toℕ<n f )
-        0<b : (a : ℕ ) → a < a Data.Nat.+ b  → 0 < b
-        0<b zero a<a+b = a<a+b
-        0<b (suc a) (s≤s a<a+b) = 0<b a a<a+b
-        lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ≤ (s≤s lt) ≡ suc (fromℕ≤ lt)
-        lemma3 (s≤s lt) = refl
-        lemma4 : {i : ℕ } → { f : Fin i} → fromℕ≤ (toℕ<n f) ≡ f
-        lemma4 {suc _} {zero} = refl
-        lemma4 {suc i} {suc f} = begin
-                   fromℕ≤ (toℕ<n (suc f))
-                ≡⟨ lemma3 _ ⟩
-                   suc (fromℕ≤ (toℕ<n f))
-                ≡⟨ cong (λ k → suc k ) (lemma4 {i} {f}) ⟩
-                   suc f
-                ∎  where
-                open ≡-Reasoning
-        lemma6 : {a b : ℕ } → {f : Fin a} → toℕ (inject+ b f) ≡ toℕ f
-        lemma6 {suc a} {b} {zero} = refl
-        lemma6 {suc a} {b} {suc f} = cong (λ k → suc k ) (lemma6 {a} {b} {f})
-        lemmaa : {a b c : ℕ } → {b<a : b <  a } → {c<a : c <  a} → b ≡ c → fromℕ≤ b<a ≡  fromℕ≤ c<a
-        lemmaa {suc a} {zero} {zero} {s≤s z≤n} {s≤s z≤n} refl = refl
-        lemmaa {suc a} {suc b} {suc b} {s≤s b<a} {s≤s c<a} refl = subst₂ ( λ j k → j ≡ k ) (sym (lemma3 _ )) (sym (lemma3 _ )) 
-           (cong (λ k → suc k ) ( lemmaa {a} {b} {b} {b<a} {c<a} refl ))
-        Q←F : Fin n → Q
-        Q←F f with Data.Nat.Properties.<-cmp (toℕ f) a
-        Q←F f | tri< lt ¬b ¬c = case1 (FiniteSet.Q←F fa (fromℕ≤ lt )) 
-        Q←F f | tri≈ ¬a eq ¬c = case2 (FiniteSet.Q←F fb (fromℕ≤ (0<b a (a<a+b eq ) ))) where
-        Q←F f | tri> ¬a ¬b c = case2 (FiniteSet.Q←F fb (f-a f a c (toℕ<n f) ))
-        F←Q : Q → Fin n
-        F←Q (case1 qa) = inject+ b (FiniteSet.F←Q fa qa)
-        F←Q (case2 qb) = raise a (FiniteSet.F←Q fb qb)
-        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
-        finiso→ (case1 qa) = lemma7 where
-            lemma5 : toℕ (inject+ b (FiniteSet.F←Q fa qa)) < a 
-            lemma5 = subst (λ k → k < a ) (sym lemma6) (toℕ<n (FiniteSet.F←Q fa qa))
-            lemma7 : Q←F (F←Q (case1 qa)) ≡ case1 qa
-            lemma7 with Data.Nat.Properties.<-cmp (toℕ (inject+ b (FiniteSet.F←Q fa qa))) a
-            lemma7 | tri< lt ¬b ¬c = begin
-                   case1 (FiniteSet.Q←F fa (fromℕ≤ lt ))
-                ≡⟨ cong (λ k → case1 (FiniteSet.Q←F fa k )) (lemmaa lemma6 ) ⟩
-                   case1 (FiniteSet.Q←F fa (fromℕ≤ (toℕ<n (FiniteSet.F←Q fa qa)) ))
-                ≡⟨ cong (λ k → case1 (FiniteSet.Q←F fa k )) lemma4 ⟩
-                   case1 (FiniteSet.Q←F fa (FiniteSet.F←Q fa qa) )
-                ≡⟨ cong (λ k → case1 k ) (FiniteSet.finiso→ fa _ ) ⟩
-                   case1 qa
-                ∎  where open ≡-Reasoning
-            lemma7 | tri≈ ¬a b ¬c = ⊥-elim ( ¬a lemma5 )
-            lemma7 | tri> ¬a ¬b c = ⊥-elim ( ¬a lemma5 )
-        finiso→ (case2 qb) = lemma9 where
-            lemmab : toℕ (raise a (FiniteSet.F←Q fb qb)) > a
-            lemmab = {!!}
-            lemmac : (f : Fin b) (f>a : toℕ (raise a f) > a ) → f-a (raise a f) a f>a (toℕ<n (raise a f)) ≡ f 
-            lemmac = {!!}
-            lemmad : {qb : B } → 0 ≡ toℕ (FiniteSet.F←Q fb qb)
-            lemmad = {!!}
-            lemma9 :  Q←F (F←Q (case2 qb)) ≡ case2 qb
-            lemma9 with Data.Nat.Properties.<-cmp (toℕ (raise a (FiniteSet.F←Q fb qb))) a
-            lemma9 | tri< a ¬b ¬c = ⊥-elim ( ¬c lemmab )
-            lemma9 | tri≈ ¬a eq ¬c = begin
-                    case2 (FiniteSet.Q←F fb (fromℕ≤ (0<b a (a<a+b eq ) )))
-                 ≡⟨ cong (λ k → case2 (FiniteSet.Q←F fb k )) (lemmaa lemmad ) ⟩
-                    case2 (FiniteSet.Q←F fb (fromℕ≤ (toℕ<n (FiniteSet.F←Q fb qb))))
-                 ≡⟨  cong (λ k → case2 (FiniteSet.Q←F fb k )) lemma4  ⟩
-                    case2 (FiniteSet.Q←F fb (FiniteSet.F←Q fb qb)) 
-                 ≡⟨ cong (λ k → case2 k ) (FiniteSet.finiso→ fb _ ) ⟩
-                    case2 qb
-                 ∎  where open ≡-Reasoning
-            lemma9 | tri> ¬a ¬b c = begin
-                    case2 (FiniteSet.Q←F fb (f-a (raise a (FiniteSet.F←Q fb qb)) a c (toℕ<n (raise a (FiniteSet.F←Q fb qb)) ) ))
-                 ≡⟨ cong (λ k → case2 (FiniteSet.Q←F fb k) ) (lemmac (FiniteSet.F←Q fb qb) c ) ⟩
-                    case2 (FiniteSet.Q←F fb (FiniteSet.F←Q fb qb)) 
-                 ≡⟨ cong (λ k → case2 k ) (FiniteSet.finiso→ fb _ ) ⟩
-                    case2 qb
-                 ∎  where open ≡-Reasoning
-        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
-        finiso← f with Data.Nat.Properties.<-cmp (toℕ f) a
-        finiso← f | tri< lt ¬b ¬c = lemma11 where
-            lemma14 : { a b : ℕ } { f : Fin ( a Data.Nat.+ b) } { lt : (toℕ f) < a } → inject+ b (fromℕ≤ lt ) ≡ f
-            lemma14 {suc a} {b} {zero} {s≤s z≤n} = refl
-            lemma14 {suc a} {b} {suc f} {s≤s lt} = begin
-                   inject+ b (fromℕ≤ (s≤s lt))
-                ≡⟨ cong (λ k → inject+ b k ) (lemma3 lt ) ⟩
-                   inject+ b (suc (fromℕ≤ lt))
-                ≡⟨⟩
-                   suc (inject+ b (fromℕ≤ lt))
-                ≡⟨ cong (λ k → suc k) (lemma14 {a} {b} {f} {lt} ) ⟩
-                   suc f
-                ∎  where
-                open ≡-Reasoning
-            lemma11 : inject+ b (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ lt ) )) ≡ f
-            lemma11 = subst ( λ k → inject+ b k ≡ f ) (sym (FiniteSet.finiso← fa _) ) lemma14 
-        finiso← f | tri≈ ¬a eq ¬c = lemma12 where
-            lemma15 : {a b : ℕ } ( f : Fin ( a Data.Nat.+ b) ) ( eq : (toℕ f) ≡ a ) → (0<b : zero < b )  → raise a (fromℕ≤ 0<b) ≡ f
-            lemma15 {zero} {suc b} zero refl (s≤s z≤n) = refl
-            lemma15 {suc a} {suc b} (suc f) eq (s≤s z≤n) = cong (λ k → suc k ) ( lemma15 {a} {suc b} f (cong (λ k → Data.Nat.pred k) eq) (s≤s z≤n))
-            lemma12 : raise a (FiniteSet.F←Q fb (FiniteSet.Q←F fb (fromℕ≤  (0<b a (a<a+b eq ))))) ≡ f
-            lemma12 = subst ( λ k → raise a k ≡ f ) (sym (FiniteSet.finiso← fb _) ) (lemma15  f eq (0<b a (a<a+b eq )))
-        finiso← f | tri> ¬a ¬b c = lemma13  where
-            lemma16 : {a b : ℕ } (f : Fin (a Data.Nat.+ b)) → (lt : toℕ f > a ) → raise a (f-a f a lt (toℕ<n f)) ≡ f
-            lemma16 {zero} {b} (suc f) (s≤s z≤n) = lemma17 where
-                 lemma17 : fromℕ≤ (s≤s (toℕ<n f)) ≡ suc f
-                 lemma17 = begin
-                    fromℕ≤ (s≤s (toℕ<n f)) 
-                  ≡⟨ lemma3 _ ⟩
-                    suc ( fromℕ≤ (toℕ<n f) )
-                  ≡⟨ cong (λ k → suc k) lemma4 ⟩
-                    suc f
-                  ∎  where
-                  open ≡-Reasoning
-            lemma16 {suc a} {b} (suc f) (s≤s lt) = cong ( λ k → suc k ) (lemma16 {a} {b} f lt)
-            lemma13 : raise a (FiniteSet.F←Q fb ((FiniteSet.Q←F fb (f-a f a c (toℕ<n f))))) ≡ f
-            lemma13 = subst ( λ k → raise a k ≡ f ) (sym (FiniteSet.finiso← fb _) ) (lemma16 f c )
+fin-∨' {A} {B} {a} {b} fa fb = iso-fin (fin-∨2 a fb ) iso2 where
+    ia = FiniteSet→Fin fa
+    iso2 : ISO (Fin a ∨ B ) (A ∨ B)
+    ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x )
+    ISO.A←B iso2 (case2 x) = case2 x
+    ISO.B←A iso2 (case1 x) = case1 ( ISO.B←A ia x )
+    ISO.B←A iso2 (case2 x) = case2 x
+    ISO.iso← iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso← ia x)
+    ISO.iso← iso2 (case2 x) = refl
+    ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x)
+    ISO.iso→ iso2 (case2 x) = refl
 
 import Data.Nat.DivMod
 import Data.Nat.Properties
@@ -374,14 +279,8 @@
         finiso→ [] = refl
         finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f
         finiso← zero = refl
-fin2List {suc n} = record {
-        Q←F = Q←F
-      ; F←Q =  F←Q
-      ; finiso→ = finiso→ 
-      ; finiso← = finiso←
-   } where
-        Q : Set 
-        Q = Vec Bool (suc  n)
+fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) {k} ) (sym (exp2 n)) ( iso-fin (fin-∨' (fin2List {n}) (fin2List {n})) iso )
+    where
         QtoR : Vec Bool (suc  n) →  Vec Bool n ∨ Vec Bool n
         QtoR ( true ∷ x ) = case1 x
         QtoR ( false ∷ x ) = case2 x
@@ -394,31 +293,8 @@
         isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x
         isoQR (case1 x) = refl
         isoQR (case2 x) = refl
-        fin∨ = fin-∨' (fin2List {n}) (fin2List {n})
-        Q←F : Fin (exp 2 (suc n)) → Q
-        Q←F f = RtoQ ( FiniteSet.Q←F fin∨ (cast (exp2 n) f ))
-        F←Q : Q → Fin (exp 2 (suc n))
-        F←Q q = cast (sym (exp2 n)) ( FiniteSet.F←Q fin∨ ( QtoR q ) )
-        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
-        finiso→ q = begin
-                  RtoQ ( FiniteSet.Q←F fin∨ (cast (exp2 n) (cast (sym (exp2 n)) ( FiniteSet.F←Q fin∨ (QtoR q)  )) ))
-              ≡⟨ cong (λ k →  RtoQ ( FiniteSet.Q←F fin∨ k)) (cast-iso (exp2 n) _ ) ⟩
-                  RtoQ ( FiniteSet.Q←F fin∨ ( FiniteSet.F←Q fin∨ (QtoR q) ))
-              ≡⟨  cong ( λ k → RtoQ k ) ( FiniteSet.finiso→ fin∨ _ ) ⟩
-                  RtoQ (QtoR _) 
-              ≡⟨ isoRQ q ⟩
-                  q
-              ∎  where open ≡-Reasoning
-        finiso← : (f : Fin (exp 2 (suc n) ))  → F←Q ( Q←F f ) ≡ f
-        finiso← f = begin
-                  cast _ (FiniteSet.F←Q fin∨ (QtoR (RtoQ (FiniteSet.Q←F fin∨ (cast _ f )) ) ))
-              ≡⟨ cong (λ k → cast (sym (exp2 n)) (FiniteSet.F←Q fin∨  k )) (isoQR (FiniteSet.Q←F fin∨ (cast _ f)))  ⟩
-                  cast (sym (exp2 n))  (FiniteSet.F←Q fin∨ (FiniteSet.Q←F fin∨ (cast (exp2 n) f )))
-              ≡⟨ cong (λ k → cast (sym (exp2 n)) k ) ( FiniteSet.finiso← fin∨ _ ) ⟩
-                  cast _ (cast (exp2 n) f )
-              ≡⟨ cast-iso (sym (exp2 n)) _ ⟩
-                  f
-              ∎  where open ≡-Reasoning
+        iso : ISO (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n))
+        iso = record { A←B = QtoR ; B←A = RtoQ ; iso← = isoQR ; iso→ = isoRQ  }
 
 Func2List : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → ( Q → Bool ) → Vec Bool n
 Func2List {Q} {zero} _ fin Q→B = []
@@ -431,7 +307,18 @@
 ... | no _ = List2Func {Q} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa ) fin t q
 
 F2L-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (x : Vec Bool n ) → Func2List a<sa fin (List2Func a<sa fin x ) ≡ x
-F2L-iso = {!!}
+F2L-iso {Q} {m} fin x = f2l m a<sa x where
+    f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → Func2List n<m fin (List2Func n<m fin x ) ≡ x
+    f2l zero (s≤s z≤n) [] = refl
+    f2l (suc n) (s≤s n<m) (h ∷ t ) with FiniteSet.F←Q fin {!!} ≟ fromℕ≤ n<m
+    ... | yes _ = {!!}
+    ... | no _ = begin
+            Func2List (s≤s n<m) fin (List2Func (s≤s n<m) fin (h ∷ t) )
+       ≡⟨ {!!} ⟩
+            h ∷ t
+       ∎  where open ≡-Reasoning
+    -- with f2l n (Data.Nat.Properties.<-trans n<m a<sa) t 
+    -- ... | tail = {!!}
 
 L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (List2Func a<sa fin (Func2List a<sa fin f )) q ≡ f q
 L2F-iso = {!!}