Library hydras.Prelude.DecPreOrder_Instances

From hydras Require Export DecPreOrder.
From Coq Require Import Arith ZArith List Sets.Finite_sets Sets.Ensembles.

#[ global ] Instance Nat_le_dec : RelDecision le := le_dec.

#[ global ] Instance Nat_le_TO : TotalPreOrder le.

#[ global ] Instance Z_le_dec : RelDecision Z.le := Z_le_dec.

#[ global ] Instance Z_le_TO : TotalPreOrder Z.le.
Qed.

Import DecPreOrder.

#[ global ] Instance Inverse_fun {A B:Type}{f : A → B}
         {leB: relation B}{PB: PreOrder leB}:
                     PreOrder (fun x y ⇒ leB (f x) (f y)).

#[ global ] Instance Total_Inverse_fun {A B:Type}{f : A → B}
         {leB: relation B}{TB: TotalPreOrder leB} :
                     TotalPreOrder (fun x y ⇒ leB (f x) (f y)).

#[ global ] Instance RelDecision_Inverse_fun {A B:Type}{f : A → B}
 {leB: relation B} {RDB : RelDecision leB} :
  RelDecision (fun x y ⇒ leB (f x) (f y)) :=
  fun x y ⇒ decide_rel leB (f x) (f y).

#[ global ] Instance PrO_Included {U:Type}: PreOrder (Included U).

Arguments Included {U} _ _.

Definition Included_s {U} (A B : Ensemble U) :=
  Included A B ∧ ¬ Included B A.

Infix "<:" := Included (at level 30).
Infix "'<s'" := Included_s (at level 30).

#[ global ] Instance List_length {A:Type}:
   TotalPreOrder (fun l l' : list A ⇒ List.length l ≤ List.length l')%nat.
Defined.

Section lexprod.
 Variables (A B : Type)
           (leA : relation A)
           (leB : relation B).
 Context (TA : TotalPreOrder leA)
         (TB : TotalPreOrder leB)
         (DA : RelDecision leA)
         (DB : RelDecision leB).

 Definition PA := @total_pre_order_pre A leA TA.
 Definition PB := @total_pre_order_pre B leB TB.


Notation "x '<=A' y" := (leA x y) (at level 70, no associativity).
Notation "x '<A' y" := (@lt A leA PA x y) (at level 70, no associativity).
Notation "x '<=B' y" := (leB x y) (at level 70, no associativity).
Notation "x '<B' y" := (@lt B leB PB x y ) (at level 70, no associativity).
Notation "x =A= y" := (@preorder_equiv A leA PA x y) (at level 70, no associativity).
Notation "x =B= y" := (@preorder_equiv B leB PB x y) (at level 70, no associativity).

Inductive lex_prod (p p':A×B): Prop :=
| lex1 : (fst p) <A (fst p') → lex_prod p p'
| lex2 : (fst p) =A= (fst p') → (snd p) ≤B (snd p') → lex_prod p p'.

Notation "x '<=lex' y" := (lex_prod x y) (at level 70, no associativity).
Notation "x '<lex' y" := (@lt (A×B) lex_prod _ x y) (at level 70, no associativity).

 #[global] Instance PO_lex_prod : PreOrder lex_prod.

Lemma lex_of_equiv (a a':A)(b b':B) :
     a =A= a' → b =B= b' → preorder_equiv (a,b) (a',b').

Lemma lex_inv_left (a a':A)(b b':B) :
  ((a,b) ≤lex (a',b')) → a ≤A a'.

Lemma lex_inv_right (a a':A)(b b':B) :
  ((a,b) ≤lex (a',b')) → a =A= a' → b ≤B b'.

Lemma lex_strict_intro_right (a a':A)(b b':B) :
  a =A= a' → b <B b' → (a,b) <lex (a',b').

Lemma lex_strict_intro_left (a a':A)(b b':B) :
  a <A a' → (a,b) <lex (a',b').

#[global] Instance To_lex_prod : TotalPreOrder lex_prod.
#[global] Instance lex_prod_dec : RelDecision lex_prod.

End lexprod.