Я читаю «Логические основы» из серии «Основы программного обеспечения» и увидел 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?
Эй, спасибо за руководство, но на самом деле это было моей целью, я новичок в Coq и дискретной математике в целом, поэтому, пока я читал этот пример, я подумал: «Эй, как я могу использовать абсурд в этом случае, чтобы доказать это» в качестве способ развить свои навыки
Вы можете использовать одну из многих основанных на противопоставлении лемм в 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, я хотел бы попробовать его, используя встроенную тактику.
Я обнаружил, что SSReflect легче понять, как новичок, чем стандартный язык тактики Coq. Конечно, это субъективно.
Я забыл упомянуть, что связь между некоторыми утверждениями и булевыми выражениями, которая лежит в основе механизма отражения, лежащего в основе SSReflect, позволяет простым образом выразить многие противоположительные леммы, такие как contra_eq
.
Если вы не хотите использовать какие-либо причудливые леммы/тактики, я не думаю, что вы можете избежать какой-либо формы переписывания в своем доказательстве (на шаге, где вы хотите перейти от
2n <> 2m
кn = m
), и поэтому вы получите доказательство по крайней мере такой же сложный, как у Software Foundation. В общем, в такого рода лёгких примерах рассуждения от противного — это всего лишь способ скрыть прямое рассуждение, так что в итоге вы проделаете те же шаги, только спрятанные за отрицаниями.