2

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)
Shersh
  • 9,019
  • 3
  • 33
  • 61
LogicChains
  • 4,332
  • 2
  • 18
  • 27

2 Answers2

3

It seems like you can't extract proof from boolean value. So is weak type. It's should be used only to guarantee performance of some checks at runtime. Also see this question:

So: what's the point?

I'm not sure it's not possible. But I tried to prove ltNeNat and failed miserably. Though, maybe I'm just stupid. Consider using some evidence instead of So, like Refl. Pattern matching on So doesn't give you more power that helps proving things. You can find valid use cases of So under this tutorial. Even if you're able to extract proofs from So it requires a lot of code from you and dealing with So is less convenient.

Shersh
  • 9,019
  • 3
  • 33
  • 61
3

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
  • That's true. I'm stucked at proving `S x < S y = True -> x < y = True` because booleans don't really help to prove things. – Shersh Jul 03 '17 at 13:47
  • 1
    You need to "reflect" booleans into propositions. ssreflect (of Coq ecosystem) uses it extensively. This way you get to use logic and computations -- this is very useful when dealing with decidable propositions. – Anton Trunov Jul 03 '17 at 15:07