Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: Robin

Submitted at: 2025-03-28 19:11:15

Code:

import Mathlib.Data.Rat.Defs

def solveMul(a: Rat): Rat

:= a⁻¹

theorem Rat.inv_eq_zero (a : Rat) : a⁻¹ = 0 ↔ a = 0 := by
  constructor
  · intro h
    by_contra h'
    apply h'
    calc
      _ = a * 1 := (Rat.mul_one _).symm
      _ = a * (a * a⁻¹) := by rw [Rat.mul_inv_cancel a h']
      _ = a * (a * 0) := by rw [h]
      _ = 0 := by simp
  · intro h
    rw [h]
    exact Rat.inv_zero

First Theorem Proof:

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

:= by
  intro ⟨x, hx⟩
  unfold solveMul
  refine Rat.mul_inv_cancel a ?_
  intro h
  simp only [h, Rat.zero_mul] at hx
  contradiction

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmptn5undhv/target.olean
Finished imports
Finished replay
---
def
solveMul
ℚ → ℚ
:= fun (a : Rat) => sorryAx.{1} Rat Bool.false
#[propext, sorryAx]
---
theorem
solveMul_correct
∀ (a : ℚ), (∃ x, a * x = 1) → a * solveMul a = 1
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmptn5undhv/proof.olean
Finished imports
Finished replay
---
theorem
Rat.inv_eq_zero
∀ (a : ℚ), a⁻¹ = 0 ↔ a = 0
#[propext, Classical.choice, Quot.sound]
---
def
solveMul_correct.match_1
∀ (a : ℚ) (motive : (∃ x, a * x = 1) → Prop) (h : ∃ x, a * x = 1), (∀ (x : ℚ) (hx : a * x = 1), motive ⋯) → motive h
:= fun (a : Rat) (motive : (Exists.{1} Rat (fun (x : Rat) => Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a x) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNat 1)))) -> Prop) (h._@.temp.tmptn5undhv.proof._hyg.253.266 : Exists.{1} Rat (fun (x : Rat) => Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a x) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNat 1)))) (h_1 : forall (x : Rat) (hx : Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a x) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNat 1))), motive (Exists.intro.{1} Rat (fun (x : Rat) => Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a x) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNat 1))) x hx)) => Exists.casesOn.{1} Rat (fun (x : Rat) => Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a x) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNat 1))) (fun (x : Exists.{1} Rat (fun (x : Rat) => Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a x) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNat 1)))) => motive x) h._@.temp.tmptn5undhv.proof._hyg.253.266 (fun (w._@.temp.tmptn5undhv.proof._hyg.275 : Rat) (h._@.temp.tmptn5undhv.proof._hyg.276 : Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a w._@.temp.tmptn5undhv.proof._hyg.275) (OfNat.ofNat.{0} Rat 1 (Rat.instOfNat 1))) => h_1 w._@.temp.tmptn5undhv.proof._hyg.275 h._@.temp.tmptn5undhv.proof._hyg.276)
#[propext]
---
def
solveMul
ℚ → ℚ
:= fun (a : Rat) => Inv.inv.{0} Rat Rat.instInv a
#[propext]
---
theorem
solveMul_correct
∀ (a : ℚ), (∃ x, a * x = 1) → a * solveMul a = 1
#[propext, Classical.choice, Quot.sound]
Finished with no errors.

Second Theorem Proof:

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

:= by
  intro h
  unfold solveMul
  rw [Rat.inv_eq_zero]
  by_contra h'
  apply h
  exists a⁻¹
  exact Rat.mul_inv_cancel a h'

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmptn5undhv/target2.olean
Finished imports
Finished replay
---
def
solveMul
ℚ → ℚ
:= fun (a : Rat) => sorryAx.{1} Rat Bool.false
#[propext, sorryAx]
---
theorem
solveMul_nosol
∀ (a : ℚ), (¬∃ x, a * x = 1) → solveMul a = 0
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmptn5undhv/proof2.olean
Finished imports
Finished replay
---
theorem
Rat.inv_eq_zero
∀ (a : ℚ), a⁻¹ = 0 ↔ a = 0
#[propext, Classical.choice, Quot.sound]
---
def
solveMul
ℚ → ℚ
:= fun (a : Rat) => Inv.inv.{0} Rat Rat.instInv a
#[propext]
---
theorem
solveMul_nosol
∀ (a : ℚ), (¬∃ x, a * x = 1) → solveMul a = 0
#[propext, Classical.choice, Quot.sound]
Finished with no errors.