# Library Coq.Wellfounded.Lexicographic_Product

Authors: Bruno Barras, Cristina Cornes
Require Import Eqdep.
Require Import Relation_Operators.
Require Import Transitive_Closure.
From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355
Section WfLexicographic_Product.
Variable A : Type.
Variable B : A -> Type.
Variable leA : A -> A -> Prop.
Variable leB : forall x:A, B x -> B x -> Prop.
Notation LexProd := (lexprod A B leA leB).
Lemma acc_A_B_lexprod :
forall x:A,
Acc leA x ->
(forall x0:A, clos_trans A leA x0 x -> well_founded (leB x0)) ->
forall y:B x, Acc (leB x) y -> Acc LexProd (existS B x y).
Theorem wf_lexprod :
well_founded leA ->
(forall x:A, well_founded (leB x)) -> well_founded LexProd.
End WfLexicographic_Product.
Section Wf_Symmetric_Product.
Variable A : Type.
Variable B : Type.
Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.
Notation Symprod := (symprod A B leA leB).
Lemma Acc_symprod :
forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod ( x , y ).
Lemma wf_symprod :
well_founded leA -> well_founded leB -> well_founded Symprod.
End Wf_Symmetric_Product.
Section Swap.
Variable A : Type.
Variable R : A -> A -> Prop.
Notation SwapProd := (swapprod A R).
Lemma swap_Acc : forall x y:A, Acc SwapProd ( x , y ) -> Acc SwapProd ( y , x ).
Lemma Acc_swapprod :
forall x y:A, Acc R x -> Acc R y -> Acc SwapProd ( x , y ).
Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
End Swap.