## Stream: Coq users

### Topic: Proof mode def for mutual recursion

#### Julin S (Jun 12 2022 at 15:47):

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?

#### Li-yao (Jun 12 2022 at 15:52):

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 ...
``````

#### Julin S (Jun 12 2022 at 16:09):

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 *)
*
``````

#### Julin S (Jun 12 2022 at 16:34):

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?

#### Julin S (Jun 12 2022 at 16:36):

I get a different error if I remove the `(n:nat)` part of the definition of `one`.

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

#### Julin S (Jun 12 2022 at 16:37):

And why is it `one := one_body zero two`? Why not just `one (n:nat) := one_body n`?

#### Pierre Castéran (Jun 12 2022 at 16:39):

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

That worked!

#### Julin S (Jun 12 2022 at 16:44):

My proof mode version of `one` isn't working though. Could anyone spot from where I went wrong?

#### Julin S (Jun 12 2022 at 16:45):

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

#### Julin S (Jun 12 2022 at 16:46):

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

#### Julin S (Jun 12 2022 at 16:49):

Okay, for starters, the ` exact 0.` should've been ` exact 1.`.

#### Pierre Castéran (Jun 12 2022 at 17:14):

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.

#### Gaëtan Gilbert (Jun 12 2022 at 17:59):

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`)

#### Julin S (Jun 12 2022 at 18:15):

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.

#### Julin S (Jun 13 2022 at 06:20):

<deleted>

(Posting as a new topic):

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Mutual.20recursion.20function.20in.20type

Last updated: Sep 25 2023 at 12:01 UTC