How to define two mutually recursive functions in Coq?

Question

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.

Answer 1

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.

Then the proof of your lemma may start with:

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

Answer 2

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)) .
(* ... *)