Submission Details

Back to Submissions List

Challenge: mapInt

Submitted by: GasStationManager

Submitted at: 2024-11-26 03:11:05

Code:

def mapInt(xs:List Int)(f:Int->Int):List Int

:= []

/- retrying Eric Wieser's entry -/

syntax (name := badTheorem) declModifiers group("theorem " declId ppIndent(declSig)) : command
@[command_elab badTheorem] def expandBadTheorem : Lean.Elab.Command.CommandElab := fun _ => pure ()

import Lean.Elab.Command

First Theorem Proof:

theorem mapInt_correct(xs:List Int)(f:Int->Int)
: (mapInt xs f).length=xs.length
∧  ∀ i:Fin xs.length, (mapInt xs f)[i]! = f xs[i]

-- sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpxno3_x9g/proof.olean
uncaught exception: mapInt_correct not found in submission
------------------
Replaying /root/CodeProofTheArena/temp/tmpxno3_x9g/target.olean
Finished imports
Finished replay
---
def
mapInt
List Int → (Int → Int) → List Int
:= fun (xs : List.{0} Int) (f : Int -> Int) => sorryAx.{1} (List.{0} Int) Bool.false
#[sorryAx]
---
theorem
mapInt_correct
∀ (xs : List Int) (f : Int → Int), (mapInt xs f).length = xs.length ∧ ∀ (i : Fin xs.length), (mapInt xs f)[i]! = f xs[i]
#[sorryAx, propext]
------------------
Replaying /root/CodeProofTheArena/temp/tmpxno3_x9g/proof.olean
Finished imports
Finished replay
---
def
expandBadTheorem
Lean.Elab.Command.CommandElab
:= fun (x._@.temp.tmpxno3_x9g.proof._hyg.44 : Lean.Syntax) => Pure.pure.{0, 0} Lean.Elab.Command.CommandElabM (Applicative.toPure.{0, 0} Lean.Elab.Command.CommandElabM (ReaderT.instApplicativeOfMonad.{0, 0} Lean.Elab.Command.Context (StateRefT' IO.RealWorld Lean.Elab.Command.State (EIO Lean.Exception)) (StateRefT'.instMonad IO.RealWorld Lean.Elab.Command.State (EIO Lean.Exception) (instMonadEIO Lean.Exception)))) Unit Unit.unit
#[propext, Quot.sound]
---
def
mapInt
List Int → (Int → Int) → List Int
:= fun (xs : List.{0} Int) (f : Int -> Int) => List.nil.{0} Int
#[]
---
def
badTheorem
Lean.ParserDescr
:= Lean.ParserDescr.node (Lean.Name.mkStr1 "badTheorem") (OfNat.ofNat.{0} Nat 1022 (instOfNatNat 1022)) (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.const (Lean.Name.mkStr1 "declModifiers")) (Lean.ParserDescr.unary (Lean.Name.mkStr1 "group") (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.symbol "theorem ") (Lean.ParserDescr.const (Lean.Name.mkStr1 "declId"))) (Lean.ParserDescr.unary (Lean.Name.mkStr1 "ppIndent") (Lean.ParserDescr.const (Lean.Name.mkStr1 "declSig"))))))
#[]