Prove that Kuratowski finite decidable sets are finite

src/Data/Array.ard

@@ -1,9 +1,13 @@
 \import Data.Bool
+\import Data.Fin
 \import Data.Maybe
 \import Data.Or
+\import Function.Meta ($)
+\import Logic
 \import Meta
 \import Paths
 \import Paths.Meta
+\import Set
 
 \func mkArray {A : \Type} {n : Nat} (f : Fin n -> A) => \new Array A n f
 
@@ -120,4 +124,73 @@
   | at j => (j, l j)
 
 \func replicate {A : \Type} (n : Nat) (a : A)
-  => \new Array A n (\lam _ => a)
+  => \new Array A n (\lam _ => a)
+
+\func remove {A : DecSet} (a : A) (l : Array A) : Array A \elim l
+  | nil => nil
+  | a' :: l => \case decideEq a a' \with {
+    | yes _ => remove a l
+    | no _ => a' :: remove a l
+  }
+  \where {
+    \lemma no-element {A : DecSet} {a : A} {l : Array A} {i : Fin (DArray.len {remove a l})} (p : remove a l i = a) : Empty \elim l
+      | nil => \case i
+      | a' :: l => cases (decideEq a a', i, p) \with {
+        | yes e, i, p => no-element p
+        | no q, 0, p => q (inv p)
+        | no q, suc i, p => no-element p
+      }
+
+    \func preimage {A : DecSet} (a : A) (l : Array A) (i : Fin (DArray.len {remove a l})) : \Sigma (j : Fin l.len) (remove a l i = l j) \elim l
+      | nil => (i,idp)
+      | a' :: l => cases (decideEq a a', i) \with {
+        | yes e, i => \let t => preimage a l i \in (suc t.1, t.2)
+        | no q, 0 => (0,idp)
+        | no q, suc i => \let t => preimage a l i \in (suc t.1, t.2)
+      }
+
+    \lemma no-repeats {A : DecSet} {l : Array A} (p : \Pi {i j : Fin l.len} -> l i = l j -> i = j) {a : A} {i j : Fin (DArray.len {remove a l})} (q : remove a l i = remove a l j) : i = j \elim l
+      | nil => \case i
+      | a' :: l => cases (decideEq a a', i, j, q) \with {
+        | yes _, i, j, q => no-repeats (\lam {i'} {j'} s => pmap (fpred i') $ p {suc i'} {suc j'} s) q
+        | no _, 0, 0, q => idp
+        | no s, 0, suc j, q => \let t => preimage a l j \in \case p {0} {suc t.1} (q *> t.2)
+        | no _, suc i, 0, q => \let t => preimage a l i \in \case p {suc t.1} {0} (inv t.2 *> q)
+        | no s, suc i, suc j, q => pmap fsuc (no-repeats (\lam {i'} {j'} s => pmap (fpred i') $ p {suc i'} {suc j'} s) q)
+      }
+  }
+
+\func nub {A : DecSet} (l : Array A) : Array A \elim l
+  | nil => nil
+  | a :: l => a :: remove a (nub l)
+
+\func nub-isSruj {A : DecSet} (l : Array A) (i : Fin l.len) : \Sigma (j : Fin (DArray.len {nub l})) (nub l j = l i) \elim l, i
+  | a :: l, 0 => (0,idp)
+  | a :: l, suc i =>
+    \case decideEq a (l i) \with {
+      | yes e => (0,e)
+      | no q =>
+        \have | t => nub-isSruj l i
+              | s => remove-isSurj a (nub l) t.1 $ \lam p => q $ inv p *> t.2
+        \in (suc s.1, s.2 *> t.2)
+    }
+  \where {
+    \func remove-isSurj {A : DecSet} (a : A) (l : Array A) (i : Fin l.len) (p : l i /= a) : \Sigma (j : Fin (DArray.len {remove a l})) (remove a l j = l i) \elim l
+      | nil => \case i
+      | a' :: l => mcases \with {
+        | yes e => cases (i,p) \with {
+          | 0, p => absurd $ p (inv e)
+          | suc i, p => remove-isSurj a l i p
+        }
+        | no q => cases (i,p) \with {
+          | 0, p => (0,idp)
+          | suc i, p => \let t => remove-isSurj a l i p \in (suc t.1, t.2)
+        }
+      }
+  }
+
+\lemma nub-isInj {A : DecSet} (l : Array A) {i j : Fin (DArray.len {nub l})} (p : nub l i = nub l j) : i = j \elim l, i, j
+  | a :: l, 0, 0 => idp
+  | a :: l, 0, suc j => absurd $ remove.no-element (inv p)
+  | a :: l, suc i, 0 => absurd (remove.no-element p)
+  | a :: l, suc i, suc j => pmap fsuc $ remove.no-repeats (nub-isInj l) p

src/Data/Fin.ard

@@ -11,6 +11,10 @@
 
 \cons fsuc {n : Nat} (x : Fin n) : Fin (suc n) => suc x
 
+\func fpred {n : Nat} (def : Fin n) (x : Fin (suc n)) : Fin n \elim x
+  | 0 => def
+  | suc x => x
+
 \func last-fin (n : Nat) : Fin (suc n) \elim n
   | 0 => 0
   | suc n => suc (last-fin n)

src/Set/Fin.ard

@@ -89,6 +89,12 @@
       | suc n, suc x0, 0, suc y => \case p
       | suc n, suc x0, suc x, 0 => \case p
       | suc n, suc x0, suc x, suc y => pmap (suc __) (skip-isInj (suc-isInj _ _ p))
+
+    \lemma fromArray {A : \Set} (l : Array A) (p : \Pi (a : A) -> ∃ (i : Fin l.len) (l i = a)) (q : \Pi {i j : Fin l.len} -> l i = l j -> i = j) : FinSet A l.len \cowith
+      | finEq => inP $ inv $ Equiv-to-= $ \new ESEquiv l {
+                                            | Embedding => Embedding.fromInjection q
+                                            | isSurj => p
+                                          }
   }
 
 \lemma transport_zero {n m : Nat} (p : n = m) : transport Fin (pmap suc p) 0 = 0 \elim p

src/Set/Fin/KFin.ard

@@ -0,0 +1,27 @@
+\import Data.Array
+\import Function
+\import Function.Meta ($)
+\import Logic
+\import Logic.Meta
+\import Paths
+\import Set
+\import Set.Fin
+
+\class KFinSet (n : Nat) \extends BaseSet
+  | finSurj : ∃ (f : Fin n -> E) (isSurj f)
+  \where {
+    \lemma fromArray {A : \Set} (l : Array A) (p : \Pi (a : A) -> ∃ (i : Fin l.len) (l i = a)) : KFinSet A l.len \cowith
+      | finSurj => inP (l,p)
+
+    \lemma toArray (A : KFinSet) : ∃ (l : Array A) (\Pi (a : A) -> ∃ (i : Fin l.len) (l i = a))
+      => TruncP.map A.finSurj $ \lam (f,p) => (f,p)
+
+    \lemma KFin+Dec=>Fin (A : KFinSet) {d : DecSet A} : FinSet A
+      => \case toArray A \with {
+        | inP (l,q) =>
+          \let l' => nub l
+          \in FinSet.fromArray l' (\lam a => TruncP.map (q a) $ \lam p =>
+              \let t => nub-isSruj l p.1
+              \in (t.1, t.2 *> p.2)) (nub-isInj l)
+      }
+  }