Co-recursion question

[Jeffrey Harris-5]

Hello!

I apologize for the imprecise phrasing, but does anyone know if the ability to do coinduction/corecursion in Coq expands the class of definable functions on inductive types? For instance, is there any function from nat->nat which is definable in Coq, but would not be definable without the use of coinduction/corecursion? (So, perhaps, a composition of functions f1:nat->stream and f2:stream->nat).

Thanks,
Jeffrey

[Yves Bertot]

Jeffrey Harris wrote:

> Hello!
>
> I apologize for the imprecise phrasing, but does anyone know if the ability
> to do coinduction/corecursion in Coq expands the class of definable
> functions on inductive types? For instance, is there any function from
> nat->nat which is definable in Coq, but would not be definable without the
> use of coinduction/corecursion? (So, perhaps, a composition of functions
> f1:nat->stream and f2:stream->nat).
>
> Thanks,
> Jeffrey
>
>  

My opinion is no.   Every function from an inductive type to an
inductive type defined using co-recursion could have been defined
without co-recursion.  Co-recursion brings in  non-functional
characteristics such as better use of memory and memoizing of
pre-computed results, but not the possibility to model more function (in
an extensional sense).

The paper Ekaterina Komendantskaya and I wrote in 2008 on the subject ,
"Using structural recursion for Corecursion",
http://hal.inria.fr/inria-00322331/en/,  shows how co-recursive
functions on streams can be replaced by structural recursive functions
from nat.  There is a particular brotherhood between nat and
stream that makes the replacement easy, but the brotherhood can be
generalized in two ways.

Here a few quick thoughts,

1/ You take any declaration of a co-inductive datatype T, you add a
singleton constructor "NYE" to represent "not yet explored" and you make
the type inductive (call it T').  Then you can define an order on
elements of this datatype, where NYE <= e for any e, and this order is a
congruence with respect to all the constructors. Then elements of T are
limits of increasing sequences in T'.  The guardedness principle
corresponds to using structural recursion while defining such an
increasing sequence, with an extra constraint that every NYE constructor
present in the term t_n must be replaced by another constructor in the
term t_{n+1}.  This forces you to define the increasing sequence in such
a way that all elements of  T' of size n are obtained in less than n
steps.  The term t_n in the sequence correspond to "what you can
construct after n co-recursive calls".

2/ For every co-inductive datatype T with constructors C1 .... Cn, if
each constructor Ci has type A1 -> ... -> Ap -> T -> ... -> T -> T, you
can define an inductive type T' with n constructors with types
C'i : A1 -> ... -> Ap -> T'.

Then every term of  T can be represented by a structurally recursive
function of type list nat -> T'.

Actually, we can replace nat by any enumerated type containing more
elements than the larger arity in T of the constructors Ci (what I call
the arity in T is the number of T arguments of the constructor).

On a more concrete example, if we consider the following co-inductive type:

CoInductive Yt1 : Type :=
  C1 : Z -> string -> Yt1 -> Yt1 -> Yt1
| C2 : bool -> Yt1 -> Yt1
| C3 : Yt1.

We define the type Yt1' in the following manner:
Inductive Yt1' : Type :=
  C1' : Z -> string -> Yt1'.
| C2' : bool -> Yt1'
| C3' : Yt1'.

The corecursive value v1 defined by:

CoFixpoint v1 : Yt1 := C1 3 "hello" C3 v1.

can be represented by the function

Fixpoint v1' (p : list nat) : Yt1' :=
match p with
  nil => C1' 3 "hello"
| 0::p' => C3'
| 1::p' => v1' p'
end.

However, the same term v1 is also represented by the following different
function:

Fixpoint v1' (p : list nat) : Yt1' :=
match p with
  nil => C1' 3 "hello"
| 0::p' => match p with nil => C3' | _ => C2' true end
| 1::p' => v1' p'
end.

In the case of Streams, the type of paths can be reduced to the type
list unit, because the maximal arity is one.
and list unit is isomorphic to nat.  Also, there is only one
constructor, with only one non-Stream component, so
that the type Stream' would be an inductive type with only one
constructor that has only one component, thus isomorphic to the type of
values carried in the stream. This is why we use functions of type nat
-> A in the paper with Ekaterina, where we show the procedure to
transform every stream value into a structurally recursive function.

The use of dependent types for the constructors adds more complications,
but still I believe that they don't add more on the co-inductive side
than on the inductive side.

Yves

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Jeffrey Harris-5]

