1

我已经在 Coq 中编写了一些项目，但我之前没有使用过 ssreflect 并且我遇到了麻烦。

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

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

我选择使用序数而不是 nat，因为否则我必须有一个单独的字段来证明它们在范围内，否则我必须在其他属性的声明中考虑这种情况。但是序数使我的一切都变得非常困难。

花了一天左右的时间，我才发现我可以用它们来构建它们，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，但我不能。

4

1 回答 1

2

您可以使用以下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比原始元组更适合表示函数。

于 2020-09-29T21:16:32.733 回答