Library Padec.Tools.TransClosAccDec

From Coq Require Import Wellfounded.
From Coq Require Import List.
From Coq Require Import SetoidList.


Definition relation A := A -> A -> Prop.

Section Relations.
  Variable A:Type.
  Variable eqA: relation A.
  Variable Adec:forall x y:A,{eqA x y}+{~eqA x y}.

  Hypothesis eqA_equiv: Equivalence eqA.

  Definition transitive (R:relation A) :=
    forall x y z:A, R x y -> R y z -> R x z.

  Definition included (R1 R2:relation A) :=
    forall x y:A, R1 x y -> R2 x y.

  Inductive transitive_closure R : A -> A -> Prop :=
    TC_incl : included R (transitive_closure R)
  | TC_trans : transitive (transitive_closure R).

  Inductive transitive_closure_alt R (a b:A) :Prop :=
  |TC_step: R a b->transitive_closure_alt R a b
  |TC_ind : forall y, transitive_closure_alt R a y ->
                      transitive_closure_alt R y b ->
                      transitive_closure_alt R a b.

  Lemma transitive_closure_transitive_closure_alt_if:
    forall R, included (transitive_closure R) (transitive_closure_alt R).

  Lemma transitive_closure_alt_transitive_closure_if:
    forall R:A->A->Prop, included (transitive_closure_alt R)
                                  (transitive_closure R) .

  Lemma transitive_closure_alt_transitive_closure_iff:
    forall (R:A->A->Prop) x y,
      (transitive_closure_alt R) x y <-> (transitive_closure R) x y.

  Lemma transitive_closure_is_smallest :
    forall R R0:relation A, included R R0 -> transitive R0 ->
                            included (transitive_closure R) R0.

  Lemma transitive_closure_monotonic :
    forall R R0:relation A, included R R0 ->
                            included (transitive_closure R)
                                     (transitive_closure R0).

  Lemma transitive_closure_split_right :
    forall R (x y:A), transitive_closure R x y ->
                      R x y \/
                      exists z, (transitive_closure R x z /\ R z y).
  Section R.
    Variable R:relation A.

    Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.


    Scheme Acc_ind_dep := Induction for Acc Sort Prop.

    Lemma acc_rel_is_non_reflexive:
      forall (x: A), Acc R x -> ~R x x.

    CoInductive path (x:A): Type :=
      path_cont : forall y, R y x -> path y -> path x
    | path_end : path x.

    Inductive finite_path : forall x, path x -> Prop :=
      finite_cont: forall x y (h:R y x) (p:path y),
        finite_path y p -> finite_path x (path_cont x y h p)
    | finite_end : forall x, finite_path x (path_end x).

    Theorem wf_finite_path : well_founded R -> forall x p, finite_path x p.
  End R.

  Section finite.
    Variable lA:list A.
    Hypothesis A_finite: forall a:A, InA eqA a lA.

    Section R.
      Variable R:relation A.

      Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.

      Inductive l_transitive_closure l : relation A :=
        LTC_incl: included R (l_transitive_closure l)
      | LTC_l_trans : forall x y z, InA eqA y l ->
                                    l_transitive_closure l x y ->
                                    l_transitive_closure l y z ->
                                    l_transitive_closure l x z.

      Lemma l_transitive_closure_compat:
        forall l, Proper (eqA==>eqA==>impl) (l_transitive_closure l).



      Lemma TC_LTC_lA_incl:
        included (transitive_closure R) (l_transitive_closure lA).

      Lemma LTC_TC_incl:
        forall l, included (l_transitive_closure l) (transitive_closure R).

      Lemma LTC_nil_R_incl:included (l_transitive_closure nil) R.

      Lemma R_LTC_nil_incl:included R (l_transitive_closure nil).

      Lemma LTC_cons_incl:
        forall a l, included
                      (l_transitive_closure l)
                      (l_transitive_closure (a::l)).

      Variable Rdec:forall x y:A,{R x y}+{~R x y}.

      Lemma trans_dec: forall x y,
          {transitive_closure R x y}+{~transitive_closure R x y}.
    End R.

  End finite.
End Relations.