Thank you for your detailed reply.

Jeffrey

On Sun, Oct 25, 2009 at 2:48 AM, Yves Bertot <Yves.Bertot@...> wrote:

Jeffrey Harris wrote:

Hello!

I apologize for the imprecise phrasing, but does anyone know if the ability
to do coinduction/corecursion in Coq expands the class of definable
functions on inductive types? For instance, is there any function from
nat->nat which is definable in Coq, but would not be definable without the
use of coinduction/corecursion? (So, perhaps, a composition of functions
f1:nat->stream and f2:stream->nat).

Thanks,
Jeffrey

 

My opinion is no.   Every function from an inductive type to an inductive type defined using co-recursion could have been defined without co-recursion.  Co-recursion brings in  non-functional characteristics such as better use of memory and memoizing of pre-computed results, but not the possibility to model more function (in an extensional sense).

The paper Ekaterina Komendantskaya and I wrote in 2008 on the subject , "Using structural recursion for Corecursion", http://hal.inria.fr/inria-00322331/en/,  shows how co-recursive functions on streams can be replaced by structural recursive functions from nat.  There is a particular brotherhood between nat and
stream that makes the replacement easy, but the brotherhood can be generalized in two ways.

Here a few quick thoughts,

1/ You take any declaration of a co-inductive datatype T, you add a singleton constructor "NYE" to represent "not yet explored" and you make the type inductive (call it T').  Then you can define an order on elements of this datatype, where NYE <= e for any e, and this order is a congruence with respect to all the constructors. Then elements of T are limits of increasing sequences in T'.  The guardedness principle corresponds to using structural recursion while defining such an increasing sequence, with an extra constraint that every NYE constructor present in the term t_n must be replaced by another constructor in the term t_{n+1}.  This forces you to define the increasing sequence in such a way that all elements of  T' of size n are obtained in less than n steps.  The term t_n in the sequence correspond to "what you can construct after n co-recursive calls".

2/ For every co-inductive datatype T with constructors C1 .... Cn, if each constructor Ci has type A1 -> ... -> Ap -> T -> ... -> T -> T, you can define an inductive type T' with n constructors with types
C'i : A1 -> ... -> Ap -> T'.
Then every term of  T can be represented by a structurally recursive function of type list nat -> T'.

Actually, we can replace nat by any enumerated type containing more elements than the larger arity in T of the constructors Ci (what I call the arity in T is the number of T arguments of the constructor).

On a more concrete example, if we consider the following co-inductive type:

CoInductive Yt1 : Type :=
 C1 : Z -> string -> Yt1 -> Yt1 -> Yt1
| C2 : bool -> Yt1 -> Yt1
| C3 : Yt1.

We define the type Yt1' in the following manner:
Inductive Yt1' : Type :=
 C1' : Z -> string -> Yt1'.
| C2' : bool -> Yt1'
| C3' : Yt1'.

The corecursive value v1 defined by:

CoFixpoint v1 : Yt1 := C1 3 "hello" C3 v1.

can be represented by the function

Fixpoint v1' (p : list nat) : Yt1' :=
match p with
 nil => C1' 3 "hello"
| 0::p' => C3'
| 1::p' => v1' p'
end.

However, the same term v1 is also represented by the following different function:

Fixpoint v1' (p : list nat) : Yt1' :=
match p with
 nil => C1' 3 "hello"
| 0::p' => match p with nil => C3' | _ => C2' true end
| 1::p' => v1' p'
end.

In the case of Streams, the type of paths can be reduced to the type list unit, because the maximal arity is one.
and list unit is isomorphic to nat.  Also, there is only one constructor, with only one non-Stream component, so
that the type Stream' would be an inductive type with only one constructor that has only one component, thus isomorphic to the type of values carried in the stream. This is why we use functions of type nat -> A in the paper with Ekaterina, where we show the procedure to transform every stream value into a structurally recursive function.

The use of dependent types for the constructors adds more complications, but still I believe that they don't add more on the co-inductive side than on the inductive side.

Yves

[Dan Doel]

On Sunday 25 October 2009 11:00:03 am Jeffrey Harris wrote:
> Thank you for your detailed reply.

There's actually an even simpler implementation of plain coinductive types
than Yves mentioned (although, not simpler than Nat -> A for Stream A). It's
similar to a Church encoding of an inductive type; one encodes a coinductive
type by the information needed to unfold it. So if your type is "ν X. F X", F
being the shape functor (specifying the destructors), then the encoding is:

  νF = ∃ (S : Type). S × (S → F S)

  unfold step seed = (seed, step)
  observe (seed, step) = map (λ seed'. (seed', step)) (step seed)

