Refactor Data.Vec.Properties : Add toList-injective and new lemmas
#2733
Conversation
While I happen to like that, this goes specifically against the stdlib naming convention which states that it should be
It has been an (unwritten!) convention to not use tactics in fairly low-level parts of the library, as we don't want those parts of the library to depend on the |
There was a problem hiding this comment.
Generally the lemmas look good, but I agree with @JacquesCarette point about the use of tactics.
| → reverse (xs ++ ys) ≈[ +-comm m n ] reverse ys ++ reverse xs | ||
| reverse-++-eqFree {m = m} {n = n} xs ys = | ||
| toList-injective (+-comm m n) (reverse (xs ++ ys)) (reverse ys ++ reverse xs) $ | ||
| begin |
There was a problem hiding this comment.
Is this really a cleaner proof? To my eyes it looks longer and more complicated?
There was a problem hiding this comment.
From my perspective, the advantages of this version are:
• It uses equational reasoning instead of induction
• It relies on existing properties from the List module
• It avoids the use of brackets from cast reasoning, which I personally find harder to follow
But if it's not what we want to take, please let me know!
| reverse (map f xs) ++ map f ys ≡⟨ unfold-ʳ++ (map f xs) (map f ys) ⟨ | ||
| map f xs ʳ++ map f ys ∎ | ||
| where open ≡-Reasoning | ||
|
|
||
| ∷-ʳ++-eqFree : ∀ a (xs : Vec A m) {ys : Vec A n} → let eq = sym (+-suc m n) in | ||
| cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys) | ||
| ∷-ʳ++-eqFree a xs {ys} = begin |
There was a problem hiding this comment.
This lemma seems to have been deleted without replacement?
There was a problem hiding this comment.
This lemma was previously used in the proof of ʳ++-ʳ++-eqFree, but since we now use the corresponding property directly from the List module, this lemma has become redundant ʳ++-ʳ++-eqFree is strictly stronger:
∷-ʳ++-eqFree a xs {ys} = ʳ++-ʳ++-eqFree (a ∷ []) {ys = xs} {zs = ys}
Should we keep it anyway ?
Replace
Data.List.Base as ListandData.List.Properties as Listwith shorterLaliases throughout the module for better readable proofAdd new utility lemma
toList-injectivethat proves vector equality from list equality using heterogeneous equalityAdd new equation-free lemmas that leverage
toList-injectivefor cleaner proofs:fromList-reverse: provesfromList (L.reverse xs) ≈[ L.length-reverse xs ] reverse (fromList xs)++-ʳ++-eqFree: proves associativity-like property for reverse-append without explicit equation parameterʳ++-ʳ++-eqFree: proves composition property for reverse-append operationsUpdate all
List.references toL.in function types and implementationsImport
Tactic.Congmodule to support thecong!tactic used in several proofsThis change improves code readability and adds a fundamental lemma for reasoning about vector equality via list conversion, which is used in several proofs throughout the module.