From Coq Require Import SetoidList.
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import BoolEq.
From Coq Require Import Morphisms.
From Coq Require Import RelationPairs.
From Coq Require Import Setoid.
From Coq Require Import SetoidClass.

From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.

Open Scope Z_scope.

Open Scope signature_scope.
Set Implicit Arguments.

Class POR {A} eqA `{equ: Equivalence A eqA} (R: relation A): Prop :=
  {
    POR_Antisymmetric :> Antisymmetric A eqA R | 4 ;
    POR_Transitive :> Transitive R | 4
  }.

Section With_A.

  Context {A} `{SA: Setoid A}.

  Section RelationA.

    Definition subrelationA (R1 R2: relation A): Prop :=
      subrelation R1 R2 /\
      Proper fequiv R1 /\ Proper fequiv R2.

    Global Instance subrelationA_POR: POR subrelationA.

    Lemma relationA_PER_POR: subrelation fequiv subrelationA.

  End RelationA.

  Section Closure.

    Context
      (P: relation A -> Prop)
      `{P_compat: Proper _ (fequiv ==> iff) P}
      (C: relation A -> relation A)
      `{C_compat: Proper _ (fequiv ==> fequiv) C}
    .

    Section Closure_Hypotheses.

      Definition closure_superrelation :=
        forall R, Proper fequiv R -> subrelationA R (C R).

      Definition closure_minimal :=
        forall R1 R2, subrelationA R1 R2 ->
                      P R2 ->
                      subrelationA (C R1) R2.

      Definition closure_valid :=
        forall R, Proper fequiv R -> P (C R).

    End Closure_Hypotheses.

    Context
      (superrelation: closure_superrelation)
      (minimal: closure_minimal)
      (valid: closure_valid)
    .

    Section Closure_Monotone.

      Instance closure_monotone: Proper (subrelationA ==> subrelationA) C.

    End Closure_Monotone.

    Section Closure_Of_Valid_Is_Subrelation.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
        (R_valid: P R)
      .

      Lemma closure_of_valid_subrelation: subrelation (C R) R.

    End Closure_Of_Valid_Is_Subrelation.

    Section Closure_Of_Valid_Is_Eq.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
        (R_valid: P R)
      .

      Lemma closure_of_valid_indentity: fequiv R (C R).

    End Closure_Of_Valid_Is_Eq.

  End Closure.

  Section Reflexive_Closure.

    Section Reflexive_Closure_Definition.
      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Definition reflexive_closure x y := x == y \/ R x y.

      Global Instance reflexive_closure_compat: Proper fequiv reflexive_closure.

    End Reflexive_Closure_Definition.

    Section Reflexive_Closure_Superrelation.

      Lemma reflexive_closure_superrelation:
        closure_superrelation reflexive_closure.

    End Reflexive_Closure_Superrelation.

    Section Reflexive_Closure_Minimal.

      Lemma reflexive_closure_minimal:
        closure_minimal Reflexive reflexive_closure.

    End Reflexive_Closure_Minimal.

    Section Reflexive_Closure_Valid.

      Lemma reflexive_closure_valid: closure_valid Reflexive reflexive_closure.

    End Reflexive_Closure_Valid.

    Section Reflexive_Closure_Monotone.

      Instance reflexive_closure_monotone:
        Proper (subrelationA ==> subrelationA) reflexive_closure.

    End Reflexive_Closure_Monotone.

    Section Reflexive_Closure_Reflexive.

      Context
        (R : relation A)
        `{R_compat : Proper _ fequiv R}.

      Instance reflexive_closure_reflexive : Reflexive (reflexive_closure R).

    End Reflexive_Closure_Reflexive.

    Section Reflexive_Closure_Transitive.

      Context
        (R : relation A)
        `{R_compat : Proper _ fequiv R}
        `{R_trans : Transitive _ R}
      .

      Instance reflexive_closure_transitive: Transitive (reflexive_closure R).

    End Reflexive_Closure_Transitive.

    Section Reflexive_Closure_Symmetric.

      Context
        (R : relation A)
        `{R_compat : Proper _ fequiv R}
        `{R_symm : Symmetric _ R}
      .

      Global Instance reflexive_closure_symmetric: Symmetric (reflexive_closure R).

    End Reflexive_Closure_Symmetric.

    Section Reflexive_Closure_Dec.
      Context
        (eqA_dec: Decider (equiv (A := A)))
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
        (R_dec: Decider R)
      .

      Lemma reflexive_closure_dec: Decider (reflexive_closure R).

    End Reflexive_Closure_Dec.

  End Reflexive_Closure.

  Section Transitive_Closure.

    Section Transitive_Closure_Definition.

      Inductive transitive_closure (R: relation A): relation A :=
      | transitive_closure_step (x y: A): R x y -> transitive_closure R x y
      | transitive_closure_transitivity (x y z: A):
          transitive_closure R x y -> transitive_closure R y z ->
          transitive_closure R x z
      .

      Global Instance transitive_closure_compat :
        Proper fequiv transitive_closure.

    End Transitive_Closure_Definition.

    Section Transitive_Closure_Left_Definition.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Inductive transitive_closure_left: relation A :=
      | transitive_closure_left_step (x y: A):
          R x y -> transitive_closure_left x y
      | transitive_closure_left_transitivity (x y z: A):
          R x y -> transitive_closure_left y z -> transitive_closure_left x z
      .

      Instance transitive_closure_left_compat:
        Proper fequiv transitive_closure_left.

    End Transitive_Closure_Left_Definition.

    Section Transitive_Closure_Left_Iff_Transitive_Closure.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Lemma transitive_closure_left_iff_transitive_closure:
        forall x y,
          (transitive_closure_left R) x y <-> (transitive_closure R) x y
      .

    End Transitive_Closure_Left_Iff_Transitive_Closure.

    Section Transitive_Closure_Right_Definition.
      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Inductive transitive_closure_right: relation A :=
      | transitive_closure_right_step (x y: A): R x y ->
                                                transitive_closure_right x y
      | transitive_closure_right_transitivity (x y z: A):
          transitive_closure_right x y -> R y z -> transitive_closure_right x z
      .

      Global Instance transitive_closure_right_compat:
        Proper fequiv transitive_closure_right.

    End Transitive_Closure_Right_Definition.

    Section Transitive_Closure_Right_Iff_Transitive_Closure.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Lemma transitive_closure_right_iff_transitive_closure:
        forall x y,
          (transitive_closure_right R) x y <-> (transitive_closure R) x y
      .

    End Transitive_Closure_Right_Iff_Transitive_Closure.

    Section Transitive_Closure_Superrelation.

      Lemma transitive_closure_superrelation:
        closure_superrelation transitive_closure.

    End Transitive_Closure_Superrelation.

    Section Transitive_Closure_Minimal.

      Lemma transitive_closure_minimal:
        closure_minimal Transitive transitive_closure.

    End Transitive_Closure_Minimal.

    Section Transitive_Closure_Valid.

      Lemma transitive_closure_valid:
        closure_valid Transitive transitive_closure.

    End Transitive_Closure_Valid.

    Section Transitive_Closure_Monotone.

      Instance transitive_closure_monotone:
        Proper (subrelationA ==> subrelationA) transitive_closure.

    End Transitive_Closure_Monotone.

    Section Transitive_Closure_Reflexive.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
        `{R_refl: Reflexive _ R}
      .

      Instance transitive_closure_reflexive: Reflexive (transitive_closure R).

    End Transitive_Closure_Reflexive.


    Section Transitive_Closure_Transitive.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Instance transitive_closure_transitive: Transitive (transitive_closure R).

    End Transitive_Closure_Transitive.

    Section Transitive_Closure_Symmetric.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
        `{R_symm: Symmetric _ R}
      .
      Instance transitive_closure_symmetric: Symmetric (transitive_closure R).

    End Transitive_Closure_Symmetric.

  End Transitive_Closure.

  Section Symmetric_Closure.

    Section Symmetric_Closure_Definition.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Definition symmetric_closure x y := R x y \/ R y x.

      Global Instance symmetric_closure_compat: Proper fequiv symmetric_closure.

    End Symmetric_Closure_Definition.

    Section Symmetric_Closure_Superrelation.

      Lemma symmetric_closure_superrelation:
        closure_superrelation symmetric_closure.

    End Symmetric_Closure_Superrelation.

    Section Symmetric_Closure_Minimal.

      Lemma symmetric_closure_minimal:
        closure_minimal Symmetric symmetric_closure.

    End Symmetric_Closure_Minimal.

    Section Symmetric_Closure_Valid.

      Lemma symmetric_closure_valid: closure_valid Symmetric symmetric_closure.

    End Symmetric_Closure_Valid.

    Section Symmetric_Closure_Monotone.

      Instance symmetric_closure_monotone:
        Proper (subrelationA ==> subrelationA) symmetric_closure.

    End Symmetric_Closure_Monotone.

    Section Symmetric_Closure_Reflexive.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
        `{R_refl: Reflexive _ R}
      .

      Instance symmetric_closure_reflexive: Reflexive (symmetric_closure R).

    End Symmetric_Closure_Reflexive.

    Section Symmetric_Closure_Transitive.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .


      Definition symmetric_closure_transitive:
        False -> Transitive (symmetric_closure R).

    End Symmetric_Closure_Transitive.

    Section Symmetric_Closure_Symmetric.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Instance symmetric_closure_symmetric: Symmetric (symmetric_closure R).

    End Symmetric_Closure_Symmetric.

    Section Symmetric_Closure_Dec.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
        (R_dec: Decider R)
      .

      Lemma symmetric_closure_dec: Decider (symmetric_closure R).

    End Symmetric_Closure_Dec.

  End Symmetric_Closure.

  Section Reflexive_Transitive_Closure.

    Section Reflexive_Transitive_Closure_Definition.

      Context (R: relation A) `{R_compat: Proper _ fequiv R}.

      Definition reflexive_transitive_closure :=
        reflexive_closure (transitive_closure R).

      Instance reflexive_transitive_closure_compat:
        Proper fequiv reflexive_transitive_closure.

    End Reflexive_Transitive_Closure_Definition.

    Section Reflexive_Transitive_Closure_Superrelation.

      Lemma reflexive_transitive_closure_superrelation:
        closure_superrelation reflexive_transitive_closure.

    End Reflexive_Transitive_Closure_Superrelation.

    Section Reflexive_Transitive_Closure_Minimal.

      Lemma reflexive_transitive_closure_minimal:
        closure_minimal PreOrder reflexive_transitive_closure.

    End Reflexive_Transitive_Closure_Minimal.

    Section Reflexive_Transitive_Closure_Valid.

      Lemma reflexive_transitive_closure_valid:
        closure_valid PreOrder reflexive_transitive_closure.

    End Reflexive_Transitive_Closure_Valid.

    Section Reflexive_Transitive_Closure_Monotone.

      Instance reflexive_transitive_closure_monotone:
        Proper (subrelationA ==> subrelationA) reflexive_transitive_closure.

    End Reflexive_Transitive_Closure_Monotone.

    Section Reflexive_Transitive_Closure_Reflexive.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Instance reflexive_symmetric_closure_reflexive:
        Reflexive (reflexive_transitive_closure R).

    End Reflexive_Transitive_Closure_Reflexive.

    Section Reflexive_Transitive_Closure_Transitive.
      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Definition reflexive_transitive_closure_transitive:
        Transitive (reflexive_transitive_closure R).

    End Reflexive_Transitive_Closure_Transitive.

    Section Reflexive_Transitive_Closure_Symmetric.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
        `{R_symm: Symmetric _ R}
      .

      Definition reflexive_transitive_closure_symmetric:
        Symmetric (reflexive_transitive_closure R).

    End Reflexive_Transitive_Closure_Symmetric.

    Section Reflexive_Transitive_Closure_Dec.
    End Reflexive_Transitive_Closure_Dec.

  End Reflexive_Transitive_Closure.

  Section Reflexive_Transitive_Symmetric_Closure.

    Section Reflexive_Transitive_Symmetric_Closure_Definition.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Definition reflexive_transitive_symmetric_closure :=
        (reflexive_transitive_closure (symmetric_closure R)).

      Definition reflexive_transitive_symmetric_closure_compat:
        Proper fequiv reflexive_transitive_symmetric_closure.

    End Reflexive_Transitive_Symmetric_Closure_Definition.

    Section Reflexive_Transitive_Symmetric_Closure_Superrelation.

      Lemma reflexive_transitive_symmetric_closure_superrelation:
        closure_superrelation reflexive_transitive_symmetric_closure.

    End Reflexive_Transitive_Symmetric_Closure_Superrelation.

    Section Reflexive_Transitive_Symmetric_Closure_Minimal.

      Lemma reflexive_transitive_symmetric_closure_minimal:
        closure_minimal Equivalence reflexive_transitive_symmetric_closure.

    End Reflexive_Transitive_Symmetric_Closure_Minimal.

    Section Reflexive_Transitive_Symmetric_Closure_Valid.

      Lemma reflexive_transitive_symmetric_closure_valid:
        closure_valid Equivalence reflexive_transitive_symmetric_closure.

    End Reflexive_Transitive_Symmetric_Closure_Valid.

    Section Reflexive_Transitive_Symmetric_Closure_Monotone.

      Instance reflexive_transitive_symmetric_closure_monotone:
        Proper (subrelationA ==> subrelationA)
               reflexive_transitive_symmetric_closure.

    End Reflexive_Transitive_Symmetric_Closure_Monotone.

    Section Reflexive_Transitive_Symmetric_Closure_Reflexive.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Instance reflexive_transitive_symmetric_closure_reflexive:
        Reflexive (reflexive_transitive_symmetric_closure R).

    End Reflexive_Transitive_Symmetric_Closure_Reflexive.

    Section Reflexive_Transitive_Symmetric_Closure_Transitive.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Instance reflexive_transitive_symmetric_closure_transitive:
        Transitive (reflexive_transitive_symmetric_closure R).

    End Reflexive_Transitive_Symmetric_Closure_Transitive.

    Section Reflexive_Transitive_Symmetric_Closure_Symmetric.
      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Instance reflexive_transitive_symmetric_closure_symmetric:
        Symmetric (reflexive_transitive_symmetric_closure R).

    End Reflexive_Transitive_Symmetric_Closure_Symmetric.

  End Reflexive_Transitive_Symmetric_Closure.

  Section Non_Empty_Chain.

    Section Non_Empty_Chain_Definition.

      Fixpoint non_empty_chain (R: relation A) x p y:=
        match p with
        | nil => R x y
        | h:: t => R x h /\ non_empty_chain R h t y
        end
      .

      Global Instance non_empty_chain_compat:
        Proper (pequiv ==> equiv ==> eqlistA equiv ==> fequiv) non_empty_chain.

    End Non_Empty_Chain_Definition.

    Section Transitive_Closure_Left_Iff_Exists_Non_Empty_Chain.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Lemma transitive_closure_left_iff_exists_non_empty_chain:
        forall x y,
          (transitive_closure_left R x y) <-> (exists c, non_empty_chain R x c y)
      .

    End Transitive_Closure_Left_Iff_Exists_Non_Empty_Chain.

    Section Transitive_Closure_Iff_Exists_Non_Empty_Chain.
      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Lemma transitive_closure_iff_exists_non_empty_chain:
        forall x y,
          (transitive_closure R x y) <-> (exists c, non_empty_chain R x c y)
      .

    End Transitive_Closure_Iff_Exists_Non_Empty_Chain.

  End Non_Empty_Chain.

  Section Chain.

    Section Chain_Definition.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Fixpoint chain x p y:=
        match p with
        | nil => x == y
        | h :: t => R x h /\ chain h t y
        end
      .

      Global Instance chain_compat:
        Proper (equiv ==> eqlistA equiv ==> fequiv) chain.

    End Chain_Definition.

    Lemma chain_equiv_equiv:
      forall (R1: relation A) (R2: relation A),
        R1 =~= R2 ->
        (equiv ==> eqlistA equiv ==> fequiv)%signature
                                            (chain R1)
                                            (chain R2).

    Section Chain_App.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Lemma chain_app: forall x p1 p2 z,
          chain R x (p1 ++ p2) z <-> exists y, chain R x p1 y /\ chain R y p2 z
      .

    End Chain_App.

    Section Chain_Cons_Iff_Non_Empty_Chain.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Lemma chain_cons_iff_non_empty_chain:
        forall x z p,
          chain R x (p ++ (z :: nil)) z <-> non_empty_chain R x p z
      .

    End Chain_Cons_Iff_Non_Empty_Chain.
    Section Chain_Exists_Iff_Reflexive_Transitive_Closure.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Lemma list_snoc_inv: forall A (l: list A), l <> nil ->
                                                 exists h t, l = t ++ (h :: nil).

      Lemma chain_last_eq:
        forall x t z y, chain R x (t ++ z :: nil) y -> z == y.

      Lemma chain_exists_iff_reflexive_transitive_closure:
        forall x y, ((exists p, chain R x p y) <->
                     (reflexive_transitive_closure R) x y)
      .

    End Chain_Exists_Iff_Reflexive_Transitive_Closure.

    Section Chain_Dec.

      Context
        (R: relation A)
        `{R_compat: Proper _ fequiv R}
      .

      Lemma chain_dec:
        Decider equiv ->
        Decider R ->
        forall x p y, {chain R x p y} + {~ (chain R x p y)}
      .
    End Chain_Dec.

  End Chain.

  Section Chain_Inclusion.

    Lemma chain_incl:
      forall (R: relation A) (R': relation A),
        inclusion R' R ->
        forall (a: A) (la: list A) (a': A),
          chain R' a' la a -> chain R a' la a.

    Lemma chain_compat_incl:
      forall (R: relation A) (R': relation A),
        Proper fequiv R ->
        Proper fequiv R' ->
        inclusion R' R ->
        forall (a: A) (b: A) (la: list A) (lb: list A)
               (a': A) (b': A),
          a == b -> a' == b' -> eqlistA equiv la lb
          -> chain R' a la a' -> chain R b lb b'.

  End Chain_Inclusion.

  Section chain_cons_non_empty.
    Context
      (R: relation A)
      `{R_compat: Proper _ fequiv R}
    .

    Lemma chain_cons_non_empty: forall (a1 a2:A) (l:list A) ,
        chain R a1 (l ++ a2 :: nil) a2 <->
        non_empty_chain R a1 l a2.

  End chain_cons_non_empty.

End With_A.

Close Scope signature_scope.
Unset Implicit Arguments.