-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathallGraphs.v
195 lines (147 loc) · 5.03 KB
/
allGraphs.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
(** Celia Picard with contributions by Ralph Matthes,
I.R.I.T., University of Toulouse and CNRS*)
(** provides the implementation of the type Graphs, properties
and lemmas on it, and the development of various examples *)
Require Export Arith.
Require Import Utf8.
Require Import Setoid.
Require Import List.
Require Import Ilist.
Require Import Fin.
Require Import Graphs.
Require Import Morphisms.
Require Import Basics.
Require Import Tools.
Require Import PermsLists.
Require Import GPerm.
Set Implicit Arguments.
Section AllGraphs_def_tools.
Variable T: Set.
(* Definition of coinductive graphs *)
Definition AllGraph: Set := Graph (option T).
Definition AGeq (R: relation T) : relation AllGraph := Geq (RelOp R).
Lemma AGeq_refl (R: relation T)(Rrefl: Reflexive R) : Reflexive (AGeq R).
Proof.
red.
apply Geq_refl.
red.
apply RelOp_refl, Rrefl.
Qed.
Lemma AGeq_sym (R: relation T)(Rsym: Symmetric R) : Symmetric (AGeq R).
Proof.
red.
apply Geq_sym.
red.
apply RelOp_sym, Rsym.
Qed.
Lemma AGeq_trans (R: relation T)(Rtrans: Transitive R) : Transitive (AGeq R).
Proof.
red.
apply Geq_trans.
red.
apply RelOp_trans, Rtrans.
Qed.
Add Parametric Relation (RelT: relation T)(Req: Equivalence RelT): (AllGraph) (AGeq RelT)
reflexivity proved by (AGeq_refl _)
symmetry proved by (AGeq_sym _)
transitivity proved by (AGeq_trans _)
as AGeqRel.
Definition ForestGr : Set := list (Graph T).
CoFixpoint G2AG (g: Graph T) : AllGraph := mk_Graph (Some (label g)) (imap G2AG (sons g)).
Definition FG2AG (lg : ForestGr) : AllGraph := mk_Graph None (list2ilist (map G2AG lg)).
Definition FGeq (R: relation T) : relation ForestGr := permut1 (GPPerm R).
Lemma FGeq_refl (R: relation T)(Rrefl: Reflexive R) : Reflexive (FGeq R).
Proof.
red.
apply permut1_refl.
red.
apply GPPerm_refl, Rrefl.
Qed.
Lemma FGeq_sym (R: relation T) : Symmetric (FGeq R).
Proof.
red.
apply permut1_sym.
red.
apply GPPerm_sym.
Qed.
Lemma FGeq_trans (R: relation T)(Rtrans: Transitive R) : Transitive (FGeq R).
Proof.
red.
apply permut1_trans.
red.
apply GPPerm_trans, Rtrans.
Qed.
Add Parametric Relation (RelT: relation T)(Req: Equivalence RelT): (ForestGr) (FGeq RelT)
reflexivity proved by (FGeq_refl _)
symmetry proved by (@FGeq_sym _)
transitivity proved by (FGeq_trans _)
as FGeqRel.
End AllGraphs_def_tools.
(* Graph 1 -> 0 <- 2*)
Definition two_roots_AllGraph : AllGraph nat.
Proof.
set (node0 := mk_Graph (Some 0) (inil (AllGraph nat))).
set (node1 := mk_Graph (Some 1) (icons node0 (inil (AllGraph nat)))).
set (node2 := mk_Graph (Some 2) (icons node0 (inil (AllGraph nat)))).
exact (mk_Graph None (icons node1 (icons node2 (inil (AllGraph nat))))).
Defined.
Definition two_roots_ForestGr : ForestGr nat.
Proof.
set (node0 := mk_Graph 0 (inil (Graph nat))).
set (node1 := mk_Graph 1 (icons node0 (inil (Graph nat)))).
set (node2 := mk_Graph 2 (icons node0 (inil (Graph nat)))).
exact (node1 :: node2 :: nil).
Defined.
Lemma two_roots_ForestGr_two_roots_AllGraph :
Geq (RelOp eq) two_roots_AllGraph (FG2AG two_roots_ForestGr).
Proof.
apply Geq_intro.
{ cbn.
trivial. }
assert (h1 := refl_equal _: lgti (sons two_roots_AllGraph) = lgti (sons (FG2AG two_roots_ForestGr))).
apply (is_ilist_rel _ _ _ h1).
intro i.
cbn in *|-*.
rewrite <- decode_Fin_match'.
elim (zerop (decode_Fin i)) ; intros a.
- rewrite (decode_Fin_0_first _ a).
apply Geq_intro.
+ reflexivity.
+ cbn.
assert (h2 := refl_equal _ :
lgti (icons (mk_Graph (Some 0) (inil (AllGraph nat))) (inil (AllGraph nat))) =
lgti (imap (@G2AG _)(icons (mk_Graph 0 (inil (Graph nat))) (inil (Graph nat))))).
apply (is_ilist_rel _ _ _ h2).
cbn in *|-*.
intro i'.
rewrite <- (decode_Fin_unique _ _ (decode_Fin_match' i' h2)).
rewrite (Fin_first_1 i').
apply Geq_intro.
* reflexivity.
* cbn.
assert (h3 := refl_equal _ : lgti (inil (AllGraph nat)) = lgti (imap (@G2AG _) (inil (Graph nat)))).
apply (is_ilist_rel _ _ _ h3).
intro i'' ; inversion i''.
- assert (h2 : i = succ (first 0)).
{ apply decode_Fin_unique.
apply symmetry, (le_antisym _ _ (lt_le_S _ _ a) (lt_n_Sm_le _ _ (decode_Fin_inf_n i))). }
rewrite h2 ; clear h2.
cbn.
apply Geq_intro.
+ reflexivity.
+ cbn.
assert (h2 := refl_equal _ :
lgti (icons (mk_Graph (Some 0) (inil (AllGraph nat))) (inil (AllGraph nat))) =
lgti (imap (@G2AG _)(icons (mk_Graph 0 (inil (Graph nat))) (inil (Graph nat))))).
apply (is_ilist_rel _ _ _ h2).
cbn in *|-*.
intro i'.
rewrite <- (decode_Fin_unique _ _ (decode_Fin_match' i' h2)).
rewrite (Fin_first_1 i').
apply Geq_intro.
* reflexivity.
* cbn.
assert (h3 := refl_equal _ : lgti (inil (AllGraph nat)) = lgti (imap (@G2AG _) (inil (Graph nat)))).
apply (is_ilist_rel _ _ _ h3).
intro i'' ; inversion i''.
Qed.