# How to define two mutually recursive functions in Coq?

I make such codes, and cannot preceed.

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Example example (f : Q -> bool) :
f 0 = false -> f 1 = true ->
exists g h : nat -> Q,
(g 0%nat = 0 /\ h 0%nat = 1) /\
(forall n : nat,
if (f ((g n%nat + h n%nat)/2))
then (g (n+1)%nat = g n%nat /\
h (n+1)%nat = ((g n%nat + h n%nat)/2))
else (g (n+1)%nat = ((g n%nat + h n%nat)/2) /\
h (n+1)%nat = h n%nat) ).
Proof.
intros.


(With Pierre Castéran's advice, I try to execute the following code.)

Fix g (n: nat) : Q :=
match n with
0% nat => 0
| S p => if (f ((g p + h p) /2))
then g p
else (g p + h p)/2
end
with h (n:nat) : Q :=
match n with
0% nat => 1
| S p => if (f ((g p + h p) /2))
then (g p + h p)/2
else  h p
end.


The last code tells me that Syntax error.

You may define gand hby mutual recursion

Section Example.

Variables (f : Q -> bool)
(f0 :  f 0 = false)
(f1 : f 1 = true).

Fixpoint g (n: nat) : Q :=
match n with
0% nat => 0
| S p => if (f ((g p + h p) /2))
then g p
else (g p + h p)/2
end
with h (n:nat) : Q :=
match n with
0% nat => 1
| S p => if (f ((g p + h p) /2))
then (g p + h p)/2
else  h p
end.



In your example, it's even simpler to use a helper:

 Fixpoint gh (n:nat) : Q * Q :=
match n with
| 0%nat => (0, 1)
| S p => match gh p with
(gp, hp) => let middle := (gp + hp)/2
in if (f middle)
then (gp, middle)
else (middle, hp)
end
end.


Proof.
exists (fun x => fst (gh x)), (fun x => snd (gh x)) .
simpl.

• Can I define Fixpoint in Proof? Commented Aug 17, 2022 at 9:42
• In interactive proof-mode, you may define mutually recursive functions with fix ... with .... In practice, I prefer using the Section mechanism, with local definitions of gand h, proving technical lemmas that may make the proof of your lemma easier, etc... Commented Aug 17, 2022 at 10:42
• I'm a beginner in Coq. As you said, after "Proof. Intros." I try to write fix ... with ... However, It tells me Syntax error. How to make it correct? Commented Aug 18, 2022 at 4:47

I'm not used to define functions in proof mode, but it's possible.

Lemma L:
exists g h : nat -> Q,
(g 0%nat = 0 /\ h 0%nat = 1) /\
(forall n : nat,
if (f ((g n%nat + h n%nat)/2))
then (g (n+1)%nat = g n%nat /\
h (n+1)%nat = ((g n%nat + h n%nat)/2))
else (g (n+1)%nat = ((g n%nat + h n%nat)/2) /\
h (n+1)%nat = h n%nat) ).
Proof.
pose  gh := (fix  gh  (n:nat) : (Q * Q) :=
match n with
0%nat => (0, 1)
|  S p => match gh p with
(gp, hp) => let middle := (gp + hp)/2
in if (f middle)
then (gp, middle)
else (middle, hp)
end
end).
exists (fun x => fst (gh x)), (fun x => snd (gh x)) .
(* ... *)