Fix simp regressions in ModalCompanion/Basic after deps update#2
Merged
Conversation
Version bump broke three proofs that relied on simp computing
`2 * (n + 1)` and `Finset.filterMap` over a singleton:
- `negRepeat_succ_rw`: factor out `negRepeat_neg` and rewrite the
multiplication explicitly before unfolding `negRepeat`.
- `notForces_double_negRepeat`: rewrite `2 * (n + 1)` to `2 * n + 1 + 1`
so `simp [negRepeat]` can unfold the two negations.
- `modal_companion_VFSer`: add `star_singleton_dni` proving
`{∼∼⊤}.star = {∼□∼□⊤}` via `ext`, and rewrite with it (plus
`Finset.singleton_union`) instead of unfolding `Axioms.star`.
Co-Authored-By: Claude Opus 4.8 <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.
依存パッケージの更新により
ModalCompanion/Basic.leanの3つの証明が壊れていたので修正した。いずれもsimpが2 * (n + 1)の計算や singleton 上のFinset.filterMapを畳めなくなったことが原因。変更点
negRepeat_succ_rw: 補題negRepeat_negを切り出し、negRepeatを展開する前に乗算を明示的に書き換え。notForces_double_negRepeat:2 * (n + 1)を2 * n + 1 + 1に書き換えてsimp [negRepeat]が2つの否定を展開できるようにした。modal_companion_VFSer:{∼∼⊤}.star = {∼□∼□⊤}をextで示す補題star_singleton_dniを追加し、Axioms.starを展開する代わりに（Finset.singleton_unionと併せて）それで書き換えるようにした。lake buildはエラー・警告なしで通過。🤖 Generated with Claude Code