Library SchemaMorphism


Require Import Utf8.
Require Import Setoid FunctionalExtensionality ProofIrrelevance JMeq Eqdep.
Require Export Schema.
Require Import Common Notations FEqualDep.

Set Implicit Arguments.

Generalizable All Variables.

Schema Morphisms


Section Schemas.
  Variables C D : Schema.

  Section transferPath.
    Variable vertexOf : CD.
    Variable pathOf : s d, C.(SEdge) s dpath (SEdge D) (vertexOf s) (vertexOf d).

    Fixpoint transferPath s d (p : path (SEdge C) s d) : path (SEdge D) (vertexOf s) (vertexOf d) :=
      match p with
        | NoEdgesNoEdges
        | AddEdge _ _ p' Econcatenate (transferPath p') (pathOf _ _ E)
      end.

    Hint Rewrite concatenate_noedges_p concatenate_p_noedges.
    Hint Rewrite <- concatenate_associative.

    Lemma concatenate_transferPath s d d' (p : path (SEdge C) s d) (p' : path (SEdge C) d d') :
      transferPath (concatenate p p') = concatenate (transferPath p) (transferPath p').
      induction p'; t_with t'.
    Qed.
  End transferPath.

  Record SchemaMorphism := {
    VertexOf :> CD;
    PathOf : s d, C.(SEdge) s dpath (SEdge D) (VertexOf s) (VertexOf d);
    TransferPath := (fun s d (p : path (SEdge C) s d) ⇒ transferPath VertexOf PathOf p);
    TEquivalenceOf : s d (p1 p2 : path (SEdge C) s d),
      PathsEquivalent C p1 p2
      → PathsEquivalent D (TransferPath _ _ p1) (TransferPath _ _ p2)
  }.

  Global Add Parametric Morphism s d T :
    (@TransferPath T s d)
    with signature (@PathsEquivalent C _ _) ==> (@PathsEquivalent D _ _)
      as TransferPath_mor.
    exact (@TEquivalenceOf T s d).
  Qed.

  Lemma concatenate_TransferPath s d d' (p : path (SEdge C) s d) (p' : path (SEdge C) d d') T :
      TransferPath T (concatenate p p') = concatenate (TransferPath T p) (TransferPath T p').
    unfold TransferPath; simpl.
    apply concatenate_transferPath.
  Qed.

  Lemma TransferPath_NoEdges x T :
    TransferPath T (@NoEdges _ _ x) = NoEdges.
    reflexivity.
  Qed.
End Schemas.

Hint Rewrite concatenate_transferPath concatenate_TransferPath.

Section SchemaMorphisms_Equal.
  Lemma SchemaMorphism_Eq
  : C D (F G : SchemaMorphism C D),
      ( x, VertexOf F x = VertexOf G x)
      → ( s d m, PathOf F s d m == PathOf G s d m)
      → F = G.
    intros C D F G H H'.
    assert (VertexOf F = VertexOf G) by (apply functional_extensionality_dep; assumption).
    clear H.
    assert (PathOf F == PathOf G);
      destruct F, G;
      subst_body;
      simpl in *;
      repeat subst;
      JMeq_eq;
      repeat (apply functional_extensionality_dep; intro);
      try solve [ apply JMeq_eq; intuition ].
    f_equal.
    apply proof_irrelevance.
  Qed.

  Lemma SchemaMorphism_equal_parts : C D (F G : SchemaMorphism C D),
    F = GVertexOf F = VertexOf G PathOf F == PathOf G.
    intros; repeat subst; split; trivial.
  Qed.
End SchemaMorphisms_Equal.

