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
       found-p : p found ≡ 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 
     equal? : Q → Q → Bool
     equal? q0 q1 with F←Q q0 ≟ F←Q q1
     ... | yes p = true
     ... | no ¬p = false
     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←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} ne q = not-found3 n (lt0 n) (first-end p ) ne where
         not-found3 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p → exists1 m m<n p ≡ false  →  p q ≡ false
         not-found3 0 m<n end prev = subst (λ k → p k ≡ false) (finiso→ q) ( end (F←Q q) z≤n ) 
         not-found3 (suc m)  m<n end prev with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
         not-found3 (suc m)  m<n end prev | yes eq =
             ⊥-elim ( ¬-bool prev (subst (λ k → k \/  exists1 m (lt2 m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (lt2 m<n) p}) )) 
         not-found3 (suc m)  m<n end prev | no np = 
              not-found3 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) ( begin
                     exists1 m (lt2 m<n) p 
                  ≡⟨ sym (bool-or-1 (¬-bool-t np )) ⟩
                     p (Q←F (fromℕ≤ m<n))  \/ exists1 m (lt2 m<n) p 
                  ≡⟨ prev ⟩
                     false 
                  ∎ ) where open ≡-Reasoning
             

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