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'),
                    PathsEquivalent p1 p2PathsEquivalent (AddEdge p1 E) (AddEdge p2 E)
  }.

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
  → PathsEquivalent _ (AddEdge p1 E) (AddEdge p2 E).
  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_noedges_p concatenate_p_addedge.
  Hint Rewrite <- concatenate_concatenate'_equivalent.
  Hint Resolve prepend_equivalent addedge_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.