Newer
Older
Lucas-He
committed
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
namespace http://mathhub.info/FrameIT/frameworld ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚
import rules scala://datatypes.LFX.mmt.kwarc.info ❚
fixmeta ?FrameworldMeta ❚
theory T3DBouncingScroll =
meta ?MetaAnnotations?problemTheory ?T3DBouncingScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?T3DBouncingScroll/Solution ❙
rule rules?FilterRule (true) ❙
include ?IfThenElseX ❙
include ?StepUntil ❙
include ?Triangles ❙
//stepUntil : {X: type} X ⟶ (X ⟶ X) ⟶ (X ⟶ bool) ⟶ List[X] ❘ # stepUntil 1 2 3 4 ❙
//filter2 : List[ℝ × wall] ⟶ ((ℝ × wall) ⟶ bool) ⟶ List[ℝ × wall] ❘ # 1 filter2 2 ❙
theory funcs =
eq_zero : ℝ ⟶ bool ❘ =
[val] (bool) ifx (leq_real_lit val 0.000001)
thenx ((bool) ifx (leq_real_lit (minus_real_lit 0.000001) val)
thenx true
elsex false)
elsex false ❙
get_abcs : List[wall] ⟶ point ⟶ point ⟶ point ⟶ List[point × wall] ❘ =
[w, p, v, g] w map ([wi : wall] ⟨⟨(plus_real_lit (times_real_lit (wi.a) (g _x)) (plus_real_lit (times_real_lit (wi.b) (g _y)) (times_real_lit (wi.c) (g _z)))),
(plus_real_lit (plus_real_lit (times_real_lit (wi.a) (v _x)) (times_real_lit (wi.b) (v _y))) (times_real_lit (wi.c) (v _z))),
(plus_real_lit (plus_real_lit (plus_real_lit (times_real_lit (wi.a) (p _x)) (times_real_lit (wi.b) (p _y))) (times_real_lit (wi.c) (p _z))) (minus_real_lit (wi.d)))⟩,
wi⟩) ❙
mget_hts : (point × wall) ⟶ (ℝ × ℝ × wall) ❘ =
[cabc] (ℝ × ℝ × wall) ifx (eq_zero ((πl cabc) _x))
thenx ((ℝ × ℝ × wall) ifx (eq_zero ((πl cabc) _y))
thenx (⟨-1.0, -1.0, (πr cabc)⟩)
elsex (⟨minus_real_lit (times_real_lit ((πl cabc) _z) (inv_real_lit ((πl cabc) _y))),
minus_real_lit (times_real_lit ((πl cabc) _z) (inv_real_lit ((πl cabc) _y))), (πr cabc)⟩))
elsex ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z))))))
thenx (⟨times_real_lit (plus_real_lit (minus_real_lit ((πl cabc) _y)) (sqrt (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z))))))) (inv_real_lit ((πl cabc) _x)),
times_real_lit (plus_real_lit (minus_real_lit ((πl cabc) _y)) (minus_real_lit (sqrt (plus_real_lit (times_real_lit ((πl cabc) _y) ((πl cabc) _y)) (minus_real_lit (times_real_lit 2.0 (times_real_lit ((πl cabc) _x) ((πl cabc) _z)))))))) (inv_real_lit ((πl cabc) _x)), (πr cabc)⟩)
elsex (⟨-1.0, -1.0, (πr cabc)⟩)) ❙
get_pt : ℝ ⟶ point ⟶ point ⟶ point ⟶ point ❘ =
[rht, rp, rv, rg] ⟨plus_real_lit (plus_real_lit (rp _x) (times_real_lit (rv _x) rht)) (times_real_lit (times_real_lit 0.5 (rg _x)) (times_real_lit rht rht)),
plus_real_lit (plus_real_lit (rp _y) (times_real_lit (rv _y) rht)) (times_real_lit (times_real_lit 0.5 (rg _y)) (times_real_lit rht rht)),
plus_real_lit (plus_real_lit (rp _z) (times_real_lit (rv _z) rht)) (times_real_lit (times_real_lit 0.5 (rg _z)) (times_real_lit rht rht))⟩ ❙
check_hit1 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ =
[rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl rw) 0.000001)
thenx (⟨-1.0, πl (πr rw), πr (πr rw)⟩)
elsex ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI np ((πr (πr rw)).point2))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI ((πr (πr rw)).point1) ((πr (πr rw)).point2)))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)))))
thenx (rw)
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))
elsex (⟨-1.0, πl (πr rw), πr (πr rw)⟩))) (get_pt (πl rw) rp rv rg)) ❙
check_hit2 : point ⟶ point ⟶ point ⟶ ((ℝ × ℝ × wall) ⟶ (ℝ × ℝ × wall)) ❘ =
[rp, rv, rg] ([rw: ℝ × ℝ × wall] ([np : point] (ℝ × ℝ × wall) ifx (leq_real_lit (πl (πr rw)) 0.000001)
thenx (⟨πl rw, -1.0, πr (πr rw)⟩)
elsex ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI np ((πr (πr rw)).point2))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point2)) (point_subtractI ((πr (πr rw)).point1) ((πr (πr rw)).point2)))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)))))
thenx ((ℝ × ℝ × wall) ifx (leq_real_lit 0.0 (scalar_productI (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI np ((πr (πr rw)).point1))) (vec_cross (point_subtractI ((πr (πr rw)).point2) ((πr (πr rw)).point1)) (point_subtractI ((πr (πr rw)).point3) ((πr (πr rw)).point1)))))
thenx (rw)
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))
elsex (⟨πl rw, -1.0, πr (πr rw)⟩))) (get_pt (πl (πr rw)) rp rv rg)) ❙
Lucas-He
committed
fold_func : (ℝ × wall) ⟶ (point × ℝ) ⟶ (point × ℝ) ❘ =
[cur][acc] (point × ℝ) ifx (leq_real_lit (πl cur) (πr acc)) thenx (⟨(πr cur).norm_vec, (πl cur)⟩) elsex acc ❙
calc_new_vals : (point × point × (point × ℝ) × ℝ) ⟶ (point × ℝ) ⟶ (point × point × ℝ) ❘ =
[v, bv] ⟨get_pt (πr (πl (πr (πr v)))) (πl v) (πl (πr v)) (πl bv), ([d : point] vec_multI (πr bv) (point_subtractI d (vec_multI (times_real_lit 2.0 (scalar_productI d (πl (πl (πr (πr v)))))) (πl (πl (πr (πr v))))))) (⟨plus_real_lit ((πl (πr v)) _x) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _x)), plus_real_lit ((πl (πr v)) _y) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _y)), plus_real_lit ((πl (πr v)) _z) (times_real_lit (πr (πl (πr (πr v)))) ((πl bv) _z))⟩), plus_real_lit (πr (πr (πr v))) (πr (πl (πr (πr v))))⟩ ❙
end_cond : (point × point × (point × ℝ) × ℝ) ⟶ bool ❘ =
[vals] (bool) ifx (leq_real_lit (πr (πl (πr (πr vals)))) 0.1)
thenx ((bool) ifx (leq_real_lit (sqrt(scalar_productI (πl (πr vals)) (πl (πr vals)))) 10.0)
thenx (true)
elsex false)
elsex ((bool) ifx (leq_real_lit 99999.0 (πr (πl (πr (πr vals)))))
thenx (true)
elsex false) ❙
map_reduce_hts : (ℝ × ℝ × wall) ⟶ (ℝ × wall) ❘ =
[wsi] (ℝ × wall) ifx (leq_real_lit (πl wsi) 0.000001)
thenx ((ℝ × wall) ifx (leq_real_lit (πl (πr wsi)) 0.000001)
thenx (⟨-1.0, πr (πr wsi)⟩)
elsex (⟨πl (πr wsi), πr (πr wsi)⟩))
elsex ((ℝ × wall) ifx (leq_real_lit (πl (πr wsi)) 0.000001)
thenx (⟨πl wsi, πr (πr wsi)⟩)
elsex ((ℝ × wall) ifx (leq_real_lit (πl wsi) (πl (πr wsi)))
thenx (⟨πl wsi, πr (πr wsi)⟩)
elsex (⟨πl (πr wsi), πr (πr wsi)⟩))) ❙
get_next_vals : List[wall] ⟶ (point × ℝ) ⟶ ((point × point × (point × ℝ) × ℝ) ⟶ (point × point × (point × ℝ) × ℝ)) ❘ =
[aw, abv] ([v : point × point × (point × ℝ) × ℝ] ([x : point × point × ℝ] ⟨πl x, πl (πr x), (((((((get_abcs aw (πl x) (πl (πr x)) (πl abv)) map mget_hts) map (check_hit1 (πl x) (πl (πr x)) (πl abv))) map (check_hit2 (πl x) (πl (πr x)) (πl abv))) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), πr (πr x)⟩) (calc_new_vals v abv)) ❙
Lucas-He
committed
prep : List[wall] ⟶ point ⟶ point ⟶ point ⟶ (point × point × (point × ℝ) × ℝ) ❘ =
[awi, p, v, g] ⟨p, v, (((((((get_abcs awi p v g) map mget_hts) map (check_hit1 p v g)) map (check_hit2 p v g)) map map_reduce_hts) filter ([wsj : ℝ × wall] leq_real_lit 0.000001 (πl wsj))) fold ⟨⟨-1.0, -1.0, -1.0⟩, 99999.9⟩ fold_func), 0.0⟩ ❙
Lucas-He
committed
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
get_pos_fun: point ⟶ point ⟶ point ⟶ (ℝ ⟶ point) ❘ =
[p, v, g] ([t] ⟨plus_real_lit (times_real_lit (times_real_lit 0.5 (g _x)) (times_real_lit t t)) (plus_real_lit (p _x) (times_real_lit (v _x) t)), plus_real_lit (times_real_lit (times_real_lit 0.5 (g _y)) (times_real_lit t t)) (plus_real_lit (p _y) (times_real_lit (v _y) t)), plus_real_lit (times_real_lit (times_real_lit 0.5 (g _z)) (times_real_lit t t)) (plus_real_lit (p _z) (times_real_lit (v _z) t))⟩) ❙
red_ht : (point × point × (point × ℝ)) ⟶ ℝ ❘ =
[cele] πr (πr (πr cele)) ❙
map_fun_list : (point × point × (point × ℝ) × ℝ) ⟶ point ⟶ ((ℝ × ℝ) × (ℝ ⟶ ℝ) × (ℝ ⟶ point)) ❘ =
[vals, g] ⟨⟨πr (πr (πr vals)), plus_real_lit (πr (πr (πr vals))) (πr (πl (πr (πr vals))))⟩, ([ts : ℝ] plus_real_lit ts (minus_real_lit (πr (πr (πr vals))))), get_pos_fun (πl vals) (πl (πr vals)) g⟩ ❙
❚
// start position and velocity ❙
theory Problem =
include ?T3DBouncingScroll/funcs ❙
position: point ❘ meta ?MetaAnnotations?label "Pos" ❙
velocity: point ❘ meta ?MetaAnnotations?label "Vel" ❙
g_base: point ❘ meta ?MetaAnnotations?label "G" ❙
bounce: ℝ ❘ meta ?MetaAnnotations?label "BO" ❙
wallsr: List[wall] ❘ meta ?MetaAnnotations?label "WallsR" ❙
❚
// the output of the scroll ❙
theory Solution =
include ?T3DBouncingScroll/Problem ❙
full_list: List[point × point × (point × ℝ) × ℝ] ❘ = stepUntil (point × point × (point × ℝ) × ℝ) (prep wallsr position velocity g_base) (get_next_vals wallsr ⟨g_base, bounce⟩) end_cond ❙
fun_list : List[(ℝ × ℝ) × (ℝ ⟶ ℝ) × (ℝ ⟶ point)] ❘ = full_list map ([vals : point × point × (point × ℝ) × ℝ] map_fun_list vals g_base) ❙
//ht_list: List[ℝ] ❘ = full_list map red_ht ❙
//fun_list : List[ℝ ⟶ point] ❘ = full_list map ([vals] get_pos_fun (πl vals) (πl (πr vals)) g_base) ❙
meta ?MetaAnnotations?label "T3DBouncingScroll" ❙
meta ?MetaAnnotations?description s"Bouncing " ❙
❚
❚