Library Coq.Wellfounded.Lexicographic_Product
Authors: Bruno Barras, Cristina Cornes
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.