2 Coinductive Types and Predicates
5 include "arithmetics/nat.ma".
6 include "basics/types.ma".
7 include "basics/lists/list.ma".
9 (* The only primitive data types of Matita are dependent products and universes.
10 So far every other user defined data type has been an inductive type. An
11 inductive type is declared by giving its list of constructors (or introduction
12 rules in the case of predicates). An inhabitant of an inductive type is obtained
13 composing together a finite number of constructors and data of other types,
14 according to the type of the constructors. Therefore all inhabitants of inductive
15 types are essentially finite objects. Natural numbers, lists, trees, states of
16 a DFA, letters of an alphabet are all finite and can be defined inductively.
18 If you think of an inhabitant of an inductive type as a tree of a certain shape,
19 whose nodes are constructors, the only trees can be represented are trees of
20 finite height. Note, however, that it is possible to have trees of infinite
21 width by putting in the argument of a constructor of a type I an enumeration
22 of elements of I (e.g. ℕ → I). *)
24 (* Example of an infinitely branching tree of elements of type A stored in
26 inductive infbrtree (A: Type[0]) : Type[0] ≝
28 | Node: A → (ℕ → infbrtree A) → infbrtree A.
30 (* Example: the tree of natural numbers whose root holds 0 and has as children
32 example infbrtree_ex ≝ Node ℕ 0 (λn. Node ℕ (S n) (λ_.Nil ℕ)).
34 (*** Infinite data types via functions ***)
36 (* In mathematics and less frequently in computer science there is the need to
37 also represent and manipulate types of infinite objects. Typical examples are:
38 sequences, real numbers (a special case of sequences), data streams (e.g. as
39 read from a network interface), traces of diverging computations of a program,
40 etc. One possible representation, used in mathematics since a long time, is
41 to describe an infinite object by means of an infinite collection of
42 approximations (also called observations). Often, the infinite collection can
43 be structured in a sequence, identified as a function from the domain of natural
46 (* Example 1: sequences of elements of type A *)
47 definition seq : Type[0] → Type[0] ≝ λA:Type[0]. ℕ → A.
49 (* Example 2: Real numbers as Cauchy sequences and their addition. *)
50 (* First we axiomatize the relevant properties of rational numbers. *)
52 axiom Qdist: Q → Q → Q.
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.
65 (* A sequence of rationals. *)
66 definition Qseq: Type[0] ≝ seq Q.
68 (* The Cauchy property *)
69 definition Cauchy: Qseq → Prop ≝
70 λR:Qseq. ∀eps. ∃n. ∀i,j. n ≤ i → n ≤ j → Qdist (R i) (R j) ≤ eps.
72 (* A real number is an equivalence class of Cauchy sequences. Here we just
73 define the carrier, omitting the necessary equivalence relation for the
80 (* The following coercion is used to write r n to extract the n-th approximation
81 from the real number r *)
82 coercion R_to_fun : ∀r:R. ℕ → Q ≝ r on _r:R to ?.
84 (* Adding two real numbers just requires pointwise addition of the
85 approximations. The proof that the resulting sequence is Cauchy is the standard
86 one: to obtain an approximation up to eps it is necessary to approximate both
87 summands up to eps/2. The proof that the function is well defined w.r.t. the
88 omitted equivalence relation is also omitted. *)
89 definition Rplus: R → R → R ≝
90 λr1,r2. mk_R (λn. r1 n + r2 n) ….
92 cases (isCauchy r1 (Qhalve eps)) #n1 #H1
93 cases (isCauchy r2 (Qhalve eps)) #n2 #H2
94 %{(max n1 n2)} #i #j #K1 #K2 @(transitive_Qleq … (Qdist_Qplus …))
95 <(Qplus_Qhalve_Qhalve eps) @Qleq_Qplus [@H1 @le_maxl | @H2 @le_maxr]
99 (* Example 3: traces of a program *)
100 (* Let us introduce a very simple programming language whose instructions
101 can test and set a single implicit variable. *)
102 inductive instr: Type[0] ≝
103 p_set: ℕ → instr (* sets the variable to a constant *)
104 | p_incr: instr (* increments the variable *)
105 | p_while: list instr → instr. (* repeats until the variable is 0 *)
107 (* The status of a program as the values of the variable and the list of
108 instructions to be executed. *)
109 definition state ≝ ℕ × (list instr).
111 (* The transition function from a state to the next one. *)
112 inductive next: state → state → Prop ≝
113 n_set: ∀n,k,o. next 〈o,(p_set n)::k〉 〈n,k〉
114 | n_incr: ∀k,o. next 〈o,p_incr::k〉 〈S o,k〉
115 | n_while_exit: ∀b,k. next 〈0,(p_while b)::k〉 〈0,k〉
116 | n_while_loop: ∀b,k,o. next 〈S o,(p_while b)::k〉 〈S o,b@(p_while b)::k〉.
118 (* A diverging trace is a sequence of states such that the n+1-th state is
119 obtained executing one step from the n-th state *)
120 record div_trace: Type[0] ≝
122 ; div_well_formed: ∀n. next (div_tr n) (div_tr (S n))
125 (* The previous definition of trace is not very computable: we cannot write
126 a program that given an initial state returns its trace. To write that function,
127 we first write a computable version of next, called step. *)
128 definition step: state → option state ≝
139 | S p ⇒ 〈S p,b@(p_while b)::k〉 ]]].
141 theorem step_next: ∀o,n. step o = Some … n → next o n.
142 * #o * [ #n normalize #abs destruct ]
146 | #b #tl * #n' #tl' cases o normalize [2: #r]]
150 theorem next_step: ∀o,n. next o n → step o = Some … n.
151 * #o #k * #n #k' #H inversion H normalize
158 (* Termination is the archetipal undecidable problem. Therefore there is no
159 function that given an initial state returns the diverging trace if the program
160 diverges or fails in case of error. The best we can do is to give an alternative
161 definition of trace that captures both diverging and converging computations. *)
162 record trace: Type[0] ≝
163 { tr: seq (option state)
164 ; well_formed: ∀n,s. tr n = Some … s → tr (S n) = step s
167 (* The trace is diverging if every state is not final. *)
168 definition diverging: trace → Prop ≝
169 λt. ∀n. tr t n ≠ None ?.
171 (* The two definitions of diverging traces are equivalent. *)
172 theorem div_trace_to_diverging_trace:
173 ∀d: div_trace. ∃t: trace. diverging t ∧ tr t 0 = Some … (div_tr d 0).
174 #d %{(mk_trace (λn.Some ? (div_tr d n)) …)}
175 [2: % // #n % #abs destruct
176 | #n #s #EQ destruct lapply (div_well_formed d n) /2 by div_well_formed, next_step/ ]
179 theorem diverging_trace_to_div_trace:
180 ∀t: trace. diverging t → ∃d: div_trace. tr t 0 = Some … (div_tr d 0).
182 [ % [ #n lapply (H n) -H cases (tr t n) [ * #abs cases (abs …) // ] #s #_ @s
183 | #n lapply (well_formed t n)
184 lapply (H n) cases (tr t n) normalize [ * #abs cases (abs …) // ]
185 * #o #k #_ lapply (H (S n)) -H
186 cases (tr t (S n)) normalize
187 [ * #abs cases (abs …) // ] * #o' #k' #_ #EQ lapply (EQ … (refl …)) -EQ
188 normalize cases k normalize [ #abs destruct ] #hd #tl #EQ destruct -EQ
190 | lapply (H O) -H cases (tr t O) [ * #abs cases (abs …) // ] // ]
193 (* However, given an initial state we can always compute a trace.
194 Note that every time the n-th element of the trace is accessed, all the
195 elements in position ≤ n are computed too. *)
196 let rec compute_trace_seq (s:state) (n:nat) on n : option state ≝
200 match compute_trace_seq s m with
202 | Some o ⇒ step o ]].
204 definition compute_trace: ∀s:state. Σt:trace. tr t 0 = Some … s.
206 [ %{(compute_trace_seq s)}
207 #n #o elim n [ whd in ⊢ (??%? → ??%?); #EQ destruct // ]
208 -n #n #_ #H whd in ; whd in ⊢ (??%?); >H //
212 (*** Infinite data types as coinductive types ***)
214 (* All the previous examples were handled very easily via sequences
215 declared as functions. A few critics can be made to this approach though:
216 1. the sequence allows for random access. In many situations, however, the
217 elements of the sequence are meant to be read one after the other, in
218 increasing order of their position. Moreover, the elements are meant to be
219 consumed (read) linearly, i.e. just once. This suggests a more efficient
220 implementation where sequences are implemented with state machines that
221 emit the next value and enter a new state every time they are read. Indeed,
222 some programming languages like OCaml differentiate (possibly infinite)
223 lists, that are immutable, from mutable streams whose only access operation
224 yields the head and turns the stream into its tail. Data streams read from
225 the network are a typical example of streams: the previously read values are
226 not automatically memoized and are lost if not saved when read. Files on
227 disk are also usually read via streams to avoid keeping all of them in main
228 memory. Another typical case where streams are used is that of diverging
229 computations: in place of generating at once an infinite sequence of values,
230 a function is turned into a stream and asking the next element of the stream
231 runs one more iteration of the function to produce the next output (often
233 2. if a sequence computes the n-th entry by recursively calling itself on every
234 entry less than n, accessing the n-th entry requires re-computation of all
235 entries in position ≤ n, which is very inefficient.
236 3. by representing an infinite object as a collection of approximations, the
237 structure of the object is lost. This was not evident in the previous
238 examples because in all cases the intrinsic structure of the datatype was
239 just that of being ordered and sequences capture the order well. Imagine,
240 however, that we want to represent an infinite binary tree of elements of
241 type A with the previous technique. We need to associate to each position
242 in the infinite tree an element of type A. A position in the tree is itself
243 a path from the root to the node of interest. Therefore the infinite tree
244 is represented as the function (ℕ → 𝔹) → A where 𝔹 are the booleans and the
245 tree structure is already less clear. Suppose now that the binary tree may
246 not be full, i.e. some nodes can have less than two children. Representing
247 such a tree is definitely harder. We may for example use the data type
248 (N → 𝔹) → option A where None would be associated to the position
249 b1 ... bn if a node in such position does not exist. However, we would need
250 to add the invariant that if b1 ... bn is undefined (i.e. assigned to None),
251 so are all suffixes b1 ... bn b_{n+1} ... b_{n+j}.
253 The previous observations suggest the need for primitive infinite datatypes
254 in the language, usually called coinductive types or codata. Matita allows
255 to declare coinductive type with the same syntax used for inductive types,
256 just replacing the keywork inductive with coinductive. Semantically, the two
257 declarations differ because a coinductive type also contains infinite
258 inhabitants that respect the typechecking rules.
261 (* Example 1 revisited: non terminated streams of elements of type A *)
262 coinductive streamseq (A: Type[0]) : Type[0] ≝
263 sscons: A → streamseq A → streamseq A.
265 (* Coinductive types can be inhabited by infinite data using coinductive
266 definitions, introduced by the keyword let corec. The syntax of let corec
267 definitions is the same of let rec definitions, but for the declarations
268 of the recursive argument. While let rec definitions are recursive definition
269 that are strictly decreasing on the recursive argument, let corec definitions
270 are productive recursive definitions. A recursive definition is productive
271 if, when fully applied to its arguments, it reduces in a finite amount of time
272 to a constructor of a coinductive type.
274 Let's see some simple examples of coinductive definitions of corecursive
277 (* The streamseq 0 0 0 ...
278 Note that all_zeros is not a function and does not have any argument.
279 The definition is clearly productive because it immediately reduces to
280 the constructor sscons. *)
281 let corec all_zeros: streamseq nat ≝ sscons nat 0 all_zeros.
283 (* The streamseq n (n+1) (n+2) ...
284 The definition behaves like an automaton with state n. When the
285 streamseq is pattern matched, the current value n is returned as head
286 of the streamseq and the tail of the streamseq is the automaton with
287 state (S n). Therefore obtaining the n-th tail of the stream requires O(n)
288 operation, but every further access to its value only costs O(1). Moreover,
289 in the future the implementation of Matita could automatically memoize
290 streams so that obtaining the n-th element would also be an O(1) operation
291 if the same element was previously accessed at least once. This is what
292 is currently done in the implementation of the Coq system for example.
294 let corec from_n (n:ℕ) : streamseq nat ≝ sscons … n (from_n (S n)).
296 (* In order to retrieve the n-th element from a streamseq we can write a
297 function recursive over n. *)
298 let rec streamseq_nth (A: Type[0]) (s: streamseq A) (n:ℕ) on n : A ≝
299 match s with [ sscons hd tl ⇒
300 match n with [ O ⇒ hd | S m ⇒ streamseq_nth … tl m ]].
302 (* Any sequence can be turned into the equivalent streamseq and the other
304 let corec streamseq_of_seq (A: Type[0]) (s: seq A) (n:ℕ) : streamseq A ≝
305 sscons … (s n) (streamseq_of_seq A s (S n)).
307 lemma streamseq_of_seq_ok:
308 ∀A:Type[0]. ∀s: seq A. ∀m,n.
309 streamseq_nth A (streamseq_of_seq … s n) m = s (m+n).
310 #A #s #m elim m normalize //
313 definition seq_of_streamseq: ∀A:Type[0]. streamseq A → seq A ≝ streamseq_nth.
315 lemma seq_of_streamseq_ok:
316 ∀A:Type[0]. ∀s: streamseq A. ∀n. seq_of_streamseq … s n = streamseq_nth … s n.
320 (* Example 2 revisited: Real numbers as Cauchy sequences and their addition.
321 We closely follow example 2 replacing sequences with streamseqs.
324 definition Qstreamseq: Type[0] ≝ streamseq Q.
326 definition Qstreamseq_nth ≝ streamseq_nth Q.
328 (* The Cauchy property *)
329 definition Cauchy': Qstreamseq → Prop ≝
330 λR:Qstreamseq. ∀eps. ∃n. ∀i,j. n ≤ i → n ≤ j → Qdist (Qstreamseq_nth R i) (Qstreamseq_nth R j) ≤ eps.
332 (* A real number is an equivalence class of Cauchy sequences. Here we just
333 define the carrier, omitting the necessary equivalence relation for the
337 ; isCauchy': Cauchy' r'
340 (* The following coercion is used to write r n to extract the n-th approximation
341 from the real number r *)
342 coercion R_to_fun' : ∀r:R'. ℕ → Q ≝ (λr. Qstreamseq_nth (r' r)) on _r:R' to ?.
344 (* Pointwise addition over Qstreamseq defined by corecursion.
345 The definition is productive because, when Rplus_streamseq is applied to
346 two closed values of type Qstreamseq, it will reduce to sscons. *)
347 let corec Rplus_streamseq (x:Qstreamseq) (y:Qstreamseq) : Qstreamseq ≝
348 match x with [ sscons hdx tlx ⇒
349 match y with [ sscons hdy tly ⇒
350 sscons … (hdx + hdy) (Rplus_streamseq tlx tly) ]].
352 (* The following lemma was for free using sequences. In the case of streamseqs
353 it must be proved by induction over the index because Qstreamseq_nth is defined by
354 recursion over the index. *)
355 lemma Qstreamseq_nth_Rplus_streamseq:
357 Qstreamseq_nth (Rplus_streamseq x y) i = Qstreamseq_nth x i + Qstreamseq_nth y i.
358 #i elim i [2: #j #IH] * #xhd #xtl * #yhd #ytl // normalize @IH
361 (* The proof that the resulting sequence is Cauchy is exactly the same we
362 used for sequences, up to two applications of the previous lemma. *)
363 definition Rplus': R' → R' → R' ≝
364 λr1,r2. mk_R' (Rplus_streamseq (r' r1) (r' r2)) ….
366 cases (isCauchy' r1 (Qhalve eps)) #n1 #H1
367 cases (isCauchy' r2 (Qhalve eps)) #n2 #H2
368 %{(max n1 n2)} #i #j #K1 #K2
369 >Qstreamseq_nth_Rplus_streamseq >Qstreamseq_nth_Rplus_streamseq
370 @(transitive_Qleq … (Qdist_Qplus …))
371 <(Qplus_Qhalve_Qhalve eps) @Qleq_Qplus [@H1 @le_maxl | @H2 @le_maxr]
375 (***** Intermezzo: the dynamics of coinductive data ********)
377 (* Let corec definitions, like let rec definitions, are a form of recursive
378 definition where the definiens occurs in the definiendum. Matita compares
379 types up to reduction and reduction always allows the expansion of non recursive
380 definitions. If it also allowed the expansion of recursive definitions, reduction
381 could diverge and type checking would become undecidable. For example,
382 we defined all_zeros as "sscons … 0 all_zeros". If the system expanded all
383 occurrences of all_zeros, it would expand it forever to
384 "sscons … 0 (sscons … 0 (sscons … 0 …))".
386 In order to avoid divergence, recursive definitions are only expanded when a
387 certain condition is met. In the case of a let-rec defined function f that is
388 recursive on its n-th argument, f is only expanded when it occurs in an
389 application (f t1 ... tn ...) and tn is (the application of) a constructor.
390 Termination is guaranteed by the combination of this restriction and f being
391 guarded by destructors: the application (f t1 ... tn ...) can reduce to a term
392 that contains another application (f t1' ... tn' ...) but the size of tn'
393 (roughly the number of nested constructors) will be smaller than the size of tn
394 eventually leading to termination.
396 Dual restrictions are put on let corec definitions. If f is a let-rec defined
397 term, f is only expanded when it occurs in the term "match f t1 ... tn with ...".
398 To better see the duality, that is not syntactically perfect, note that: in
399 the recursive case f destructs terms and is expanded only when applied to a
400 constructor; in the co-recursive case f constructs terms and is expanded only
401 when it becomes argument of the match destructor. Termination is guaranteed
402 by the combination of this restriction and f being productive: the term
403 "match f t1 ... tn ... with" will reduce in a finite amount of time to
404 a match applied to a constructor, whose reduction can expose another application
405 of f, but not another "match f t1' .. tn' ... width". Therefore, since no
406 new matches around f can be created by reduction, the number of
407 destructors that surrounds the application of f decreases at every step,
408 eventually leading to termination.
410 Even if a coinductively defined f does not reduce in every context to its
411 definiendum, it is possible to prove that the definiens is equal to its
412 definiendum. The trick is to prove first an eta-expansion lemma for the
413 inductive type that states that an inhabitant of the inductive type is
414 equal to the one obtained destructing and rebuilding it via a match. The proof
415 is simply by cases over the inhabitant. Let's see an example. *)
418 ∀A:Type[0]. ∀s: streamseq A.
419 match s with [ sscons hd tl ⇒ sscons … hd tl ] = s.
423 (* In order to prove now that the definiens of all_zeros is equal to its
424 definiendum, it suffices to rewrite it using the eta_streamseq lemma in order
425 to insert around the definiens the match destructor that triggers its
427 lemma all_zeros_expansion: all_zeros = sscons … 0 all_zeros.
428 <(eta_streamseq ? all_zeros) in ⊢ (??%?); //
431 (* Expansions lemmas as the one just presented are almost always required to
432 progress in non trivial proofs, as we will see in the next example. Instead
433 the equivalent expansions lemmas for let-rec definitions are rarely required.
436 (* Example 3 revisited: traces of a program. *)
438 (* A diverging trace is a streamseq of states such that the n+1-th state is
439 obtained executing one step from the n-th state. The definition of
440 div_well_formed' is the same we already used for sequences, but on
443 definition div_well_formed' : streamseq state → Prop ≝
445 ∀n. next (streamseq_nth … s n) (streamseq_nth … s (S n)).
447 record div_trace': Type[0] ≝
448 { div_tr':> streamseq state
449 ; div_well_formed'': div_well_formed' div_tr'
452 (* The well formedness predicate over streamseq can also be redefined using as a
453 coinductive predicate. A streamseq of states is well formed if the second
454 element is the next of the first and the stream without the first element
455 is recursively well formed. *)
456 coinductive div_well_formed_co: streamseq state → Prop ≝
458 ∀hd1:state. ∀hd2:state. ∀tl:streamseq state.
459 next hd1 hd2 → div_well_formed_co (sscons … hd2 tl) →
460 div_well_formed_co (sscons … hd1 (sscons … hd2 tl)).
462 (* Note that Matita automatically proves the inversion principles for every
463 coinductive type, but no general coinduction principle. That means that
464 the elim tactic does not work when applied to a coinductive type. Inversion
465 and cases are the only ways to eliminate a coinductive hypothesis. *)
467 (* A proof of div_well_formed cannot be built stacking a finite
468 number of constructors. The type can only be inhabited by a coinductive
469 definition. As an example, we show the equivalence between the two
470 definitions of well formedness for streamseqs. *)
472 (* A div_well_formed' stream is also div_well_formed_co. We write the proof
473 term explicitly, omitting the subterms that prove "next hd1 hd2" and
474 "div_well_formed' (sscond … hd2 tl)". Therefore we will obtain two proof
475 obligations. The given proof term is productive: if we apply it to a closed
476 term of type streamseq state and a proof that it is well formed, the two
477 matches in head position will reduce and the lambda-abstraction will be
478 consumed, exposing the is_next constructor. *)
480 let corec div_well_formed_to_div_well_formed_co
481 (s: streamseq state): div_well_formed' s → div_well_formed_co s ≝
482 match s with [ sscons hd1 tl1 ⇒
483 match tl1 with [ sscons hd2 tl ⇒
484 λH: div_well_formed' (sscons … hd1 (sscons … hd2 tl)).
485 is_next … (div_well_formed_to_div_well_formed_co (sscons … hd2 tl) …) ]].
486 [ (* First proof obligation: next hd1 hd2 *) @(H 0)
487 | (* Second proof obligation: div_well_formed' (sscons … hd2 tl) *) @(λn. H (S n)) ]
490 (* A div_well_formed_co stream is also div_well_formed'. This time the proof is
491 by induction over the index and inversion over the div_well_formed_co
493 theorem div_well_formed_co_to_div_well_formed:
494 ∀s: streamseq state. div_well_formed_co s → div_well_formed' s.
495 #s #H #n lapply H -H lapply s -s elim n [2: #m #IH]
496 * #hd1 * #hd2 #tl normalize #H inversion H #hd1' #hd2' #tl' #Hnext #Hwf
500 (* Like for sequences, because of undecidability of termination there is no
501 function that given an initial state returns the diverging trace if the program
502 diverges or fails in case of error. We need a new data type to represent a
503 possibly infinite, possibly terminated stream of elements. Such data type is
504 usually called stream and can be defined elegantly as a coinductive type. *)
505 coinductive stream (A: Type[0]) : Type[0] ≝
507 | scons: A → stream A → stream A.
509 (* The definition of trace based on streams is more natural than that based
510 on sequences of optional states because there is no need of the invariant that
511 a None state is followed only by None states (to represent a terminated
512 sequence). Indeed, this is the first example where working with coinductive
513 types seems to yield advantages in terms of simplicity of the formalization.
514 However, in order to give the definition we first need to coinductively define
515 the well_formedness predicate, whose definition is more complex than the
517 coinductive well_formed': stream state → Prop ≝
518 wf_snil: ∀s. step s = None … → well_formed' (scons … s (snil …))
521 step hd1 = Some … hd2 →
522 well_formed' (scons … hd2 tl) →
523 well_formed' (scons … hd1 (scons … hd2 tl)).
525 (* Note: we could have equivalently defined well_formed' avoiding coinduction
526 by defining a recursive function to retrieve the n-th element of the stream,
527 if any. From now on we will stick to coinductive predicates only to show more
528 examples of usage of coinduction. In a formalization, however, it is always
529 better to explore several alternatives and see which ones work best for the
532 record trace': Type[0] ≝
534 ; well_formed'': well_formed' tr'
537 (* The trace is diverging if every state is not final. Again, we show here
538 a coinductive definition. *)
539 coinductive diverging': stream state → Prop ≝
540 mk_diverging': ∀hd,tl. diverging' tl → diverging' (scons … hd tl).
542 (* The two coinductive definitions of diverging traces are equivalent.
543 To state the two results we first need a function to retrieve the head
544 from traces and diverging traces. *)
545 definition head_of_streamseq: ∀A:Type[0]. streamseq A → A ≝
546 λA,s. match s with [ sscons hd _ ⇒ hd ].
548 definition head_of_stream: ∀A:Type[0]. stream A → option A ≝
549 λA,s. match s with [ snil ⇒ None … | scons hd _ ⇒ Some … hd ].
551 (* A streamseq can be extracted from a diverging stream using corecursion. *)
552 let corec mk_diverging_trace_to_div_trace'
553 (s: stream state) : diverging' s → streamseq state ≝
554 match s return λs. diverging' s → streamseq state
556 [ snil ⇒ λabs: diverging' (snil …). ?
557 | scons hd tl ⇒ λH. sscons ? hd (mk_diverging_trace_to_div_trace' tl …) ].
558 [ cases (?:False) inversion abs #hd #tl #_ #abs' destruct
559 | inversion H #hd' #tl' #K #eq destruct @K ]
562 (* An expansion lemma will be needed soon. *)
563 lemma mk_diverging_trace_to_div_trace_expansion:
565 mk_diverging_trace_to_div_trace' (scons state hd tl) H =
566 sscons … hd (mk_diverging_trace_to_div_trace' tl K).
567 #hd #tl #H cases (eta_streamseq … (mk_diverging_trace_to_div_trace' ??)) /2/
570 (* CSC: BUG CHE APPARE NEL PROSSIMO LEMMA AL MOMENTO DELLA QED. IL DEMONE
571 SERVE PER DEBUGGARE *)
574 (* To complete the proof we need a final lemma: streamseqs extracted from
575 well formed diverging streams are well formed too. *)
576 let corec div_well_formed_co_mk_diverging_trace_to_div_trace (t : stream state) :
577 ∀H:diverging' t. div_well_formed_co (mk_diverging_trace_to_div_trace' t H) ≝
578 match t return λt. diverging' t → ?
581 | scons hd tl ⇒ λH. ? ].
582 [ cases (?:False) inversion abs #hd #tl #_ #eq destruct
583 | cases (mk_diverging_trace_to_div_trace_expansion … H) #H' #eq
584 lapply (sym_eq ??? … eq) #Req cases Req -Req -eq -H
586 [ #abs cases (?:False) inversion abs #hd #tl #_ #eq destruct
588 cases (mk_diverging_trace_to_div_trace' … H) #H'
589 #eq lapply (sym_eq ??? … eq) #Req cases Req -Req
590 % [2: (*CSC: BIG BUG HERE*) cases daemon (* cases eq @div_well_formed_co_mk_diverging_trace_to_div_trace *)
594 theorem diverging_trace_to_div_trace':
595 ∀t: trace'. diverging' t → ∃d: div_trace'.
596 head_of_stream … t = Some … (head_of_streamseq … d).
598 [ %{(mk_diverging_trace_to_div_trace' … H)}
599 | cases t in H; * normalize // #abs cases (?:False) inversion abs
600 [ #s #_ #eq destruct | #hd1 #hd2 #tl #_ #_ #eq destruct ]]
602 #n lapply (well_formed t n)
603 lapply (H n) cases (tr t n) normalize [ * #abs cases (abs …) // ]
604 * #o #k #_ lapply (H (S n)) -H
605 cases (tr t (S n)) normalize
606 [ * #abs cases (abs …) // ] * #o' #k' #_ #EQ lapply (EQ … (refl …)) -EQ
607 normalize cases k normalize [ #abs destruct ] #hd #tl #EQ destruct -EQ
609 | lapply (H O) -H cases (tr t O) [ * #abs cases (abs …) // ] // ]
612 (* A stream can be extracted from a streamseq using corecursion. *)
613 let corec stream_of_streamseq (A: Type[0]) (s: streamseq A) : stream A ≝
614 match s with [ sscons hd tl ⇒ scons … hd (stream_of_streamseq … tl) ].
616 (* The proof that the resulting stream is diverging also need corecursion.*)
617 let corec diverging_stream_of_streamseq (s: streamseq state) :
618 diverging' (stream_of_streamseq … s) ≝
619 match s return λs. diverging' (stream_of_streamseq … s)
620 with [ sscons hd tl ⇒ mk_diverging' … ].
621 mk_diverging' hd (stream_of_streamseq … tl) (diverging_stream_of_streamseq tl) ].
624 theorem div_trace_to_diverging_trace':
625 ∀d: div_trace'. ∃t: trace'. diverging' t ∧
626 head_of_stream … t = Some … (head_of_streamseq … d).
627 #d %{(mk_trace' (stream_of_streamseq … d) …)}
630 [2: cases d * // ] #n % #abs destruct
631 | #n #s #EQ destruct lapply (div_well_formed d n) /2 by div_well_formed, next_step/ ]
635 (* ################## COME SPIEGARLO QUI? ####################### *)
638 (*let corec stream_coind (A: Type[0]) (P: Prop) (H: P → Sum unit (A × P))
642 | inr cpl ⇒ let 〈hd,p'〉 ≝ cpl in scons A hd (stream_coind A P H p') ]. *)
644 (*lemma eta_streamseq:
645 ∀A:Type[0]. ∀s: streamseq A.
646 s = match s with [ sscons hd tl ⇒ sscons … hd tl ].
650 lemma Rplus_streamseq_nf:
652 Rplus_streamseq (sscons … xhd xtl) (sscons … yhd ytl) =
653 sscons … (xhd + yhd) (Rplus_streamseq xtl ytl).
654 #xhd #xtl #yhd #ytl >(eta_streamseq Q (Rplus_streamseq …)) in ⊢ (??%?); //