Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: James Payor

Submitted at: 2024-11-26 04:17:28

Code:

import Init.Data.Int

def solveAdd (a b:Int): Int

:= b - a

First Theorem Proof:

theorem solveAdd_correct (a b: Int): a + (solveAdd a b) =b 

:= by
  have p: solveAdd a b = -a + b := Eq.trans Int.sub_eq_add_neg (Int.add_comm b (-a))
  have q: a + (-a + b) = b := Int.add_neg_cancel_left a b
  simp [p, q]

Status: Correct

Feedback:

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