BouncingScroll.mmt

namespace http://mathhub.info/FrameIT/frameworld ❚

import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚
import rules scala://rules.frameit.mmt.kwarc.info ❚
fixmeta ?FrameworldMeta ❚

theory BouncingScroll =
    meta ?MetaAnnotations?problemTheory ?BouncingScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?BouncingScroll/Solution ❙
    include ?StepUntil ❙
    theory funcs =
        get_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
            [z,zv,g] times_real_lit (minus_real_lit (plus_real_lit zv (sqrt (plus_real_lit (times_real_lit zv zv) (minus_real_lit (times_real_lit (times_real_lit 2.0 g) z)))))) (inv_real_lit g) ❙
        new_ht : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ =
            [zv,g,ht,bo] times_real_lit (times_real_lit (minus_real_lit 2.0) (times_real_lit (minus_real_lit bo) (plus_real_lit (times_real_lit g ht) zv))) (inv_real_lit g) ❙
        prep : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
            [x,y,z,xv,yv,zv,g,bo] ⟨⟨x, y, z⟩, ⟨xv, yv, zv⟩, ⟨g, get_ht z zv g, bo⟩⟩ ❙
        //vals order: (x,y,z),(xv,yv,zv),(g,ht,bo) ❙
        edit : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ❘ =
            [vals] ⟨⟨plus_real_lit (πl (πl vals)) (times_real_lit (πl (πr (πr (πr vals)))) (πl (πl (πr vals)))),
                    plus_real_lit (πl (πr (πl vals))) (times_real_lit (πl (πr (πr (πr vals)))) (πl (πr (πl (πr vals))))),
                    0.0⟩,
                    ⟨times_real_lit (πr (πr (πr (πr vals)))) (πl (πl (πr vals))),
                    times_real_lit (πr (πr (πr (πr vals)))) (πl (πr (πl (πr vals)))),
                    times_real_lit (minus_real_lit (πr (πr (πr (πr vals))))) (plus_real_lit (times_real_lit (πl (πr (πr vals))) (πl (πr (πr (πr vals))))) (πr (πr (πl (πr vals)))))⟩,
                    ⟨(πl (πr (πr vals))),
                    new_ht (πr (πr (πl (πr vals)))) (πl (πr (πr vals))) (πl (πr (πr (πr vals)))) (πr (πr (πr (πr vals)))),
                    (πr (πr (πr (πr vals))))⟩⟩ ❙
        red_ht : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ ℝ ❘ =
            [cele] πl (πr (πr (πr cele))) ❙
        get_pos_fun: ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ (ℝ ⟶ (ℝ × ℝ × ℝ)) ❘ =
            [x,y,z,xv,yv,zv,g] ([t] ⟨plus_real_lit x (times_real_lit xv t), plus_real_lit y (times_real_lit yv t), plus_real_lit (times_real_lit (times_real_lit 0.5 g) (times_real_lit t t)) (plus_real_lit z (times_real_lit zv t))⟩ ) ❙
        end_cond : ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) ⟶ bool ❘ =
            [vals] leq_real_lit (πl (πr (πr (πr vals)))) 0.1 ❙
    ❚
    // start position and velocity ❙
    theory Problem =
        include ?BouncingScroll/funcs ❙
        xposition: ℝ ❘ meta ?MetaAnnotations?label "X" ❙
        yposition: ℝ ❘ meta ?MetaAnnotations?label "Y" ❙
        zposition: ℝ ❘ meta ?MetaAnnotations?label "Z" ❙
        xvelocity: ℝ ❘ meta ?MetaAnnotations?label "XV" ❙
	    yvelocity: ℝ ❘ meta ?MetaAnnotations?label "YV" ❙
        zvelocity: ℝ ❘ meta ?MetaAnnotations?label "ZV" ❙
	    g_base: ℝ ❘ meta ?MetaAnnotations?label "G" ❙
        bounce: ℝ ❘ meta ?MetaAnnotations?label "BO" ❙
    ❚

    // the output of the scroll ❙
    theory Solution =
        include ?BouncingScroll/Problem ❙
        full_list: List[(ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)] ❘ = stepUntil ((ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ) × (ℝ × ℝ × ℝ)) (prep xposition yposition zposition xvelocity yvelocity zvelocity g_base bounce) edit 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)) (πl (πr (πl vals))) (πr (πr (πl vals)))  (πl (πl (πr vals))) (πl (πr (πl (πr vals)))) (πr (πr (πl (πr vals)))) (πl (πr (πr vals)))) ❙
        meta ?MetaAnnotations?label "BouncingScroll" ❙
        meta ?MetaAnnotations?description s"Bouncing " ❙
    ❚
❚