Submission Details

Back to Submissions List

Challenge: solve1x1

Submitted by: kvanvels

Submitted at: 2024-11-15 17:53:15

Code:

import Mathlib.Data.Rat.Defs

def solve1x1(a b: Rat): Option Rat

if (a = 0) then (if (b = 0) then (1:Rat) else 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 ⟨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: Incorrect

Feedback:

/tmp/tmprxe441k1/code.lean:4:34: error: unexpected token 'if'; expected ':=', 'where' or '|'

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]
  rfl
  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: Incorrect