Submission Details

Back to Submissions List

Challenge: solve1x1

Submitted by: Robin

Submitted at: 2025-03-28 18:49:41

Code:

import Mathlib.Data.Rat.Defs

def solve1x1(a b: Rat): Option Rat

:= if a = 0 ∧ b ≠ 0 then none else some (b / a)

theorem Rat.mul_div_cancel (a b : Rat) (h : a ≠ 0) : a * (b / a) = b := by
  change a * (b * a⁻¹) = b
  rw [Rat.mul_comm b, ← Rat.mul_assoc, Rat.mul_inv_cancel _ h, Rat.one_mul]

First Theorem Proof:

theorem solve1x1_correct(a b:Rat): (∃ x, a*x=b) -> a * (solve1x1 a b).get! =b

:= by
  intro ⟨x, hx⟩
  unfold solve1x1
  by_cases h : a = 0
  · simp only [h, Rat.zero_mul] at hx
    cases hx
    simp [Rat.div_def]
  · simp only [h, ne_eq, false_and, ↓reduceIte, Option.get!_some]
    exact Rat.mul_div_cancel _ _ h

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmplv__a9_x/target.olean
Finished imports
Finished replay
---
def
solve1x1
ℚ → ℚ → Option ℚ
:= fun (a : Rat) (b : Rat) => sorryAx.{1} (Option.{0} Rat) Bool.false
#[propext, sorryAx]
---
theorem
solve1x1_correct
∀ (a b : ℚ), (∃ x, a * x = b) → a * (solve1x1 a b).get! = b
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmplv__a9_x/proof.olean
Finished imports
Finished replay
---
def
solve1x1
ℚ → ℚ → Option ℚ
:= fun (a : Rat) (b : Rat) => ite.{1} (Option.{0} Rat) (And (Eq.{1} Rat a (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (Ne.{1} Rat b (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0)))) (instDecidableAnd (Eq.{1} Rat a (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (Ne.{1} Rat b (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (instDecidableEqRat a (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (instDecidableNot (Eq.{1} Rat b (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (instDecidableEqRat b (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))))) (Option.none.{0} Rat) (Option.some.{0} Rat (HDiv.hDiv.{0, 0, 0} Rat Rat Rat (instHDiv.{0} Rat Rat.instDiv) b a))
#[propext]
---
theorem
solve1x1_correct
∀ (a b : ℚ), (∃ x, a * x = b) → a * (solve1x1 a b).get! = b
#[propext, Classical.choice, Quot.sound]
---
def
solve1x1_correct.match_1
∀ (a b : ℚ) (motive : (∃ x, a * x = b) → Prop) (h : ∃ x, a * x = b), (∀ (x : ℚ) (hx : a * x = b), motive ⋯) → motive h
:= fun (a : Rat) (b : 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) b)) -> Prop) (h._@.temp.tmplv__a9_x.proof._hyg.159.172 : Exists.{1} Rat (fun (x : Rat) => Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a x) b)) (h_1 : forall (x : Rat) (hx : Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a x) b), 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) b) 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) b) (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) b)) => motive x) h._@.temp.tmplv__a9_x.proof._hyg.159.172 (fun (w._@.temp.tmplv__a9_x.proof._hyg.181 : Rat) (h._@.temp.tmplv__a9_x.proof._hyg.182 : Eq.{1} Rat (HMul.hMul.{0, 0, 0} Rat Rat Rat (instHMul.{0} Rat Rat.instMul) a w._@.temp.tmplv__a9_x.proof._hyg.181) b) => h_1 w._@.temp.tmplv__a9_x.proof._hyg.181 h._@.temp.tmplv__a9_x.proof._hyg.182)
#[propext]
---
theorem
Rat.mul_div_cancel
∀ (a b : ℚ), a ≠ 0 → a * (b / a) = b
#[propext, Classical.choice, Quot.sound]
Finished with no errors.

Second Theorem Proof:

theorem solve1x1_none(a b:Rat): (Not (∃ x, a*x=b)) -> solve1x1 a b=none

:= by
  intro h
  unfold solve1x1
  simp only [ne_eq, ite_eq_left_iff, not_and, Decidable.not_not, reduceCtorEq, imp_false,
    Classical.not_imp]
  constructor
  · by_contra h'
    apply h
    exists b / a
    exact Rat.mul_div_cancel _ _ h'
  · rintro rfl
    apply h
    exists 0
    exact Rat.mul_zero a

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmplv__a9_x/target2.olean
Finished imports
Finished replay
---
def
solve1x1
ℚ → ℚ → Option ℚ
:= fun (a : Rat) (b : Rat) => sorryAx.{1} (Option.{0} Rat) Bool.false
#[propext, sorryAx]
---
theorem
solve1x1_none
∀ (a b : ℚ), (¬∃ x, a * x = b) → solve1x1 a b = none
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmplv__a9_x/proof2.olean
Finished imports
Finished replay
---
theorem
temp.tmplv__a9_x.proof2._auxLemma.1
∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x y : α}, ((if p then x else y) = x) = (¬p → y = x)
#[propext]
---
def
solve1x1
ℚ → ℚ → Option ℚ
:= fun (a : Rat) (b : Rat) => ite.{1} (Option.{0} Rat) (And (Eq.{1} Rat a (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (Ne.{1} Rat b (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0)))) (instDecidableAnd (Eq.{1} Rat a (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (Ne.{1} Rat b (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (instDecidableEqRat a (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (instDecidableNot (Eq.{1} Rat b (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))) (instDecidableEqRat b (OfNat.ofNat.{0} Rat 0 (Rat.instOfNat 0))))) (Option.none.{0} Rat) (Option.some.{0} Rat (HDiv.hDiv.{0, 0, 0} Rat Rat Rat (instHDiv.{0} Rat Rat.instDiv) b a))
#[propext]
---
theorem
solve1x1_none
∀ (a b : ℚ), (¬∃ x, a * x = b) → solve1x1 a b = none
#[propext, Classical.choice, Quot.sound]
---
theorem
temp.tmplv__a9_x.proof2._auxLemma.3
∀ {p : Prop} [inst : Decidable p], (¬¬p) = p
#[propext]
---
theorem
temp.tmplv__a9_x.proof2._auxLemma.2
∀ {a b : Prop}, (¬(a ∧ b)) = (a → ¬b)
#[propext]
---
theorem
temp.tmplv__a9_x.proof2._auxLemma.4
∀ {a : Prop}, (a → False) = ¬a
#[propext]
---
theorem
Rat.mul_div_cancel
∀ (a b : ℚ), a ≠ 0 → a * (b / a) = b
#[propext, Classical.choice, Quot.sound]
---
theorem
temp.tmplv__a9_x.proof2._auxLemma.5
∀ {a b : Prop}, (¬(a → b)) = (a ∧ ¬b)
#[propext, Classical.choice, Quot.sound]
Finished with no errors.