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?
| fromList-reverse : (xs : List A) → (fromList (List.reverse xs)) ≈[ List.length-reverse xs ] reverse (fromList xs) | ||
| fromList-reverse xs = toList-injective (List.length-reverse xs) (fromList (List.reverse xs)) (reverse (fromList xs)) $ | ||
| begin | ||
| toList (fromList (List.reverse xs)) ≡⟨ toList∘fromList (List.reverse xs) ⟩ |
There was a problem hiding this comment.
Can we align the reasoning combinators?
| @@ -1304,8 +1339,8 @@ cast-fromList {xs = List.[]} {ys = List.[]} eq = refl | |||
| cast-fromList {xs = x List.∷ xs} {ys = y List.∷ ys} eq = | |||
| let x≡y , xs≡ys = List.∷-injective eq in begin | |||
| x ∷ cast (cong (pred ∘ List.length) eq) (fromList xs) ≡⟨ cong (_ ∷_) (cast-fromList xs≡ys) ⟩ | |||
| x ∷ fromList ys ≡⟨ cong (_∷ _) x≡y ⟩ | |||
| y ∷ fromList ys ∎ | |||
| x ∷ fromList ys ≡⟨ cong (_∷ _) x≡y ⟩ | |||
There was a problem hiding this comment.
The only change here seems to be to misalign the combinators?
| @@ -52,6 +53,19 @@ private | |||
| m n o : ℕ | |||
| ws xs ys zs : Vec A n | |||
|
|
|||
| ------------------------------------------------------------------------ | |||
| -- Properties to List | |||
There was a problem hiding this comment.
This should be Properties of toList
|
|
||
| toList-injective | ||
| : ∀ {m n} | ||
| → .(m=n : m ≡ n) |
There was a problem hiding this comment.
Can we follow the style guide about the placement of arrows on new lines?
Also can the name of this proof use ≡ instead of =?
| -- Properties to List | ||
|
|
||
| toList-injective | ||
| : ∀ {m n} |
There was a problem hiding this comment.
This are variables and therefore not needed.
| toList-reverse : ∀ (xs : Vec A n) → toList (reverse xs) ≡ List.reverse (toList xs) | ||
| toList-reverse [] = refl | ||
| toList-reverse (x ∷ xs) = begin | ||
| toList (reverse (x ∷ xs)) ≡⟨ cong toList (reverse-∷ x xs) ⟩ |
There was a problem hiding this comment.
Can we align the reasoning combinators? (you may need to install a monospaced font to make this easier)
| where open CastReasoning | ||
| toList-ʳ++ : ∀ (xs : Vec A m) {ys : Vec A n} → toList (xs ʳ++ ys) ≡ (toList xs) List.ʳ++ toList ys | ||
| toList-ʳ++ xs {ys} = begin | ||
| toList (xs ʳ++ ys) ≡⟨ cong toList (unfold-ʳ++ xs ys) ⟩ |
There was a problem hiding this comment.
Can we align the reasoning combinators? (for all new proofs in this file)
| 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?
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.