nat元组的词典比较 [英] Lexicographical comparison of tuples of nats
问题描述
我正在使用 nat
s元组(特别是三元组, nat * nat * nat
),并且会就像在字典上比较元组的方法一样。与此等效的东西:
I'm working with tuples of nat
s (specifically triples, nat*nat*nat
) and would like a way to lexicographically compare tuples. Something equivalent to this:
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).
我想证明一些基本特性,例如传递性和有根据的。标准库中是否有可以完成大部分工作的内容?如果没有,我对有根据的最感兴趣。我该如何证明呢?
I would like to have proofs of basic properties such as transitivity and well-foundedness. Are there things in the standard library that do most of the work? If not, I'm most interested in well-foundedness. How would I go about proving it?
推荐答案
标准库有自己的定义以及证明有充分根据的。但是,该定义的问题在于它是为相关对声明的:
The standard library has its own definition of lexicographic product, along with a proof of well-foundedness. The problem with that definition, however, is that it is stated for dependent pairs:
lexprod : forall (A : Type) (B : A -> Type), relation {x : A & B x}
如果需要,可以实例化 B
的常量类型族形式为 fun _ => B’
,因为类型 A * B’
和 {x:A& B’}
是同构的。但是,如果您想直接使用Coq类型的常规对,则可以简单地将证明复制为词典产品的更受限版本。证明不是很复杂,但是它需要对定义有充分根据的可访问性谓词进行嵌套归纳。
If you want, you can instantiate B
with a constant type family of the form fun _ => B'
, because the types A * B'
and {x : A & B'}
are isomorphic. But if you want to work directly with the Coq type of regular pairs, you can simply replicate the proofs for a more restricted version of the lexicographic product. The proof is not very complicated, but it requires a nested induction on the accessibility predicate that defines well-foundedness.
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.
然后您可以实例化此通用版本以进行恢复,例如,您对字典产品的三元组定义自然数:
You can then instantiate this general version to recover, for instance, your definition of the lexicographic product for triples of natural numbers:
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.
这篇关于nat元组的词典比较的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!