The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

I'm not sure it answers correctly your mail, but I cases like yours, 
it's often easier
to build functions interactively, and look at the built term.

If I want to build a function of the form you wrote, it can be done as 
follows:

Pierre


Definition Less n :={j| j< n}.

Definition restrict (n:nat)(f : Less (S n) -> nat) : Less n -> nat.
Proof.
intros n f X.
apply f.
case X;intros p Hp.
exists p;auto.
Defined.

Print restrict.

Require Import Max.


Definition supL (n:nat)(f:Less n -> nat):nat.
intro n;elim n.
intros;exact 0.
intros p Supp fp.
refine (max (fp (exist _ p _)) (Supp (restrict _ fp))).
auto.
Defined.

Print supL.





Andrei Popescu a écrit :
> I apologize for the potential amount of ignorance in this question, 
> justified by the fact that I am a beginner with Coq.
> Consider the definition:
> Definition Less n := {j | j < n}.
> And the following part of definition (some code is omitted)
> Fixpoint SupL (n:nat) (f:Less n -> nat) {struct n} : nat :=
> match n with
> ...
> |S n' => ... f (exist (fun j => j < n) n' (lt_n_Sn n')))...
> end.
> where
> lt_n_Sn: forall n : nat, n < S n
> The function SupL n f tries to compute the supremum of {f 0, f 1,...,f 
> (n-1)}, and employs the lemma le_n_Sn in an attempt to build the 
> necessary proof of n' < n. However,
> the definition of SupL does not type check, because (I quote):
> << The term "lt_n_Sn n' " has type "n' < S n' " while it is expected 
> to have type
> "(fun j : nat => j < n) n' " >>
> Even though I understand pragmatically what the problem is (n is not 
> identified to S n' ), I do not know how to fix it, since I do not know 
> how to produce a proof that the "volatile" n' is less than n. My more 
> general question is: after a match is performed, what facts are 
> available about the matched term and the matching pattern?
> Thank you in advance for any hint on this,
> Andrei Popescu
>
>
> ------------------------------------------------------------------------
> Be a better friend, newshound, and know-it-all with Yahoo! Mobile. Try 
> it now. 
> <http://us.rd.yahoo.com/evt=51733/*http://mobile.yahoo.com/;_ylt=Ahu06i62sR8HDtDypao8Wcj9tAcJ%20> 
> -------------------------------------------------------- Bug reports: 
> http://logical.futurs.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