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.

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.

And then you can defer the proof of the second projection to a later time.

Your definition is completely fine by the way. You can even peak at it using `Print`

to see what the underlying term looks like.

Read more about program here: https://coq.inria.fr/refman/addendum/program.html

Thank you so much, I am learning a lot an I am grateful for your assistance.

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.

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

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.

@walker replace `vec A (n + 1)`

with `vec A (1 + n)`

(or `vec A (S n)`

) and things should work better.

I mean, in the type of `vec_hd`

.

Oh right I can see the problem now 1 + n is easy without induction! that stuff can easily get tricky without noticing,

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.

the rule of thumb is that `n + 1`

is a bug

re "no default", again you want `Program`

, but let me write it up...

Paolo Giarrusso said:

the rule of thumb is that

`n + 1`

is a bug

I am learning (:

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.

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

the proof you pass to `False_rect`

is hidden from clients, but they won't care.

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`

(`proj1_sig`

is printed as a backtick but that's hard to type here)

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.

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: Feb 06 2023 at 12:04 UTC