如何在 Idris 中重写类型签名中的术语以进行证明？

Question

基本上，我想证明n - m 或m - n 在递归算术中等于零。为了做到这一点，我一直在尝试使用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

您只需再进行一次模式匹配即可完成证明：

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

另外，如果您将减法函数定义为

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

（请注意，我在第一个参数上进行模式匹配，而不是您的版本在第二个参数上开始模式匹配），然后 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