RanDair Scott Porter (May 10 2021 at 21:43): RanDair Scott Porter (May 10 2021 at 21:43):I'm using Proof.run_tactic in Coq 8.9, and I would like to get back the new contexts (an env) and conclusions (a constr) for each subgoal.
I am able to get a Goal.goal list, and I am able to use the functions Goal.V82.env, Goal.V82.concl, and Goal.V82.abstract_type.
Goal.V82.env seems to return nothing.Goal.V82.concl returns the correct conclusion, but all of the Rel indices are replaced with Vars.Goal.V82.abstract_type returns the conclusion with the correct indices, BUT it is prepended with a Product for every name in the new context. This isn't enough because I can't tell how many products still belong in the new conclusion.Any tips? Thank you!
Talia Ringer (May 12 2021 at 17:41):buuump we'd super love help if anyone knows :). @Emilio Jesús Gallego Arias ?
Talia Ringer (May 12 2021 at 17:43):RanDair does val hyps : t -> EConstr.named_context get you anything?
Talia Ringer (May 12 2021 at 17:43):I think that would be what maps the vars
Gaëtan Gilbert (May 12 2021 at 18:42):have a look around https://github.com/coq/coq/blob/5714656cb3f8a676c126a8d8e67ea2d92781d780/engine/proofview.mli#L517 (8.9 api should be similar)
Goal.V82.env seems to return nothing.
I don't know what you mean by "nothing"
Goal.V82.concl returns the correct conclusion, but all of the Rel indices are replaced with Vars.
Var is correct, I don't know why you expect Rel
Emilio Jesús Gallego Arias (May 12 2021 at 18:45):I don't even have a 8.9 tree around that works in my current dev workflow sorry @Talia Ringer , I was hesitant to give thus incorrect advice; one thing that may help is to look at the goal printer, there you can see how the different bits of goals are extracted from the proof state, but that API is still a bit in flux (Proof.t and friends)
RanDair Scott Porter (May 12 2021 at 18:56):Gaëtan Gilbert said:
I don't know what you mean by "nothing"
My bad, I meant that I did not see any indices pushed onto that environment.
Var is correct, I don't know why you expect Rel
I think I expected a Rel because I want to use the goal to call Proof.run_tactic again with the proper goal and context.
Gaëtan Gilbert (May 12 2021 at 19:13):My bad, I meant that I did not see any indices pushed onto that environment.
context variables are in the named_context part of the env
I think I expected a Rel because I want to use the goal to call Proof.run_tactic again with the proper goal and context.
I don't see how the 2 parts of this sentence are connected
Last updated: Jun 09 2023 at 07:01 UTC