Transparent abstract

[JasonGross]

This is a small change that allows a transparent version of tclABSTRACT.
Additionally, it factors the machinery of abstract through a
plugin-accessible function which allows alternate continuations (other
than exact_no_check), and allows alternate types (other than the type of the current goal).

It might be nice to have a better interface for caching terms. The use-case of cache_term_by_tactic_then is something like

  Tactic Notation "cache_term" constr(term) "run" tactic(tacK) :=
    let T := type of term in
    cache_term_by_tactic_then id gk ~opaque:false ~tac_type_from_gl:(fun gl -> T) ltac:(exact_no_check term) (fun (lem, args) -> ltac_apply tacK (applist (lem, args))).

I've separated this out into three commits: one which gives tclABSTRACT an option for transparent lemmas, one which makes a transparent_abstract tactic, and one which allows Fiat's plugin to not need typeclass hackery to cache terms. I'd like this to get merged into 8.6.

[ppedrot]

The code looks OK to me, and I find the feature useful. Nonetheless, I though that the general trend promoted by @gares was to get rid of abstract rather than using it more...

[gares]

Why 8.6? It was not in the road map was it?

[ppedrot]

That is right, I assumed it was and categorized it carelessly. Changing the tag then.

[gares]

The code works if using ... is not given. Otherwise I get an interpretation error. @maximedenes and @ppedrot may clarify the ident v.s. preident mess.

The feature should be marked as "use at your own risk" for the following reasons:

• building relevant (as in computationally relevant) terms with tactics is fragile and should not be recommended (e.g. recent regression in unimath in the econstr branch)
• abstract cannot play well with asynchronous proofs, so scripts full of abstract .. using ... are doomed to be processed slower.

It also seems that there was a blacklist for .*_subproof and this patch introduces a .*_subterm class of definitions. Not sure we want to see these as results of Search.

[ejgallego]

I was thinking of proposing some modifications on how abstract is handled, so maybe we could wait a bit on the decision for this PR?

[JasonGross]

The feature should be marked as "use at your own risk" for the following reasons:

Done

It also seems that there was a blacklist for ._subproof and this patch introduces a ._subterm class of definitions. Not sure we want to see these as results of Search.

Added _subterm to the blacklist.

I was thinking of proposing some modifications on how abstract is handled, so maybe we could wait a bit on the decision for this PR?

@ejgallego Can you say more?

The code works if using ... is not given. Otherwise I get an interpretation error.

I can't reproduce. The test-suite file includes a test case for transparent_abstract tac using foo, and, other than misc/deps-order, the test-suite builds fine for me.

[ejgallego]

@ejgallego Can you say more?

The idea won't be concrete at least until the next WG, but I was thinking of replacing side-effects with proof-local environments, such that:

• the environment is guaranteed to be the same before and after Qed;
• term cooking is removed;
• pairs of (constr,env) are stored at Qed time, proofs are checked against their own env;
• thus proof-private constants are not visible anymore (removing the need for the blacklist, etc);
• Definitions and Proofs inside Proofs would be supported and reasonably clean;
• and abstract shouldn't differ too much from the above.

this builds on the functional state handling patch for the STM. However I lack the necessary knowledge to see it the above proposed approach is a) workable and b) desirable.

[JasonGross]

What about abstract and the transparent version here when used in Defined proofs?

Regardless, transparent_abstract is something I'd like to have regardless of such a change, and I expect that the bulk of abstract would not be changed, and that making such a change to abstract wouldn't be significantly complicated by this patch. Do you see a place where they'd conflict?

[ejgallego]

In defined proofs you indeed must propagate the full modified env. Right now the mechanism relies on static analysis, but I'd like to experiment with futures. Thus, for the case of Qed, the env future is resolved immediately, and processing of the next sentence can continue, whereas for Defined they will block on the evaluation of the proof.

I think indeed the ideas I outlined above are orthogonal to this patch, but I wanted to be sure that there is no conflict.

[ejgallego]

@JasonGross travis says that doc building is broken .

[JasonGross]

Sorry for the delay. I've updated the docs to replace _ with \_ when outside of math mode, and they now build for me.

[JasonGross]

Rebased on top of newly-merged econstr. Any update on the status of merging this?

[JasonGross]

Bump. Any update on this?

[JasonGross]

@maximedenes please remove the fix_needed tag

[maximedenes]

@ejgallego @gares do you confirm this is ok for you? If yes, I'll merge it.

[ejgallego]

Based on my understanding of the current situation and roadmap, this patch is fine for me. However, as @gares said, I would mark this tactic "use at your own risk/experimental".

People relying on this should be willing to deal with a possibly unstable feature.

[JasonGross]

@ejgallego is the current warning in the refman insufficient?

[ejgallego]

Personally that's OK for me, but I wonder what is the general policy here wrt experimental features. Maybe we should keep a list ?

[JasonGross]

Thanks!