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.