Skip to Content.
Sympa Menu

coq-club - [Coq-Club] trying to use Init.Wf.Fix .

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] trying to use Init.Wf.Fix .


chronological Thread 
  • From: dehlinge AT dpt-info.u-strasbg.fr
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] trying to use Init.Wf.Fix .
  • Date: Wed, 5 May 2004 17:34:42 +0200 (CEST)
  • Importance: Normal
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi all,

I'm trying to translate the following function into Coq :
        f n = 0         if n=1
        f n = n+1       if n is even
        f n = n-3       if n is odd

Obviously, a simple Fixpoint with n as the variable will not work, as n
isn't structurally decreasing. So I tried to  use the Fix function,
defined in the Wf library.

Set Implicit Arguments.
Require Export Arith.
Require Export Even.
Require Export Peano_dec.
Require Export Wf_nat.

(* creating a well-founded relation between the argument value of a
recursive call and the original value*)

Inductive l : nat -> nat -> Prop :=
          L : forall n : nat, (even n)->(l (S n) n)
        | L2 : forall n : nat, n<>1->(odd n)->(l (n-3) n).


Lemma WFL :
        well_founded l.
Proof.
intro n.
apply (lt_wf_ind n (Acc l)).
clear n.
intros n rec.
constructor.
intros y l1.
inversion l1.
generalize l1.
rewrite <- H0.
rewrite H1.
clear H1 H0 H n0 l1 y.
unfold next in |- *.
elim (even_odd_dec n); intros.
 constructor.
   intros.
   inversion H.
   unfold next in |- *.
   elim (even_odd_dec (S n)); intros.
  elim (not_even_and_odd (S n)); auto with arith.
  apply rec.
    destruct n.
   elim H0.
     auto.
   unfold lt in |- *.
     rewrite minus_Sn_m.
    simpl in |- *.
      rewrite <- minus_n_O.
      apply le_S.
      apply le_n.
    do 2 apply le_n_S.
      destruct n.
     inversion a.
       inversion H4.
     apply le_n_S.
       apply le_O_n.
 apply rec.
   destruct n.
  inversion b.
  unfold lt in |- *.
    apply le_n_S.
    simpl in |- *.
    apply le_minus.
Defined.

Definition f : nat->nat := Fix WFL (fun _ => nat)
        (fun (x:nat) (rec:(forall y : nat, l y x -> nat)) =>
                match (eq_nat_dec x 1) with
                  (left _) => 0
                | (right neqx1) =>
                        (match (even_odd_dec x) with
                          (left e) => rec _ (L e)
                        | (right o) => rec _ (L2 neqx1 o)
                        end)
                end).


Now I've got my function. My question is : how do I use it ? I tried
  Eval compute (f 1).
as well as other flag combinations, but the only computations that occur
are within f itself; there is no fixpoint reduction with 1 and (WFL 1),
and I can't see why. Note that this computation doesn't even need any
recursive calls.

Thanks for any insight.

Christophe Dehlinger
LSIIT, UMR 7005, CNRS & Louis-Pasteur University (Strasbourg 1),
Pole Technologique, Boulevard S. Brant, BP 10413, 67412 Illkirch





Archive powered by MhonArc 2.6.16.

Top of Page