Submission Details

Back to Submissions List

Challenge: findIf

Submitted by: m-ow

Submitted at: 2026-01-07 15:05:02

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

import Mathlib.Tactic

:= 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: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmpzkqz0rde/target.olean
Finished imports
Finished replay
---
theorem
findIf_some
∀ (xs : List Int) (p : Int → Bool), (∃ x, x ∈ xs ∧ p x = true) → ∃ y, y ∈ xs ∧ findIf xs p = some y ∧ p y = true
#[sorryAx]
---
def
findIf
List Int → (Int → Bool) → Option Int
:= fun (xs : List.{0} Int) (p : Int -> Bool) => sorryAx.{1} (Option.{0} Int) Bool.false
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpzkqz0rde/proof.olean
Finished imports
Finished replay
---
def
findIf._sunfold
List ℤ → (ℤ → Bool) → Option ℤ
:= fun (xs : List.{0} Int) (p : Int -> Bool) => [mdata sunfoldMatch:1 findIf.match_1.{1} (fun (xs._@.temp.tmpzkqz0rde.proof._hyg.15 : List.{0} Int) => Option.{0} Int) xs (fun (_ : Unit) => [mdata sunfoldMatchAlt:1 Option.none.{0} Int]) (fun (x : Int) (rest : List.{0} Int) => [mdata sunfoldMatchAlt:1 ite.{1} (Option.{0} Int) (Eq.{1} Bool (p x) Bool.true) (instDecidableEqBool (p x) Bool.true) (Option.some.{0} Int x) (findIf rest p)])]
#[]
---
theorem
findIf_some
∀ (xs : List ℤ) (p : ℤ → Bool), (∃ x ∈ xs, p x = true) → ∃ y ∈ xs, findIf xs p = some y ∧ p y = true
#[Quot.sound, propext]
---
def
findIf
List ℤ → (ℤ → Bool) → Option ℤ
:= fun (xs : List.{0} Int) (p : Int -> Bool) => List.brecOn.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) xs (fun (xs : List.{0} Int) (f : List.below.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) xs) (p : Int -> Bool) => findIf.match_1.{1} (fun (xs._@.temp.tmpzkqz0rde.proof._hyg.15 : List.{0} Int) => (List.below.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) xs._@.temp.tmpzkqz0rde.proof._hyg.15) -> (Option.{0} Int)) xs (fun ([anonymous] : Unit) (x._@.temp.tmpzkqz0rde.proof._hyg.44 : List.below.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) (List.nil.{0} Int)) => Option.none.{0} Int) (fun (x : Int) (rest : List.{0} Int) (x._@.temp.tmpzkqz0rde.proof._hyg.44 : List.below.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) (List.cons.{0} Int x rest)) => ite.{1} (Option.{0} Int) (Eq.{1} Bool (p x) Bool.true) (instDecidableEqBool (p x) Bool.true) (Option.some.{0} Int x) (x._@.temp.tmpzkqz0rde.proof._hyg.44.1 p)) f) p
#[]
---
def
_private.temp.tmpzkqz0rde.proof.0.findIf.match_1.splitter
(motive : List ℤ → Sort u_1) → (xs : List ℤ) → motive [] → ((x : ℤ) → (rest : List ℤ) → motive (x :: rest)) → motive xs
:= fun (motive : (List.{0} Int) -> Sort.{u_1}) (xs._@.temp.tmpzkqz0rde.proof._hyg.15 : List.{0} Int) (h_1 : motive (List.nil.{0} Int)) (h_2 : forall (x : Int) (rest : List.{0} Int), motive (List.cons.{0} Int x rest)) => List.casesOn.{u_1, 0} Int (fun (x : List.{0} Int) => motive x) xs._@.temp.tmpzkqz0rde.proof._hyg.15 h_1 (fun (head._@.temp.tmpzkqz0rde.proof._hyg.42 : Int) (tail._@.temp.tmpzkqz0rde.proof._hyg.43 : List.{0} Int) => h_2 head._@.temp.tmpzkqz0rde.proof._hyg.42 tail._@.temp.tmpzkqz0rde.proof._hyg.43)
#[]
---
def
findIf.match_1
(motive : List ℤ → Sort u_1) →
  (xs : List ℤ) → (Unit → motive []) → ((x : ℤ) → (rest : List ℤ) → motive (x :: rest)) → motive xs
