Coq Library
Tools

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.
Any well-founded relation cannot be reflexive!
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.