Background
PR #55 closed the build-oracle cascade (closes #49) but introduced 3 documented admits with explicit model-gap notes. This is the smallest of the three to close.
Admit
proofs/coq/filesystem_composition.v:611 — Example mkdir_two_dirs_reversible
Closure path
The example as stated:
apply_sequence (reverse_sequence [OpMkdir p1; OpMkdir p2]) (apply_sequence [OpMkdir p1; OpMkdir p2] fs) = fs
reverses with non-LIFO rmdir p1; rmdir p2 order — the LIFO order is rmdir p2; rmdir p1. The general two_op_sequence_reversible lemma can only discharge the LIFO case.
Restate as LIFO — change the example to take the sequence [OpMkdir p2; OpMkdir p1] so the reverse [OpRmdir p1; OpRmdir p2] matches. Trivial restatement; the underlying theorem is true for LIFO.
OR: prove a new reverse_sequence_definition lemma showing reverse_sequence [op1; op2] = [reverse_op op2; reverse_op op1] and chase through.
Refs
🤖 Filed from PR #55 closure
Background
PR #55 closed the build-oracle cascade (closes #49) but introduced 3 documented admits with explicit model-gap notes. This is the smallest of the three to close.
Admit
proofs/coq/filesystem_composition.v:611—Example mkdir_two_dirs_reversibleClosure path
The example as stated:
reverses with non-LIFO
rmdir p1; rmdir p2order — the LIFO order isrmdir p2; rmdir p1. The generaltwo_op_sequence_reversiblelemma can only discharge the LIFO case.Restate as LIFO — change the example to take the sequence
[OpMkdir p2; OpMkdir p1]so the reverse[OpRmdir p1; OpRmdir p2]matches. Trivial restatement; the underlying theorem is true for LIFO.OR: prove a new
reverse_sequence_definitionlemma showingreverse_sequence [op1; op2] = [reverse_op op2; reverse_op op1]and chase through.Refs
proofs/coq/filesystem_composition.v:611🤖 Filed from PR #55 closure