Как я могу доказать абсурд с помощью coq?

Я читаю «Логические основы» из серии «Основы программного обеспечения» и увидел plus_id_example, то есть:

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

Proof.
  intros n m.
  intros H.
  rewrite H.
  reflexivity.  Qed.

Я мог понять решение, поэтому я попытался решить его, используя абсурд, я хочу сделать следующее:

Давайте считать абсурдным, что n+n <> m+m, поэтому у нас есть 2n <> 2m, n <> m, что является противоречием, поскольку у нас есть n=m в качестве нашей гипотезы.

Как я мог написать это, используя тактику Coq?

Если вы не хотите использовать какие-либо причудливые леммы/тактики, я не думаю, что вы можете избежать какой-либо формы переписывания в своем доказательстве (на шаге, где вы хотите перейти от 2n <> 2m к n = m), и поэтому вы получите доказательство по крайней мере такой же сложный, как у Software Foundation. В общем, в такого рода лёгких примерах рассуждения от противного — это всего лишь способ скрыть прямое рассуждение, так что в итоге вы проделаете те же шаги, только спрятанные за отрицаниями.

Meven Lennon-Bertrand 12.05.2022 09:37

Эй, спасибо за руководство, но на самом деле это было моей целью, я новичок в Coq и дискретной математике в целом, поэтому, пока я читал этот пример, я подумал: «Эй, как я могу использовать абсурд в этом случае, чтобы доказать это» в качестве способ развить свои навыки

udduu 12.05.2022 21:28
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
0
2
48
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Вы можете использовать одну из многих основанных на противопоставлении лемм в Coq: вы можете увидеть их, используя, например, Search "contra". в Coq.

Используя тактический язык ssreflect, доказательство, основанное на этой идее, можно получить следующим образом (я уверен, что должны быть более короткие доказательства):

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.
Proof.
  move=> n m.
  apply: contra_eq.
  have twice : forall p, p + p = p * 2.
    move=> p.
    by rewrite -iter_addn_0 /= addn0.
  by rewrite !twice eqn_mul2r.
Qed.  

Является ли использование SSreflex самым простым способом? Поскольку я новичок в Coq, я хотел бы попробовать его, используя встроенную тактику.

udduu 12.05.2022 03:20

Я обнаружил, что SSReflect легче понять, как новичок, чем стандартный язык тактики Coq. Конечно, это субъективно.

Pierre Jouvelot 12.05.2022 10:25

Я забыл упомянуть, что связь между некоторыми утверждениями и булевыми выражениями, которая лежит в основе механизма отражения, лежащего в основе SSReflect, позволяет простым образом выразить многие противоположительные леммы, такие как contra_eq.

Pierre Jouvelot 12.05.2022 15:17

Другие вопросы по теме