Stream: Coq users

Topic: ✔ Append of two length-indexed vectors does not type-check

Sebastian Ertel (Sep 20 2022 at 15:14):

Hi there!

I'm trying to define the following lemma:

Lemma msb_n : forall {sz:nat} (width:nat) (n : (vect bool sz)),
    ( n >=?sb (vect_app (vect_const (sz - width) false) (vect_const width true)) ) = true ->
    vect_slice sz width n = vect_const width true.

But Coq cannot unify:

Error:
In environment
sz : nat
width : nat
n : bits sz
The term "(vect_app (vect_const (sz - width) false) (vect_const width true))%vect" has type "vect bool (sz - width + width)"
while it is expected to have type "vect bool sz".

How come?
What can I do to help Coq here?

Just for completeness:

Check vect_app.

vect_app
     : vect ?T ?sz1 -> vect ?T ?sz2 -> vect ?T (?sz1 + ?sz2)
where
?T : [ |- Type]
?sz1 : [ |- nat]
?sz2 : [ |- nat]

Check vect_const.

vect_const
     : forall sz : nat, ?T -> vect ?T sz
where
?T : [ |- Type]

Gaëtan Gilbert (Sep 20 2022 at 15:23):

• in general length-indexed vectors are a pain to work with
• if you had a proof eq : sz - width + width = sz then you could do rew eq in vect_app ... (https://github.com/coq/coq/blob/d9180a0774afd0f17d26c4828c8ee2c316a0571b/theories/Init/Logic.v#L476) to get it at the right type
• however when sz < width, sz - width = 0 so sz - width + width = width not sz and this is just not possible

Sebastian Ertel (Sep 20 2022 at 18:57):

@Gaëtan Gilbert thanks for your comments and especially for the hint with the rewrite notation (EqNotations)!
That in the end did work but I used Nat.sub_add which in the end it the eq proof that you proposed.

Notification Bot (Sep 20 2022 at 18:58):

Sebastian Ertel has marked this topic as resolved.

Last updated: Oct 01 2023 at 18:01 UTC