nats的元组的字典对比

Question

我正在使用nat s的元组（特别是三元组，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字典产品，以及有充分理由的proof。与定义的问题，但是，它指出了相关的对：

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

如果你愿意，你可以实例B以恒定型家庭形式fun _ => 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.