CSCI H343 Data Structures Fall 2025

Deduce Proof Exercise 1

Overview

For this assignment, you will get started writing your own proofs of theorems in Deduce.

As a reminder, you can refer to the following

• Deduce Reference Manual,
• Introduction to proofs in Deduce
• Cheat Sheet for Proofs

Learning Goals

These exercises are meant for you to practice the following logical concepts in Deduce:

• all formulas, arbitrary, and proof instantiation.
• if-then formulas, assume, apply-to
• and formulas, conjunct, combining proofs with comma.
• expand a definition
• replace equals for equals
• forward reasoning using have

Problems

(1) Complete the following proof. The append function ++ is defined in lib/List.pf.

theorem append_xy: all T:type. all x:T, y:T.
  node(x, empty) ++ node(y, empty) = node(x, node(y, empty))
proof
  ?
end

(2) Prove that [1] ++ [2] = [1, 2] by using the append_xy theorem.

theorem append_1_2:
  [1] ++ [2] = [1, 2]
proof
  ?
end

(3) Prove that if xs = [], then length(xs) = 0.

theorem equal_empty_length_zero: all T:type, xs:List<T>.
  if xs = []
  then length(xs) = 0
proof
  ?
end

(4) Prove that if P and Q then R implies if Q then if P then R.

theorem ex_all_if_and: all P:bool, Q:bool, R:bool.
  if (if P and Q then R) then (if Q then if P then R)
proof
  ?
end

(5) Prove that if P then Q and if Q then R implies if P then R.

theorem ex_if3: all P:bool, Q:bool, R:bool.
  if (if P then Q) and (if Q then R)
  then (if P then R)
proof
  ?
end

(6) Prove that if if P then (if Q then R) and if P then Q and also P, then R.

theorem ex_if_if: all P:bool, Q:bool, R:bool. if (if P then (if Q then R)) and (if P then Q) and P then R
proof
  ?
end

This site is open source. Improve this page.