Submission Details

Back to Submissions List

Challenge: findIf

Submitted by: m-ow

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

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/tmpc8l2z60a/proof.lean:
/root/CodeProofTheArena/temp/tmpc8l2z60a/proof.lean:4:47: error: unexpected token 'def'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmpc8l2z60a/proof.lean:5:4: error: 'findIf' has already been declared
/root/CodeProofTheArena/temp/tmpc8l2z60a/proof.lean:17:53: error: unexpected token 'theorem'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmpc8l2z60a/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 (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/tmpc8l2z60a/proof2.lean:
/root/CodeProofTheArena/temp/tmpc8l2z60a/proof2.lean:4:47: error: unexpected token 'def'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmpc8l2z60a/proof2.lean:5:4: error: 'findIf' has already been declared
/root/CodeProofTheArena/temp/tmpc8l2z60a/proof2.lean:18:43: error: unexpected token 'theorem'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmpc8l2z60a/proof2.lean:27:5: error: unknown tactic