# 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 (existT 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.