Idris - 2つの数値の等価性を証明する

Question

2つの自然な引数をとり、それらの等価性の証明の多分を返す関数を書いてみたいと思います。

私は

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) 
equal a b = case (a == b) of 
    True => Just Refl 
    False => Nothing 

にしようとしているが、私はこれを行うには正しい方法で、次のエラー

When checking argument x to constructor Prelude.Maybe.Just: 
     Type mismatch between 
       True = True (Type of Refl) 
     and 
       Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == a 
                        b = 
       True (Expected type) 

     Specifically: 
       Type mismatch between 
         True 
       and 
         Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == a 
                          b 

を取得しますか？

また、ボーナス質問として、私がしなければ

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) 
equal a b = case (a == b) of 
    True => proof search 
    False => Nothing 

私は

INTERNAL ERROR: Proof done, nothing to run tactic on: Solve 
pat {a_504} : Prelude.Nat.Nat. pat {b_505} : Prelude.Nat.Nat. Prelude.Maybe.Nothing (= Prelude.Bool.Bool Prelude.Bool.Bool (Prelude.Interfaces.Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == {a_504} {b_505}) Prelude.Bool.True) 
This is probably a bug, or a missing error message. 
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues 

は、それが既知の問題であり得るか、私はそれを報告しなければなりませんか？

Answer 1

のはNatためEqインタフェースの実装を見てみましょう：

Eq Nat where 
    Z == Z   = True 
    (S l) == (S r) = l == r 
    _ == _   = False 

あなただけの、次のように(==)機能の構造に従うことによって問題を解決することができます

total 
equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) 
equal Z Z = Just Refl 
equal (S l) (S r) = equal l r 
equal _ _ = Nothing 

Answer 2

あなたはcase（従属パターンマッチング）の代わりにwithを使用するとできます。

equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True) 
equal a b with (a == b) 
    | True = Just Refl 
    | False = Nothing 

アントンが指摘しているように、これは単なるブール値テスト結果の証人であり、適切な平等よりも弱い主張です。それはif a==b then ...についての証拠を前進させるのに役立つかもしれませんが、bの代わりにaを代用することはできません。