The Coq mailing list

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

Le Sun, 25 Oct 2009 21:34:34 +0100, AUGER Cédric <Cedric.Auger AT lri.fr> 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