Submission Details

Back to Submissions List

Challenge: findMax

Submitted by: GasStationManager

Submitted at: 2024-11-24 12:54:28

Code:

import Init.Data.List

def findMax (xs : List Int) : Option Int 

:=sorry

First Theorem Proof:

theorem findMax_correct(x: Int) (xs : List Int):
  ∃ max∈ (x::xs),
    And (findMax (x::xs) = some max) (∀ y ∈ (x::xs) , y ≤ max) 

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpzi6rknei/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpzi6rknei/target.olean
Finished imports
Finished replay
---
def
findMax
List Int → Option Int
:= fun (xs : List.{0} Int) => sorryAx.{1} (Option.{0} Int) Bool.false
#[sorryAx]
---
theorem
findMax_correct
∀ (x : Int) (xs : List Int), ∃ max, max ∈ x :: xs ∧ findMax (x :: xs) = some max ∧ ∀ (y : Int), y ∈ x :: xs → y ≤ max
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpzi6rknei/proof.olean
Finished imports
Finished replay
---
def
findMax
List Int → Option Int
:= fun (xs : List.{0} Int) => sorryAx.{1} (Option.{0} Int) Bool.false
#[sorryAx]
---
theorem
findMax_correct
∀ (x : Int) (xs : List Int), ∃ max, max ∈ x :: xs ∧ findMax (x :: xs) = some max ∧ ∀ (y : Int), y ∈ x :: xs → y ≤ max
#[sorryAx]

Second Theorem Proof:

theorem findMax_base : findMax [] = none

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpzi6rknei/proof2.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpzi6rknei/target2.olean
Finished imports
Finished replay
---
def
findMax
List Int → Option Int
:= fun (xs : List.{0} Int) => sorryAx.{1} (Option.{0} Int) Bool.false
#[sorryAx]
---
theorem
findMax_base
findMax [] = none
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpzi6rknei/proof2.olean
Finished imports
Finished replay
---
def
findMax
List Int → Option Int
:= fun (xs : List.{0} Int) => sorryAx.{1} (Option.{0} Int) Bool.false
#[sorryAx]
---
theorem
findMax_base
findMax [] = none
#[sorryAx]