/* REQUIRED INFORMATION:

Statistics can be obtained from Proof -> Show Proof Statistics.

Name: Milda Zizyte & Felix Hutchison
AndrewID: mzizyte; fhutchin
KeYmaera version: 3.6.12
Backends used (Mathematica, Z3, ...): Mathematica
Nodes: 26815
Branches: 2221
Interactive steps: 28 
Arithmetic Solver: 2079.829
Time: 2537.517 s
Proof completes (Y/N): N

*/

\functions {
R Width;
R Height;
R vel;
R r;
}

\programVariables {
R bx;
R by;
R vx;
R vy;

R paddleWidth;
//R Px;
R Py;
R Pvy;
//R Ox;
R Oy;
R Ovy;
R Yimp;
}

/* Prove that adding English and computing impact point works.
English is some fraction of the paddle velocity being imparted to the ball */

\problem{

/* INITIAL CONDITIONS */

/* Player paddle starts where the ball is. English ratio r satisfies -1 <= r <= 1. */
(Width > 0 & Height > 0 & bx > 0 & by > 0 & bx < Width & by < Height & vx^2 + vy^2 = vel^2 & vel > 0 & paddleWidth > 0 & Py = by & r^2 <= 1) /* & Px = 0 & Ox = Width) */
->
\[
  (
  
    /* WALL PHYSICS EVENTS */
       if (by = 0 & vy < 0) then (vy := -vy)
       else (if (by = Height & vy > 0) then (vy := -vy) fi)
       fi;
       

    /* Impact point geometry is calculated using reflections over the
    horizontal. We set the velocity so the paddle reaches the ball center
    within the time the ball reaches the horizontal, which is -vx/bx. */
    if (vx < 0 & bx > 0)
    then 
    (
    Yimp := (bx/vx)*vy + by;
       	    (if (Yimp > Height)
       	    	then (Yimp := 2*Height - Yimp)
       		else (if (Yimp < 0)
       	    	     then (Yimp := Height - Yimp)
		     fi)
	     fi)*;
    	?(0 <= Yimp & Yimp <= Height);
    	Pvy := (Yimp - Py)*vx/(-bx)
	)

	/* Don't move the paddle if the ball is moving away from us */
	else (Pvy := 0) 
	fi;

    /* CONTROL */
    /* Opponent paddle is always where the ball is and velocity is arbitrary */
    Oy := by;
    Ovy := *;
  
    /* PADDLE PHYSICS EVENTS */    
    /* Note we apply English now when we hit the paddle */
    if (bx = 0 & by > Py - paddleWidth & 
            by < Py + paddleWidth & vx < 0) then (vx := -vx; vy := r * Pvy)
       else (if (bx = Width & by > Oy - paddleWidth & 
            by < Oy + paddleWidth & vx > 0) then (vx := -vx; vy := r * Ovy) 
           fi)
        fi;

    /* CONTINUOUS DYNAMICS */
    /* Evolution domains include the screen and areas to the right and left */
    ({bx' = vx, by' = vy, Py' = Pvy & bx >= 0 & bx <= Width & by >= 0 & by <= Height} ++
     {bx' = vx, by' = vy, Py' = Pvy & bx <= 0 & by >= 0 & by <= Height} ++
    {bx' = vx, by' = vy, Py' = Pvy & bx >= Width & by >= 0 & by <= Height})@invariant(Py = by) /* Diff Invariant*/
    )*@invariant(bx >= 0 & bx <= Width & Py = by)  /* Loop Invariant */
\]
/* Prove we always reach the impact point */
(bx = 0 -> by = Yimp) /* Safety Condition */
}
