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

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
     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
     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} → (f : Fin i ) → (a : ℕ ) → toℕ f > a  → toℕ f < a Data.Nat.+ b  → Fin b
        f-a {i} 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) () _
        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
            a<a+b : toℕ f ≡ a → a < a Data.Nat.+ b 
            a<a+b 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
        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) = {!!} 
        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 | 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 _∧_

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 : ℕ } → FiniteSet Q {n}  → ( Q → Bool ) → Vec Bool n
Func2List = {!!}

List2Func : { Q : Set } → {n : ℕ } → FiniteSet Q {n}  → Vec Bool n → ( Q → Bool ) 
List2Func = {!!}