coq - 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

使用下划线

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

(*
Error: Cannot infer this placeholder of type
"A" in environment:
A, B : Prop
H : (A -> B) /\ A
H1 : A -> B
H2 : A
*)

或使用 Program

Require Import Program.
Obligation Tactic := idtac.  (* By default Program tries to be smart and solve simple obligations automatically. This commands disables it. *)

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

Next Obligation. intros. (* See the type of the hole *)