# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574411712 -32400
# Node ID 0ee5c7f4627476c17fe2d92ac3d5ade065ec0ae2
# Parent  f7f0a994daef9df760958f994b4e517463b69a4b
clean up

diff -r f7f0a994daef -r 0ee5c7f46274 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Fri Nov 22 17:20:12 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 22 17:35:12 2019 +0900
@@ -294,9 +294,13 @@
         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 = []
-Func2List {Q} {suc n} {m} (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) ∷ Func2List {Q} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa ) fin Q→B
+F2L : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} ) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
+F2L  {Q} {zero} fin _ Q→B = []
+F2L  {Q} {suc n}  (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) lemma6 ∷ F2L {Q} {n} (Data.Nat.Properties.<-trans n<m a<sa ) fin qb1 where
+   lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))) < suc n
+   lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ≤ n<m ))  a<sa )
+   qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
+   qb1 q q<n = Q→B q (Data.Nat.Properties.<-trans q<n a<sa)
 
 List2Func : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → Vec Bool n →  Q → Bool 
 List2Func {Q} {zero} (s≤s z≤n) fin [] q = false
@@ -304,33 +308,17 @@
 ... | yes _ = h
 ... | 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 {Q} {m} fin x = trans (sym ( F2L=Func2List (List2Func a<sa fin x) a<sa )) (f2l m a<sa x) where
-    F2L : {n  : ℕ } → n < suc m → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
-    F2L  {zero} _ Q→B = []
-    F2L  {suc n}  (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) lemma6 ∷ F2L {n} (Data.Nat.Properties.<-trans n<m a<sa ) qb1 where
-       lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))) < suc n
-       lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ≤ n<m ))  a<sa )
-       qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
-       qb1 q q<n = Q→B q (Data.Nat.Properties.<-trans q<n a<sa)
-    F2L=Func2List : ( qb : Q → Bool )  → {n : ℕ } → ( n<m : n < suc m)  → F2L {n} n<m (λ q _ → qb q ) ≡ Func2List {Q} {n} n<m fin qb
-    F2L=Func2List qb {0} (s≤s z≤n) = refl
-    F2L=Func2List qb {suc n} (s≤s n<m) with qb (FiniteSet.Q←F fin (fromℕ≤ n<m))
-    ... | true = cong ( λ k → true ∷ k ) ( F2L=Func2List qb {n} (Data.Nat.Properties.<-trans n<m a<sa)  )
-    ... | false = cong ( λ k → false ∷ k ) ( F2L=Func2List qb {n} (Data.Nat.Properties.<-trans n<m a<sa)  )
-    L2F : {n : ℕ } → n < suc m → Vec Bool n → (q :  Q ) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool
-    L2F n<m x q q<n = List2Func n<m fin x q 
-    f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L  n<m (λ q q<n → L2F n<m x q q<n )  ≡ x 
+F2L-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (x : Vec Bool n ) → F2L a<sa fin (λ q _ → List2Func a<sa fin x q ) ≡ x
+F2L-iso {Q} {m} fin x = f2l m a<sa x where
+    f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L  n<m fin (λ q q<n → List2Func n<m fin x q )  ≡ x 
     f2l zero (s≤s z≤n) [] = refl
     f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3 where
-       lemma : FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m)) ≡  fromℕ≤ n<m
-       lemma = FiniteSet.finiso← fin _
        lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 →  h ∷ t ≡ h1 ∷ t1
        lemma1 refl refl = refl
        lemma2 : List2Func (s≤s n<m) fin (h ∷ t) (FiniteSet.Q←F fin (fromℕ≤ n<m)) ≡ h
        lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))  ≟ fromℕ≤ n<m
        lemma2 | yes p = refl
-       lemma2 | no ¬p = ⊥-elim ( ¬p lemma )
+       lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
        lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func (s≤s n<m) fin (h ∷ t) q ≡ List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q
        lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m 
        lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ≤ n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where 
@@ -338,22 +326,20 @@
            lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s  z≤n
            lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
        lemma4 q _ | no ¬p = refl
-       lemma3 :  F2L (Data.Nat.Properties.<-trans n<m a<sa) (λ q q<n → L2F (s≤s n<m) (h ∷ t) q (Data.Nat.Properties.<-trans q<n a<sa) ) ≡ t
+       lemma3 :  F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q  ) ≡ t
        lemma3 = begin 
-            F2L (Data.Nat.Properties.<-trans n<m a<sa) (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q )
-          ≡⟨ cong (λ k → F2L (Data.Nat.Properties.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
+            F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q )
+          ≡⟨ cong (λ k → F2L (Data.Nat.Properties.<-trans n<m a<sa) fin ( λ q q<n → k q q<n ))
                  (FiniteSet.f-extensionality fin ( λ q →  
                  (FiniteSet.f-extensionality fin ( λ q<n →  lemma4 q q<n )))) ⟩
-            F2L (Data.Nat.Properties.<-trans n<m a<sa) (λ q q<n → List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q )
-          ≡⟨⟩
-            F2L (Data.Nat.Properties.<-trans n<m a<sa) (L2F (Data.Nat.Properties.<-trans n<m a<sa) t) 
+            F2L (Data.Nat.Properties.<-trans n<m a<sa) fin (λ q q<n → List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q )
           ≡⟨ f2l n (Data.Nat.Properties.<-trans n<m a<sa ) t ⟩
             t
           ∎  where
             open ≡-Reasoning
 
-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 : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (List2Func a<sa fin (F2L a<sa fin (λ q _ → f q) )) q ≡ f q
 L2F-iso {Q} {m} fin f q = l2f m a<sa where
-    l2f :  (n : ℕ ) → (n<m : n < suc m )→  (List2Func n<m fin (Func2List n<m fin f )) q ≡ f q
-    l2f zero (s≤s z≤n) = {!!}
+    l2f :  (n : ℕ ) → (n<m : n < suc m )→  (List2Func n<m fin (F2L n<m  fin (λ q _ → f q))) q ≡ f q
+    l2f zero (s≤s z≤n) = ?
     l2f (suc n) n<m = {!!}