forked from ndslusarz/formal_LDL
-
Notifications
You must be signed in to change notification settings - Fork 0
/
example.v
159 lines (138 loc) · 4.96 KB
/
example.v
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
From HB Require Import structures.
Require Import Coq.Program.Equality.
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import lra.
From mathcomp Require Import all_classical.
From mathcomp Require Import reals ereal signed.
From mathcomp Require Import topology derive normedtype sequences
exp measure lebesgue_measure lebesgue_integral hoelder.
Require Import mathcomp_extra analysis_extra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Num.Def Num.Theory GRing.Theory.
Import Order.TTheory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Require Import ldl.
Section example.
Local Open Scope ldl_scope.
Context {R : realType}.
Let ldl_norm_infty (n : nat) : @expr R (Fun_T n.+1 1) := ldl_fun (fun (t : (n.+1).-tuple R) =>
[tuple \big[maxr/[tnth t 0] ]_(i <- t) i ])%R.
Let ldl_vec_sub (n : nat) : @expr R (Vector_T n) -> @expr R (Vector_T n) -> @expr R (Vector_T n).
Proof.
elim.
- move=> r. apply.
- move=> p b. apply.
- move=> m i. apply.
- move=> m t1.
elim.
+ move=> r. exact: (ldl_real 0).
+ move=> p b. exact: (ldl_bool _ true).
+ move=> l i. exact: (ldl_idx i).
+ move=> l t2. exact: (ldl_vec [tuple nth 0 t1 i - nth 0 t2 i | i < l])%R.
+ move=> p s. exact: (ldl_bool _ true).
+ move=> p s. exact: (ldl_bool _ true).
+ move=> e1 e2. exact: e1.
+ move=> p c e1 e2 e3 e4. exact: (ldl_bool _ true).
+ move=> l k f. exact: ldl_fun f.
+ move=> l k e1 e2 v1 v2. exact: (ldl_vec [tuple 0 | i < k])%R.
+ move=> l v1 v2 i1 i2. exact: (ldl_real 0).
- move=> p s e. exact: e.
- move=> p s e. exact: e.
- move=> p s e. exact: e.
- move=> p c e f1 e1 f2 e2. exact: e2.
- move=> m l f e. exact: e.
- move=> m l e1 f1 e2 f2. exact.
- move=> m e1 f1 e2 f2. exact.
Defined.
Context (n m : nat) (eps delta : @expr R Real_T) (f : @expr R (Fun_T (n.+1) (m.+1)))
(v : @expr R (Vector_T (n.+1))) (x : @expr R (Vector_T (n.+1))).
Definition eps_delta_robust :=
(((ldl_lookup (ldl_app (ldl_norm_infty n) (ldl_vec_sub x v)) (ldl_idx ord0)) `<= eps)
`=> ((ldl_lookup (ldl_app (ldl_norm_infty m) (ldl_vec_sub (ldl_app f x) (ldl_app f v))) (ldl_idx ord0))
`<= delta)).
End example.
Section example2.
Local Open Scope ldl_scope.
Context {R : realType}.
Let ldl_sum_real : @expr R Real_T -> @expr R Real_T -> @expr R Real_T.
Proof.
elim.
- move=> r. apply.
- move=> p b. apply.
- move=> m i. apply.
- move=> m t1.
elim.
+ move=> r. exact: (ldl_real 0).
+ move=> p b. exact: (ldl_bool _ true).
+ move=> l i. exact: (ldl_idx i).
+ move=> l t2. exact: (ldl_vec [tuple nth 0 t1 i - nth 0 t2 i | i < l])%R.
+ move=> p s. exact: (ldl_bool _ true).
+ move=> p s. exact: (ldl_bool _ true).
+ move=> e1 e2. exact: e1.
+ move=> p c e1 e2 e3 e4. exact: (ldl_bool _ true).
+ move=> l k f. exact: ldl_fun f.
+ move=> l k e1 e2 v1 v2. exact: (ldl_vec [tuple 0 | i < k])%R.
+ move=> l v1 v2 i1 i2. exact: (ldl_real 0).
- move=> p s e. exact: e.
- move=> p s e. exact: e.
- move=> p s e. exact: e.
- move=> p c e f1 e1 f2 e2. exact: e2.
- move=> m l f e. exact: e.
- move=> m l e1 f1 e2 f2. exact.
- move=> m e1 f1 e2 f2. exact.
Defined.
Let ldl_real_sub : @expr R Real_T -> @expr R Real_T -> @expr R Real_T.
Proof.
elim.
- move=> r. apply.
- move=> p b. apply.
- move=> m i. apply.
- move=> m t1.
elim.
+ move=> r. exact: (ldl_real 0).
+ move=> p b. exact: (ldl_bool _ true).
+ move=> l i. exact: (ldl_idx i).
+ move=> l t2. exact: (ldl_vec [tuple nth 0 t1 i - nth 0 t2 i | i < l])%R.
+ move=> p s. exact: (ldl_bool _ true).
+ move=> p s. exact: (ldl_bool _ true).
+ move=> e1 e2. exact: e1.
+ move=> p c e1 e2 e3 e4. exact: (ldl_bool _ true).
+ move=> l k f. exact: ldl_fun f.
+ move=> l k e1 e2 v1 v2. exact: (ldl_vec [tuple 0 | i < k])%R.
+ move=> l v1 v2 i1 i2. exact: (ldl_real 0).
- move=> p s e. exact: e.
- move=> p s e. exact: e.
- move=> p s e. exact: e.
- move=> p c e f1 e1 f2 e2. exact: e2.
- move=> m l f e. exact: e.
- move=> m l e1 f1 e2 f2. exact.
- move=> m e1 f1 e2 f2. exact.
Defined.
(*Notes:
- does not say groups need to cover ALL indices*)
Fixpoint ldl_sum_vec (x : seq (@expr R Real_T)) :=
match x with
| nil => ldl_real 0
| a::l => ldl_sum_real a (ldl_sum_vec l)
end.
Definition prob_group (n m : nat)
(f : @expr R (Fun_T (n.+1) (m.+1)))
(x : @expr R (Vector_T (n.+1)))
(gs : seq (@expr R (Index_T (m.+1)))) :=
ldl_sum_vec (map (ldl_lookup (ldl_app f x)) gs).
Context (n m : nat) (eps : @expr R Real_T) (f : @expr R (Fun_T (n.+1) (m.+1)))
(x : @expr R (Vector_T (n.+1))) (Gs : seq (seq (@expr R (Index_T (m.+1)))))
(r : flag).
Let fancy_or (r : @flag) (eps p: @expr R Real_T) :=
(ldl_cmp r cmp_le p eps) `\/ (ldl_cmp r cmp_le (ldl_real_sub (ldl_real 1%R) p) eps).
(*could not get the notation to work
- could not resolve implicit argument of type flag
unsure how to solve that
*)
(* (p `<= eps) `\/ ((ldl_real_sub (ldl_real 1%R) p) `<= eps).*)
Definition group_similiarity :=
ldl_and (map (fancy_or r eps) (map (prob_group f x) Gs)).
End example2.