Как я могу доказать, что H и моя цель одинаковы для всех элементов списка?Проверка всех элементов списка в coq
X : Type
P : X -> Prop
l : list X
H : forall n : X, ~ (In n l /\ ~ P n)
______________________________________(1/1)
forall b : X, In b l -> P b
Два утверждения ~ (In n l /\ ~ P n) и In b l -> P b равны. Я пробовал apply imply_to_or о цели, чтобы упростить, но не мог объединиться.
Спасибо,
Прежде всего, нам нужно импорт:
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Lists.List.
рассуждаем "назад" при применении леммы к цели. Это означает, что вам нужна лемма, которая подразумевает ее последующее, не посылка.
Мы можем Search (~ ?p \/ ?c -> ?p -> ?c). для него, и это поможет вам:
or_to_imply: forall P Q : Prop, ~ P \/ Q -> P -> Q
выше лемма будет работать, но мы можем сделать немного лучше: мы можем сделать использование tauto тактики, и вуаля, у вас имеют простое доказательство:
Goal forall (X : Type) (P : X -> Prop) (l : list X),
(forall n, ~ (In n l /\ ~ P n)) ->
forall b, In b l -> P b.
intros X P l H b.
specialize H with b.
tauto.
Qed.
Вы уверены, что это конструктивно верно? – jbapple
Было бы лучше, если бы вы предоставили свой импорт и фактическое утверждение о том, что вы пытаетесь доказать ([mcve]). (1) Это поможет нам печатать. (2) Это скажет нам, что вы работаете в сфере классической логики. Кроме того, я думаю, что все, что вы доказываете о списках, может быть доказано с помощью конструктивной логики. (Я имею в виду в широком масштабе, а не в этом примере). –