Skip to content

[ fix #1443 ] Fin & Vec casts and properties #1839

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

Merged
MatthewDaggitt merged 4 commits into from
Oct 4, 2022
Merged

[ fix #1443 ] Fin & Vec casts and properties #1839

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
20279b7
[ re #1443 ] Missing Fin.cast properties
gallais Sep 30, 2022
c6a1ae0
[ cleanup ] trailing whitespace in CHANGELOG
gallais Sep 30, 2022
9b241ca
[ fix #1443 ] Also add cast for Vec
gallais Sep 30, 2022
3fc3872
[ discussion ] replace cast-is-subst with subst-is-cast
gallais Oct 2, 2022
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
29 changes: 22 additions & 7 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -370,15 +370,15 @@ Non-backwards compatible changes

* The definitions of the types for cancellativity in `Algebra.Definitions` previously
made some of their arguments implicit. This was under the assumption that the operators were
defined by pattern matching on the left argument so that Agda could always infer the
defined by pattern matching on the left argument so that Agda could always infer the
argument on the RHS.

* Although many of the operators defined in the library follow this convention, this is not
always true and cannot be assumed in user's code.

* Therefore the definitions have been changed as follows to make all their arguments explicit:
- `LeftCancellative _•_`
- From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z`
- `LeftCancellative _•_`
- From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z`
- To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z`

- `RightCancellative _•_`
Expand All @@ -394,10 +394,10 @@ Non-backwards compatible changes
- To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`

* Correspondingly some proofs of the above types will need additional arguments passed explicitly.
Instances can easily be fixed by adding additional underscores, e.g.
Instances can easily be fixed by adding additional underscores, e.g.
- `∙-cancelˡ x` to `∙-cancelˡ x _ _`
- `∙-cancelʳ y z` to `∙-cancelʳ _ y z`

### Change in the definition of `Prime`

* The definition of `Prime` in `Data.Nat.Primality` was:
Expand Down Expand Up @@ -1520,6 +1520,10 @@ Other minor changes
<⇒notInjective : ∀ {f : Fin m → Fin n} → n ℕ.< m → ¬ (Injective f)
ℕ→Fin-notInjective : ∀ (f : ℕ → Fin n) → ¬ (Injective f)
cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} → Injective f → Injective g → m ≡ n

cast-is-id : cast eq k ≡ k
subst-is-cast : subst Fin eq k ≡ cast eq k
cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k
```

* Added new functions in `Data.Integer.Base`:
Expand Down Expand Up @@ -1832,6 +1836,8 @@ Other minor changes
diagonal : Vec (Vec A n) n → Vec A n
DiagonalBind._>>=_ : Vec A n → (A → Vec B n) → Vec B n
_ʳ++_ : Vec A m → Vec A n → Vec A (m + n)

cast : .(eq : m ≡ n) → Vec A m → Vec A n
```

* Added new instance in `Data.Vec.Categorical`:
Expand Down Expand Up @@ -1890,6 +1896,15 @@ Other minor changes
reverse-injective : reverse xs ≡ reverse ys → xs ≡ ys

transpose-replicate : transpose (replicate xs) ≡ map replicate xs

toList-cast : toList (cast eq xs) ≡ toList xs
cast-is-id : cast eq xs ≡ xs
subst-is-cast : subst (Vec A) eq xs ≡ cast eq xs
cast-trans : cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
map-cast : map f (cast eq xs) ≡ cast eq (map f xs)
lookup-cast : lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
lookup-cast₁ : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
lookup-cast₂ : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
```

* Added new proofs in `Data.Vec.Functional.Properties`:
Expand Down
15 changes: 14 additions & 1 deletion src/Data/Fin/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -249,13 +249,26 @@ toℕ-fromℕ<″ {m} {n} m<n = begin
where open ≡-Reasoning

------------------------------------------------------------------------
-- cast
-- Properties of cast
------------------------------------------------------------------------

toℕ-cast : ∀ .(eq : m ≡ n) (k : Fin m) → toℕ (cast eq k) ≡ toℕ k
toℕ-cast {n = suc n} eq zero = refl
toℕ-cast {n = suc n} eq (suc k) = cong suc (toℕ-cast (cong ℕ.pred eq) k)

cast-is-id : .(eq : m ≡ m) (k : Fin m) → cast eq k ≡ k
cast-is-id eq zero = refl
cast-is-id eq (suc k) = cong suc (cast-is-id (ℕₚ.suc-injective eq) k)

subst-is-cast : (eq : m ≡ n) (k : Fin m) → subst Fin eq k ≡ cast eq k
subst-is-cast refl k = sym (cast-is-id refl k)

cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (k : Fin m) →
cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k
cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ zero = refl
cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (suc k) =
cong suc (cast-trans (ℕₚ.suc-injective eq₁) (ℕₚ.suc-injective eq₂) k)

------------------------------------------------------------------------
-- Properties of _≤_
------------------------------------------------------------------------
Expand Down
6 changes: 5 additions & 1 deletion src/Data/Vec/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ open import Data.Product as Prod using (∃; ∃₂; _×_; _,_)
open import Data.These.Base as These using (These; this; that; these)
open import Function.Base using (const; _∘′_; id; _∘_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
open import Relation.Nullary using (does)
open import Relation.Unary using (Pred; Decidable)

Expand Down Expand Up @@ -93,6 +93,10 @@ xs [ i ]≔ y = xs [ i ]%= const y
------------------------------------------------------------------------
-- Operations for transforming vectors

cast : .(eq : m ≡ n) → Vec A m → Vec A n
cast {n = zero} eq [] = []
cast {n = suc _} eq (x ∷ xs) = x ∷ cast (cong pred eq) xs

map : (A → B) → Vec A n → Vec B n
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs
Expand Down
62 changes: 57 additions & 5 deletions src/Data/Vec/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ open import Data.Bool.Base using (true; false)
open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ; _↑ˡ_; _↑ʳ_)
open import Data.List.Base as List using (List)
open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Nat.Properties as ℕₚ
using (+-assoc; ≤-step; ≤-refl; ≤-trans)
open import Data.Product as Prod
using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
Expand All @@ -25,7 +25,7 @@ open import Function.Inverse using (_↔_; inverse)
open import Level using (Level)
open import Relation.Binary hiding (Decidable)
open import Relation.Binary.PropositionalEquality
using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (Dec; does; yes; no)
open import Relation.Nullary.Decidable using (map′)
Expand All @@ -39,7 +39,7 @@ private
a b c d p : Level
A B C D : Set a
w x y z : A
m n : ℕ
m n o : ℕ
ws xs ys zs : Vec A n

------------------------------------------------------------------------
Expand Down Expand Up @@ -386,6 +386,27 @@ lookup∘update′ : ∀ {i j} → i ≢ j → ∀ (xs : Vec A n) y →
lookup (xs [ j ]≔ y) i ≡ lookup xs i
lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs

------------------------------------------------------------------------
-- cast

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) =
cong (x List.∷_) (toList-cast (cong pred eq) xs)

cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
cast-is-id eq [] = refl
cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (ℕₚ.suc-injective eq) xs)

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)

cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (xs : Vec A m) →
cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
cast-trans {m = zero} {n = zero} {o = zero} eq₁ eq₂ [] = refl
cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
cong (x ∷_) (cast-trans (ℕₚ.suc-injective eq₁) (ℕₚ.suc-injective eq₂) xs)

------------------------------------------------------------------------
-- map

Expand All @@ -397,6 +418,12 @@ map-const : ∀ (xs : Vec A n) (y : B) → map (const y) xs ≡ replicate y
map-const [] _ = refl
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-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) →
map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++ f [] ys = refl
Expand Down Expand Up @@ -487,9 +514,34 @@ lookup-splitAt (suc m) (x ∷ xs) ys (suc i) = trans
------------------------------------------------------------------------
-- concat

lookup-concat : ∀ (xss : Vec (Vec A m) n) i j → lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j
lookup-cast : .(eq : m ≡ n) (xs : Vec A m) (i : Fin m) →
lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
lookup-cast {n = suc _} eq (x ∷ _) zero = refl
lookup-cast {n = suc _} eq (_ ∷ xs) (suc i) =
lookup-cast (ℕₚ.suc-injective eq) xs i

lookup-cast₁ : .(eq : m ≡ n) (xs : Vec A m) (i : Fin n) →
lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
lookup-cast₁ eq (x ∷ _) zero = refl
lookup-cast₁ eq (_ ∷ xs) (suc i) =
lookup-cast₁ (ℕₚ.suc-injective eq) xs i

lookup-cast₂ : .(eq : m ≡ n) (xs : Vec A n) (i : Fin m) →
lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
lookup-cast₂ {n = suc _} eq (x ∷ _) zero = refl
lookup-cast₂ {n = suc _} eq (_ ∷ xs) (suc i) =
lookup-cast₂ (ℕₚ.suc-injective eq) xs i

lookup-concat : ∀ (xss : Vec (Vec A m) n) i j →
lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j
lookup-concat (xs ∷ xss) zero j = lookup-++ˡ xs (concat xss) j
lookup-concat (xs ∷ xss) (suc i) j = trans (lookup-++ʳ xs (concat xss) (Fin.combine i j)) (lookup-concat xss i j)
lookup-concat (xs ∷ xss) (suc i) j = begin
lookup (concat (xs ∷ xss)) (Fin.combine (suc i) j)
≡⟨ lookup-++ʳ xs (concat xss) (Fin.combine i j) ⟩
lookup (concat xss) (Fin.combine i j)
≡⟨ lookup-concat xss i j ⟩
lookup (lookup (xs ∷ xss) (suc i)) j
∎ where open ≡-Reasoning

------------------------------------------------------------------------
-- zipWith
Expand Down