nats元组的字典序比较

Question

我正在处理 nat 的元组（特别是三元组，nat*nat*nat），并且想要一种按字典顺序比较元组的方法。与此等效的东西：

Inductive lt3 : nat*nat*nat -> nat*nat*nat -> Prop :=
| lt3_1 : forall n1 n2 n3 m1 m2 m3, n1 < m1 -> lt3 (n1,n2,n3) (m1,m2,m3)
| lt3_2 : forall n1 n2 n3    m2 m3, n2 < m2 -> lt3 (n1,n2,n3) (n1,m2,m3)
| lt3_3 : forall n1 n2 n3       m3, n3 < m3 -> lt3 (n1,n2,n3) (n1,n2,m3).

我想要证明传递性和有根据性等基本属性。标准库中是否有可以完成大部分工作的东西？如果不是，我最感兴趣的是有根据的。我将如何证明它？

Answer 1

标准库有其自身的 definition of lexicographic product, along with a proof 基础。然而，该定义的问题在于它是针对依赖对声明的：

lexprod : forall (A : Type) (B : A -> Type), relation {x : A & B x}

如果需要，您可以使用 fun _ => B' 形式的常量类型族实例化 B，因为类型 A * B' 和 {x : A & B'} 是同构的。但是如果你想直接使用 Coq 类型的正则对，你可以简单地复制一个更受限版本的词典产品的证明。证明不是很复杂，但它需要对定义有根据性的可访问性谓词进行嵌套归纳。

Require Import
  Coq.Relations.Relation_Definitions
  Coq.Relations.Relation_Operators.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Lexicographic.

Variables (A B : Type) (leA : relation A) (leB : relation B).

Inductive lexprod : A * B -> A * B -> Prop :=
| left_lex  : forall x x' y y', leA x x' -> lexprod (x, y) (x', y')
| right_lex : forall x y y',    leB y y' -> lexprod (x, y) (x, y').

Theorem wf_trans :
  transitive _ leA ->
  transitive _ leB ->
  transitive _ lexprod.
Proof.
intros tA tB [x1 y1] [x2 y2] [x3 y3] H.
inversion H; subst; clear H.
- intros H.
  inversion H; subst; clear H; apply left_lex; now eauto.
- intros H.
  inversion H; subst; clear H.
  + now apply left_lex.
  + now apply right_lex; eauto.
Qed.

Theorem wf_lexprod :
  well_founded leA ->
  well_founded leB ->
  well_founded lexprod.
Proof.
intros wfA wfB [x].
induction (wfA x) as [x _ IHx]; clear wfA.
intros y.
induction (wfB y) as [y _ IHy]; clear wfB.
constructor.
intros [x' y'] H.
now inversion H; subst; clear H; eauto.
Qed.

End Lexicographic.

然后您可以实例化这个通用版本来恢复，例如，您对自然数三元组的词典积的定义：

Require Import Coq.Arith.Wf_nat.

Definition myrel : relation (nat * nat * nat) :=
  lexprod (lexprod lt lt) lt.

Lemma wf_myrel : well_founded myrel.
Proof. repeat apply wf_lexprod; apply lt_wf. Qed.

nats元组的字典序比较

Lexicographical comparison of tuples of nats

coq