Submission Details

Back to Submissions List

Challenge: solve1x1

Submitted by: GasStationManager

Submitted at: 2024-11-16 08:03:12

Code:

import Mathlib.Data.Rat.Defs

def solve1x1(a b: Rat): Option Rat

:=
  if a = 0 then
    if b=0 then
      some 0
    else
      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
    intro hsol
    simp[solve1x1]
    split_ifs
    next hb=>simp[hb]
    next ha hb=> simp[ha] at hsol; rw[hsol] at hb; contradiction
    next ha=>
      simp
      simp[Rat.div_def]
      simp[Rat.mul_comm b]
      simp[← Rat.mul_assoc]
      have: a*a.inv=1 :=by{
        have hainv: a⁻¹ = a.inv :=by {
          exact rfl
        }
        rw[← hainv]
        rw[Rat.mul_inv_cancel]
        assumption
      }
      simp[this]

Status: Correct

Feedback:

Second Theorem Proof:

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

:= by
    intro h
    simp[solve1x1]
    split_ifs
    next ha hb=> simp[ha] at h;rw[hb] at h; contradiction
    next=>rfl
    next ha=>
      contrapose! h
      use b/a
      exact mul_div_cancel₀ b ha

Status: Incorrect