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})
     <s : {m : ℕ} → m Data.Nat.≤ suc m
     <s {zero} = z≤n
     <s {suc m} = s≤s <s
     lemma0 : {n : ℕ } {i j : ℕ } → i ≡ j → ( i<n : (suc i) Data.Nat.≤ n ) → ( j<n : (suc j) Data.Nat.≤ n ) → i<n ≅ j<n
     lemma0 {_} {0} {0} refl (s≤s z≤n) (s≤s z≤n) = HE.refl
     lemma0 {suc n} {suc i} {suc i} refl (s≤s (s≤s x)) (s≤s (s≤s y))  = HE.cong ( λ k → s≤s k) (lemma0 {n} {i} {i} refl (s≤s x)  (s≤s y))
     lemma : {n : ℕ } {i j : ℕ } → i ≡ j → { i<n : (suc i) Data.Nat.≤ n } → { j<n : (suc j) Data.Nat.≤ n } → fromℕ≤ i<n ≅ fromℕ≤ j<n
     lemma refl {x} {y} = HE.cong ( λ k → fromℕ≤ k ) ( lemma0 refl x y )
     lemma1 : {i m : ℕ } (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) → i < n
     lemma1 {i} {m} i≤m m<n =  Data.Nat.Properties.≤-trans i≤m m<n 
     found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
     found {p} {q} pt = found1 n (toℕ (F←Q q)) (fin<n {n} {F←Q q}) (lt0 n) {!!} where
         lemma2 : F←Q q ≅ fromℕ≤ (lemma1 (fin<n {n} {F←Q q}) (lt0 n))
         lemma2 = {!!}
         lemma3 : {m i : ℕ} → ( m<n : m Data.Nat.≤ n ) → (i≤m : i Data.Nat.≤ suc m )
             → (iq :  F←Q q ≅ fromℕ≤ {i} {n} {!!} ) → Q←F (fromℕ≤ {!!}) ≡ q
         lemma3 = {!!}
         found1 : (m : ℕ ) (i : ℕ) (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) ( iq : F←Q q ≡ fromℕ≤ {i} (lemma1 i≤m m<n) ) →  exists1 m m<n p ≡ true
         found1 (suc m) i lt m<n iq with Data.Nat._≟_ m i
         found1 (suc m) i lt m<n iq | 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 )) (
                 begin
                    Q←F (fromℕ≤ m<n) 
                 ≡⟨ lemma HE.refl ⟩
                    Q←F (fromℕ≤ {i} (lemma1 lt m<n))
                 ≡⟨ cong ( λ k → Q←F k ) (sym iq)  ⟩
                    Q←F (F←Q q)
                 ≡⟨ {!!} ⟩
                    q
                 ∎ ) ⟩
                 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) i lt m<n iq | no ¬p = {!!}
             

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