# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574088827 -32400
# Node ID a7364dfcc51ed8a7a507723bdf82148faa928fe4
# Parent  58b009043733d747aa6f7ee3de0a50dccf95363f
finite-or

diff -r 58b009043733 -r a7364dfcc51e agda/finiteSet.agda
--- a/agda/finiteSet.agda	Mon Nov 18 19:51:08 2019 +0900
+++ b/agda/finiteSet.agda	Mon Nov 18 23:53:47 2019 +0900
@@ -11,7 +11,6 @@
 open import logic
 open import nat
 open import Data.Nat.Properties  hiding ( _≟_ )
-open import Data.List
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
@@ -41,12 +40,13 @@
      exists : ( Q → Bool ) → Bool
      exists p = exists1 n (lt0 n) p 
 
-     list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q
+     open import Data.List
+     list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q 
      list1  zero  _ _ = []
      list1 ( suc m ) m<n p with bool-≡-? (p (Q←F (fromℕ≤ {m} {n} m<n))) true
      ... | yes _ = Q←F (fromℕ≤ {m} {n} m<n) ∷ list1 m (lt2 m<n) p
-     ... | no  _ = list1 m (lt2 m<n) p
-     to-list : ( Q → Bool ) → List Q
+     ... | no  _ = list1 m (lt2 m<n)  p
+     to-list : ( Q → Bool ) → List Q 
      to-list p = list1 n (lt0 n) p 
 
      equal? : Q → Q → Bool
@@ -158,59 +158,108 @@
         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) = {!!}
-        -- finiso→ (case2 qb) = {!!}
+        finiso→ (case1 qa) = {!!} 
+        finiso→ (case2 qb) = {!!}
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
-        finiso← f = {!!} -- with Data.Nat.Properties.<-cmp (toℕ f) a
+        finiso← f with Data.Nat.Properties.<-cmp (toℕ f) a
+        finiso← f | tri< lt ¬b ¬c = lemma11 where
+            lemma11 : inject+ b (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ lt ) )) ≡ f
+            lemma11 = {!!}
+        finiso← f | tri≈ ¬a eq ¬c = lemma12 where
+            lemma12 : raise a (FiniteSet.F←Q fb (FiniteSet.Q←F fb (fromℕ≤  {!!} ))) ≡ f
+            lemma12 = {!!}
+        finiso← f | tri> ¬a ¬b c = lemma13  where
+            lemma13 : raise a (FiniteSet.F←Q fb ((FiniteSet.Q←F fb (f-a f a c (toℕ<n f))))) ≡ f
+            lemma13 = {!!}
 
 import Data.Nat.DivMod
 import Data.Nat.Properties
 
 open _∧_
 
-fin→' : {A : Set} → { a : ℕ } → FiniteSet A {suc a} → FiniteSet (A → Bool ) {exp 2 (suc a)}
-fin→' {A} {a} fin = record {
-        Q←F = Q←F  
-      ; F←Q =  F←Q  
+open import Data.Vec
+import Data.Product
+
+exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n
+exp2 n = begin
+        exp 2 (suc n)
+     ≡⟨⟩
+        2 * ( exp 2 n )
+     ≡⟨ *-comm 2 (exp 2 n)  ⟩
+        ( exp 2 n ) * 2
+     ≡⟨ +-*-suc ( exp 2 n ) 1 ⟩
+        (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1
+     ≡⟨ cong ( λ k →  (exp 2 n ) Data.Nat.+  k ) (proj₂ *-identity (exp 2 n) ) ⟩
+        exp 2 n Data.Nat.+ exp 2 n
+     ∎  where
+         open ≡-Reasoning
+         open Data.Product
+
+cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f)  ≡ f
+cast-iso refl zero =  refl
+cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )
+
+
+fin2List : {n : ℕ } → FiniteSet (Vec Bool n) {exp 2 n }
+fin2List {zero} = record {
+        Q←F = λ _ → Vec.[]
+      ; F←Q =  λ _ → # 0
       ; finiso→ = finiso→ 
       ; finiso← = finiso← 
    } where
-        n : ℕ
-        n = exp 2 (suc a)
-        shift : (n : ℕ) →  ℕ ∧ Bool
-        shift n with (n Data.Nat.DivMod.mod 2) ≟ (# 0)
-        shift n | yes p = record { proj1 = n Data.Nat.DivMod.div 2 ; proj2 = true }
-        shift n | no ¬p = record { proj1 = n Data.Nat.DivMod.div 2 ; proj2 = false }
-        Q←F-shift : (n : ℕ) → ℕ → ℕ → Bool
-        Q←F-shift zero an flag with zero Data.Nat.Properties.≟ an | shift flag
-        ... | yes _ | F = proj2 F
-        ... | no _ | _ = true
-        Q←F-shift (suc n) an flag with zero Data.Nat.Properties.≟ an | shift flag
-        ... | yes _ | F = proj2 F
-        ... | no _ | F = Q←F-shift n an (proj1 F)
+        Q = Vec Bool zero
+        finiso→ : (q : Q) → [] ≡ q
+        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 = A → Bool
-        Q←F : Fin n → Q
-        Q←F f = λ qa → Q←F-shift a (toℕ (FiniteSet.F←Q fin qa)) (toℕ f)
-        unshift : {i : ℕ } (n : Fin i) → Bool → Fin (i Data.Nat.+ i)
-        unshift {i} n true = fromℕ≤ 2n<2i where
-            2n<2i : (toℕ n) Data.Nat.+ (toℕ n) <  i Data.Nat.+ i
-            2n<2i = {!!}
-        unshift {i} n false = fromℕ≤ 2n<2i+1 where
-            2n<2i+1 : (toℕ n) Data.Nat.+ (toℕ n) Data.Nat.+ 1 <  i Data.Nat.+ i
-            2n<2i+1 = {!!}
-        F←Q-unshift : Q → (i : ℕ ) → i < suc a → Fin (exp 2 (suc i)) 
-        F←Q-unshift fq zero lt with fq (FiniteSet.Q←F fin (fromℕ≤ a<sa))
-        ... | false = # 0
-        ... | true = # 1
-        F←Q-unshift fq (suc n) lt = cast {!!} (unshift (F←Q-unshift fq n {!!} ) (fq (FiniteSet.Q←F fin (fromℕ≤ lt )))) 
-        F←Q : Q → Fin n
-        F←Q fq = F←Q-unshift fq a a<sa
+        Q = Vec Bool (suc  n)
+        QtoR : Vec Bool (suc  n) →  Vec Bool n ∨ Vec Bool n
+        QtoR ( true ∷ x ) = case1 x
+        QtoR ( false ∷ x ) = case2 x
+        RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc  n) 
+        RtoQ ( case1 x ) = true ∷ x
+        RtoQ ( case2 x ) = false ∷ x
+        isoRQ : (x : Vec Bool (suc  n) ) → RtoQ ( QtoR x ) ≡ x
+        isoRQ (true ∷ _ ) = refl
+        isoRQ (false ∷ _ ) = refl
+        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→ = {!!}
-        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
-        finiso← = {!!}
+        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
 
+Func2List : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → ( Q → Bool ) → Vec Bool n
+Func2List = {!!}
 
-
+List2Func : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → Vec Bool n → ( Q → Bool ) 
+List2Func = {!!}