Submission Details

Back to Submissions List

Challenge: solve1x1

Submitted by: Kyle Miller

Submitted at: 2024-11-15 16:41:44

Code:

import Mathlib.Data.Rat.Defs

def solve1x1(a b: Rat): Option Rat

:= if a = 0 then none else b / a

First Theorem Proof:

theorem solve1x1_correct(a b:Rat): (∃ x, a*x=b) -> a * (solve1x1 a b).get! =b

:= by rintro ⟨x, rfl⟩; unfold solve1x1; split_ifs <;> simp [*]

Status: Correct

Feedback:

Second Theorem Proof:

theorem solve1x1_none(a b:Rat): (Not (∃ x, a*x=b)) -> solve1x1 a b=none

:= by rw [not_imp_comm]; simp [solve1x1]; intro h; use b/a; exact mul_div_cancel₀ b h

Status: Incorrect