Theorem Marketplace

Theorem Details

-- Prove that reversing a list does not change its length

theorem list_length_reverse {α : Type} (l : List α) : l.reverse.length = l.length := by
  induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [List.reverse_cons, List.length_append, List.length_singleton, ih]
    simp

Bounty: 0.02 ETH

Status: Open

Submit Your Proof

Back to Bounties