Coq Library
Tools

#### Global imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
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.

#### Local imports

Open Scope Z_scope.

Open Scope signature_scope.
Set Implicit Arguments.

(Strict) Partial Order Relation
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.

## Closure

Section Closure.

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

#### Closure hypotheses

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)
.

#### Closure properties

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.

## Reflexive closure

Section Reflexive_Closure.

#### Definition

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.

#### Reflexive_Closure_Properties

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}
.

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.

### Transitive closure

Section Transitive_Closure.

#### Transitive closure properties

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.

### Symmetric closure

Section Symmetric_Closure.

#### Definition

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.

#### Symmetric closure properties

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.

### Reflexive transitive closure

Section Reflexive_Transitive_Closure.

#### Definition

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.

#### Reflexive transitive closure properties

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.

# CHAINS of related elements

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.