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?

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

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

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

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

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.

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