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
|
Module test1.
Section test1.
Variable (A B C A' B' C' : Type).
Variable (f1 : A -> A') (f2 : B -> B') (f3 : C -> C').
Variable (g1 : A -> B) (g2 : A' -> B') (h1 : B -> C) (h2 : B' -> C').
Local Coercion g1 : A >-> B.
Local Coercion g2 : A' >-> B'.
Local Coercion h1 : B >-> C.
Local Coercion h2 : B' >-> C'.
Local Coercion f1 : A >-> A'.
Local Coercion f2 : B >-> B'.
Local Coercion f3 : C >-> C'.
(* [g1; h1; f3], [f1; g2; h2] : A >-> C' should not be reported as ambiguous *)
(* paths because they are redundant with `[g1; f2], [f1; g2] : A >-> B'` and *)
(* `[h1; f3], [f2; h2] : B >-> C'`. *)
Print Graph.
End test1.
End test1.
Module test2.
Section test2.
Variable (A B C D : Type).
Variable (ab : A -> B) (bc : B -> C) (ac : A -> C) (cd : C -> D).
Local Coercion ac : A >-> C.
Local Coercion cd : C >-> D.
Local Coercion ab : A >-> B.
Local Coercion bc : B >-> C.
(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be reported as ambiguous *)
(* paths because they are redundant with `[ab; bc], [ac] : A >-> C`. *)
Print Graph.
End test2.
End test2.
Module test3.
Section test3.
Variable (A B C : Type).
Variable (ab : A -> B) (ba : B -> A) (ac : A -> C) (bc : B -> C).
Local Coercion ac : A >-> C.
Local Coercion bc : B >-> C.
Local Coercion ab : A >-> B.
Local Coercion ba : B >-> A.
(* `[ba; ac], [bc] : B >-> C` should not be reported as ambiguous paths *)
(* because they are redundant with `[ab; bc], [ac] : A >-> C` and *)
(* `[ba; ab] : B >-> B`. *)
Print Graph.
End test3.
End test3.
Module test4.
Section test4.
Variable (A : Type) (P Q : A -> Prop).
Record B := {
B_A : A;
B_P : P B_A }.
Record C := {
C_A : A;
C_Q : Q C_A }.
Record D := {
D_A : A;
D_P : P D_A;
D_Q : Q D_A }.
Local Coercion B_A : B >-> A.
Local Coercion C_A : C >-> A.
Local Coercion D_A : D >-> A.
Local Coercion D_B (d : D) : B := Build_B (D_A d) (D_P d).
Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
Print Graph.
End test4.
End test4.
Module test5.
Section test5.
Variable (A : Type) (P Q : A -> Prop).
Definition A' (x : bool) := A.
Record B (x : bool) := {
B_A' : A' x;
B_P : P B_A' }.
Record C (x : bool) := {
C_A' : A' x;
C_Q : Q C_A' }.
Record D := {
D_A : A;
D_P : P D_A;
D_Q : Q D_A }.
Local Coercion A'_A (x : bool) (a : A' x) : A := a.
Local Coercion B_A' : B >-> A'.
Local Coercion C_A' : C >-> A'.
Local Coercion D_A : D >-> A.
Local Coercion D_B (d : D) : B false := Build_B false (D_A d) (D_P d).
Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
Print Graph.
End test5.
End test5.
Module test6.
Section test6.
Variable (A : Type) (P Q : A -> Prop).
Record A' (x : bool) := { A'_A : A }.
Record B (x : bool) := {
B_A' : A' x;
B_P : P (A'_A x B_A') }.
Record C (x : bool) := {
C_A' : A' x;
C_Q : Q (A'_A x C_A') }.
Record D := {
D_A : A;
D_P : P D_A;
D_Q : Q D_A }.
Local Coercion A'_A : A' >-> A.
Local Coercion B_A' : B >-> A'.
Local Coercion C_A' : C >-> A'.
Local Coercion D_A : D >-> A.
Local Coercion D_B (d : D) : B false :=
Build_B false (Build_A' false (D_A d)) (D_P d).
Local Coercion D_C (d : D) : C true :=
Build_C true (Build_A' true (D_A d)) (D_Q d).
Print Graph.
End test6.
End test6.
Module test7.
Record > NAT := wrap_nat { unwrap_nat :> nat }.
Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }.
Record > TYPE := wrap_Type { unwrap_Type :> Type }.
End test7.
Module test8.
Set Primitive Projections.
Record > NAT_prim := wrap_nat { unwrap_nat :> nat }.
Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }.
Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }.
End test8.
|
