not exactly coq quetion but technique qeustion:

```
Inductive vec T : nat -> Type :=
| vnil: vec T 0
| vcons (a: T) (n: nat) (v: vec T n): vec T (S n).
Definition vtail T (n: nat) (v: vec T (S n)): vec T n.
:=
@vec_rect T
(fun l v => match l with | 0 => False | S n' => vec T n end) (*can be easily done without match *)
_ (* I need a proof of false here *)
_ (* it is almost match ... and case analysis but I cannot use match or case analysis *)
(S n) v.
```

I am not sure what should I be filling in he holes

the second argument of vec_rect should use True not False, and `vec T n'`

not `vec T n`

then the first hole needs a proof of True (easy)

and the second hole should also be easy

the `n`

and `n'`

is a typo... and it is obvious why, but I cannot see the intuition behind `True`

part

isn't what we are saying that this case is unreachable ?

The function was trivial once I replaced false with true, but I cannot see the intuition:

```
Definition vtail T (n: nat) (v: vec T (S n)) : vec T n :=
@vec_rect T
(fun l v => @nat_rect (fun _ => Type) True (fun l' _ => vec T l') l)
I
(fun _ n v _ => v) (S n) v.
```

the case isn't really unreachable, rather we are defining a generalized tail function

```
@vec_rect T
(fun l v => @nat_rect (fun _ => Type) True (fun l' _ => vec T l') l)
I
(fun _ n v _ => v)
```

then using it for the specific case of `S n`

this generalized tail returns the tail for nonzero n, and nothing of interest (True / unit) for 0

I have a follow up question with different example:

```
Definition vlast T (n: nat) (v: vec T (S n)) : T:=
@vec_rect T
(fun l v => @nat_rect (fun _ => Type) True (fun _ _ => T) l)
I
(fun a' n' v' IH => @vec_rect T (fun l v => T) a' (fun a'' n'' b'' IH' => IH (*problem here*)) n' v')
(S n) v.
```

The term `IH`

has type `nat_rect (fun=> Type) True (fun=> (fun=> T)) n'`

while it is expected to have type `T`

.

But then `nat_rect (fun=> Type) True (fun=> (fun=> T)) n'`

is actually `T`

because we are in the second branch of the nested recursor.

I assume this information does not just emerge out of no where, and this information must be passed around somewhere, perhaps in the motive? but I cannot come up with the right technique

A bit unrelated but just to be sure you didn't miss it: as you can see, vector is famous for being very painful to use https://github.com/coq/coq/pull/18032 If you don't have a very good reason to use them, it's recommended to go for dependent pairs of lists and proof about their length.

I know it is tricky, that is precisely the point, I am stress testing my own inductive definition implementation, and for that I need indutive type with indices that keep changing. vector felt like good example.

The strategy is to do things in coq first then to make sure it works, then do it in my language.

I thought the good thing about vectors is that they don't need lots of infrastructure unlike other things which will require me to implement equality, and peano, that is restriction because as of now, I am building ast by hand, and don't want to build the whole peano in ast.

but I am open to other alternatives with indices that behave like real indices rather than parameters.

you want to say something like "in the `cons a' n' v'`

case, if v' is nil return a' otherwise recurse (which means use the induction hypothesis IH)"

using the induction hypothesis in the `cons _ _ (cons _ _ _)`

case needs us to update its type from n' to (S something), we use the convoy pattern for this

```
Definition vlast T (n: nat) (v: vec T (S n)) : T:=
let P := @nat_rect (fun _ => Type) True (fun _ _ => T) in
@vec_rect T
(fun l v => P l)
I
(fun a' n' v' IH => @vec_rect T (fun n'' _ => P n'' -> T) (fun _ => a') (fun _ _ _ _ IH' => IH') n' v' IH)
(S n) v.
```

the convoy pattern is where you do your match/foo_rect with the hypothesis you want to update in the predicate, here `fun n'' _ => P n'' -> T`

`IH'`

is the update `IH`

`fun _ => a'`

ignores the updated IH (with type annotation it is `fun _ : True => a'`

)

but I am open to other alternatives with indices that behave like real indices rather than parameters.

maybe worth working with equalities a bit

- prove transitivity, symmetry,
`transport : forall {A} (P:A -> Type) {a b}, a = b -> a -> b`

- prove non dependent congruence
`forall A B (f:A -> B) x y, x = y -> f x = f y`

- prove
`0 = 1 -> False`

- prove injectivity of a non dependent constructor eg
`forall n m, S n = S m -> n = m`

- prove
`forall n, n = S n -> False`

(hint: needs induction in nat) - prove dependent congruence
`forall A B (f:forall x:A, B x) (x y : A) (e:x = y), transport B e (f x) = f y`

- state and prove injectivity of dependent constructor (eg the constructor for
`sigT`

) - try and fail to prove
`forall A (x:A) (e:x = x), e = eq_refl`

(if you succeed, report a Coq bug) (the autogenerated`eq_ind`

isn't dependent enough to try to use here, instead use the`eq_ind_dep`

generated by`Scheme Induction for eq Sort Prop.`

)

Thanks alot, I didn't know the convoy's pattern trick! And thanks for the equality suggestions!

for fancy index wrangling while stll staying relatively simple there's hedberg's theorem

the following is a specialized proof for the case of singleton types:

```
Scheme Induction for eq Sort Prop.
Section S.
Variable A:Type.
Definition trans_sym_eq {x y:A} (e : x = y) : eq_trans (eq_sym e) e = eq_refl
:= eq_ind_dep A x (fun z e' => eq_trans (eq_sym e') e' = eq_refl)
eq_refl y e.
Variable x:A.
Hypothesis isHProp : forall y:A, x = y.
Definition left_inv_on y (e:x = y) : eq_trans (eq_sym (isHProp x)) (isHProp y) = e
:= eq_ind_dep A x (fun z e' => eq_trans (eq_sym (isHProp x)) (isHProp z) = e')
(trans_sym_eq (isHProp x)) y e.
Definition uip y (e1 e2:x = y) : e1 = e2
:= eq_trans (eq_sym (left_inv_on y e1)) (left_inv_on y e2).
End S.
```

you can try to understand it and how to generalize it to replace `isHProp`

with `eq_dec : forall y, x = y \/ not (x = y)`

(the generalized proof is in the stdlib called `Eqdep_dec.eq_proofs_unicity_on`

)

One can do this with dependent pattern matching but avoiding `eq_rect`

(ie type cast) like this:

```
Inductive vec T : nat -> Type :=
| vnil: vec T 0
| vcons (a: T) (n: nat) (v: vec T n): vec T (S n).
Definition is_nz n := match n with 0 => False | S _ => True end.
Definition dpred {n} : is_nz n -> nat :=
match n with
| 0 => fun C => match C with end
| S n => fun _ => n
end.
Definition vtail T n (v : vec T (S n)) : vec T n :=
match v in vec _ m return forall h : is_nz m, vec _ (dpred h) with
| vnil _ => fun C => match C with end
| vcons _ _ _ v => fun _ => v
end I.
```

One could also use the non-dependent `pred`

from the standard library in this case but in general, one needs a default value in excluded cases and using `match _ : False with end`

works in a more generic way.

Last updated: Jun 23 2024 at 04:03 UTC