CSCI C343 Data Structures Spring 2025

Writing Proofs in Deduce

Concepts:

• theorem statement
• definition proof

Example:

theorem len_empty: 0 = len(Empty)
proof
  definition len
end

Concepts:

• all formula,
• arbitrary proof,
• suffices proof, and
• evaluate proof.

Example:

theorem len_one: all x:Nat. len(Node(x, Empty)) = 1
proof
  arbitrary x:Nat
  suffices 1 + 0 = 1 by definition {len, len}
  evaluate
end