Library Exercise_4_4_1_5

Require Import Utf8.
Require Import FunctionalExtensionality JMeq EqdepFacts Relation_Definitions.
Require Import Schema SchemaMorphism Path.
Require Import Common Notations FEqualDep.

Set Implicit Arguments.

Generalizable All Variables.

Exercise 4.4.1.5

Problem

```              g
a ---> b
C :=   \     |
i \   | h
↘ ↓
c

```
Consider the schema [2] and the schema C pictured above, except where this time we do not impose any path equivalence declarations on C, so [g, h] [i] in our current version of C.
(a) How many schema morphisms are there [2] C that send 0 to a?
(b) How many schema morphisms are there C [2] that send a to 0?

Inductive C_Vertex := a | b | c.
Inductive C_Edge : C_VertexC_VertexSet :=
| g : C_Edge a b
| h : C_Edge b c
| i : C_Edge a c.
Definition C : Schema.
refine (@Build_Schema C_Vertex
C_Edge
(fun _ _ ⇒ @eq _)
_
_
_);
abstract (repeat (intro || split); subst; reflexivity).
Defined.
Inductive LinearOrder2Schema_Vertex := Zero | One | Two.
Inductive LinearOrder2Schema_Edge
: LinearOrder2Schema_VertexLinearOrder2Schema_VertexSet :=
| Zero_One : LinearOrder2Schema_Edge Zero One
| One_Two : LinearOrder2Schema_Edge One Two.
Definition LinearOrder2Schema : Schema.
refine (@Build_Schema LinearOrder2Schema_Vertex
LinearOrder2Schema_Edge
(fun _ _ ⇒ @eq _)
_
_
_);
abstract (repeat (intro || split); subst; reflexivity).
Defined.
Definition SchemaMorphism_template
(VO : LinearOrder2SchemaC)
(PO : s d,
SEdge LinearOrder2Schema s d
→ path (SEdge C) (VO s) (VO d))
: SchemaMorphism LinearOrder2Schema C.
refine (@Build_SchemaMorphism LinearOrder2Schema C
VO
PO
_).
abstract (intros; hnf in *; subst; reflexivity).
Defined.

