The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

(* This message should be executable in Coq 8.2 *)
Require Import ZArith Wellfounded.

(* I am sorry that one of my messages was sent only to Guilhem.  Here is 
a complete solution for two
mutually recursive functions returning outputs in two different types.

Suppose we wish to define two mutually recursive functions with the 
following equations:

f (x:nat) = match x with 0 => 0 | S p => Zabs_nat (2+(g (Z_of_nat p)))

g (x:Z) = if Z_le_dec x 0 then 0%Z else Z_of_nat (2 + f (Zabs_nat (x - 1)))

Two different input types, which will be reflected in the single input 
type for the
one recursive function used as a model, and two different output types, 
which
will be reflected by a dependent type. *)

Inductive inp2 : Type :=   f2_arg (x:nat) | g2_arg (x:Z).

Definition type_fg(x:inp2) := match x with f2_arg _ => nat | g2_arg _ => 
Z end.

(* We will use a measure to show that recursion terminates. *)

Definition inp2_nat (x:inp2) := match x with f2_arg n => n | g2_arg z => 
Zabs_nat z end.

(* Now we need to prove that recursive calls are made on decreasing 
arguments. *)

Lemma l1 :
 forall x, ~(x <= 0)%Z ->
  inp2_nat (f2_arg (Zabs_nat (x-1))) < inp2_nat (g2_arg x).
intros; simpl; apply Zabs_nat_lt; omega.
Qed.

Lemma l2 :
 forall x, inp2_nat (g2_arg (Z_of_nat x)) < inp2_nat (f2_arg (S x)).
intros; simpl; rewrite Zabs_nat_Z_of_nat; auto with arith.
Qed.

(* Well-founded induction works by using a functional, where recursive 
calls are represented
 by "protected" argument function, which can only be called on values 
where the measure
 decreases; this function is dependently typed and return values in the 
type corresponding to
 the argument. *)

Definition F :
 forall x:inp2,
   (forall y, inp2_nat y < inp2_nat x -> type_fg y) ->
   type_fg x :=
 fun x =>
   match x return
      (forall y, inp2_nat y < inp2_nat x -> type_fg y) -> type_fg x with
   | f2_arg v =>
     match v return
        (forall y, inp2_nat y < inp2_nat (f2_arg v) -> type_fg y) ->
           type_fg (f2_arg v) with
       0 => fun _ => 0
     | S p => fun f => Zabs_nat (2 + f (g2_arg (Z_of_nat p)) (l2 p))
     end
   | g2_arg v =>
     match Z_le_dec v 0 with
       left _ => fun f => 0%Z
     | right h => fun f => Z_of_nat (S (S (f (f2_arg (Zabs_nat (v-1)))
                                             (l1 v h))))
     end
   end.

(* To construct the functions, it only remains to call the Fix function 
with the right
parameters, especially with F *)

Definition h :forall x:inp2, type_f x :=
  Fix (well_founded_ltof inp2 inp2_nat) type_f F.

Definition f : nat -> nat := fun x => h (f2_arg x).

Definition g : Z -> Z := fun x => h (g2_arg x).

(* You can execute these functions inside Coq *)

Eval vm_compute in (f 10, g 3).

(* To reason on this function, it is useful to have the fixpoint 
equation. *)


Lemma h_eq :
 forall x, h x =
   match x return type_fg x with
     f2_arg v =>
     match v with
       0 => 0
     | S p => Zabs_nat (2 + g (Z_of_nat p))
     end
   | g2_arg x =>
     match Z_le_dec x 0 with
       left _ => 0%Z
     | right _ => Z_of_nat (S (S (f (Zabs_nat (x-1)))))
     end
   end.
assert (H :forall (x : inp2)
    (f g : forall y : inp2, ltof inp2 inp2_nat y x -> type_fg y),
  (forall (y : inp2) (p : ltof inp2 inp2_nat y x), f y p = g y p) ->
  F x f = F x g).
unfold F; intros [[ | p] | x] f' g' q;try (simpl;solve[auto]);
try(case (Z_le_dec x 0); intros h'); try rewrite q; try (simpl; 
solve[auto]).
intros x; rewrite (Fix_eq (well_founded_ltof _ inp2_nat) type_fg F H).
unfold F; destruct x as [[|n] | x]; auto.
case (Z_le_dec x 0); auto.
Qed.

(* The readable fixpoint equations are the following ones, which just 
appear in h_eq. *)
Lemma f_eq :
 forall x, f x =
   match x with 0 => 0 | S p => Zabs_nat (2 + g (Z_of_nat p)) end.
Proof (fun x => h_eq (f2_arg x)).

Lemma g_eq :
 forall y, g y =
    if Z_le_dec y 0 then 0%Z else Z_of_nat (S (S (f (Zabs_nat (y-1))))).
Proof (fun y => h_eq (g2_arg y)).

(* Now it is a good exercise to look at this example from the point of 
view of Bove-Capretta or
ad-hoc predicates. *)