How to index a tuple with ssreflect ordinals

Question

I have written a few projects in Coq but I haven't used ssreflect before and I'm having trouble with it.

I have a data structure with indices into itself. Below is the simplified version.

Record Graph :=
  { size: nat
  ; nodes : size.-tuple (seq 'I_size)
    ...
  }.

I chose to use ordinals instead of nats because otherwise I would have to have a separate field for a proof that they are in range or I'd have to take that case into account in the statement of other properties. But the ordinals are making everything very hard for me.

It took a day or so until I found that I can construct them with inord instead of making countless x < n lemmas.

With the lemmas I was at least able to get to the point where my problem was that I couldn't prove that forall i : 1 < 2, Ordinal i = Ordinal lt_1_2.

Using inord I can't figure out a way to evaluate tnth further after unfolding it. I didn't find any helpful lemmas either.

Am I using ordinals for the wrong purpose? If not, how should I be using them?

Minimized example

There is no MRE because this is about what I should be doing. I've tried various things and ordinals seemed like a good solution before the (minimized) attempt below.

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq tuple fintype.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Record Graph :=
  { size: nat
  ; nodes : size.-tuple 'I_size
  ; pair n := tnth nodes n
  ; pair_sym : forall x, pair (pair x) = x
  }.

Definition net : Graph.
refine {|
  nodes := [tuple inord 1; inord 0];
  pair_sym := _
|}.
case.
case.
unfold tnth. simpl. intro.

I don't know how to continue from here. I think that I should be able to fully evaluate tnth but I can't.

Answer 1

You can use the val_inj lemma from eqtype:

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq tuple fintype.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Record Graph :=
  { size: nat
  ; nodes : size.-tuple 'I_size
  ; pair n := tnth nodes n
  ; pair_sym : forall x, pair (pair x) = x
  }.

Definition net : Graph.
refine {|
  nodes := [tuple inord 1; inord 0];
  pair_sym := _
|}.
rewrite /tnth.
case.
case=> [|[|//]] iP /=; rewrite inordK //=;
by apply: val_inj; rewrite /= inordK.
Qed.

Side comment: you might prefer to use finite functions (cf. the finfun library) to represent nodes. They are better for representing functions 'I_size -> 'I_size than raw tuples.