Stream: Coq users

Topic: nth element on coquelicot Tn sequence


view this post on Zulip 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?

view this post on Zulip 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_).

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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 *)

view this post on Zulip 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:

view this post on Zulip 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: Jun 20 2024 at 11:02 UTC