Доказательство натурального (n) - ноль - PullRequest
Новая
       25

Доказательство натурального (n) - ноль

1 голос
/ 07 октября 2019

Я пытаюсь выучить парадигму идриса и все еще борюсь. Здесь у меня есть функция isZero, которая принимает естественный Nat и возвращает True или False.

Моя проблема связана с нерелексивным случаем. 

namespace Numbers

  data Nat : Type where
    Zero : Numbers.Nat
    Successor : Numbers.Nat -> Numbers.Nat

  isZero: Numbers.Nat -> Prelude.Bool.Bool
  isZero Zero = True
  isZero _ = False

  isNotZero: Numbers.Nat -> Prelude.Bool.Bool
  isNotZero Zero = False
  isNotZero _ = True

  proofNIsZero : (n : Numbers.Nat) -> isZero n = Bool.True
  proofNIsZero Zero = Refl
  proofNIsZero (Successor _) = ?rhs

Кажется очевидным, что какой-то преемник любого нат не может быть нулем. Но моя борьба в доказательство. Тип дыры? Rhs: 

--------------------------------------
rhs : False = True

Попытка ориентироваться в том, что я думаю, должно быть (и будет однажды) простой, привела к uninhabited, Void, absurd и impossible. Ничего из этого я не могу устранить.

Возможно, это ключи - но я не могу расшифровать!

1 Ответ

3 голосов
/ 07 октября 2019

Я отвечаю, поскольку мне кажется, что я понял, что, вероятно, приведенное выше доказательство не было сформулировано правильно. Я добавил утверждение, в котором утверждается n = Zero, что позволяет isZero n = Bool.True иметь значение. n = Zero переносится как prf и позволяет мне объявить absurd prf как isZero n = Bool.True, который не может быть истинным, если n равен Successor некоторым Nat. 

  Uninhabited (Successor _ = Zero) where
    uninhabited Refl impossible

  proofNIsZero : (n : Numbers.Nat) -> n = Zero -> isZero n = Bool.True
  proofNIsZero Zero prf = Refl
  proofNIsZero (Successor _) prf = absurd prf

Есть лидругой подход или способ думать об их определении, чтобы не попасться в ловушку?

...