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.