Я не могу доказать (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, и тогда это рефлексивно верно. Что я пропустил?


idris proof
person Vic Smith    schedule 07.05.2014    source источник
comment
Идрис - это язык программирования с зависимой типизацией, который делает доказательства и программы синонимичными из-за изоморфизма Карри-Ховарда. Мне нужно доказать эту теорему в коде, чтобы моя функция была хорошо типизирована (я пропустил функцию, потому что ее объяснение займет ненужное место). По этой причине Idris поставляется с интерактивным прувером. Таким образом, вопрос заключается в том, как использовать язык программирования Idris, а не в самой математике.   -  person Vic Smith    schedule 07.05.2014
comment
Извините, если это очевидно, незнание языка, но просмотр некоторых примеров для этого языка - это далеко не ясно. Всегда ли 0 и Z рассматриваются как синонимы или что-то требуется для их работы?   -  person Damien_The_Unbeliever    schedule 07.05.2014
comment
Числовые литералы полиморфно перегружены, как в Haskell. Nat является членом класса Num, одной из функций которого является fromInteger. И fromInteger 0 = Z. (Для Nat также существует особая оболочка, которая присутствует в самом языке и, я думаю, в терминале.) Короче говоря, я не думаю, что это проблема, хотя я не уверен в этом полностью.   -  person Vic Smith    schedule 07.05.2014
comment
В стороне: я не думаю, что это доказуемо, как указано. Конечно, математически это имеет смысл, но минус не совсем четко определен на Naturals. Неудачный случай: если m равно нулю, а n не равно нулю, ноль минус все определяется как ноль. Таким образом, вам остается пытаться доказать (S k) + 0 = 0. Может быть, нам нужно лучшее определение минусовой операции для Nats, иначе прекратите попытки использовать их для математических доказательств.   -  person pdxleif    schedule 08.05.2014

Ответы (4)


arrow_upward
26
arrow_downward

К сожалению, теорема, которую вы хотите здесь доказать, на самом деле неверна, потому что 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

Идрис - это строгий язык вызова по значению, поэтому мы сначала оцениваем аргументы функций. Таким образом сокращаем выражение 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 работало. Помните, что он выполняется сверху вниз в соответствии с шаблоном, и первый шаблон имеет конкретный конструктор для первого аргумента, что означает, что сокращение не может продолжаться, пока он не узнает, соответствует ли этот конструктор.

person David Christiansen    schedule 08.05.2014

arrow_upward
10
arrow_downward

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

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

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

person pdxleif    schedule 08.05.2014

arrow_upward
1
arrow_downward

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

total minusZeroRight : (left : Nat) -> left - 0 = left
minusZeroRight Z        = refl
minusZeroRight (S left) = refl
person Yuuri    schedule 02.12.2014

arrow_upward
1
arrow_downward

Для полноты (тактический язык устарел в пользу рефлексии разработчика), я добавлю, что способ доказать вашу лемму на тактическом языке - это вызвать 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
person ballesta25    schedule 02.11.2015