In this lecture we begin to learn how to write proofs in Deduce.
The proofs will use the definitions from the previous lecture.
Concepts:
Example:
theorem prove_true: true
proof
.
end
Concepts:
Examples:
theorem len_empty: 0 = len(Empty)
proof
expand len. // len(Empty) = 0
end
theorem ex_expand: search([4, 3, 8], 8) = 2
proof
expand search
show 1 + search([3, 8], 8) = 2
expand search
show 2 + search([8], 8) = 2
expand search
.
end
Concepts:
Example:
theorem len_one: all x:UInt. len(Node(x, Empty)) = 1
proof
arbitrary x:UInt
expand len | len.
end
Concepts:
Examples:
theorem len_42: 1 = len(Node(42, Empty))
proof
replace len_one[42].
end
theorem first_pair_123: first(second(pair(1,pair(2,3)))) = 2
proof
replace second_pair
show first(pair(2, 3)) = 2
replace first_pair.
end
Concepts:
Example:
theorem if_commute: all P:bool, Q:bool, R:bool.
if (if P then if Q then R) then (if Q then if P then R)
proof
arbitrary P:bool, Q:bool, R:bool
assume pqr: if P then if Q then R
assume: Q
assume: P
have qr: if Q then R by apply pqr to (recall P)
apply qr to (recall Q)
end
Concepts:
Example:
theorem ex_and: all P:bool, Q:bool, R:bool. if P and Q and R then R and P
proof
arbitrary P:bool, Q:bool, R:bool
assume pqr
have r: R by conjunct 2 of pqr
have p: P by conjunct 0 of pqr
r, p
end