Submission Details

Back to Submissions List

Challenge: rev

Submitted by: Zhe Ye

Submitted at: 2025-05-18 00:47:11

Code:

def rev(xs: List Int): List Int

:= xs.reverse

First Theorem Proof:

theorem reverse_correct(xs:List Int):
  xs.length=(rev xs).length ∧
  ∀ i<xs.length, xs[i]! =(rev xs)[xs.length-1-i]!

:= by
  unfold rev
  constructor
  · exact Eq.symm List.length_reverse
  · intro i hi
    have hi' : xs.length - 1 - i < xs.length := by exact Nat.sub_one_sub_lt_of_lt hi
    simp only [List.getElem!_eq_getElem?_getD, hi, List.getElem?_eq_getElem, Int.default_eq_zero,
      Option.getD_some, List.length_reverse, hi']
    exact List.getElem_eq_getElem_reverse hi

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmp1zbqbzfx/proof.lean:
/root/CodeProofTheArena/temp/tmp1zbqbzfx/proof.lean:14:18: error: application type mismatch
  Eq.symm List.length_reverse
argument
  List.length_reverse
has type
  ∀ (as : List ?m.357), as.reverse.length = as.length : Prop
but is expected to have type
  xs.reverse.length = xs.length : Prop
/root/CodeProofTheArena/temp/tmp1zbqbzfx/proof.lean:17:15: error: unknown constant 'List.getElem!_eq_getElem?_getD'
/root/CodeProofTheArena/temp/tmp1zbqbzfx/proof.lean:17:4: error: simp made no progress