Не удалось решить ограничения: (k ≤ 5) x (k * 2 ≡ 5). Как я мог заставить это работать?
Я новичок в Agda и пытаюсь доказать, что 5 — простое число :).
Сейчас я пытаюсь отмахнуться от того, что 2 является делителем 5. У меня есть:
p1 : k * 2 ≡ 5
p2 : k ≤ 5
Теперь я надеюсь, что соответствие шаблону будет выглядеть так:
case (p2 ,′ p1 ) of λ where ()
проверил бы тип, так как выполняются 6 условий p2 и ни одно из них не выполняется p1. Не похоже, что вычислительный бюджет должен быть превышен так быстро, не так ли?
Есть ли способ заставить это работать? Как еще я могу продолжить с p1 и p2 и вообще: как доказать, что 5 — простое число или что 2 его не делит?
Agda не пытается выполнить поиск доказательств, вам придется либо вручную направлять ее, как в ответе @NaïmFavier, либо использовать решатель, такой как Schmitty.
Ответы 1
Попробуем определить следующее:
goal : ∀ k → (k ≤ 5) × (k * 2 ≡ 5) → ⊥
Если мы просто свяжем все переменные, мы получим
Goal: ⊥
y : k * 2 ≡ 5
x : k ≤ 5
k : ℕ
Хотя мы видим, что это абсурдно, Agda не может: каждая из посылок возможна изолированно, и Agda не собирается проверять все возможные значения k, потому что не знает, когда остановиться. Поэтому мы должны направлять его, разделяя соответствующий случай. Давайте посмотрим, что произойдет, если мы один раз разделимся на k:
goal (suc k) (x , y) = {! !}
Теперь Агда смогла отбросить случай zero как абсурдный, потому что в этом случае мы имеем y : zero ≡ suc (suc (suc (suc (suc zero)))), что невозможно. У нас остался случай suc k, который еще не является абсурдным. Давайте разделимся на k еще два раза:
goal (suc (suc zero)) (x , y) = {! !}
goal (suc (suc (suc k))) (x , y) = {! !}
Теперь Агда видит, что оба эти случая абсурдны, потому что в первом мы имеем y : 4 ≡ 5, а во втором — y : 6 + k * 2 ≡ 5, что сводится к suc (k * 2) ≡ zero. Однако мы не можем просто отбросить оба случая, потому что Agda должна знать, что ей следует произвести такое разделение. Таким образом, самое простое определение, которое работает, это
goal : ∀ k → (k ≤ 5) × (k * 2 ≡ 5) → ⊥
goal 2 ()
Agda создаст дерево случаев, включающее 2, и увидит, что каждый случай абсурден (это также будет работать и с большим числом). Обратите внимание, что мы не использовали аргумент k ≤ 5.
Более принципиальным подходом было бы использование доказательства путем размышления: например, если вы можете доказать, что делимость натуральных чисел разрешима, то это доказательство также станет эффективной процедурой принятия решения о делимости. Затем вы можете спросить Агду, делит ли 2 5, и извлечь доказательство из (отрицательного) ответа.
Эй, спасибо, но я вообще ничего не понимаю. Что также работает, так это если я сопоставляю шаблон только с s<=s (s<=s z<=n). Как это работает, если это не единственный способ, которым число может быть меньше 5? Как это может работать, если я перечислю только один шаблон и почему он работает с любым шаблоном из группы?
Агда может знать, что второй шаблон абсурден только тогда, когда k равен 0, 1, 2 или имеет форму suc (suc (suc m)), поэтому вам нужно направить его, чтобы каким-то образом осуществить это разделение. Честно говоря, у меня не очень хорошая ментальная модель абсурдных закономерностей, и я нашел ее более или менее методом проб и ошибок. Более принципиальным подходом было бы использование доказательства посредством размышления , см. эту суть, например.
но только ли это из-за глубины поиска? Потому что 1) когда k равно 4, это не тот случай, когда 4 * 2 равно 5, точно так же это не так для 0, 1 и 2, верно? И 2) в этом шаблоне по умолчанию допустимо также k = 4 или 5. Если Agda может закрыть это дело, почему она борется с 0, 1, 2? Поскольку я также пробовал использовать другое количество конструкторов s<=s, я предполагаю, что, сделав этот хак, мы упростим для agda поиск в пространстве - НО если да, то а) я не понимаю, почему б) я бы хотел параметризуйте компилятор с большим бюджетом для поиска. Спасибо
Бюджета на увеличение нет, Agda по умолчанию не выполняет поиск доказательств. Я отредактировал свой ответ более подробно.
большое спасибо. Итак, я получил то, что agda проверяет, что одиночный шаблон пуст, если это так. Но если шаблон не изолирован изолированно, а является совокупностью нескольких шаблонов, то agda не выполняет никакого поиска, чтобы это выяснить. Кстати, когда вы написали «самый простой случай, который работает», вы имели в виду, что это повторяется не только для k=2, но и для k=3, k=1 и так далее, верно? Спасибо
Нет, всего лишь одного числа (≥ 2) достаточно, чтобы сказать Агда, насколько глубоко она должна разделиться, и тогда любая другая ветвь в дереве случаев будет абсурдной.
case ( p2 ) of λ where p2' -> case ( p1 ) of λ where ()тоже не работает