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.