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

- 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

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

Sebastian Ertel has marked this topic as resolved.

Last updated: Jan 28 2023 at 06:30 UTC