Submission Details

Back to Submissions List

Challenge: findIf

Submitted by: GasStationManager

Submitted at: 2024-11-24 11:17:25

Code:

def findIf(xs:List Int)(p:Int->Bool):Option Int

:=sorry

First Theorem Proof:

theorem findIf_some(xs:List Int)(p:Int->Bool):
  (∃ x∈ xs, p x) -> ∃ y∈ xs, findIf xs p=some y ∧ p y

:=sorry

Status: Incorrect

Feedback:

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

Second Theorem Proof:

theorem findIf_none(xs:List Int)(p:Int->Bool):
  (¬ ∃ y∈ xs, p y =true)-> findIf xs p=none 

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmp4sckznj7/proof2.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmp4sckznj7/target2.olean
Finished imports
Finished replay
---
def
findIf
List ℤ → (ℤ → Bool) → Option ℤ
:= fun (xs : List.{0} Int) (p : Int -> Bool) => sorryAx.{1} (Option.{0} Int) Bool.false
#[sorryAx]
---
theorem
findIf_none
∀ (xs : List ℤ) (p : ℤ → Bool), (¬∃ y ∈ xs, p y = true) → findIf xs p = none
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmp4sckznj7/proof2.olean
Finished imports
Finished replay
---
def
findIf
List ℤ → (ℤ → Bool) → Option ℤ
:= fun (xs : List.{0} Int) (p : Int -> Bool) => sorryAx.{1} (Option.{0} Int) Bool.false
#[sorryAx]
---
theorem
findIf_none
∀ (xs : List ℤ) (p : ℤ → Bool), (¬∃ y ∈ xs, p y = true) → findIf xs p = none
#[sorryAx]