# Library Exercise_3_5_2_4

## Problem

Consider the graph shown in (3.14), and the two declarations shown at the top. They generate a CPER. Is it true that under this CPER we have
Local Infix "≃" := eq (at level 70, right associativity).

Inductive Node := Employee | Department | FirstNameString

| LastNameString | DepartmentNameString.

Inductive Arrow : Node → Node → Type :=

| identity : ∀ {x}, Arrow x x

| compose : ∀ {s d d'}, Arrow s d → Arrow d d' → Arrow s d'

| manager : Arrow Employee Employee

| firstName : Arrow Employee FirstNameString

| lastName : Arrow Employee LastNameString

| worksIn : Arrow Employee Department

| secretary : Arrow Department Employee

| name : Arrow Department DepartmentNameString.

Local Infix "○" := compose.

Axiom Rule1 : manager ○ worksIn ≃ worksIn.

Axiom Rule2 : secretary ○ worksIn ≃ identity.

Axiom LeftIdentity : ∀ s d (m : Arrow s d), identity ○ m ≃ m.

Axiom RightIdentity : ∀ s d (m : Arrow s d), m ○ identity ≃ m.

Axiom Associativity : ∀ a b c d

(m1 : Arrow a b)

(m2 : Arrow b c)

(m3 : Arrow c d),

(m1 ○ m2) ○ m3 ≃ m1 ○ (m2 ○ m3).

Lemma Exercise_3_5_2_4_a : manager ○ manager ○ worksIn ≃ worksIn.

rewrite Associativity.

repeat rewrite Rule1.

reflexivity.

Qed.

Lemma Exercise_3_5_2_4_c : secretary ○ manager ○ worksIn ○ name ≃ name.

match goal with

| [ |- ?a ○ ?b ○ ?c ○ ?d ≃ _ ] ⇒ transitivity (a ○ (b ○ c) ○ d);

[ repeat rewrite Associativity;

reflexivity | ]

end.

rewrite Rule1.

rewrite Rule2.

rewrite LeftIdentity.

reflexivity.

Qed.

End Exercise_3_5_2_4.

Inductive Node := Employee | Department | FirstNameString

| LastNameString | DepartmentNameString.

Inductive Arrow : Node → Node → Type :=

| identity : ∀ {x}, Arrow x x

| compose : ∀ {s d d'}, Arrow s d → Arrow d d' → Arrow s d'

| manager : Arrow Employee Employee

| firstName : Arrow Employee FirstNameString

| lastName : Arrow Employee LastNameString

| worksIn : Arrow Employee Department

| secretary : Arrow Department Employee

| name : Arrow Department DepartmentNameString.

Local Infix "○" := compose.

Axiom Rule1 : manager ○ worksIn ≃ worksIn.

Axiom Rule2 : secretary ○ worksIn ≃ identity.

Axiom LeftIdentity : ∀ s d (m : Arrow s d), identity ○ m ≃ m.

Axiom RightIdentity : ∀ s d (m : Arrow s d), m ○ identity ≃ m.

Axiom Associativity : ∀ a b c d

(m1 : Arrow a b)

(m2 : Arrow b c)

(m3 : Arrow c d),

(m1 ○ m2) ○ m3 ≃ m1 ○ (m2 ○ m3).

Lemma Exercise_3_5_2_4_a : manager ○ manager ○ worksIn ≃ worksIn.

rewrite Associativity.

repeat rewrite Rule1.

reflexivity.

Qed.

Lemma Exercise_3_5_2_4_c : secretary ○ manager ○ worksIn ○ name ≃ name.

match goal with

| [ |- ?a ○ ?b ○ ?c ○ ?d ≃ _ ] ⇒ transitivity (a ○ (b ○ c) ○ d);

[ repeat rewrite Associativity;

reflexivity | ]

end.

rewrite Rule1.

rewrite Rule2.

rewrite LeftIdentity.

reflexivity.

Qed.

End Exercise_3_5_2_4.