feat: iloeb

[ayhon]

Description

Implements the iLöb tactic.

Addresses #361

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

[MackieLoeffel]

This function does not follow the general pattern how proofmode tactics are written. Instead of directly manipulating MVarIds and IrisGoals, proof mode tactics take a Hyps and a goal as an argument and produce a new Hyps and goal as the result. Each proofmode tactic only has a single MVarId.assign call. You can look at the other tactics, e.g. at ispecialize or iintro for how tactics are written. This should also make the functions ProofModeM.getMainGoal and similar unnecessary. If you have questions for how to rewrite this, let me know.

[ayhon]

I have indeed found this pattern in the code, but I wasn't sure how to best compose tactics with this interface. In particular, I have understood that Hyps |- goal usually corresponds to the main target, and that we return the assignment for this main target. However, I don't really see how this API can be used to compose different tactics. In the end, once I am done executing iRevertCore I need to continue the proof under the new generated Hyps' |- goal', but to retrieve it I need to use either a ProofModeM.getMainGoal, or a continuation, which seems to be the method preferred by iModIntros. Do you suggest I rewrite this in terms of continuations, or am I missing something?

[MackieLoeffel]

You can compose the tactics by just calling the different ...Core functions (though sometimes they do not have the Core postfix, naming is a bit inconsistent). See for example here where iintros calls icases or here where icases calls iclear. Note that none of these functions need something like getMainGoal. The problem in this case is that the iRevertCore function that this PR adds also does not follow the right style and thus it is tricky to call.
If you want, I can sketch the iRevertCore function with the right signature.

[ayhon]

But for some of these functions, like iIntroCore or iRevertCore, I would need to be able to get the context after the operation has finished. In these cases the goal is always the same, but hyps does change at each operation, so I need to retrieve it somehow. That's what I was using getMainGoal for.

I see how I could get around this by doing what iModIntro is doing, asking for a continuation to run on the new hyps-goal pair, which is what I meant by "rewrite this in terms of continuations". The other way would be to change the signature of these functions to also give me access to the resulting transformed hypothesis, such as iSpecializeCore, but I'm not a big fan of this way.

I have started work on rewriting my solution in the continuation style. For this, the signature of iRevertCore would look something like this:

abbrev ProofModeTactic : Type _ := ∀ {u : Level}{prop: Q(Type $u)}{bi : Q(BI $prop)}{e : Q($prop)}
  (hyps : Hyps bi e)(goal: Q($prop)), ProofModeM Q($e ⊢ $goal)

def ProofModeM.revertingTelescope
  (hs : List RevertTarget)
  (k : ProofModeTactic) : ProofModeTactic := -- ...
-- `k` is run on the generalized environment.

Is something like this what you had in mind?

[MackieLoeffel]

Yes, this is roughly what I had in mind, but I am not sure if you actually need to pass a continuation in this case. Instead, it might be possible to just return the new hyps and goal. See for example iSpecializeCore, which works without a continuation. (The signature will be slightly different in your case since iRevertCore needs to return a new goal, not just change the Hyps.)

(Though thinking about this again, maybe you need a continuation to remove the fvars from the context for goals created in the continuation? Not sure about this.)

I would also not introduce an abstraction like ProofModeTactic at this point, but follow the style of the other functions that take a continuation like iModIntro or iIntros. Note that different proof mode functions have different signatures and not all tactics use continuation passing style. Having such an abstraction can be discussed in a separate issue.

[ayhon]

I have addressed the changes you mentioned. It took me more time than I would have liked since I had to debug some silly issues, but I'm quite satisfied with the final result. Lmk what you think of it and if it was closer to what you were expecting

[MackieLoeffel]

Great! I think the changed version looks very good! Thanks for working on this. I have minor stylistic comments, but it is probably the easiest if I make a pass over the code and directly apply them. I hope to find time for this in the next week.

[MackieLoeffel]

Here are some small points I noticed when looking over this. You can fix this or I can take care of it when I make my pass.

[MackieLoeffel]

The k does not need to take u, prop, and bi as arguments (also applies to other places).

[ayhon]

Actually, because of iModIntroCore, they might have to generalize over at least prop. iIntroCore specifically needs it to compile, the only one that maybe gets away with sharing the same u prop and bi is iRevertCore. However, u is for sure shared everywhere, and I would expect it to not really have to change.

[MackieLoeffel]

Usually we use elab instead of syntax + elab_rule. Is there a specific reason to use syntax + elab_rule here?

[ayhon]

I was just running into issues with the definition, and I find it easier to debug those when separating parsing and elaboration. Probably now those two can be merged, I simply forgot to test them

[ayhon]

Ok, the issue I was having is matching under the ? and *, I'm not sure how to do that in the elab syntax

[ayhon]

Addressed most review comments. Left a couple open for further comment.

I can't reproduce the CI build failure locally (with all other git changes staged)

EDIT: I'm guessing they're due to warnings?