The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

this definition works just as well with Program in Coq v8.1. 

You just don't get any obligations to solve as the default tactic

included [auto with *] at this time.

-- Matthieu

Le 21 avr. 09 à 09:22, Adam Koprowski a écrit :

   Dear Dimitri,
  Sure, you can do the same thing without Program, but it gets slightly more complicated as you need to manually get the equality for the pattern-matched variable:

Section testing.

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

Definition check (i : nat) (H : i < 10) : nat.
Proof.
  refine (fix check (i : nat) (H : i < 10) {struct i} : nat :=
    match i as j return i = j -> nat with
    | 0 => fun _ => 0
    | S n => fun ij => P n _ (check n _)
    end refl); subst; auto with arith.
Defined.

End testing.

  Hope that helps,
  Adam

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

Thanks Adam. But I am not familiar with the new features of Coq. I still use
the previous version. I am wondering if there is still something that can be
done with "old" Coq. If not, I might consider seriously to switch to the new
version.

-----
Never say never.
--
View this message in context: http://www.nabble.com/Question-on-recursion-tp23153959p23155523.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)
=====================================================