Теорема plus_n_n_injective, упражнение

Нужна помощь с упражнением от Software Foundations. Это теорема:

Theorem plus_n_n_injective : ∀n m,
 n + n = m + m →
 n = m.
Proof.

Я получаю n = 0 в качестве цели и n + n = 0 в качестве гипотезы. Как двигаться дальше?


coq
person Olle Härstedt    schedule 16.04.2014    source источник

Ответы (3)


arrow_upward
0
arrow_downward

Если вы исследуете n (destruct это), это будет либо 0, и в этом случае цель доказуема с помощью рефлексивности, либо S n', и в этом случае гипотеза противоречива на congruence/inversion.

person Ptival    schedule 16.04.2014
comment
Не могли бы вы подробнее рассказать о тактике destruct и inversion? - person Olle Härstedt; 17.04.2014
comment
destruct n. выполняет анализ вариантов для n, предоставляя по одному случаю для каждого конструктора типа n. inversion анализирует случаи, сохраняя при этом факты об индексах n. Вы сможете узнать о них из любого приличного введения в Coq. Например, эта глава CPDT охватывает inversion: adam.chlipala.net/cpdt/html/ Предикаты.html - person Ptival; 17.04.2014
comment
Хорошо спасибо. Теперь я застрял в другом месте с целью n + n = m + m и гипотезой S n + S n = S m + S m. Я сделал что-то не так? - person Olle Härstedt; 19.04.2014
comment
-1 Как 0 = m доказывается с помощью рефлексивности? Кроме того, в книге предлагается доказывать индукцией по n не разрушать. Это довольно вводит в заблуждение и делает @OlleHärstedt несколько хуже. - person David Grenier; 31.05.2014

arrow_upward
3
arrow_downward

n + n нельзя упростить, потому что n — это переменная, а не конструктор типа. Вы можете раскрыть все случаи построения n, destruct используя его, как сказал Ptival. Однако использование inversion в этом контексте кажется мне немного экстремальным, и это не то, о чем это упражнение Sf.

При замене конструктором O O + O уменьшится (например, с использованием simpl) до O, а reflexivity должно помочь.

При замене конструктором S S foo + bar всегда будет уменьшаться до формы S something, которая не может быть равна O (самый простой способ подтвердить это — использовать discriminate), потому что это два конструктора одного типа.

Бест, В.

person Vinz    schedule 17.04.2014

arrow_upward
0
arrow_downward

Уловку для решения этой проблемы можно почерпнуть из теоремы для length_snoc, показанной ранее в той же главе.

Поскольку это был первый раз в книге, когда некоторые переменные/гипотезы вводились после индукции по n, новичкам (таким как я) это может показаться необычным. Это позволяет вам получить более общие гипотезы в вашем контексте после доказательства базового случая.

Как упоминалось ранее, вы сможете доказать некоторые цели просто с помощью рефлексии. Некоторые из них могут быть доказаны инверсией ложных гипотез в вашем контексте (они должны стать очевидными, как только вы их обнаружите, идея о том, что 2 + 2 = 5 -> anything верна, может иметь большое значение).

Наконец, вам придется переработать одну из ваших гипотез, используя ранее определенные леммы plus_n_Sm и eq_add_S, а также симметрию, чтобы иметь возможность применять более общие гипотезы, которые мы обсуждали ранее.

person David Grenier    schedule 31.05.2014
comment
По крайней мере, в текущей версии во всей книге нет length_snoc' теоремы :( - person Waiting for Dev...; 23.05.2018