nat의 튜플의 사전 비교

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의 사전 편집 제품과 잘 설립 된 proof을 가지고 있습니다. 유형 A * B' 및 {x : A & B'}가 동형 때문에,

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

원하는 경우 양식 fun _ => B'의 일정한 유형의 가족과 함께 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.