Submission Details

Back to Submissions List

Challenge: solve1x1

Submitted by: kvanvels_2

Submitted at: 2024-11-19 00:54:06

Code:

import Mathlib.Data.Rat.Defs

def solve1x1(a b: Rat): Option Rat

:= if (a = 0) then (if (b = 0) then (some (1:Rat)) 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
   rintro ⟨p,h1⟩
   unfold solve1x1
   split_ifs with h2 h3
   rw [h2,h3,zero_mul]
   exfalso
   apply h3
   rw [←h1,h2,zero_mul]
   rw [←h1]
   have h3: (a * p)/a = p := mul_div_cancel_left₀ p h2
   rw [h3]
   rfl   

Status: Correct

Feedback:

Second Theorem Proof:

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

:= by
  contrapose
  intro h0
  push_neg
  use (solve1x1 a b).get!
  unfold solve1x1 
  unfold solve1x1 at h0
  
  split_ifs with h2 h3
  rw [h2,h3]
  rw [zero_mul]
  rw [h2] at h0
  by_contra _
  apply h0
  split_ifs with h5
  rfl
  apply h5
  rfl
  have h3: (some (b / a)).get! = b/a := rfl
  rw [h3]
  exact mul_div_cancel₀ b h2

Status: Correct