Download Matita Tutorial - Dipartimento di Informatica

Matita Tutorial
·
179
The following coercion is used to write r n to extract the n-th approximation
from the real number r.
coercion R_to_fun’ : ∀r:R’. N→ Q :=(λr. Qstreamseq_nth (r’ r)) on _r:R’ to ?.
Pointwise addition over Qstreamseq defined by corecursion. The definition is
productive because, when Rplus_streamseq is applied to two closed values of type
Qstreamseq, it will reduce to sscons.
let corec Rplus_streamseq (x:Qstreamseq) (y:Qstreamseq) : Qstreamseq :=
match x with [ sscons hdx tlx ⇒
match y with [ sscons hdy tly ⇒
sscons . . . (hdx + hdy) (Rplus_streamseq tlx tly) ]].
The following lemma was for free using sequences. In the case of streamseqs it
must be proved by induction on the index because Qstreamseq_nth is defined by
recursion on the index.
lemma Qstreamseq_nth_Rplus_streamseq:
∀i,x,y.
Qstreamseq_nth (Rplus_streamseq x y) i
= Qstreamseq_nth x i + Qstreamseq_nth y i.
#i elim i [2: #j #IH] * #xhd #xtl * #yhd #ytl // normalize @IH
qed.
The proof that the resulting sequence is Cauchy is exactly the same we used for
sequences, up to two applications of the previous lemma.
definition Rplus_’: R_’ → R_’ → R_’ :=
λr1,r2. mk_R_’ (Rplus_streamseq (r’ r1) (r’ r2)) . . . .
#eps
cases (isCauchy’ r1 (Qhalve eps)) #n1 #H1
cases (isCauchy’ r2 (Qhalve eps)) #n2 #H2
%{(max n1 n2)} #i #j #K1 #K2
>Qstreamseq_nth_Rplus_streamseq >Qstreamseq_nth_Rplus_streamseq
@(transitive_Qleq . . . (Qdist_Qplus . . . ))
<(Qplus_Qhalve_Qhalve eps) @Qleq_Qplus [@H1 @le_maxl | @H2 @le_maxr]
[2,6: @K1 |4,8: @K2]
qed.
We lift Rplus_’ to a morphism by proving that it respects the equality for real
numbers. The script is exactly the same we used to lift Rplus_, but for two applications of Qstreamseq_nth_Rplus_streamseq.
definition Rplus’: R’ →· R’ →· R’ :=
mk_bin_morphism . . . Rplus_’ . . . .
#x1 #x2 #y1 #y2 #Hx #Hy #eps
cases (Hx (Qhalve eps)) #i -Hx #Hx
cases (Hy (Qhalve eps)) #j -Hy #Hy
%{(max i j)} #l #Hmax <(Qplus_Qhalve_Qhalve eps) @transitive_Qleq
[3: @(Qleq_Qplus . . . (Hx l . . . ) (Hy l . . . )) /2 by le_maxl,le_maxr/
|2: >Qstreamseq_nth_Rplus_streamseq >Qstreamseq_nth_Rplus_streamseq // ]
qed.
Journal of Formalized Reasoning Vol. 7, No. 2, 2014.