# Library Schema

Require Import Utf8.
Require Import Setoid Eqdep.
Require Export Path.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

# Schemas

Record Schema :=
{
SVertex :> Type;
SEdge : SVertexSVertexType;

PathsEquivalent : s d, Relation_Definitions.relation (path SEdge s d);
PathsEquivalent_Equivalence : s d, equivalence _ (@PathsEquivalent s d);

PreCompose : s d (E : SEdge s d) d' (p1 p2 : path _ d d'),
PathsEquivalent p1 p2PathsEquivalent (prepend p1 E) (prepend p2 E);
PostCompose : s d (p1 p2 : path _ s d) d' (E : SEdge d d'),
}.

Hint Resolve PreCompose PostCompose.

Theorem PreCompose' : S s d (E : S.(SEdge) s d) d' (p1 p2 : path _ d d'),
PathsEquivalent _ p1 p2PathsEquivalent _ (prepend p1 E) (prepend p2 E).
intros; auto.
Qed.

Theorem PostCompose' : S s d (p1 p2 : path _ s d) d' (E : S.(SEdge) d d'),
PathsEquivalent _ p1 p2
intros; auto.
Qed.

Hint Resolve PreCompose' PostCompose'.

Add Parametric Relation S s d : _ (@PathsEquivalent S s d)
reflexivity proved by (equiv_refl _ _ (@PathsEquivalent_Equivalence _ _ _))
symmetry proved by (equiv_sym _ _ (@PathsEquivalent_Equivalence _ _ _))
transitivity proved by (equiv_trans _ _ (@PathsEquivalent_Equivalence _ _ _))
as paths_eq.

Hint Resolve paths_eq_Reflexive paths_eq_Symmetric.

Section path_Equivalence_Theorems.
Variable S : Schema.

Lemma addedge_equivalent : s d d' (p p' : path _ s d), PathsEquivalent S p p'
→ e : SEdge _ d d', PathsEquivalent S (AddEdge p e) (AddEdge p' e).
t.
Qed.

Lemma prepend_equivalent : s' s d (p p' : path _ s d), PathsEquivalent S p p'
→ e : SEdge _ s' s, PathsEquivalent S (prepend p e) (prepend p' e).
t.
Qed.

Hint Rewrite <- concatenate_concatenate'_equivalent.

Lemma pre_concatenate_equivalent : s' s d (p1 : path _ s' s) (p p' : path _ s d),
PathsEquivalent S p p'PathsEquivalent S (concatenate p1 p) (concatenate p1 p').
induction p1; t.
repeat rewrite concatenate_concatenate'_equivalent.
t.
Qed.

Lemma post_concatenate_equivalent : s d d' (p p' : path _ s d) (p2 : path _ d d'),
PathsEquivalent S p p'PathsEquivalent S (concatenate p p2) (concatenate p' p2).
induction p2; t.
Qed.

Hint Resolve pre_concatenate_equivalent post_concatenate_equivalent.

