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:
? 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? block with a function, and it will make new ? blocks for the needed argumentsmatch in a function, having Coq automatically write expand out the possible branches (like C-c C-c in Agda-mode)Is this possible, in CoqIde or Proof General?
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.