Submission Details

Back to Submissions List

Challenge: findIf

Submitted by: m-ow

Submitted at: 2026-01-07 14:56:26

Code:

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

def findIf (xs : List Int) (p : Int -> Bool) : Option Int :=
  match xs with
  | [] => none
  | x :: rest => 
    if p x then 
      some x 
    else 
      findIf rest p

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

theorem findIf_some (xs : List Int) (p : Int → Bool) :
  (∃ x ∈ xs, p x) → ∃ y ∈ xs, findIf xs p = some y ∧ p y := by
  induction xs with
  | nil => 
    intro h
    simp at h 
  | cons head tail ih =>
    intro h
    by_cases h_head : p head
    · simp [findIf, h_head]
    simp [findIf, h_head]
    aesop

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmplie56i6w/proof.lean:
/root/CodeProofTheArena/temp/tmplie56i6w/proof.lean:4:47: error: unexpected token 'def'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmplie56i6w/proof.lean:5:4: error: 'findIf' has already been declared
/root/CodeProofTheArena/temp/tmplie56i6w/proof.lean:17:53: error: unexpected token 'theorem'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmplie56i6w/proof.lean:29:5: error: unknown tactic

Second Theorem Proof:

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

theorem findIf_none_short (xs : List Int) (p : Int → Bool) :
  (¬ ∃ y ∈ xs, p y) → findIf xs p = none := by
  induction xs with
  | nil => simp [findIf]
  | cons head tail ih =>
    intro h
    rw [findIf]
    aesop

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmplie56i6w/proof2.lean:
/root/CodeProofTheArena/temp/tmplie56i6w/proof2.lean:4:47: error: unexpected token 'def'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmplie56i6w/proof2.lean:5:4: error: 'findIf' has already been declared
/root/CodeProofTheArena/temp/tmplie56i6w/proof2.lean:18:43: error: unexpected token 'theorem'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmplie56i6w/proof2.lean:27:5: error: unknown tactic
/root/CodeProofTheArena/temp/tmplie56i6w/proof2.lean:23:11: warning: declaration uses 'sorry'
/root/CodeProofTheArena/temp/tmplie56i6w/proof2.lean:23:8: error: unsolved goals
case nil
p : Int → Bool
⊢ sorry = none
/root/CodeProofTheArena/temp/tmplie56i6w/proof2.lean:24:22: error: unsolved goals
case cons
p : Int → Bool
head : Int
tail : List Int
ih : (¬∃ y, y ∈ tail ∧ p y = true) → findIf tail p = none
h : ¬∃ y, y ∈ head :: tail ∧ p y = true
⊢ sorry = none