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

[Ramana K. <Ram...@cl...>]

My proposal using constant definitions would not work if the metavar
instantiations contain free variables.
One way to recover is to add the free variables as arguments to the
constant.

I think in your example, there is no problem, because you never have a
lifted tactic followed by an evars-tactic that instantiates metavars that
the lifted tactic can see.

However, I think Magnus's suggestion (change the tactic type in HOL to
support evars) is more worth exploring than my suggestion based on defining
constants and re-running lifted tactics inside their validation (which is
rather slow/ugly).

On 1 September 2016 at 02:28, Armaël Guéneau <arm...@en...>
wrote:

> > >     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...> <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...> <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...> <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 > >
>
>