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

Question

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

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

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.

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

Answer 1

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