coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proofs involving variables appeared from matching

From: Edsko de Vries <devriese AT cs.tcd.ie>
To: Andrei Popescu <uuomul AT yahoo.com>
Cc: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] proofs involving variables appeared from matching
Date: Mon, 28 Apr 2008 10:48:48 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi Andrei,

I think your problem can be solved by doing a dependent match instead,
something like this

Fixpoint SupL (n:nat) : (Less n -> nat) -> nat :=
  match n return (Less n -> nat) -> nat with
    ...
    |S n' => fun f => ... f (exist (fun j => j < n) n' (lt_n_Sn
n')))...
  end.

Now Coq will realize that the type of f changes in the various branches
of the match. See Coq'Art p 387 for more info.

Edsko

[Coq-Club] proofs involving variables appeared from matching, Andrei Popescu
- Re: [Coq-Club] proofs involving variables appeared from matching, Pierre Casteran
- Re: [Coq-Club] proofs involving variables appeared from matching, Edsko de Vries
  - Re: [Coq-Club] proofs involving variables appeared from matching, Matthieu Sozeau
  - Re: [Coq-Club] proofs involving variables appeared from matching, Andrei Popescu