在伊德里斯，我如何从一个类型中提取证据？

Question

如果我有一个So的类型，比如So (x < y)，通过创造的东西像

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

我怎样才能提取(x < y)证明了这件事？我无法在标准库中找到此功能。

So在标准库中定义为：

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

而且我不知道如何从提取的证据，用于在证明这样的：

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

Answer 1

您可以通过感应上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 

我有lt更换<否则伊德里斯看不出So (S x < S y)和So (x < y)是definitionally相等。

注意到我在第一个和最后一个条款中使用了编码在So中的信息。

Answer 2

似乎就像你不能从布尔值中提取证据一样。 So是弱类型。它应该仅用于保证在运行时进行一些检查的性能。也看到了这个问题：

So: what's the point?

我不知道这是不可能的。但我试图证明ltNeNat并惨败。虽然，也许我只是愚蠢的。考虑使用一些证据而不是So，如Refl。 So上的模式匹配不会为您提供更多帮助证明事物的力量。您可以在this tutorial下找到So的有效用例。即使您能够从So中提取证据，它也需要您提供大量代码，处理So不太方便。