Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: Command Master

Submitted at: 2024-11-15 11:55:55

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 omega

Status: Incorrect

Feedback:

/tmp/tmpazercpkd/proof.lean:8:6: error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  c - d - e ≥ 1
where
 c := b
 d := a
 e := solveAdd a b