Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] More dependent pattern matching

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] More dependent pattern matching


chronological Thread 
  • From: rcp AT Cs.Nott.AC.UK
  • To: Edsko de Vries <devriese AT cs.tcd.ie>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] More dependent pattern matching
  • Date: 09 Jun 2008 16:13:46 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
  • Source-info: From (or Sender) name not authenticated.

I'm stuck again in trying to write some dependent code. I want to index a
vector:

  Section vectors.
Variable (A : Set).
Inductive vec : nat -> Set :=
    | vnil : vec 0
    | vcons : forall n, A -> vec n -> vec (S n).
Inductive fin : nat -> Set :=
    | finz : fin 1
| fins : forall n, fin n -> fin (S n). Fixpoint vind n (i : fin n) {struct i} : vec n -> A :=
    match i in fin n return vec n -> A with
| finz => fun v => match v in vec m return (match m with 0 => True | S _ => A end) with
        | vnil => I
        | vcons _ x _ => x
        end
    | fins m j => fun v =>
match v in vec m return (match m with 0 => True | S _ => A end) with
        | vnil => I
        | vcons m' _ xs => vind m j xs (* wrong *)
        end
    end.

vec A n is isomorphic to (Fin n -> A). If you intend to work with both vec and Fin, you should define this isomorphism, and you'd then be able to get the function you want rather easily.

Best,

RP>

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.





Archive powered by MhonArc 2.6.16.

Top of Page