Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: kvanvels_2

Submitted at: 2024-11-19 01:09:59

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 h2
    rw [h2,zero_mul] at h0
    linarith
  unfold solveMul
  split_ifs with h2
  exfalso 
  exact h1 h2
  exact mul_one_div_cancel h1

Status: Incorrect

Feedback:

/tmp/tmplu1e6w4j/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