Prove So (0 < m) -> (n ** m = S n)

Question

I'm trying to make an Idris function of type (j : Nat) -> {auto p : So (j < n)} -> Fin n to convert a Nat into a Fin n. To get the Z case to work (and output FZ), I'm trying to prove that a proof of 0 < n is sufficient to be able to make FZ : Fin n. But I can't work out how to do this.

I'm open to making a completely different function, as long as it can convert Nat values into Fin n values (where they exist). My goal is to have some other function that can convert any Nat into a Mod n value, so that, for example, 15 : Nat is mapped to 3 : Mod 4. My Mod type currently has a single constructor, mkMod : Fin n -> Mod n.

Answer 1

After learning about LT : Nat -> Nat -> Type, I took a different approach. I started with the declaration:

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n
natToFin {n} j {p} = ?natToFin_rhs_1

. Case-splitting on n, then on p in the n = Z case resulted in:

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n
natToFin {n = (S k)} j {p = p} = ?natToFin_rhs_2

, which is essentially the proof I was asking for. From there, I case-split on j and filled the zero case, leaving:

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n
natToFin {n = (S k)} Z = FZ
natToFin {n = (S k)} (S j) {p = p} = ?natToFin_rhs_3

. I wanted to fill ?natToFin_rhs_3 with FS (natToFin j), but the type checker wasn't letting me. However, after a case split on p, it was fine:

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n
natToFin {n = (S k)} Z = FZ
natToFin {n = (S k)} (S j) {p = (LTESucc x)} = FS (natToFin j)

Finally, I added total, and it all checked out.

---

The only problem now is that Idris can't seem to find LT proofs automatically. This is what happens:

λΠ> the (Fin 6) (natToFin 2)
When elaborating argument p to function mod2.natToFin:
        Can't solve goal 
                LT (fromInteger 2) (fromInteger 6)

Is there any way to fix that?