Library Stdlib.Wellfounded.Lexicographic_Product
Authors: Bruno Barras, Cristina Cornes
Require Import EqdepFacts.
Require Import Relation_Operators.
Require Import Transitive_Closure.
Require Import Inclusion.
Require Import Inverse_Image.
From : Constructing Recursion Operators in Type Theory
L. Paulson JSC (1986) 2, 325-355
Section WfLexicographic_Product.
Import SigTNotations.
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 (x; y).
Theorem wf_lexprod :
well_founded leA ->
(forall x : A, well_founded (leB x)) -> well_founded LexProd.
End WfLexicographic_Product.
Section WfSimple_Lexicographic_Product.
Variable A : Type.
Variable B : Type.
Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.
Notation LexProd := (slexprod A B leA leB).
Theorem wf_slexprod :
well_founded leA -> well_founded leB -> well_founded LexProd.
End WfSimple_Lexicographic_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.