feat: irevert tactic#74
Conversation
MackieLoeffel
left a comment
MackieLoeffel
left a comment
There was a problem hiding this comment.
I looked over the MR and noticed some minor points.
| λ x => h.trans (forall_elim x) | ||
|
|
||
| theorem pure_revert [BI PROP] {P Q : PROP} {φ : Prop} | ||
| (h : P ⊢ ⌜φ⌝ -∗ Q) : φ → P ⊢ Q := |
There was a problem hiding this comment.
This should use the MakeAffinely ⌜ φ ⌝ P to add the <affine> modality in front of ⌜ φ ⌝ for logics that require it. Otherwise, irevert can make the goal unprovable. See
https://gitlab.mpi-sws.org/iris/iris/-/blob/306d8d024f9d6522c0e733fd7eb27b0af676d4ca/iris/proofmode/coq_tactics.v
| end intro | ||
|
|
||
| -- revert | ||
| namespace revert |
There was a problem hiding this comment.
It would also be good to have tests for the failing cases:
- What happens when the name is not used?
- What happens when a pure hypothesis is used in another hypothesis?
For the second point: When I try the following test,
theorem fail [BI PROP] (Φ : Bool → PROP) : ⊢ ∀ x, <affine> ⌜x = true⌝ -∗ Φ x -∗ Φ x := by
iintro x %_ H
irevert xsomething very weird happens:
Goals (1)
PROP : Type u_1
inst : BI PROP
Φ : Bool → PROP
⊢
∗H : Φ _fvar.2200
⊢ «forall» fun x x_1 => Φ x
|
Sorry for letting this PR go stale. @MackieLoeffel or @lzy0505 could you look at this again, given the changes to the proofmode? |
|
Will do, I have it on my list to update this PR to master. |
3 participants
Implements the
ireverttactic, closes #69.