Library Exercise_4_4_1_6


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

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.4.1.6

Problem

Consider the graph Loop pictured below
                  __
                 /   ↘
     Loop :=  f |     s
                 \___/

and for any natural number n, let L_n denote the schema (Loop, _n) where _n is the PED f^{n+1} f^n. This is the "finite hierarchy" schema of Example 3.5.2.11. Let 1 denote the graph with one vertex and no arrows; consider it as a schema.
(a) Is 1 isomorphic to L_1 in Sch?
(b) Is it isomorphic to any (other) L_n?

  Inductive Loop_Vertex := s.
  Inductive Loop_Edge : Loop_VertexLoop_VertexSet := f : Loop_Edge s s.

  Fixpoint count_edges x y (p : path Loop_Edge x y) :
    := match p with
         | NoEdges ⇒ 0
         | AddEdge _ _ p e ⇒ 1 + (count_edges p)
       end.

  Lemma count_edges_prepend x y z (e : Loop_Edge x y) (p : path Loop_Edge y z)
  : count_edges (prepend p e) = 1 + count_edges p.
    induction p; simpl in *; intuition.
  Qed.

  Lemma count_edges_concatenate x y z (p1 : path Loop_Edge x y) (p2 : path Loop_Edge y z)
  : count_edges (concatenate p1 p2) = count_edges p2 + count_edges p1.
    revert x p1.
    induction p2; simpl in *; intuition.
  Qed.
  Definition Loop_Equiv (n : ) x y
  : Relation_Definitions.relation (path Loop_Edge x y)
    := fun p qcount_edges p = count_edges q
                   (count_edges p n count_edges q n).

  Local Notation "x ≃_ n y" := (@Loop_Equiv n x y) (at level 70).

  Hint Extern 1 ⇒ etransitivity; (eassumption || (symmetry; eassumption)).
  Definition L (n : ) : Schema.
    refine {| SVertex := Loop_Vertex;
              SEdge := Loop_Edge;
              PathsEquivalent := (@Loop_Equiv n) |};
    abstract (
        repeat (intro || split);
        hnf in *;
          repeat match goal with
                   | _progress simpl in ×
                   | _progress rewrite count_edges_prepend
                   | [ H0 : _, H1 : _ |- _ ] ⇒ progress rewrite H0 in H1
                   | [ H : _ |- _ ] ⇒ progress rewrite H
                   | _progress intuition eauto
                 end
      ).
  Defined.
  Definition SingletonSchema : Schema.
    refine {| SVertex := unit;
              SEdge := (fun _ _ ∅);
              PathsEquivalent := (fun _ _ @eq _) |};
    abstract (repeat (esplit || intro); intuition eauto).
  Defined.
  Definition L0_to_singleton : SchemaMorphism (L 0) SingletonSchema.
    refine (@Build_SchemaMorphism (L 0) SingletonSchema
                                  (fun _tt)
                                  (fun _ _ _NoEdges)
                                  _).
    abstract (
        intros;
        simpl;
        apply JMeq_eq;
        match goal with
          | [ |- ?a == ?b ] ⇒ let a' := fresh in
                               let b' := fresh in
                               set (a' := a); set (b' := b);
          simpl in *;
            try destruct a';
          try destruct b'
        end;
        try reflexivity;
        destruct_head_hnf
      ).
  Defined.

  Definition singleton_to_L0 : SchemaMorphism SingletonSchema (L 0).
    refine (@Build_SchemaMorphism SingletonSchema (L 0)
                                  (fun _s)
                                  (fun _ _ _NoEdges)
                                  _).
    abstract (
        intros;
        hnf in *;
          subst;
        intuition
      ).
  Defined.
  Lemma singleton_to_L0_to_singleton_id
  : ComposeSchemaMorphisms L0_to_singleton singleton_to_L0
    = IdentitySchemaMorphism _.
    apply SchemaMorphism_Eq;
    repeat intros [].
    reflexivity.
  Qed.
  Lemma L0_to_singleton_to_L0_id
  : SchemaMorphismsEquivalent (ComposeSchemaMorphisms singleton_to_L0 L0_to_singleton)
                              (IdentitySchemaMorphism _).
    apply SchemaMorphisms_equivalent;
    repeat (intros [] || intro);
    repeat (right || constructor).
  Qed.
 End Exercise_4_4_1_6.