Definition SchemaMorphism_template'
(VO : CLinearOrder2Schema)
(PO : s d,
SEdge C s d
→ path (SEdge LinearOrder2Schema) (VO s) (VO d))
: SchemaMorphism C LinearOrder2Schema.
refine (@Build_SchemaMorphism C LinearOrder2Schema
VO
PO
_).
abstract (intros; hnf in *; subst; reflexivity).
Defined.
Local Ltac paths_unique_t :=
intros; compute;
try apply JMeq_eq;
repeat match goal with
| [ |- ?a = ?b ?c = ?d ] ⇒
cut (a == b c == d);
[
intros [? | ?]; solve [ left; apply JMeq_eq; assumption
| right; apply JMeq_eq; assumption ]
| ]
| [ |- AddEdge _ _ == NoEdges ] ⇒ exfalso
| [ H : _ |- _ ] ⇒ inversion H; subst;
match goal with
| [ H : _ |- _ ] ⇒ solve [ inversion H ]
end
| [ H : C_Edge _ _ |- _ ] ⇒ destruct H
| [ H : LinearOrder2Schema_Edge _ _ |- _ ] ⇒ destruct H
| _subst; apply eq_JMeq; apply f_equal2; try reflexivity; []; apply JMeq_eq
| _subst; right; apply eq_JMeq; apply f_equal2; try reflexivity; []; apply JMeq_eq
| _subst; left; apply eq_JMeq; apply f_equal2; try reflexivity; []; apply JMeq_eq
| [ p : path ?E ?x ?y |- _ ]
⇒ let x' := fresh in
let y' := fresh in
pose x as x';
pose y as y';
assert (x = x') by reflexivity;
assert (y = y') by reflexivity;
change (path E x y) with (path E x' y') in p;
repeat match goal with
| [ |- context[@JMeq (path E x y) p ?T ?p'] ] ⇒
progress (change (@JMeq (path E x y) p T p')
with (@JMeq (path E x' y') p T p'))
end;
clearbody x' y';
destruct p;
try (subst; reflexivity)
end.

Local Ltac mk_f_x f x fx :=
let H := fresh in
pose (f x) as fx; assert (f x = fx) by reflexivity; clearbody fx.
Local Ltac t_unique_solve :=
solve [
apply SchemaMorphism_Eq; simpl;
intros;
try assumption;
match goal with
| [ H : _ |- _ ] ⇒ rewrite H; reflexivity
end
].
Local Ltac t_unique_solve_recr :=
t_unique_solve || (left; t_unique_solve_recr) || (right; t_unique_solve_recr).

Section part_a.
Definition a_OnVertices0 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Onea | Twoa end.
Definition a_OnVertices1 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Onea | Twob end.
Definition a_OnVertices2 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Onea | Twoc end.
Definition a_OnVertices3 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Oneb | Twoa end.
Definition a_OnVertices4 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Oneb | Twob end.
Definition a_OnVertices5 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Oneb | Twoc end.
Definition a_OnVertices6 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Onec | Twoa end.
Definition a_OnVertices7 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Onec | Twob end.
Definition a_OnVertices8 : LinearOrder2SchemaC :=
fun vmatch v with Zeroa | Onec | Twoc end.
Definition a_path_a_a_0 : path C_Edge a a := NoEdges.
Definition a_path_b_b_0 : path C_Edge b b := NoEdges.
Definition a_path_c_c_0 : path C_Edge c c := NoEdges.
Definition a_path_a_b_0 : path C_Edge a b := AddEdge NoEdges g.
Definition a_path_b_c_0 : path C_Edge b c := AddEdge NoEdges h.
Definition a_path_a_c_0 : path C_Edge a c := AddEdge NoEdges i.
Definition a_path_a_c_1 : path C_Edge a c := AddEdge (AddEdge NoEdges g) h.
Definition Exercise_4_4_1_5_a_SchemaMorphism0 : SchemaMorphism LinearOrder2Schema C
:= SchemaMorphism_template a_OnVertices0 (fun _ _ ematch e with Zero_Onea_path_a_a_0 | One_Twoa_path_a_a_0 end).
Definition Exercise_4_4_1_5_a_SchemaMorphism1 : SchemaMorphism LinearOrder2Schema C
:= SchemaMorphism_template a_OnVertices1 (fun _ _ ematch e with Zero_Onea_path_a_a_0 | One_Twoa_path_a_b_0 end).
Definition Exercise_4_4_1_5_a_SchemaMorphism2 : SchemaMorphism LinearOrder2Schema C
:= SchemaMorphism_template a_OnVertices2 (fun _ _ ematch e with Zero_Onea_path_a_a_0 | One_Twoa_path_a_c_0 end).
Definition Exercise_4_4_1_5_a_SchemaMorphism3 : SchemaMorphism LinearOrder2Schema C
:= SchemaMorphism_template a_OnVertices2 (fun _ _ ematch e with Zero_Onea_path_a_a_0 | One_Twoa_path_a_c_1 end).
Definition Exercise_4_4_1_5_a_SchemaMorphism4 : SchemaMorphism LinearOrder2Schema C
:= SchemaMorphism_template a_OnVertices4 (fun _ _ ematch e with Zero_Onea_path_a_b_0 | One_Twoa_path_b_b_0 end).
Definition Exercise_4_4_1_5_a_SchemaMorphism5 : SchemaMorphism LinearOrder2Schema C
:= SchemaMorphism_template a_OnVertices5 (fun _ _ ematch e with Zero_Onea_path_a_b_0 | One_Twoa_path_b_c_0 end).
Definition Exercise_4_4_1_5_a_SchemaMorphism6 : SchemaMorphism LinearOrder2Schema C
:= SchemaMorphism_template a_OnVertices8 (fun _ _ ematch e with Zero_Onea_path_a_c_0 | One_Twoa_path_c_c_0 end).
Definition Exercise_4_4_1_5_a_SchemaMorphism7 : SchemaMorphism LinearOrder2Schema C
:= SchemaMorphism_template a_OnVertices8 (fun _ _ ematch e with Zero_Onea_path_a_c_1 | One_Twoa_path_c_c_0 end).

Lemma a_path_a_a_only : x : path _ a a, x = a_path_a_a_0. paths_unique_t. Qed.
Lemma a_path_b_b_only : x : path _ b b, x = a_path_b_b_0. paths_unique_t. Qed.
Lemma a_path_c_c_only : x : path _ c c, x = a_path_c_c_0. paths_unique_t. Qed.
Lemma a_path_a_b_only : x : path _ a b, x = a_path_a_b_0. paths_unique_t. Qed.
Lemma a_path_b_c_only : x : path _ b c, x = a_path_b_c_0. paths_unique_t. Qed.
Lemma a_path_a_c_only : x : path _ a c, x = a_path_a_c_0 x = a_path_a_c_1. paths_unique_t. Qed.
Lemma a_path_b_a_only : path C_Edge b aFalse. paths_unique_t. Qed.
Lemma a_path_c_b_only : path C_Edge c bFalse. paths_unique_t. Qed.
Lemma a_path_c_a_only : path C_Edge c aFalse. paths_unique_t. Qed.

Lemma a_OnVertices_only : f : LinearOrder2SchemaC,
f Zero = a
→ f = a_OnVertices0
f = a_OnVertices1
f = a_OnVertices2
f = a_OnVertices3
f = a_OnVertices4
f = a_OnVertices5
f = a_OnVertices6
f = a_OnVertices7
f = a_OnVertices8.
intros f H.
mk_f_x f Zero fZero.
mk_f_x f One fOne.
mk_f_x f Two fTwo.
let H := fresh in
assert (H : f = fun vmatch v with ZerofZero | OnefOne | TwofTwo end)
by (apply functional_extensionality_dep; intros []; intuition);
repeat rewrite H; clear H;
subst fZero;
match goal with
| [ H : f Zero = _ |- _ ] ⇒ rewrite H
end;
clear;
compute;
destruct fOne, fTwo;
intuition.
Qed.
Lemma a_schema_morphism_all_template
: F : SchemaMorphism LinearOrder2Schema C,
F = SchemaMorphism_template (VertexOf F) (PathOf F).
intros.
apply SchemaMorphism_Eq; simpl;
reflexivity.
Qed.

Lemma a_schema_morphsim_on_paths
VO
(PO : s d : LinearOrder2Schema,
SEdge LinearOrder2Schema s d path (SEdge C) (VO s) (VO d))
: PO = (fun _ _ ematch e with Zero_OnePO _ _ Zero_One | One_TwoPO _ _ One_Two end).
repeat (apply functional_extensionality_dep; intro).
match goal with | [ |- context[match ?E with __ end] ] ⇒ destruct E end;
reflexivity.
Qed.
Local Ltac pose_path_uniqueness_proof p :=
((pose proof (a_path_a_a_only p))
|| (pose proof (a_path_a_b_only p))
|| (pose proof (a_path_a_c_only p))
|| (pose proof (a_path_b_a_only p))
|| (pose proof (a_path_b_b_only p))
|| (pose proof (a_path_b_c_only p))
|| (pose proof (a_path_c_a_only p))
|| (pose proof (a_path_c_b_only p))
|| (pose proof (a_path_c_c_only p))).
Theorem a_schema_morphism_all
: F : SchemaMorphism LinearOrder2Schema C,
F Zero = a
→ F = Exercise_4_4_1_5_a_SchemaMorphism0
F = Exercise_4_4_1_5_a_SchemaMorphism1
F = Exercise_4_4_1_5_a_SchemaMorphism2
F = Exercise_4_4_1_5_a_SchemaMorphism3
F = Exercise_4_4_1_5_a_SchemaMorphism4
F = Exercise_4_4_1_5_a_SchemaMorphism5
F = Exercise_4_4_1_5_a_SchemaMorphism6
F = Exercise_4_4_1_5_a_SchemaMorphism7.
intros F H.
rewrite (a_schema_morphism_all_template F).
rewrite (@a_schema_morphsim_on_paths _ (PathOf F)).
destruct (a_OnVertices_only F H); clear H;
match goal with
| [ H : VertexOf ?F = ?G |- _ ]
⇒ let p01 := fresh in
let H01 := fresh in
let p12 := fresh in
let H12 := fresh in
let f0 := fresh in
let f1 := fresh in
let f2 := fresh in
let fH0 := fresh in
let fH1 := fresh in
let fH2 := fresh in
pose (VertexOf F Zero) as f0;
pose (VertexOf F One) as f1;
pose (VertexOf F Two) as f2;
assert (fH0 : VertexOf F Zero = f0) by reflexivity;
assert (fH1 : VertexOf F One = f1) by reflexivity;
assert (fH2 : VertexOf F Two = f2) by reflexivity;
pose (PathOf F _ _ Zero_One : path _ f0 f1) as p01;
pose (PathOf F _ _ One_Two : path _ f1 f2) as p12;
assert (H01 : PathOf F _ _ Zero_One == p01) by reflexivity;
assert (H12 : PathOf F _ _ One_Two == p12) by reflexivity;
clearbody p01 p12 f0 f1 f2;
rewrite H in fH0, fH1, fH2;
subst; simpl in *;
pose_path_uniqueness_proof p01;
pose_path_uniqueness_proof p12
end;
subst;
t_unique_solve_recr.
Qed.
End part_a.

Section part_b.
Definition b_OnVertices0 : CLinearOrder2Schema :=
fun vmatch v with aZero | bZero | cZero end.
Definition b_OnVertices1 : CLinearOrder2Schema :=
fun vmatch v with aZero | bZero | cOne end.
Definition b_OnVertices2 : CLinearOrder2Schema :=
fun vmatch v with aZero | bZero | cTwo end.
Definition b_OnVertices3 : CLinearOrder2Schema :=
fun vmatch v with aZero | bOne | cZero end.
Definition b_OnVertices4 : CLinearOrder2Schema :=
fun vmatch v with aZero | bOne | cOne end.
Definition b_OnVertices5 : CLinearOrder2Schema :=
fun vmatch v with aZero | bOne | cTwo end.
Definition b_OnVertices6 : CLinearOrder2Schema :=
fun vmatch v with aZero | bTwo | cZero end.
Definition b_OnVertices7 : CLinearOrder2Schema :=
fun vmatch v with aZero | bTwo | cOne end.
Definition b_OnVertices8 : CLinearOrder2Schema :=
fun vmatch v with aZero | bTwo | cTwo end.
Definition b_path_0_0 : path LinearOrder2Schema_Edge Zero Zero := NoEdges.
Definition b_path_1_1 : path LinearOrder2Schema_Edge One One := NoEdges.
Definition b_path_2_2 : path LinearOrder2Schema_Edge Two Two := NoEdges.
Definition b_path_0_1 : path LinearOrder2Schema_Edge Zero One := AddEdge NoEdges Zero_One.
Definition b_path_1_2 : path LinearOrder2Schema_Edge One Two := AddEdge NoEdges One_Two.
Definition b_path_0_2 : path LinearOrder2Schema_Edge Zero Two := AddEdge (AddEdge NoEdges Zero_One) One_Two.
Definition Exercise_4_4_1_5_b_SchemaMorphism0 : SchemaMorphism C LinearOrder2Schema
:= SchemaMorphism_template' b_OnVertices0 (fun _ _ ematch e with gb_path_0_0 | hb_path_0_0 | ib_path_0_0 end).
Definition Exercise_4_4_1_5_b_SchemaMorphism1 : SchemaMorphism C LinearOrder2Schema
:= SchemaMorphism_template' b_OnVertices1 (fun _ _ ematch e with gb_path_0_0 | hb_path_0_1 | ib_path_0_1 end).
Definition Exercise_4_4_1_5_b_SchemaMorphism2 : SchemaMorphism C LinearOrder2Schema
:= SchemaMorphism_template' b_OnVertices2 (fun _ _ ematch e with gb_path_0_0 | hb_path_0_2 | ib_path_0_2 end).
Definition Exercise_4_4_1_5_b_SchemaMorphism3 : SchemaMorphism C LinearOrder2Schema
:= SchemaMorphism_template' b_OnVertices4 (fun _ _ ematch e with gb_path_0_1 | hb_path_1_1 | ib_path_0_1 end).
Definition Exercise_4_4_1_5_b_SchemaMorphism4 : SchemaMorphism C LinearOrder2Schema
:= SchemaMorphism_template' b_OnVertices5 (fun _ _ ematch e with gb_path_0_1 | hb_path_1_2 | ib_path_0_2 end).
Definition Exercise_4_4_1_5_b_SchemaMorphism5 : SchemaMorphism C LinearOrder2Schema
:= SchemaMorphism_template' b_OnVertices8 (fun _ _ ematch e with gb_path_0_2 | hb_path_2_2 | ib_path_0_2 end).

Lemma b_path_0_0_only : x : path _ Zero Zero, x = b_path_0_0. paths_unique_t. Qed.
Lemma b_path_1_1_only : x : path _ One One, x = b_path_1_1. paths_unique_t. Qed.
Lemma b_path_2_2_only : x : path _ Two Two, x = b_path_2_2. paths_unique_t. Qed.
Lemma b_path_0_1_only : x : path _ Zero One, x = b_path_0_1. paths_unique_t. Qed.
Lemma b_path_1_2_only : x : path _ One Two, x = b_path_1_2. paths_unique_t. Qed.
Lemma b_path_0_2_only : x : path _ Zero Two, x = b_path_0_2. paths_unique_t. Qed.
Lemma b_path_1_0_only : path LinearOrder2Schema_Edge One ZeroFalse. paths_unique_t. Qed.
Lemma b_path_2_1_only : path LinearOrder2Schema_Edge Two OneFalse. paths_unique_t. Qed.
Lemma b_path_2_0_only : path LinearOrder2Schema_Edge Two ZeroFalse. paths_unique_t. Qed.

Lemma b_OnVertices_only : f : CLinearOrder2Schema,
f a = Zero
→ f = b_OnVertices0
f = b_OnVertices1
f = b_OnVertices2
f = b_OnVertices3
f = b_OnVertices4
f = b_OnVertices5
f = b_OnVertices6
f = b_OnVertices7
f = b_OnVertices8.
intros f H.
mk_f_x f a fa.
mk_f_x f b fb.
mk_f_x f c fc.
let H := fresh in
assert (H : f = fun vmatch v with afa | bfb | cfc end)
by (apply functional_extensionality_dep; intros []; intuition);
repeat rewrite H; clear H;
subst fa;
match goal with
| [ H : f a = _ |- _ ] ⇒ rewrite H
end;
clear;
compute;
destruct fb, fc;
intuition.
Qed.
Lemma b_schema_morphism_all_template'
: F : SchemaMorphism C LinearOrder2Schema,
F = SchemaMorphism_template' (VertexOf F) (PathOf F).
intros.
apply SchemaMorphism_Eq; simpl;
reflexivity.
Qed.

Lemma b_schema_morphsim_on_paths
VO
(PO : s d : C,
SEdge C s d path (SEdge LinearOrder2Schema) (VO s) (VO d))
: PO = (fun _ _ ematch e with gPO _ _ g | hPO _ _ h | iPO _ _ i end).
repeat (apply functional_extensionality_dep; intro).
match goal with | [ |- context[match ?E with __ end] ] ⇒ destruct E end;
reflexivity.
Qed.
Local Ltac pose_path_uniqueness_proof p :=
((pose proof (b_path_0_0_only p))
|| (pose proof (b_path_0_1_only p))
|| (pose proof (b_path_0_2_only p))
|| (pose proof (b_path_1_0_only p))
|| (pose proof (b_path_1_1_only p))
|| (pose proof (b_path_1_2_only p))
|| (pose proof (b_path_2_0_only p))
|| (pose proof (b_path_2_1_only p))
|| (pose proof (b_path_2_2_only p))).
Theorem b_schema_morphism_all
: F : SchemaMorphism C LinearOrder2Schema,
F a = Zero
→ F = Exercise_4_4_1_5_b_SchemaMorphism0
F = Exercise_4_4_1_5_b_SchemaMorphism1
F = Exercise_4_4_1_5_b_SchemaMorphism2
F = Exercise_4_4_1_5_b_SchemaMorphism3
F = Exercise_4_4_1_5_b_SchemaMorphism4
F = Exercise_4_4_1_5_b_SchemaMorphism5.
intros F H.
rewrite (b_schema_morphism_all_template' F).
rewrite (@b_schema_morphsim_on_paths _ (PathOf F)).
destruct (b_OnVertices_only F H); clear H;
match goal with
| [ H : VertexOf ?F = ?G |- _ ]
⇒ let pab := fresh in
let Hab := fresh in
let pbc := fresh in
let Hbc := fresh in
let pac := fresh in
let Hac := fresh in
let fa := fresh in
let fb := fresh in
let fc := fresh in
let fHa := fresh in
let fHb := fresh in
let fHc := fresh in
pose (VertexOf F a) as fa;
pose (VertexOf F b) as fb;
pose (VertexOf F c) as fc;
assert (fHa : VertexOf F a = fa) by reflexivity;
assert (fHb : VertexOf F b = fb) by reflexivity;
assert (fHc : VertexOf F c = fc) by reflexivity;
pose (PathOf F _ _ g : path _ fa fb) as pab;
pose (PathOf F _ _ h : path _ fb fc) as pbc;
pose (PathOf F _ _ i : path _ fa fc) as pac;
assert (Hab : PathOf F _ _ g == pab) by reflexivity;
assert (Hbc : PathOf F _ _ h == pbc) by reflexivity;
assert (Hac : PathOf F _ _ i == pac) by reflexivity;
clearbody pab pbc pac fa fb fc;
rewrite H in fHa, fHb, fHc;
subst; simpl in *;
pose_path_uniqueness_proof pab;
pose_path_uniqueness_proof pbc;
pose_path_uniqueness_proof pac
end;