I'm trying to read through The Little Prover and the book introduces a language, ACL2, a Common Lisp derivative, for talking about proofs about programming languages.
The book introduces the following statement:
(if (if (equal a 't)
(if 't
a
b)
(equal 'or '(black coffee)))
c
c)
Where (if 't a b) is a, the if-true rule, and (if 'nil a b) is b, the if-false rule.
Now, the book also says we can simplify this statement by using the if-true rule.
(if (if (equal a 't)
a
(equal 'or '(black coffee)))
c
c)
The book then says:
Does the if question (equal a 't) tell us anything about a?
And then answers:
Yes, since a is in the if answer of the question (equal a 't), we know that a is equal to 't.
This deduction really confuses me! It seems to me that since (equal 'or '(black coffee)) is nil, we know the interior if statement is either 't because (equal a 't) is 't if a is 't and then the statement equals a, which we then know to be 't or the statement is 'nill because a is not 't. But, I don't see how we know a is 't.
The book then introduces this theorem:
(dethm equal-if (x y)
(if (equal x y) (equal x y) 't))
Which confuses me even more.