Does Gallina have holes like in Agda?

Question

When proving in Coq, it's nice to be able to prove one little piece at a time, and have Coq help keep track of the obligations.

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

At this point I can see the proof state to know what is required to finish the proof.

But when writing Gallina, do we have to solve the whole thing in one bang, or make lots of little helper functions? I'd love to be able to put use a question mark to ask Coq what it's looking for:

Definition ModusPonens' :=
  fun (A B : Prop) (H : (A -> B) /\ A) =>
    match H with
    | conj H1 H2 => H1 _ (* hole of type B *)
    end.
The following term contains unresolved implicit arguments:
  (fun (A B : Prop) (H : (A -> B) /\ A) =>
   match H with
   | conj H1 H2 => H1 ?a
   end)
More precisely: 
- ?a: Cannot infer this placeholder of type "A" in
  environment:
  A, B : Prop
  H : (A -> B) /\ A
  H1 : A -> B
  H2 : A

It really seems like Coq should be able to do this, because I can even put ltac in there and Coq will find what it needs:

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

If Coq is smart enough to finish writing the definition for me, it's probably smart enough to tell me what I need to write in order to finish the function myself, at least in simple cases like this.

So how do I do this? Does Coq have this kind of feature?

Answer (larsr)

You can use refine for this. You can write underscores which will turn into obligations for you to solve later.

Definition ModusPonens: forall (A B : Prop), ((A -> B) /\ A) -> B.
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, B: Prop
H: (A -> B) /\ A
H1: A -> B
H2: A
A

Now your goal is to provide an A. This can be discharged with

  exact H2. Defined.

Answer (Li-yao Xia)

Use an underscore

Definition ModusPonens' :=
  fun (A B : Prop) (H : (A -> B) /\ A) =>
    match H with
    | conj H1 H2 => H1 _ (* hole of type A *)
    end.
The following term contains unresolved implicit arguments:
  (fun (A B : Prop) (H : (A -> B) /\ A) =>
   match H with
   | conj H1 H2 => H1 ?a
   end)
More precisely: 
- ?a: Cannot infer this placeholder of type "A" in
  environment:
  A, B : Prop
  H : (A -> B) /\ A
  H1 : A -> B
  H2 : A

or use 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.
forall (A B : Prop) (H : (A -> B) /\ A) (H1 : A -> B)
  (H2 : A), conj H1 H2 = H -> A intros. (* See the type of the hole *)
A, B: Prop
H: (A -> B) /\ A
H1: A -> B
H2: A
Heq_H: conj H1 H2 = H
A