A stab at reified type classes

partial-typeclasses.v

Require Import Notations Common SpecializedCategory Functor NaturalTransformation.

Set Implicit Arguments.

Generalizable All Variables.

Section SimplifiedMorphism.
  Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
  | ReifiedIdentityMorphism : forall objC C x, @ReifiedMorphism objC C x x
  | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'
  | ReifiedNaturalTransformationMorphism : forall objB (B : SpecializedCategory objB)
                                                  objC (C : SpecializedCategory objC)
                                                  (F G : SpecializedFunctor B C)
                                                  (T : SpecializedNaturalTransformation F G)
                                                  x,
                                             ReifiedMorphism C (F x) (G x)
  | ReifiedFunctorMorphism : forall objB (B : SpecializedCategory objB)
                                    objC (C : SpecializedCategory objC)
                                    (F : SpecializedFunctor B C)
                                    s d,
                               @ReifiedMorphism objB B s d -> @ReifiedMorphism objC C (F s) (F d)
  | ReifiedGenericMorphism : forall objC (C : SpecializedCategory objC) s d, Morphism C s d -> @ReifiedMorphism objC C s d.

  Fixpoint ReifiedMorphismSimplify objC C s d (m : @ReifiedMorphism objC C s d) : ReifiedMorphism C s d
    := match
        m in (ReifiedMorphism C s d) return (ReifiedMorphism C s d)
      with
        | ReifiedComposedMorphism _ _ _ _ _ m1 m2 =>
          match
            ReifiedMorphismSimplify m1
            in (ReifiedMorphism C d d')
            return
            (forall s,
               ReifiedMorphism C s d -> ReifiedMorphism C s d')
          with
            | ReifiedIdentityMorphism _ _ _ => fun _ m2' => m2'
            | m1' => fun _ m2' => match m2'
                                        in (ReifiedMorphism C s d)
                                        return (forall d',
                                                  ReifiedMorphism C d d' -> ReifiedMorphism C s d')
                                  with
                                    | ReifiedIdentityMorphism _ _ _ => fun _ m1'' => m1''
                                    | m2'' => fun _ m1'' => ReifiedComposedMorphism m1'' m2''
                                  end _ m1'
          end _ (ReifiedMorphismSimplify m2)
        | ReifiedFunctorMorphism objB B objC0 C0 F s0 d0 m0 =>
          match
            ReifiedMorphismSimplify m0
            in (ReifiedMorphism C1 o o0)
            return
            (forall F0 : SpecializedFunctor C1 C0,
               ReifiedMorphism C0 (F0 o) (F0 o0))
          with
            | ReifiedIdentityMorphism _ _ x =>
              fun F0 => ReifiedIdentityMorphism _ (F0 x)
            | ReifiedComposedMorphism _ _ _ _ _ m11 m12 =>
              fun F0 =>
                ReifiedComposedMorphism (ReifiedFunctorMorphism F0 m11)
                                        (ReifiedFunctorMorphism F0 m12)
            | m' =>
              fun F0 =>
                ReifiedFunctorMorphism F0 m'
          end F
        | m' => m'
  end.

  Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d :=
    match m in @ReifiedMorphism objC C s d return Morphism C s d with
      | ReifiedIdentityMorphism _ _ x => Identity x
      | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
                                                           (@ReifiedMorphismDenote _ _ _ _ m2)
      | ReifiedNaturalTransformationMorphism _ _ _ _ _ _ T x => T x
      | ReifiedFunctorMorphism _ _ _ _ F _ _ m => MorphismOf F (@ReifiedMorphismDenote _ _ _ _ m)
      | ReifiedGenericMorphism _ _ _ _ m => m
    end.

(*  Fixpoint ReifiedMorphismSimplify' objC C s d (m : @ReifiedMorphism objC C s d)
  : { sm : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote sm }.
  refine (match m
                as r
                in (ReifiedMorphism C s d)
                return { sm : ReifiedMorphism C s d | ReifiedMorphismDenote r = ReifiedMorphismDenote sm }
          with
            | ReifiedComposedMorphism _ _ _ _ _ m1 m2 =>
              let (m1', H1) := ReifiedMorphismSimplify' _ _ _ _ m1 in
              match
                m1' as r in (ReifiedMorphism C1 o o0)
                return
                (forall (s2 : C1) (m3 : ReifiedMorphism C1 o o0)
                        (m4 : ReifiedMorphism C1 s2 o),
                   ReifiedMorphismDenote m3 = ReifiedMorphismDenote r ->
                   {sm : ReifiedMorphism C1 s2 o0 |
                    ReifiedMorphismDenote (ReifiedComposedMorphism m3 m4) =
                    ReifiedMorphismDenote sm})
              with
                | ReifiedIdentityMorphism objC1 C1 x =>
                  fun _ _ m2' _ =>
                    exist _ m2' _
                | m1'' => fun _ m1''' m2''' H1 => _
              end _ m1 m2 H1
            | ReifiedFunctorMorphism objB B objC C F s0 d0 m0 =>
              let (m0', H) := ReifiedMorphismSimplify' _ _ _ _ m0 in
              match
                m0' as r in (ReifiedMorphism B o o0)
                return
                (forall (F0 : SpecializedFunctor B C)
                        (m1 : ReifiedMorphism B o o0),
                   ReifiedMorphismDenote m1 = ReifiedMorphismDenote r ->
                   {sm : ReifiedMorphism C (F0 o) (F0 o0) |
                    ReifiedMorphismDenote (ReifiedFunctorMorphism F0 m1) =
                    ReifiedMorphismDenote sm})
              with
                | ReifiedIdentityMorphism objC1 C1 x =>
                  fun _ _ _ => exist _ (ReifiedIdentityMorphism _ _) _
                | ReifiedComposedMorphism objC1 C1 s2 d1 d' m0'1 m0'2 =>
                  fun F0 _ _ => exist _ (ReifiedComposedMorphism (ReifiedFunctorMorphism F0 m0'1)
                                                                 (ReifiedFunctorMorphism F0 m0'2)) _
                | m0'' =>
                  fun _ _ _ => exist _ (ReifiedFunctorMorphism _ m0'') _
              end F m0 H
            | m' => exist _ m' eq_refl
          end);
    try abstract (
          simpl;
          repeat match goal with
                   | [ H : _ |- _ ] => rewrite H
                 end;
          simpl;
          repeat rewrite FCompositionOf;
          repeat rewrite Associativity;
          autorewrite with category;
          try reflexivity
        ).
  destruct (ReifiedMorphismSimplify'  _ _ _ _ m2''') as [ m2'''' H2'''' ].
  destruct m2''''.
  exists m1'''.
  simpl.
  Show Proof.

  exists (Reified
  destruct (ReifiedMorphismSimplify' _ _ _ _ m0) as [ m0' H ].
  destruct m0'.
  Show Proof.
    := match
        m in (ReifiedMorphism C s d) return (ReifiedMorphism C s d)
      with
        | ReifiedComposedMorphism _ _ _ _ _ m1 m2 =>
          match
            ReifiedMorphismSimplify m1
            in (ReifiedMorphism C d d')
            return
            (forall s,
               ReifiedMorphism C s d -> ReifiedMorphism C s d')
          with
            | ReifiedIdentityMorphism _ _ _ => fun _ m2' => m2'
            | m1' => fun _ m2' => match m2'
                                        in (ReifiedMorphism C s d)
                                        return (forall d',
                                                  ReifiedMorphism C d d' -> ReifiedMorphism C s d')
                                  with
                                    | ReifiedIdentityMorphism _ _ _ => fun _ m1'' => m1''
                                    | m2'' => fun _ m1'' => ReifiedComposedMorphism m1'' m2''
                                  end _ m1'
          end _ (ReifiedMorphismSimplify m2)
        | ReifiedFunctorMorphism objB B objC0 C0 F s0 d0 m0 =>
          match
            ReifiedMorphismSimplify m0
            in (ReifiedMorphism C1 o o0)
            return
            (forall F0 : SpecializedFunctor C1 C0,
               ReifiedMorphism C0 (F0 o) (F0 o0))
          with
            | ReifiedIdentityMorphism _ _ x =>
              fun F0 => ReifiedIdentityMorphism _ (F0 x)
            | ReifiedComposedMorphism _ _ _ _ _ m11 m12 =>
              fun F0 =>
                ReifiedComposedMorphism (ReifiedFunctorMorphism F0 m11)
                                        (ReifiedFunctorMorphism F0 m12)
            | m' =>
              fun F0 =>
                ReifiedFunctorMorphism F0 m'
          end F
        | m' => m'
  end.
*)
  Lemma ReifiedMorphismSimplifyOk objC C s d (m : @ReifiedMorphism objC C s d)
  : ReifiedMorphismDenote m =
    ReifiedMorphismDenote (ReifiedMorphismSimplify m).
    induction m; simpl; try reflexivity.
    rewrite IHm1; rewrite IHm2; clear IHm1 IHm2.
    Focus 2.
    rewrite IHm; clear IHm;
    simpl.
    set (H := ReifiedMorphismSimplify m) in *; clearbody H.
    destruct H;
      simpl;
      repeat rewrite Associativity;
      repeat rewrite FCompositionOf;
      autorewrite with category;
      try reflexivity.
    set (H1 := (ReifiedMorphismSimplify m1)) in *;
      set (H2 := (ReifiedMorphismSimplify m2)) in *;
      clearbody H1 H2.
    clear m1 m2.
    destruct H1; simpl;
    try (destruct H2; simpl; repeat rewrite Associativity; repeat rewrite FCompositionOf; autorewrite with category; try reflexivity).
    Focus 2.
    repeat match goal with | [ H : _ |- _ ] => clear H end.
    set (FH := (ReifiedFunctorMorphism F H1)).

    revert H1.
    revert d.

    destruct H2; simpl;
    try (destruct H1; simpl; repeat rewrite Associativity; repeat rewrite FCompositionOf; autorewrite with category; try reflexivity).
    set (A := (ReifiedNaturalTransformationMorphism T x)).
    set (y := (G x)) in *.

    destruct H1; simpl; repeat rewrite Associativity; repeat rewrite FCompositionOf; autorewrite with category; try reflexivity.
    destruct H1; simpl; repeat rewrite Associativity; repeat rewrite FCompositionOf; autorewrite with category; try reflexivity.
      try destruct H2;
      simpl;
      repeat rewrite Associativity;
      repeat rewrite FCompositionOf;
      autorewrite with category;
      try reflexivity.
    destruct H2.
    repeat match goal with
             | [ H : ReifiedMorphismDenote _ = _ |- _ ] => progress repeat rewrite H; clear H
             | [ |- context[ReifiedMorphismSimplify ?m1] ] =>
               let H := fresh in
               set (H := ReifiedMorphismSimplify m1) in *
             | [ H := _ : ReifiedMorphism _ _ _ |- _ ] => clearbody H;
                                                         destruct H;
                                                         simpl;
                                                         repeat rewrite Associativity;
                                                         repeat rewrite FCompositionOf;
                                                         autorewrite with category;
                                                         try reflexivity
             | [ H : _ |- _ ] => clear H
           end.
    Focus 2.
    destruct H0;
      simpl;
      repeat rewrite Associativity;
      repeat rewrite FCompositionOf;
      autorewrite with category;
      try reflexivity.
    match goal with
      | [ |- context[match _ with _ => _ end ?a ?b] ] => pattern b
    end.
    pattern
    destruct H0;                                                         simpl;
                                                         repeat rewrite Associativity;
                                                         repeat rewrite FCompositionOf;
                                                         autorewrite with category;
                                                         try reflexivity.
    f_equal.

    etransitivity; try destruct H.
    destruct H0
    destruct H.
    destruct
    repeat match goal with
             | [ H : ReifiedMorphismDenote _ = _ |- _ ] => rewrite H
             | [ |- context[ReifiedMorphismSimplify ?m1] ] =>
               let H := fresh in
               set (H := ReifiedMorphismSimplify m1) in *;
                 clearbody H;
                 try destruct H
             | [ H : _ |- _ ] => clear H
           end.
    Focus 2.
    destruct H; simpl;
                 simpl;
                 repeat rewrite Associativity;
                 repeat rewrite FCompositionOf;
                 autorewrite with category;
                 try reflexivity.
    apply f_equal.
    Focus.
    set (Fx := (ReifiedFunctorMorphism F (ReifiedIdentityMorphism C0 x))) in *.
    let Fx' := (eval simpl in (ReifiedMorphismDenote Fx)) in
    assert (ReifiedMorphismDenote Fx = Fx') by reflexivity;
      clearbody Fx;
      autorewrite with category in *; present_spfunctor.
    set (y := F x) in *.
    clearbody y.

    pose Fx'.
    assert (
    destruct H0.
    Require Import FEqualDep JMeq.
    apply JMeq_eq.
    simpl.
    clear m1.
    clear m2.

    admit.
    admit.
    admit.
    admit.
    admit.
    admit.
  Defined.
    destruct H0.
    destruct H0.
    destruct H0.
    simpl.
    destruct H.
  Qed.