Stream: Coq users

Topic: ✔ Implicit coercions for length-indexed list


view this post on Zulip 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.
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.

view this post on Zulip 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:

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.

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)).

view this post on Zulip Sebastian Ertel (May 16 2023 at 18:49):

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

view this post on Zulip Notification Bot (May 16 2023 at 18:50):

Sebastian Ertel has marked this topic as resolved.


Last updated: Jun 16 2024 at 01:42 UTC