Idris에서 증명을 위해 유형 서명에서 용어를 다시 쓰는 방법은 무엇입니까?

Question

기본적으로 n - m 또는 m - n 중 하나가 재귀 산술 연산에서 0과 같음을 증명하고 싶습니다. 이를 수행하기 위해 나는 성공없이 rewrite ... in ... 패턴을 사용하려고 노력했습니다. 처음 두 구멍을 검사 할 때, 그러나

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 

- + 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 AlgunoEsCero의 보조 정리 함께, 다음

은 기본 코드 앞으로 내가 읽은 내용의 방법은 다음이 제로가 될 것입니다 둘 중 어느 마이너스 지적하고 뭔가 데이터 유형을 구축하기 쉬울 것이다 그래서

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

당신은 증거를 마무리하는 패턴 매치에 한 번 더 시간이 필요합니다 :

당신이

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 

또한, 다음, (두 번째에 패턴 매칭을 시작으로 버전이 아닌 첫 번째 인수에 해당 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