Submission Details

Back to Submissions List

Challenge: solve1x1

Submitted by: Violeta Hernández Palacios

Submitted at: 2024-11-19 09:14:26

Code:

import Mathlib.Data.Rat.Defs

def solve1x1(a b: Rat): Option Rat

:= if a = 0 then none else some (b/a)

First Theorem Proof:

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

:= by
  rw [solve1x1]
  split <;> rename_i h
  · obtain rfl := h
    simp
  · simp [mul_div_cancel₀ b h]

Status: Correct

Feedback:

Second Theorem Proof:

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

 := by
  simp [solve1x1]
  contrapose!
  intro h
  use b / a
  exact mul_div_cancel₀ b h

Status: Correct