The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Using the Bove-Capretta method it is like this:

Require Import List.

(* The function itsself
 *
 * f (c:nat) (d:list nat) : nat
 * | 0   := 0
 * | S n := f n d + g n d.
 *
 * g (c:nat) (d:list nat) : nat
 * | nil := 0
 * | a::l := f c l + g c l.
 *
 *)

(* Accessability predicates *)
Inductive f_acc : nat -> list nat -> Prop :=
| f_acc_0 : forall d,
  f_acc 0 d
| f_acc_S : forall n d, 
  f_acc n d ->
  g_acc n d ->
  f_acc (S n) d
with g_acc : nat -> list nat -> Prop :=
| g_acc_nil : forall c,
  g_acc c nil
| g_acc_cons : forall c a l,
  f_acc c l ->
  g_acc c l ->
  g_acc c (a::l).

(* projections, which must be defined carefully to make the termination
checker later on happy *)
Definition f_acc_proj_1 {n d c} : c = S n -> f_acc c d -> f_acc n d.
intros.
destruct H0.
discriminate.
injection H.
intro.
subst n.
assumption.
Defined.

Definition f_acc_proj_2 {n d c} : c = S n -> f_acc c d -> g_acc n d.
intros.
destruct H0.
discriminate.
injection H.
intro.
subst n.
assumption.
Defined.

Definition g_acc_proj_1 {c a l d} : d = a::l -> g_acc c d -> f_acc c l.
intros.
destruct H0.
discriminate H.
injection H.
intros.
subst l a. 
assumption.
Defined.

Definition g_acc_proj_2 {c a l d} : d = a::l -> g_acc c d -> g_acc c l.
intros.
destruct H0.
discriminate H.
injection H.
intros.
subst l a. 
assumption.
Defined.

(* The function is defined by 'prop bounded recursion' here *)
Fixpoint f' (c:nat) (d:list nat) (acc:f_acc c d) {struct acc} : nat :=
  match c as c' return c = c' -> nat with
    | O => fun e : c = O => O
    | S n => fun e : c = S n =>
      f' n d (f_acc_proj_1 e acc) + g' n d (f_acc_proj_2 e acc)
  end (refl_equal c)
with g' (c:nat) (d:list nat) (acc:g_acc c d) {struct acc} : nat :=
  match d as d' return d = d' -> nat with
    | nil => fun e : d = nil => O
    | a::l => fun e : d = a::l =>
      f' c l (g_acc_proj_1 e acc) + g' c l (g_acc_proj_2 e acc)
  end (refl_equal d).


(* Now to produce f and g, we should show that they are total by proving
their domain is accessible *)
Require Import Program.

Definition pif (c:nat) (d:list nat) := c + length d.

(* I tried to prove it in this way, but it did not work .. *)
(*
Program Fixpoint fg_Acc c d {measure (pif c d)} : f_acc c d /\ g_acc c d
  conj
  (match c with
     | O => f_acc_0 d
     | S n => f_acc_S n d (proj1 (fg_Acc n d)) (proj2 (fg_Acc n d))
   end)
  (match d with
    | nil => g_acc_nil c
    | a::l => g_acc_cons c a l (proj1 (fg_Acc c l)) (proj2 (fg_Acc c l))
   end).

*)

Theorem f_Acc : forall c d, f_acc c d
with    g_Acc : forall c d, g_acc c d.
Admitted.

(* Anyway, then you define: *)
Definition f c d := f' c d (f_Acc c d).
Definition g c d := g' c d (g_Acc c d).


-- 
View this message in context: 
http://www.nabble.com/Mutual-definition-using-a-well-founded-measure-tp23724448p23727027.html
Sent from the Coq mailing list archive at Nabble.com.