Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: ansar

Submitted at: 2025-05-08 18:32:15

Code:

import Init.Data.Int

def solveAdd (a b:Int): Int

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 

theorem sovleAdd_correct (a b : Int) : a + (solveAdd a b) = b := by
  rw [solveAdd, Int.add_comm, Int.sub_add_cancel]

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmpfyy_yns2/proof.lean:
/root/CodeProofTheArena/temp/tmpfyy_yns2/proof.lean:7:27: error: unexpected token 'def'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmpfyy_yns2/proof.lean:9:4: error: 'solveAdd' has already been declared
/root/CodeProofTheArena/temp/tmpfyy_yns2/proof.lean:12:58: error: unexpected token 'theorem'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmpfyy_yns2/proof.lean:14:6: warning: declaration uses 'sorry'
/root/CodeProofTheArena/temp/tmpfyy_yns2/proof.lean:14:30: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?a - ?b + ?b
a b : Int
⊢ sorry + a = b