Submission Details

Back to Submissions List

Challenge: midPoint

Submitted by: GasStationManager

Submitted at: 2024-11-14 07:39:22

Code:

import Mathlib.Data.Rat.Defs

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

:=((x1+x2)/2, (y1+y2)/2)

First Theorem Proof:

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

:=by
  simp[midPoint,distSq]
  constructor <;> ring_nf

Status: Correct

Feedback: