# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574128235 -32400
# Node ID a8b55fbca18d2d8a957f4538f16c59a81c160252
# Parent  1b54c0623d01f046b092b7be58b01ee0c235b223
...

diff -r 1b54c0623d01 -r a8b55fbca18d agda/finiteSet.agda
--- a/agda/finiteSet.agda	Tue Nov 19 00:25:43 2019 +0900
+++ b/agda/finiteSet.agda	Tue Nov 19 10:50:35 2019 +0900
@@ -141,19 +141,31 @@
         n = a Data.Nat.+ b
         Q : Set 
         Q = A ∨ B
-        f-a : ∀{i} → (f : Fin i ) → (a : ℕ ) → toℕ f > a  → toℕ f < a Data.Nat.+ b  → Fin b
-        f-a {i} 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 : ∀{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
         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
-            a<a+b : toℕ f ≡ a → a < a Data.Nat.+ b 
-            a<a+b 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
         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)
@@ -164,14 +176,41 @@
         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 = {!!}
+            lemma11 = subst ( λ k → inject+ b k ≡ f ) (sym (FiniteSet.finiso← fa _) ) lemma14 
         finiso← f | tri≈ ¬a eq ¬c = lemma12 where
-            lemma12 : raise a (FiniteSet.F←Q fb (FiniteSet.Q←F fb (fromℕ≤  {!!} ))) ≡ f
-            lemma12 = {!!}
+            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 = {!!}
+            lemma13 = subst ( λ k → raise a k ≡ f ) (sym (FiniteSet.finiso← fb _) ) (lemma16 f c )
 
 import Data.Nat.DivMod
 import Data.Nat.Properties
@@ -259,6 +298,31 @@
                   f
               ∎  where open ≡-Reasoning
 
+record FiniteSubSet ( Q : Set ) ( n m : ℕ ) : Set  where
+     field
+        n<m : n < suc m
+        finite : FiniteSet Q {m}
+        Q←F : Fin n → Q
+        F←Q : Q → Fin n
+        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
+        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+
+finiteSubSetN :  { Q : Set } → {n  : ℕ } → FiniteSet Q {n} → FiniteSubSet Q n n 
+finiteSubSetN = {!!}
+
+finiteSubSet-1 :  { Q : Set } → {n m : ℕ } → FiniteSubSet Q (suc n) m → FiniteSubSet Q n m 
+finiteSubSet-1 = {!!}
+
+Func2List' : { Q : Set } → {n m : ℕ } → FiniteSubSet Q  n m → ( Q → Bool ) → Vec Bool n
+Func2List' {Q} {zero} fin Q→B = []
+Func2List' {Q} {suc n} {m} fin Q→B = Q→B (FiniteSubSet.Q←F fin (fromℕ≤ (a<sa {n})))  ∷ Func2List' {Q} {n} {m} (finiteSubSet-1 fin ) Q→B
+
+List2Func' : { Q : Set } → {n m : ℕ } → FiniteSubSet Q n m → Vec Bool n →  Q → Bool 
+List2Func' {Q} {zero}  fin [] q = false
+List2Func' {Q} {suc n} {m} fin (h ∷ t) q with  FiniteSubSet.F←Q fin q ≟ fromℕ≤ (a<sa {n})
+... | yes _ = h
+... | no _ = List2Func' {Q} {n} {m} (finiteSubSet-1 fin) t q
+
 Func2List : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → ( Q → Bool ) → Vec Bool n
 Func2List {Q} {n} fin Q→B = to-list Q→B where
      list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Vec Bool m