Submission Details

Back to Submissions List

Challenge: solveAdd0

Submitted by: QuantumWar

Submitted at: 2026-01-09 13:49:25

Code:

import Init.Data.Int

def solveAdd0(a:Int): Int

:=
  -a

First Theorem Proof:

theorem solveAdd0_correct(a: Int): a +(solveAdd0 a)=0

:= by
  unfold solveAdd0
  rw [Int.add_neg_eq_sub]
  simp

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmpd3m02mhh/proof.lean:
/root/CodeProofTheArena/temp/tmpd3m02mhh/proof.lean:14:6: error: unknown constant 'Int.add_neg_eq_sub'
/root/CodeProofTheArena/temp/tmpd3m02mhh/proof.lean:14:6: error: tactic 'rewrite' failed, equality or iff proof expected
  ?m.78
a : Int
⊢ a + -a = 0