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 sorry

Bounty: 0.02 ETH

Status: Closed

Proof

theorem list_length_reverse {α : Type} (l : List α) : l.reverse.length = l.length := by
  induction l with
  | nil => simp
  | cons hd tl => simp

Back to Bounties