The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  You can easily define such function using the new Program feature (Coq >= 8.2):

Section testing.

Variable P : forall i, i < 10 -> nat -> nat.

Program Fixpoint check (i : nat) (H : i < 10) : nat :=
  match i with
  | 0 => 0
  | S n => @P n _ (check n _)
  end.
Next Obligation. Proof. auto with arith. Qed.
Next Obligation. Proof. auto with arith. Qed.

Program Definition testing := check 5 _.
Next Obligation. Proof. auto with arith. Qed.

End testing.

  Cheers,
   Adam

On Tue, Apr 21, 2009 at 13:21, dimitrisg7 <dvekris AT hotmail.com> wrote:

Hi everyone.
In the code that follows, I would like to substitute cheating with an object
(H: i<10). Function testing uses recursion as you can see. Therefore, this
object should be constructed recursively for every call. Is there a easy way
to do that?

Thanks in advance!

Variable cheating : forall (A : Type), A.
Implicit Arguments cheating [A].

Definition testing (P: forall i, i < 10 -> nat -> nat)  : nat.
Proof.
intros.
refine ((fix check (i : nat) : nat :=
         match i with
           | 0 => 0
           | S n => P n cheating (check n)
         end) 5).
Qed.

-----
Never say never.
--
View this message in context: http://www.nabble.com/Question-on-recursion-tp23153959p23153959.html
Sent from the Coq mailing list archive at Nabble.com.

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

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================