I left the mucking with the existential quantification out of the above, but
hopefully it's still comprehensible. This encoding might bump things up a
universe level* (unless you use Set with impredicativity), but it actually
mimics the underlying foundation of coinductive types pretty well. For
instance, since Church encodings have weaker eliminators than their
corresponding inductive type, you might expect the above encoding to be weaker
in some way (I did), but equality proofs on coinductives (for instance) are
extensional anyway, and the observation produces (presumably) a type with
actual constructors, so perhaps things are covered. In fact, the dual of
stronger eliminators might be stronger introduction rules for coinductives,
but I couldn't come up with any such thing thinking about it for a while.

One significant difference with the coinductives in Coq is that this doesn't
have issues with subject reduction. Values of νF are opaque, and all you can
do is call "observe" on them, and use the result. They are not treated as
actually being *made* out of the constructors of F, and subject to evaluation
by case analysis. This means that there are things you can't prove about them
that you could prove about Coq coinductives (for instance, way back I think
someone showed how to prove intensional equality via bisimulation), but
arguably, you shouldn't be able to prove them in Coq either.

The other issue is how well this extends to indexed types and families, which,
I suspect it doesn't very nicely. But it does indicate that plain coinductive
types aren't likely to give you increased computational power.

Cheers,

-- Dan

* I noticed while trying to do this in Agda that the universe bump makes this
encoding extra painful, because "F νF" is not a valid construction. F has type
Set -> Set, while νF has type Set1, so observe isn't well typed.
Impredicativity solves this, of course, since νF : Set is allowed, but I think
it might not actually be a problem in Coq even with Type, due to universe
polymorphism. However, my Coq-fu is too weak to test this hypothesis, so it's
an exercise left to the reader. :) I have got it working with Agda's
experimental universe polymorphism:

data ℕ-Shape {i : Level} (X : Set i) : Set i where
  z : ℕ-Shape X
  s : X → ℕ-Shape X

map-ℕ : ∀{i j} {X : Set i} {Y : Set j} → (X → Y) → ℕ-Shape X → ℕ-Shape Y
map-ℕ f z     = z
map-ℕ f (s x) = s (f x)

data ∃ {i : Level} (T : Set i → Set i) : Set (suc i) where
  _,_ : (S : Set i) (t : T S) → ∃ T

Coℕ : Set₁
Coℕ = ∃ λ S → S × (S → ℕ-Shape S)

obs-Coℕ : Coℕ → ℕ-Shape Coℕ
obs-Coℕ (S , (seed , step)) =
  map-ℕ (λ seed' -> (S , (seed' , step))) (step seed)

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[AUGER Cédric]

