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

Paolo Giarrusso (Oct 22 2021 at 18:35):

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?

Paolo Giarrusso (Oct 22 2021 at 18:40):

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: Oct 03 2023 at 04:02 UTC