[isabelle-dev] Safe approach to hypothesis substitution mark II

[Thomas Sewell]

OK, I've finished repairing all of HOL for "isabelle build -a", though I see in the log that perhaps I should set ISABELLE_FULL_TEST.

I also found a bug while converting some old L4.verified proofs. It's a minor issue to do with tactic ordering and a missing REPEAT_DETERM1 in the var-specific case of the preexisting hypsubst. The new version I attach makes doubly sure that equalities have been substituted before they're thinned. (This is also a patch against Isabelle2013-1.)

The impression I get is that we might proceed with this change, but let me address some concerns people had.

To address Jasmin and Larry's concern, it is possible to switch back to the "compatibility mode" by setting a config variable in the context, or by calling the ML version with an extra parameter. Any legacy proof script can be repaired by adding the line "using [[ hypsubst_thin = true ]]" before any apply/by line. Some of the adjustments in my patch take this approach. Given the small percentage of scripts that break, this seems acceptable for all but the largest developments.

I mostly avoided this approach in patching HOL, since I think that proofs in the distribution should aim to be self-explanatory, and use of this feature is particularly mysterious.

I understand why Tjark and Larry would prefer a minimal change, using contextual information to decide when to deviate from the old behaviour. It would certainly create less maintenance work. Let me elaborate why this approach is my first preference:
  1) As mentioned before, the existing behaviour can be unsafe in subtle cases involving schematic variables with only locally fixed variables.
  2) Having the behaviour of tactics change because of largely invisible background concerns seems a recipe for confusion. This particularly applies to building-block tactics such as safe and clarify. I would prefer they be predictable and reliable.
  3) The extra assumptions are sometimes valuable in their own right. For instance, having the extra premise that "xs = [(a, b), (aa, ba), (aaa, baa)]" allows me to:
  - understand which case my subgoal is in and what the local variables mean.
  - strengthen my assumptions to assist in this case, e.g. if "aa = aaa" creates a problem, maybe I need to assume "distinct (map fst xs)"
  - give names to values using global names, e.g. "fst (xs ! 2)", rather than invented ones "aaa", for instance if rule_tac/subgoal_tac is needed.

For those reasons I'd prefer to plough ahead as long as the impact is manageable. I'll test the AFP and ISABELLE_FULL_TEST soon. I'm running out of energy for this side project, however. If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] globally in them, but I hope to avoid that for the same reason as (2) above: having invisible adjustments to standard tactics seems like something we should avoid.

All thoughts still welcome.

Cheers,
    Thomas.

________________________________________
From: Makarius [makarius at sketis.net]
Sent: Tuesday, January 14, 2014 2:47 AM
To: Thomas Sewell
Cc: isabelle-dev at in.tum.de
Subject: Re: [isabelle-dev] Safe approach to hypothesis substitution mark II

On Mon, 13 Jan 2014, Thomas Sewell wrote:

> Given a hypothesis of the form "x = Suc a" or "Suc a = x", where x is a
> free (blue) variable, hypsubst will substitute "Suc a" for x throughout
> the goal, and then discard the hypothesis. The substitution is almost
> always wanted. Discarding the hypothesis may, however, be unsafe, since
> there may be facts about x at the proof or locale level that now cannot
> be used. It may also be unsafe in the subtle case where a schematic
> variable in the goal can be instantiated to functions of x but not of
> "Suc a". This unsafeness is undesirable because hypsubst is called from
> tactics that are meant to be safe.

> Here's what's changed:
>  1) the new behaviour is to keep hypotheses of the form "x = Suc a"
>     where x is free, and to reorient equalities of the form "Suc a = x"
>     (to "x = Suc a", which is kept). Equalities on bound variables are
>     still removed immediately.
>  2) when any action is taken (substitution or reorientation) and a
>     hypothesis kept, it is moved to last place amongst the hypotheses in
>     the goal. This is different to my previous proposed patch. I suspect
>     it might reduce the number of times the new hypotheses are picked by
>     erule or similar in old scripts. I do not yet have any empirical
>     evidence this helps.
>  3) the old behaviour is provided via new method hypsubst_thin and
>     Hypsubst.hyp_subst_tac_thin in ML. The setting [[ hypsubst_thin =
>     true ]] also restores the old behaviour, and can be used to repair
>     otherwise unrepairable proofs.Some of these features might need a
>     better name.

This sounds quite reasonable to me, although I am not a proven expert of
hypsubst.  Whenever I had a question about it in the past, I would first
consult Stefan Berghofer.

As I've already pointed out in the discussion some years ago, the "proof
of correctness" of such a change works empirically, against the body of
existing applications in the Isabelle repository and AFP.  You have also
access to classified L4.verified material, and might take big external
projects like IsaFoR into account.

The changes so far appear to be below the level of significance -- we've
had much more substantial upheavals in the past.

With an easy escape, i.e. the alternate name of the proof method and a
confifuration option to recover the old behaviour, users should manage to
convert their old stuff reasonably well.


        Makarius

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hypsubst.diff
Type: text/x-patch
Size: 57000 bytes
Desc: hypsubst.diff
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140114/fe2e2958/attachment-0002.bin>