Sync upstream leanprover-community/iris-lean and bump to Lean 4.28.0#162
Closed
quangvdao wants to merge 54 commits intoleanprover-community:masterfrom
Closed
Sync upstream leanprover-community/iris-lean and bump to Lean 4.28.0#162quangvdao wants to merge 54 commits intoleanprover-community:masterfrom
quangvdao wants to merge 54 commits intoleanprover-community:masterfrom
Conversation
…into update_lean
chore: mathlib dependency + workflows
* add bluebell paper * update gitignore
* add bluebell paper * update gitignore * new files * add lemmas * more progress * more progress * splitting up the paper into sections in separate files * split out appendices * minor * finish extracting sections from paper * further split subsections * stuff * update gitignore * more progress * more independent product * progress * finish porting, still has errors (instance diamonds) * error-free at last * add check-import workflow * add import, fix wp def
Pr summary workflow
* Prove wp_conseq theorem This proves the monotonicity property for weakest preconditions: if postcondition Q entails Q', then wp t Q entails wp t Q'. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> * Clean up wp_conseq proof - Omit unused MeasurableSpace section variable - Combine intro tactics per linter suggestion 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> --------- Co-authored-by: Claude <noreply@anthropic.com>
* Prove wp_frame theorem The frame rule for weakest preconditions: P ∗ (wp t Q) ⊢ (wp t (sep P Q)). The key insight is to use the frame resource `p` as part of the extended frame `p • c` when applying the WP hypothesis, then use CMRA associativity and commutativity to show the result satisfies the postcondition. Also adds reusable CMRA lemmas `op_left_comm` and `op_right_comm` for swapping the first two elements in a triple product. Closes #201 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> * Remove docstrings from op_left_comm and op_right_comm 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> * Simplify op_right_comm by moving after op_left_eqv By reordering, we can use comm.op_l to directly transform (x • y) • z to (y • x) • z, reducing the proof from 5 steps to 3. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> * Add comment explaining IsTotal assumption in wp_frame 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> --------- Co-authored-by: Claude <noreply@anthropic.com>
Use mathlib's measurableSet_bot_iff which states the same result. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude <noreply@anthropic.com>
- bot_sum: Show that (⊥ : MeasurableSpace).sum m = m by proving MeasurableSet[⊥] ∪ MeasurableSet[m] = MeasurableSet[m] and using generateFrom_measurableSet from mathlib. - sum_bot: Follows from bot_sum via sum_comm. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude <noreply@anthropic.com>
… (#252) - Prove Measure.IndependentProduct.symm by transporting the measure along MeasurableSpace.sum_comm and using Set.inter_comm + mul_comm - Prove MeasureSpace.indepProduct_isSome_comm using symm to show existence of independent product is symmetric 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude <noreply@anthropic.com>
🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude <noreply@anthropic.com>
* Add UCMRA instance for resource algebra using PermissionRat - Add cmraFunUCMRA and ucmraFun instances for function spaces with UCMRA components - Add compatiblePermRat predicate for paper-style rational permissions - Define PSpPmRat structure pairing PSp with PermissionRat - Add OFE, CMRA, and UCMRA instances for PSpPmRat - Define IndexedPSpPmRat with UCMRA instance - Update WeakestPre.lean to use IndexedPSpPmRat This enables proving wp_frame without the IsTotal workaround, as the resource algebra now has a unit element (zero permissions paired with trivial probability space). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> * Fill in sorrys in PSpPm.lean using insensitive lemmas - Add MeasurableSpace.insensitive_bot lemma: trivial σ-algebra is insensitive to any set - Fix op_closed proofs when indepProduct returns none (result is ⊤, always compatible) - Fix liftProb compatibility using insensitive_empty (full permission → empty set) - Fix compatiblePermRat_unit_compat using insensitive_bot - Fix op compatibility using CompatibleRel.op_closed - Fix extend using componentwise extend and dist_closed 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> * Fill sorrys in Probability.lean for insensitivity lemmas Prove 4 of 5 sorrys: - insensitive_anti: antitonicity in the set argument - insensitive_sum_inter: closure under MeasurableSpace.sum (uses π-λ theorem) - compatiblePerm_indepProduct: DFrac compatibility preserved under indepProduct - compatiblePermRat_indepProduct: PermissionRat compatibility preserved Added helper lemmas: - DFrac.op_eq_discard_iff: x • y = discard ↔ both are discard - NNRat.add_eq_zero_iff: a + b = 0 ↔ both are 0 The remaining sorry (indepMul_assoc) is blocked by ProbabilitySpace.indepProduct_assoc in IndepProduct.lean which requires uniqueness proofs not yet available. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com> * removed unused simp lemmas * cleanup * removed unused simp lemmas * fix wp frame --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: Quang Dao <qvd@andrew.cmu.edu>
This commit ports Logic/Ownership.lean from IndexedPSpPm to IndexedPSpPmRat. The latter has the unit element. The port started in #251 in WeakestPre.lean. This commit is continuation of the transition. The code changes were generated with Sonnet-4.5
Generated by Sonnet-4.5
Found by Sonnet-4.5
…259) * review only on request * fix: replace old PR summary workflow and remove scripts
Port Ownership.lean and JointCondition.lean to IndexedPSpPmRat
Prove indepMul_assoc
Proof of sep_of_and
Added a note about active development status and stability of src/Bluebell.
* Prove sep_of_and_assertTrue using CMRA associativity and upward closure 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com> * Remove warnings * Remove a too obvious comment --------- Co-authored-by: Claude Sonnet 4.5 <noreply@anthropic.com>
- Remove unnecessary `by exact` wrappers in IsCoupling.map and IsCoupling.symm - Simplify Lift.graph proof using grind tactic - No behavioral changes, purely syntactic improvements Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
… subset_singleton_iff Reduce verbosity in Coupling.lean by: eliminating intermediate `have` bindings for composition equalities (using inline `show ... from rfl`), leveraging `Set.Nonempty.subset_singleton_iff` for support equality proofs, collapsing case splits with `by_cases`, and inlining support membership witnesses. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace `by ext ⟨a, b⟩; rfl` with just `rfl` in SPMF.IsCoupling.map and SPMF.IsCoupling.symm. Lean's definitional equality handles these function compositions directly without explicit extensionality. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
proofs for probabilitytheory/coupling
Merge upstream master (38 commits) bringing: Auth CMRA, HeapView, View CMRA, internal fixpoints, coinduction, proof mode improvements (imod, imodintro, ihave, ispecialize), IProp instances, GenMap refactor, and Lean 4.28.0 toolchain. Keep mathlib dependency (required by Bluebell) and bump to v4.28.0. Fix DFrac name resolution in Permission.lean and Probability.lean (DFrac_CMRA/op -> CMRA.op/DFrac.op) for compatibility with Lean 4.28. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
|
Opened against wrong repo by mistake, re-creating on Verified-zkEVM/iris-lean. |
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.
Summary
leanprover-community/iris-lean, making this fork strictly ahead (54 ahead, 0 behind)DFrac_CMRA/op→CMRA.op/DFrac.op) inPermission.leanandProbability.leanUpstream features brought in
imod,imodintro,ihave,ispecializeimprovements,ProofModeMmonad,SynthInstanceBuild status
sorrys in incomplete Bluebell proofs (unchanged)Test plan
lake buildsucceeds for all default targets (Iris, Bluebell, IrisTest)lake build IrisTestpassessorrys introducedMade with Cursor