# 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;
).
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.