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
201
202
203
204
205
206
207
208
209
210
|
(*
Require Import CPoly_Newton.
Require Import CRArith.
Require Import Unicode.Utf8
Setoid Arith List Program Permutation metric2.Classified
CSetoids CPoly_ApZero CRings CPoly_Degree
CRArith Qmetric Qring CReals
stdlib_omissions.Pair stdlib_omissions.Q
list_separates SetoidPermutation.
Require ne_list.
Import ne_list.notations.
(* Require Import ProductMetric CompleteProduct.*)
(** Outline of the definition of the derivative using div diff.
Should lead to FTC.
Should also be the basis for Newton iteration.
Becomes very sketchy at the end.
*)
Notation "'one' a":=(ne_list.one a) (at level 60).
Implicit Arguments ne_zip [A B].
Section divdiff.
Definition divdiff2 (f: Q-> CR) :=fun x:Q*Q =>
let (p , q) := x in let l:= (p ::: (one q)) in (divdiff (ne_zip l (ne_list.map f l) )).
End divdiff.
(*
Section extra.
Context {X Y : MetricSpace} (f: X → Complete Y) `{!UniformlyContinuous_mu f} `{!UniformlyContinuous f}.
Definition Cbind_slowC: UCFunction (Complete X) (Complete Y):=
ucFunction (Cbind_slow (wrap_uc_fun' f)).
End extra.
Notation " x >>= f ":= (Cbind_slowC f x) (at level 50).
*)
Section derivative.
(* Notation Q:=Q_as_MetricSpace.*)
(** Definition of the derivative. The usual rules should follow from the ones for dd*)
Context (f:Q->CR) `{!UniformlyContinuous_mu f}
`{!UniformlyContinuous f}.
Context `{!UniformlyContinuous_mu (divdiff2 f)}
`{!UniformlyContinuous (divdiff2 f)}.
Definition der : UCFunction Q CR := ucFunction (compose (divdiff2 f) diagonal).
End derivative.
Section towardsLBC.
(** We work towards the Law of Bounded change *)
(* This is seq 1 (S n) *)
Fixpoint posnats (n: nat): ne_list nat:=
match n with
| O => one (S O)
| S n' => (S (S n')) ::: (posnats n')
end.
Eval compute in (posnats 2).
Notation QPoint := (Q * CR)%type.
Notation CRPoint := (CR * CR)%type.
Local Notation Σ := cm_Sum.
(* Unfortunately, this is not allowed:
Fixpoint interleave {A:Type} (l1 l2 : list A) {struct l1}: list A :=
match l1 with
| nil => l2
| a :: l1 => a :: (interleave l2 l1)
end.
*)
Fixpoint interleave {A:Type} (l1 l2 : ne_list A) {struct l1}: ne_list A :=
match l1 with
| one a => a ::: l2
| a ::: l1 => a ::: match l2 with | one b => b :::l1
| b ::: l2 => b ::: (interleave l1 l2) end
end.
(*
Fixpoint ne_removelast {A:Set} (l:ne_list A) : ne_list A :=
match l with
| one a => one a
| a ::: l => a ::: ne_removelast l
end.
*)
Eval compute in (interleave ( 1 ::: (one 2#1)) (ne_list.map Qopp (ne_list.app (one 3#1) (one 0)))).
Definition diff_list (x y: Q) (m:nat) (f:Q->CR):=
let h:=(x-y)/(S m) in
let l:= (ne_list.map (λ x: Q * Q, fst x + snd x)
(ne_zip (ne_list.map (λ n:nat, h * n) (posnats m)) (ne_list.replicate_Sn x m))) in
Σ (ne_list.map (divdiff2 f) (ne_zip (x ::: l) (ne_list.app l (one 0)))).
(* (map (λ x0 : Q and Q, let (p, q) := x0 in (f p - f q )* ' (/p -q))%CR)*)
Check (diff_list 1 1 2 inject_Q_CR).
Section telescope.
(*
This really holds for a group, but we do not want to use the group tactic plugin.
*)
(* Should be type classified *)
Context {R:CRing}.
Add Ring R: (CRing_Ring R)(preprocess [unfold cg_minus;simpl]).
Lemma telescope_sum : forall l:ne_list R, forall x y:R,
Σ (interleave (x ::: l) (ne_list.map cg_inv (ne_list.app l (one y)))) [=] x [-] y.
Proof with ring.
induction l.
unfold ne_list.last;simpl. intros...
intros; simpl.
change (x [+] ([--] t [+] Σ (interleave (t ::: l) (ne_list.map cg_inv (ne_list.app l (one y))))) [=] x[-]y).
rewrite IHl...
Qed.
End telescope.
Require Import Morphisms.
(* We would like to use a Map2 for vectors. However, this only works for lists of a fixed length.
Define a general theory of applicative functors from a (strong) monad using type classes.
https://secure.wikimedia.org/wikibooks/en/wiki/Haskell/Applicative_Functors
Map2 should be for vectors
We need the rules:
f ^@> l <@> C a = fun x => (f x a) ^@> l
f ^@> C a <@> l = (f a) ^@> l
Or even f ^@> C a = C f a
*)
Definition dd_pointfree(f:Q->Q):=(compose (uncurry Qdiv)
(compose (map_pair (compose (uncurry Qminus) (map_pair f f))
(uncurry Qminus)) (@diagonal (Q*Q)))).
(* This example seems to be too difficult for pointfree:
Require Export PointFree.
Definition test0: PointFree (@fst (unit*unit) unit) _ := _.
Check test0.
Definition test1: PointFree (λ x y: Q, (Qdiv x y)) _ := _.
Check test1.
Opaque Qdiv.
Definition test2: PointFree (uncurry (λ x y: Q, (Qdiv x y))) _ := _.
Check test2.
Definition test1: PointFree (λ x y: Q, (x-y)) _ := (uncurry Qminus (map_pair fst snd)).
*)
(* Sanity check: The derivative of 2x is 2*)
Eval compute in (dd_pointfree (fun x =>(2#1)*x) (1#1,0#1)).
Context (f:Q->CR).
Lemma dd_sum:forall x y:Q, forall m:nat,
(('(S m))* (divdiff2 f (x, y)))%CR [=] diff_list x y m f.
intros.
pose h:=(x-y)/(S m).
transitivity ( ((f x) - (f y))*('(/h))%CR)%CR.
change divdiff2 with dd_pointfree.
unfold divdiff2.
change ((' S m * ((f x - f y) * ' (/ (x - y))))%CR[=]
((f x - f y) * ' (/ h))%CR).
unfold h.
unfold Qdiv.
set ((f x) - (f y))%CR.
rewrite Qinv_mult_distr Qinv_involutive -CRmult_Qmult.
set (/(x - y)). ring.
unfold diff_list. fold h. unfold divdiff2.
set l:= (ne_list.map (λ x: Q * Q, fst x + snd x)
(ne_zip (ne_list.map (λ n:nat, h * n) (posnats m)) (ne_list.replicate_Sn x m))).
set fl:= (ne_list.map f l).
transitivity (Σ (interleave (f x ::: fl) (ne_list.map cg_inv (ne_list.app fl (one f y))))*'(/h))%CR.
rewrite (telescope_sum fl); reflexivity.
(* setoid_rewrite divdiff_e. *)(* we need map to be a morphism *)
transitivity (Σ
(ne_list.map
(λ x0 : Q and Q,
let (p, q) := x0 in
((f p [-] f q)%CR *'(/ (p -q))))%CR
(ne_zip
(x
::: l) (ne_list.app l (one 0))))).
2:admit.
(* transitivity Σ
(ne_list.map (fun x => (fst x *snd x))
etc.
(λ x0 : Q and Q, let (p, q) := x0 in ((f p[-]f q) * ' (/ (p - q)))%CR)
(ne_zip (x ::: l) (ne_list.app l (one 0))))
set (ne_list.map (λ x0 : Q and Q, fst x0 + snd x0)
(ne_zip (ne_list.map (λ n : nat, h * n) (posnats m))
(ne_list.replicate_Sn x m))).
*)
admit.
Qed.
Context (f:Q->CR) `{!UniformlyContinuous_mu f}
`{!UniformlyContinuous f}.
Context `{!UniformlyContinuous_mu (divdiff2 f)}
`{!UniformlyContinuous (divdiff2 f)}.
(* Use compare to avoid dependency on proofs of being in the interval *)
Lemma der_pos_dd_pos: (forall x:Q, (('0 <= (der f) x)%CR))
-> forall x y, ('0<= (divdiff2 f (x, y)))%CR.
intros.
rewrite CRle_not_lt. intro.
contradict H.
(* definition of der is not correct *)
unfold der . simpl. unfold diagonal. simpl. unfold compose. simpl.
setoid_rewrite divdiff_e. simpl.
SearchAbout [CRlt].
admit.
Qed.
End bla.
*)
|
