I was trying to make a function that would return the last element of a bit vector.

So I tried this:

```
Definition isLsbSet {n:nat} (v: Bvector n): bool.
Proof.
refine (
match n with
| O => false (* There is no LSB *)
| S n' => nth_order v (_:n'<n)
end).
```

Now the proof state is just:

```
n : nat
v : Bvector n
n' : nat
============================
n' < n
```

I couldn't bring about the `n = S n'`

relation to the hypotheses section.

Any idea how that can be done?

Coq a priori does note link n and n'. You can write your match as "match n as m return m = n -> bool with", turn all you cases into functions of type _ = n -> bool and add a term of type (n = n) after the end (as a matter of fact, here, m <= n instead of m = n yields a shorter proof)

Last updated: Jun 23 2024 at 04:03 UTC