The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-11-09 11:33 GMT+01:00 John Wiegley <johnw AT newartisans.com>:

Hello,

I'm having difficulty proving the following, using Coq.Vectors.Vector:

    Lemma nth_replace {A : Type} : forall n (v : t A n) k x,
      nth (replace v k x) k = x.

The induction principle is unable to accept an argument of type t A n.+1.  Is
this a case where a custom principle is needed?  What form would that take?
I've tried a few, but nothing so far has allowed me to progress.

Any help is greatly appreciated,
  John

​Which induction principle are you speaking of?

The one on nat (n) or on vector (v)?

The way I would start the proof would be:

intros n v k x.

revert k. (* It will have to be changed over the calls unlike x *)

induction v.​

​Starting by induction on n would be more annoying.

Still if you prefer to do induction on n, I would rather recommand the following definition of vector:

Definition vector (A:Type) : nat -> Type :=

  fix vec n := match n with O => Empty_set | S n => prod A (vec n) end.

This way dependant types will be less annoying to deal with.

The reason is that inductive types have two kind of arguments:

- parameters (left of the :) which are not to be pattern matched

- indices (right of the :) which are to be pattern matched

Example with the a vector type:

Inductive is_succ (n : nat) : nat -> Type :=

| is_succ_intro : is_succ n (S n).

Inductive vector_p (A:Type) (n:nat) : Type :=

| VO : n=O -> vector_p A n

| VS : forall m, is_succ m n -> vector_p A m -> A -> vector_p A n.

Here, second argument of is_succ, but first is a parameter.

That is first argument is not constrained, although the second one is.

In vector_p, all arguments are parameters, I used is_succ to establish a link between the "nat" in the recursive calls. Most of the time parameters are kept the same along the calls ("A" for example). But here, it is not the case for "n". An other common example where the parameter changes is in the definition of Acc.

The standard definition is more straightforward and uses an indice:

​Inductive vector_i (A:Type) : nat -> Type :=

| VO : vector_i A O

| VS : forall n, vector_i A n -> A -> vector_i A (S n).

When indices are involved, the pattern matching rules to be used are more complex. That is why you will need to use "inversion" instead of "destruct" in proofs, and that is why I recommend not to define inductive with indices if you can define them with parameters with no cost.

So if you start proof by induction on "n" and want to stick with the standard definition, you will find useful to use "inversion v" later in your proof.

​

--

.../Sedrikov\...