# Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step

On 2/28/2013 8:41 PM, Thomas Sewell wrote:

`I think that the problem with providing "A <= B; B <= A ==> A = B" as
``a conditional rewrite rule is that the simplifier will (probably) see
``this as a rule for rewriting A into B rather than a rule for rewriting
``"A = B" into True. This is too general, it will be applied anywhere
``there is an A with an appropriate type.
`

`One solution is to resolve your rule with Eq_TrueI, for instance, "thm
``equalityI[THEN Eq_TrueI]". Your rule should then look like "A <= B; B
``<= A ==> (A = B) == True", which strongly suggests to the simplifier
``that it should be used only for rewriting actual equalities.
`

`For some reason the system seems to figure this out by itself when
``given the equalityI rule from HOL, which may invalidate this comment.
`
Yours,
Thomas.

Thomas,
Thanks for the input.

`Extraordinarily simple stuff can be a real show stopper for the novice.
``I tried "A <= B; B <= A ==> A = B" after Lar's comment, and it gave me a
``syntax error, and after searching for documentation on how to use
``conditional rewrite rule syntax, particularly how to use the semicolon,
``I couldn't find any, so I gave up.
`

`This time I tried a little harder, doing searches and stuff, looking for
``that semicolon, and finally I decided it must be an operator, so I
``finally tried \<and>, which got me to the next step.
`

`As an aside, the syntax for two other operators that have never worked
``for me in jEdit are "/\" and "\/", but they're listed in the symbols panel.
`

`I could talk about Stackexchange more also, about whether this comment
``would have gotten made if the replies were split up.
`

`Anyway, the conditional rewrite rule looked a little promising, because
``it might be onerous to have to type "(rule)" if I knew I could set
``things up without having to do that.
`

`However, the performance of either of "A <= B; B <= A ==> A = B" or "A
``<= B; B <= A ==> (A = B) == True" is very slow.
`

`I have some examples of sets which are nested about 11 levels deep. It's
``obvious now that Ramana gave me the same formula, but with my own
``notation. I told him it was creating some non-termination, but that's
``not the case. It's just that it takes forever for simp to simplify these
``nested sets. Each level of nesting adds at least twice the time to
``simplify it.
`

`At 7 levels it takes about 15 to 20 seconds, where without this
``conditional simp rule in, it takes no time, and those examples don't
``even need that rule.
`

`Conditional rewriting will come in handy now that I've made the
``connection between "conditional" and the conditional "==>". That wasn't
``an easy connection to make. Information overload or just a lack of the
``necessary amount of hand holding.
`
Thanks for the suggestion,
GB

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*