Implicit coercions for length-indexed list · Coq users

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.

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.

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.

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.

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 Coercions 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:

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.

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

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

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 //=.
  - admit.
Admitted.

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

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

Stream: Coq users

Topic: Implicit coercions for length-indexed list

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