What do we need to be able to compute reverse tactics application?

Miscellaneous
1

I was curious to know what (minimum) knowledge/information was necessary to reverse the application of a tactic.

Let’s say I only have a goal and the tactic application (perhaps atomic tactic) that lead that goal. What information do we need to be able to compute goals that could have lead to that result?

My guess is that we need all the imports (what I cal environment, not sure if that is the right terminology), resulting context and resulting goal. i.e.

parent_goal = ReverseCoq(child_goal, tactic_leading_to_child_goal, env, child_context)

is enough to compute the (possible) parents goals that lead to a specific child_goal?

I am alright with returning a list of possible goals (or more likely goals). I am aware that the problem might be ill-posed so I’m flexible with solutions.

But I guess the only thing that is more of a stricter requirement that any goal in the parent goals should always return the child_goal. i.e.

for any

g_parent \in parent_goal(s)

I do want

child_goal = Coq(g_parent, tactic_leading_to_child_goal, context_parent, env)

That should be satisfied/returned.

2

It’s impossible
https://coq.github.io/doc/master/refman/proof-engine/tactics.html#coq:tacn.exfalso

3

not even with all the information that resulted in the current goal, context and environment?

Also, apologies for being dense but the link you pasted doesn’t make sense to me. What is it suppose to mean wrt the original question?

4

If the tactic is exfalso the original goal can be anything. The only way to tell what it was is if you already know it.

5

Apologies for being dense. Let me copy paste the tactic you are referring to:

Tactic exfalso
This tactic implements the “ex falso quodlibet” logical principle: an elimination of False is performed on the current goal, and the user is then required to prove that False is indeed provable in the current context. This tactic is a macro for elimtype False .

I have to admit I am not 100% sure what that means. I assume it changes the goal so that we need to prove false?

Goal(g1) --> Tactic(ex falso) --> Goal(False)

so you are saying that then Reverse(False, ex falso) = # any goal, is that correct?

I am trying to figure out if the case you are pointing out is an uninteresting edge case or not. If that’s the only case (or a collection of similar cases) can be ignored I am fine with that…

I am trying to understand a real case when that tactic is used so to understand the scenario your bringing up better.

6

Why are you interested in this question? Is there a practical value? This isn’t something users ask for.

@SkySkimmer has the right idea though he didn’t elaborate. Basically if you apply exfalso to any goal you get a new goal of False. If you want to go backwards from False, the previous goal could be absolutely anything–doesn’t seem promising. Even with another current goal, the previous goal may not be unique. And no easy way to find such a goal.

7

It’s not an academic edge case at all. It’s quite useful when you have an impossible goal, but a contradiction above the line. Changing the goal to “false” makes it easier to manipulate. Example:

you have something like H:~(1=1) above the line. Your goal is 1=2 or something impossible like that. exfalso; auto will solve the goal…it makes the goal false, then you can apply H; reflexivity. It’s definitely not an edge case.

AFAIK, what you want is not impossible. I bet there’s a way to reduce it to something impossible (halting problem etc)