2 Coinductive Types and Predicates
5 include "basics/lists/list.ma".
6 include "tutorial/chapter12.ma".
8 (* The only primitive data types of Matita are dependent products and universes.
9 So far every other user defined data type has been an inductive type. An
10 inductive type is declared by giving its list of constructors (or introduction
11 rules in the case of predicates). An inhabitant of an inductive type is obtained
12 composing together a finite number of constructors and data of other types,
13 according to the type of the constructors. Therefore all inhabitants of inductive
14 types are essentially finite objects. Natural numbers, lists, trees, states of
15 a DFA, letters of an alphabet are all finite and can be defined inductively.
17 If you think of an inhabitant of an inductive type as a tree of a certain shape,
18 whose nodes are constructors, the only trees can be represented are trees of
19 finite height. Note, however, that it is possible to have trees of infinite
20 width by putting in the argument of a constructor of a type I an enumeration
21 of elements of I (e.g. ℕ → I). *)
23 (* Example of an infinitely branching tree of elements of type A stored in
25 inductive infbrtree (A: Type[0]) : Type[0] ≝
27 | Node: A → (ℕ → infbrtree A) → infbrtree A.
29 (* Example: the tree of natural numbers whose root holds 0 and has as children
31 example infbrtree_ex ≝ Node ℕ 0 (λn. Node ℕ (S n) (λ_.Nil ℕ)).
33 (*** Infinite data types via functions ***)
35 (* In mathematics and less frequently in computer science there is the need to
36 also represent and manipulate types of infinite objects. Typical examples are:
37 sequences, real numbers (a special case of sequences), data streams (e.g. as
38 read from a network interface), traces of diverging computations of a program,
39 etc. One possible representation, used in mathematics since a long time, is
40 to describe an infinite object by means of an infinite collection of
41 approximations (also called observations). Often, the infinite collection can
42 be structured in a sequence, identified as a function from the domain of natural
45 (* Example 1: sequences of elements of type A *)
46 definition seq : Type[0] → Type[0] ≝ λA:Type[0]. ℕ → A.
48 (* Example 2: Real numbers as Cauchy sequences and their addition. *)
49 (* First we axiomatize the relevant properties of rational numbers. *)
51 axiom Qdist: Q → Q → Q.
52 axiom symmetric_Qdist: ∀x,y. Qdist x y = Qdist y x.
53 axiom Qleq: Q → Q → Prop.
54 interpretation "Qleq" 'leq x y = (Qleq x y).
55 axiom transitive_Qleq: transitive … Qleq.
56 axiom Qplus: Q → Q → Q.
57 interpretation "Qplus" 'plus x y = (Qplus x y).
59 ∀qa1,qb1,qa2,qb2. qa1 ≤ qb1 → qa2 ≤ qb2 → qa1 + qa2 ≤ qb1 + qb2.
61 ∀qa1,qb1,qa2,qb2. Qdist (qa1 + qa2) (qb1 + qb2) ≤ Qdist qa1 qb1 + Qdist qa2 qb2.
63 axiom Qplus_Qhalve_Qhalve: ∀q. Qhalve q + Qhalve q = q.
64 axiom triangular_Qdist: ∀x,y,z. Qdist x z ≤ Qdist x y + Qdist y z.
66 (* A sequence of rationals. *)
67 definition Qseq: Type[0] ≝ seq Q.
69 (* The Cauchy property *)
70 definition Cauchy: Qseq → Prop ≝
71 λR:Qseq. ∀eps. ∃n. ∀i,j. n ≤ i → n ≤ j → Qdist (R i) (R j) ≤ eps.
73 (* A real number is an equivalence class of Cauchy sequences. In type theory
74 we can define R as a setoid whose carrier R_ is the type of Cauchy sequences. *)
80 (* Two sequences are equal when for every epsilon they are eventually pointwise
81 closer than epsilon. *)
82 definition R : setoid ≝
84 (mk_equivalence_relation …
85 (λr1,r2:R_. ∀eps. ∃n. ∀i. n ≤ i → Qdist (r r1 i) (r r2 i) ≤ eps) …).
86 [ (* transitivity *) #x #y #z #H1 #H2 #eps cases (H1 (Qhalve eps)) #i -H1 #H1
87 cases (H2 (Qhalve eps)) #j -H2 #H2 %{(max i j)} #l #Hmax
88 <(Qplus_Qhalve_Qhalve eps) @transitive_Qleq
89 [3: @(Qleq_Qplus … (H1 l …) (H2 l …)) /2 by le_maxl,le_maxr/
91 | (* symmetry *) #x #y #H #eps cases (H eps) /3 by ex_intro/
92 | (* reflexivity *) #x #eps cases (isCauchy x eps) /3 by ex_intro/ ]
95 unification hint 0 ≔ ;
97 (* ---------------------------------------- *) ⊢
100 (* The following coercion is used to write r n to extract the n-th approximation
101 from the real number r *)
102 coercion R_to_fun : ∀r:R. ℕ → Q ≝ r on _r:R to ?.
104 (* Adding two real numbers just requires pointwise addition of the
105 approximations. The proof that the resulting sequence is Cauchy is the standard
106 one: to obtain an approximation up to eps it is necessary to approximate both
107 summands up to eps/2. *)
108 definition Rplus_: R_ → R_ → R_ ≝
109 λr1,r2. mk_R_ (λn. r1 n + r2 n) ….
111 cases (isCauchy r1 (Qhalve eps)) #n1 #H1
112 cases (isCauchy r2 (Qhalve eps)) #n2 #H2
113 %{(max n1 n2)} #i #j #K1 #K2 @(transitive_Qleq … (Qdist_Qplus …))
114 <(Qplus_Qhalve_Qhalve eps) @Qleq_Qplus [@H1 @le_maxl | @H2 @le_maxr]
118 (* We lift Rplus_ to a morphism by proving that it respects the equality for
119 real numbers. We closely follow the usual mathematical proof: to compute the
120 sum up to epsilon it is sufficient to fetch the arguments at precision
122 definition Rplus: R ⤞ R ⤞ R ≝
123 mk_bin_morphism … Rplus_ ….
124 #x1 #x2 #y1 #y2 #Hx #Hy #eps
125 cases (Hx (Qhalve eps)) #i -Hx #Hx
126 cases (Hy (Qhalve eps)) #j -Hy #Hy
127 %{(max i j)} #l #Hmax <(Qplus_Qhalve_Qhalve eps) @transitive_Qleq
128 [3: @(Qleq_Qplus … (Hx l …) (Hy l …)) /2 by le_maxl,le_maxr/
132 (* Example 3: traces of a program *)
133 (* Let us introduce a very simple programming language whose instructions
134 can test and set a single implicit variable. *)
135 inductive instr: Type[0] ≝
136 p_set: ℕ → instr (* sets the variable to a constant *)
137 | p_incr: instr (* increments the variable *)
138 | p_while: list instr → instr. (* repeats until the variable is 0 *)
140 (* The status of a program as the values of the variable and the list of
141 instructions to be executed. *)
142 definition state ≝ ℕ × (list instr).
144 (* The transition function from a state to the next one. *)
145 inductive next: state → state → Prop ≝
146 n_set: ∀n,k,o. next 〈o,(p_set n)::k〉 〈n,k〉
147 | n_incr: ∀k,o. next 〈o,p_incr::k〉 〈S o,k〉
148 | n_while_exit: ∀b,k. next 〈0,(p_while b)::k〉 〈0,k〉
149 | n_while_loop: ∀b,k,o. next 〈S o,(p_while b)::k〉 〈S o,b@(p_while b)::k〉.
151 (* A diverging trace is a sequence of states such that the n+1-th state is
152 obtained executing one step from the n-th state *)
153 record div_trace: Type[0] ≝
155 ; div_well_formed: ∀n. next (div_tr n) (div_tr (S n))
158 (* The previous definition of trace is not computable: we cannot write
159 a program that given an initial state returns its trace. To write that function,
160 we first write a computable version of next, called step. *)
161 definition step: state → option state ≝
172 | S p ⇒ 〈S p,b@(p_while b)::k〉 ]]].
174 theorem step_next: ∀o,n. step o = Some … n → next o n.
175 * #o * [ #n normalize #abs destruct ]
179 | #b #tl * #n' #tl' cases o normalize [2: #r]]
183 theorem next_step: ∀o,n. next o n → step o = Some … n.
184 * #o #k * #n #k' #H inversion H normalize
191 (* Termination is the archetipal undecidable problem. Therefore there is no
192 function that given an initial state returns the diverging trace if the program
193 diverges or fails in case of error. The best we can do is to give an alternative
194 definition of trace that captures both diverging and converging computations. *)
195 record trace: Type[0] ≝
196 { tr: seq (option state)
197 ; well_formed: ∀n,s. tr n = Some … s → tr (S n) = step s
200 (* The trace is diverging if every state is not final. *)
201 definition diverging: trace → Prop ≝
202 λt. ∀n. tr t n ≠ None ?.
204 (* The two definitions of diverging traces are equivalent. *)
205 theorem div_trace_to_diverging_trace:
206 ∀d: div_trace. ∃t: trace. diverging t ∧ tr t 0 = Some … (div_tr d 0).
207 #d %{(mk_trace (λn.Some ? (div_tr d n)) …)}
208 [2: % // #n % #abs destruct
209 | #n #s #EQ destruct lapply (div_well_formed d n) /2 by div_well_formed, next_step/ ]
212 theorem diverging_trace_to_div_trace:
213 ∀t: trace. diverging t → ∃d: div_trace. tr t 0 = Some … (div_tr d 0).
215 [ % [ #n lapply (H n) -H cases (tr t n) [ * #abs cases (abs …) // ] #s #_ @s
216 | #n lapply (well_formed t n)
217 lapply (H n) cases (tr t n) normalize [ * #abs cases (abs …) // ]
218 * #o #k #_ lapply (H (S n)) -H
219 cases (tr t (S n)) normalize
220 [ * #abs cases (abs …) // ] * #o' #k' #_ #EQ lapply (EQ … (refl …)) -EQ
221 normalize cases k normalize [ #abs destruct ] #hd #tl #EQ destruct -EQ
223 | lapply (H O) -H cases (tr t O) [ * #abs cases (abs …) // ] // ]
226 (* However, given an initial state we can always compute a trace.
227 Note that every time the n-th element of the trace is accessed, all the
228 elements in position ≤ n are computed too. *)
229 let rec compute_trace_seq (s:state) (n:nat) on n : option state ≝
233 match compute_trace_seq s m with
235 | Some o ⇒ step o ]].
237 definition compute_trace: ∀s:state. Σt:trace. tr t 0 = Some … s.
239 [ %{(compute_trace_seq s)}
240 #n #o elim n [ whd in ⊢ (??%? → ??%?); #EQ destruct // ]
241 -n #n #_ #H whd in ; whd in ⊢ (??%?); >H //
245 (*** Infinite data types as coinductive types ***)
247 (* All the previous examples were handled very easily via sequences
248 declared as functions. A few critics can be made to this approach though:
249 1. the sequence allows for random access. In many situations, however, the
250 elements of the sequence are meant to be read one after the other, in
251 increasing order of their position. Moreover, the elements are meant to be
252 consumed (read) linearly, i.e. just once. This suggests a more efficient
253 implementation where sequences are implemented with state machines that
254 emit the next value and enter a new state every time they are read. Indeed,
255 some programming languages like OCaml differentiate (possibly infinite)
256 lists, that are immutable, from mutable streams whose only access operation
257 yields the head and turns the stream into its tail. Data streams read from
258 the network are a typical example of streams: the previously read values are
259 not automatically memoized and are lost if not saved when read. Files on
260 disk are also usually read via streams to avoid keeping all of them in main
261 memory. Another typical case where streams are used is that of diverging
262 computations: in place of generating at once an infinite sequence of values,
263 a function is turned into a stream and asking the next element of the stream
264 runs one more iteration of the function to produce the next output (often
266 2. if a sequence computes the n-th entry by recursively calling itself on every
267 entry less than n, accessing the n-th entry requires re-computation of all
268 entries in position ≤ n, which is very inefficient.
269 3. by representing an infinite object as a collection of approximations, the
270 structure of the object is lost. This was not evident in the previous
271 examples because in all cases the intrinsic structure of the datatype was
272 just that of being ordered and sequences capture the order well. Imagine,
273 however, that we want to represent an infinite binary tree of elements of
274 type A with the previous technique. We need to associate to each position
275 in the infinite tree an element of type A. A position in the tree is itself
276 a path from the root to the node of interest. Therefore the infinite tree
277 is represented as the function (ℕ → 𝔹) → A where 𝔹 are the booleans and the
278 tree structure is already less clear. Suppose now that the binary tree may
279 not be full, i.e. some nodes can have less than two children. Representing
280 such a tree is definitely harder. We may for example use the data type
281 (N → 𝔹) → option A where None would be associated to the position
282 b1 ... bn if a node in such position does not exist. However, we would need
283 to add the invariant that if b1 ... bn is undefined (i.e. assigned to None),
284 so are all suffixes b1 ... bn b_{n+1} ... b_{n+j}.
286 The previous observations suggest the need for primitive infinite datatypes
287 in the language, usually called coinductive types or codata. Matita allows
288 to declare coinductive type with the same syntax used for inductive types,
289 just replacing the keywork inductive with coinductive. Semantically, the two
290 declarations differ because a coinductive type also contains infinite
291 inhabitants that respect the typechecking rules.
294 (* Example 1 revisited: non terminated streams of elements of type A *)
295 coinductive streamseq (A: Type[0]) : Type[0] ≝
296 sscons: A → streamseq A → streamseq A.
298 (* Coinductive types can be inhabited by infinite data using coinductive
299 definitions, introduced by the keyword let corec. The syntax of let corec
300 definitions is the same of let rec definitions, but for the declarations
301 of the recursive argument. While let rec definitions are recursive definition
302 that are strictly decreasing on the recursive argument, let corec definitions
303 are productive recursive definitions. A recursive definition is productive
304 if, when fully applied to its arguments, it reduces in a finite amount of time
305 to a constructor of a coinductive type.
307 Let's see some simple examples of coinductive definitions of corecursive
310 (* The streamseq 0 0 0 ...
311 Note that all_zeros is not a function and does not have any argument.
312 The definition is clearly productive because it immediately reduces to
313 the constructor sscons. *)
314 let corec all_zeros: streamseq nat ≝ sscons nat 0 all_zeros.
316 (* The streamseq n (n+1) (n+2) ...
317 The definition behaves like an automaton with state n. When the
318 streamseq is pattern matched, the current value n is returned as head
319 of the streamseq and the tail of the streamseq is the automaton with
320 state (S n). Therefore obtaining the n-th tail of the stream requires O(n)
321 operation, but every further access to its value only costs O(1). Moreover,
322 in the future the implementation of Matita could automatically memoize
323 streams so that obtaining the n-th element would also be an O(1) operation
324 if the same element was previously accessed at least once. This is what
325 is currently done in the implementation of the Coq system for example.
327 let corec from_n (n:ℕ) : streamseq nat ≝ sscons … n (from_n (S n)).
329 (* In order to retrieve the n-th element from a streamseq we can write a
330 function recursive over n. *)
331 let rec streamseq_nth (A: Type[0]) (s: streamseq A) (n:ℕ) on n : A ≝
332 match s with [ sscons hd tl ⇒
333 match n with [ O ⇒ hd | S m ⇒ streamseq_nth … tl m ]].
335 (* Any sequence can be turned into the equivalent streamseq and the other
337 let corec streamseq_of_seq (A: Type[0]) (s: seq A) (n:ℕ) : streamseq A ≝
338 sscons … (s n) (streamseq_of_seq A s (S n)).
340 lemma streamseq_of_seq_ok:
341 ∀A:Type[0]. ∀s: seq A. ∀m,n.
342 streamseq_nth A (streamseq_of_seq … s n) m = s (m+n).
343 #A #s #m elim m normalize //
346 definition seq_of_streamseq: ∀A:Type[0]. streamseq A → seq A ≝ streamseq_nth.
348 lemma seq_of_streamseq_ok:
349 ∀A:Type[0]. ∀s: streamseq A. ∀n. seq_of_streamseq … s n = streamseq_nth … s n.
353 (* Example 2 revisited: Real numbers as Cauchy sequences and their addition.
354 We closely follow example 2 replacing sequences with streamseqs.
357 definition Qstreamseq: Type[0] ≝ streamseq Q.
359 definition Qstreamseq_nth ≝ streamseq_nth Q.
361 (* The Cauchy property *)
362 definition Cauchy': Qstreamseq → Prop ≝
363 λR:Qstreamseq. ∀eps. ∃n. ∀i,j. n ≤ i → n ≤ j → Qdist (Qstreamseq_nth R i) (Qstreamseq_nth R j) ≤ eps.
365 (* A real number is an equivalence class of Cauchy sequences. In type theory
366 we can define R' as a setoid whose carrier R_' is the type of Cauchy sequences. *)
367 record R_': Type[0] ≝
369 ; isCauchy': Cauchy' r'
372 (* Two sequences are equal when for every epsilon they are eventually pointwise
373 closer than epsilon. The script is exactly the same already used when we
374 defined R using functions. *)
375 definition R' : setoid ≝
377 (mk_equivalence_relation …
378 (λr1,r2:R_'. ∀eps. ∃n. ∀i. n ≤ i →
379 Qdist (Qstreamseq_nth (r' r1) i) (Qstreamseq_nth (r' r2) i) ≤ eps) …).
380 [ (* transitivity *) #x #y #z #H1 #H2 #eps cases (H1 (Qhalve eps)) #i -H1 #H1
381 cases (H2 (Qhalve eps)) #j -H2 #H2 %{(max i j)} #l #Hmax
382 <(Qplus_Qhalve_Qhalve eps) @transitive_Qleq
383 [3: @(Qleq_Qplus … (H1 l …) (H2 l …)) /2 by le_maxl,le_maxr/
385 | (* symmetry *) #x #y #H #eps cases (H eps) /3 by ex_intro/
386 | (* reflexivity *) #x #eps cases (isCauchy' x eps) /3 by ex_intro/ ]
389 unification hint 0 ≔ ;
391 (* ---------------------------------------- *) ⊢
394 (* The following coercion is used to write r n to extract the n-th approximation
395 from the real number r *)
396 coercion R_to_fun' : ∀r:R'. ℕ → Q ≝ (λr. Qstreamseq_nth (r' r)) on _r:R' to ?.
398 (* Pointwise addition over Qstreamseq defined by corecursion.
399 The definition is productive because, when Rplus_streamseq is applied to
400 two closed values of type Qstreamseq, it will reduce to sscons. *)
401 let corec Rplus_streamseq (x:Qstreamseq) (y:Qstreamseq) : Qstreamseq ≝
402 match x with [ sscons hdx tlx ⇒
403 match y with [ sscons hdy tly ⇒
404 sscons … (hdx + hdy) (Rplus_streamseq tlx tly) ]].
406 (* The following lemma was for free using sequences. In the case of streamseqs
407 it must be proved by induction over the index because Qstreamseq_nth is defined by
408 recursion over the index. *)
409 lemma Qstreamseq_nth_Rplus_streamseq:
411 Qstreamseq_nth (Rplus_streamseq x y) i = Qstreamseq_nth x i + Qstreamseq_nth y i.
412 #i elim i [2: #j #IH] * #xhd #xtl * #yhd #ytl // normalize @IH
415 (* The proof that the resulting sequence is Cauchy is exactly the same we
416 used for sequences, up to two applications of the previous lemma. *)
417 definition Rplus_': R_' → R_' → R_' ≝
418 λr1,r2. mk_R_' (Rplus_streamseq (r' r1) (r' r2)) ….
420 cases (isCauchy' r1 (Qhalve eps)) #n1 #H1
421 cases (isCauchy' r2 (Qhalve eps)) #n2 #H2
422 %{(max n1 n2)} #i #j #K1 #K2
423 >Qstreamseq_nth_Rplus_streamseq >Qstreamseq_nth_Rplus_streamseq
424 @(transitive_Qleq … (Qdist_Qplus …))
425 <(Qplus_Qhalve_Qhalve eps) @Qleq_Qplus [@H1 @le_maxl | @H2 @le_maxr]
429 (* We lift Rplus_' to a morphism by proving that it respects the equality for
430 real numbers. The script is exactly the same we used to lift Rplus_, but for
431 two applications of Qstreamseq_nth_Rplus_streamseq. *)
432 definition Rplus': R' ⤞ R' ⤞ R' ≝
433 mk_bin_morphism … Rplus_' ….
434 #x1 #x2 #y1 #y2 #Hx #Hy #eps
435 cases (Hx (Qhalve eps)) #i -Hx #Hx
436 cases (Hy (Qhalve eps)) #j -Hy #Hy
437 %{(max i j)} #l #Hmax <(Qplus_Qhalve_Qhalve eps) @transitive_Qleq
438 [3: @(Qleq_Qplus … (Hx l …) (Hy l …)) /2 by le_maxl,le_maxr/
439 |2: >Qstreamseq_nth_Rplus_streamseq >Qstreamseq_nth_Rplus_streamseq // ]
442 (***** Intermezzo: the dynamics of coinductive data ********)
444 (* Let corec definitions, like let rec definitions, are a form of recursive
445 definition where the definiens occurs in the definiendum. Matita compares
446 types up to reduction and reduction always allows the expansion of non recursive
447 definitions. If it also allowed the expansion of recursive definitions, reduction
448 could diverge and type checking would become undecidable. For example,
449 we defined all_zeros as "sscons … 0 all_zeros". If the system expanded all
450 occurrences of all_zeros, it would expand it forever to
451 "sscons … 0 (sscons … 0 (sscons … 0 …))".
453 In order to avoid divergence, recursive definitions are only expanded when a
454 certain condition is met. In the case of a let-rec defined function f that is
455 recursive on its n-th argument, f is only expanded when it occurs in an
456 application (f t1 ... tn ...) and tn is (the application of) a constructor.
457 Termination is guaranteed by the combination of this restriction and f being
458 guarded by destructors: the application (f t1 ... tn ...) can reduce to a term
459 that contains another application (f t1' ... tn' ...) but the size of tn'
460 (roughly the number of nested constructors) will be smaller than the size of tn
461 eventually leading to termination.
463 Dual restrictions are put on let corec definitions. If f is a let-rec defined
464 term, f is only expanded when it occurs in the term "match f t1 ... tn with ...".
465 To better see the duality, that is not syntactically perfect, note that: in
466 the recursive case f destructs terms and is expanded only when applied to a
467 constructor; in the co-recursive case f constructs terms and is expanded only
468 when it becomes argument of the match destructor. Termination is guaranteed
469 by the combination of this restriction and f being productive: the term
470 "match f t1 ... tn ... with" will reduce in a finite amount of time to
471 a match applied to a constructor, whose reduction can expose another application
472 of f, but not another "match f t1' .. tn' ... width". Therefore, since no
473 new matches around f can be created by reduction, the number of
474 destructors that surrounds the application of f decreases at every step,
475 eventually leading to termination.
477 Even if a coinductively defined f does not reduce in every context to its
478 definiendum, it is possible to prove that the definiens is equal to its
479 definiendum. The trick is to prove first an eta-expansion lemma for the
480 inductive type that states that an inhabitant of the inductive type is
481 equal to the one obtained destructing and rebuilding it via a match. The proof
482 is simply by cases over the inhabitant. Let's see an example. *)
485 ∀A:Type[0]. ∀s: streamseq A.
486 match s with [ sscons hd tl ⇒ sscons … hd tl ] = s.
490 (* In order to prove now that the definiens of all_zeros is equal to its
491 definiendum, it suffices to rewrite it using the eta_streamseq lemma in order
492 to insert around the definiens the match destructor that triggers its
494 lemma all_zeros_expansion: all_zeros = sscons … 0 all_zeros.
495 <(eta_streamseq ? all_zeros) in ⊢ (??%?); //
498 (* Expansions lemmas as the one just presented are almost always required to
499 progress in non trivial proofs, as we will see in the next example. Instead
500 the equivalent expansions lemmas for let-rec definitions are rarely required.
503 (* Example 3 revisited: traces of a program. *)
505 (* A diverging trace is a streamseq of states such that the n+1-th state is
506 obtained executing one step from the n-th state. The definition of
507 div_well_formed' is the same we already used for sequences, but on
510 definition div_well_formed' : streamseq state → Prop ≝
512 ∀n. next (streamseq_nth … s n) (streamseq_nth … s (S n)).
514 record div_trace': Type[0] ≝
515 { div_tr':> streamseq state
516 ; div_well_formed'': div_well_formed' div_tr'
519 (* The well formedness predicate over streamseq can also be redefined using as a
520 coinductive predicate. A streamseq of states is well formed if the second
521 element is the next of the first and the stream without the first element
522 is recursively well formed. *)
523 coinductive div_well_formed_co: streamseq state → Prop ≝
525 ∀hd1:state. ∀hd2:state. ∀tl:streamseq state.
526 next hd1 hd2 → div_well_formed_co (sscons … hd2 tl) →
527 div_well_formed_co (sscons … hd1 (sscons … hd2 tl)).
529 (* Note that Matita automatically proves the inversion principles for every
530 coinductive type, but no general coinduction principle. That means that
531 the elim tactic does not work when applied to a coinductive type. Inversion
532 and cases are the only ways to eliminate a coinductive hypothesis. *)
534 (* A proof of div_well_formed cannot be built stacking a finite
535 number of constructors. The type can only be inhabited by a coinductive
536 definition. As an example, we show the equivalence between the two
537 definitions of well formedness for streamseqs. *)
539 (* A div_well_formed' stream is also div_well_formed_co. We write the proof
540 term explicitly, omitting the subterms that prove "next hd1 hd2" and
541 "div_well_formed' (sscond … hd2 tl)". Therefore we will obtain two proof
542 obligations. The given proof term is productive: if we apply it to a closed
543 term of type streamseq state and a proof that it is well formed, the two
544 matches in head position will reduce and the lambda-abstraction will be
545 consumed, exposing the is_next constructor. *)
547 let corec div_well_formed_to_div_well_formed_co
548 (s: streamseq state): div_well_formed' s → div_well_formed_co s ≝
549 match s with [ sscons hd1 tl1 ⇒
550 match tl1 with [ sscons hd2 tl ⇒
551 λH: div_well_formed' (sscons … hd1 (sscons … hd2 tl)).
552 is_next … (div_well_formed_to_div_well_formed_co (sscons … hd2 tl) …) ]].
553 [ (* First proof obligation: next hd1 hd2 *) @(H 0)
554 | (* Second proof obligation: div_well_formed' (sscons … hd2 tl) *) @(λn. H (S n)) ]
557 (* A div_well_formed_co stream is also div_well_formed'. This time the proof is
558 by induction over the index and inversion over the div_well_formed_co
560 theorem div_well_formed_co_to_div_well_formed:
561 ∀s: streamseq state. div_well_formed_co s → div_well_formed' s.
562 #s #H #n lapply H -H lapply s -s elim n [2: #m #IH]
563 * #hd1 * #hd2 #tl normalize #H inversion H #hd1' #hd2' #tl' #Hnext #Hwf
567 (* Like for sequences, because of undecidability of termination there is no
568 function that given an initial state returns the diverging trace if the program
569 diverges or fails in case of error. We need a new data type to represent a
570 possibly infinite, possibly terminated stream of elements. Such data type is
571 usually called stream and can be defined elegantly as a coinductive type. *)
572 coinductive stream (A: Type[0]) : Type[0] ≝
574 | scons: A → stream A → stream A.
576 (* The following lemma will be used to unblock blocked reductions, as
577 previously explained for eta_streamseq. *)
579 ∀A:Type[0]. ∀s: stream A.
580 match s with [ snil ⇒ snil … | scons hd tl ⇒ scons … hd tl ] = s.
584 (* The definition of trace based on streams is more natural than that based
585 on sequences of optional states because there is no need of the invariant that
586 a None state is followed only by None states (to represent a terminated
587 sequence). Indeed, this is the first example where working with coinductive
588 types seems to yield advantages in terms of simplicity of the formalization.
589 However, in order to give the definition we first need to coinductively define
590 the well_formedness predicate, whose definition is more complex than the
592 coinductive well_formed': stream state → Prop ≝
593 wf_snil: ∀s. step s = None … → well_formed' (scons … s (snil …))
596 step hd1 = Some … hd2 →
597 well_formed' (scons … hd2 tl) →
598 well_formed' (scons … hd1 (scons … hd2 tl)).
600 (* Note: we could have equivalently defined well_formed' avoiding coinduction
601 by defining a recursive function to retrieve the n-th element of the stream,
602 if any. From now on we will stick to coinductive predicates only to show more
603 examples of usage of coinduction. In a formalization, however, it is always
604 better to explore several alternatives and see which ones work best for the
607 record trace': Type[0] ≝
609 ; well_formed'': well_formed' tr'
612 (* The trace is diverging if every state is not final. Again, we show here
613 a coinductive definition. *)
614 coinductive diverging': stream state → Prop ≝
615 mk_diverging': ∀hd,tl. diverging' tl → diverging' (scons … hd tl).
617 (* The two coinductive definitions of diverging traces are equivalent.
618 To state the two results we first need a function to retrieve the head
619 from traces and diverging traces. *)
620 definition head_of_streamseq: ∀A:Type[0]. streamseq A → A ≝
621 λA,s. match s with [ sscons hd _ ⇒ hd ].
623 definition head_of_stream: ∀A:Type[0]. stream A → option A ≝
624 λA,s. match s with [ snil ⇒ None … | scons hd _ ⇒ Some … hd ].
626 (* A streamseq can be extracted from a diverging stream using corecursion. *)
627 let corec mk_diverging_trace_to_div_trace'
628 (s: stream state) : diverging' s → streamseq state ≝
629 match s return λs. diverging' s → streamseq state
631 [ snil ⇒ λabs: diverging' (snil …). ?
632 | scons hd tl ⇒ λH. sscons ? hd (mk_diverging_trace_to_div_trace' tl …) ].
633 [ cases (?:False) inversion abs #hd #tl #_ #abs' destruct
634 | inversion H #hd' #tl' #K #eq destruct @K ]
637 (* An expansion lemma will be needed soon. *)
638 lemma mk_diverging_trace_to_div_trace_expansion:
640 mk_diverging_trace_to_div_trace' (scons state hd tl) H =
641 sscons … hd (mk_diverging_trace_to_div_trace' tl K).
642 #hd #tl #H cases (eta_streamseq … (mk_diverging_trace_to_div_trace' ??)) /2/
645 (* CSC: BUG CHE APPARE NEL PROSSIMO LEMMA AL MOMENTO DELLA QED. IL DEMONE
646 SERVE PER DEBUGGARE *)
649 (* To complete the proof we need a final lemma: streamseqs extracted from
650 well formed diverging streams are well formed too. The definition is mostly
651 interactive because we need to use the expansion lemma above to rewrite
652 the type of the scons branch. Otherwise, Matita rejects the term as ill-typed *)
653 let corec div_well_formed_co_mk_diverging_trace_to_div_trace (t : stream state) :
655 ∀H:diverging' t. div_well_formed_co (mk_diverging_trace_to_div_trace' t H) ≝
656 match t return λt. well_formed' t → diverging' t → ?
659 | scons hd tl ⇒ λW.λH. ? ].
660 [ cases (?:False) inversion abs #hd #tl #_ #eq destruct
661 | cases (mk_diverging_trace_to_div_trace_expansion … H) #H' #eq
662 lapply (sym_eq ??? … eq) #Req cases Req -Req -eq -H
664 [ #_ #abs cases (?:False) inversion abs #hd #tl #_ #eq destruct
666 cases (mk_diverging_trace_to_div_trace_expansion … H) #K #eq >eq
667 inversion W [ #s #_ #abs destruct ]
668 #hd1' #hd2' #tl' #eq1 #wf #eq2 lapply eq1
669 cut (hd=hd1' ∧ hd2 = hd2' ∧ tl=tl') [ cases daemon (* destruct /3/ *) ]
673 | cases daemon (*<eq @div_well_formed_co_mk_diverging_trace_to_div_trace cases daemon (*//*) ]]]
676 theorem diverging_trace_to_div_trace':
677 ∀t: trace'. diverging' t → ∃d: div_trace'.
678 head_of_stream … t = Some … (head_of_streamseq … d).
680 [ %{(mk_diverging_trace_to_div_trace' … H)}
681 @div_well_formed_co_to_div_well_formed
682 @div_well_formed_co_mk_diverging_trace_to_div_trace
684 | cases t in H; * normalize // #abs cases (?:False) inversion abs
685 [ #s #_ #eq destruct | #hd1 #hd2 #tl #_ #_ #eq destruct ]]
688 (* A stream can be extracted from a streamseq using corecursion. *)
689 let corec stream_of_streamseq (A: Type[0]) (s: streamseq A) : stream A ≝
690 match s with [ sscons hd tl ⇒ scons … hd (stream_of_streamseq … tl) ].
692 (* We need again an expansion lemma to typecheck the proof that the resulting
693 stream is divergent. *)
694 lemma stream_of_streamseq_expansion:
696 stream_of_streamseq A (sscons … hd tl) = scons … hd (stream_of_streamseq … tl).
697 #A #hd #tl <(eta_stream … (stream_of_streamseq …)) //
700 (* The proof that the resulting stream is diverging also need corecursion.*)
701 let corec diverging_stream_of_streamseq (s: streamseq state) :
702 diverging' (stream_of_streamseq … s) ≝
703 match s return λs. diverging' (stream_of_streamseq … s)
704 with [ sscons hd tl ⇒ ? ].
705 >stream_of_streamseq_expansion % //
708 let corec well_formed_stream_of_streamseq (d: streamseq state) :
709 div_well_formed' … d → well_formed' (stream_of_streamseq state d) ≝
711 return λd. div_well_formed' d → ?
712 with [ sscons hd1 tl ⇒
713 match tl return λtl. div_well_formed' (sscons … tl) → ?
714 with [ sscons hd2 tl2 ⇒ λH.? ]].
715 >stream_of_streamseq_expansion >stream_of_streamseq_expansion %2
716 [2: <stream_of_streamseq_expansion @well_formed_stream_of_streamseq
718 | @next_step @(H O) ]
721 theorem div_trace_to_diverging_trace':
722 ∀d: div_trace'. ∃t: trace'. diverging' t ∧
723 head_of_stream … t = Some … (head_of_streamseq … d).
724 #d %{(mk_trace' (stream_of_streamseq … d) …)}
725 [ /2/ | % // cases d * // ]
728 (******** How to compare coinductive types *********)
730 (* Inhabitants of inductive types are compared using Leibniz's equality that,
731 on closed terms, coincides with convertibility. Two closed inductive terms
732 are equal iff they reduce to the same normal form.
734 Because of the lazy evaluation of coinductively defined terms, conversion
735 does not behave as expected on inhabitants of coinductive types. For example,
736 the following two definitions, both in normal form, produce the same
737 streamseq 0,1,0,1,… but are not equal because the normal forms are
738 syntactically different. *)
740 let corec zero_one_streamseq1: streamseq ℕ ≝
741 sscons … 0 (sscons … 1 zero_one_streamseq1).
743 let corec one_zero_streamseq: streamseq ℕ ≝
744 sscons … 1 (sscons … 0 one_zero_streamseq).
746 definition zero_one_streamseq2: streamseq ℕ ≝ sscons … 0 one_zero_streamseq.
748 (* In place of Leibniz equality, the right notion to compare coinductive terms
749 is bisimulation. Two terms t1,t2 are bisimilar if every observation on t1 can
750 be performed on t2 as well, and the observed subterms are co-recursively
751 bisimilar. In practice two coinductive terms are bisimilar if they are the same
752 constructor applied to bisimilar coinductive subterms.
754 We define bisimilarity for streamseqs using a coinductive predicate. *)
755 coinductive ss_bisimilar (A: Type[0]) : streamseq A → streamseq A → Prop ≝
758 ss_bisimilar … tl1 tl2 →
759 ss_bisimilar … (sscons … x tl1) (sscons … x tl2).
761 (* The two streams above can be proved to be bisimilar. By using the
762 eta_streamseq trick twice, we expand both definitions once so to obtain the
763 new proof obligation 0,1,zero_one_streamseq1 = 0,1,zero_one_streamseq2.
764 Then we apply twice the sscons_bisim constructor to consume the leading 0 and 1,
765 finding again the original goal. Finally we conclude with the coinductive
766 hypothesis. The proof is productive because, after the two rewriting, it
767 reduces to two applications of the sscons_bisim constructor, immediately
768 followed by the recursive call. *)
769 let corec zero_one_streamseq_eq: ss_bisimilar … zero_one_streamseq1 zero_one_streamseq2 ≝
771 <(eta_streamseq … zero_one_streamseq1) normalize
772 <(eta_streamseq … one_zero_streamseq) normalize
773 % % @zero_one_streamseq_eq
776 (* We can finally turn streamseqs into a setoid and lift every operation on
777 streamseqs to morphisms. We first prove reflexivity, symmetry and transitivity
778 of bisimulation because each proof must be given using let corec. *)
779 let corec reflexive_ss_bisimilar (A: Type[0]): reflexive … (ss_bisimilar A) ≝ ?.
780 * #hd #tl % @reflexive_ss_bisimilar
783 let corec symmetric_ss_bisimilar (A: Type[0]): symmetric … (ss_bisimilar A) ≝ ?.
784 * #hd1 #tl1 * #hd2 #tl2 * #hd #tl1' #tl2' #H % @symmetric_ss_bisimilar @H
787 (* In the proof of transitivity we face a technical problem. After inverting one
788 of the bisimilarity hypothesis we are left with an equation of the form
789 sscons … hd1 tl1 = sscons … hd2 tl2 and we need to extract hd1 = hd2 and
790 tl1 = tl2 to conclude the proof. The destruct tactic does exactly this, but
791 it produces a proof term that is not recognized to be productive by Matita.
792 The trick is to cut the two equalities and to use destruct to prove them.
793 In this way the destruct tactic is used only in a side proof inside which there
794 is no recursive call, and the whole proof term is recognized to be productive. *)
795 let corec transitive_ss_bisimilar (A: Type[0]): transitive … (ss_bisimilar A) ≝ ?.
796 * #hd1 #tl1 * #hd2 #tl2 * #hd3 #tl3
797 * #hd #tl1' #tl2' #H1
798 #H inversion H #hd' #tl1'' #tl2'' -H #H #EQ1 #_
799 cut (hd=hd' ∧ tl1''=tl2') [ destruct /2/ ] ** #EQ % @transitive_ss_bisimilar //
802 definition STREAMSEQ: Type[0] → setoid ≝
804 mk_setoid (streamseq A)
805 (mk_equivalence_relation … (ss_bisimilar A) …).
809 unification hint 0 ≔ A:Type[0];
811 (* ---------------------------------------- *) ⊢
812 streamseq A ≡ carrier X.
814 (* As an example, we lift streamseq_nth to a morphism. *)
815 definition STREAMSEQ_NTH: ∀A: Type[0]. STREAMSEQ A ⤞ (LEIBNIZ ℕ) ⤞ (LEIBNIZ A) ≝
816 λA. mk_bin_morphism ??? (streamseq_nth A) ….
817 #x1 #x2 #n1 #n2 #bisim * lapply bisim -bisim lapply x2 -x2 lapply x1 -x1 -n2 elim n1
818 [ #x1 #x2 #H inversion H //
819 | #m #IH #x1 #x2 #H inversion H #hd #tl1 #tl2 #bisim #EQ1 #EQ2 destruct @IH //]
822 (* Working with setoids introduce technical complications that one would rather
823 avoid. The alternative encoding of streams via sequences doen not solve the
824 issue. Sequences are functions and, to capture the mathematical meaning of
825 equality for sequences, functions need to be compare using functional
826 extensionality. Two functions are extensionally equal when they are pointiwse
827 equal, i.e. they map equal inputs to the same outputs. Intensional equality of
828 functions, instead, just compares the two codes.
830 For example, the next two enumerations 0,1,2,… are extensionally, but not
831 intensionally equal. *)
832 definition enum_N1: seq ℕ ≝ λi. i.
833 definition enum_N2: seq ℕ ≝ λi. i+0.
835 (* Functional extensionality is defined in the standard library of Matita as
837 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
838 λA,B.λf,g.∀a.f a = g a.
840 (* The proof that the two sequences above are extensionally equal is trivial. *)
841 lemma enum_N_equal: exteqF … enum_N1 enum_N2.
845 (* Like for bisimulation, to work sistematically with functional extensionality
846 we need to turn the type of sequences into a setoid. The two alternatives are
847 actually equivalent with respect to this issue. *)
849 (******* Generic construction principles *******)
851 (* When an inductive type is defined Matita automatically
852 proves a generic elimination principle using a recursive definition. Later the
853 user can apply the generic eliminator in the middle of a proof, without the
854 need to make a lemma and prove it using a let rec.
856 For example, the principle generated for a list is the following:
858 ∀A:Type[0]. ∀P: A → Prop.
859 P (nil …) → (∀hd:A. ∀tl: list A. P tl → P (hd::tl)) →
862 Here the predicate P is dependent, i.e. it is not just a proposition, but
863 a proposition indexed by the list we are analysing.
865 The corresponding non dependent principle is:
867 ∀A:Type[0]. ∀P: Prop.
868 P → (∀hd:A. ∀tl: list A. P → P) →
871 that we can rewrite up to currification as
873 ∀A:Type[0]. ∀P: Prop.
874 ((unit + A × list A × P) → P) →
877 and, turning the recursor into an iterator, to the simpler form
879 ∀A:Type[0]. ∀P: Prop.
880 ((unit + A × P) → P) →
883 Thinking of a list as the least fixpoint of the equation
885 list A = unit + A × list A
887 The above principle says that we can prove P as soon as we can prove P for
888 every possible shape of the list, replacing sublists (list A) with the
889 result P of recursive calls of the iterator.
891 Streams are the greatest fixpoint of the same equation
893 stream A = unit + A × stream A
895 Dualizing the idea of a generic destructor for list, we obtain the type of the
896 generic constructor for streams:
898 ∀A:Type[0]. ∀P: Prop.
899 (P → (unit + A × P)) →
902 The above principle says that we can build a stream from a proof of P as soon
903 as we can observe from P what shape the stream has and what P will be used to
904 generate the reamining of the stream. The principle is indeed easily provable
907 let corec stream_coind (A: Type[0]) (P: Prop) (H: P → Sum unit (A × P))
911 | inr cpl ⇒ let 〈hd,p'〉 ≝ cpl in scons A hd (stream_coind A P H p') ].
913 (* At the moment Matita does not automatically prove any generic construction
914 principle. One reason is that the type of the generated principles is less
915 informative than that for elimination principles. The problem is that in the
916 type theory of Matita it is not possible to generalize the above type to a
917 dependent version, to obtain the exact dual of the elimination principle.
918 In case of the elimination principle, the type P depends on the value of the
919 input, and the principle proves the dependent product ∀l: list A. P A.
920 In the case of the introduction principle, the output is P → list A.
921 To obtain a dependent version, we would need a dual of the dependent product
922 such that the type of the input is dependent on the value of the output: a
923 notion that is not even meaningful when the function is not injective. *)
925 (* AGGIUNGERE SPIEGAZIONE SU PRODUTTIVITA' *)
927 (* AGGIUNGERE ESEMPI DI SEMANTICA OPERAZIONE BIG STEP PER LA DIVERGENZA;
928 DI PROPRIETA' DI SAFETY;
929 DI TOPOLOGIE COINDUTTIVAMENTE GENERATE? *)
931 (* ################## COME SPIEGARLO QUI? ####################### *)