Dear Coqers,

I would like to understand whether there is a chance to define a coercing for length-indexed lists.

In particular, I would like to coerce `vec t (n +1)`

to `vec t (S n)`

which is of course readily given by Lemma `Nat.add_1_r`

.

More precisely, given the following standard definition:

```
Inductive vec t : nat -> Type :=
| Nil: vec t 0
| Cons: forall n, t -> vec t n -> vec t (S n).
Arguments Nil {t}%type_scope.
Arguments Cons {t n}%type_scope _ _.
Fixpoint app {t n1 n2} (l1:vec t n1) (l2:vec t n2) : vec t (n1 + n2) :=
match l1 in (vec _ n1) return (vec t (n1+n2)) with
| Nil => l2
| Cons x xs => Cons x (app xs l2)
end.
```

Coercing `vec t (1+n)`

to `vec t (S n)`

does work:

```
Lemma coerce_1_plus_n:
forall (t:Type) (n:nat) (xs:vec t n) (x:t),
Cons x xs = app (Cons x Nil) xs.
Admitted.
```

But the following coercion does not work:

```
Fail Lemma coerce_n_plus_1:
forall (t:Type) (n:nat) (xs:vec t n) (x:t),
Cons x xs = app xs (Cons x Nil).
```

I know, this equality does not hold. But given Lemma `Nat.add_1_r`

, it could/should type-check.

I have a feeling that this may not be possible due to what is written here:

https://stackoverflow.com/questions/70726083/coq-coercion-of-list-nat

But I nevertheless wanted ask.

Any help would be greatly appreciated.

Thanks,

Sebastian.

The short answer is that `1 + n = S n`

and `n + 1 = S n`

are subtly but crucially different — the first is a definitional equality (so the typechecker will use it automatically without inserting coercions), the latter is a propositional equality (so the typechecker can't use it automatically on its own). And indeed, your link explains one reason why defining `Coercion`

s between `vector A (n + 1)`

and `vector A (S n)`

wouldn't help here.

In general, these useless type errors are why vectors are a questionable idea. Quoting a thread right now:

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Padding.20bitvectors/near/358414689

Just saw in another thread that indexed vectors are a pain and dependent sums (I guess that means subset types) are better.

I'm pretty much stuck with these because I'm using a library that is based upon them.

I can make the lemma type-check by using rewrites in terms like so:

```
Lemma coerce_n_plus_1:
forall (t:Type) (n:nat) (xs:vec t n) (x:t),
Cons x xs = rew (Nat.add_1_r n) in (app xs (Cons x Nil)).
```

But them I'm stuck in the proof with this `rew ...`

term.

```
Lemma coerce_n_plus_1:
forall (t:Type) (n:nat) (xs:vec t n) (x:t),
Cons x xs = rew (Nat.add_1_r n) in (app xs (Cons x Nil)).
Proof.
move => t n //=.
case => //=.
- move => x //=.
```

gives me the following goal (state):

```
t : Type
n : nat
x : t
============================
Cons x Nil = rew [vec t] Nat.add_1_r 0 in Cons x Nil
```

In this goal the `rew ...`

part is actually not needed anymore.

But how do I "get rid of it"?

Had `Nat.add_1_r`

(and all lemmas it depends upon) been transparent, `Nat.add_1_r 0`

would reduce to `eq_refl`

and your transport would vanish. Now, you can still destruct that equality and it will work

It can sometimes be useful to work with a more “gradual” version of equality when you want things to compute more smoothly. Here I give a version of equality specific to the natural numbers, following the pattern of its constructors, that allows `cast_vec`

to compute a little bit each time it sees a constructor – rather than all-at-once, as required when working with Martin-Löf equality `eq`

.

```
Require Import ssreflect.
From Equations Require Import Equations.
Set Equations Transparent.
Inductive eq_nat : nat -> nat -> Type :=
| eq_O : eq_nat O O
| eq_S {m n} : eq_nat m n -> eq_nat (S m) (S n)
.
Inductive vec t : nat -> Type :=
| Nil: vec t 0
| Cons: forall n, t -> vec t n -> vec t (S n).
Arguments Nil {t}%type_scope.
Arguments Cons {t n}%type_scope _ _.
Fixpoint app {t n1 n2} (l1:vec t n1) (l2:vec t n2) : vec t (n1 + n2) :=
match l1 in (vec _ n1) return (vec t (n1+n2)) with
| Nil => l2
| Cons x xs => Cons x (app xs l2)
end.
Equations cast_vec {t m n} (q : eq_nat m n) (xs : vec t m) : vec t n :=
| eq_O, Nil => Nil
| eq_S q, Cons x xs => Cons x (cast_vec q xs).
Definition add_1_r' m : eq_nat (m + 1) (S m).
Proof.
induction m; repeat constructor; assumption.
Defined.
Lemma coerce_n_plus_1:
forall (t:Type) (n:nat) (xs:vec t n) (x:t),
Cons x xs = cast_vec (add_1_r' n) (app xs (Cons x Nil)).
Proof.
move => t n.
case.
- move => x //=.
- admit.
Admitted.
```

Yann Leray schrieb:

Had

`Nat.add_1_r`

(and all lemmas it depends upon) been transparent,`Nat.add_1_r 0`

would reduce to`eq_refl`

and your transport would vanish. Now, you can still destruct that equality and it will work

Thanks a lot for the advice.

I'm not sure though which equality you are actually referring to.

`case (Nat.add_1_r 0)`

fails though:

```
Error: Abstracting over the terms "1" and "e0" leads to a term fun (a : nat) (e1 : 0 + a = a) => Cons x Nil = rew [vec t] e1 in Cons x Nil
which is ill-typed.
Reason is: Illegal application:
The term "eq_rect" of type "forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, x = y -> P y"
cannot be applied to the terms
"nat" : "Set"
"a" : "nat"
"vec t" : "nat -> Type"
"Cons x Nil" : "vec t 1"
"a" : "nat"
"e1" : "0 + a = a"
The 4th term has type "vec t 1" which should be coercible to "vec t a".
```

@James Wood

That is also a very interesting approach. Thanks a lot!

I will certainly give that a try.

You should at least try with destruct, not case, but such dependent-type errors are often a barrier

Otoh, it should be possible to rewrite Nat.add_1_r 0 to eq_refl by Hedberg's theorem (I forget what the stdlib calls it)

It is called `UIP`

. More precisely, in this case, it is `(UIP_refl_nat _ (Nat.add_1_r 0))`

.

@Paolo Giarrusso , `destruct`

gave me the same error message.

But `move => x; rewrite (UIP_refl_nat _ (Nat.add_1_r 0)) //=.`

really does finish the goal.

Thanks a lot for this hint, @Paolo Giarrusso and @Guillaume Melquiond .

Sebastian Ertel has marked this topic as resolved.

Last updated: Jun 16 2024 at 01:42 UTC