{-# 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 ) )

record ISO (A B : Set) : Set where
   field
       A←B : B → A
       B←A : A → B
       iso← : (q : A) → A←B ( B←A q ) ≡ q
       iso→ : (f : B) → B←A ( A←B f ) ≡ f

iso-fin : {A B : Set} → {n : ℕ } → FiniteSet A {n} → ISO A B → FiniteSet B {n}
iso-fin {A} {B} {n} fin iso = record {
        Q←F = λ f → ISO.B←A iso ( FiniteSet.Q←F fin f )
      ; F←Q = λ b → FiniteSet.F←Q fin ( ISO.A←B iso b )
      ; finiso→ = finiso→ 
      ; finiso← = finiso← 
   } where
        finiso→ : (q : B) → ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) ≡ q
        finiso→ q = begin
                   ISO.B←A iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (ISO.A←B iso q))) 
                ≡⟨ cong (λ k → ISO.B←A iso k ) (FiniteSet.finiso→ fin _ ) ⟩
                   ISO.B←A iso (ISO.A←B iso q)
                ≡⟨ ISO.iso→ iso _ ⟩
                   q
                ∎  where
                open ≡-Reasoning
        finiso← : (f : Fin n) → FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) ≡ f
        finiso← f = begin
                   FiniteSet.F←Q fin (ISO.A←B iso (ISO.B←A iso (FiniteSet.Q←F fin f))) 
                ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (ISO.iso← iso _) ⟩
                   FiniteSet.F←Q fin (FiniteSet.Q←F fin f) 
                ≡⟨ FiniteSet.finiso← fin _  ⟩
                   f
                ∎  where
                open ≡-Reasoning

data One : Set where
   one : One

fin-∨1 : {B : Set} → { b : ℕ } → FiniteSet B {b} → FiniteSet (One ∨ B) {suc b}
fin-∨1 {B} {b} fb =  record {
        Q←F = Q←F
      ; F←Q =  F←Q
      ; finiso→ = finiso→
      ; finiso← = finiso←
   }  where
        Q←F : Fin (suc b) → One ∨ B
        Q←F zero = case1 one
        Q←F (suc f) = case2 (FiniteSet.Q←F fb f)
        F←Q : One ∨ B → Fin (suc b)
        F←Q (case1 one) = zero
        F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) 
        finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q
        finiso→ (case1 one) = refl
        finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b)
        finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q
        finiso← zero = refl
        finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f)


fin-∨2 : {B : Set} → ( a : ℕ ) → { b : ℕ } → FiniteSet B {b} → FiniteSet (Fin a ∨ B) {a Data.Nat.+ b}
fin-∨2 {B} zero {b} fb = iso-fin fb iso where
   iso : ISO B (Fin zero ∨ B)
   iso =  record {
          A←B = A←B
        ; B←A = λ b → case2 b
        ; iso→ = iso→
        ; iso← = λ _ → refl
      } where
          A←B : Fin zero ∨ B → B
          A←B (case2 x) = x 
          iso→ : (f : Fin zero ∨ B ) → case2 (A←B f) ≡ f
          iso→ (case2 x)  = refl
fin-∨2 {B} (suc a) {b} fb =  iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
    where
       iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B)
       ISO.A←B iso (case1 zero) = case1 one
       ISO.A←B iso (case1 (suc f)) = case2 (case1 f)
       ISO.A←B iso (case2 b) = case2 (case2 b)
       ISO.B←A iso (case1 one) = case1 zero
       ISO.B←A iso (case2 (case1 f)) = case1 (suc f)
       ISO.B←A iso (case2 (case2 b)) = case2 b
       ISO.iso← iso (case1 one) = refl
       ISO.iso← iso (case2 (case1 x)) = refl
       ISO.iso← iso (case2 (case2 x)) = refl
       ISO.iso→ iso (case1 zero) = refl
       ISO.iso→ iso (case1 (suc x)) = refl
       ISO.iso→ iso (case2 x) = refl


