Submission Details

Back to Submissions List

Challenge: solveAdd0

Submitted by: GasStationManager

Submitted at: 2024-11-24 08:23:02

Code:

import Init.Data.Int

def solveAdd0(a:Int): Int

:= -a

First Theorem Proof:

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

:= by rw[solveAdd0]; omega

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmp4ksxodw6/target.olean
Finished imports
Finished replay
---
def
solveAdd0
ℤ → ℤ
:= fun (a : Int) => sorryAx.{1} Int Bool.false
#[sorryAx]
---
theorem
solveAdd0_correct
∀ (a : ℤ), a + solveAdd0 a = 0
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmp4ksxodw6/proof.olean
Finished imports
Finished replay
---
def
solveAdd0
ℤ → ℤ
:= fun (a : Int) => Neg.neg.{0} Int Int.instNegInt a
#[]
---
theorem
solveAdd0.eq_1
∀ (a : ℤ), solveAdd0 a = -a
#[]
---
theorem
solveAdd0_correct
∀ (a : ℤ), a + solveAdd0 a = 0
#[propext, Quot.sound]
Finished with no errors.