Idrisの証明のためにタイプシグネチャの用語を書き換えるには？

Question

基本的には、再帰算術でn - mまたはm - nのいずれかがゼロに等しいことを証明したいと思います。これを達成するために、私は成功なしでrewrite ... in ...パターンを使用しようとしています。

以下は、基本コードである：最初の二つの穴

- + Main.hoyo1 [P] 
`--   m : Natural 
    ----------------------------------------- 
     Main.hoyo1 : AlgunoEsCero (resta C m) m 

- + Main.hoyo2 [P] 
`--   n : Natural 
    ----------------------------------------- 
     Main.hoyo2 : AlgunoEsCero n (resta C n) 

を検査する際

data Natural = C | S Natural 

resta : Natural -> Natural -> Natural 
resta a  C  = a 
resta C  b  = C 
resta (S a) (S b) = resta a b 

data AlgunoEsCero : (n, m : Natural) -> Type where 
    IzquierdoEsCero : AlgunoEsCero C m 
    DerechoEsCero : AlgunoEsCero n C 

alguna_resta_es_cero : (n, m: Natural) -> AlgunoEsCero (resta n m) (resta m n) 
alguna_resta_es_cero C  m  = ?hoyo1 
alguna_resta_es_cero n  C  = ?hoyo2 
alguna_resta_es_cero (S n) (S m) = ?hoyo3 

しかし、私は前方に移動することができた唯一の方法は、data AlgunoEsCeroに補題です。前方に私が読んだものから、方法は、ゼロになるだろう2のどちらマイナス指摘し、何かを持つデータ型を構築することは簡単だろうだから、

cero_menos_algo_es_cero : (m: Natural) -> resta C m = C 
cero_menos_algo_es_cero C  = Refl 
cero_menos_algo_es_cero (S m) = Refl 

のような別の定理を使ってタイプを書き換えることであろうrewrite cero_menos_algo_es_cero in IzquierdoEsCeroのように。しかし、それは吐き出す：

When checking right hand side of alguna_resta_es_cero with expected type 
      AlgunoEsCero (resta C m) (resta m C) 

    _ does not have an equality type ((m1 : Natural) -> resta C m1 = C) 

すべてのリソースポインタがあります。 （タイプ駆動開発にも文書で良い点を見つけることができませんでした。多分、私は一般的にrewrite /証明を誤解しています）

Answer 1

あなただけの証拠を完了するために、パターンマッチに1人のより多くの時間を必要とする：

あなたは

resta : Natural -> Natural -> Natural 
resta C  b  = C 
resta a  C  = a 
resta (S a) (S b) = resta a b 

としてあなた減算機能を定義した場合

alguna_resta_es_cero : (n, m: Natural) -> AlgunoEsCero (resta n m) (resta m n) 
alguna_resta_es_cero C C = IzquierdoEsCero 
alguna_resta_es_cero C (S x) = IzquierdoEsCero 
alguna_resta_es_cero (S x) C = DerechoEsCero 
alguna_resta_es_cero (S x) (S y) = alguna_resta_es_cero x y 

また、その後、（1秒にパターンマッチングを開始して、あなたのバージョンとは反対に、最初の引数にそのIパターンマッチに注目してください） alguna_resta_es_ceroは、関数の構造をより詳しく模倣するでしょう：

alguna_resta_es_cero : (n, m: Natural) -> AlgunoEsCero (resta n m) (resta m n) 
alguna_resta_es_cero C m = IzquierdoEsCero 
alguna_resta_es_cero (S x) C = DerechoEsCero 
alguna_resta_es_cero (S x) (S y) = alguna_resta_es_cero x y