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.