Agda-like programming in Coq/Proof General?

Question

Unlike Agda, Coq tends to separate proofs from functions. The tactics Coq gives are great for writing proofs, but I'm wondering if there is a way to replicate some Agda-mode functionality.

Specifically, I'd like:

• Some equivalent of Agda's ? or Haskell's _, where I can omit part of a function while I'm writing it, and (hopefully) have Coq tell me the type I need to put there
• An equivalent of C-c C-r in Agda mode (reify), where you fill a ? block with a function, and it will make new ? blocks for the needed arguments
• When I'm doing a match in a function, having Coq automatically write expand out the possible branches (like C-c C-a in Agda-mode)

Is this possible, in CoqIde or Proof General?

Depew

You can do some of that, but not in the same exact way. You 1, you can use refine (see the docs). The second bullet may be harder as current Coq IDEs I believe cannot use type information (yet), I guess company-coq could help with the 3rd. – Foundling

@Foundling Does company Coq make all the branches for you (i.e. with the pattern on the LHS filled in), or does it just add a branch and make you fill in both sides? – Depew

In CoqIDE, there is a shortcut to create a match ("ctrl + shift + m" by default). You have to put the cursor or select the right type beforehand. – Peddle

For match, you mean C-c C-c, right? – Pitt

Answer 1

As was suggested by ejgallego in the comments, you can (almost) do it. There is company-coq tool, which works on top of ProofGeneral.

Let me demonstrate how the map function could be implemented using company-coq and the refine tactic. Start with

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.

Type in refine ()., then put the cursor inside the parens and type C-c C-a RET list RET -- it inserts a match expression on lists with holes you fill in manually (let's fill in the list name and the base case).

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.
  refine (match xs with
          | nil => nil
          | cons x x0 => cons _ _
          end).

To finish it off we rename x0 into tl and provide the recursive case exact (map A B f tl).:

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.
  refine (match xs with
          | nil => nil
          | cons x tl => cons _ _
          end).
  exact (f x).
  exact (map A B f tl).
Defined.

There is also a useful keyboard shortcut C-c C-a C-x which helps with extracting the current goal into a separate lemma/helper function.

Strutting

Very cool! So, I the big thing I was missing is that you can use tactics like refine and exact to define Fixpoints, as well as proofs. – Depew

Under Curry-Howard correspondence there should be no difference :) Tactics are a language for building terms. You just need to end computationally relevant definitions with Defined instead of Qed, otherwise Coq considers a definition opaque and won't unfold it. – Strutting

The main problem is that company-coq support for holes is a bit fragile as it mostly communicates with Coq using regular expressions. Hopefully in the future a more structured protocol (as in Agda) can be used. – Foundling

Looks like the apply tactic is pretty close to Reify in Agda. – Depew

Answer 2

Let me teach you one weird trick. It may not be the answer to all your concerns, but it might help, at least conceptually.

Let's implement addition for natural numbers, the latter being given by

Inductive nat : Set :=
  | zero : nat
  | suc : nat -> nat.

You can try to write addition by tactics, but this happens.

Theorem plus' : nat -> nat -> nat.
Proof.
  induction 1.

plus' < 2 subgoals

  ============================
   nat -> nat

subgoal 2 is:
 nat -> nat

you can't see what you're doing.

The trick is to look more closely at what you're doing. We can introduce a gratuitously dependent type, cloning nat.

Inductive PLUS (x y : nat) : Set :=
  | defPLUS : nat -> PLUS x y.

The idea is that PLUS x y is the type of "the way to compute plus x y". We'll need a projection, allowing us to extract the result of such a computation.

Theorem usePLUS : forall x y, PLUS x y -> nat.
Proof.
  induction 1.
    exact n.
Defined.

Now we're ready to program by proving.

Theorem mkPLUS : forall x y, PLUS x y.
Proof.

mkPLUS < 1 subgoal

  ============================
   forall x y : nat, PLUS x y

The conclusion of the goal shows us our current left-hand side and context. The analogue of C-c C-c in Agda is...

  induction x.

mkPLUS < 2 subgoals

  ============================
   forall y : nat, PLUS zero y

subgoal 2 is:
 forall y : nat, PLUS (suc x) y

And you can see it has done a case split! Let's knock off the base case.

    intros y.
      exact (defPLUS zero y    y).

Invoking the constructor of PLUS is like writing an equation. Imagine an = sign before its third argument. For the step case, we need to make a recursive call.

    intros y.
      eapply (fun h => (defPLUS (suc x) y    (suc (usePLUS x y h)))).

To make the recursive call, we invoke usePLUS with the arguments we want, here x and y, but we abstract over the third argument, which is the explanation of how actually to compute it. We are left with just that subgoal, effectively the termination check.

mkPLUS < 1 subgoal

  x : nat
  IHx : forall y : nat, PLUS x y
  y : nat
  ============================
   PLUS x y

And now, rather than using Coq's guardedness check, you use...

        auto.

...which checks that the inductive hypotheses cover the recursive call. We're

Defined.

We have a worker, but we need a wrapper.

Theorem plus : nat -> nat -> nat.
Proof.
  intros x y.
    exact (usePLUS x y (mkPLUS x y)).
Defined.

And we're ready to go.

Eval compute in (plus (suc (suc zero)) (suc (suc zero))).

Coq <      = suc (suc (suc (suc zero)))
     : nat

You have an interactive construction tool. You can game it to show you the pertinent details of the problem you're solving by making types more informative. The resulting proof script...

Theorem mkPLUS : forall x y, PLUS x y.
Proof.
  induction x.
    intros y.
      exact             (defPLUS zero    y    y).
    intros y.
      eapply (fun h =>  (defPLUS (suc x) y    (suc (usePLUS x y h)))).
        auto.
Defined.

...is explicit about the program it constructs. You can see that's defining addition.

If you automate this setup for program construction, then layer on an interface showing you the program you're building and the key problem-simplifying tactics, you get a funny little programming language called Epigram 1.

Pitt