Hi, all; in Coq, there is currently no way for Function to produce  
mutually recursive functions with wf or measure, as far as I know.

For some functions, we may want to use a rev to a list to avoid stack  
overflows in extracted code in ocaml (I don't know if tail-recursion is  
meaningful for haskell/scheme).

Doing this can break mutual structural recursion.

So I explored a little this problem, and would appreciate what you think  
of this:

-Can it easily be generalized to be implemented by Function?
-Is there a way to modify g_rec, so that it doesn't require the u  
parameter anymore?
-Is there a way to define f_rec and g_rec such that no Obj.t will be  
generated?
=============================================================================
Set Implicit Arguments.

(** * utree : trees of unit *)
(** The aim is to provide a structure to test
     mutual recursion with non structural recursion;
     as exemple, here is an induction principle for type Set,
     with a fold-right defined as a fold left on a reverse;
     it can be useful for extraction, since induction principles
     are naturally fold-right, but using a (tail-recursive) fold-left
     on a reverse does the same thing but breaks the structural induction *)
Inductive utree :=
| L : utree                       (* Leaf *)
| N : lutree -> utree             (* Node *)
with lutree :=
| E : lutree                      (* nil *)
| C : utree -> lutree -> lutree.  (* cons *)
(** Note that the "L" constructor is not mandatory, it only
     make the recursion (a bit) more complex, but I am not
     sure it makes it more interesting. *)

Inductive eertul :=
| F : eertul
| D : eertul -> utree -> eertul.
(** [eertul] type is isomorph to [lutree]; the aim to make a stand alone  
type
is to keep in mind it is the reverse of a list *)

Fixpoint rev l acc :=
match l with
| E => acc
| C a b => rev b (D acc a)
end.

(** * Now, we define functions to use while folding *)
Record inductions A B :=
{ uL : A;
   uN : B -> A;
   uF : B;
   uD : A -> B -> B
}.

(** * And some relation for well foundness *)
Definition bigger1 u :=
match u with
| L => fun _ => False
| N l => fun m => exists n, rev l F = rev n m
end.
Definition IN v :=
  fix IN l := match l with E => False | C a b => a = v \/ IN b end.
