Submission Details

Back to Submissions List

Challenge: findMin

Submitted by: GasStationManager

Submitted at: 2024-11-24 12:55:55

Code:

import Init.Data.List

def findMin (xs : List Int) : Option Int 

:=sorry

First Theorem Proof:

theorem findMin_correct(x: Int) (xs : List Int):
  ∃ min∈ (x::xs),
    And (findMin (x::xs) = some min) (∀ y ∈ (x::xs) , y >= min) 

:=sorry

Status: Incorrect

Feedback:

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

Second Theorem Proof:

theorem findMin_base : findMin [] = none

:=sorry

Status: Incorrect

Feedback:

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