## Stream: Coq users

### Topic: nth element in a vector

#### Proof By Sledgehammer (Oct 22 2021 at 18:14):

I am currently trying to implement my own (Byte-)Vectors and just implemented the `nth` element operation.
However, I feel like my solution is far from readable, so I am wondering if there exists a nicer solution for this.

1. I first match over the element index `n`, then over the vector length `l` to make sure `l` is not zero.
I feel like this second match should not be needed, but I don't know how to get rid of it.

2. I match both `n` and `l` and give them an alternative name (`k` and `m`).
Is this really needed in such a `match`?

3. I apply `eq_rect` to cast the vector to the correct type. Is there a way for Coq to do that automatically?

``````  Program Fixpoint nth_byte `{l : nat} (v : ByteVec \$ S l) (n : nat) (H : n < S l) : Byte :=
match n as k return k = n -> n < S l -> Byte with
| 0    => fun _ _ => hd v
| S n' => fun Hk H =>
match l as m return l = m -> Byte with
| 0 => fun _ => False_rect Byte _
| S l' => fun Hm => let v' : ByteVec \$ S (S l') := eq_rect _ _ v _ _ in
@nth_byte l' (tl v') n' _
end _
end _ H.
Solve Obligations with abstract lia.
``````

#### Paolo Giarrusso (Oct 22 2021 at 18:32):

There are multiple kinds of approaches to this problem:

1. What you're doing looks mostly like it could be written without Program: you're writing manual dependent pattern matches, using the convoy pattern, etc.

#### Paolo Giarrusso (Oct 22 2021 at 18:34):

to call `abstract lia`, you can write in a term `ltac:(abstract lia)` and it should usually work, up to bugs in `abstract`.

#### Paolo Giarrusso (Oct 22 2021 at 18:34):

for this kind of approach, this is more or less the expected verbosity and complexity.

#### Gaëtan Gilbert (Oct 22 2021 at 18:35):

putting abstract in `ltac:()` is useless

interesting :-(

#### Paolo Giarrusso (Oct 22 2021 at 18:36):

then I think `refine` tactic could achieve something similar, without using `Program`?

#### Proof By Sledgehammer (Oct 22 2021 at 18:36):

What is a prettier approach than the convoy pattern?

#### Paolo Giarrusso (Oct 22 2021 at 18:37):

option 2 is relying on `Program`’s handling of matches (not sure it’d work here, and has issues), and option 3 is moving to Equations altogether.

#### Paolo Giarrusso (Oct 22 2021 at 18:38):

re 2, if you use `Program` and omit `as` and `return` annotations from a match, `Program` will do something similar to the convoy pattern on its own…

#### Paolo Giarrusso (Oct 22 2021 at 18:38):

but the resulting generated term is visible to clients, unless you jump through extra hoops, so proofs about this are hard.

#### Paolo Giarrusso (Oct 22 2021 at 18:39):

using Equations handles most of those issues automatically, and hides the needed translation from clients by sealing the entire definition and only exposing the defining equations.

#### Proof By Sledgehammer (Oct 22 2021 at 18:39):

From what I understand: the cleanest solution would be just using Equations?

yes, IMHO

#### Proof By Sledgehammer (Oct 22 2021 at 18:41):

I see. I was hoping there was also a nice solution in plain Coq, but I see how Equations can make my life easier. Thanks.

#### Gaëtan Gilbert (Oct 22 2021 at 18:43):

instead of convoying equalities you can convoy the vector itself
something like

``````Fixpoint nth_byte {l : nat} (n : nat)
: n < S l -> ByteVec (S l) -> Byte :=
match n with
| 0    => fun _ v => hd v
| S n' =>
match l with
| 0 => fun H _ => False_rect Byte _ (* obligation H : S n' < S 0 |- False *)
| S l' => fun H v => @nth_byte l' (tl v) n' _ (* obligation H : S n' < S l' |- n' < l' *)
end
end.
``````

(also the backquote in ` `{l : nat} ` does nothing)
might need some `return` annotations but I think Coq can figure them out

#### Proof By Sledgehammer (Oct 22 2021 at 18:51):

Awesome, this is already much better.

(also the backquote in `{l : nat} does nothing)

Where can I read when exactly a backquote does something? I always assumed : If I really want the argument to be implicit, I need a backtick

#### Gaëtan Gilbert (Oct 22 2021 at 18:53):

no
the backtick is about generalization, ie adding binders for unbound names

``````Generalizable All Variables.

Fail Check forall {x:foo}, x = x.
(* error foo unbound *)

Check forall `{x:foo}, x = x.
(* forall foo (x:foo), x = x *)

Check forall `{x}, x = x.
(* forall x, x -> x = x *)
(* equivalent to *)
Check forall `{_:x}, x = x.
``````

Last updated: Jun 15 2024 at 05:01 UTC