midPoint

write a function that, given rational number coordinates of two points x1, y1 and x2, y2, return the rational number coordinates of a point (xmid, ymid) such that: the distance betwee (xmid,ymid) and (x1, y1) is equal to the distance between (xmid,ymid) and (x2,y2), which is equal to half of the distance between (x1, y1) and (x2, y2).

Function Signature

import Mathlib.Data.Rat.Defs

def midPoint (x1 y1 x2 y2: Rat):Rat × Rat

Theorem Signature

def distSq( x1  y1 x2 y2: Rat):Rat:=
  (x1-x2)^2 + (y1-y2)^2

theorem midPoint_correct (x1 y1 x2 y2: Rat)
: let (xmid,ymid) :=midPoint x1 y1 x2 y2
distSq xmid ymid x1 y1=distSq xmid ymid x2 y2
∧ 4*(distSq xmid ymid x1 y1)=distSq x1  y1 x2 y2

View All Submissions

Please log in or register to submit a solution for this challenge.