Re: [Hol-developers] CF tactics, postcondition inference, meta-variables

[Armaël G. <arm...@en...>]

> >     This discussion should probably move to the HOL mailing lists, >     even though most active HOL developers are also on the CakeML dev >     list. > > I agree. Therefore, I am replying to the HOL dev mailing list. See the initial thread copied below. > > I have a suggestion for defining lift, following your approach that re-runs the tactic in the validation. > How about introducing intermediate terms for the specialisation, to avoid the tactic doing too much? > Thus, I suggest something like: > > fun lift tac metavars g = >   let >     val (gls, _) = tac g >     fun validation inst thl = >       let >         val (inst1,defs) = fresh_evars metavars inst >         val thl1 = uninst_thms gls defs thl >         val g1 = inst_goal inst1 g >       in >         snd (tac g1) thl1 >       end >   in (gls, validation) end > > Given an instantiation inst which takes metavars x and y to 2 and 3, I suggest fresh_evars introduce new constants representing the instantiated evars, Cx
and Cy, and returns inst1 = [x|->Cx, y|->Cy] and defs = [|- Cx = 2, |- Cy = 3]. > > Then, uninst_thms looks for places in the proved subgoals where a metavar has been instantiated, and uses the defs to replace the instantiation with the new constant. So if you had |- 2 = 2 in thl, but the original subgoal was ?- x = 2, then the new thl1 becomes |- Cx = 2, by rewriting the lhs with SYM (el 1 defs). > > I'm not sure if this is possible to achieve without definitions of new constants. You could possibly do it with fresh variables, but you may need to carry around the defs as assumptions in that case. The advantage of constants is that their definitions can be kept around in separate theorems. But you probably want to delete them afterwards, and it's quite heavyweight.

I don't know much about the constant definition system, but how would that work if the metavariable is instantiated by a free variable (at that time)?
More precisely, how would the following "proof with evars" work:

g `!x. ?y. x = y`
e (lift gen_tac \\ meta_exists \\ meta_inst1 `y` `x` \\ lift (fs []))

(where meta_exists turns a goal of the form `?y. P` into `P` where `y` became a metavariable; and meta_inst1 instantiates a metavariable). `y` as a metavariable is instantiated with `x`, a free variable that then gets generalized by gen_tac. Do you think that would work with the method you suggest?

— Armaël

