BT
Ну sub 0 m тождественно 0
Вот
Size: a a a
2020 November 08
S
Если мы о нат числах
Почему?
BT
Это вообще не имеющее смысла выражение
Почему же
BT
Эти два тоже доказуемы
М
Ну ты не можешь из 3 зайцев убить 5
BT
Ну ты не можешь из 3 зайцев убить 5
Короче, у тебя на выходе натрусльное число всегда получается, то есть меньше нуля не может быть
S
Мы же говорим о корректности объявленной функции. Которая, по условию, возвращает 0 при попытке вычесть из нуля что-то
BT
3-5=0
Тождественно
Тождественно
S
И ты на любых числах рекурсивно её вызываешь, выкидывая сукцессоры, т. е делая аргумент n -1 и агрумент m - 1
М
В
да как угодно ебать
В
даже просто через запись
S
Так у нас функция же, мы пытаемся относительно неё леммы доказать. Она не может вернуть не натуральное число
S
Но это не доказано
М
Ты не можешь ей даже предложить такой вариант не оперируя целыми числами над множеством натуральных
S
Могу. Прочитай ещё раз.
Тут паттернматчинг
Если мы получили 0, m => 0
Если мы получили n, 0 => n
Иначе => sub n - 1, m - 1
fun sub :: "nat ⇒ nat ⇒ nat"
where
"sub 0 m = 0" |
"sub n 0 = n" |
"sub (Suc n) (Suc m) = sub n m"
Тут паттернматчинг
Если мы получили 0, m => 0
Если мы получили n, 0 => n
Иначе => sub n - 1, m - 1
S
Suc - это конструктор натуральных чисел. Suc 0 будет 1, Suc ( Suc 0 ) будет 2, и так далее
S
Мы оперируем конструкторами числа, а не числами
S
И он справлдлив только для натуральных чисел
S
Вот, например, доказательство сложения двух натуральных чисел
theory Add
imports Main
begin
fun add :: "nat ⇒ nat ⇒ nat"
where "add 0 n = n" |
"add (Suc n) m = Suc (add n m)"
lemma support1[simp]: "add n 0 = n"
apply (induction n)
apply auto
done
lemma support2[simp]: "Suc (add y x) = add y (Suc x)"
apply (induction y)
apply auto
done
lemma "add x y = add y x"
apply (induction x)
apply auto
done
end