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.