Stream: Coq users

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

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

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 ?T ?sz1 -> vect ?T ?sz2 -> vect ?T (?sz1 + ?sz2)
?T : [ |- Type]
?sz1 : [ |- nat]
?sz2 : [ |- nat]

Check vect_const.

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

view this post on Zulip Gaëtan Gilbert (Sep 20 2022 at 15:23):

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

view this post on Zulip Notification Bot (Sep 20 2022 at 18:58):

Sebastian Ertel has marked this topic as resolved.

Last updated: Jan 28 2023 at 06:30 UTC