[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: What have I missed ? (a proof failed)




Yechiel:
 Here's some more information to add to what has
already been said in response to your query.

1. As John Hoffman noted, the axiom is false, as is the
theorem.

2. The axiom is a well-formed rewrite rule: it rewrites
s = st to TRUE when size(s) = size(st) and
(FORALL i: (i < size(s) => lmnts(s)(i) = lmnts(st)(i))).
A well-formed rewrite rule is one which is of the form
H => l = r or its universal closure (with H possibly empty),
where the free variables in H and r are a subset
of those in l.  In this case, l is s = st and r is TRUE.

3. The reason it doesn't get rewritten is that the
simplifier does not have the smarts to simplify the
universally quantified hypothesis to TRUE.  The simplifier
might be strengthened to do this in a future patch release.

4.  If rewrite rules (say "equal_ax" and "equal_ax2") appear to not have
been triggered, then give the proof command
 (track-rewrite "equal_ax" "equal_ax2") before invoking assert
or grind.  This displays the reason why the rewrite rule
wasn't triggered.

-Shankar