Я не могу доказать (n - 0) = n с Идрисом

Я пытаюсь доказать, что на мой взгляд является разумной теоремой: 

theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m
Доказательство индукцией доходит до точки, где мне нужно доказать это: 
lemma1 : (n : Nat) -> (n - 0) = n
Вот что происходит, когда я пытаюсь доказать это (лемму, для простоты) с помощью интерактивного пословицы: 
----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n

> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n

> trivial
Can't unify
        n = n
with
        minus n 0 = n

Specifically:
        Can't unify
                n
        with
                minus n 0

Мне показалось, что я что-то упустил в определении минуса, поэтому я поискал его в источнике: 

||| Subtract natural numbers. If the second number is larger than the first, return 0.
total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right
Определение, которое мне нужно, прямо здесь! minus left Z = left. Насколько я понял, это был Идрис. следует просто заменить minus m 0 на m здесь, и это тогда рефлексивно верно. Что я пропустил?
4 14
proof

4 ответа:

К сожалению, теорема, которую вы хотите доказать здесь, на самом деле не верна, потому что Idris naturals усекает вычитание при 0. Контрпример к вашему theorem1 - это n=3, m=0. Давайте пройдем через оценку:

Сначала подставим: 

3 + (0 - 3) = 0

Далее мы десугарируем синтаксис к нижележащему экземпляру Num и помещаем в него собственно вызываемые функции: 

plus (S (S (S Z))) (minus Z (S (S (S Z))))) = Z

Idris-это строгий язык вызовов по значениям, поэтому сначала мы оцениваем аргументы функций. Таким образом, мы уменьшите выражение minus Z (S (S (S Z)))). Глядя на определение minus, первый паттерн применим, потому что первый аргумент - Z. Итак, мы имеем: 

plus (S (S (S Z))) Z = Z

plus является рекурсивным по своему первому аргументу, поэтому следующий шаг вычисления дает: 

S (plus (S (S Z)) Z) = Z

Мы продолжаем этот путь до тех пор, пока plus не получит Z в качестве своего первого аргумента, после чего он возвращает свой второй аргумент Z, давая тип: 

S (S (S Z)) = Z

Которого мы не можем построить жителя для.

Извините, если вышесказанное показалось немного педантичным и низкоуровневым, но очень важно учитывать конкретные шаги сокращения при работе с зависимыми типами. Это вычисления, которые вы получаете "бесплатно" внутри типов, поэтому хорошо организовать их так, чтобы они давали удобные результаты.

Однако решение Pdxleif, приведенное выше, хорошо работает для вашей леммы. Разбиение кейса на первый аргумент было необходимо, чтобы получить соответствие паттерна в minus для работы. Помните, что она продолжается сверху вниз в шаблоне совпадений, и первый шаблон имеет конкретный конструктор на первом аргументе,что означает, что сокращение не может продолжаться, пока он не знает, соответствует ли этот конструктор.
22

Просто поиграл с интерактивным редактированием, сделал разбиение кейса и поиск доказательств, дает: 

lemma1 : (n : Nat) -> (n - 0) = n
lemma1 Z = refl
lemma1 (S k) = refl

Это очевидно из определения минуса, поэтому оно просто refll. Может быть, он отказывался, когда входной var был просто n, потому что он мог бы иметь другое поведение, если бы это был Z или что-то еще? Или рекурсия?

10

На всякий случай, многие арифметические леммы уже определены в прелюдии Идриса, как и Ваша: 

total minusZeroRight : (left : Nat) -> left - 0 = left
minusZeroRight Z        = refl
minusZeroRight (S left) = refl
1

Для полноты картины (язык тактики был отвергнут в пользу рефлексии разработчика) я добавлю, что способ доказать вашу лемму на языке тактики-это вызвать induction n. Затем вы можете использовать trivial, чтобы показать каждый случай (после intros в индуктивном случае).

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n
-lemma1> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n
-lemma1> induction n
----------              Other goals:              ----------
elim_S0,{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
elim_Z0 : minus 0 0 = 0
-lemma1> trivial
----------              Other goals:              ----------
{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
elim_S0 : (n__0 : Nat) ->
          (minus n__0 0 = n__0) -> minus (S n__0) 0 = S n__0
-lemma1> intros
----------              Other goals:              ----------
{hole8},elim_S0,{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
 n__0 : Nat
 ihn__0 : minus n__0 0 = n__0
----------                 Goal:                  ----------
{hole9} : minus (S n__0) 0 = S n__0
-lemma1> trivial
lemma1: No more goals.
-lemma1> qed
Proof completed!
lemma1 = proof
  intros
  induction n
  trivial
  intros
  trivial
1