Library Exercise_3_5_2_4

Require Import Utf8.
Require Import Notations.

Set Implicit Arguments.

Generalizable All Variables.



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
[Employee manager manager worksIn Employee worksIn?]
What about
[Employee worksIn secretary Employee?]
What about
[Department 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.

  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 | ]
    rewrite Rule1.
    rewrite Rule2.
    rewrite LeftIdentity.
End Exercise_3_5_2_4.