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.
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.
I match both n
and l
and give them an alternative name (k
and m
).
Is this really needed in such a match
?
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.
There are multiple kinds of approaches to this problem:
to call abstract lia
, you can write in a term ltac:(abstract lia)
and it should usually work, up to bugs in abstract
.
for this kind of approach, this is more or less the expected verbosity and complexity.
putting abstract in ltac:()
is useless
interesting :-(
then I think refine
tactic could achieve something similar, without using Program
?
What is a prettier approach than the convoy pattern?
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.
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…
but the resulting generated term is visible to clients, unless you jump through extra hoops, so proofs about this are hard.
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.
From what I understand: the cleanest solution would be just using Equations?
yes, IMHO
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.
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
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
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