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

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