Submission Details

Back to Submissions List

Challenge: solveAdd0

Submitted by: GasStationManager

Submitted at: 2024-11-14 05:07:46

Code:

import Init.Data.Int

def solveAdd0(a:Int): Int

:= -a

First Theorem Proof:

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

:= simp[solveAdd0]

Status: Incorrect

Feedback:

/tmp/tmpwb26hghw/proof.lean:8:3: error: unknown identifier 'simp'
/tmp/tmpwb26hghw/proof.lean:8:3: error: failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
a : ℤ
⊢ ?m.101 sorry solveAdd0