Skip to content

Refactor Data.Vec.Properties : Add toList-injective and new lemmas #2733

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Refactor Data.Vec.Properties : Add toList-injective and new lemmas #2733

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
6fcf132
toList
jmougeot Jun 5, 2025
ab3633c
better proof
jmougeot Jun 9, 2025
6f4e8ef
update propreties
jmougeot Jun 9, 2025
adb5eb3
Revert changes to WithK.agda
jmougeot Jun 9, 2025
d4f5f59
update CHANGELOG
jmougeot Jun 9, 2025
2dcfd84
fixwhitespace
jmougeot Jun 9, 2025
aadc9cb
change L. to List.
jmougeot Jun 11, 2025
b0a934a
update 1
jmougeot Jun 16, 2025
fa4cd0c
fix-whitespace
jmougeot Jun 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -294,6 +294,17 @@ Additions to existing modules
LeftInverse (I ×ₛ A) (J ×ₛ B)
```

* In `Data.Vec.Properties`:
```agda
toList-injective : ∀ {m n} → .(m=n : m ≡ n) → (xs : Vec A m) (ys : Vec A n) →
toList xs ≡ toList ys → xs ≈[ m=n ] ys
fromList-reverse : (xs : List A) → (fromList (L.reverse xs)) ≈[ L.length-reverse xs ] reverse (fromList xs)
++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
ʳ++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
```

* In `Data.Vec.Relation.Binary.Pointwise.Inductive`:
```agda
zipWith-assoc : Associative _∼_ f → Associative (Pointwise _∼_) (zipWith {n = n} f)
Expand Down
145 changes: 89 additions & 56 deletions src/Data/Vec/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary.Decidable.Core
using (Dec; does; yes; _×-dec_; map′)
open import Relation.Nullary.Negation.Core using (contradiction)
open import Tactic.Cong using (cong!)
import Data.Nat.GeneralisedArithmetic as ℕ

private
Expand All @@ -52,6 +53,15 @@ private
m n o : ℕ
ws xs ys zs : Vec A n

------------------------------------------------------------------------
-- Properties of toList

toList-injective : .(m≡n : m ≡ n) → (xs : Vec A m) (ys : Vec A n) →
toList xs ≡ toList ys → xs ≈[ m≡n ] ys
toList-injective m≡n [] [] xs=ys = refl
toList-injective m≡n (x ∷ xs) (y ∷ ys) xs=ys =
cong₂ _∷_ (List.∷-injectiveˡ xs=ys) (toList-injective (cong pred m≡n) xs ys (List.∷-injectiveʳ xs=ys))

------------------------------------------------------------------------
-- Properties of propositional equality over vectors

Expand Down Expand Up @@ -1016,26 +1026,41 @@ map-reverse : ∀ (f : A → B) (xs : Vec A n) →
map f (reverse xs) ≡ reverse (map f xs)
map-reverse f [] = refl
map-reverse f (x ∷ xs) = begin
map f (reverse (x ∷ xs)) ≡⟨ cong (map f) (reverse-∷ x xs) ⟩
map f (reverse xs ∷ʳ x) ≡⟨ map-∷ʳ f x (reverse xs) ⟩
map f (reverse xs) ∷ʳ f x ≡⟨ cong (_∷ʳ f x) (map-reverse f xs ) ⟩
map f (reverse (x ∷ xs)) ≡⟨ cong (map f) (reverse-∷ x xs) ⟩
map f (reverse xs ∷ʳ x) ≡⟨ map-∷ʳ f x (reverse xs) ⟩
map f (reverse xs) ∷ʳ f x ≡⟨ cong (_∷ʳ f x) (map-reverse f xs ) ⟩
reverse (map f xs) ∷ʳ f x ≡⟨ reverse-∷ (f x) (map f xs) ⟨
reverse (f x ∷ map f xs) ≡⟨⟩
reverse (map f (x ∷ xs)) ∎
where open ≡-Reasoning

