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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
Co-inductive types and co-recursive functions
=============================================
.. _coinductive-types:
Co-inductive types
------------------
The objects of an inductive type are well-founded with respect to the
constructors of the type. In other words, such objects contain only a
*finite* number of constructors. Co-inductive types arise from relaxing
this condition, and admitting types whose objects contain an infinity of
constructors. Infinite objects are introduced by a non-ending (but
effective) process of construction, defined in terms of the constructors
of the type.
More information on co-inductive definitions can be found in
:cite:`Gimenez95b,Gim98,GimCas05`.
.. cmd:: CoInductive @inductive_definition {* with @inductive_definition }
This command introduces a co-inductive type.
The syntax of the command is the same as the command :cmd:`Inductive`.
No principle of induction is derived from the definition of a co-inductive
type, since such principles only make sense for inductive types.
For co-inductive types, the only elimination principle is case analysis.
This command supports the :attr:`universes(polymorphic)`,
:attr:`universes(template)`, :attr:`universes(cumulative)`,
:attr:`private(matching)`, :attr:`bypass_check(universes)`,
:attr:`bypass_check(positivity)`, and :attr:`using` attributes.
.. example::
The type of infinite sequences of natural numbers, usually called streams,
is an example of a co-inductive type.
.. coqtop:: in
CoInductive Stream : Set := Seq : nat -> Stream -> Stream.
The usual destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str`
can be defined as follows:
.. coqtop:: in
Definition hd (x:Stream) := let (a,s) := x in a.
Definition tl (x:Stream) := let (a,s) := x in s.
Definitions of co-inductive predicates and blocks of mutually
co-inductive definitions are also allowed.
.. example::
The extensional equality on streams is an example of a co-inductive type:
.. coqtop:: in
CoInductive EqSt : Stream -> Stream -> Prop :=
eqst : forall s1 s2:Stream,
hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
In order to prove the extensional equality of two streams :g:`s1` and :g:`s2`
we have to construct an infinite proof of equality, that is, an infinite
object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite
objects in Section :ref:`cofixpoint`.
Caveat
~~~~~~
The ability to define co-inductive types by constructors, hereafter called
*positive co-inductive types*, is known to break subject reduction. The story is
a bit long: this is due to dependent pattern-matching which implies
propositional η-equality, which itself would require full η-conversion for
subject reduction to hold, but full η-conversion is not acceptable as it would
make type checking undecidable.
Since the introduction of primitive records in Coq 8.5, an alternative
presentation is available, called *negative co-inductive types*. This consists
in defining a co-inductive type as a primitive record type through its
projections. Such a technique is akin to the *co-pattern* style that can be
found in e.g. Agda, and preserves subject reduction.
The above example can be rewritten in the following way.
.. coqtop:: none
Reset Stream.
.. coqtop:: all
Set Primitive Projections.
CoInductive Stream : Set := Seq { hd : nat; tl : Stream }.
CoInductive EqSt (s1 s2: Stream) : Prop := eqst {
eqst_hd : hd s1 = hd s2;
eqst_tl : EqSt (tl s1) (tl s2);
}.
Some properties that hold over positive streams are lost when going to the
negative presentation, typically when they imply equality over streams.
For instance, propositional η-equality is lost when going to the negative
presentation. It is nonetheless logically consistent to recover it through an
axiom.
.. coqtop:: all
Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s).
More generally, as in the case of positive coinductive types, it is consistent
to further identify extensional equality of coinductive types with propositional
equality:
.. coqtop:: all
Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2.
As of Coq 8.9, it is now advised to use negative co-inductive types rather than
their positive counterparts.
.. seealso::
:ref:`primitive_projections` for more information about negative
records and primitive projections.
.. index::
single: cofix
Co-recursive functions: cofix
-----------------------------
.. insertprodn term_cofix cofix_body
.. prodn::
term_cofix ::= let cofix @cofix_body in @term
| cofix @cofix_body {? {+ with @cofix_body } for @ident }
cofix_body ::= @ident {* @binder } {? : @type } := @term
The expression
":n:`cofix @ident__1 @binder__1 : @type__1 with … with @ident__n @binder__n : @type__n for @ident__i`"
denotes the :math:`i`-th component of a block of terms defined by a mutual guarded
co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When
:math:`n=1`, the ":n:`for @ident__i`" clause is omitted.
.. _cofixpoint:
Top-level definitions of co-recursive functions
-----------------------------------------------
.. cmd:: CoFixpoint @cofix_definition {* with @cofix_definition }
.. insertprodn cofix_definition cofix_definition
.. prodn::
cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations }
This command introduces a method for constructing an infinite object of a
coinductive type. For example, the stream containing all natural numbers can
be introduced applying the following method to the number :g:`O` (see
Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd`
and :g:`tl`):
.. coqtop:: all
CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
Unlike recursive definitions, there is no decreasing argument in a
co-recursive definition. To be admissible, a method of construction must
provide at least one extra constructor of the infinite object for each
iteration. A syntactical guard condition is imposed on co-recursive
definitions in order to ensure this: each recursive call in the
definition must be protected by at least one constructor, and only by
constructors. That is the case in the former definition, where the single
recursive call of :g:`from` is guarded by an application of :g:`Seq`.
On the contrary, the following recursive function does not satisfy the
guard condition:
.. coqtop:: all
Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
The elimination of co-recursive definition is done lazily, i.e. the
definition is expanded only when it occurs at the head of an application
which is the argument of a case analysis expression. In any other
context, it is considered as a canonical expression which is completely
evaluated. We can test this using the command :cmd:`Eval`, which computes
the normal forms of a term:
.. coqtop:: all
Eval compute in (from 0).
Eval compute in (hd (from 0)).
Eval compute in (tl (from 0)).
As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously
defining several mutual cofixpoints.
If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode.
This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
In this case, the proof should be terminated with :cmd:`Defined` in order to define a :term:`constant`
for which the computational behavior is relevant. See :ref:`proof-editing-mode`.
|
