Added first part of Lab#22
Open
DumitruIlie wants to merge 9 commits into
Open
Conversation
Collaborator
Author
|
Also added optional lemmas. Last one was not the hardest (: |
alexoltean61
reviewed
May 7, 2026
Comment on lines
+30
to
+37
| induction r | ||
| · rename_i μ st'' h | ||
| simp only [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek1, | ||
| replaceMemStackAndIncrPC, stackPeek2, beq_iff_eq, gt_iff_lt] at h | ||
| by_cases pc_ok : μ.pc < μ.code.length | ||
| · simp only [pc_ok, ↓reduceDIte] at h | ||
| generalize m : μ.code[μ.pc] = c | ||
| cases c |
Owner
There was a problem hiding this comment.
Ohhh this looks like it was painful. See my comment here. When you have repetitive case analysis, aesop is generally your friend. The idea is to distribute as many of the simp lemmas (e.g., bind, Except.bind) before you perform the case analysis, not after.
| rw [←stp] | ||
| unfold isError | ||
| simp only | ||
| · rename_i st1 st2 sti st1i sti2 ih0 ih1 |
Owner
There was a problem hiding this comment.
If you do induction or cases, you can give explicit names to your hypotheses and avoid using rename_i. The keyword you're missing is with.
Suggested change
| · rename_i st1 st2 sti st1i sti2 ih0 ih1 | |
| induction r with | |
| | @step μ st'' stp => | |
| unfold isFinal at h | |
| simp only at h | |
| simp only [step, bind, Except.bind, fetchInstr, h, Nat.lt_irrefl, ↓reduceDIte] at stp | |
| rw [←stp] | |
| unfold isError | |
| simp only | |
| | @trans st1 st2 sti st1i sti2 ih0 ih1 => | |
| specialize ih0 h | |
| cases sti | |
| · exact isErrorLemma.elim sti2 | |
| · unfold isError at ih0 | |
| simp at ih0 |
Same goes for cases. There's an "at" symbol there (@) because you also provide names to the anonymous parameters of step and trans. If you don't need those names, just skip the "at".
Comment on lines
+228
to
+229
| lemma execTrans {μ μ'} (h : Reachable (.ok μ) (.ok μ')) : | ||
| ∃ k : ℕ, ∀ n : ℕ, execute (n + k) μ = execute n μ' := by |
alexoltean61
force-pushed
the
master
branch
3 times, most recently
from
c7c1340 to
0a51137
Compare
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
2 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.
No description provided.