:= fun (motive : (List.{0} Int) -> Sort.{u_1}) (xs._@.temp.tmpzkqz0rde.proof._hyg.15 : List.{0} Int) (h_1 : Unit -> (motive (List.nil.{0} Int))) (h_2 : forall (x : Int) (rest : List.{0} Int), motive (List.cons.{0} Int x rest)) => List.casesOn.{u_1, 0} Int (fun (x : List.{0} Int) => motive x) xs._@.temp.tmpzkqz0rde.proof._hyg.15 (h_1 Unit.unit) (fun (head._@.temp.tmpzkqz0rde.proof._hyg.42 : Int) (tail._@.temp.tmpzkqz0rde.proof._hyg.43 : List.{0} Int) => h_2 head._@.temp.tmpzkqz0rde.proof._hyg.42 tail._@.temp.tmpzkqz0rde.proof._hyg.43)
#[]
---
theorem
_private.temp.tmpzkqz0rde.proof.0.findIf.match_1.eq_1
∀ (motive : List ℤ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (x : ℤ) → (rest : List ℤ) → motive (x :: rest)),
  findIf.match_1 motive [] h_1 h_2 = h_1 ()
#[]
---
theorem
_private.temp.tmpzkqz0rde.proof.0.findIf.match_1.eq_2
∀ (motive : List ℤ → Sort u_1) (x : ℤ) (rest : List ℤ) (h_1 : Unit → motive [])
  (h_2 : (x : ℤ) → (rest : List ℤ) → motive (x :: rest)), findIf.match_1 motive (x :: rest) h_1 h_2 = h_2 x rest
#[]
---
theorem
findIf.eq_1
∀ (p : ℤ → Bool), findIf [] p = none
#[]
---
theorem
findIf.eq_2
∀ (p : ℤ → Bool) (x : ℤ) (rest : List ℤ), findIf (x :: rest) p = if p x = true then some x else findIf rest p
#[]
Finished with no errors.

Second Theorem Proof:

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

import Mathlib.Tactic

:= by
  induction xs with
  | nil => simp [findIf]
  | cons head tail ih =>
    intro h
    rw [findIf]
    aesop

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmpzkqz0rde/target2.olean
Finished imports
Finished replay
---
def
findIf
List Int → (Int → Bool) → Option Int
:= fun (xs : List.{0} Int) (p : Int -> Bool) => sorryAx.{1} (Option.{0} Int) Bool.false
#[sorryAx]
---
theorem
findIf_none
∀ (xs : List Int) (p : Int → Bool), (¬∃ y, y ∈ xs ∧ p y = true) → findIf xs p = none
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpzkqz0rde/proof2.olean
Finished imports
Finished replay
---
def
findIf._sunfold
List ℤ → (ℤ → Bool) → Option ℤ
:= fun (xs : List.{0} Int) (p : Int -> Bool) => [mdata sunfoldMatch:1 findIf.match_1.{1} (fun (xs._@.temp.tmpzkqz0rde.proof2._hyg.15 : List.{0} Int) => Option.{0} Int) xs (fun (_ : Unit) => [mdata sunfoldMatchAlt:1 Option.none.{0} Int]) (fun (x : Int) (rest : List.{0} Int) => [mdata sunfoldMatchAlt:1 ite.{1} (Option.{0} Int) (Eq.{1} Bool (p x) Bool.true) (instDecidableEqBool (p x) Bool.true) (Option.some.{0} Int x) (findIf rest p)])]
#[]
---
theorem
_private.temp.tmpzkqz0rde.proof2.0.findIf.match_1.eq_2
∀ (motive : List ℤ → Sort u_1) (x : ℤ) (rest : List ℤ) (h_1 : Unit → motive [])
  (h_2 : (x : ℤ) → (rest : List ℤ) → motive (x :: rest)), findIf.match_1 motive (x :: rest) h_1 h_2 = h_2 x rest
