Defining functions in proof mode

Using Coq
1

I’m relatively new to Coq. I’ve learnt that proof mode is not restricted to constructing proofs (terms whose type is a proposition), but can in fact construct any term. I like this a lot because I’m not yet familiar with all Gallina ways of doing things, and more familiar with tactics. So, instead of doing

Fixpoint even (n : nat) :=
  match n with
  | O => True
  | S O => False
  | S (S n') => even n'
  end.

… I prefer to do

Fixpoint even (n : nat) : Prop.
Proof. (* well, "Proof" *)
  destruct n as [|n'].
  - exact True.
  - destruct n' as [|n''].
    * exact False.
    * exact (even n'').
Defined.

My question is very simple. Is there a way to do this, but in the local context of a proof while in proof mode, not as a toplevel definition? This is one thing I naively tried:

Goal exists f : nat -> nat, True.
Proof.
  Fail exists (fun (x : nat) => (_ : nat)).
  (* Cannot infer this placeholder of type "nat" in environment: x : nat *)
2

Of course it’s always 1 minute after asking the question that you remember the answer:

Goal exists f : nat -> nat, True.
Proof.
  exists (fun (x : nat) => (ltac:(exact 2))).
  exact I.
Defined.

Still, is there a way to have interactive (“proof”) mode available when defining this function, like with the definition of even?

3

try unshelve eexists (fun (x : nat) => (_ : nat)).

4

Wonderful! Thanks a lot.

5

If you want to combine syntactic and interactive construction of functions, the standard advice I give these days is to use Equations (with _ for what you want to build with tactics), which is nowadays part of the Coq Platform. See a simple use example.

1 Like
6

To add to what Karl has said (Equations is wonderful), you can also inject ltac:(...) into your Gallina terms when you aren’t clear what the term should be, but you know the tactic that would solve that hole for you.

1 Like
7

You may also take into account how documentation making tools deal with the Definition foo:<type>. Proof. ... Defined. pattern.
For instance, coqdoc’s popular -g option (applied to your first example) just produces Definition even (n:nat): Prop without more information.

1 Like