Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: kvanvels_2

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

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/tmpjmhgzu8y/proof.lean:15:17: warning: unused name: h_eleven
/tmp/tmpjmhgzu8y/proof.lean:17:13: error: unknown identifier 'h_eleven'
/tmp/tmpjmhgzu8y/proof.lean:18:2: error: no goals to be solved

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