Library Exercise_4_4_1_5


Require Import Utf8.
Require Import FunctionalExtensionality JMeq EqdepFacts Relation_Definitions.
Require Import Schema SchemaMorphism Path.
Require Import Common Notations FEqualDep.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.4.1.5

Problem

              g
           a ---> b
     C :=   \     |
            i \   | h
                ↘ ↓
                  c

Consider the schema [2] and the schema C pictured above, except where this time we do not impose any path equivalence declarations on C, so [g, h] [i] in our current version of C.
(a) How many schema morphisms are there [2] C that send 0 to a?
(b) How many schema morphisms are there C [2] that send a to 0?

  Inductive C_Vertex := a | b | c.
  Inductive C_Edge : C_VertexC_VertexSet :=
  | g : C_Edge a b
  | h : C_Edge b c
  | i : C_Edge a c.
  Definition C : Schema.
    refine (@Build_Schema C_Vertex
                          C_Edge
                          (fun _ _ ⇒ @eq _)
                          _
                          _
                          _);
    abstract (repeat (intro || split); subst; reflexivity).
  Defined.
  Inductive LinearOrder2Schema_Vertex := Zero | One | Two.
  Inductive LinearOrder2Schema_Edge
  : LinearOrder2Schema_VertexLinearOrder2Schema_VertexSet :=
  | Zero_One : LinearOrder2Schema_Edge Zero One
  | One_Two : LinearOrder2Schema_Edge One Two.
  Definition LinearOrder2Schema : Schema.
    refine (@Build_Schema LinearOrder2Schema_Vertex
                          LinearOrder2Schema_Edge
                          (fun _ _ ⇒ @eq _)
                          _
                          _
                          _);
    abstract (repeat (intro || split); subst; reflexivity).
  Defined.
  Definition SchemaMorphism_template
             (VO : LinearOrder2SchemaC)
             (PO : s d,
                     SEdge LinearOrder2Schema s d
                     → path (SEdge C) (VO s) (VO d))
  : SchemaMorphism LinearOrder2Schema C.
    refine (@Build_SchemaMorphism LinearOrder2Schema C
                                  VO
                                  PO
                                  _).
    abstract (intros; hnf in *; subst; reflexivity).
  Defined.

  Definition SchemaMorphism_template'
             (VO : CLinearOrder2Schema)
             (PO : s d,
                     SEdge C s d
                     → path (SEdge LinearOrder2Schema) (VO s) (VO d))
  : SchemaMorphism C LinearOrder2Schema.
    refine (@Build_SchemaMorphism C LinearOrder2Schema
                                  VO
                                  PO
                                  _).
    abstract (intros; hnf in *; subst; reflexivity).
  Defined.
  Local Ltac paths_unique_t :=
    intros; compute;
    try apply JMeq_eq;
    repeat match goal with
             | [ |- ?a = ?b ?c = ?d ] ⇒
               cut (a == b c == d);
                 [
                   intros [? | ?]; solve [ left; apply JMeq_eq; assumption
                                         | right; apply JMeq_eq; assumption ]
                 | ]
             | [ |- AddEdge _ _ == NoEdges ] ⇒ exfalso
             | [ H : _ |- _ ] ⇒ inversion H; subst;
                                 match goal with
                                   | [ H : _ |- _ ] ⇒ solve [ inversion H ]
                                 end
             | [ H : C_Edge _ _ |- _ ] ⇒ destruct H
             | [ H : LinearOrder2Schema_Edge _ _ |- _ ] ⇒ destruct H
             | _subst; apply eq_JMeq; apply f_equal2; try reflexivity; []; apply JMeq_eq
             | _subst; right; apply eq_JMeq; apply f_equal2; try reflexivity; []; apply JMeq_eq
             | _subst; left; apply eq_JMeq; apply f_equal2; try reflexivity; []; apply JMeq_eq
             | [ p : path ?E ?x ?y |- _ ]
               ⇒ let x' := fresh in
                  let y' := fresh in
                  pose x as x';
                    pose y as y';
                    assert (x = x') by reflexivity;
                    assert (y = y') by reflexivity;
                    change (path E x y) with (path E x' y') in p;
                    repeat match goal with
                             | [ |- context[@JMeq (path E x y) p ?T ?p'] ] ⇒
                               progress (change (@JMeq (path E x y) p T p')
                                         with (@JMeq (path E x' y') p T p'))
                           end;
                    clearbody x' y';
                    destruct p;
                    try (subst; reflexivity)
           end.

  Local Ltac mk_f_x f x fx :=
    let H := fresh in
    pose (f x) as fx; assert (f x = fx) by reflexivity; clearbody fx.
  Local Ltac t_unique_solve :=
    solve [
        apply SchemaMorphism_Eq; simpl;
        intros;
        destruct_head_hnf LinearOrder2Schema_Edge;
        destruct_head_hnf C_Edge;
        try assumption;
        match goal with
          | [ H : _ |- _ ] ⇒ rewrite H; reflexivity
        end
      ].
  Local Ltac t_unique_solve_recr :=
    t_unique_solve || (left; t_unique_solve_recr) || (right; t_unique_solve_recr).

  Section part_a.
    Definition a_OnVertices0 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Onea | Twoa end.
    Definition a_OnVertices1 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Onea | Twob end.
    Definition a_OnVertices2 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Onea | Twoc end.
    Definition a_OnVertices3 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Oneb | Twoa end.
    Definition a_OnVertices4 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Oneb | Twob end.
    Definition a_OnVertices5 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Oneb | Twoc end.
    Definition a_OnVertices6 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Onec | Twoa end.
    Definition a_OnVertices7 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Onec | Twob end.
    Definition a_OnVertices8 : LinearOrder2SchemaC :=
      fun vmatch v with Zeroa | Onec | Twoc end.
    Definition a_path_a_a_0 : path C_Edge a a := NoEdges.
    Definition a_path_b_b_0 : path C_Edge b b := NoEdges.
    Definition a_path_c_c_0 : path C_Edge c c := NoEdges.
    Definition a_path_a_b_0 : path C_Edge a b := AddEdge NoEdges g.
    Definition a_path_b_c_0 : path C_Edge b c := AddEdge NoEdges h.
    Definition a_path_a_c_0 : path C_Edge a c := AddEdge NoEdges i.
    Definition a_path_a_c_1 : path C_Edge a c := AddEdge (AddEdge NoEdges g) h.
    Definition Exercise_4_4_1_5_a_SchemaMorphism0 : SchemaMorphism LinearOrder2Schema C
      := SchemaMorphism_template a_OnVertices0 (fun _ _ ematch e with Zero_Onea_path_a_a_0 | One_Twoa_path_a_a_0 end).
    Definition Exercise_4_4_1_5_a_SchemaMorphism1 : SchemaMorphism LinearOrder2Schema C
      := SchemaMorphism_template a_OnVertices1 (fun _ _ ematch e with Zero_Onea_path_a_a_0 | One_Twoa_path_a_b_0 end).
    Definition Exercise_4_4_1_5_a_SchemaMorphism2 : SchemaMorphism LinearOrder2Schema C
      := SchemaMorphism_template a_OnVertices2 (fun _ _ ematch e with Zero_Onea_path_a_a_0 | One_Twoa_path_a_c_0 end).
    Definition Exercise_4_4_1_5_a_SchemaMorphism3 : SchemaMorphism LinearOrder2Schema C
      := SchemaMorphism_template a_OnVertices2 (fun _ _ ematch e with Zero_Onea_path_a_a_0 | One_Twoa_path_a_c_1 end).
    Definition Exercise_4_4_1_5_a_SchemaMorphism4 : SchemaMorphism LinearOrder2Schema C
      := SchemaMorphism_template a_OnVertices4 (fun _ _ ematch e with Zero_Onea_path_a_b_0 | One_Twoa_path_b_b_0 end).
    Definition Exercise_4_4_1_5_a_SchemaMorphism5 : SchemaMorphism LinearOrder2Schema C
      := SchemaMorphism_template a_OnVertices5 (fun _ _ ematch e with Zero_Onea_path_a_b_0 | One_Twoa_path_b_c_0 end).
    Definition Exercise_4_4_1_5_a_SchemaMorphism6 : SchemaMorphism LinearOrder2Schema C
      := SchemaMorphism_template a_OnVertices8 (fun _ _ ematch e with Zero_Onea_path_a_c_0 | One_Twoa_path_c_c_0 end).
    Definition Exercise_4_4_1_5_a_SchemaMorphism7 : SchemaMorphism LinearOrder2Schema C
      := SchemaMorphism_template a_OnVertices8 (fun _ _ ematch e with Zero_Onea_path_a_c_1 | One_Twoa_path_c_c_0 end).

    Lemma a_path_a_a_only : x : path _ a a, x = a_path_a_a_0. paths_unique_t. Qed.
    Lemma a_path_b_b_only : x : path _ b b, x = a_path_b_b_0. paths_unique_t. Qed.
    Lemma a_path_c_c_only : x : path _ c c, x = a_path_c_c_0. paths_unique_t. Qed.
    Lemma a_path_a_b_only : x : path _ a b, x = a_path_a_b_0. paths_unique_t. Qed.
    Lemma a_path_b_c_only : x : path _ b c, x = a_path_b_c_0. paths_unique_t. Qed.
    Lemma a_path_a_c_only : x : path _ a c, x = a_path_a_c_0 x = a_path_a_c_1. paths_unique_t. Qed.
    Lemma a_path_b_a_only : path C_Edge b aFalse. paths_unique_t. Qed.
    Lemma a_path_c_b_only : path C_Edge c bFalse. paths_unique_t. Qed.
    Lemma a_path_c_a_only : path C_Edge c aFalse. paths_unique_t. Qed.

    Lemma a_OnVertices_only : f : LinearOrder2SchemaC,
                                f Zero = a
                                → f = a_OnVertices0
                                    f = a_OnVertices1
                                    f = a_OnVertices2
                                    f = a_OnVertices3
                                    f = a_OnVertices4
                                    f = a_OnVertices5
                                    f = a_OnVertices6
                                    f = a_OnVertices7
                                    f = a_OnVertices8.
      intros f H.
      mk_f_x f Zero fZero.
      mk_f_x f One fOne.
      mk_f_x f Two fTwo.
      let H := fresh in
      assert (H : f = fun vmatch v with ZerofZero | OnefOne | TwofTwo end)
        by (apply functional_extensionality_dep; intros []; intuition);
        repeat rewrite H; clear H;
        subst fZero;
        match goal with
          | [ H : f Zero = _ |- _ ] ⇒ rewrite H
        end;
        clear;
        compute;
        destruct fOne, fTwo;
        intuition.
    Qed.
    Lemma a_schema_morphism_all_template
    : F : SchemaMorphism LinearOrder2Schema C,
        F = SchemaMorphism_template (VertexOf F) (PathOf F).
      intros.
      apply SchemaMorphism_Eq; simpl;
      reflexivity.
    Qed.

    Lemma a_schema_morphsim_on_paths
          VO
          (PO : s d : LinearOrder2Schema,
                  SEdge LinearOrder2Schema s d path (SEdge C) (VO s) (VO d))
    : PO = (fun _ _ ematch e with Zero_OnePO _ _ Zero_One | One_TwoPO _ _ One_Two end).
      repeat (apply functional_extensionality_dep; intro).
      match goal with | [ |- context[match ?E with __ end] ] ⇒ destruct E end;
        reflexivity.
    Qed.
    Local Ltac pose_path_uniqueness_proof p :=
      ((pose proof (a_path_a_a_only p))
         || (pose proof (a_path_a_b_only p))
         || (pose proof (a_path_a_c_only p))
         || (pose proof (a_path_b_a_only p))
         || (pose proof (a_path_b_b_only p))
         || (pose proof (a_path_b_c_only p))
         || (pose proof (a_path_c_a_only p))
         || (pose proof (a_path_c_b_only p))
         || (pose proof (a_path_c_c_only p))).
    Theorem a_schema_morphism_all
    : F : SchemaMorphism LinearOrder2Schema C,
        F Zero = a
        → F = Exercise_4_4_1_5_a_SchemaMorphism0
            F = Exercise_4_4_1_5_a_SchemaMorphism1
            F = Exercise_4_4_1_5_a_SchemaMorphism2
            F = Exercise_4_4_1_5_a_SchemaMorphism3
            F = Exercise_4_4_1_5_a_SchemaMorphism4
            F = Exercise_4_4_1_5_a_SchemaMorphism5
            F = Exercise_4_4_1_5_a_SchemaMorphism6
            F = Exercise_4_4_1_5_a_SchemaMorphism7.
      intros F H.
      rewrite (a_schema_morphism_all_template F).
      rewrite (@a_schema_morphsim_on_paths _ (PathOf F)).
      destruct (a_OnVertices_only F H); clear H;
      destruct_head_hnf @or;
      match goal with
        | [ H : VertexOf ?F = ?G |- _ ]
          ⇒ let p01 := fresh in
             let H01 := fresh in
             let p12 := fresh in
             let H12 := fresh in
             let f0 := fresh in
             let f1 := fresh in
             let f2 := fresh in
             let fH0 := fresh in
             let fH1 := fresh in
             let fH2 := fresh in
             pose (VertexOf F Zero) as f0;
               pose (VertexOf F One) as f1;
               pose (VertexOf F Two) as f2;
               assert (fH0 : VertexOf F Zero = f0) by reflexivity;
               assert (fH1 : VertexOf F One = f1) by reflexivity;
               assert (fH2 : VertexOf F Two = f2) by reflexivity;
               pose (PathOf F _ _ Zero_One : path _ f0 f1) as p01;
               pose (PathOf F _ _ One_Two : path _ f1 f2) as p12;
               assert (H01 : PathOf F _ _ Zero_One == p01) by reflexivity;
               assert (H12 : PathOf F _ _ One_Two == p12) by reflexivity;
               clearbody p01 p12 f0 f1 f2;
               rewrite H in fH0, fH1, fH2;
               subst; simpl in *;
               pose_path_uniqueness_proof p01;
               pose_path_uniqueness_proof p12
      end;
      destruct_head_hnf False;
      destruct_head_hnf @or;
      subst;
      t_unique_solve_recr.
    Qed.
  End part_a.

  Section part_b.
    Definition b_OnVertices0 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bZero | cZero end.
    Definition b_OnVertices1 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bZero | cOne end.
    Definition b_OnVertices2 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bZero | cTwo end.
    Definition b_OnVertices3 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bOne | cZero end.
    Definition b_OnVertices4 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bOne | cOne end.
    Definition b_OnVertices5 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bOne | cTwo end.
    Definition b_OnVertices6 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bTwo | cZero end.
    Definition b_OnVertices7 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bTwo | cOne end.
    Definition b_OnVertices8 : CLinearOrder2Schema :=
      fun vmatch v with aZero | bTwo | cTwo end.
    Definition b_path_0_0 : path LinearOrder2Schema_Edge Zero Zero := NoEdges.
    Definition b_path_1_1 : path LinearOrder2Schema_Edge One One := NoEdges.
    Definition b_path_2_2 : path LinearOrder2Schema_Edge Two Two := NoEdges.
    Definition b_path_0_1 : path LinearOrder2Schema_Edge Zero One := AddEdge NoEdges Zero_One.
    Definition b_path_1_2 : path LinearOrder2Schema_Edge One Two := AddEdge NoEdges One_Two.
    Definition b_path_0_2 : path LinearOrder2Schema_Edge Zero Two := AddEdge (AddEdge NoEdges Zero_One) One_Two.
    Definition Exercise_4_4_1_5_b_SchemaMorphism0 : SchemaMorphism C LinearOrder2Schema
      := SchemaMorphism_template' b_OnVertices0 (fun _ _ ematch e with gb_path_0_0 | hb_path_0_0 | ib_path_0_0 end).
    Definition Exercise_4_4_1_5_b_SchemaMorphism1 : SchemaMorphism C LinearOrder2Schema
      := SchemaMorphism_template' b_OnVertices1 (fun _ _ ematch e with gb_path_0_0 | hb_path_0_1 | ib_path_0_1 end).
    Definition Exercise_4_4_1_5_b_SchemaMorphism2 : SchemaMorphism C LinearOrder2Schema
      := SchemaMorphism_template' b_OnVertices2 (fun _ _ ematch e with gb_path_0_0 | hb_path_0_2 | ib_path_0_2 end).
    Definition Exercise_4_4_1_5_b_SchemaMorphism3 : SchemaMorphism C LinearOrder2Schema
      := SchemaMorphism_template' b_OnVertices4 (fun _ _ ematch e with gb_path_0_1 | hb_path_1_1 | ib_path_0_1 end).
    Definition Exercise_4_4_1_5_b_SchemaMorphism4 : SchemaMorphism C LinearOrder2Schema
      := SchemaMorphism_template' b_OnVertices5 (fun _ _ ematch e with gb_path_0_1 | hb_path_1_2 | ib_path_0_2 end).
    Definition Exercise_4_4_1_5_b_SchemaMorphism5 : SchemaMorphism C LinearOrder2Schema
      := SchemaMorphism_template' b_OnVertices8 (fun _ _ ematch e with gb_path_0_2 | hb_path_2_2 | ib_path_0_2 end).

    Lemma b_path_0_0_only : x : path _ Zero Zero, x = b_path_0_0. paths_unique_t. Qed.
    Lemma b_path_1_1_only : x : path _ One One, x = b_path_1_1. paths_unique_t. Qed.
    Lemma b_path_2_2_only : x : path _ Two Two, x = b_path_2_2. paths_unique_t. Qed.
    Lemma b_path_0_1_only : x : path _ Zero One, x = b_path_0_1. paths_unique_t. Qed.
    Lemma b_path_1_2_only : x : path _ One Two, x = b_path_1_2. paths_unique_t. Qed.
    Lemma b_path_0_2_only : x : path _ Zero Two, x = b_path_0_2. paths_unique_t. Qed.
    Lemma b_path_1_0_only : path LinearOrder2Schema_Edge One ZeroFalse. paths_unique_t. Qed.
    Lemma b_path_2_1_only : path LinearOrder2Schema_Edge Two OneFalse. paths_unique_t. Qed.
    Lemma b_path_2_0_only : path LinearOrder2Schema_Edge Two ZeroFalse. paths_unique_t. Qed.

    Lemma b_OnVertices_only : f : CLinearOrder2Schema,
                                f a = Zero
                                → f = b_OnVertices0
                                    f = b_OnVertices1
                                    f = b_OnVertices2
                                    f = b_OnVertices3
                                    f = b_OnVertices4
                                    f = b_OnVertices5
                                    f = b_OnVertices6
                                    f = b_OnVertices7
                                    f = b_OnVertices8.
      intros f H.
      mk_f_x f a fa.
      mk_f_x f b fb.
      mk_f_x f c fc.
      let H := fresh in
      assert (H : f = fun vmatch v with afa | bfb | cfc end)
        by (apply functional_extensionality_dep; intros []; intuition);
        repeat rewrite H; clear H;
        subst fa;
        match goal with
          | [ H : f a = _ |- _ ] ⇒ rewrite H
        end;
        clear;
        compute;
        destruct fb, fc;
        intuition.
    Qed.
    Lemma b_schema_morphism_all_template'
    : F : SchemaMorphism C LinearOrder2Schema,
        F = SchemaMorphism_template' (VertexOf F) (PathOf F).
      intros.
      apply SchemaMorphism_Eq; simpl;
      reflexivity.
    Qed.

    Lemma b_schema_morphsim_on_paths
          VO
          (PO : s d : C,
                  SEdge C s d path (SEdge LinearOrder2Schema) (VO s) (VO d))
    : PO = (fun _ _ ematch e with gPO _ _ g | hPO _ _ h | iPO _ _ i end).
      repeat (apply functional_extensionality_dep; intro).
      match goal with | [ |- context[match ?E with __ end] ] ⇒ destruct E end;
        reflexivity.
    Qed.
    Local Ltac pose_path_uniqueness_proof p :=
      ((pose proof (b_path_0_0_only p))
         || (pose proof (b_path_0_1_only p))
         || (pose proof (b_path_0_2_only p))
         || (pose proof (b_path_1_0_only p))
         || (pose proof (b_path_1_1_only p))
         || (pose proof (b_path_1_2_only p))
         || (pose proof (b_path_2_0_only p))
         || (pose proof (b_path_2_1_only p))
         || (pose proof (b_path_2_2_only p))).
    Theorem b_schema_morphism_all
    : F : SchemaMorphism C LinearOrder2Schema,
        F a = Zero
        → F = Exercise_4_4_1_5_b_SchemaMorphism0
            F = Exercise_4_4_1_5_b_SchemaMorphism1
            F = Exercise_4_4_1_5_b_SchemaMorphism2
            F = Exercise_4_4_1_5_b_SchemaMorphism3
            F = Exercise_4_4_1_5_b_SchemaMorphism4
            F = Exercise_4_4_1_5_b_SchemaMorphism5.
      intros F H.
      rewrite (b_schema_morphism_all_template' F).
      rewrite (@b_schema_morphsim_on_paths _ (PathOf F)).
      destruct (b_OnVertices_only F H); clear H;
      destruct_head_hnf @or;
      match goal with
        | [ H : VertexOf ?F = ?G |- _ ]
          ⇒ let pab := fresh in
             let Hab := fresh in
             let pbc := fresh in
             let Hbc := fresh in
             let pac := fresh in
             let Hac := fresh in
             let fa := fresh in
             let fb := fresh in
             let fc := fresh in
             let fHa := fresh in
             let fHb := fresh in
             let fHc := fresh in
             pose (VertexOf F a) as fa;
               pose (VertexOf F b) as fb;
               pose (VertexOf F c) as fc;
               assert (fHa : VertexOf F a = fa) by reflexivity;
               assert (fHb : VertexOf F b = fb) by reflexivity;
               assert (fHc : VertexOf F c = fc) by reflexivity;
               pose (PathOf F _ _ g : path _ fa fb) as pab;
               pose (PathOf F _ _ h : path _ fb fc) as pbc;
               pose (PathOf F _ _ i : path _ fa fc) as pac;
               assert (Hab : PathOf F _ _ g == pab) by reflexivity;
               assert (Hbc : PathOf F _ _ h == pbc) by reflexivity;
               assert (Hac : PathOf F _ _ i == pac) by reflexivity;
               clearbody pab pbc pac fa fb fc;
               rewrite H in fHa, fHb, fHc;
               subst; simpl in *;
               pose_path_uniqueness_proof pab;
               pose_path_uniqueness_proof pbc;
               pose_path_uniqueness_proof pac
      end;
      destruct_head_hnf False;
      destruct_head_hnf @or;
      subst;
      t_unique_solve_recr.
    Qed.
  End part_b.
End Exercise_4_4_1_5.