Gallina 是否也像 Agda 一样有洞？

Question

在 Coq 中证明时，能够一次证明一小部分并让 Coq 帮助跟踪义务是件好事。

Theorem ModusPonens: forall (A B : Prop), ((A -> B) /\ A) -> B.
Proof.
  intros A B [H1 H2].
  apply H1.

此时我可以看到证明状态以了解完成证明需要什么：

context
H2: B
------
goal: B

但是在编写 Gallina 时，我们是否必须一次性解决整个问题，或者创建许多小辅助函数？我希望能够使用问号来询问 Coq 它在寻找什么：

Definition ModusPonens' := fun (A B : Prop) (H : (A -> B) /\ A) =>
  match H with
    | conj H1 H2 => H1 {?} (* hole of type B *)
  end.

看起来 Coq 确实应该能够做到这一点，因为我什至可以将 ltac 放在那里，Coq 会找到它需要的东西：

Definition ModusPonens' := fun (A B : Prop) (H : (A -> B) /\ A) =>
  match H with
    | conj H1 H2 => H1 ltac:(assumption)
  end.

如果 Coq 足够聪明，可以为我完成定义，那么它可能也足够聪明，可以告诉我需要编写什么才能自己完成函数，至少在像这样的简单情况下是这样。

那么我该怎么做呢？Coq有这样的功能吗？

Answer 1

您可以用于refine此用途。你可以写下划线，它会变成你以后要解决的义务。

Definition ModusPonens: forall (A B : Prop), ((A -> B) /\ A) -> B.

    refine (fun A B H =>
              match H with
                 | conj H1 H2 => H1 _ (* hole of type A *)
               end).

现在您的目标是提供一个A. 这可以通过以下方式排出：exact H2. Defined.