Add Parametric Morphism s d d' p:
(@concatenate _ S.(SEdge) s d d' p)
with signature (@PathsEquivalent S _ _) ==> (@PathsEquivalent S _ _) as concatenate_pre_mor.
t.
Qed.

Add Parametric Morphism s d d' p:
(fun p' ⇒ (@concatenate _ S.(SEdge) s d d' p' p))
with signature (@PathsEquivalent S _ _) ==> (@PathsEquivalent S _ _) as concatenate_post_mor.
t.
Qed.

Lemma concatenate_equivalent : s d d' (p1 p1' : path _ s d) (p2 p2' : path _ d d'),
PathsEquivalent S p1 p1'PathsEquivalent S p2 p2'PathsEquivalent S (concatenate p1 p2) (concatenate p1' p2').
t; etransitivity; eauto.
Qed.
End path_Equivalence_Theorems.

Hint Resolve concatenate_equivalent.

Add Parametric Morphism S s d d' :
(@concatenate _ S.(SEdge) s d d')
with signature (@PathsEquivalent S _ _) ==> (@PathsEquivalent S _ _) ==> (@PathsEquivalent S _ _) as concatenate_mor.
t.
Qed.

Add Parametric Morphism S s d d' :
(@AddEdge S _ s d d')
with signature (@PathsEquivalent S _ _) ==> (@eq _) ==> (@PathsEquivalent S _ _) as AddEdge_mor.
t.
Qed.

Add Parametric Morphism S s d d' :
(fun p ⇒ @concatenate' S _ s d p d')
with signature (@PathsEquivalent S _ _) ==> (@PathsEquivalent S _ _) ==> (@PathsEquivalent S _ _) as concatenate'_mor.
intros; repeat rewrite <- concatenate_concatenate'_equivalent; t.
Qed.

Add Parametric Morphism S s' s d :
(fun p ⇒ @prepend S _ s d p s')
with signature (@PathsEquivalent S _ _) ==> (@eq _) ==> (@PathsEquivalent S _ _) as prepend_mor.
t.
Qed.

Section Schema.
Variable C : Schema.

Definition SEpimorphism x y (p : path (SEdge C) x y) : Prop :=
z (p1 p2 : path (SEdge C) y z), PathsEquivalent _ (concatenate p p1) (concatenate p p2) →
PathsEquivalent _ p1 p2.
Definition SMonomorphism x y (p : path (SEdge C) x y) : Prop :=
z (p1 p2 : path (SEdge C) z x), PathsEquivalent _ (concatenate p1 p) (concatenate p2 p) →
PathsEquivalent _ p1 p2.

Definition SInverseOf s d (p : path (SEdge C) s d) (p' : path (SEdge C) d s) : Prop :=
PathsEquivalent _ (concatenate p p') NoEdges
PathsEquivalent _ (concatenate p' p) NoEdges.

Lemma SInverseOf_sym s d m m' : @SInverseOf s d m m' → @SInverseOf d s m' m.
firstorder.
Qed.

Definition SchemaIsomorphism' s d (p : path (SEdge C) s d) : Prop :=
p', SInverseOf p p'.

Definition SchemaIsomorphism s d (p : path (SEdge C) s d) := { p' | SInverseOf p p' }.

Hint Unfold SInverseOf SchemaIsomorphism' SchemaIsomorphism.

Lemma SInverseOf1 : (s d : C) (p : _ s d) p', SInverseOf p p'
→ PathsEquivalent _ (concatenate p p') NoEdges.
firstorder.
Qed.

Lemma SInverseOf2 : (s d : C) (p : _ s d) p', SInverseOf p p'
→ PathsEquivalent _ (concatenate p p') NoEdges.
firstorder.
Qed.

Lemma SchemaIsomorphism2Isomorphism' s d (p : path (SEdge C) s d) : SchemaIsomorphism pSchemaIsomorphism' p.
firstorder.
Qed.

Hint Rewrite <- SInverseOf1 SInverseOf2 using assumption.

Lemma s_iso_is_epi s d (p : path (SEdge C) s d) : SchemaIsomorphism pSEpimorphism p.
destruct 1 as [ x [ i0 i1 ] ]; intros z p1 p2 e.
transitivity (concatenate (concatenate x p) p1). t_con @PathsEquivalent.
transitivity (concatenate (concatenate x p) p2); repeat rewrite concatenate_associative; t_con @PathsEquivalent;
repeat rewrite <- concatenate_associative; t_con @PathsEquivalent.
Qed.

Lemma SInverseOf1' : x y z (p : path (SEdge C) x y) (p' : path (SEdge C) y x) (p'' : path (SEdge C) z _),
SInverseOf p p'
→ PathsEquivalent _ (concatenate (concatenate p'' p) p') p''.
unfold SInverseOf; intros; destruct_hypotheses; repeat rewrite concatenate_associative; t_con @PathsEquivalent.
Qed.

Hint Rewrite SInverseOf1' using assumption.

Lemma s_iso_is_mono s d (p : path (SEdge C) s d) : SchemaIsomorphism pSMonomorphism p.
destruct 1 as [ x [ i0 i1 ] ]; intros z p1 p2 e.
transitivity (concatenate p1 (concatenate p x)). t_con @PathsEquivalent.
transitivity (concatenate p2 (concatenate p x)); solve [ repeat rewrite <- concatenate_associative; t_con @PathsEquivalent ] || t_con @PathsEquivalent.
Qed.

Theorem SchemaIdentityInverse (x : C) : SInverseOf (@NoEdges _ _ x) (@NoEdges _ _ x).
hnf; t.
Qed.

Hint Resolve SchemaIdentityInverse.

Theorem SchemaIdentityIsomorphism (x : C) : SchemaIsomorphism (@NoEdges _ _ x).
eauto.
Qed.
End Schema.

Hint Resolve SchemaIsomorphism2Isomorphism'.

Ltac concatenate4associativity' a b c d := transitivity (concatenate a (concatenate (concatenate b c) d));
try solve [ repeat rewrite concatenate_associative; reflexivity ].
Ltac concatenate4associativity :=
match goal with
| [ |- ?Rel (concatenate (concatenate ?a ?b) (concatenate ?c ?d)) _ ] ⇒ concatenate4associativity' a b c d
| [ |- ?Rel _ (concatenate (concatenate ?a ?b) (concatenate ?c ?d)) ] ⇒ concatenate4associativity' a b c d
end.

Section SchemaIsomorphismEquivalenceRelation.
Variable C : Schema.
Variable s d d' : C.

Theorem SchemaIsomorphismComposition (p : path (SEdge C) s d) (p' : path (SEdge C) d d') :
SchemaIsomorphism _ pSchemaIsomorphism _ p'SchemaIsomorphism _ (concatenate p p').
repeat destruct 1; unfold SInverseOf in *; destruct_hypotheses.
match goal with
| [ m : path _ _ _, m' : path _ _ _ |- _ ] ⇒ (concatenate m m')
end;
split;
concatenate4associativity; t_con @PathsEquivalent.
Qed.
End SchemaIsomorphismEquivalenceRelation.

Definition path_unique (A : Schema) s d (x : path (SEdge A) s d) := x' : path (SEdge A) s d, PathsEquivalent _ x' x.

Section GeneralizedPathEquivalence.
Variable S : Schema.

Inductive GeneralizedPathsEquivalent s d (p : path (SEdge S) s d) : s' d' (p' : path (SEdge S) s' d'), Prop :=
| GPathsEquivalent (p' : path (SEdge S) s d) : PathsEquivalent _ p p'GeneralizedPathsEquivalent p p'.

Lemma GeneralizedPathsEquivalent_PathsEquivalent s d (p p' : path (SEdge S) s d) :
GeneralizedPathsEquivalent p p'PathsEquivalent _ p p'.
intro H; inversion H.
repeat match goal with
| [ H : _ |- _ ] ⇒ apply inj_pair2 in H
end.
repeat subst.
assumption.
Qed.

Lemma GeneralizedPathsEquivalent_eq s d (p : path (SEdge S) s d) s' d' (p' : path (SEdge S) s' d') :
GeneralizedPathsEquivalent p p's = s' d = d'.
intro H; inversion H.
repeat subst.
split; trivial.
Qed.
End GeneralizedPathEquivalence.

Ltac simpl_GeneralizedPathsEquivalent := intros;
repeat match goal with
| [ H : GeneralizedPathsEquivalent _ _ _ |- _ ]
⇒ destruct (GeneralizedPathsEquivalent_eq H); repeat subst;
apply GeneralizedPathsEquivalent_PathsEquivalent in H
| [ |- GeneralizedPathsEquivalent _ _ _ ] ⇒ apply GPathsEquivalent
end.

Section GeneralizedPathsEquivalenceRelation.
Variable S : Schema.

Lemma GeneralizedPathsEquivalent_refl s d (p : path (SEdge S) s d) : GeneralizedPathsEquivalent _ p p.
simpl_GeneralizedPathsEquivalent; reflexivity.
Qed.

Lemma GeneralizedPathsEquivalent_sym s d (p : path (SEdge S) s d) s' d' (p' : path (SEdge S) s' d') :
GeneralizedPathsEquivalent _ p p'GeneralizedPathsEquivalent _ p' p.
simpl_GeneralizedPathsEquivalent; symmetry; assumption.
Qed.

Lemma GeneralizedPathsEquivalent_trans s d (p : path (SEdge S) s d) s' d' (p' : path (SEdge S) s' d') s'' d'' (p'' : path (SEdge S) s'' d'') :
GeneralizedPathsEquivalent _ p p'GeneralizedPathsEquivalent _ p' p''GeneralizedPathsEquivalent _ p p''.
simpl_GeneralizedPathsEquivalent; transitivity p'; eauto.
Qed.
End GeneralizedPathsEquivalenceRelation.