The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

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