-- append and reverse
toList-∷ʳ : ∀ x (xs : Vec A n) → toList (xs ∷ʳ x) ≡ toList xs List.++ List.[ x ]
toList-∷ʳ x [] = refl
toList-∷ʳ x (y ∷ xs) = cong (y List.∷_) (toList-∷ʳ x xs)

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) ⟩
toList (reverse xs ∷ʳ x) ≡⟨ toList-∷ʳ x (reverse xs) ⟩
toList (reverse xs) List.++ List.[ x ] ≡⟨ cong (List._++ List.[ x ]) (toList-reverse xs) ⟩
List.reverse (toList xs) List.++ List.[ x ] ≡⟨ List.unfold-reverse x (toList xs) ⟨
List.reverse (toList (x ∷ xs)) ∎
where open ≡-Reasoning

reverse-++-eqFree : ∀ (xs : Vec A m) (ys : Vec A n) → let eq = +-comm m n in
cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
reverse-++-eqFree {m = zero} {n = n} [] ys = ≈-sym (++-identityʳ-eqFree (reverse ys))
reverse-++-eqFree {m = suc m} {n = n} (x ∷ xs) ys = begin
reverse (x ∷ xs ++ ys) ≂⟨ reverse-∷ x (xs ++ ys) ⟩
reverse (xs ++ ys) ∷ʳ x ≈⟨ ≈-cong′ (_∷ʳ x) (reverse-++-eqFree xs ys) ⟩
(reverse ys ++ reverse xs) ∷ʳ x ≈⟨ ++-∷ʳ-eqFree x (reverse ys) (reverse xs) ⟩
reverse ys ++ (reverse xs ∷ʳ x) ≂⟨ cong (reverse ys ++_) (reverse-∷ x xs) ⟨
reverse ys ++ (reverse (x ∷ xs)) ∎
where open CastReasoning
reverse-++-eqFree : ∀ (xs : Vec A m) (ys : Vec A n)
→ 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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this really a cleaner proof? To my eyes it looks longer and more complicated?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!

toList (reverse (xs ++ ys)) ≡⟨ toList-reverse ((xs ++ ys)) ⟩
List.reverse (toList (xs ++ ys)) ≡⟨ cong List.reverse (toList-++ xs ys) ⟩
List.reverse (toList xs List.++ toList ys) ≡⟨ List.reverse-++ (toList xs) (toList ys) ⟩
List.reverse (toList ys) List.++ List.reverse (toList xs) ≡⟨ cong₂ List._++_ (toList-reverse ys) (toList-reverse xs) ⟨
toList (reverse ys) List.++ toList (reverse xs) ≡⟨ toList-++ (reverse ys) (reverse xs) ⟨
toList (reverse ys ++ reverse xs) ∎
where open ≡-Reasoning

cast-reverse : ∀ .(eq : m ≡ n) → cast eq ∘ reverse {A = A} {n = m} ≗ reverse ∘ cast eq
cast-reverse _ _ = ≈-cong′ reverse refl
Expand All @@ -1061,53 +1086,57 @@ foldr-ʳ++ B f {e} xs = foldl-fusion (foldr B f e) refl (λ _ _ → refl) xs
map-ʳ++ : ∀ (f : A → B) (xs : Vec A m) →
map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
map-ʳ++ {ys = ys} f xs = begin
map f (xs ʳ++ ys) ≡⟨ cong (map f) (unfold-ʳ++ xs ys) ⟩
map f (reverse xs ++ ys) ≡⟨ map-++ f (reverse xs) ys ⟩
map f (reverse xs) ++ map f ys ≡⟨ cong (_++ map f ys) (map-reverse f xs) ⟩
map f (xs ʳ++ ys) ≡⟨ cong (map f) (unfold-ʳ++ xs ys) ⟩
map f (reverse xs ++ ys) ≡⟨ map-++ f (reverse xs) ys ⟩
map f (reverse xs) ++ map f ys ≡⟨ cong (_++ map f ys) (map-reverse f xs) ⟩
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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This lemma seems to have been deleted without replacement?

Copy link
Contributor Author

@jmougeot jmougeot Jun 16, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 ?

