Как переписать термин в подписи типа для доказательства в Идрисе?

По сути, я хочу доказать, что либо 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)

Любые указатели ресурсов будут оценены. (Не удалось найти хороших моментов ни в Type Driven Development, ни в документации; возможно, я неправильно понимаю rewrite/доказательства в целом)


idris proof-of-correctness
person Fabián Heredia Montiel    schedule 11.09.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вам просто нужно сопоставить шаблон еще раз, чтобы закончить доказательство:

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
person Anton Trunov    schedule 11.09.2017
comment
Привет, я просто хотел бы задать второй вопрос. Если он проверит эти изменения, то доказательство будет завершено, верно? - person Fabián Heredia Montiel; 11.09.2017
comment
Пока вы используете %default total в исходном файле или помечаете функции и доказательства как total. - person Anton Trunov; 11.09.2017
comment
При условии, что реализация Idris верна, а теория верна :) - person Anton Trunov; 11.09.2017