Remarks on the Chessboard Proof

Thm*  (AH ~ 8)  ((AH{1...8}) ~ 64)

By a series of rewrites and arithmetic simplifications (the Reduce tactic), the goal is successively reduced down to 64 ~ 64, which is implicitly justified by Auto using Thm*  A ~ A,

The theorems

Thm*  a,b:. {a...b} ~ (1+b-a) and

Thm*  a,b:. (ab) ~ (ab)

are invoked explicitly for rewriting, as is the assumption AH ~ 8. For example, the last rewrite reduces the goal

(88) ~ 64 to

(88) ~ 64

rewriting one part by matching against

Thm*  a,b:. (ab) ~ (ab)

to get the instance

(88) ~ (88).

The principle Thm*  (A ~ A')  (B ~ B')  ((A ~ B)  (A' ~ B')) is also implicitly used to justify performing this rewrite inside the "? ~ ?" operator, as is the principle Thm*  (A ~ A')  (B ~ B')  ((A ~ B)  (A' ~ B')) for rewriting inside the "??" operator.

A person assembling a proof without this strict top-down method, might establish the following sequence of facts:

AH ~ 8	[by hypothesis]
{1...8} ~ 8	[Thm*  a,b:. {a...b} ~ (1+b-a) and arithmetic]
(AH{1...8}) ~ (88)	[Thm*  (A ~ A')  (B ~ B')  ((AB) ~ (A'B')) and above]
(88) ~ (88)	[Thm*  a,b:. (ab) ~ (ab)]
(88) ~ 64	[arithmetic]
(AH{1...8}) ~ 64	[chaining through the last 3 facts using Thm*  (A ~ B)  (B ~ C)  (A ~ C)]

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html