FiniteSet→Fin : {A : Set} → { a : ℕ } → (fin : FiniteSet A {a} ) → ISO (Fin a) A
ISO.A←B (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f
ISO.B←A (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f
ISO.iso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin
ISO.iso→ (FiniteSet→Fin fin) =  FiniteSet.finiso→ fin
   

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 = iso-fin (fin-∨2 a fb ) iso2 where
    ia = FiniteSet→Fin fa
    iso2 : ISO (Fin a ∨ B ) (A ∨ B)
    ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x )
    ISO.A←B iso2 (case2 x) = case2 x
    ISO.B←A iso2 (case1 x) = case1 ( ISO.B←A ia x )
    ISO.B←A iso2 (case2 x) = case2 x
    ISO.iso← iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso← ia x)
    ISO.iso← iso2 (case2 x) = refl
    ISO.iso→ iso2 (case1 x) = cong ( λ k → case1 k ) (ISO.iso→ ia x)
    ISO.iso→ iso2 (case2 x) = refl

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} = subst (λ k → FiniteSet (Vec Bool (suc n)) {k} ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List {n}) (fin2List {n})) iso )
    where
        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
        iso : ISO (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n))
        iso = record { A←B = QtoR ; B←A = RtoQ ; iso← = isoQR ; iso→ = isoRQ  }

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
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 ) → 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
       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 (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 
           lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
           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) 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) 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) 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 : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} )  → Vec Bool n → (q :  Q ) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool
L2F n<m fin x q q<n = List2Func n<m fin x q 

L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (L2F a<sa fin (F2L a<sa fin (λ q _ → f q) )) q (toℕ<n _) ≡ f q
L2F-iso {Q} {m} fin f q = l2f m a<sa (toℕ<n _) where
    lemma11 : {n : ℕ } → (n<m : n < m )  → ¬ ( FiniteSet.F←Q fin q ≡ fromℕ≤ n<m ) → toℕ (FiniteSet.F←Q fin q) ≤ n → toℕ (FiniteSet.F←Q fin q) < n
    lemma11 {n} n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where
       lemma13 : {n nq : ℕ } → (n<m : n < m )  → ¬ ( nq ≡ n ) → nq  ≤ n → nq < n
       lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
       lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
       lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (Data.Nat.Properties.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
       lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ≤ (s≤s lt) ≡ suc (fromℕ≤ lt)
       lemma3 (s≤s lt) = refl
       lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ≤ n<m 
       lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
       lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3 n<m) ) ( cong ( λ k → suc k ) ( lemma12 {n} {m} n<m f refl  ) )
    l2f :  (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n )  →  (L2F n<m fin (F2L n<m  fin (λ q _ → f q))) q q<n ≡ f q
    l2f zero (s≤s z≤n) ()
    l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m 
    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p with inspect f q
    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | record { eq = refl } = begin 
             f (FiniteSet.Q←F fin (fromℕ≤ n<m)) 
          ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p)  ⟩
             f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q ))
          ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
             f q 
          ∎  where
            open ≡-Reasoning
    l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (Data.Nat.Properties.<-trans n<m a<sa) (lemma11 n<m ¬p n<q)

fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
fin→ {A} {a} fin = iso-fin fin2List iso where
    iso : ISO (Vec Bool a ) (A → Bool)
    ISO.A←B iso x = F2L a<sa fin ( λ q _ → x q )
    ISO.B←A iso x = List2Func a<sa fin x 
    ISO.iso← iso x  =  F2L-iso fin x 
    ISO.iso→ iso x = lemma where
       lemma : List2Func a<sa fin (F2L a<sa fin (λ q _ → x q)) ≡ x
       lemma = FiniteSet.f-extensionality fin ( λ q → L2F-iso fin x q )
    

open import Data.Product

Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) {n}
Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }

