feat: iframe with existential quantifiers - #511

Merged

MackieLoeffel merged 31 commits into

leanprover-community:masterfrom

ISTA-PLV:iFrameExist

Jul 27, 2026

Commits on Jul 12, 2026

Create `frameExist` as a type class instance
alvinylt
committed
62e0fce
Perform parsing in `frameExist`
alvinylt
committed
303b7e7
Introduce `frame_exist`, use it in `frameExist`
alvinylt
committed
897e5d2
First functioning version of `frameExist`
alvinylt
committed
0f957ae
Port `frame_exist_no_instantiate`
alvinylt
committed
0645c20
Handle inner existential variables
alvinylt
committed
15ac9bc
Add one more test
alvinylt
committed
583f87a
Reuse the binder name
alvinylt
committed
bb40d71
Add an option `iris.frame.instantiateExists` for disabling existential quantifiers framing
alvinylt
committed
67047d5
Handle the flag `iris.frame.instantiateExists` in `frameExist`
alvinylt
committed
e5ec8ec
Implement `frameImp`, `frameWand` and `frameForall` as `SynthTactic`
alvinylt
committed
7eed7f8
Add `rocq_ignore` annotations
alvinylt
committed
6fbeb90
Update documentation
alvinylt
committed
c97962e
Update proof due to changes in `iframe`
alvinylt
committed
3c5f102
Bug fix: `frameImp`, `frameWand` and `frameForall` has lower priority
alvinylt
committed
e4e43c6
Minor refinements
alvinylt
committed
6bcee85
Port `FrameInstantiateExistDisabled` for `frameWp` (#400)
alvinylt
committed
0c58c91
Header update
alvinylt
committed
181b00f
Remove stale `rocq_ignore` entry (`FrameExistRequirements`)
alvinylt
committed
a7f55d8

Commits on Jul 23, 2026

Introduce `FrameInstantiateExistDisabled` as its own type class
alvinylt
committed
2fa1f0a
Restore the proofs for `Frame` instances
alvinylt
committed
440a4a7
Restore position of instance
alvinylt
committed
737c8d7
Merge remote-tracking branch 'upstream/master' into iFrameExist
alvinylt
committed
795c299
Update `AbstractLangCompleteness.lean`
alvinylt
committed
c6365b0
Remove unnecessary imports
alvinylt
committed
14d4bf4
Move `FrameInstantiateExistDisabled` to `Classes.lean`
alvinylt
committed
8dfca0a
Implement `solveGatherEvarsEq` and fix bug in `iframe`
alvinylt
committed
142a286
Add comments
alvinylt
committed
b9f5c05

Commits on Jul 27, 2026

Merge remote-tracking branch 'upstream/master' into iFrameExist
alvinylt
committed
9484478
simplify code
MackieLoeffel
committed
0f9968b
fix
MackieLoeffel
committed
6878531