{-# OPTIONS --allow-unsolved-metas #-}
module finiteSet  where

open import Data.Nat hiding ( _≟_ )
open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
open import Data.Fin.Properties
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import logic
open import nat
open import Data.Nat.Properties  hiding ( _≟_ )

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 

record Found ( Q : Set ) (p : Q → Bool ) : Set where
     field
       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
        F←Q : Q → Fin n
        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
     finℕ : ℕ
     finℕ = n
     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
     exists : ( Q → Bool ) → Bool
     exists p = exists1 n (lt0 n) p 

     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 
     to-list p = list1 n (lt0 n) p 

     equal? : Q → Q → Bool
     equal? q0 q1 with F←Q q0 ≟ F←Q q1
     ... | yes p = true
     ... | no ¬p = false
     equal→refl  : { x y : Q } → equal? x y ≡ true → x ≡ y
     equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1
     equal→refl {q0} {q1} refl | yes eq = begin
            q0
        ≡⟨ sym ( finiso→ q0) ⟩
            Q←F (F←Q q0)
        ≡⟨ cong (λ k → Q←F k ) eq ⟩
            Q←F (F←Q q1)
        ≡⟨ finiso→ q1 ⟩
            q1
        ∎  where open ≡-Reasoning
     equal→refl {q0} {q1} () | no ne 
     equal?-refl : {q : Q} → equal? q q ≡ true
     equal?-refl {q} with F←Q q ≟ F←Q q
     ... | yes p = refl
     ... | no ne = ⊥-elim (ne refl)
     fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
     fin<n {_} {zero} = s≤s z≤n
     fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
     i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j
     i=j {suc n} zero zero refl = refl
     i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) )
     --   ¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P → ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
     End : (m : ℕ ) → (p : Q → Bool ) → Set
     End m p = (i : Fin n) → m ≤ toℕ i → p (Q←F i )  ≡ false 
     next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
              → (m<n : m < n ) → p (Q←F (fromℕ≤ m<n )) ≡ false
              → End m p
     next-end {m} p prev m<n np i m<i with Data.Nat.Properties.<-cmp m (toℕ i) 
     next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a
     next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c )
     next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where
              m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n )  → fromℕ≤ m<n ≡ i
              m<n=i i eq m<n = i=j (fromℕ≤ m<n) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq )
     first-end :  ( p : Q → Bool ) → End n p
     first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {n} {i}) )
     found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true
     found {p} q pt = found1 n  (lt0 n) ( first-end p ) where
         found1 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → ((i : Fin n) → m ≤ toℕ i → p (Q←F i )  ≡ false ) →  exists1 m m<n p ≡ true
         found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt )
         found1 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
         found1 (suc m)  m<n end | yes eq = subst (λ k → k \/ exists1 m (lt2 m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (lt2 m<n) p} ) 
         found1 (suc m)  m<n end | no np = begin
                 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p
              ≡⟨ bool-or-1 (¬-bool-t np ) ⟩
                 exists1 m (lt2 m<n) p
              ≡⟨ found1 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) ⟩
                 true
              ∎  where open ≡-Reasoning
     not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
     not-found {p} pn = not-found2 n (lt0 n) where
         not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false
         not-found2  zero  _ = refl
         not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n))
         not-found2 (suc m) m<n | eq = begin
                  p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p 
              ≡⟨ bool-or-1 eq ⟩
                  exists1 m (lt2 m<n) p 
              ≡⟨ not-found2 m (lt2 m<n)  ⟩
                  false
              ∎  where open ≡-Reasoning
     open import Level
     postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
     found← : { p : Q → Bool } → exists p ≡ true → Found Q p
     found← {p} exst = found2 n (lt0 n) (first-end p ) where
         found2 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p →  Found Q p
         found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q)  z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where
             lemma : (λ z → p (Q←F (F←Q z))) ≡ p
             lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl )
         found2 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
         found2 (suc m)  m<n end | yes eq = record { found-q = Q←F (fromℕ≤ m<n) ; found-p = eq }
         found2 (suc m)  m<n end | no np = 
               found2 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) 
     not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
     not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) )

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 )

import Data.Nat.DivMod
import Data.Nat.Properties

open _∧_

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
        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 = 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→ 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 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

List2Func : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → Vec Bool n →  Q → Bool 
List2Func {Q} {zero} _ fin [] q = false
List2Func {Q} {suc n} {m} (s≤s n<m) fin (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ≤ n<m
... | 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 = {!!}

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 = {!!}