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

Question

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

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

Answer 1

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

Во-первых, мы подставим:

3 + (0 - 3) = 0 

Далее мы desugar синтаксис для базового экземпляра Num, и поместить в реальных функций, вызываемых:

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

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

Answer 2

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

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

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

Answer 3

Только в случае, много арифметических чешуй уже определен в Prelude Идриса, как ваши:

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

Answer 4

Для полноты (тактика языка является устаревшим в пользу разработчик отражения), я добавит, что способ доказать вашу лемму на тактическом языке - вызывать 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