feat: add weakest precondition#393
Merged
Kaptch merged 79 commits intoMay 21, 2026
Merged
Conversation
Collaborator
|
A general comment: please do not state theorems as functions unless you have a good reason to. It's better to give names to all hypotheses so it is easier to cleanup later (implicits, named arguments, etc.) |
Collaborator
|
Also: no universe names unless you have a really good reason. |
markusdemedeiros
approved these changes
May 20, 2026
Collaborator
|
Awesome, this will be great to have in. I looked over the BI code and it looks good enough to me. |
Collaborator
MackieLoeffel
left a comment
MackieLoeffel
left a comment
There was a problem hiding this comment.
This PR looks really great! I had some minor thoughts when looking over it (but none of this should be blocking merging this. (I hope that I will have time to look into the printing problem with iloeb at some point, but not sure when that will exactly be.)
Collaborator
Hi Michael, thanks for the tip with icases <-, H>, that's exactly what I wanted! Please take a look at https://github.com/leanprover-community/iris-lean/pull/393/changes#diff-6e68887200b797a6df93c0284434bf155c23f7c61bea9d8f8452950382bfb2fcR72 |
lihaokun
added a commit
to lihaokun/iris-lean
that referenced
this pull request
May 21, 2026
…kestpre interface
Lean 4 port of `iris/program_logic/adequacy.v`, adapted to the
`IrisGS_gen` / `wp.pre` / `WP _ @ s ; E {{ Φ }}` interface from PR leanprover-community#393.
Proven in this branch (5 lemmas + 2 theorems):
- `wp_step`, `wptp_step`, `wp_not_stuck`
- `wptp_preservation` (refl case)
- `adequate_alt`, `adequate_tp_safe`
Remaining sorries:
- `wptp_preservation` cons (skeleton + ~40 lines of working IPM; blocked
at `imod Hbody` — goal is step_fupdN, not fupd outermost)
- `wptp_postconditions`, `wptp_progress` (plain sorry, follow same pattern
as `wptp_preservation`)
- `wp_progress_gen`, `wp_strong_adequacy_gen`, `wp_adequacy_gen`,
`wp_invariance_gen` (4 meta-level theorems with `_hwp : True` placeholders;
unblocked once `InvGpreS`-style existential is finalized)
Helper `step_fupdN_compose` proves `(|=...=>^[a] P) ⊢ (P -∗ |=...=>^[b] Q) -∗
|=...=>^[a+b] Q` (`step_fupdN_wand` + `Nat.repeat_add`).
lihaokun
added a commit
to lihaokun/iris-lean
that referenced
this pull request
May 21, 2026
…kestpre interface
Lean 4 port of `iris/program_logic/adequacy.v`, adapted to the
`IrisGS_gen` / `wp.pre` / `WP _ @ s ; E {{ Φ }}` interface from PR leanprover-community#393.
Proven in this branch (5 lemmas + 2 theorems):
- `wp_step`, `wptp_step`, `wp_not_stuck`
- `wptp_preservation` (refl case)
- `adequate_alt`, `adequate_tp_safe`
Remaining sorries:
- `wptp_preservation` cons (skeleton + ~40 lines of working IPM; blocked
at `imod Hbody` — goal is step_fupdN, not fupd outermost)
- `wptp_postconditions`, `wptp_progress` (plain sorry, follow same pattern
as `wptp_preservation`)
- `wp_progress_gen`, `wp_strong_adequacy_gen`, `wp_adequacy_gen`,
`wp_invariance_gen` (4 meta-level theorems with `_hwp : True` placeholders;
unblocked once `InvGpreS`-style existential is finalized)
Helper `step_fupdN_compose` proves `(|=...=>^[a] P) ⊢ (P -∗ |=...=>^[b] Q) -∗
|=...=>^[a+b] Q` (`step_fupdN_wand` + `Nat.repeat_add`).
lihaokun
added a commit
to lihaokun/iris-lean
that referenced
this pull request
May 21, 2026
`wp_invariance_gen`: full structural proof using `adequate_alt` + `wp_strong_adequacy_gen` (oracle) + `erasedStep_nSteps` + per-element bigSepL2 handling. Internal sorry at the `bridge` step: our Lean signature has `iG.stateInterp σ2 0 [] (t2.length - 1)` with literal `ns = 0`, while `wp_strong_adequacy_gen` yields `ns = n` from the NSteps count. Coq absorbs this via `(λ σ _ _ _, stateI σ)` in the user- constructed `irisGS_gen`; the Lean PR leanprover-community#393 interface receives iG externally, so the `ns` parameter is literal `0` in the user signature. `stateInterp_mono` only goes `ns → ns+1` (not downward), so we cannot bridge `n → 0`. Fix path: change wp_invariance_gen's `_Hwp` signature to take a `stateI : State → IProp GF` (without ns/obs/nt) and construct `iG.stateInterp σ _ _ _ = stateI σ` via a custom IrisGS_gen instance. Deferred. Other meta proofs (wp_strong_adequacy_gen, wp_progress_gen, wp_adequacy_gen): agents either still running or hit fromOptionVal/match-form ispecialize blockers; left as plain `sorry`.
Collaborator
|
I've looked into this and your fix seems like the best option. I added some comments and a test for this behavior. |
lihaokun
added a commit
to lihaokun/iris-lean
that referenced
this pull request
May 22, 2026
…kestpre interface
Lean 4 port of `iris/program_logic/adequacy.v`, adapted to the
`IrisGS_gen` / `wp.pre` / `WP _ @ s ; E {{ Φ }}` interface from PR leanprover-community#393.
Proven in this branch (5 lemmas + 2 theorems):
- `wp_step`, `wptp_step`, `wp_not_stuck`
- `wptp_preservation` (refl case)
- `adequate_alt`, `adequate_tp_safe`
Remaining sorries:
- `wptp_preservation` cons (skeleton + ~40 lines of working IPM; blocked
at `imod Hbody` — goal is step_fupdN, not fupd outermost)
- `wptp_postconditions`, `wptp_progress` (plain sorry, follow same pattern
as `wptp_preservation`)
- `wp_progress_gen`, `wp_strong_adequacy_gen`, `wp_adequacy_gen`,
`wp_invariance_gen` (4 meta-level theorems with `_hwp : True` placeholders;
unblocked once `InvGpreS`-style existential is finalized)
Helper `step_fupdN_compose` proves `(|=...=>^[a] P) ⊢ (P -∗ |=...=>^[b] Q) -∗
|=...=>^[a+b] Q` (`step_fupdN_wand` + `Nat.repeat_add`).
lihaokun
added a commit
to lihaokun/iris-lean
that referenced
this pull request
May 22, 2026
`wp_invariance_gen`: full structural proof using `adequate_alt` + `wp_strong_adequacy_gen` (oracle) + `erasedStep_nSteps` + per-element bigSepL2 handling. Internal sorry at the `bridge` step: our Lean signature has `iG.stateInterp σ2 0 [] (t2.length - 1)` with literal `ns = 0`, while `wp_strong_adequacy_gen` yields `ns = n` from the NSteps count. Coq absorbs this via `(λ σ _ _ _, stateI σ)` in the user- constructed `irisGS_gen`; the Lean PR leanprover-community#393 interface receives iG externally, so the `ns` parameter is literal `0` in the user signature. `stateInterp_mono` only goes `ns → ns+1` (not downward), so we cannot bridge `n → 0`. Fix path: change wp_invariance_gen's `_Hwp` signature to take a `stateI : State → IProp GF` (without ns/obs/nt) and construct `iG.stateInterp σ _ _ _ = stateI σ` via a custom IrisGS_gen instance. Deferred. Other meta proofs (wp_strong_adequacy_gen, wp_progress_gen, wp_adequacy_gen): agents either still running or hit fromOptionVal/match-form ispecialize blockers; left as plain `sorry`.
ayhon
added a commit
to ayhon/iris-lean
that referenced
this pull request
May 22, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Porting of the weakest precondition definitions (
program_logic/weakestpre.v) and notation (bi/weakestpre.v).Implements #253.
Checklist
PORTING.mdas appropriateauthorssection of any appropriate files