How to rewrite term in type signature for proof in Idris?

Question

Basically, I want to prove that either n - m or m - n is equal to zero in Recursive Arithmetic. To accomplish this I have been trying to use a rewrite ... in ... pattern without sucess.

The following is the base code:

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

However, when inspecting the first two holes

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

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

The only way I have been able to move forward is with a lemma in data AlgunoEsCero; the way forward from what I have read would be to rewrite the type using another theorem like

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

So then it would be easy to point out which of the two minus is going to be zero and build the datatype with something like rewrite cero_menos_algo_es_cero in IzquierdoEsCero. However that spits out:

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)

Any resource pointers would be appreciated. (Haven't been able to find good points in Type Driven Development nor on the documentation; maybe I am misunderstanding rewrite / proofs in general)

Answer 1

You just need to pattern-match one more time to finish the proof:

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

Also, if you defined your subtraction function as

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

(notice that I pattern-match on the first argument, as opposed to your version with starts pattern-matching on the second one), then the proof of alguna_resta_es_cero would mimic the structure of the function more closely:

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