walker (Apr 12 2022 at 20:58): walker (Apr 12 2022 at 20:58):This is follow up on previous question:
I learned here that this is the best way to do vectors in coq:
Definition vec A n := { xs : list A | length xs = n }.
Then I tried writing some basic functions for this new vector like:
Definition concat {A: Type} {n m: nat} (v1: vec A n) (v2: vec A m) : vec A (n + m).
Proof.
destruct v1 as [l1 H1], v2 as [l2 H2]; subst.
exists (l1 ++ l2).
apply app_length.
Defined.
and the question I am having here are basically few things:
A- if this is superior implementation why is not part of standard library of coq instead of the current one
B- I am asking for code review for my concat function. It seams like abusing coq, and this doesn't seam like the right way to do it, so maybe someone can point out if I did something wrong here (the coq way of doing the implementation). P.S I struggled to write normal functions but then I find it hard to see what this function is doing by looking at the implementation.
Ali Caglayan (Apr 12 2022 at 21:09):Another advantage of using a sigma type here is that you can take advantage of Coq's Program vernacular:
Program Definition concat' {A n m}
(v1 : vec A n) (v2 : vec A m) : vec A (n + m) := v1 ++ v2.
Next Obligation.
Proof.
destruct v1, v2; cbn.
rewrite app_length.
f_equal; trivial.
Qed.
This lets you add together elements of the sigma type as if you were really talking about their first projections.
Ali Caglayan (Apr 12 2022 at 21:10):And then you can defer the proof of the second projection to a later time.
Ali Caglayan (Apr 12 2022 at 21:10):Your definition is completely fine by the way. You can even peak at it using Print to see what the underlying term looks like.
Ali Caglayan (Apr 12 2022 at 21:11):Read more about program here: https://coq.inria.fr/refman/addendum/program.html
walker (Apr 12 2022 at 21:35):Thank you so much, I am learning a lot an I am grateful for your assistance.
Li-yao (Apr 12 2022 at 21:56):A- if this is superior implementation why is not part of standard library of coq instead of the current one
I wouldn't say one way is invariably better than the other. There are many styles of dependently typed programming with their own preferences. The old Vector.t allows many operations to be defined naturally without a single explicit proof, because the implementation actually encodes the proof. But it does require more care to rely minimally on propositional equality.
The standard library is an old thing. For something that everybody in the community depends on, the incentive to remove or change things is rather low. If there really is a need, it's easy to create a new package.
walker (Apr 12 2022 at 23:18):Alright, this is a small follow up with I cannot figure out let alone solve:
Definition vec_hd {A: Type} {n: nat}(v: vec A (n + 1)) : A.
Proof.
destruct v as [l H].
destruct l as [| a l].
- simpl in H. lia.
- apply a.
Defined.
Example vec_hd_example: @vec_hd nat 2 ([1;2;3] ↾ eq_refl) = 1.
Proof.
reflexivity.
Qed.
Fail Example vec_hd_example_failed: vec_hd ([1;2;3] ↾ eq_refl) = 1.
I always knew that type inference will be pain. But why cannot coq see that for vec_hd, length v = 3 then n must equal 2
Paolo Giarrusso (Apr 12 2022 at 23:20):Ali Caglayan said:
Your definition is completely fine by the way. You can even peak at it using
It's a matter of style, but some (including me) recommend avoiding tactics for proof-relevant terms; I've seen coding styles recommend sticking to "predictable" tactics, but that's trickier to explain (okay, exists is fine, but in general it's more complex).
Rationale: Clients writing proofs about concat' will reason about the underlying list (and not really about the equality proof), so they'll depend on the exact body, and the easiest way to keep it fixed is to use write it by hand.
Paolo Giarrusso (Apr 12 2022 at 23:21):@walker replace vec A (n + 1) with vec A (1 + n) (or vec A (S n)) and things should work better.
Paolo Giarrusso (Apr 12 2022 at 23:21):I mean, in the type of vec_hd.
walker (Apr 12 2022 at 23:21):Oh right I can see the problem now 1 + n is easy without induction! that stuff can easily get tricky without noticing,
walker (Apr 12 2022 at 23:22):It's a matter of style, but some (including me) recommend avoiding tactics for proof-relevant terms; I've seen coding styles recommend sticking to "predictable" tactics, but that's trickier to explain (okay, exists is fine, but in general it's more complex).
I also had the same feeling but I find it hard to do sometimes as when dealing with the vec_hd function. I don't know how to convince coq that we don't need a default.
Paolo Giarrusso (Apr 12 2022 at 23:22):the rule of thumb is that n + 1 is a bug
Paolo Giarrusso (Apr 12 2022 at 23:23):re "no default", again you want Program, but let me write it up...
walker (Apr 12 2022 at 23:23):Paolo Giarrusso said:
the rule of thumb is that
n + 1is a bug
I am learning (:
walker (Apr 12 2022 at 23:26):That is what I tried with program
Program Definition vec_hd {A: Type} {n: nat}(v: vec A (1+ n)) : A := hd (*don't know what goes here*) `v.
and I know that we cannot have a defautl variable for arbitrary type A. so I gave up.
Paolo Giarrusso (Apr 12 2022 at 23:28):So what about
Set Program Cases. (* This is often the default*)
Program Definition vec_hd {A : Type} {n : nat} (v : vec A (S n)) : A :=
match proj1_sig v with
| [] => False_rect _ _
| x :: xs => x
end.
Next Obligation.
simpl; intros ?? v ?; destruct v; simpl in *; subst; simpl in *. lia.
Qed.
where False_rect : ∀ P : Type, False → P can produce an arbitrary P, given a proof of contradiction
Paolo Giarrusso (Apr 12 2022 at 23:30):the proof you pass to False_rect is hidden from clients, but they won't care.
Paolo Giarrusso (Apr 12 2022 at 23:30):crucially, with Set Program Cases, the obligation will be:
∀ (A : Type) (n : nat) (v : vec A (S n)), let filtered_var := proj1_sig v in [] = filtered_var → False
Paolo Giarrusso (Apr 12 2022 at 23:31):(proj1_sig is printed as a backtick but that's hard to type here)
Paolo Giarrusso (Apr 12 2022 at 23:32):the point is that with Set Program Cases, match v behaves not like destruct v (as usual) but like destruct v eqn:? — it remembers which was the case.
walker (Apr 12 2022 at 23:35):I will have to keep staring at it till It feels natural :) I am also trying the rest of lists from coq here and I hope by the end of it it will be natural to do things this way.
Last updated: Oct 08 2024 at 14:01 UTC