Я пытаюсь доказать следующую лемму в Coq:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> [] \/ b <> []) -> a ++ b <> [].
Прямо сейчас моя текущая стратегия состояла в том, чтобы уничтожить a, и после разрыва дизъюнкции в идеале я мог бы просто заявить, что если a <> [], то a ++ b также должен быть <> []... Это был план, но я не может пройти мимо подзадачи, которая напоминает первый "a ++ b <> []", даже когда мой контекст ясно утверждает, что "b <> []". Любой совет?
Я также просмотрел множество уже существующих теорем о списках и не нашел ничего особенно полезного (за исключением app_nil_l и app_nil_r, для некоторых подцелей).
Начинать с destruct a - это действительно хорошая идея.
В случае, когда a равно Nil, вы должны разрушить гипотезу (a <> [] \/b <> []). Будет два случая:
[] <> [] является contradiction,b <> [] - ваша цель (так как a = []) Для случая, когда a - a :: a0, вы должны использовать discriminate как сказал Жюльен.
Вы начали правильный путь с вашего destruct a.
В какой-то момент вы должны получить a0::a++b<>0. Он напоминает a++b<>0 но он совершенно другой, так как здесь есть cons, поэтому discriminate знает, что он отличается от nil.
Во-первых, я не уверен, какую версию Coq вы используете, синтаксис, безусловно, выглядит странно. В-третьих, нам трудно помочь, если вы не покажете нам доказательства, которые у вас есть. Я должен сказать, что на самом деле ваша стратегия кажется правильной, вам следует уничтожить оба списка, хотя лучше сначала проверить или не посмотреть, какой список не пуст.
Другой вариант - использовать вычисления, чтобы показать вашу лемму, в этом случае будет вычислено равенство, и, таким образом, вы получите результат сравнения. В этом случае достаточно уничтожить только один список из-за порядка или аргументов:
From mathcomp Require Import all_ssreflect.
Lemma not_empty (A : eqType) (a b : seq A) :
[|| a != [::] | b != [::]] -> a ++ b != [::].
Proof. by case: a. Qed.