Stream: Coq users

Topic: Last element of a vector


view this post on Zulip Julin Shaji (Sep 30 2023 at 05:38):

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?

view this post on Zulip Quentin VERMANDE (Sep 30 2023 at 06:00):

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