Submission Details

Back to Submissions List

Challenge: findIf

Submitted by: m-ow

Submitted at: 2026-01-07 15:03:58

Code:

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

:= 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/tmpzxq2i2a0/proof.lean:
/root/CodeProofTheArena/temp/tmpzxq2i2a0/proof.lean:28:5: error: unknown tactic
/root/CodeProofTheArena/temp/tmpzxq2i2a0/proof.lean:23:22: error: unsolved goals
case neg
p : Int → Bool
head : Int
tail : List Int
ih : (∃ x, x ∈ tail ∧ p x = true) → ∃ y, y ∈ tail ∧ findIf tail p = some y ∧ p y = true
h : ∃ x, x ∈ head :: tail ∧ p x = true
h_head : ¬p head = true
⊢ ∃ a, a ∈ tail ∧ findIf tail p = some a ∧ p a = true

Second Theorem Proof:

theorem findIf_none(xs:List Int)(p:Int->Bool):
  (¬ ∃ y∈ xs, p y =true)-> 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/tmpzxq2i2a0/proof2.lean:
/root/CodeProofTheArena/temp/tmpzxq2i2a0/proof2.lean:26:5: error: unknown tactic
/root/CodeProofTheArena/temp/tmpzxq2i2a0/proof2.lean:23: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
⊢ (if p head = true then some head else findIf tail p) = none