feat: add weakest precondition#393
Draft
ayhon wants to merge 35 commits into
Draft
Conversation
ayhon
force-pushed
the
fele/feat/add-weakestpre
branch
from
85bda17 to
bfbe200
Compare
3 tasks
ayhon
force-pushed
the
fele/feat/add-weakestpre
branch
from
bfbe200 to
04858f5
Compare
3 tasks
lihaokun
added a commit
to lihaokun/iris-lean
that referenced
this pull request
May 14, 2026
按 Coq adequacy.v 严格 1:1 对齐：补 5 个 local lemma 缺失的 £ premise—— 之前漏看 Coq wp_step / wptp_step / wptp_preservation / wptp_postconditions / wptp_progress 都各自带一个 `£ (S num_laters_per_step ns)` 或 `£ (steps_sum num_laters_per_step ns n)` 作为 hypothesis（用于消耗 later credits 跨过 step_fupd 链）。 - wp_step: 加 `£ (iG.num_laters_per_step ns + 1) -∗` - wptp_step: 同 - wptp_preservation: 加 `£ (steps_sum iG.num_laters_per_step ns n) -∗` - wptp_postconditions: 同 - wptp_progress: 同 - wp_not_stuck: 无 £（Coq 也无），不变 注：当前 fork stage/1 的 `wp_pre` 也缺 £ premise（原 commit b884d99 翻译时 漏看 Coq line 74）。本 PR 暂不改 wp_pre——adequacy 用 `wp` 而非 `wp_pre`， 签名层独立；rebase 到 ayhon leanprover-community#393（其 wp.pre 已正确含 £）后两端自然一致。 `£` 通过 `Iris.Instances.Lib.LaterCredits` 的 `notation:max "£ " i:40 => lc i` （line 60）可见——已被 `Iris.Instances.Lib.FUpd` 间接 import 进来，无需新加 import。 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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
1 participant
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