## Stream: Coq users

### Topic: Implicit coercions for length-indexed list

#### Sebastian Ertel (May 15 2023 at 19:51):

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.
``````

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

Any help would be greatly appreciated.

Thanks,
Sebastian.

#### Paolo Giarrusso (May 16 2023 at 12:03):

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:

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

#### Sebastian Ertel (May 16 2023 at 12:58):

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.

#### Sebastian Ertel (May 16 2023 at 13:09):

``````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"?

#### Yann Leray (May 16 2023 at 13:44):

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

#### James Wood (May 16 2023 at 13:58):

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 //=.
``````

#### Sebastian Ertel (May 16 2023 at 14:27):

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".
``````

#### Sebastian Ertel (May 16 2023 at 14:33):

@James Wood
That is also a very interesting approach. Thanks a lot!
I will certainly give that a try.

#### Paolo Giarrusso (May 16 2023 at 17:38):

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

#### Paolo Giarrusso (May 16 2023 at 17:41):

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)

#### Guillaume Melquiond (May 16 2023 at 17:50):

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

Last updated: Oct 04 2023 at 23:01 UTC