(a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩
reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩
(reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++-eqFree a (reverse xs) ⟩
reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨
xs ʳ++ (a ∷ ys) ∎
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) ⟩
toList (reverse xs ++ ys) ≡⟨ toList-++ ((reverse xs )) ys ⟩
toList (reverse xs) List.++ toList ys ≡⟨ cong (List._++ toList ys) (toList-reverse xs) ⟩
List.reverse (toList xs) List.++ toList ys ≡⟨ List.ʳ++-defn (toList xs) ⟨
toList xs List.ʳ++ toList ys ∎
where open ≡-Reasoning


++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs)
++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
((xs ++ ys) ʳ++ zs) ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩
reverse (xs ++ ys) ++ zs ≈⟨ ≈-cong′ (_++ zs) (reverse-++-eqFree xs ys) ⟩
(reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc-eqFree (reverse ys) (reverse xs) zs ⟩
reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨
reverse ys ++ (xs ʳ++ zs) ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨
ys ʳ++ (xs ʳ++ zs) ∎
where open CastReasoning
++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} =
toList-injective (m+n+o≡n+[m+o] m n o) ((xs ++ ys) ʳ++ zs) (ys ʳ++ (xs ʳ++ zs)) $
begin
toList ((xs ++ ys) ʳ++ zs) ≡⟨ toList-ʳ++ (xs ++ ys) ⟩
toList (xs ++ ys) List.ʳ++ toList zs ≡⟨ cong (List._ʳ++ toList zs) (toList-++ xs ys) ⟩
((toList xs) List.++ toList ys ) List.ʳ++ toList zs ≡⟨ List.++-ʳ++ (toList xs) ⟩
toList ys List.ʳ++ (toList xs List.ʳ++ toList zs) ≡⟨ cong (toList ys List.ʳ++_) (toList-ʳ++ xs) ⟨
toList ys List.ʳ++ toList (xs ʳ++ zs) ≡⟨ toList-ʳ++ ys ⟨
toList (ys ʳ++ (xs ʳ++ zs)) ∎
where open ≡-Reasoning