Definition bigger2 u :=
match u with
| L => fun _ => False
| N l => fun v => IN v l
end.
Inductive ACC u : Prop :=
ACC_intro : (forall u', bigger2 u u' -> ACC u') -> ACC u.

(** * Some lemmas for our recursions *)
(** an analog of IN for reversed lists *)
Definition IN_ v :=
  fix IN_ l := match l with F => False | D b a => a = v \/ IN_ b end.
Fixpoint append l :=
match l with
| F => fun m => m
| D b a => fun m => D (append b m) a
end.
Lemma lemAA : forall x y z, append (rev x y) z = rev x (append y z).
Proof.
   induction x; simpl; intros.
     reflexivity.
     apply IHx.
Qed.
Lemma lemA : forall x y, rev x y = append (rev x F) y.
Proof.
   intros; rewrite lemAA; reflexivity.
Qed.

(** The recursion engine *)
Definition g_rec A B : forall
(k : inductions A B)
(u : utree)
(f_rec : forall u' : utree, bigger2 u u' -> A),
          forall e : eertul, bigger1 u e -> B -> B.
Proof.
   refine (fun A B k u f_rec =>
               fix g_rec e :=
               match e as e0 return bigger1 u e0 -> B -> B with
               | F => fun _ acc => acc
               | D a b => fun Hbig acc => g_rec a _ (k.(uD) (f_rec b _) acc)
               end);
   (* cleaning, avoiding non structured recursion application *)
     clear g_rec e.
   (* 1st proof obligation *)
     destruct u; simpl in *; auto.
     destruct Hbig as [x Hbig].
     exists (C b x); simpl; assumption.
   (* 2nd proof obligation *)
     clear f_rec acc.
     destruct u; simpl in *; auto.
     destruct Hbig as [x Hbig].
     assert (IN b l \/ IN_ b F).
       revert Hbig; generalize F.
       induction l; simpl; intros e Hbig.
         right; rewrite Hbig; clear Hbig e.
         rewrite lemA; generalize (rev x F); clear x.
         induction e; simpl.
           left; reflexivity.
         right; assumption.
       destruct (IHl (D e u) Hbig) as [in_b_l | in_b_e]; clear Hbig IHl.
         left; right; assumption.
       simpl in in_b_e; destruct in_b_e; [left; left|right]; assumption.
     destruct H as [evidence | absurd].
       exact evidence.
     destruct absurd.
Qed.

Definition f_rec A B (k : inductions A B) : forall u, ACC u -> A.
Proof.
   refine (fun A B k => fix f_rec u a :=
           match a with
           | ACC_intro h =>
              (match u as u0 return u = u0 -> A with
               | L => fun _ => k.(uL)
               | N l => fun Heq => k.(uN) (g_rec k u
                                             (fun u H => f_rec u (h u H))
                                             (rev l F)
                                             _
                                             k.(uF))
               end) (refl_equal u)
           end);
   (* cleaning, avoiding non structured recursion application *)
     clear f_rec a.
   (* 1st proof obligation *)
     rewrite Heq; clear Heq u h; simpl.
     exists E; easy.
Defined.

Theorem utree_well_founded : forall u, ACC u.
Proof.
   refine (fix uwf u : ACC u :=
               match u with
               | L => ACC_intro _ (fun u' H => _)
               | N l => ACC_intro _ (fun u' H => _)
               end);
   simpl in H.
     destruct H.
   induction l; simpl in H; destruct H.
     rewrite <- H; exact (uwf u0).
     exact (IHl H).
Qed.

(** * Finalization *)
Definition f_rec_extraction_ready :=
(*Eval compute in*) fun A B k u =>
  @f_rec A B k u (utree_well_founded u).

Extract Inductive bool => bool [true false].
Extract Inductive lutree => "utree list" ["[]" "(::)"].
Extract Inductive eertul => "utree list" ["[]" "(::)"].

Recursive Extraction f_rec_extraction_ready.

(** We now have a fold function which uses tail-recursion
on the [utree list] *)

(** * Some alternative *)
Record funs A B :=
{ utree_fun : utree -> A;
   eertul_fun : eertul -> B -> B
}.
Notation "{ 'utree_fun' = u ; 'eertul_fun' = e }" := (Build_funs u e).
Record pars :=
{ up : utree;
   ep : eertul
}.
Notation "{ 'up' = u ; 'ep' = e }" := (Build_pars u e).
Record res A B :=
{ ur : A;
   er : B -> B
}.
Notation "{ 'ur' = u ; 'er' = e }" := (Build_res u e).
Notation "'app_funs'" := (fun funs pars =>
{ ur = funs.(utree_fun) pars.(up);
   er = funs.(eertul_fun) pars.(ep)
}).
Definition funs_F A B (k : inductions A B) funs :=
{ utree_fun = fun u => match u with
                        | L => k.(uL)
                        | N l => k.(uN) (funs.(eertul_fun) (rev l F) k.(uF))
                        end;
   eertul_fun = fun l acc => match l with
                | F => acc
                | D a b => funs.(eertul_fun) a (k.(uD) (funs.(utree_fun) b)  
acc)
                end
}.

Fixpoint gt a :=
match a with
| O => fun _ => False
| S k => fun m => match m with O => True | S n => gt k n end
end.

Fixpoint max a :=
match a with
| O => fun b => b
| S k => fun m => match m with O => S k | S n => S (max k n) end
end.

Variable smaller : pars -> pars -> Prop.

Definition embeded A B (k : inductions A B) :
  forall (p : pars) (P : Acc smaller p), (res A B).
refine (fun A B k => fix emb p a := match a with Acc_intro f => _
end).
assert (sub := fun p H => emb p (f p H)); clear a emb f.
destruct p as [u_p e_p].
assert (u : A).
destruct u_p as [|l].
exact k.(uL).
destruct (sub {up=L; ep=rev l F}) as [_ r].
clear sub.
admit.
exact (k.(uN) (r k.(uF))).
assert (e : B -> B).
destruct e_p as [|a b].
exact (fun x => x).
destruct (sub {up=b; ep=a}) as [ru re].
clear sub u.
admit.
exact (fun acc => re (k.(uD) ru acc)).
exact {ur = u; er = e}.
Qed.

(** Then we have to define a fixpoint with embeded with function and
consider the projections; unhappily, I didn't succeed in using Function  
for this pourpose *)

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Thorsten Altenkirch]

Hi Jeffrey,

the answer is no, because in extensional Type Theory coinductive types  
can be encoded using inductive types. And as far as the strength of  
the theory is concerned there is no difference between extensional and  
intensional Type Theory. For me detail see our paper

@Article{alti:cont-tcs,
  author = {Michael Abott and Thorsten Altenkirch and Neil Ghani},
  title = {Containers - Constructing Strictly Positive Types},
  journal = {Theoretical Computer Science},
  year = {2005},
  volume = {342},
  pages = {3--27},
  month = {September},
  note = {Applied Semantics: Selected Topics},
}
available from my webpage http://www.cs.nott.ac.uk/~txa/publ/cont-tcs.pdf

In section 4 we show how to derive M-types from W-types and this is  
enough because all strictly positive types can be constructed from W-  
and M-types. The basic idea can be concisely expressed in the language  
of category theory: every signature functor is \omega-continous hence  
its terminal coalgebra can be constructed as an \omega-limit and  
'omega-limits are easily definable within Type Theory.

Cheers,
Thorsten

On 25 Oct 2009, at 00:14, Jeffrey Harris wrote:

> Hello!
>
> I apologize for the imprecise phrasing, but does anyone know if the  
> ability to do coinduction/corecursion in Coq expands the class of  
> definable functions on inductive types? For instance, is there any  
> function from nat->nat which is definable in Coq, but would not be  
> definable without the use of coinduction/corecursion? (So, perhaps,  
> a composition of functions f1:nat->stream and f2:stream->nat).
>
> Thanks,
> Jeffrey

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[AUGER Cédric]

Le Sun, 25 Oct 2009 21:34:34 +0100, AUGER Cédric <Cedric.Auger@...> a  
écrit:

> Hi, all; in Coq, there is currently no way for Function to produce  
> mutually recursive functions with wf or measure, as far as I know.
>
> For some functions, we may want to use a rev to a list to avoid stack  
> overflows in extracted code in ocaml (I don't know if tail-recursion is  
> meaningful for haskell/scheme).
>
> Doing this can break mutual structural recursion.
>
> So I explored a little this problem, and would appreciate what you think  
> of this:
>
> -Can it easily be generalized to be implemented by Function?

What I did seems quite hard to generalize...

> -Is there a way to modify g_rec, so that it doesn't require the u  
> parameter anymore?

Couldn't find a way to do it, but inlining g_rec_aux in g_rec with an
Eval compute works as g_rec_aux is no more extracted ...

> -Is there a way to define f_rec and g_rec such that no Obj.t will be  
> generated?

Ok, it was trivial, just had to change the f_rec parameter in g_rec_aux

I am not sure such an example would be worth an advanced tutorial, but if  
you are interested, write me.

> =============================================================================

Definition g_rec_aux A B : forall
(k : inductions A B)
(u : utree)
(f_rec : {u' : utree | bigger2 u u'} -> A),
forall (e : eertul), bigger1 u e -> B -> B.
Proof.
   refine (fun A B k u f_rec =>
               fix g_rec e :=
               match e as e0 return bigger1 u e0 -> B -> B with
               | F => fun _ acc => acc
               | D a b => fun Hbig acc => g_rec a _ (k.(uD) (f_rec (exist _  
b _)) acc)
               end);
   (* cleaning, avoiding non structured recursion application *)
     clear g_rec e.
   (* 1st proof obligation *)
     exact (bigger1_bigger1 u a b Hbig).
   (* 2nd proof obligation *)
     exact (bigger1_bigger2 u a b Hbig).
Defined.

Definition f_rec_aux A B (k : inductions A B) : forall u, ACC u -> A.
Proof.
   refine (fun A B k => fix f_rec u a :=
           match a with
           | ACC_intro h =>
              (match u as u0 return u = u0 -> A with
               | L => fun _ => k.(uL)
               | N l => fun Heq => k.(uN) (g_rec_aux k u
                                             (fun u => let (u, pi) := u in
                                                  f_rec u (h u pi))
                                             (rev l F)
                                             _
                                             k.(uF))
               end) (refl_equal u)
           end);
   (* cleaning, avoiding non structured recursion application *)
     clear f_rec a.
   (* 1st proof obligation *)
     exact (bigger1_N Heq).
Defined.
=================================================================================
(** * Finalization *)
Definition f_rec A B k u :=
(*Eval compute in*)
  @f_rec_aux A B k u (utree_well_founded u).

Definition g_rec A B (k : inductions A B) :=
(*Eval compute in*)
   fix g_rec e acc :=
       match e with
       | F => acc
       | D a b => g_rec a (k.(uD) (f_rec k b) acc)
       end.

(** * equations *)
(** first a simple induction principle *)
(* strangely, Scheme Equality for utree. it doesn't work here *)
Lemma g_rec_equation :
   forall A B (k : inductions A B) e,
   g_rec k e =
   match e with
   | F => fun acc => acc
   | D a b => fun acc => g_rec k a (k.(uD) (f_rec k b) acc)
   end.
Proof.
   intros.
   destruct e; simpl.
     reflexivity.
   reflexivity.
Qed.
Lemma f_rec_aux_irrelevant :
   forall A B (k : inductions A B) u (H K : ACC u),
   f_rec_aux k H =
   f_rec_aux k K.
Proof.
   intros A B k.
   refine (fix frai u H {struct H} :=
           match H with
           | ACC_intro h => let rec := fun u0 H => frai u0 (h u0 H) in _
           end
           ); assert (REC := rec); subst rec; clear frai H.
   destruct u; simpl.
     intro K; case_eq K; simpl; intros _ _; reflexivity.
   intro K; case_eq K; simpl; intros; f_equal; generalize (uF k);
   generalize (bigger1_N (refl_equal (N l))); generalize (rev l F).
   induction e; simpl.
     reflexivity.
   intros.
   rewrite IHe; clear IHe.
   rewrite (REC _ _ (a u (bigger1_bigger2 (N l) e u b))); reflexivity.
Qed.
Lemma f_rec_equation :
   forall A B (k : inductions A B) u,
   f_rec k u =
   match u with
   | L => k.(uL)
   | N l => k.(uN) (g_rec k (rev l F) k.(uF))
   end.
Proof.
   intros; unfold f_rec.
   case_eq (utree_well_founded u); intros a _.
   destruct u; simpl.
     reflexivity.
   f_equal; generalize (bigger1_N (refl_equal (N l))); simpl; generalize  
(uF k).
   set (m := rev l F) at 2 3 4; generalize m; subst m.
   induction m; simpl; intros.
     reflexivity.
   rewrite IHm; clear IHm.
   unfold f_rec.
   f_equal; f_equal.
   apply f_rec_aux_irrelevant.
Qed.

Extract Inductive bool => bool [true false].
Extract Inductive lutree => "utree list" ["[]" "(::)"].
Extract Inductive eertul => "utree list" ["[]" "(::)"].

Recursive Extraction g_rec.

> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club