In Idris, how do I extract a proof from a So type?

Question

If I have a So type, like So (x < y), created by something like

IsLt : Ord a => (x: a) -> (y: a) -> Type
IsLt x y = So (x < y)

How can I extract the proof of (x < y) out of this? I can't find a function in the standard library for this.

So is defined in the standard library as:

data So : Bool -> Type where 
    Oh : So True

And I'm not sure how to extract the proof from that, for use in proving something like:

ltNeNat : {x: Nat} -> {y: Nat} -> So (x < y) -> Not (x = y)

Answer 1

You can prove the lemma by induction on x:

ltNeNat : {x: Nat} -> {y: Nat} -> So (lt x y) -> Not (x = y)
ltNeNat {x = Z} {y = Z} Oh _ impossible
ltNeNat {x = Z} {y = S _} _ Refl impossible
ltNeNat {x = S x} {y = Z} so Refl impossible
ltNeNat {x = S x} {y = S y} so eq =
  let IH = ltNeNat {x} {y} so in
  IH $ succInjective _ _ eq

I had to replace < with lt because otherwise Idris couldn't see that So (S x < S y) and So (x < y) are definitionally equal.

Observe that I used information encoded in So in the first and the last clauses.