# Defining functions in proof mode

**URL:** <https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786>\
**Category:** Using Rocq\
**Created:** [September 8, 2022, 8:28pm UTC](https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786 "2022-09-08T20:28:40Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![jeanas](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jeanas/32/762_2.png) [@jeanas](https://discourse.rocq-prover.org/u/jeanas)\
**Post date:** [September 8, 2022, 8:28pm UTC](https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786/1 "2022-09-08T20:28:40Z")

</div>

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

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

```

… I prefer to do

```auto
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:

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

```

---

<div class="post-metadata">

**Author:** ![jeanas](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jeanas/32/762_2.png) [@jeanas](https://discourse.rocq-prover.org/u/jeanas)\
**Post date:** [September 8, 2022, 8:31pm UTC](https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786/2 "2022-09-08T20:31:59Z")

</div>

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

```auto
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`?

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [September 8, 2022, 8:43pm UTC](https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786/3 "2022-09-08T20:43:22Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![jeanas](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jeanas/32/762_2.png) [@jeanas](https://discourse.rocq-prover.org/u/jeanas)\
**Post date:** [September 8, 2022, 8:46pm UTC](https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786/4 "2022-09-08T20:46:38Z")

</div>

Wonderful! Thanks a lot.

---

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [September 8, 2022, 8:52pm UTC](https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786/5 "2022-09-08T20:52:23Z")

</div>

If you want to combine syntactic and interactive construction of functions, the standard advice I give these days is to use [Equations](https://github.com/mattam82/Coq-Equations) (with `_` for what you want to build with tactics), which is nowadays part of the [Coq Platform](https://github.com/coq/platform/). See a simple [use example](https://discourse.rocq-prover.org/t/fixpoint-with-two-decreasing-arguments/544/4).

---

<div class="post-metadata">

**Author:** ![jwiegley](https://avatars.discourse-cdn.com/v4/letter/j/bbce88/32.png) [@jwiegley](https://discourse.rocq-prover.org/u/jwiegley)\
**Post date:** [September 8, 2022, 9:50pm UTC](https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786/6 "2022-09-08T21:50:50Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![casteran](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/casteran/32/451_2.png) [@casteran](https://discourse.rocq-prover.org/u/casteran)\
**Post date:** [September 9, 2022, 8:47am UTC](https://discourse.rocq-prover.org/t/defining-functions-in-proof-mode/1786/7 "2022-09-09T08:47:36Z")

</div>

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.