Abbrevs should not have their variables rewritten

[mn200]

Tactics such as FULL_SIMP_TAC should not rewrite the variable occurring to the left in an Abbrev assumption. This should be easy enough to achieve with a custom congruence.

[binghe]

I have been trying very hard to avoid this issue (by choosing alternative, less damaging tactics) when proving borelTheory.lborel0_premeasure. Hope it can be fixed soon, then I can replay some proofs and simplify them.

[mn200]

I'm glad someone else finds this annoying! (In that it provides extra motivation to make the fix; not that I'm happy in someone else's suffering... 😄 )

[mn200]

Equally, the variable elimination that happens as part of rw and friends shouldn't result in assumptions such as

   Abbrev(complicated-term1 = complicated-term2)

the abbreviation could be left alone entirely, but this seems like it would probably be a mistake. My feeling is that instead we should just pick up a new assumption

  complicated-term1 = complicated-term2

[binghe]

Somehow currently rw and its friends modifies assumptions, replacing variables defined by Abbrev. This doesn't seem right -- only FULL_SIMP_TAC (or fs) should rewrite existing assumptions.

Besides, rw and its friends rewrite the goal using assumptions in forms u = v no matter a single variable is u or v, but actually the user may carefully choose to push u = v instead of v = u (into assumptions) just to make sure that any potential rewriting can only be from u to v but the other direction.

Overall speaking, rw and its friends are too "smart" which means "stupid" in non-trivial cases as their effects are often out of control, and user has to limit their uses and use simp-series tactics whatever possible.

[konrad-slind]

The original design for rw_tac (underlying rw[]) deliberately got rid of all suitable v = t or t = v bindings in the assumptions. Abbrev is supposed to stake out a "hard" name for a term and the abbrev-binding should survive the operations of rw_tac. Now rw_tac eliminates variable bindings via VAR_EQ_TAC. So maybe VAR_EQ_TAC should be Abbrev-aware. Not quite sure what this would entail though, without seeing examples of good and bad behavior. However, assuming that equations t=v should be left alone would be a big change I expect.

Konrad.

On Sat, Apr 18, 2020 at 10:17 AM Chun Tian notifications@github.com wrote:

Somehow currently rw and its friends modifies assumptions, replacing variables defined by Abbrev. This doesn't seem right -- only FULL_SIMP_TAC (or fs) should rewrite existing assumptions.

Besides, rw and its friends rewrite the goal using assumptions in forms u = v no matter a single variable is u or v, but actually the user may carefully choose to push u = v instead of v = u (into assumptions) just to make sure that any potential rewriting can only be from u to v but the other direction.

Overall speaking, rw and its friends are too "smart" which means "stupid" in non-trivial cases as their effects are often out of control, and user has to limit their uses and use simp-series tactics whatever possible.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/800#issuecomment-615887983, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD6Q4VYXJNBL5K336I3RNG77HANCNFSM4LSKHZ3A .

[mn200]

My latest idea for the branch where I'm working on this is to have VAR_EQ_TAC replace malformed abbreviations Abbrev (t1 = t2) (malformed means that t1 is no longer a variable) with the equation t2 = t1. This approximates the way such abbreviations will have been handled when still wrapped in the Abbrev tag.

[mn200]

Work on this is now merged to develop and master, via ee0a2108d

[binghe]

Work on this is now merged to develop and master, via ee0a210

Great work. I'll merge latest develop into the branch of my PR and see if anything is broken.