Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: kvanvels_2

Submitted at: 2024-11-19 01:16:14

Code:

import Mathlib.Data.Rat.Defs

def solveMul(a: Rat): Rat

:= if(a = 0) then (0:Rat) else (1:Rat)/a

First Theorem Proof:

theorem solveMul_correct(a:Rat): (∃ x, a*x=1)->a * (solveMul a)=1

 by
  rintro ⟨ainv,h0⟩
  have h1 : ¬(a = 0) := by
    intro htemp
    rw [htemp,zero_mul] at h0
    linarith
  unfold solveMul
  split_ifs with h_eleven
  · exfalso 
    exact h1 h_eleven
  · exact mul_one_div_cancel h1

Status: Incorrect

Feedback:

/tmp/tmpp4ybi0qs/proof.lean:7:65: error: unexpected token 'by'; expected ':=', 'where' or '|'

Second Theorem Proof:

theorem solveMul_nosol (a:Rat): (Not (∃ x, a*x=1)) ->solveMul a =0

:= by
  intro h0
  unfold solveMul
  split_ifs with h1
  rfl
  exfalso
  apply h0
  use 1/a
  exact mul_one_div_cancel h1

Status: Correct