Короче говоря
В вашем фрагменте кода есть несовместимость типов, а именно, что (x NotLessThan y) является типом, а не значением типа (x NotLessThan y), которое вы должны предоставить для своей функциичтобы быть правильным.Следующие фрагменты исправляют проблему:
sub : (m n : ℕ) → (a : m NotLessThan n) → ℕ
sub .zero .zero ZERO = zero
sub .(suc n) .zero SUC n ZERO = suc n
sub .(suc m) .(suc n) (STEP m n a) = sub m n a
В длинных
Это основная проблема в вашем коде, но есть также несколько неточностей, которые не позволяют вам написать правильный код.Вот они:
Ваше имя типа данных _NotLessThan_ может быть несколько улучшено, чтобы лучше соответствовать математическим понятиям (и соответствовать тому, что вы найдете в стандартной библиотеке).
Обычно конструкторы пишутся не заглавными буквами.
Вы предоставляете два конструктора ZERO и SUC_ZERO, которые имеют одинаковое назначение, то естьчто любое натуральное число больше или равно нулю.Они могут быть разложены на множители.
Ваш второй конструктор SUC_ZERO содержит подчеркивание, которое Agda интерпретирует как место, где будет размещен параметр для этого конструктора.Я чувствую, что это не было задумано, и в этом случае вам определенно следует избегать подчеркивания в именах конструкторов.
В вашей функции sub вы разделяете регистр на две естественные переменные, хотя третьяАргумент (доказательство того, что a больше, чем b) уже содержит необходимую информацию для выполнения вычислений.Вместо этого сопоставление с образцом по этому аргументу также позволит избежать любых пустых случаев.
Принимая во внимание эти замечания, приведем следующее определение для вашего типа данных:
data _≤_ : ℕ → ℕ → Set where
z≤s : ∀ {a} → zero ≤ a
s≤s : ∀ {a b} → a ≤ b → suc a ≤ suc b
ОтВ этом типе данных подфункция записывается очень естественно:
sub' : ∀ a b → b ≤ a → ℕ
sub' a .zero z≤s = a
sub' ._ ._ (s≤s p) = sub' _ _ p
Обратите внимание, что в этом фрагменте подчеркивания (и точки в левой части определения) используются для обозначения параметров, значение которых может быть выведено с помощьюAgda, который делает очевидным тот факт, что доказательство является достаточным для вычисления вычитания.
Чтобы пойти дальше
Это может быть интересно, чтобы Agda вычисляла только доказательство вместо того, чтобы предоставлять его всякий раз, когдаВы хотите сделать вычитание.Чтобы сделать это, ваш тип данных должен быть доказуемо разрешимым, что означает, что, учитывая два натуральных числа a и b, должна быть написана функция, которая либо вычисляет доказательство того, что a ≤ b, либо отрицаниеЭто.Это требует нескольких шагов, первым из которых является определение логического ложного (пустой тип):
data ⊥ : Set where
Из этого типа данных может быть определено логическое отрицание:
¬ : Set → Set
¬ A = A → ⊥
Теперь мы можем определить тип разрешимых типов (примерно, это может быть доказано как истинное или ложное):
data Dec (A : Set) : Set where
yes : A → Dec A
no : ¬ A → Dec A
Затем мы можем доказать, что для любого ввода, меньший или равный тип данных является разрешимым относительноэто определение:
_≤?_ : ∀ a b → Dec (a ≤ b)
zero ≤? b = yes z≤s
suc a ≤? zero = no (λ ())
suc a ≤? suc b with a ≤? b
suc a ≤? suc b | yes p = yes (s≤s p)
suc a ≤? suc b | no ¬p = no λ {(s≤s q) → ¬p q}
Чтобы инкапсулировать регистр ошибок для вычитания, нам нужна монада возможно, которая либо и регистр ошибок, либо значение:
data Maybe (A : Set) : Set where
nothing : Maybe A
just : A → Maybe A
Наконецмы можем написать вычитание, которое принимает два натуральных числа, проверяет, удовлетворяет ли требование для вычитания, возвращает ошибку, если нет, и вычисляет ее, когда это возможно:
_-M_ : (a b : ℕ) → Maybe ℕ
a -M b with b ≤? a
a -M b | yes p = just (sub' a b p)
a -M b | no _ = nothing
В качестве примера ошибки здесьнеправильное вычитание:
error : Maybe ℕ
error = suc (suc (zero)) -M (suc (suc (suc (suc (suc (suc zero))))))
Вот что дает Агда при оценке error:
nothing
В качестве примера успеха приведем звуковое вычитание:
success : Maybe ℕ
success = (suc (suc (suc (suc (suc (suc zero)))))) -M suc (suc (zero))
Вот что дает Агда при оценке success:
just (suc (suc (suc (suc zero))))
Обратите внимание, что все эти величины (вплоть до определения, возможно, типа данных) можно найти в стандартной библиотеке,и что я сознательно опустил вселенские уровни при их представлении.