Download Matita Tutorial - Dipartimento di Informatica

·
Matita Tutorial
93
7 Quotienting in type theory
7.1 Rewriting setoid equalities . . . . . . . . . . . . . . . . . . . . . . . .
7.2 Dependent setoids . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.3 Avoiding setoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
162
167
170
170
8 Infinite structures and Coinductive Types
8.1 Real Numbers as Cauchy sequences . . . . . .
8.2 Traces of a program . . . . . . . . . . . . . .
8.3 Infinite data types as coinductive types . . .
8.4 Real numbers via coinductive types . . . . . .
8.5 Intermezzo: the dynamics of coinductive data
8.6 Traces of a program via coinductive types . .
8.7 How to compare coinductive types . . . . . .
8.8 Generic construction principles . . . . . . . .
172
172
174
176
178
180
181
185
188
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
9 Logical Restrictions
190
9.1 Positivity in inductive definitions . . . . . . . . . . . . . . . . . . . . 190
9.2 Universe Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . 192
9.3 Informative and non informative content . . . . . . . . . . . . . . . . 194
10 Further readings
197
Journal of Formalized Reasoning Vol. 7, No. 2, 2014.