module finiteSet  where

open import Data.Nat hiding ( _≟_ )
open import Data.Fin renaming ( _<_ to _<<_ )
open import Data.Fin.Properties
open import Relation.Nullary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import logic

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
     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)
     exists : ( Q → Bool ) → Bool
     exists p = exists1 n (lt0 n) p where
         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
     equal? : Q → Q → Bool
     equal? q0 q1 with F←Q q0 ≟ F←Q q1
     ... | yes p = true
     ... | no ¬p = false

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