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

diff -r a7364dfcc51e -r 1b54c0623d01 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Mon Nov 18 23:53:47 2019 +0900
+++ b/agda/finiteSet.agda	Tue Nov 19 00:25:43 2019 +0900
@@ -19,6 +19,14 @@
        found-q : Q
        found-p : p found-q ≡ true
 
+lt0 : (n : ℕ) →  n Data.Nat.≤ n
+lt0 zero = z≤n
+lt0 (suc n) = s≤s (lt0 n)
+lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
+lt2 {zero} lt = z≤n
+lt2 {suc m} {zero} ()
+lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
+
 record FiniteSet ( Q : Set ) { n : ℕ } : Set  where
      field
         Q←F : Fin n → Q
@@ -27,13 +35,6 @@
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
      finℕ : ℕ
      finℕ = n
-     lt0 : (n : ℕ) →  n Data.Nat.≤ n
-     lt0 zero = z≤n
-     lt0 (suc n) = s≤s (lt0 n)
-     lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
-     lt2 {zero} lt = z≤n
-     lt2 {suc m} {zero} ()
-     lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
      exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
      exists1  zero  _ _ = false
      exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
@@ -259,7 +260,19 @@
               ∎  where open ≡-Reasoning
 
 Func2List : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → ( Q → Bool ) → Vec Bool n
-Func2List = {!!}
+Func2List {Q} {n} fin Q→B = to-list Q→B where
+     list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Vec Bool m
+     list1  zero  _ _ = []
+     list1 ( suc m ) m<n p with bool-≡-? (p (FiniteSet.Q←F fin (fromℕ≤ {m} {n} m<n))) true
+     ... | yes _ = true ∷ list1 m (lt2 m<n) p
+     ... | no  _ = false ∷ list1 m (lt2 m<n) p
+     to-list : ( Q → Bool ) → Vec Bool n
+     to-list p = list1 n (lt0 n) p 
 
-List2Func : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → Vec Bool n → ( Q → Bool ) 
-List2Func = {!!}
+get : { Σ : Set  } {n : ℕ} →  (x : Vec Σ n ) → { i : ℕ } → i < n  → Σ
+get [] ()
+get (h ∷ t) {0} (s≤s lt) = h
+get (h ∷ t) {suc i} (s≤s lt) = get t lt
+
+List2Func : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → Vec Bool n →  Q → Bool 
+List2Func {Q} {n} fin x q = get (reverse x) (toℕ<n (FiniteSet.F←Q fin q ) )