Логика: All_In не может расширять вложенные поля - PullRequest
Новая
       22

Логика: All_In не может расширять вложенные поля

1 голос
/ 25 апреля 2019

Я сталкиваюсь с довольно странной проблемой: coq не хочет перемещать переменную forall в контекст.

В старые времена это делалось: 

Example and_exercise :
  forall n m : nat, n + m = 0 -> n = 0 /\ m = 0.
Proof.
  intros n m.

Генерирует: 

n, m : nat
============================
n + m = 0 -> n = 0 /\ m = 0

Но когда у нас есть все внутри, это не работает: 

(* Auxilliary definition *)
Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
  (* ... *)

Lemma All_In :
  forall T (P : T -> Prop) (l : list T),
    (forall x, In x l -> P x) <->
    All P l.
Proof.
  intros T P l. split.
  - intros H.

После этого получаем: 

T : Type
P : T -> Prop
l : list T
H : forall x : T, In x l -> P x
============================
All P l

Но как вывести х за пределы Н и разложить его на более мелкие части? Я попробовал: 

destruct H as [x H1].

Но выдает ошибку: 

Error: Unable to find an instance for the variable x.

Что это? Как исправить?

1 Ответ

3 голосов
/ 26 апреля 2019

Проблема в том, что forall вложено слева от импликации, а не справа. Не имеет смысла вводить x из гипотезы в форме forall x, P x, так же как не имеет смысла вводить n в plus_comm : forall n m, n + m = m + n в контексте другого доказательства , Вместо этого вам нужно использовать гипотезу H, применяя в нужном месте. Я не могу дать вам ответ на этот вопрос, но вы можете обратиться к упражнению dist_not_exists в той же главе.

...