Newer
Older
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
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 WBouncingScroll =
meta ?MetaAnnotations?problemTheory ?WBouncingScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?WBouncingScroll/Solution ❙
rule rules?FilterRule (true) ❙
include ?IfThenElseX ❙
include ?StepUntilX ❙
theory funcs =
calc_new_vals : (ℝ × ℝ) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ =
[bv, v] ⟨⟨plus_real_lit (πl (πl v)) (times_real_lit (πl (πl (πr v))) (πl (πr (πr v)))), plus_real_lit (plus_real_lit (πr (πl v)) (times_real_lit (πr (πl (πr v))) (πl (πr (πr v))))) (times_real_lit (times_real_lit 0.5 (πl bv)) (times_real_lit (πl (πr (πr v))) (πl (πr (πr v)))))⟩, ⟨ times_real_lit (πr bv) (plus_real_lit (πl (πl (πr v))) (times_real_lit (times_real_lit (times_real_lit 2.0 (πr (πr (πr v)))) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))), times_real_lit (πr bv) (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (times_real_lit 2.0 (plus_real_lit (plus_real_lit (πr (πl (πr v))) (times_real_lit (πl bv) (πl (πr (πr v))))) (minus_real_lit (times_real_lit (πr (πr (πr v))) (πl (πl (πr v))))))) (inv_real_lit (plus_real_lit 1.0 (times_real_lit (πr (πr (πr v))) (πr (πr (πr v)))))))))⟩⟩ ❙
fold_func : (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ⟶ (ℝ × ℝ) ⟶ (ℝ × ℝ) ❘ =
[cur][acc] (ℝ × ℝ) ifx (leq_real_lit (πl acc) (πr (πl (πl cur)))) thenx acc elsex ⟨πr (πl (πl cur)), πr cur⟩ ❙
check_hit : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit 0.000001 (πr (πl p)) ❙
check_hit2 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit (πl (πr p)) (πl (πl p)) ❙
check_hit3 : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[p] leq_real_lit (πl (πl p)) (πr (πr p)) ❙
get_hit_time_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi))))))))) ❙
get_hit_time_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
[wi, x, y, xv, yv, g] times_real_lit (inv_real_lit g) (plus_real_lit (plus_real_lit (times_real_lit (πl (πl wi)) xv) (minus_real_lit yv)) (minus_real_lit (sqrt ( plus_real_lit (times_real_lit (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv))) (plus_real_lit yv (minus_real_lit (times_real_lit (πl (πl wi)) xv)))) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) (plus_real_lit (plus_real_lit y (minus_real_lit (times_real_lit (πl (πl wi)) x))) (minus_real_lit (πr (πl wi)))))))))) ❙
get_x_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = [x, xv, ht] plus_real_lit x (times_real_lit xv ht) ❙
combine_ht_info_pos : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ =
[wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_pos wi x y xv yv g), get_hit_time_pos wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
combine_ht_info_neg : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (((ℝ × ℝ) × (ℝ × ℝ)) × ℝ) ❘ =
[wi, x, y, xv, yv, g] ⟨⟨⟨get_x_ht x xv (get_hit_time_neg wi x y xv yv g), get_hit_time_neg wi x y xv yv g⟩, ⟨(πl (πr wi)), (πr (πr wi))⟩⟩, (πl (πl wi))⟩ ❙
get_m : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ = [w] times_real_lit (plus_real_lit (πr (πr w)) (minus_real_lit (πr (πl w)))) (inv_real_lit (plus_real_lit (πl (πr w)) (minus_real_lit (πl (πl w))))) ❙
get_c : (ℝ × ℝ) ⟶ ℝ ⟶ ℝ ❘ = [w][m] plus_real_lit (πr w) (minus_real_lit (times_real_lit (πl w) m)) ❙
get_mc : ((ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ)) ❘ = [w] ⟨⟨get_m w, get_c (πl w) (get_m w)⟩, ⟨πl (πl w), πl (πr w)⟩⟩ ❙
reduce_list_ht_pos : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
[wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_pos wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
reduce_list_ht_neg : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ List[((ℝ × ℝ) × (ℝ × ℝ)) × ℝ] ❘ =
[wsi, x, y, xv, yv, g] (((wsi map ([wi] combine_ht_info_neg wi x y xv yv g)) filter ([wib] check_hit (πl wib))) filter ([wib] check_hit2 (πl wib))) filter ([wib] check_hit3 (πl wib)) ❙
prep : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ =
[wsi, x, y, xv, yv, g] ⟨⟨x, y⟩, ⟨xv, yv⟩, (reduce_list_ht_pos wsi x y xv yv g) fold ((reduce_list_ht_neg wsi x y xv yv g) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩ ❙
get_next_vals : List[(ℝ × ℝ) × (ℝ × ℝ)] ⟶ (ℝ × ℝ) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ =
[wsi, bv, v] ([x : ((ℝ × ℝ) × (ℝ × ℝ))] ⟨⟨πl (πl x), πr (πl x)⟩, ⟨πl (πr x), πr (πr x)⟩, (reduce_list_ht_pos wsi (πl (πl x)) (πr (πl x)) (πl (πr x)) (πr (πr x)) (πl bv)) fold ((reduce_list_ht_neg wsi (πl (πl x)) (πr (πl x)) (πl (πr x)) (πr (πr x)) (πl bv)) fold ⟨99999.9, -1.0⟩ fold_func) fold_func ⟩) (calc_new_vals bv v) ❙
end_cond : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ bool ❘ =
[vals] leq_real_lit (πl (πr (πr vals))) 0.1 ❙
red_ht : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ⟶ ℝ ❘ =
[cele] πl (πr (πr cele)) ❙
get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ)) ❘ =
[x,y,xv,yv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit y (times_real_lit yv t))⟩ ) ❙
❚
// start position and velocity ❙
theory Problem =
include ?WBouncingScroll/funcs ❙
xposition: ℝ ❘ meta ?MetaAnnotations?label "X" ❙
yposition: ℝ ❘ meta ?MetaAnnotations?label "Y" ❙
xvelocity: ℝ ❘ meta ?MetaAnnotations?label "XV" ❙
yvelocity: ℝ ❘ meta ?MetaAnnotations?label "YV" ❙
g_base: ℝ ❘ meta ?MetaAnnotations?label "G" ❙
bounce: ℝ ❘ meta ?MetaAnnotations?label "BO" ❙
walls: List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ meta ?MetaAnnotations?label "Walls" ❙
❚
// the output of the scroll ❙
theory Solution =
include ?WBouncingScroll/Problem ❙
//mcws : List[(ℝ × ℝ) × (ℝ × ℝ)] ❘ = get_mc_list walls ❙
//basev : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = prep (walls map get_mc) xposition yposition xvelocity yvelocity g_base ❙
//nextv : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = get_next_vals (walls map get_mc ) ⟨g_base, bounce⟩ basev ❙
//nextv2 : ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) ❘ = get_next_vals (walls map get_mc ) ⟨g_base, bounce⟩ nextv ❙
full_list: List[(ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)] ❘ = stepUntilX ((ℝ × ℝ) × (ℝ × ℝ) × (ℝ × ℝ)) List[(ℝ × ℝ) × (ℝ × ℝ)] (ℝ × ℝ) (walls map get_mc) ⟨g_base, bounce⟩ (prep (walls map get_mc) xposition yposition xvelocity yvelocity g_base) get_next_vals end_cond ❙
ht_list: List[ℝ] ❘ = full_list map ([xele] red_ht xele) ❙
fun_list : List[ℝ ⟶ (ℝ × ℝ)] ❘ = full_list map ([vals] get_pos_fun (πl (πl vals)) (πr (πl vals)) (πl (πl (πr vals))) (πr (πl (πr vals))) g_base) ❙
meta ?MetaAnnotations?label "WBouncingScroll" ❙
meta ?MetaAnnotations?description s"Bouncing " ❙
❚
❚