ʳ++-ʳ++-eqFree : ∀ (xs : Vec A m) {ys : Vec A n} {zs : Vec A o} → let eq = m+n+o≡n+[m+o] m n o in
cast eq ((xs ʳ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ++ zs)
ʳ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} = begin
(xs ʳ++ ys) ʳ++ zs ≂⟨ cong (_ʳ++ zs) (unfold-ʳ++ xs ys) ⟩
(reverse xs ++ ys) ʳ++ zs ≂⟨ unfold-ʳ++ (reverse xs ++ ys) zs ⟩
reverse (reverse xs ++ ys) ++ zs ≈⟨ ≈-cong′ (_++ zs) (reverse-++-eqFree (reverse xs) ys) ⟩
(reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩
(reverse ys ++ xs) ++ zs ≈⟨ ++-assoc-eqFree (reverse ys) xs zs ⟩
reverse ys ++ (xs ++ zs) ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨
ys ʳ++ (xs ++ zs) ∎
where open CastReasoning
ʳ++-ʳ++-eqFree {m = m} {n} {o} xs {ys} {zs} =
toList-injective (m+n+o≡n+[m+o] m n o) ((xs ʳ++ ys) ʳ++ zs) (ys ʳ++ (xs ++ zs)) $
begin
toList ((xs ʳ++ ys) ʳ++ zs) ≡⟨ toList-ʳ++ (xs ʳ++ ys) ⟩
toList (xs ʳ++ ys) List.ʳ++ toList zs ≡⟨ cong (List._ʳ++ toList zs) (toList-ʳ++ xs) ⟩
(toList xs List.ʳ++ toList ys) List.ʳ++ toList zs ≡⟨ List.ʳ++-ʳ++ (toList xs) ⟩
toList ys List.ʳ++ (toList xs List.++ toList zs) ≡⟨ cong (toList ys List.ʳ++_) (toList-++ xs zs) ⟨
toList ys List.ʳ++ (toList (xs ++ zs)) ≡⟨ toList-ʳ++ ys ⟨
toList (ys ʳ++ (xs ++ zs)) ∎
where open ≡-Reasoning

------------------------------------------------------------------------
-- sum
--sum

sum-++ : ∀ (xs : Vec ℕ m) → sum (xs ++ ys) ≡ sum xs + sum ys
sum-++ {_} [] = refl
sum-++ {ys = ys} (x ∷ xs) = begin
x + sum (xs ++ ys) ≡⟨ cong (x +_) (sum-++ xs) ⟩
x + sum (xs ++ ys) ≡⟨ cong (x +_) (sum-++ xs) ⟩
x + (sum xs + sum ys) ≡⟨ +-assoc x (sum xs) (sum ys) ⟨
sum (x ∷ xs) + sum ys ∎
where open ≡-Reasoning
Expand Down Expand Up @@ -1293,6 +1322,10 @@ toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
toList∘fromList List.[] = refl
toList∘fromList (x List.∷ xs) = cong (x List.∷_) (toList∘fromList xs)

fromList∘toList : ∀ (xs : Vec A n) → fromList (toList xs) ≈[ length-toList xs ] xs
fromList∘toList [] = refl
fromList∘toList (x ∷ xs) = cong (x ∷_) (fromList∘toList xs)

toList-cast : ∀ .(eq : m ≡ n) (xs : Vec A m) → toList (cast eq xs) ≡ toList xs
toList-cast {n = zero} eq [] = refl
toList-cast {n = suc _} eq (x ∷ xs) =
Expand All @@ -1318,17 +1351,16 @@ fromList-++ : ∀ (xs : List A) {ys : List A} →
fromList-++ List.[] {ys} = cast-is-id refl (fromList ys)
fromList-++ (x List.∷ xs) {ys} = cong (x ∷_) (fromList-++ xs)

fromList-reverse : (xs : List A) → cast (List.length-reverse xs) (fromList (List.reverse xs)) ≡ reverse (fromList xs)
fromList-reverse List.[] = refl
fromList-reverse (x List.∷ xs) = begin
fromList (List.reverse (x List.∷ xs)) ≈⟨ cast-fromList (List.ʳ++-defn xs) ⟩
fromList (List.reverse xs List.++ List.[ x ]) ≈⟨ fromList-++ (List.reverse xs) ⟩
fromList (List.reverse xs) ++ [ x ] ≈⟨ unfold-∷ʳ-eqFree x (fromList (List.reverse xs)) ⟨
fromList (List.reverse xs) ∷ʳ x ≈⟨ ≈-cong′ (_∷ʳ x) (fromList-reverse xs) ⟩
reverse (fromList xs) ∷ʳ x ≂⟨ reverse-∷ x (fromList xs) ⟨
reverse (x ∷ fromList xs) ≈⟨⟩
reverse (fromList (x List.∷ xs)) ∎
where open CastReasoning
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) ⟩
List.reverse xs ≡⟨ cong (λ x → List.reverse x) (toList∘fromList xs) ⟨
List.reverse (toList (fromList xs)) ≡⟨ toList-reverse (fromList xs) ⟨
toList (reverse (fromList xs)) ∎
where open ≡-Reasoning

------------------------------------------------------------------------
-- TRANSITION TO EQ-FREE LEMMA
Expand Down Expand Up @@ -1385,7 +1417,8 @@ Please use reverse-++-eqFree instead, which does not take eq."

∷-ʳ++ : ∀ .(eq : (suc m) + n ≡ m + suc n) a (xs : Vec A m) {ys} →
cast eq ((a ∷ xs) ʳ++ ys) ≡ xs ʳ++ (a ∷ ys)
∷-ʳ++ _ = ∷-ʳ++-eqFree
∷-ʳ++ _ a xs {ys} = ʳ++-ʳ++-eqFree (a ∷ []) {ys = xs} {zs = ys}

{-# WARNING_ON_USAGE ∷-ʳ++
"Warning: ∷-ʳ++ was deprecated in v2.2.
Please use ∷-ʳ++-eqFree instead, which does not take eq."
Expand Down