Proof of constructive stone: finite sets (http://math.andrej.com/2009/09/07/constructive-stone-finite-sets/) in Idris

nodupListingLEM.idr

import Data.Fin
import Data.List

%default total

Surjective : {A,B:Type} -> (A -> B) -> Type
Surjective {A} {B} f = (y:B) -> (x:A ** f x = y)

||| A listing of size n of a type A is a surjective map from the first n numbers
||| to A. If such a listing exists, then A is finite.
data Listing : Nat -> Type -> Type where
  MkListing : {A:Type} ->
              (n:Nat) ->
              (f : Fin n -> A) ->
              Surjective f ->
              Listing n A

||| Get the ith element from a listing.
apl : {A:Type} -> Listing n A -> Fin n -> A
apl (MkListing _ f _) i = f i

||| If f i = f j implies i = j then f has no duplicates.
data NoDup : {A:Type} -> Listing n A -> Type where
  MkNoDup : {A:Type} ->
            (f : Listing c A) ->
            ((i,j : Fin c) -> apl f i = apl f j -> i = j) -> NoDup f

||| Trick A has 1 inhabitant if A is uninhabited
||| otherwise there are more inhabitants.
data Trick : Type -> Type where
  FreeTrick   : {A : Type} -> Trick A
  CostlyTrick : {A : Type} -> A -> Trick A

||| Computational law of excluded middle. Implementing this should be
||| impossible.
LEM : Type
LEM = (A:Type) -> Dec A

lemma0 : Fin 0 -> Void
lemma0 FZ     impossible
lemma0 (FS _) impossible

||| The inhabitant of Fin 1 is unique.
covering lemma1 : (i,j:Fin 1) -> i = j
lemma1 FZ FZ = Refl
lemma1 FZ (FS FZ)      impossible
lemma1 (FS FZ) FZ      impossible
lemma1 (FS FZ) (FS FZ) impossible

lemma2 : FreeTrick = CostlyTrick x -> Void
lemma2 Refl impossible

||| 0 does not equal 1 in Fin.
lemma3 : FZ = FS FZ -> Void
lemma3 Refl impossible

||| Assume x:A. By surjection we get two indexes for FreeTrick and CostlyTrick x.
||| The indexes are both of type Fin 1, so must be equal. But that would make
||| FreeTrick and CostlyTrick x equal, which is impossible.
single : {A:Type} -> A -> (f : Fin 1 -> Trick A) -> Surjective f -> Void
single x f surj =
  let (i ** p) = surj FreeTrick in
  let (j ** q) = surj (CostlyTrick x) in
  let iej = lemma1 i j in
  let p2 = sym p in
  let p3 = replace {P = \x => FreeTrick = f x} iej p2 in
  let p4 = trans p3 q in
  lemma2 p4

||| Assume a no-dup listing of Trick A has size at least 2. The first two
||| elements must be different. At most one of them can be the A-less FreeTrick.
||| The other trick must contain an A.
over1 : {A:Type} ->
       (f : Fin (S (S n)) -> Trick A) -> 
         ((i,j:Fin (S (S n))) -> f i = f j -> i = j) -> A
over1 f g with (f 0) proof p1
  over1 f g | FreeTrick with (f 1) proof p2
    over1 _ g | FreeTrick | FreeTrick = let q0 = sym p1 in
                                        let q1 = trans q0 p2 in
                                        let bomb = lemma3 (g 0 1 q1) in
                                        absurd bomb
    over1 _ _ | FreeTrick | CostlyTrick x = x
  over1 _ _ | CostlyTrick x = x

||| If the listing has size 1 then A is uninhabited.
|||
||| If the listing has size greater than 1 then A is inhabited.
doTheTrick : (A:Type) -> (n:Nat) -> (l:Listing n (Trick A)) -> NoDup l -> Dec A
doTheTrick A n (MkListing _ f surj) (MkNoDup _ info) = case n of
  -- n can't be zero, Trick A has at least one inhabitant
  Z       => let (bomb ** _) = surj FreeTrick in absurd bomb
  -- n = 1 so A must be uninhabited
  S Z     => No (\myA => single myA f surj)
  -- n > 1 so f 0 or f 1 must contain an A, or else f 0 and f1 are duplicates
  S (S _) => Yes (over1 f info)

||| If any finite type has a listing with no duplicates, then you have
||| law of excluded middle.
|||
||| After fixing the type... this can't be proved as such.
nodupListingLEM : ((A:Type) -> Listing n A -> (l : Listing n A ** NoDup l)) -> LEM
nodupListingLEM hyp B = ?cantBeDoneNow