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
[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.
    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.