存在性实例化和概念化

Question

有人可以给我一个关于Coq存在实例化和存在概括的简单例子吗？当我想要证明exists x, P,在P某些地方Prop使用时x,我经常想要命名x(作为x0或某些),并操纵P.这可能是Coq中的一个吗？

Answer 1

如果你要直接证明存在主义,而不是通过引理,你可以使用eapply ex_intro.这引入了一个存在变量(书面?42).然后,您可以操纵该术语.要完成证明,您需要最终提供一种为该变量构造值的方法.您可以使用instantiate策略明确地执行此操作,也可以通过诸如此类的策略隐式执行此操作eauto.

请注意,使用存在变量通常很麻烦.许多策略都假设所有术语都被实例化,并且可能隐藏子目标中的存在物; 你只会Qed告诉你"错误:尝试保存不完整的证据".只有在计划很快实例化它们时,才应使用存在变量.

这是一个愚蠢的例子,说明了使用eapply.

Goal exists x, 1 + x = 3.
Proof.                        (* ? exists x, 1 + x = 3 *)
  eapply ex_intro.            (* ? 1 + ?42 = 3 *)
  simpl.                      (* ? S ?42 = 3 *)
  apply f_equal.              (* ? ?42 = 2 *)
  reflexivity.                (* proof completed *)
Qed.