Agad-like programming in Coq / Proof General?

Question

Unlike Agda, Coq tends to separate evidence from functions. Coq's tactics provide excellent evidence writing capabilities, but I wonder if there is a way to reproduce some Agda-mode features.

In particular, I would like to:

• Some equivalent to Agda ? or Haskell _ , where I can omit part of the function while I am writing it, and (hopefully) Coq will tell me the type I need to put there
• Equivalent to Cc Cr in Agda (reify) mode, where do you fill in the block ? function and it will create new blocks ? for the necessary arguments
• When I execute a match function in a function, when Coq automatically records expandable possible branches (for example, Cc Ca in Agda mode)

Is this possible in CoqIde or Proof General?

Answer 1

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

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

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

Enter refine (). , then place the cursor inside parens and enter Cc Ca RET list RET - it inserts the match expression into the lists with holes that you fill in manually (let the list name and base case be filled in).

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

To finish it, rename x0 to tl and provide the recursive case exact (map AB f tl). :

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

There is also a useful Cc Ca Cx key combination that helps with extracting the current target into a separate lemma / helper function.

Answer 2

Let me teach you one strange trick. This may not be the answer to all your problems, but it can help, at least conceptually.

Let the addition for natural numbers be realized, the latter is given

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

You can try writing an add-on on tactics, but it happens.

 Theorem plus' : nat -> nat -> nat. Proof. induction 1. plus' < 2 subgoals ============================ nat -> nat subgoal 2 is: nat -> nat 

you cannot see what you are doing.

The trick is to take a closer look at what you are doing. We can introduce a gratis dependent type, nat cloning.

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

The idea is that PLUS xy is a type of "method for calculating PLUS xy ." We need a projection that allows us to extract the result of such a calculation.

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

Now we are ready to program by proving.

 Theorem mkPLUS : forall xy, PLUS x y. Proof. mkPLUS < 1 subgoal ============================ forall xy : nat, PLUS xy 

The conclusion of the goal shows us our current left side and context. The analogue of Cc Cc 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 that he laid out the case! Let me knock down the base case.

  intros y. exact (defPLUS zero yy). 

Calling the PLUS constructor is like writing an equation. Imagine the = sign in front of 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 xyh)))). 

To make a recursive call, we call usePLUS with the necessary arguments here x and y , but we abstract out the third argument, which explains how to actually compute it. We only have this sub-goal left, the completion check is effective.

 mkPLUS < 1 subgoal x : nat IHx : forall y : nat, PLUS xy y : nat ============================ PLUS xy 

And now, instead of using Coq's security check, you use ...

  auto. 

... which verifies that inductive hypotheses embrace a recursive call. we

 Defined. 

We have a worker, but we need a cover.

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

And we are ready to go.

 Eval compute in (plus (suc (suc zero)) (suc (suc zero))). Coq < = suc (suc (suc (suc zero))) : nat 

You have an interactive building tool. You can play the game to show you the relevant details of the problem you are solving, making the types more informative. Received proof script ...

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

... clearly about the program he creates. You can see this defining addition.

If you automate this setting to build a program, then the layer on the interface showing your program that you are building and the key problem is simplifying tactics, you get a funny little programming language called Epigram 1.