data f-1 { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
  elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → f-1 n<m fa

-- f-1-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
--    → ( elm s ≡ elm t) → ( elm<n s ≅ elm<n t ) → elm1 e0 e0<n ≡ elm1 e1 e1<n
-- f-1-<-cong n<m fa _ _ refl HE.refl = refl

fin-<' : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (f-1 n<m fa) {n}
fin-<' {A} {n} {m} n<m fa  = iso-fin (Fin2Finite n) iso where
    iso : ISO (Fin n) (f-1 n<m fa)
    ISO.A←B iso (elm1 elm x) = fromℕ≤ x
    ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m ))) to<n where
        x<n : toℕ x < n
        x<n = toℕ<n x
        to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m)))) < n
        to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m) )) x<n )
    ISO.iso← iso x  = lemma2 where
        lemma2 : fromℕ≤ (subst (λ k → toℕ k < n) (sym
          (FiniteSet.finiso← fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
          (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
        lemma2 = {!!}
    ISO.iso→ iso (elm1 elm x) = lemma1 where
        lemma : FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm 
        lemma = {!!}
        lemma1 : ISO.B←A iso (ISO.A←B iso (elm1 elm x)) ≡ elm1 elm x
        lemma1 with lemma
        ... | eq = {!!}


record Fin-< { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) : Set where
  field 
    elm : A
    elm<n : toℕ (FiniteSet.F←Q fa elm ) < n

open Fin-<

Fin-<-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
   → ( s t : Fin-< n<m fa ) 
   → ( elm s ≡ elm t) → ( elm<n s ≅ elm<n t ) → s ≡ t
Fin-<-cong n<m fa _ _ refl HE.refl = refl

lemma1 : {m n : ℕ } → ( i j : m < n ) → i ≡ j
lemma1 {zero} {suc n} (s≤s z≤n) (s≤s z≤n) = refl
lemma1 {suc m} {suc n} (s≤s i) (s≤s j) = cong ( λ k → s≤s k ) ( lemma1 {m} {n} i j )

fin-< : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (Fin-< n<m fa) {n}
fin-< {A} {zero} {m} (s≤s z≤n) fa  = record { Q←F = λ () ; F←Q = λ () ; finiso← = λ () ; finiso→ = λ ()  }
fin-< {A} {suc n} {m} (s≤s n<m) fa = iso-fin (fin-∨1 (fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa)) iso where
   fin- : FiniteSet (Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa)
   fin- = fin-< {A} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa) fa
   iso : ISO (One ∨ Fin-< (Data.Nat.Properties.<-trans n<m a<sa) fa) (Fin-< (s≤s n<m) fa)
   lastf = FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ))
   c1 : toℕ lastf ≡ n 
   c1 = subst (λ k → toℕ k ≡ n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k ≡ n) (sym (toℕ-fromℕ≤ _ )) refl )
   f<n : toℕ lastf < suc n
   f<n = subst ( λ k → k < suc n ) (sym c1) a<sa
   last1 = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
   ISO.A←B iso x with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n
   ISO.A←B iso x | tri< a ¬b ¬c = case2 record { elm = elm x ; elm<n = a }
   ISO.A←B iso x | tri≈ ¬a b ¬c = case1 one
   ISO.A←B iso x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )
   ISO.B←A iso (case1 one)  = record { elm = last1 ; elm<n = f<n }
   ISO.B←A iso (case2 x)  = record { elm = elm x ; elm<n = Data.Nat.Properties.<-trans (elm<n x) a<sa }
   ISO.iso← iso (case1 one) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm (ISO.B←A iso (case1 one))))) n
   ISO.iso← iso (case1 one) | tri< a ¬b ¬c = ⊥-elim ( ¬b c1 )
   ISO.iso← iso (case1 one) | tri≈ ¬a b ¬c = refl
   ISO.iso← iso (case1 one) | tri> ¬a ¬b c = ⊥-elim ( ¬b c1 )
   ISO.iso← iso (case2 x) with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x))) n
   ISO.iso← iso (case2 x) | tri< a ¬b ¬c = cong ( λ k → case2 record { elm = elm x ; elm<n = k } ) (lemma1 _ _) where
   ISO.iso← iso (case2 x) | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (elm<n x) )
   ISO.iso← iso (case2 x) | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (elm<n x) )
   ISO.iso→ iso x with ISO.A←B iso x  
   ISO.iso→ iso x | case1 one with Data.Nat.Properties.<-cmp (toℕ (FiniteSet.F←Q fa (elm x )) ) n 
   ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c (elm<n x) )
   ... | tri< a ¬b ¬c =  {!!}
   ... | tri≈ ¬a b ¬c =  begin
           record { elm = FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) ; elm<n = lemma5 }
       ≡⟨ Fin-<-cong (s≤s n<m) fa _ _ (sym (lemma2 b)) lemma7 ⟩
           record { elm = elm x ; elm<n = elm<n x }
       ≡⟨⟩
           x
       ∎
    where
      open ≡-Reasoning
      lemma3 : {n m : ℕ } (x : Fin m)  → toℕ x ≡ n → (n<m : n < m ) → x ≡ fromℕ≤ n<m
      lemma3 _ refl n<m = sym ( fromℕ≤-toℕ  _ n<m )
      lemma4 : {x : A } → (x=n : toℕ (FiniteSet.F←Q fa x)  ≡ n ) → fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa) ≡ FiniteSet.F←Q fa x
      lemma4 {x} refl = sym ( lemma3 _ refl (Data.Nat.Properties.<-trans n<m a<sa)) 
      lemma2 : {x : A} → toℕ (FiniteSet.F←Q fa x) ≡ n → x ≡ FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))
      lemma2 {x} refl = sym ( begin
                 FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)) 
              ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma4 refl) ⟩
                 FiniteSet.Q←F fa ( FiniteSet.F←Q fa x )
              ≡⟨ FiniteSet.finiso→ fa _ ⟩
                 x 
              ∎ ) where open ≡-Reasoning
      lemma5 : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa)))) < suc n
      lemma5 = subst (λ k → suc k ≤ suc n)
            (sym
             (subst (λ k → toℕ k ≡ n)
              (sym
               (FiniteSet.finiso← fa
                (fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))))
              (subst (λ k → k ≡ n)
               (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans n<m a<sa))) refl)))
                    a<sa
      lemma7 : lemma5 ≅ elm<n x
      lemma7 with lemma2 b
      ... | refl with lemma1 lemma5 (elm<n x)
      ... | refl = HE.refl

   ISO.iso→ iso x | case2 x1 = {!!}
   -- ISO.iso→ iso x | case2 x1 | tri< a ¬b ¬c = ?
   -- ISO.iso→ iso x | case2 x1 | tri≈ ¬a b ¬c = {!!}
   -- ISO.iso→ iso x | case2 x1 | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (elm<n x) )

fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
fin-× {A} {B} {a} {b} fa fb with FiniteSet→Fin fa
... | a=f = iso-fin (fin-×-f a ) iso-1 where
   iso-1 : ISO (Fin a × B) ( A × B )
   ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x) 
   ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x) 
   ISO.iso← iso-1 x  =  lemma  where
      lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
      lemma = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso← fa _ )
   ISO.iso→ iso-1 x = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso→ fa _ )
   iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B)
   ISO.A←B iso-2 (zero , b ) = case1 b
   ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b )
   ISO.B←A iso-2 (case1 b) = ( zero , b )
   ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b )
   ISO.iso← iso-2 (case1 x) = refl
   ISO.iso← iso-2 (case2 x) = refl
   ISO.iso→ iso-2 (zero , b ) = refl
   ISO.iso→ iso-2 (suc a , b ) = refl
   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) × B) {a * b}
   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () }
   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2