> By the way I also want to note that Isabelle/HOL has schematic variables for these metavars. So Coq has evars, Isabelle has schematic vars, ... are we about to join that club? It would be really nice to find a lighter weight way of achieving this. > > > On 21 August 2016 at 07:51, Konrad Slind <kon...@gm...> wrote: > >       Datapoint: years ago, John Harrison spent some time implementing >     meta-variables for HOL Light. Not sure if this was inside the kernel, or just >     on top. (The latter, I think, which means that he had to deal with the same >     issues as being discussed here.) > >     He dropped the effort on the grounds that the code was becoming too complex >     for his goals in HOL Light, e.g., simplicity.  But there is no doubt more to >     the story and you should go to the source (have cc'ed John). > >     Cheers, >     Konrad. > > > >     On Sat, Aug 20, 2016 at 12:09 PM, Magnus Myreen <mag...@gm...> wrote: > >         Hi Armaël and dev, > >         Thanks for the clear explanation. > >         > 2) Implement metavariables in HOL. >         > >         > Provided that they work nicely, they would have the advantage of producing nicer >         > goals. [...] > >         I
prefer option (2) because it seems like the right thing to do for >         the long term. > >         > Implementing metavars requires defining a custom proof manager, and (among >         > others) an alternative [Evars.tactic] type, for tactics that know about >         > metavariables, and that can instantiate them. > >         Having two proof managers sounds like a mess. > >         Would it be possible to change the tactic type in HOL to support evars? > >         I know such a change could potentially cause an enormous amount of >         breakage. However, as far as I know, most tactic implementations are >         written as compositions of very low-level tactics. If the breakage >         would mostly be limited to simple adjustments to the very lowest level >         tactics, then maybe there is a chance to change the tactic type to >         allow evars. I'm thinking that we might be able to get things working >         as they were before for all proofs that do
not use metavariables, and >         then one could gradually make match_mp_tac etc. smarter in cases where >         evars are present. > >         I'm keen to hear what Michael and the other HOL developers think of >         this. This discussion should probably move to the HOL mailing lists, >         even though most active HOL developers are also on the CakeML dev >         list. > >         Cheers, >         Magnus > > >         On 20 August 2016 at 16:15, Armaël Guéneau <arm...@en...> wrote: >         > >         > Hi dev, >         > >         > I appear to be half-stuck/indecise on the question of how to get the proper >         > tactics to deal with CFs for let. So I thought I'd ask for advices. >         > >         > Currently, when dealing with the CF for [let val x = e1 in e2 end], one has to >         > provide manually beforehand the postcondition for evaluating [e1]. This is not >         > ideal, and can be avoided. In particular, in CFML it
is not required. >         > >         > The goal corresponding to a CF for [let val x = e1 in e2 end] is of the form: >         > >         >   cf_let x (cf e1) (cf e2) env H Q >         > >         > After some unfolding, it becomes: >         > >         >   ?Q'. >         >     (cf e1) env H Q' /\ >         >     !xv. (cf e2) ((x, xv)::env) (Q' xv) Q >         > >         > Now, 99% of the time, you do not want to give an instantiation for Q' right >         > away: H being known, proving the first subgoal [(cf e1) env H Q'] will in fact >         > end up providing an instantiation for Q'. >         > >         > CFML deals with that by using the "metavariables" mechanism of Coq (or "evars"), >         > which allows instantiating an exists by a metavariable, which will be actually >         > instantiated later in the proof. >         > >         > If _Q' is the metavariable for Q', then the goal becomes >         > >         >   (cf e1) env H _Q' /\ >         >   !xv.
(cf e2) ((x, xv)::env) (_Q' xv) Q >         > >         > It is then easy to split it, prove the first subgoal, which will instantiate _Q' >         > to the real thing, and then the proof can continue with >         > [!xv. (cf e2) ((x, xv)::env) (Q'' xv) Q] for some Q''. >         > >         > >         > For CFs in CakeML, as HOL doesn't currently have such a feature, I experimented >         > with two options: >         > >         > 1) Implement a small library of composable "rewrites", à la conseqConv, that >         > would apply under existential quantifications, and that would be able to >         > instantiate them. >         > >         > With a goal of the form >         > >         >   ?Q'. >         >     X /\ >         >     Y >         > >         > the CF tactics would do some work on X, hopefully eventually instantiating Q', >         > such that the goal would reduce to Y[Q''/Q']. >         > >         > Now, in full generality, these composable rewrites
need not only to apply under >         > exists, but under a succession of exists and forall, which spices things up a >         > bit. >         > >         > For example, consider a program of the form: >         > >         >   let val x = >         >     let val y = e1 >         >     in e2 end >         >   in e3 end >         > >         > The corresponding goal is of the form (for some env, H, Q): >         > >         >   cf_let x >         >     (cf_let y (cf e1) (cf e2)) >         >     (cf e3) >         > >         > and after some unfolding: >         > >         >   ?Q' Q''. >         >     ((cf e1) env H Q'' /\ >         >      !yv. (cf e2) ((y, yv)::env) (Q'' yv) Q') /\ >         >     !xv. (cf e3) ((x, xv)::env) (Q' xv) Q >         > >         > After doing work on [(cf e1) env H Q''], Q'' usually gets instantiated, and the >         > goal becomes: >         > >         >   ?Q'. >         >     (!yv. (cf e2) ((y, yv)::env) (Q'' yv) Q') /\ >         >     !xv.
(cf e3) ((x, xv)::env) (Q' xv) Q >         > >         > We want to do work on [(cf e2) ((y, yv)::env) (Q'' yv) Q'], and hopefully >         > instantiate Q'. >         > >         > -------/ end of the example /--------- >         > >         > For the moment (and with the help of Thomas Tuerk), I have a small library of >         > conseqConv+instantiations that only work under toplevel exists, and allow to >         > instantiate them. >         > >         > I think I can extend it to handle nestings of forall and exists. My concerns are >         > that: >         > >         > - Although they appear only when nesting lets (which I guess is not so common >         >   but can definitely happen), these goals with nested exists and forall may look >         >   scary and annoying to manipulate for the user. >         > >         > - In non-trivial program proofs, CF-specific tactics should clearly make less >         >   than half of the proof. Most of the work would be
proving invariants of the >         >   specific program that is being certified. >         > >         >   Then, would that mean the user would also have to use complex proof machinery >         >   to deal with this goals, where the current "subgoal" is under several exists >         >   and forall?  Maybe it's not too bad, but it's definitely an additionnal >         >   difficulty to be taken into account. >         > >         > >         > 2) Implement metavariables in HOL. >         > >         > Provided that they work nicely, they would have the advantage of producing nicer >         > goals. The intuition is that they allow to strip the exists and forall from the >         > goal altogether, and then check that metavariables are not instantiated using >         > foralls that have been introduced after them. >         > And with the way the CF tactics are designed, this kind of illegal >         > instantiations will likely never be an issue, or appear to the user.
>         > >         > Implementing metavars requires defining a custom proof manager, and (among >         > others) an alternative [Evars.tactic] type, for tactics that know about >         > metavariables, and that can instantiate them. >         > >         > I implemented that, although it's hardly tested and probably buggued, + some >         > features are missing. >         > >         > However, the main issue is as follows: there needs to be a "lift" function, of >         > type [Abbrev.tactic -> Evars.tactic]. This is such that users can use their >         > everyday tactics when arriving to the bulk of the proof. And also such that not >         > every tactic in the world needs to be reimplemented "with evars". >         > >         > The way the proofmanager with evars works is as follows: >         > >         > - metavariables (evars) are free variables of the goal >         > - an Evars.tactic is called with the goal, and the list of free variables that
>         >   are metavariables >         > - the Evars.tactic produces subgoals >         > - the theorems that the validation function receives prove the subgoals, *except >         >   that some metavariables may have been instantiated*. >         > >         > This last point is problematic for lifting standard tactics. These do not expect >         > to receive theorems for the validation function that do not directly prove the >         > subgoals. >         > >         > Therefore, the naive implementation of lift does not work: >         > >         >   fun lift tac metavars g = >         >     tac g >         > >         > For example, [MATCH_MP_TAC (|- P x ==> Q x)] produces a ``P x`` subgoal, and a >         > validation function that expects (|- P x) as input. If given (|- P 3), the >         > validation function will of course fail, and not produce (|- Q 3). >         > >         > I do not know if it's possible to define lift in a way that works around this
>         > problem. >         > >         > I thought of re-running the tactic entirely in the validation function, but this >         > does not work as the tactic may perform too much work on the specialized goal. >         > >         >   fun lift tac metavars g = >         >     let >         >       val (gls, _) = tac g >         >       fun validation inst thl = >         >         snd (tac (inst_goal inst g)) thl >         >     in (gls, validation) end >         > >         > For example, EVAL_TAC on [x = 2] produces the subgoal [x = 2], so even if x is a >         > metavariable that is specialized to 2 afterwards, lifted EVAL_TAC should produce >         > the subgoal [2 = 2]. Re-runing EVAL_TAC in the lift's validation on [2 = 2] will >         > produce a validation function that solves the goal instead. >         > >         > One idea would be to extend the common HOL tactics so that they handle this >         > situation. I don't know what amount of work this
represent, in order to cover >         > most of the everyday tactics. Or whether it is possible to be implemented >         > without too much overhead (as this may mean re-running some parts of the tactic >         > in the validation function, if the input theorems only prove a specialization of >         > the subgoals). Or whether this is a change that is even remotely likely to get >         > merged... >         > >         > >         > Thoughts? >         > Sorry for the wall of text. >         > >         > — Armaël >         > >         > >         > _______________________________________________ >         > Dev mailing list >         > De...@ca... >         > https://lists.cakeml.org/listinfo/dev > >         _______________________________________________ >         Dev mailing list >         De...@ca... >         https://lists.cakeml.org/listinfo/dev > > > >     _______________________________________________ >     Dev mailing list >     De...@ca...
>     https://lists.cakeml.org/listinfo/dev > >