nth element on coquelicot Tn sequence · Coq users

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: Apr 20 2024 at 12:02 UTC

Stream: Coq users