如何使用ssreflect序号对元组进行索引

Question

我用Coq写了几个项目，但我以前没有用过ssreflect，我在使用它时遇到了麻烦。

我有一个带有索引的数据结构。下面是简化版。

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

我选择使用序数而不是nats，因为否则我必须有一个单独的字段来证明它们在范围内，或者我必须在其他属性的语句中考虑这种情况。但是序数对我来说是非常困难的。

我花了一天左右的时间才发现，我可以用inord来构建它们，而不是创建无数的x < n引理。

有了这些引理，我至少能够达到我的问题所在，那就是我不能证明forall i : 1 < 2, Ordinal i = Ordinal lt_1_2。

使用inord时，我想不出在展开tnth之后如何进一步评估它。我也没有找到任何有用的引理。

我把序数用在错误的地方了吗？如果不是，我应该如何使用它们？

最小化示例

没有MRE，因为这是关于我应该做的事情。我已经尝试了各种方法，在下面的(最小化)尝试之前，序数似乎是一个很好的解决方案。

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.

我不知道如何从这里继续。我认为我应该能够充分评估tnth，但我不能。

Answer 1

您可以使用eqtype中的val_inj引理

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.

附注:您可能更喜欢使用有限函数(参见finfun库)来表示节点。它们比原始元组更适合表示函数元组( 'I_size -> 'I_size )。