I needed to define a function like:

```
Fixpoint zero (n:nat) : nat :=
match n with
| S (S n') => two n'
| S n' => one n'
| O => 0
end
with one (n:nat) : nat :=
match n with
| S (S n') => zero n'
| S n' => two n'
| O => 1
end
with two (n:nat) : nat :=
match n with
| S (S n') => one n'
| S n' => zero n'
| O => 2
end.
```

Is it possible to do just one of these three definitions in proof mode?

As in:

```
Fixpoint zero (n:nat) : nat :=
match n with
| S (S n') => two n'
| S n' => one n'
| O => 0
end.
with one (n:nat). (* proof mode definition *)
with two (n:nat) : nat :=
match n with
| S (S n') => one n'
| S n' => zero n'
| O => 2
end.
```

Or can't we mix usual definition and proof mode definitons?

You can define the body of one function as a function of the others:

```
Section One.
Context (zero two : nat -> nat).
Definition one_body (n : nat) : nat.
Proof.
...
Defined.
End One.
Fixpoint zero ...
with one := one_body zero two
with two ...
```

Just out of curiosity, how can we define `one`

here in proof mode?

I sort of blindly tried till:

```
Section mutrec.
Context (zero two: nat -> bool).
Definition one_body (n:nat) : bool.
Proof.
induction n.
- exact true. (* n = 0 *)
- destruct n. (* n = 1 *)
*
```

I finished that (probably incorrectly) and made this:

```
Section mutrec.
Context (zero two: nat -> nat).
Definition one_body (n:nat) : nat.
Proof.
induction n.
- exact 0. (* n = 0 *)
- destruct IHn. (* n = 1 *)
* exact (two n).
* exact (zero n).
Defined.
End mutrec.
Fixpoint zero (n:nat) : nat :=
match n with
| S (S n') => two n'
| S n' => one n'
| O => 0
end
with one (n:nat) := one_body zero two
with two (n:nat) : nat :=
match n with
| S (S n') => one n'
| S n' => zero n'
| O => 2
end.
```

but it says:

```
The term "one_body zero two" has type "nat -> nat"
while it is expected to have type "nat".
```

How can that be fixed?

I get a different error if I remove the `(n:nat)`

part of the definition of `one`

.

```
A fixpoint needs at least one parameter
```

And why is it `one := one_body zero two`

? Why not just `one (n:nat) := one_body n`

?

Did you try ` with one (n:nat) := one_body zero two n`

?

That worked!

My proof mode version of `one`

isn't working though. Could anyone spot from where I went wrong?

The term looks like:

```
one_body =
fun (zero two : nat -> nat) (n : nat) =>
nat_rec (fun _ : nat => nat) 0
(fun n0 IHn : nat => match IHn with
| 0 => two n0
| S _ => zero n0
end) n
: (nat -> nat) -> (nat -> nat) -> nat -> nat
Arguments one_body (_ _)%function_scope _%nat_scope
```

After seeing the beginning of this term, I get why the `one_body zero two n`

was needed.

Okay, for starters, the ` exact 0.`

should've been ` exact 1.`

.

Here is an interactive definition of one_body.

```
Definition one_body (n:nat) : nat.
Proof.
induction n as [|p recp].
- exact 1. (* n = 0 *)
- destruct p as [| q].
* exact (two 0).
* exact (zero q).
Defined.
```

But I don't think it is as readable (assuming it is correct!) as the direct one.

I think that interactive definitions are OK if the considered type is informative enough (e.g with `sumbool`

, `sumor`

, `sig`

, etc. ) to make you sure that you obtain interactively the "good" function you want to define. Otherwise, you have to look carefully at the proof script and verify it's OK.

Julin S said:

I needed to define a function like:

`Fixpoint zero (n:nat) : nat := match n with | S (S n') => two n' | S n' => one n' | O => 0 end with one (n:nat) : nat := match n with | S (S n') => zero n' | S n' => two n' | O => 1 end with two (n:nat) : nat := match n with | S (S n') => one n' | S n' => zero n' | O => 2 end.`

Is it possible to do just one of these three definitions in proof mode?

As in:

`Fixpoint zero (n:nat) : nat := match n with | S (S n') => two n' | S n' => one n' | O => 0 end. with one (n:nat). (* proof mode definition *) with two (n:nat) : nat := match n with | S (S n') => one n' | S n' => zero n' | O => 2 end.`

Or can't we mix usual definition and proof mode definitons?

you want

```
Fixpoint zero (n:nat) : nat :=
match n with
| S (S n') => two n'
| S n' => one n'
| O => 0
end
with one (n:nat) : nat
with two (n:nat) : nat :=
match n with
| S (S n') => one n'
| S n' => zero n'
| O => 2
end.
Proof. (* whtevr *) Defined.
```

(no `.`

between `one`

and `two`

)

Ah.. that was the way that I was looking for first.

But having the bodies defined separately feels nice. Probably because that's what I got to work first.

<deleted>

(Posting as a new topic):

Last updated: Jun 24 2024 at 00:02 UTC