Submission Details

Back to Submissions List

Challenge: solveSub

Submitted by: QuantumWar

Submitted at: 2026-01-09 13:55:16

Code:

import Init.Data.Int

def solveSub(a b:Int): Int

:=
  a - b

First Theorem Proof:

theorem solveSub_correct(a b:Int): a - (solveSub a b)=b

:= by
  unfold solveSub
  rw [Int.sub_sub_self]

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmplkhammpv/target.olean
Finished imports
Finished replay
---
theorem
solveSub_correct
∀ (a b : Int), a - solveSub a b = b
#[sorryAx]
---
def
solveSub
Int → Int → Int
:= fun (a : Int) (b : Int) => sorryAx.{1} Int Bool.false
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmplkhammpv/proof.olean
Finished imports
Finished replay
---
theorem
solveSub_correct
∀ (a b : Int), a - solveSub a b = b
#[propext]
---
def
solveSub
Int → Int → Int
:= fun (a : Int) (b : Int) => HSub.hSub.{0, 0, 0} Int Int Int (instHSub.{0} Int Int.instSub) a b
#[]
Finished with no errors.