Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: kvanvels_2

Submitted at: 2024-11-19 01:13:43

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 h2
  exfalso 
  exact h1 h2
  exact mul_one_div_cancel h1

Status: Incorrect

Feedback:

/tmp/tmpeziwugog/proof.lean:15:17: warning: unused name: h2
/tmp/tmpeziwugog/proof.lean:17:11: error: unknown identifier 'h2'
/tmp/tmpeziwugog/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