abstract:{ tactic block

[SkySkimmer]

Overlays:

• Adapt to coq/coq#19023 (Vernacexpr.subproof_kind) rocq-community/rocq-lsp#866

[SkySkimmer]

I guess if there are problems we need users to find them.

[SkySkimmer]

@coqbot run full ci

[Alizter]

How do we abstract goals?

Goal True * True * True.
refine (_, _, _).
1: abstract: auto.

?

[SkySkimmer]

I don't understand the question.

[Alizter]

How would we focus on say the second goal and abstract it at the same time? Do we have to do

2: { abstract: { ... } }

or would something like

abstract 2: { ... }

make more sense?

[SkySkimmer]

Do we have to do

In the current state of the PR yes

[JasonGross]

Maybe it's worth adding transparent_abstract:{ as well while we're at it?

[JasonGross]

Ah, but for transparent abstract we need a name, and I guess that might be ambiguous to parse? We could do transparent_abstract as name: { or transparent_abstract [name]:{. At the very least, it seems worth having low level support for transparent abstract, even if the syntax is not added.

[JasonGross]

We should have a test for the behavior of nested abstract blocks, for the behavior of structured braces inside an abstract block, as well as for invoking abstract tac inside an abstract:{ block.

[SkySkimmer]

Why would transparent_abstract need a name more than abstract?

[JasonGross]

abstract has four more-or-less legitimate use-cases and one questionable use-case:

1. avoid duplication of kernel typechecking while still getting local failures; typical example abstract vm_cast_no_check (eq_refl true) for a reflective procedure
2. compact the evar-map / reduce memory (probably Optimize Proof. is better here); typical example abstract lia
3. opacify a subproof so it is not accessible to conversion; typical examples: everywhere abstract is used in HoTT
4. hide a subproof behind a name so that unfolding of the parent definition does not immediately reveal a big subproof; examples: use in HoTT
5. add a constant to the global environment; examples in fiat-crypto-legacy

Of these, only 5 really needs a name (though 4 may benefit from one). Probably 3 and 4 (and maybe 5) are the ones where the abstract block would be especially nice.

transparent_abstract adds an additional use case:

6. hide a subproof behind an unfoldable name so that the body does not appear in the hypotheses of dependent goals

transparent_abstract would be used for 1 only in exceptional cases, would almost never be used for 2, and is not useful for 3. So transparent_abstract is really only used for 4, 5, and 6, and 4 and 5 both benefit from a name, and 5 only makes sense when the name is specified.

[JasonGross]

I don't want to derail this PR and would love to see it get merged, so feel free to ignore this comment if it is too far out of scope:
It seems like this code is largely generic over abstract. Might it make sense to have a general with_tactic f : { which accepts any Ltac / Ltac2 tactical which accepts a single argument, and applies f to the tactic that instantiates the goal when run? (Alternatively, if it's simpler, it can apply it to the now-defined evar that was instantiated with the block.). So abstract:{ would be syntax sugar for with_tactic (fun tac => abstract tac):{ (or with_tactic (fun v => abstract exact_no_check v):{). This would also make naming with transparent abstract easier, etc. And in some future PR, the ability to add syntax sugar for goal selectors in user-land could be added.

[SkySkimmer]

It's basically equivalent to

Goal True. (* example goal *)
let g := match goal with |- ?g => g end in
let _ := open_constr:(?[tmp] :> g) in
(* we won't be able to do "?tmp" once it's defined, so put it in the goal context *)
unshelve let gevar := open_constr:(let tmp := ?tmp in _ :> g) in
(* reduce the letin before refine so there's no trace in the proof *)
let gevar := eval cbv in gevar in
refine gevar.
[tmp]:{
  exact I. (* or any other tactics *)
}
(* without this unfold the subproof lemma is "let tmp := I in tmp" *)
let tmp := eval unfold tmp in tmp in 
abstract exact tmp.

but a bit more efficient as it doesn't need to communicate through the goal context and so gets to generate one less evar.

I don't really see the point of this with_tactic idea.

[SkySkimmer]

What may make sense as a general feature is some evar variant which doesn't modify the proof but only generates the evar and adds it to the current goal's context. Then the above example would just be

Goal True.
match goal with |- ?g => ghost evar (tmp:g) end.
[tmp]:{ 
  exact I.
}
let tmp := eval unfold tmp in tmp in 
abstract exact tmp.

[ppedrot]

@JasonGross I've been advocating for a while that there should be a way to allow selectors based on arbitrary functions (of Ltac2 type unit -> unit or OCaml type unit tactic). This is clearly outside of the scope of this PR but it's something to keep in mind.

[SkySkimmer]

The current syntax does not seem very forward compatible, it would be good to have a better one. For instance we will probably want to have abstract using, but abstract using foo : { may be problematic for the parser (untested though).

And if we want to allow generalized focus operations using a pair of tactics we need something that handles them, but since abstract is not a tactic (only abstract tac is a tactic) I'm not sure how it should work exactly.

[andres-erbsen]

What about 2: { abstract., also supporting 2: { abstract using name. and 2:{ idtac. abstract. and all : abstract., with potentially a less efficient implementation for the last two? For the computation-blocking use-case, I think I have seen something along the lines of rewrite sealed_eq_refl as a makeshift implementation, and it's always seemed weird that abstract takes a tactic as an argument rather than working like refine.

[SkySkimmer]

@mattam82 suggested something based on [#, eg [#abstract]:{, [#abstract using fo]:{, maybe someday [#select |- _ = true]:{ or some such thing

[proux01]

Maybe we could even skip the semicolumn then.