The Coq mailing list

[Andrei Popescu <uuomul AT yahoo.com>]

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.