## Stream: Coq users

### Topic: tail of vector using recursion

#### walker (Jan 10 2024 at 22:00):

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

#### Gaëtan Gilbert (Jan 10 2024 at 22:15):

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

#### walker (Jan 10 2024 at 22:17):

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

#### walker (Jan 10 2024 at 22:18):

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

#### walker (Jan 10 2024 at 22:24):

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.
``````

#### Gaëtan Gilbert (Jan 10 2024 at 22:34):

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

#### walker (Jan 11 2024 at 10:24):

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.
``````

#### walker (Jan 11 2024 at 10:25):

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.

#### walker (Jan 11 2024 at 10:26):

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

#### Pierre Roux (Jan 11 2024 at 10:30):

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.

#### walker (Jan 11 2024 at 10:33):

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.

#### walker (Jan 11 2024 at 10:35):

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.

#### walker (Jan 11 2024 at 10:35):

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

#### Gaëtan Gilbert (Jan 11 2024 at 10:41):

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'`)

#### Gaëtan Gilbert (Jan 11 2024 at 10:50):

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.`)

#### walker (Jan 11 2024 at 10:55):

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

#### Gaëtan Gilbert (Jan 11 2024 at 11:17):

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`)

#### Dominique Larchey-Wendling (Jan 18 2024 at 14:01):

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