Submission Details

Back to Submissions List

Challenge: rev

Submitted by: GasStationManager

Submitted at: 2024-11-24 11:27:58

Code:

def rev(xs: List Int): List Int

:=sorry

First Theorem Proof:

theorem reverse_correct(xs:List Int):
  xs.length=(rev xs).length ∧
  ∀ i<xs.length, xs[i]! =(rev xs)[xs.length-1-i]!

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpgo2gnvkj/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpgo2gnvkj/target.olean
Finished imports
Finished replay
---
theorem
reverse_correct
∀ (xs : List ℤ), xs.length = (rev xs).length ∧ ∀ i < xs.length, xs[i]! = (rev xs)[xs.length - 1 - i]!
#[sorryAx]
---
def
rev
List ℤ → List ℤ
:= fun (xs : List.{0} Int) => sorryAx.{1} (List.{0} Int) Bool.false
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpgo2gnvkj/proof.olean
Finished imports
Finished replay
---
theorem
reverse_correct
∀ (xs : List ℤ), xs.length = (rev xs).length ∧ ∀ i < xs.length, xs[i]! = (rev xs)[xs.length - 1 - i]!
#[sorryAx]
---
def
rev
List ℤ → List ℤ
:= fun (xs : List.{0} Int) => sorryAx.{1} (List.{0} Int) Bool.false
#[sorryAx]