Теорема о добавлении непустого списка в Coq - PullRequest
Новая
       92

Теорема о добавлении непустого списка в Coq

0 голосов
/ 20 ноября 2018

Я пытаюсь доказать следующую лемму в 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, для некоторых подцелей).

Ответы [ 3 ]

0 голосов
/ 22 ноября 2018

Вы начали правильный путь со своим destruct a.

В какой-то момент вы должны получить a0::a++b<>0. Это повторяет a++b<>0, но оно совершенно иное, поскольку у вас есть cons, поэтому discriminate знает, что оно отличается от nil.

0 голосов
/ 22 ноября 2018

Начиная с destruct a действительно хорошая идея.

В случае, когда a равно Nil, вы должны разрушить гипотезу (a <> [] \/ b <> []). Будет два случая:

  • правильная гипотеза [] <> [] contradiction,
  • левый, гипотеза b <> [] ваша цель (так как a = [])

Для случая, когда a равен a :: a0, вы должны использовать discriminate, как сказал Жюльен.

0 голосов
/ 21 ноября 2018

Во-первых, я не уверен, какую версию 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.
...