如何使用 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

您可以使用 val_inj 来自 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.

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

如何使用 ssreflect 序号索引元组

How to index a tuple with ssreflect ordinals

coq

ssreflect

最小化示例