# Library Exercise_3_5_2_4

Require Import Utf8.
Require Import Notations.

Set Implicit Arguments.

Generalizable All Variables.

# 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
manager manager worksIn Employee worksIn?]
worksIn secretary Employee?]
secretary manager worksIn name Department name?]
Local Infix "≃" := eq (at level 70, right associativity).

Inductive Node := Employee | Department | FirstNameString
| LastNameString | DepartmentNameString.

Inductive Arrow : NodeNodeType :=
| identity : {x}, Arrow x x
| compose : {s d d'}, Arrow s dArrow 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.