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.
Proof.
  intros A B [H1 H2].
  apply H1.

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

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

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.

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?

Luthuli

Answer 1

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.

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

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

Apportion

I noticed I could keep the definition transparent / unfoldable by using "Definition" instead of "Theorem". Could I make the edit to your answer? – Luthuli

Is there a way to finish off the proof/definition in a computational rather than logical way? I noticed that after the . (dot), I can finish off the proof with assumption, but is there a way to do it without tactics / in Gallina? – Luthuli

Yes! Go ahead please! – Apportion

The transparency of the definition is more related to whether you end proof mode with Defined. instead of Qed. than to what keyword you use to start the definition. – Senega

Answer 2

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.

(*
Error: 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. intros. (* See the type of the hole *)

Comintern

Thanks! I wish I could mark both answer correct, as they both enable the kind of workflow I'm looking for! – Luthuli