Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] More dependent pattern matching


chronological Thread 
  • From: Edsko de Vries <devriese AT cs.tcd.ie>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] More dependent pattern matching
  • Date: Mon, 9 Jun 2008 14:56:22 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

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.

Unfortunately, this code does not typecheck; the line marked as (* wrong *)
gives

  Error:
  In environment
  A : Set
  vind : forall n : nat, fin n -> vec n -> A
  n : nat
  i : fin n
  m : nat
  j : fin m
  v : vec (S m)
  m' : nat
  a : A
  xs : vec m'
  The term "xs" has type "vec m'" while it is expected to have type "vec m"

It seems clear to me (but apparently not to the Coq typechecker) that m and m'
must be the same. Obviously, I can rewrite this code using inversion, but that
yields a large term which, moreover, includes an equality proof of m and m' --
which makes proofs more difficult because equality proofs are not transparent.
Is there another way?

Thanks,

Edsko 





Archive powered by MhonArc 2.6.16.

Top of Page