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?

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.