This pull request adds a set of combinators for equational reasoning about vector equality of the form cast eq xs ≡ ys and a few properties demonstrating its application. In particular, the new combinators deal with the threading of index equality proofs, greatly reducing the boilerplate that manipulates casts to make writing equational proofs about vectors more or less feasible.
(Sorry for the piles of PR and the mess of the commit history. I promise this is the last one I have in hand. The first commit is the content of #2041 and #2045. After these two PRs get in, I'll rebase to remove the first commit. To see the code of this PR, please check https://github.com/agda/agda-stdlib/commit/f8971193dce2620cdabf4c7f1d8319c2aa8fb0ed.)
Index arithmetic is notably troublesome when it comes to proving vector properties (#942). Existing solutions include stating and proving cast-equality by induction, proving pointwise equality (#1668, #1621), or turning to heterogeneous equality with K. However, sometimes even an inductive proof can benefit from equational reasoning as seen in reverse-++, and that one really wants to convert back to propositional equality at the end to facilitate type casting. Therefore, the goal of this PR is to design a set of combinators that interoperates with _≡_ while reducing explicit index castings in the proofs to an tolerable level.
@JacquesCarette pointed me to @Taneb's nice PR on displayed categories and equational reasoning over some base equality in agda/agda-categories#382. It seems to me that the core combinators in this PR can be seen as a instance of displayed setoid, but I am not sure if I understand it correctly.
In this PR, the new combinators directly operate on equality of the form cast eq xs ≡ ys. Fortunately, this type of equality is 'reflexive', 'symmetric' and 'transitive', therefore cast eq xs ≡ ys admits the standard equational reasoning combinators. The combinators can hide casts in the terms from the user to reduce redundancy. Index equality is inferred from the proof in each step and automatically threaded throughout the process. In addition, since the underlying type is just cast eq xs ≡ ys, the combinators automatically work with _≡_.
Let xs ≈[ n≡m ] ys denote cast n≡m xs ≡ ys, the standard combinators are:
begin_ : ∀ .{m≡n} {xs : Vec A m} {ys} → xs ≈[ m≡n ] ys → cast m≡n xs ≡ ys
begin xs≈ys = xs≈ys
_∎ : ∀ xs → cast refl xs ≡ xs
_∎ xs = ≈-reflexive refl
step-≈ : ∀ .{m≡n} .{m≡o} (xs : Vec A m) {ys zs} →
(ys ≈[ trans (sym m≡n) m≡o ] zs) → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡o ] zs)
step-≈ xs ys≈zs xs≈ys = ≈-trans xs≈ys ys≈zs
syntax step-≈ xs ys≈zs xs≈ys = xs ≈⟨ xs≈ys ⟩ ys≈zsAs an example, the PR proves the property ∷-ʳ++ : cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys). The third step in the proof changes the index from (suc m) + n to m + suc n, so in principle the first two steps are implicitly wrapped in a cast. The other steps do not change the index, so they use the operator xs ≂⟨ xs≡ys ⟩ ys≈zs to inject ordinary propositional equality _≡_ into _≈[_]_.
{-
unfold-ʳ++ : xs ʳ++ ys ≡ reverse xs ++ ys
reverse-∷ : reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
∷ʳ-++ : cast eq ((xs ∷ʳ a) ++ ys) ≡ xs ++ (a ∷ ys)
-}
∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
∷-ʳ++ eq a xs {ys} = begin
(a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
(reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩
reverse xs ++ (a ∷ ys) ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩
xs ʳ++ (a ∷ ys) ∎Very often casts occur deep inside a term instead of at the outermost position. It then become necessary to cong over existing proofs for better reuse (or just to apply the induction hypothesis). Nonetheless, pushing casts into the term also takes one equational reasoning step, so the PR provides xs≈fys ≈cong[ f ] ys≈zs to push the cast inside and conging f, producing xs≈fzs.
For example, consider the proof of cast eq (reverse ((xs ∷ʳ a) ++ ys)) ≡ reverse ((xs ++ [ a ]) ++ ys) that re-uses unfold-∷ʳ from the standard library. In order to apply unfold-∷ʳ, the proof must first push cast into reverse and then push the inner cast into (_++ ys). Therefore we chain two ≈congs together:
{-
cast-++ˡ : cast ... (xs ++ ys) ≡ cast eq xs ++ ys
unfold-∷ʳ : cast eq (xs ∷ʳ x) ≡ xs ++ [ x ]
-}
example : ∀ .eq a xs ys → cast eq (reverse ((xs ∷ʳ a) ++ ys)) ≡ reverse ((xs ++ [ a ]) ++ ys)
example {m = m} {n} eq a xs ys = begin
reverse ((xs ∷ʳ a) ++ ys) ≈⟨ cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys)
≈cong[ reverse ] cast-++ˡ (+-comm 1 m) (xs ∷ʳ a)
≈cong[ (_++ ys) ] unfold-∷ʳ _ a xs ⟩
reverse ((xs ++ [ a ]) ++ ys) ∎To interoperate with _≡_, the PR includes two more operators for injecting _≡_ into _≈[_]_ and escaping _≈[_]_ back to _≡_. That is, the cast equational reasoning can stop at any point using xs ≃⟨ xs≈ys ⟩ ys≡zs and switch back to plain equational reasoning. However, from the proofs in this PR, xs ≂⟨ xs≡ys ⟩ ys≈zs is commonly used but xs ≃⟨ xs≈ys ⟩ ys≡zs isn't, assuming the availability of xs≈fys ≈cong[ f ] ys≈zs.
-- composition of the equality type on the right-hand side of _≈[_]_, or escaping to ordinary _≡_
step-≃ : ∀ xs → (ys ≡ zs) → (xs ≈[ m≡n ] ys) → (xs ≈[ m≡n ] zs)
step-≃ xs ys≡zs xs≈ys = ≈-trans xs≈ys (≈-reflexive ys≡zs)
syntax step-≃ xs ys≡zs xs≈ys = xs ≃⟨ xs≈ys ⟩ ys≡zs
-- composition of the equality type on the left-hand side of _≈[_]_
step-≂ : ∀ xs → (ys ≈[ m≡n ] zs) → (xs ≡ ys) → (xs ≈[ m≡n ] zs)
step-≂ xs ys≈zs xs≡ys = ≈-trans (≈-reflexive xs≡ys) ys≈zs
syntax step-≂ xs ys≈zs xs≡ys = xs ≂⟨ xs≡ys ⟩ ys≈zsIn principle, cast proofs can be written directly without using the combinators in this PR. Sadly, the chaining of the proofs of indices quickly become tedious to the degree of unmanageable. Here are two examples comparing proofs using the new combinators versus the proofs in #2045. It would be even annoying to prove fromList-reverse,
fromList-reverse : cast ... (fromList (List.reverse xs)) ≡ reverse (fromList xs)since the proof necessarily involves List equational reasoning that ended up changing the index at every step.
cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
cast-reverse {n = zero} eq [] = refl
-cast-reverse {n = suc n} eq (x ∷ xs) = begin
- cast eq (reverse (x ∷ xs)) ≡⟨ cong (cast eq) (reverse-∷ x xs) ⟩
- cast eq (reverse xs ∷ʳ x) ≡⟨ cast-∷ʳ eq x (reverse xs) ⟩
- (cast (cong pred eq) (reverse xs)) ∷ʳ x ≡⟨ cong (_∷ʳ x) (cast-reverse (cong pred eq) xs) ⟩
- (reverse (cast (cong pred eq) xs)) ∷ʳ x ≡˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩
- reverse (x ∷ cast (cong pred eq) xs) ≡⟨⟩
- reverse (cast eq (x ∷ xs)) ∎
+cast-reverse {n = suc n} eq (x ∷ xs) = begin′
+ reverse (x ∷ xs) ≂⟨ reverse-∷ x xs ⟩
+ reverse xs ∷ʳ x ≈⟨ cast-∷ʳ eq x (reverse xs)
+ ≈cong[ (_∷ʳ x) ] cast-reverse (cong pred eq) xs ⟩
+ reverse (cast _ xs) ∷ʳ x ≂˘⟨ reverse-∷ x (cast (cong pred eq) xs) ⟩
+ reverse (x ∷ cast _ xs) ≈⟨⟩
+ reverse (cast eq (x ∷ xs)) ∎′ reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++ {m = zero} {n = n} eq [] ys = begin
- cast _ (reverse ys) ≡˘⟨ cong (cast eq) (++-identityʳ (sym eq) (reverse ys)) ⟩
- cast _ (cast _ (reverse ys ++ [])) ≡⟨ cast-trans (sym eq) eq (reverse ys ++ []) ⟩
- cast _ (reverse ys ++ []) ≡⟨ cast-is-id (trans (sym eq) eq) (reverse ys ++ []) ⟩
- reverse ys ++ [] ≡⟨⟩
- reverse ys ++ reverse [] ∎
+reverse-++ {m = zero} {n = n} eq [] ys = ≈-sym (++-identityʳ (sym eq) (reverse ys))
-reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
- cast eq (reverse (x ∷ xs ++ ys)) ≡⟨ cong (cast eq) (reverse-∷ x (xs ++ ys)) ⟩
- cast eq (reverse (xs ++ ys) ∷ʳ x) ≡˘⟨ cast-trans eq₂ eq₁ (reverse (xs ++ ys) ∷ʳ x) ⟩
- (cast eq₁ ∘ cast eq₂) (reverse (xs ++ ys) ∷ʳ x) ≡⟨ cong (cast eq₁) (cast-∷ʳ _ x (reverse (xs ++ ys))) ⟩
- cast eq₁ ((cast eq₃ (reverse (xs ++ ys))) ∷ʳ x) ≡⟨ cong (cast eq₁) (cong (_∷ʳ x) (reverse-++ _ xs ys)) ⟩
- cast eq₁ ((reverse ys ++ reverse xs) ∷ʳ x) ≡⟨ ++-∷ʳ _ x (reverse ys) (reverse xs) ⟩
- reverse ys ++ (reverse xs ∷ʳ x) ≡˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
- reverse ys ++ (reverse (x ∷ xs)) ∎
- where
- eq₁ = sym (+-suc n m)
- eq₂ = cong suc (+-comm m n)
- eq₃ = cong pred eq₂
+reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin′
+ reverse (x ∷ xs ++ ys) ≂⟨ reverse-∷ x (xs ++ ys) ⟩
+ reverse (xs ++ ys) ∷ʳ x ≈⟨ cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys))
+ ≈cong[ (_∷ʳ x) ] reverse-++ _ xs ys ⟩
+ (reverse ys ++ reverse xs) ∷ʳ x ≈⟨ ++-∷ʳ (sym (+-suc n m)) x (reverse ys) (reverse xs) ⟩
+ reverse ys ++ (reverse xs ∷ʳ x) ≂˘⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟩
+ reverse ys ++ (reverse (x ∷ xs)) ∎′Here are some limitations I found while proving properties in this PR using the proposed combinators.
-
The combinators heavily expects other lemmas to be properly shaped in the form of
case eq xs ≡ ys. This is not surprising, but requires some sort of convention. -
The combinators don't help with more primitive lemmas that have to be proved directly using fold fusion. In other words, without the more fundamentals lemmas like
reverse-∷,unfold-ʳ++etc, the combinators probably can't prove anything. Thanks to @jamesmckinna for porting thereverselemmas for vectors! -
An equational reasoning step
xs ≈⟨ xs≈ys ⟩ ys≈zsobtains the underlyingeqofcastfrom the result type and from the proofxs≈ys. Therefore, in the middle of an equational proof, the underlyingeqwill become an unsolved metavariable.pf : cast eq xs ≡ ys pf = begin xs ≈⟨ xs≈zs ⟩ zs ≈⟨ {! !} ⟩ -- this step introduces an unsolved metavariable until it's filled in ys ∎