Section SchemaMorphismComposition.
  Variable B C D E : Schema.

  Hint Resolve concatenate_transferPath.

  Lemma compose_transferPath (vertexOf : CD) pathOf (vertexOf' : DE) pathOf' : s d (p : path (SEdge C) s d),
    (transferPath _ _ (fun c : CvertexOf' (vertexOf c))
      (fun (s0 d0 : C) (e : SEdge C s0 d0) ⇒
        transferPath _ _ vertexOf' pathOf' (pathOf s0 d0 e)) p) =
    transferPath _ _ vertexOf' pathOf' (transferPath _ _ vertexOf pathOf p).
  Proof.
    induction p; reflexivity || symmetry; t_with t'.
  Qed.

  Hint Rewrite compose_transferPath.
  Hint Resolve TEquivalenceOf.

  Definition ComposeSchemaMorphisms (G : SchemaMorphism D E) (F : SchemaMorphism C D) : SchemaMorphism C E.
    refine {| VertexOf := (fun c G (F c));
      PathOf := (fun _ _ e G.(TransferPath) (F.(PathOf) _ _ e))
    |}; abstract (unfold TransferPath; t_with t'; repeat apply TEquivalenceOf; assumption).
  Defined.
End SchemaMorphismComposition.

Implicit Arguments ComposeSchemaMorphisms [C D E].

Section IdentitySchemaMorphsims.
  Variable C D : Schema.

  Definition IdentitySchemaMorphism : SchemaMorphism C C.
    refine {| VertexOf := (fun x x);
      PathOf := (fun _ _ x AddEdge NoEdges x)
    |}; abstract (
      intros ? ? p1 p2 ?;
        transitivity p1;
          try solve [ induction p1; try apply AddEdge_mor; try apply (IHp1 p1); reflexivity ];
            transitivity p2;
              try solve [ induction p2; try apply AddEdge_mor; try apply (IHp2 p2); reflexivity ];
                assumption
    ).
  Defined.

  Hint Unfold ComposeSchemaMorphisms IdentitySchemaMorphism VertexOf PathOf.

  Lemma LeftIdentitySchemaMorphism (F : SchemaMorphism D C) : ComposeSchemaMorphisms IdentitySchemaMorphism F = F.
    apply SchemaMorphism_Eq; try reflexivity; simpl; intros.
    JMeq_eq.
    match goal with
      | [ |- ?a = ?b ] ⇒ induction b; t_with t'
    end.
  Qed.

  Lemma RightIdentitySchemaMorphism (F : SchemaMorphism C D) : ComposeSchemaMorphisms F IdentitySchemaMorphism = F.
    apply SchemaMorphism_Eq; try reflexivity; simpl; intros.
    t_with t'.
  Qed.
End IdentitySchemaMorphsims.

Section SchemaMorphismCompositionLemmas.
  Variable B C D E : Schema.

  Lemma ComposeSchemaMorphismsAssociativity (F : SchemaMorphism B C) (G : SchemaMorphism C D) (H : SchemaMorphism D E) :
    ComposeSchemaMorphisms (ComposeSchemaMorphisms H G) F = ComposeSchemaMorphisms H (ComposeSchemaMorphisms G F).
    unfold ComposeSchemaMorphisms; apply SchemaMorphism_Eq; try reflexivity; simpl; intros.
    JMeq_eq.
    match goal with
      | [ |- TransferPath _ ?p = _ ] ⇒ induction p; t_with t'
    end.
  Qed.
End SchemaMorphismCompositionLemmas.

Section SchemaMorphismsEquivalent.
  Variables C D : Schema.
  Variables F G : SchemaMorphism C D.

  Definition SchemaMorphismsEquivalent :=
     vo po po' eo eo',
      F = {| VertexOf := vo; PathOf := po; TEquivalenceOf := eo |}
      G = {| VertexOf := vo; PathOf := po'; TEquivalenceOf := eo' |}
       s d (e : C.(SEdge) s d), PathsEquivalent _ (po _ _ e) (po' _ _ e).

  Lemma SchemaMorphisms_equivalent :
    ( x, VertexOf F x = VertexOf G x)
    → (VertexOf F = VertexOf G
         s d (e : C.(SEdge) s d), GeneralizedPathsEquivalent _ (PathOf F _ _ e) (PathOf G _ _ e))
    → SchemaMorphismsEquivalent.
    intro H.
    assert (H' : VertexOf F = VertexOf G) by (apply functional_extensionality_dep; assumption);
      clear H;
      revert H'.
    unfold SchemaMorphismsEquivalent;
      destruct F as [ vo po tp eo ], G as [ vo' po' tp' eo' ];
        simpl; intros; subst tp tp'; intuition; repeat subst;
          repeat esplit; f_equal; intros.
    match goal with
      | [ s : _, d : _, e : _, H : _ |- _ ] ⇒ specialize (H s d e); simpl_GeneralizedPathsEquivalent; assumption
    end.
  Qed.
End SchemaMorphismsEquivalent.

Section SchemaMorphismsEquivalent_Relation.
  Variables C D E : Schema.

  Local Ltac t0 :=
    repeat ((apply SchemaMorphisms_equivalent)
              || reflexivity
              || (progress repeat subst)
              || (progress (simpl in *; JMeq_eq; intuition eauto))
              || (progress destruct_hypotheses)
              || intro
              || constructor
              || (match goal with
                    | [ H : _ |- _ ] ⇒ apply SchemaMorphism_equal_parts in H
                  end)
              || (progress split_and)
              || solve [ etransitivity; eauto ]).

  Lemma SchemaMorphismsEquivalent_refl (T : SchemaMorphism C D) : SchemaMorphismsEquivalent T T.
    t0.
  Qed.

  Lemma SchemaMorphismsEquivalent_sym (T U : SchemaMorphism C D) :
    SchemaMorphismsEquivalent T USchemaMorphismsEquivalent U T.
    intro H; destruct H; t0.
    symmetry.
    t0.
  Qed.

  Lemma SchemaMorphismsEquivalent_trans (T U V : SchemaMorphism C D) :
    SchemaMorphismsEquivalent T USchemaMorphismsEquivalent U VSchemaMorphismsEquivalent T V.
    intros H0 H1; destruct H0, H1; t0.
  Qed.

  Hint Resolve TEquivalenceOf.

  Lemma PreComposeSchemaMorphismsEquivalent (T T' : SchemaMorphism C D) (U : SchemaMorphism D E) :
    SchemaMorphismsEquivalent T T'SchemaMorphismsEquivalent (ComposeSchemaMorphisms U T) (ComposeSchemaMorphisms U T').
    intro H; destruct H. t0.
  Qed.

  Hint Resolve concatenate_mor.

  Lemma PostComposeSchemaMorphismsEquivalent (T : SchemaMorphism C D) (U U' : SchemaMorphism D E) :
    SchemaMorphismsEquivalent U U'SchemaMorphismsEquivalent (ComposeSchemaMorphisms U T) (ComposeSchemaMorphisms U' T).
    intro H; destruct H; t0.
    destruct T; unfold TransferPath; t0.
    match goal with
      | [ |- ?Rel (transferPath _ _ _ _ ?p) (transferPath _ _ _ _ ?p) ] ⇒ induction p; simpl; try reflexivity
    end; eauto.
  Qed.
End SchemaMorphismsEquivalent_Relation.

Add Parametric Relation C D : _ (@SchemaMorphismsEquivalent C D)
  reflexivity proved by (@SchemaMorphismsEquivalent_refl _ _)
  symmetry proved by (@SchemaMorphismsEquivalent_sym _ _)
  transitivity proved by (@SchemaMorphismsEquivalent_trans _ _)
    as SchemaMorphismsEquivalent_rel.

Add Parametric Morphism C D E : (@ComposeSchemaMorphisms C D E)
  with signature (@SchemaMorphismsEquivalent _ _) ==> (@SchemaMorphismsEquivalent _ _) ==> (@SchemaMorphismsEquivalent _ _)
    as ComposeSchemaMorphisms_mor.
  intros ? ? H0 ? ? H1.
  etransitivity; try apply PostComposeSchemaMorphismsEquivalent; eauto;
    apply PreComposeSchemaMorphismsEquivalent; eauto.
Qed.