## Stream: Coq users

### Topic: nth element on coquelicot Tn sequence

#### laka (Mar 12 2023 at 14:48):

Hey! I'm quite new to coq and I'm trying to write an accessor for specific values in a matrix using the Coquelicot library. From what I can gather from its definition, it's a 2D structure of Tn sequences (http://coquelicot.saclay.inria.fr/html/Coquelicot.Hierarchy.html#Tn). So to access a value from the matrix I'm first writing a helper to get the nth element from that sequence of type Tn. So I wrote a Fixpoint like this:

``````Fixpoint Tn_nth {dim: nat} (n: nat) (tn: Tn dim R) : option R :=
match n, tn with
| O, (x, _) => Some x
| S n', (_, s) => Tn_nth n' s
| _, _ => None
end
.
``````

However the first arm of the match gives me an error:

``````Error: In environment
Tn_nth : forall dim : nat, nat -> Tn dim R -> option R
dim : nat
n : nat
tn : Tn dim R
The term "tn" has type "Tn dim R" while it is expected to have type
"(?T * ?T0)%type".
``````

I don't quite understand what's going on here. The way I understand it Tn is a recursive sum type of either a unit type or a pair of a value and another Tn, much like how lists are defined. Why can't I match Tn against a pair? I looked at the library and it can construct Tn sequences from pairs just fine. What am I missing here?

#### Paolo Giarrusso (Mar 12 2023 at 15:20):

First of all — the function you want can be written in Coq (I'll post a version), but this will require Coq dependent pattern matching, which is often frustrating; many people will be happier using the Coq-equations plugin for this (which is included in the Coq platform).

Coq (like other statically typed languages) only let you `tn` match against a pair if `tn` has a pair type — otherwise the match (1) could be a bug (2) might not even be executable at runtime — values might not carry enough info to distinguish units from pairs (but I'm oversimplifying here _a lot_).

#### Paolo Giarrusso (Mar 12 2023 at 15:21):

It seems `coeff_Tn` is almost the function you want, but it's not quite flexible enough. Here is a variant:

``````Fixpoint coeff_Tn' {T} {n : nat} : (Tn n T) → nat → option T :=
match n with
| O => fun (_ : Tn O T) (_ : nat) => None
| S n' => fun (v : Tn (S n') T) (i : nat) => match i with
| O => Some (fst v)
| S i => coeff_Tn' (snd v) i
end
end.
``````

however, this is somewhat subtle...

#### Paolo Giarrusso (Mar 12 2023 at 15:24):

once you match `n` against `S n'`, you _can_ match `v : T (S n')` against a pair — for instance this works:

``````Fixpoint coeff_Tn' {T} {n : nat} : (Tn n T) → nat → option T :=
match n with
| O => fun (_ : Tn O T) (_ : nat) => None
| S n' => fun (v : Tn (S n') T) (i : nat) => match v, i with
| (a, b), O => Some a
| (a, b), S i => coeff_Tn' b i
end
end.
``````

#### Paolo Giarrusso (Mar 12 2023 at 15:33):

OTOH, both versions are a bit convoluted and one might try to write the _following_ version — which does not work in Coq, but does work when translated to Coq-Equations (below):

``````Fixpoint coeff_Tn' {T} {n : nat} (v : Tn n T) (i : nat) : option T :=
match n, i with
| O, _ => None
| S n', O => Some (fst v)
| S n' , S i => coeff_Tn' (snd v) i
end.
(*
Error: In environment
coeff_Tn' : ∀ (T : Type) (n : nat), Tn n T → nat → option T
T : Type
n : nat
v : Tn n T
i : nat
n' : nat
The term "v" has type "Tn n T" while it is expected to have type "(?A0 * ?B)%type".
*)

From Equations Require Import Equations.

Equations coeff_Tn {T} {n : nat} (v : Tn n T) (i : nat) : option T :=
@coeff_Tn _ O v i := None;
@coeff_Tn _ (S n') v O := Some (fst v);
@coeff_Tn _ (S n') v (S i) := coeff_Tn (snd v) i.
(* works! — see equations manual/tutorials to learn how to reason about it *)
``````

#### Paolo Giarrusso (Mar 12 2023 at 15:42):

the _rule_ why Coq demands `coeff_Tn'` to be written in that style is short to state but tricky to understand, and is typically considered an advanced topic; and Equations is often more convenient even if you've learned it. You can google the "convoy pattern" or try this summary:

• Matching on `n` only "updates" the current _return type_, but not types of variables in the _typing context_ — and let me explain on these examples.
• So, in `Fixpoint coeff_Tn' {T} {n : nat} : (Tn n T) → nat → option T :=`, when we match `n` against `S n'`, then `Tn n T` becomes `Tn (S n') T` which is a pair.
• Instead, in `Fixpoint coeff_Tn' {T} {n : nat} (v : Tn n T) (i : nat) : option T :=`, when we again match `n` against `S n'`, the return type is just `option T` and stays unchanged; we still have an argument `v : Tn n T`, but this is already outside the return type! `v` was introduced into the context, and the types in the context are not updated.

#### Pierre Roux (Mar 12 2023 at 15:54):

Side note: as you discovered this kind of dependent types can be difficult to work with. If you are only interested in matrices, the mathcomp library offers a formalization that is more convenient: https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/matrix.v

Last updated: Oct 04 2023 at 19:01 UTC