Интуитивно заявить, что xs
равно ys
, — это то же самое, что сказать, что соответствующие обратные списки равны друг другу.
В настоящее время я изучаю Lean 4, поэтому я поставил себе следующее упражнение. Я хочу доказать следующую теорему в Lean 4:
theorem rev_eq (xs ys : List α) : (xs = ys) = (reverse xs = reverse ys)
Однако я не уверен, можно ли доказать эту теорему в Lean 4. Если нет, то почему ее нельзя доказать?
Самое близкое, что я мог сделать, это доказать утверждение в предположении, что xs = ys
:
theorem rev_eq' (xs ys : List α) :
xs = ys -> (xs = ys) = (reverse xs = reverse ys) := by
intros h
rw [h]
simp
Возможно, если бы можно было доказать, что утверждение также выполняется, если предположить, что xs
не равно ys
, то исходная теорема последовала бы. Хотя я тоже застрял на этом маршруте.
Есть идеи?
Это свойство обычно доказывается по индукции. Я никогда не использовал бережливое производство, но как только введение в список будет сделано, это должно быть легко. Вам может понадобиться лемма, говорящая, что (xs = ys) -> xs@l = xs@l
(также по индукции, я думаю, @ означает конкатенацию списков).
Конечно, индукция звучит разумно. Я просто борюсь с тем фактом, что не могу делать никаких предположений о значениях xs
и ys
. Кажется, все, что я могу сделать, это построить равенство, а затем использовать правила перезаписи, чтобы манипулировать им.
В Lean обычно идиоматично заявлять о равенстве предложений, используя Iff
, что эквивалентно согласно аксиоме propext
. Отсюда iff
— индуктивный тип с двумя сторонами, одно направление, которое вы доказали, а другое направление следует из индукции. (Эта теорема доказуема и без этой аксиомы, между прочим)
Но я бы порекомендовал вам сделать induction xs
и induction ys
, а затем посмотреть на цели. Два должны быть невозможными, и бережливое производство должно показать вам, что это противоречия (или вы действительно получите а, которое можно упростить до false = false
) и две тривиально истинные цели. Не забудьте расширить определение reverse
.
Обратите внимание, что эта теорема представлена в mathlib как List.reverse_inj. По соглашению мы обычно заявляем об эквивалентности предложений, используя
↔
, а не=
.