Library hydras.Prelude.Simple_LexProd

From Coq Require Import Relations Wellfounded.Lexicographic_Product
        Wellfounded.Inverse_Image Wellfounded.Inclusion Setoid.
From Coq Require Export RelationClasses.

Section Definitions.

  Variables (A B : Type)
            (ltA : relation A)
            (ltB : relation B).

  Hypothesis wfA : well_founded ltA.
  Hypothesis wfB : well_founded ltB.

  Let pair2sig (p: A × B) := existT (fun _ : A ⇒ B) (fst p) (snd p).


  Inductive lexico : relation (A × B) :=
    lex_1 : ∀ a a' b b', ltA a a' → lexico (a,b) (a',b')
  | lex_2 : ∀ a b b', ltB b b' → lexico (a,b) (a,b') .


  #[global] Instance Trans_lex {SA : StrictOrder ltA}
         {SB : StrictOrder ltB} :Transitive lexico.

  #[global] Instance Strict_lex {SA : StrictOrder ltA}
         {SB : StrictOrder ltB} : StrictOrder lexico.


  Lemma wf_lexico : well_founded lexico.


End Definitions.

Arguments lexico {A B} _ _ _ _.
Arguments wf_lexico {A B ltA ltB} _ _ _.

Example Ex1 : lexico lt lt (3,5) (4,2).

Example Ex2 : lexico lt lt (3,5) (3,6).