module finiteSet  where

open import Data.Nat hiding ( _≟_ )
open import Data.Fin renaming ( _<_ to _<<_ )
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 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 
     equal? : Q → Q → Bool
     equal? q0 q1 with F←Q q0 ≟ F←Q q1
     ... | yes p = true
     ... | no ¬p = false
     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 
              ≡⟨ cong (λ k → k \/ exists1 m (lt2 m<n) p ) eq ⟩
                  false \/ exists1 m (lt2 m<n) p 
              ≡⟨ bool-or-1 refl  ⟩
                  exists1 m (lt2 m<n) p 
              ≡⟨ not-found2 m (lt2 m<n)  ⟩
                  false
              ∎  where open ≡-Reasoning
     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})
     found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
     found {p} {q} pt = found1 n  (fin<n {n} {F←Q q}) (lt0 n) where
         iq : {m : ℕ} (lt : suc m Data.Nat.≤ n ) → toℕ (F←Q q) ≡ m → Q←F (fromℕ≤ lt) ≡ q
         iq {m} lt refl = begin
                 Q←F (fromℕ≤ lt) 
              ≡⟨ {!!} ⟩
                 Q←F (F←Q q)
              ≡⟨ finiso→ q ⟩
                 q 
              ∎  where open ≡-Reasoning
         found1 : (m : ℕ ) {i : ℕ} (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) →  exists1 m m<n p ≡ true
         found1 (suc m)  lt m<n with Data.Nat._≟_ m (toℕ (F←Q q))
         found1 (suc m)  lt m<n | yes refl = begin
                 p (Q←F (fromℕ≤ m<n )) \/ exists1 m (lt2 m<n ) p
              ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (iq m<n refl ) ⟩
                 p q \/ exists1 m (lt2 m<n ) p
              ≡⟨ cong (λ k → ( k \/ exists1 m (lt2 m<n ) p )) pt ⟩
                  true \/ exists1 m (lt2 m<n ) p
              ≡⟨⟩
                 true 
              ∎  where open ≡-Reasoning
         found1 (suc m)  lt m<n | no ¬p = {!!}
             

fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
fless zero = s≤s z≤n
fless (suc f) = s≤s ( fless f )