Переменная Coq существует в списке

-3

У меня проблема с доказательством существования экзистенциальной переменной в списке. Как я могу доказать что-то вроде этого:Переменная Coq существует в списке

Lemma exists_in_list_helper: forall (X : Type) (a : X) (P : X -> Prop), 
     (exists b : X, In b [a] -> P b) -> 
     P a. 
Proof. 
Admitted.

У меня есть другой вопрос. Как я могу анализировать регистр над значениями в списке (если он существует в этой части списка или нет)? Это основная лемма, которую я доказываю. Любая помощь приветствуется:

Lemma in_list: forall (X : Type) (a : X) l (P : X -> Prop), 
     (a :: l <> [] /\ exists b : X, In b (a :: l) -> P b) -> 
     (P a /\ l = []) \/ 
     (P a /\ l <> [] /\ exists b : X, In b l -> P b) \/ 
     (P a /\ l <> [] /\ forall b : X, In b l -> ~ P b) \/ 
     (~ P a /\ l <> [] /\ exists b : X, In b l -> P b). 
Proof.

Спасибо,

источник

2016-09-15 saeed M

Ваша первая лемма не представляется вероятной: мы знаем, что существует b такой, что P b имеет значение iff b \in [a]. Однако мы не знаем, держится ли b \in [a], так что это сложно доказать. Вы можете возможно видеть ваше заявление как:

Lemma exists_in_list_helper (X : Type) (a : X) (P : X -> Prop) : 
     (exists b : X, a = b -> P b) -> 
     P a.

Затем, не сразу следует, что a = b. Вы можете лемма, такие как:

Lemma in1 T (x y : T) : In x [y] <-> x = y. 
Proof. 
split; intros H. 
+ now apply in_inv in H; case H. 
+ now rewrite H; constructor. 
Qed.

Что касается вашего второго вопроса, то я не уверен, что я полностью понять цель вашей леммы. Как правило, один хочет иметь:

forall x l, x \in l \/ x \notin l

, но это требует разрешимости для равенства по типу x см леммы in_dec. Если разделить список l в l1, l2, то отсюда следует, что:

x \in l1 ++ l2 <-> x \in l1 \/ x \in l2

, который позволяет для случая рассуждения. Более интересные объекты определяются path.v Math-Comp, которая позволяет выводить в удобном виде:

x \in l -> { l1, l2 & l = l1 ++ [x] ++ l2 }

где { x & P x} является версия exists x, P xType.

источник

2016-09-16 07:21:27 ejgallego

Благодарим вас за добрый ответ. У меня есть еще один вопрос. Я получаю ошибку «Невозможно унифицировать» при использовании. Я видел, что мы можем использовать тактику «шаблон», но я не мог ее правильно использовать. Я доказал следующее: ~ (существует b: X, In b l -> P b) -> (forall b: X, In b l -> ~ P b). –

и хотел бы изменить выражение forall в моей цели на ~ существует .... –

Я использовал шаблон (forall b: X, In bl -> ~ P b), который сгенерировал «забаву», но снова не мог использовать примените my_lemma, чтобы заменить forall на ~ существует ... Можете ли вы помочь мне, как я могу правильно использовать шаблон для руководства тактикой применения? –

-1

Для первого, я бы сказал, что вы, возможно, также понадобится тот факт, что равенство на X разрешима: либо a = b, и вы можете заменить или a <> b и вы получить противоречие, но вы должны иметь возможность выполнить такой анализ случаев.

Для второго, вы можете удалить часть a :: l <> [], она всегда верна и ничего не дает. И я уверен, что вам также необходимо решительное равенство (по тем же причинам).

источник

2016-09-16 07:08:16 Vinz

Переменная Coq существует в списке

ответ

Смежные вопросы