#[]
---
def
findIf
List ℤ → (ℤ → Bool) → Option ℤ
:= fun (xs : List.{0} Int) (p : Int -> Bool) => List.brecOn.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) xs (fun (xs : List.{0} Int) (f : List.below.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) xs) (p : Int -> Bool) => findIf.match_1.{1} (fun (xs._@.temp.tmpzkqz0rde.proof2._hyg.15 : List.{0} Int) => (List.below.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) xs._@.temp.tmpzkqz0rde.proof2._hyg.15) -> (Option.{0} Int)) xs (fun ([anonymous] : Unit) (x._@.temp.tmpzkqz0rde.proof2._hyg.44 : List.below.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) (List.nil.{0} Int)) => Option.none.{0} Int) (fun (x : Int) (rest : List.{0} Int) (x._@.temp.tmpzkqz0rde.proof2._hyg.44 : List.below.{1, 0} Int (fun (xs : List.{0} Int) => (Int -> Bool) -> (Option.{0} Int)) (List.cons.{0} Int x rest)) => ite.{1} (Option.{0} Int) (Eq.{1} Bool (p x) Bool.true) (instDecidableEqBool (p x) Bool.true) (Option.some.{0} Int x) (x._@.temp.tmpzkqz0rde.proof2._hyg.44.1 p)) f) p
#[]
---
def
_private.temp.tmpzkqz0rde.proof2.0.findIf.match_1.splitter
(motive : List ℤ → Sort u_1) → (xs : List ℤ) → motive [] → ((x : ℤ) → (rest : List ℤ) → motive (x :: rest)) → motive xs
:= fun (motive : (List.{0} Int) -> Sort.{u_1}) (xs._@.temp.tmpzkqz0rde.proof2._hyg.15 : List.{0} Int) (h_1 : motive (List.nil.{0} Int)) (h_2 : forall (x : Int) (rest : List.{0} Int), motive (List.cons.{0} Int x rest)) => List.casesOn.{u_1, 0} Int (fun (x : List.{0} Int) => motive x) xs._@.temp.tmpzkqz0rde.proof2._hyg.15 h_1 (fun (head._@.temp.tmpzkqz0rde.proof2._hyg.42 : Int) (tail._@.temp.tmpzkqz0rde.proof2._hyg.43 : List.{0} Int) => h_2 head._@.temp.tmpzkqz0rde.proof2._hyg.42 tail._@.temp.tmpzkqz0rde.proof2._hyg.43)
#[]
---
def
findIf.match_1
(motive : List ℤ → Sort u_1) →
  (xs : List ℤ) → (Unit → motive []) → ((x : ℤ) → (rest : List ℤ) → motive (x :: rest)) → motive xs
:= fun (motive : (List.{0} Int) -> Sort.{u_1}) (xs._@.temp.tmpzkqz0rde.proof2._hyg.15 : List.{0} Int) (h_1 : Unit -> (motive (List.nil.{0} Int))) (h_2 : forall (x : Int) (rest : List.{0} Int), motive (List.cons.{0} Int x rest)) => List.casesOn.{u_1, 0} Int (fun (x : List.{0} Int) => motive x) xs._@.temp.tmpzkqz0rde.proof2._hyg.15 (h_1 Unit.unit) (fun (head._@.temp.tmpzkqz0rde.proof2._hyg.42 : Int) (tail._@.temp.tmpzkqz0rde.proof2._hyg.43 : List.{0} Int) => h_2 head._@.temp.tmpzkqz0rde.proof2._hyg.42 tail._@.temp.tmpzkqz0rde.proof2._hyg.43)
#[]
---
theorem
_private.temp.tmpzkqz0rde.proof2.0.findIf.match_1.eq_1
∀ (motive : List ℤ → Sort u_1) (h_1 : Unit → motive []) (h_2 : (x : ℤ) → (rest : List ℤ) → motive (x :: rest)),
  findIf.match_1 motive [] h_1 h_2 = h_1 ()
#[]
---
theorem
findIf.eq_1
∀ (p : ℤ → Bool), findIf [] p = none
#[]
---
theorem
findIf_none
∀ (xs : List ℤ) (p : ℤ → Bool), (¬∃ y ∈ xs, p y = true) → findIf xs p = none
#[Quot.sound, propext]
---
theorem
findIf.eq_2
∀ (p : ℤ → Bool) (x : ℤ) (rest : List ℤ), findIf (x :: rest) p = if p x = true then some x else findIf rest p
#[]
Finished with no errors.