Stream: Coq users

Topic: Which tactics manipulate the whole proof term?

Patrick Nicodemus (Mar 28 2023 at 11:58):

Most tactics are in some sense based on refine in that they replace a unification variable with a partially defined term. What tactics, if any, cannot be accomplished this way and you have to change the proof term outside of the unification variable corresponding to the goal

Gaëtan Gilbert (Mar 28 2023 at 12:46):

https://coq.github.io/doc/master/refman/proofs/writing-proofs/proof-mode.html#coq:tacn.solve_constraints ?

Patrick Nicodemus (Mar 28 2023 at 13:59):

Nice, thank you. This is a good example. This command instantiates unification variables and thus fleshes out an existing (partially defined) term with more structure. Are there tactics which rearrange already existing structure of the proof tree. For example, the existing proof term is t[X] where X is some unification variable, and after the tactic is executed, the proof term becomes

match a with (...) return (...) in
|  constr s1 s2 =>   t[f(s1, s2, Y)]
end

for some unification variable Y.

Patrick Nicodemus (Mar 28 2023 at 14:00):

My point is that we are not just (partially) instantiating unification variables but perhaps adding new structure above and around the existing proof term which changes the context in which the metavariable X lives?

Gaëtan Gilbert (Mar 28 2023 at 14:08):

My point is that we are not just (partially) instantiating unification variables but perhaps adding new structure above and around the existing proof term which changes the context in which the metavariable X lives?

I don't think that's allowed

Gaëtan Gilbert (Mar 28 2023 at 14:11):

the structure of the proof data is this stuff https://github.com/coq/coq/blob/dc2dd34bd23e55c3deeb556c5136c72ea3352e99/proofs/proof.ml#L111-L113
entry is the proof term of the whole proof, typically starts as an evar
then as we run tactics they may define evars in the evar map (which is inside the Proofview.proofview)
undefining evars is not allowed (modulo some hacks in ssr which AFAIK are supposed to be local)

Pierre-Marie Pédrot (Mar 28 2023 at 14:55):

yes, basically the only thing you can do is define evars and create new ones (+ additional metadata storing)

Last updated: Sep 23 2023 at 07:01 UTC