From 52faa1dedc90038f4377c0086140f301f06578c6 Mon Sep 17 00:00:00 2001 From: Alba Mendez Date: Mon, 1 Jul 2024 16:43:12 +0200 Subject: [PATCH 1/7] =?UTF-8?q?Vec.Properties:=20introduce=20`=E2=89=88-co?= =?UTF-8?q?ng=E2=80=B2`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Vec/Properties.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index bea3cfea95..84b6d9cfc6 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -381,6 +381,12 @@ cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs[eq]≡yys = let x≡y , xs[eq]≡ys = ∷-injective xxs[eq]≡yys in cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs[eq]≡ys) +≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n)) + {xs : Vec A m} {ys : Vec A n} .{eq} → xs ≈[ eq ] ys → + f xs ≈[ cong f-len eq ] f ys +≈-cong′ f {xs = []} {ys = []} refl = cast-is-id refl (f []) +≈-cong′ f {xs = x ∷ xs} {ys = y ∷ ys} refl = ≈-cong′ (f ∘ (x ∷_)) refl + ------------------------------------------------------------------------ -- map From d10ff67d1c70923f7155edbd56e6fabf8fca5fb4 Mon Sep 17 00:00:00 2001 From: Alba Mendez Date: Mon, 1 Jul 2024 16:43:01 +0200 Subject: [PATCH 2/7] derive cast-* lemmas from it --- src/Data/Vec/Properties.agda | 23 +++++------------------ 1 file changed, 5 insertions(+), 18 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 84b6d9cfc6..ff70d48183 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -400,9 +400,7 @@ map-const (_ ∷ xs) y = cong (y ∷_) (map-const xs y) map-cast : (f : A → B) .(eq : m ≡ n) (xs : Vec A m) → map f (cast eq xs) ≡ cast eq (map f xs) -map-cast {n = zero} f eq [] = refl -map-cast {n = suc _} f eq (x ∷ xs) - = cong (f x ∷_) (map-cast f (suc-injective eq) xs) +map-cast f _ _ = sym (≈-cong′ (map f) refl) map-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) → map f (xs ++ ys) ≡ map f xs ++ map f ys @@ -481,13 +479,11 @@ toList-map f (x ∷ xs) = cong (f x List.∷_) (toList-map f xs) cast-++ˡ : ∀ .(eq : m ≡ o) (xs : Vec A m) {ys : Vec A n} → cast (cong (_+ n) eq) (xs ++ ys) ≡ cast eq xs ++ ys -cast-++ˡ {o = zero} eq [] {ys} = cast-is-id refl (cast eq [] ++ ys) -cast-++ˡ {o = suc o} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ˡ (cong pred eq) xs) +cast-++ˡ _ _ {ys} = ≈-cong′ (_++ ys) refl cast-++ʳ : ∀ .(eq : n ≡ o) (xs : Vec A m) {ys : Vec A n} → cast (cong (m +_) eq) (xs ++ ys) ≡ xs ++ cast eq ys -cast-++ʳ {m = zero} eq [] {ys} = refl -cast-++ʳ {m = suc m} eq (x ∷ xs) {ys} = cong (x ∷_) (cast-++ʳ eq xs) +cast-++ʳ _ xs = ≈-cong′ (xs ++_) refl lookup-++-< : ∀ (xs : Vec A m) (ys : Vec A n) → ∀ i (i Date: Mon, 1 Jul 2024 16:43:54 +0200 Subject: [PATCH 3/7] use it in proofs --- .../Data/Vec/Relation/Binary/Equality/Cast.agda | 9 ++++----- src/Data/Vec/Properties.agda | 12 ++++-------- 2 files changed, 8 insertions(+), 13 deletions(-) diff --git a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda index e06cdb49f0..c55b1dac72 100644 --- a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda +++ b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda @@ -20,6 +20,7 @@ open import Data.Nat.Properties open import Data.Vec.Base open import Data.Vec.Properties open import Data.Vec.Relation.Binary.Equality.Cast +open import Function using (_∘_) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; module ≡-Reasoning) @@ -187,7 +188,7 @@ example3a-fromList-++-++ {xs = xs} {ys} {zs} eq = begin fromList (xs List.++ ys List.++ zs) ≈⟨ fromList-++ xs ⟩ fromList xs ++ fromList (ys List.++ zs) - ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (List.length-++ ys) (fromList xs)) (fromList-++ ys) ⟩ + ≈⟨ ≈-cong′ (fromList xs ++_) (fromList-++ ys) ⟩ fromList xs ++ fromList ys ++ fromList zs ∎ where open CastReasoning @@ -218,9 +219,7 @@ example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys → cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a) example4-cong² {m = m} {n} eq a xs ys = begin reverse ((xs ++ [ a ]) ++ ys) - ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys)) - (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a)) - (unfold-∷ʳ _ a xs)) ⟨ + ≈⟨ ≈-cong′ (reverse ∘ (_++ ys)) (unfold-∷ʳ (+-comm 1 m) a xs) ⟨ reverse ((xs ∷ʳ a) ++ ys) ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩ reverse ys ++ reverse (xs ∷ʳ a) @@ -264,7 +263,7 @@ example6a-reverse-∷ʳ {n = n} x xs = begin-≡ reverse (xs ∷ʳ x) ≡⟨ ≈-reflexive refl ⟨ reverse (xs ∷ʳ x) - ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩ + ≈⟨ ≈-cong′ reverse (unfold-∷ʳ (+-comm 1 n) x xs) ⟩ reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩ x ∷ reverse xs diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index ff70d48183..a862a009d4 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -1016,8 +1016,7 @@ reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) → reverse-++ {m = zero} {n = n} eq [] ys = ≈-sym (++-identityʳ (sym eq) (reverse ys)) reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin reverse (x ∷ xs ++ ys) ≂⟨ reverse-∷ x (xs ++ ys) ⟩ - reverse (xs ++ ys) ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (+-comm m n)) x (reverse (xs ++ ys))) - (reverse-++ _ xs ys) ⟩ + reverse (xs ++ ys) ∷ʳ x ≈⟨ ≈-cong′ (_∷ʳ x) (reverse-++ (+-comm m n) 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)) ∎ @@ -1068,8 +1067,7 @@ map-ʳ++ {ys = ys} f xs = begin cast eq ((xs ++ ys) ʳ++ zs) ≡ ys ʳ++ (xs ʳ++ zs) ++-ʳ++ {m = m} {n} {o} eq xs {ys} {zs} = begin ((xs ++ ys) ʳ++ zs) ≂⟨ unfold-ʳ++ (xs ++ ys) zs ⟩ - reverse (xs ++ ys) ++ zs ≈⟨ ≈-cong (_++ zs) (cast-++ˡ (+-comm m n) (reverse (xs ++ ys))) - (reverse-++ (+-comm m n) xs ys) ⟩ + reverse (xs ++ ys) ++ zs ≈⟨ ≈-cong′ (_++ zs) (reverse-++ (+-comm m n) xs ys) ⟩ (reverse ys ++ reverse xs) ++ zs ≈⟨ ++-assoc (trans (cong (_+ o) (+-comm n m)) eq) (reverse ys) (reverse xs) zs ⟩ reverse ys ++ (reverse xs ++ zs) ≂⟨ cong (reverse ys ++_) (unfold-ʳ++ xs zs) ⟨ reverse ys ++ (xs ʳ++ zs) ≂⟨ unfold-ʳ++ ys (xs ʳ++ zs) ⟨ @@ -1081,8 +1079,7 @@ map-ʳ++ {ys = ys} f xs = begin ʳ++-ʳ++ {m = m} {n} {o} eq 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) (cast-++ˡ (+-comm m n) (reverse (reverse xs ++ ys))) - (reverse-++ (+-comm m n) (reverse xs) ys) ⟩ + reverse (reverse xs ++ ys) ++ zs ≈⟨ ≈-cong′ (_++ zs) (reverse-++ (+-comm m n) (reverse xs) ys) ⟩ (reverse ys ++ reverse (reverse xs)) ++ zs ≂⟨ cong ((_++ zs) ∘ (reverse ys ++_)) (reverse-involutive xs) ⟩ (reverse ys ++ xs) ++ zs ≈⟨ ++-assoc (+-assoc n m o) (reverse ys) xs zs ⟩ reverse ys ++ (xs ++ zs) ≂⟨ unfold-ʳ++ ys (xs ++ zs) ⟨ @@ -1312,8 +1309,7 @@ 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-∷ʳ (+-comm 1 _) x (fromList (List.reverse xs)) ⟨ - fromList (List.reverse xs) ∷ʳ x ≈⟨ ≈-cong (_∷ʳ x) (cast-∷ʳ (cong suc (List.length-reverse xs)) _ _) - (fromList-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)) ∎ From 9146bee57bf438e62dfbde42e77c072fb7cc3cd8 Mon Sep 17 00:00:00 2001 From: Alba Mendez Date: Fri, 5 Jul 2024 17:47:15 +0200 Subject: [PATCH 4/7] match m and n before the Vecs --- src/Data/Vec/Properties.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index a862a009d4..4b832844a0 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -382,10 +382,10 @@ cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs[eq]≡yys = in cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs[eq]≡ys) ≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n)) - {xs : Vec A m} {ys : Vec A n} .{eq} → xs ≈[ eq ] ys → + {m n} {xs : Vec A m} {ys : Vec A n} .{eq} → xs ≈[ eq ] ys → f xs ≈[ cong f-len eq ] f ys -≈-cong′ f {xs = []} {ys = []} refl = cast-is-id refl (f []) -≈-cong′ f {xs = x ∷ xs} {ys = y ∷ ys} refl = ≈-cong′ (f ∘ (x ∷_)) refl +≈-cong′ f {m = zero} {n = zero} {xs = []} {ys = []} refl = cast-is-id refl (f []) +≈-cong′ f {m = suc m} {n = suc n} {xs = x ∷ xs} {ys = y ∷ ys} refl = ≈-cong′ (f ∘ (x ∷_)) refl ------------------------------------------------------------------------ -- map From 438f95aef8fe55d9965b001997040e876bebe3e2 Mon Sep 17 00:00:00 2001 From: Alba Mendez Date: Sun, 7 Jul 2024 13:00:58 +0200 Subject: [PATCH 5/7] convert Cast's implicit module param to variable (needed for next commit) --- src/Data/Vec/Relation/Binary/Equality/Cast.agda | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda index cc18556ea7..0d1fa78365 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda @@ -10,8 +10,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Data.Vec.Relation.Binary.Equality.Cast {a} {A : Set a} where +module Data.Vec.Relation.Binary.Equality.Cast where +open import Level using (Level) open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Nat.Properties using (suc-injective) open import Data.Vec.Base @@ -24,6 +25,8 @@ open import Relation.Binary.PropositionalEquality.Properties private variable + a : Level + A : Set a l m n o : ℕ xs ys zs : Vec A n @@ -41,16 +44,16 @@ cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) = infix 3 _≈[_]_ -_≈[_]_ : ∀ {n m} → Vec A n → .(eq : n ≡ m) → Vec A m → Set a +_≈[_]_ : ∀ {n m} → Vec A n → .(eq : n ≡ m) → Vec A m → Set _ xs ≈[ eq ] ys = cast eq xs ≡ ys ------------------------------------------------------------------------ -- _≈[_]_ is ‘reflexive’, ‘symmetric’ and ‘transitive’ -≈-reflexive : ∀ {n} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys) +≈-reflexive : ∀ {n} → _≡_ ⇒ (λ xs ys → _≈[_]_ {A = A} {n} xs refl ys) ≈-reflexive {x = x} eq = trans (cast-is-id refl x) eq -≈-sym : .{m≡n : m ≡ n} → Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_ +≈-sym : .{m≡n : m ≡ n} → Sym {A = Vec A m} _≈[ m≡n ]_ _≈[ sym m≡n ]_ ≈-sym {m≡n = m≡n} {xs} {ys} xs≈ys = begin cast (sym m≡n) ys ≡⟨ cong (cast (sym m≡n)) xs≈ys ⟨ cast (sym m≡n) (cast m≡n xs) ≡⟨ cast-trans m≡n (sym m≡n) xs ⟩ @@ -58,7 +61,8 @@ xs ≈[ eq ] ys = cast eq xs ≡ ys xs ∎ where open ≡-Reasoning -≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_ +≈-trans : ∀ .{m≡n : m ≡ n} .{n≡o : n ≡ o} → + Trans {A = Vec A m} _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_ ≈-trans {m≡n = m≡n} {n≡o} {xs} {ys} {zs} xs≈ys ys≈zs = begin cast (trans m≡n n≡o) xs ≡⟨ cast-trans m≡n n≡o xs ⟨ cast n≡o (cast m≡n xs) ≡⟨ cong (cast n≡o) xs≈ys ⟩ From cc6addb60c8249f4e0af46c9b155c6aa2671e8b8 Mon Sep 17 00:00:00 2001 From: Alba Mendez Date: Sun, 7 Jul 2024 13:05:14 +0200 Subject: [PATCH 6/7] =?UTF-8?q?move=20=E2=89=88-cong=E2=80=B2=20to=20Cast?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Vec/Properties.agda | 8 +------- src/Data/Vec/Relation/Binary/Equality/Cast.agda | 11 +++++++++-- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 4b832844a0..cf6ad9fc4f 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -369,7 +369,7 @@ lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs -- cast open VecCast public - using (cast-is-id; cast-trans) + using (cast-is-id; cast-trans; ≈-cong′) subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs subst-is-cast refl xs = sym (cast-is-id refl xs) @@ -381,12 +381,6 @@ cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs[eq]≡yys = let x≡y , xs[eq]≡ys = ∷-injective xxs[eq]≡yys in cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs[eq]≡ys) -≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n)) - {m n} {xs : Vec A m} {ys : Vec A n} .{eq} → xs ≈[ eq ] ys → - f xs ≈[ cong f-len eq ] f ys -≈-cong′ f {m = zero} {n = zero} {xs = []} {ys = []} refl = cast-is-id refl (f []) -≈-cong′ f {m = suc m} {n = suc n} {xs = x ∷ xs} {ys = y ∷ ys} refl = ≈-cong′ (f ∘ (x ∷_)) refl - ------------------------------------------------------------------------ -- map diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda index 0d1fa78365..cb8d5d6770 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda @@ -13,6 +13,7 @@ module Data.Vec.Relation.Binary.Equality.Cast where open import Level using (Level) +open import Function using (_∘_) open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Nat.Properties using (suc-injective) open import Data.Vec.Base @@ -25,8 +26,8 @@ open import Relation.Binary.PropositionalEquality.Properties private variable - a : Level - A : Set a + a b : Level + A B : Set a l m n o : ℕ xs ys zs : Vec A n @@ -70,6 +71,12 @@ xs ≈[ eq ] ys = cast eq xs ≡ ys zs ∎ where open ≡-Reasoning +≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n)) + {m n} {xs : Vec A m} {ys : Vec A n} .{eq} → xs ≈[ eq ] ys → + f xs ≈[ cong f-len eq ] f ys +≈-cong′ f {m = zero} {n = zero} {xs = []} {ys = []} refl = cast-is-id refl (f []) +≈-cong′ f {m = suc m} {n = suc n} {xs = x ∷ xs} {ys = y ∷ ys} refl = ≈-cong′ (f ∘ (x ∷_)) refl + ------------------------------------------------------------------------ -- Reasoning combinators From f702bee12e5ff05744bad99a384517557570e8c3 Mon Sep 17 00:00:00 2001 From: Alba Mendez Date: Sun, 7 Jul 2024 23:14:41 +0200 Subject: [PATCH 7/7] add changelog entry --- CHANGELOG.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index d5851dde0d..81f978660b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -736,6 +736,13 @@ Additions to existing modules toVec : (as : Vec≤ A n) → Vec A (Vec≤.length as) ``` +* Added new proofs to `Data.Vec.Relation.Binary.Equality.Cast`: + ```agda + ≈-cong′ : ∀ {f-len : ℕ → ℕ} (f : ∀ {n} → Vec A n → Vec B (f-len n)) + {m n} {xs : Vec A m} {ys : Vec A n} .{eq} → + xs ≈[ eq ] ys → f xs ≈[ _ ] f ys + ``` + * In `Data.Word64.Base`: ```agda _≤_ : Rel Word64 zero