Idrisでは、どのようにしてSo型から証明を抽出しますか？

Question

私はこのうち(x < y)の証明を抽出するにはどうすればよい

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

のようなものが作成したSo (x < y)ようSoタイプを、持っている場合は？私はこれのための標準ライブラリで関数を見つけることができません。

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 

私はそうイドリスはSo (S x < S y)とSo (x < y)はdefinitionally同じであることを見ることができなかったのでltで<を交換しなければなりませんでした。

最初の句と最後の句には、Soでエンコードされた情報を使用していることを確認してください。

Answer 2

それはそうですブール値から証明を抽出することはできません。 Soは弱いタイプです。実行時にいくつかのチェックのパフォーマンスを保証するためにのみ使用してください。

So: what's the point?

私はそれは不可能ですわからない。また、この質問を参照してください。しかし、私はltNeNatを証明しようとし、惨めに失敗しました。しかし、多分私はばかだ。 Reflのように、Soの代わりにいくつかの証拠を使用することを検討してください。 Soのパターンマッチングでは、証明に役立つより多くのパワーはありません。有効なユースケースはSoで、this tutorialの下にあります。 Soから証明書を抽出することができても、多くのコードが必要で、Soを扱うのはあまり便利ではありません。