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
|
.. index::
single: fix
Recursive functions: fix
------------------------
.. insertprodn term_fix fixannot
.. prodn::
term_fix ::= let fix @fix_body in @term
| fix @fix_body {? {+ with @fix_body } for @ident }
fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
fixannot ::= %{ struct @ident %}
| %{ wf @one_term @ident %}
| %{ measure @one_term {? @ident } {? @one_term } %}
The expression ":n:`fix @ident__1 @binder__1 : @type__1 := @term__1 with … with @ident__n @binder__n : @type__n := @term__n for @ident__i`" denotes the
:math:`i`-th component of a block of functions defined by mutual structural
recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When
:math:`n=1`, the ":n:`for @ident__i`" clause is omitted.
The association of a single fixpoint and a local definition have a special
syntax: :n:`let fix @ident {* @binder } := @term in` stands for
:n:`let @ident := fix @ident {* @binder } := @term in`. The same applies for co-fixpoints.
Some options of :n:`@fixannot` are only supported in specific constructs. :n:`fix` and :n:`let fix`
only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in
commands such as :cmd:`Function` and :cmd:`Program Fixpoint`.
.. _Fixpoint:
Top-level recursive functions
-----------------------------
This section describes the primitive form of definition by recursion over
inductive objects. See the :cmd:`Function` command for more advanced
constructions.
.. cmd:: Fixpoint @fix_definition {* with @fix_definition }
.. insertprodn fix_definition fix_definition
.. prodn::
fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations }
This command allows defining functions by pattern matching over inductive
objects using a fixed point construction. The meaning of this declaration is
to define :n:`@ident` as a recursive function with arguments specified by
the :n:`@binder`\s such that :n:`@ident` applied to arguments
corresponding to these :n:`@binder`\s has type :n:`@type`, and is
equivalent to the expression :n:`@term`. The type of :n:`@ident` is
consequently :n:`forall {* @binder }, @type` and its value is equivalent
to :n:`fun {* @binder } => @term`.
To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
constraints on a special argument called the decreasing argument. They
are needed to ensure that the :cmd:`Fixpoint` definition always terminates.
The point of the :n:`{struct @ident}` annotation (see :n:`@fixannot`) is to
let the user tell the system which argument decreases along the recursive calls.
The :n:`{struct @ident}` annotation may be left implicit, in which case the
system successively tries arguments from left to right until it finds one
that satisfies the decreasing condition.
:cmd:`Fixpoint` without the :attr:`program` attribute does not support the
:n:`wf` or :n:`measure` clauses of :n:`@fixannot`.
The :n:`with` clause allows simultaneously defining several mutual fixpoints.
It is especially useful when defining functions over mutually defined
inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`.
If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing 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 constant
for which the computational behavior is relevant. See :ref:`proof-editing-mode`.
.. note::
+ Some fixpoints may have several arguments that fit as decreasing
arguments, and this choice influences the reduction of the fixpoint.
Hence an explicit annotation must be used if the leftmost decreasing
argument is not the desired one. Writing explicit annotations can also
speed up type checking of large mutual fixpoints.
+ In order to keep the strong normalization property, the fixed point
reduction will only be performed when the argument in position of the
decreasing argument (which type should be in an inductive definition)
starts with a constructor.
.. example::
One can define the addition function as :
.. coqtop:: all
Fixpoint add (n m:nat) {struct n} : nat :=
match n with
| O => m
| S p => S (add p m)
end.
The match operator matches a value (here :g:`n`) with the various
constructors of its (inductive) type. The remaining arguments give the
respective values to be returned, as functions of the parameters of the
corresponding constructor. Thus here when :g:`n` equals :g:`O` we return
:g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`.
The match operator is formally described in
Section :ref:`match-construction`.
The system recognizes that in the inductive call :g:`(add p m)` the first
argument actually decreases because it is a *pattern variable* coming
from :g:`match n with`.
.. example::
The following definition is not correct and generates an error message:
.. coqtop:: all
Fail Fixpoint wrongplus (n m:nat) {struct n} : nat :=
match m with
| O => n
| S p => S (wrongplus n p)
end.
because the declared decreasing argument :g:`n` does not actually
decrease in the recursive call. The function computing the addition over
the second argument should rather be written:
.. coqtop:: all
Fixpoint plus (n m:nat) {struct m} : nat :=
match m with
| O => n
| S p => S (plus n p)
end.
.. example::
The recursive call may not only be on direct subterms of the recursive
variable :g:`n` but also on a deeper subterm and we can directly write
the function :g:`mod2` which gives the remainder modulo 2 of a natural
number.
.. coqtop:: all
Fixpoint mod2 (n:nat) : nat :=
match n with
| O => O
| S p => match p with
| O => S O
| S q => mod2 q
end
end.
.. _example_mutual_fixpoints:
.. example:: Mutual fixpoints
The size of trees and forests can be defined the following way:
.. coqtop:: all
Fixpoint tree_size (t:tree) : nat :=
match t with
| node a f => S (forest_size f)
end
with forest_size (f:forest) : nat :=
match f with
| leaf b => 1
| cons t f' => (tree_size t + forest_size f')
end.
|
