Сохранение структуры с индукциями по 2 переменным

Question

Я изучал тактику Coq и знакомился с системой, укоряя основные факты о натуральных числах.

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

Однако я был в тупике в нескольких случаях, когда у меня есть свойство для nm: nat, которое я хочу доказать, но когда я пытаюсь сделать индукцию по n и m, структура индуктивных гипотез бесполезно пытаться доказать собственность.

Я доказал n = m -> o * n = o * m очень легко:

Theorem times_alg_left : forall n m o:nat, n = m -> o * n = o * m.
intros n m o H.
rewrite H; reflexivity.
Defined.

Но попытка доказать, что S o * n = S o * m -> n = m, полностью меня расстроила. После значительных усилий я решил попытаться доказать, что 2 * n = 2 * m -> n = m, но это было не легче.

У меня возникают такие ситуации:

Theorem m2_eq : forall n m:nat, 2 * n = 2 * m -> n = m.
intros n m H.
induction n.
destruct m.
reflexivity.
discriminate.
induction m.
discriminate.

1 subgoal
n, m : nat
H : 2 * S n = 2 * S m
IHn : 2 * n = 2 * S m -> n = S m
IHm : 2 * S n = 2 * m -> (2 * n = 2 * m -> n = m) -> S n = m
______________________________________(1/1)
S n = S m

У меня есть 2 * S n = 2 * S м, но мои индуктивные предпосылки говорят о 2 * n = 2 * S м и 2 * S n = 2 * м.

Я ничего не могу сделать из этой ситуации.

Точно так же я начал пытаться доказать, что такое Nat.sub и меньше или равно, чтобы обойти это ограничение, но я столкнулся с той же ситуацией.

Theorem sub0_imp_le : forall n m:nat, n - m = 0 -> n <= m.
intros n m H.
induction n; induction m.
apply le_n.
apply le_0.
rewrite sub0 in H.
discriminate.

1 subgoal
n, m : nat
H : S n - S m = 0
IHn : n - S m = 0 -> n <= S m
IHm : S n - m = 0 -> (n - m = 0 -> n <= m) -> S n <= m
______________________________________(1/1)
S n <= S m

Но я в том же рассоле, где мои индуктивные помещения бесполезны.

Как мне структурировать свою тактику для решения теорем такого типа, с 2 переменными nat и какой-то ситуацией равенства или вычитания?

Answer 1

Используя книгу «Основы программного обеспечения», о которой упоминал Артур, я нашел рассматриваемый пример.Мне не нужно вводить m, прежде чем делать индукцию по n.Мне нужно было сначала сделать индукцию по n, а затем ввести m.

https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html#lab143

Theorem times_alg_rem_left : forall n o m:nat, (S o) * n = (S o) * m -> n = m.
intros n o.
induction n.
simpl.
intros m eq.
destruct m.
reflexivity.
rewrite (timesz o) in eq.
simpl in eq.
discriminate.
intros m eq.
destruct m.
rewrite (timesz (S o)) in eq.
inversion eq.
apply f_equal.
apply IHn.
rewrite (times_nSm (S o) n) in eq.
rewrite (times_nSm (S o) m) in eq.
apply plus_alg_rem_right in eq.
assumption.
Defined.

Answer 2

Вам нужно ввести индукцию по одному номеру, а обобщать другой, например, используя тактику generalize dependent.Это подробно объясняется в книге Основы программного обеспечения .