From bdb964dc9d036eb8d0f6f0a0ab1075c144913577 Mon Sep 17 00:00:00 2001 From: Nils Anders Danielsson Date: Thu, 7 Apr 2022 18:28:03 +0200 Subject: [PATCH 1/5] Changed the fixity of _/Var_. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit So that one can write t /Var ρ₁ / ρ₂ without parentheses. --- CHANGELOG.md | 2 ++ src/Data/Fin/Substitution.agda | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b1625a1861..d878b2b6fa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1142,6 +1142,8 @@ Other minor changes cantor-schröder-bernstein : ∀ {f : Fin m → Fin n} {g : Fin n → Fin m} → Injective f → Injective g → m ≡ n ``` +* Changed the fixity of `Data.Fin.Substitution.TermSubst._/Var_`. + * Added new functions in `Data.Integer.Base`: ``` _^_ : ℤ → ℕ → ℤ diff --git a/src/Data/Fin/Substitution.agda b/src/Data/Fin/Substitution.agda index da76267ad7..809b235dd4 100644 --- a/src/Data/Fin/Substitution.agda +++ b/src/Data/Fin/Substitution.agda @@ -160,7 +160,7 @@ record TermSubst (T : Pred ℕ 0ℓ) : Set₁ where varLift : Lift Fin T varLift = record { simple = VarSubst.simple; lift = var } - infix 8 _/Var_ + infixl 8 _/Var_ _/Var_ : ∀ {m n} → T m → Sub Fin m n → T n _/Var_ = app varLift From 3ec8125b45558731d2b92c83c14d147bc046e34e Mon Sep 17 00:00:00 2001 From: Nils Anders Danielsson Date: Thu, 7 Apr 2022 18:57:28 +0200 Subject: [PATCH 2/5] Added some lemmas relating renamings to substitutions. --- CHANGELOG.md | 30 ++++++++++++ src/Data/Fin/Substitution/Lemmas.agda | 66 +++++++++++++++++++++++++++ 2 files changed, 96 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index d878b2b6fa..76ee6f5f5b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1144,6 +1144,36 @@ Other minor changes * Changed the fixity of `Data.Fin.Substitution.TermSubst._/Var_`. +* Added new lemmas in `Data.Fin.Substitution.Lemmas.TermLemmas`: + ``` + map-var≡ : + ∀ {m n} {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → + (∀ x → lookup ρ₁ x ≡ f x) → + (∀ x → lookup ρ₂ x ≡ T.var (f x)) → + map T.var ρ₁ ≡ ρ₂ + wk≡wk : + ∀ {n} → map T.var VarSubst.wk ≡ T.wk {n = n} + id≡id : + ∀ {n} → map T.var VarSubst.id ≡ T.id {n = n} + sub≡sub : + ∀ {n} {x : Fin n} → + map T.var (VarSubst.sub x) ≡ T.sub (T.var x) + ↑≡↑ : + ∀ {m n} {ρ : Sub Fin m n} → + map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ + /Var≡/ : + ∀ {m n} {ρ : Sub Fin m n} {t} → + t /Var ρ ≡ t T./ map T.var ρ + sub-renaming-commutes : + ∀ {m n t x} {ρ : Sub T m n} → + t /Var VarSubst.sub x T./ ρ ≡ + t T./ ρ T.↑ T./ T.sub (lookup ρ x) + sub-commutes-with-renaming : + ∀ {m n} {t t′} {ρ : Sub Fin m n} → + t T./ T.sub t′ /Var ρ ≡ + t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) + ``` + * Added new functions in `Data.Integer.Base`: ``` _^_ : ℤ → ℕ → ℤ diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda index 05fd00a4cc..fc1bc66036 100644 --- a/src/Data/Fin/Substitution/Lemmas.agda +++ b/src/Data/Fin/Substitution/Lemmas.agda @@ -543,3 +543,69 @@ record TermLemmas (T : ℕ → Set) : Set₁ where T.weaken t₁ T./ (T.sub t₂) ≡⟨ weaken-∷ t₁ ⟩ t₁ T./ T.id ≡⟨ id-vanishes t₁ ⟩ t₁ ∎ + + -- Lemmas relating renamings to substitutions. + + map-var≡ : + ∀ {m n} {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → + (∀ x → lookup ρ₁ x ≡ f x) → + (∀ x → lookup ρ₂ x ≡ T.var (f x)) → + map T.var ρ₁ ≡ ρ₂ + map-var≡ {ρ₁ = ρ₁} {ρ₂ = ρ₂} {f = f} hyp₁ hyp₂ = extensionality λ x → + lookup (map T.var ρ₁) x ≡⟨ VecProp.lookup-map x _ ρ₁ ⟩ + T.var (lookup ρ₁ x) ≡⟨ cong T.var $ hyp₁ x ⟩ + T.var (f x) ≡⟨ sym $ hyp₂ x ⟩ + lookup ρ₂ x ∎ + + wk≡wk : ∀ {n} → map T.var VarSubst.wk ≡ T.wk {n = n} + wk≡wk = map-var≡ VarLemmas.lookup-wk lookup-wk + + id≡id : ∀ {n} → map T.var VarSubst.id ≡ T.id {n = n} + id≡id = map-var≡ VarLemmas.lookup-id lookup-id + + sub≡sub : + ∀ {n} {x : Fin n} → + map T.var (VarSubst.sub x) ≡ T.sub (T.var x) + sub≡sub = cong (_ ∷_) id≡id + + ↑≡↑ : + ∀ {m n} {ρ : Sub Fin m n} → + map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ + ↑≡↑ {ρ = ρ} = map-var≡ + (VarLemmas.lookup-↑⋆ (lookup ρ) (λ _ → refl) 1) + (lookup-↑⋆ (lookup ρ) (λ _ → VecProp.lookup-map _ _ ρ) 1) + + /Var≡/ : + ∀ {m n} {ρ : Sub Fin m n} {t} → + t /Var ρ ≡ t T./ map T.var ρ + /Var≡/ {ρ = ρ} {t = t} = + /✶-↑✶ (ε ▻ ρ) (ε ▻ map T.var ρ) + (λ k x → + T.var x /Var ρ VarSubst.↑⋆ k ≡⟨ app-var ⟩ + T.var (lookup (ρ VarSubst.↑⋆ k) x) ≡⟨ cong T.var $ VarLemmas.lookup-↑⋆ _ (λ _ → refl) k _ ⟩ + T.var (lift k (VarSubst._/ ρ) x) ≡⟨ sym $ lookup-↑⋆ _ (λ _ → VecProp.lookup-map _ _ ρ) k _ ⟩ + lookup (map T.var ρ T.↑⋆ k) x ≡⟨ sym app-var ⟩ + T.var x T./ map T.var ρ T.↑⋆ k ∎) + zero t + + sub-renaming-commutes : + ∀ {m n t x} {ρ : Sub T m n} → + t /Var VarSubst.sub x T./ ρ ≡ + t T./ ρ T.↑ T./ T.sub (lookup ρ x) + sub-renaming-commutes {t = t} {x = x} {ρ = ρ} = + t /Var VarSubst.sub x T./ ρ ≡⟨ cong (T._/ ρ) /Var≡/ ⟩ + t T./ map T.var (VarSubst.sub x) T./ ρ ≡⟨ cong (λ ρ′ → t T./ ρ′ T./ ρ) sub≡sub ⟩ + t T./ T.sub (T.var x) T./ ρ ≡⟨ sub-commutes _ ⟩ + t T./ ρ T.↑ T./ T.sub (T.var x T./ ρ) ≡⟨ cong (λ t′ → t T./ ρ T.↑ T./ T.sub t′) app-var ⟩ + t T./ ρ T.↑ T./ T.sub (lookup ρ x) ∎ + + sub-commutes-with-renaming : + ∀ {m n} {t t′} {ρ : Sub Fin m n} → + t T./ T.sub t′ /Var ρ ≡ + t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) + sub-commutes-with-renaming {t = t} {t′ = t′} {ρ = ρ} = + t T./ T.sub t′ /Var ρ ≡⟨ /Var≡/ ⟩ + t T./ T.sub t′ T./ map T.var ρ ≡⟨ sub-commutes _ ⟩ + t T./ map T.var ρ T.↑ T./ T.sub (t′ T./ map T.var ρ) ≡⟨ sym $ cong (λ ρ′ → t T./ ρ′ T./ T.sub (t′ T./ map T.var ρ)) ↑≡↑ ⟩ + t T./ map T.var (ρ VarSubst.↑) T./ T.sub (t′ T./ map T.var ρ) ≡⟨ sym $ cong₂ (λ t ρ → t T./ T.sub ρ) /Var≡/ /Var≡/ ⟩ + t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) ∎ From 41f796f128e6455c9e97a36748000d96e891d163 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 17 Aug 2023 12:44:39 +0100 Subject: [PATCH 3/5] added fixity change --- CHANGELOG.md | 42 ++++++++++++++++-------------------------- 1 file changed, 16 insertions(+), 26 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 76ee6f5f5b..1403738bca 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1143,35 +1143,25 @@ Other minor changes ``` * Changed the fixity of `Data.Fin.Substitution.TermSubst._/Var_`. + ```agda + infix 8 ↦ infixl 8 + ``` * Added new lemmas in `Data.Fin.Substitution.Lemmas.TermLemmas`: ``` - map-var≡ : - ∀ {m n} {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → - (∀ x → lookup ρ₁ x ≡ f x) → - (∀ x → lookup ρ₂ x ≡ T.var (f x)) → - map T.var ρ₁ ≡ ρ₂ - wk≡wk : - ∀ {n} → map T.var VarSubst.wk ≡ T.wk {n = n} - id≡id : - ∀ {n} → map T.var VarSubst.id ≡ T.id {n = n} - sub≡sub : - ∀ {n} {x : Fin n} → - map T.var (VarSubst.sub x) ≡ T.sub (T.var x) - ↑≡↑ : - ∀ {m n} {ρ : Sub Fin m n} → - map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ - /Var≡/ : - ∀ {m n} {ρ : Sub Fin m n} {t} → - t /Var ρ ≡ t T./ map T.var ρ - sub-renaming-commutes : - ∀ {m n t x} {ρ : Sub T m n} → - t /Var VarSubst.sub x T./ ρ ≡ - t T./ ρ T.↑ T./ T.sub (lookup ρ x) - sub-commutes-with-renaming : - ∀ {m n} {t t′} {ρ : Sub Fin m n} → - t T./ T.sub t′ /Var ρ ≡ - t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) + map-var≡ : {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → + (∀ x → lookup ρ₁ x ≡ f x) → + (∀ x → lookup ρ₂ x ≡ T.var (f x)) → + map T.var ρ₁ ≡ ρ₂ + wk≡wk : map T.var VarSubst.wk ≡ T.wk {n = n} + id≡id : map T.var VarSubst.id ≡ T.id {n = n} + sub≡sub : {x : Fin n} → map T.var (VarSubst.sub x) ≡ T.sub (T.var x) + ↑≡↑ : {ρ : Sub Fin m n} → map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ + /Var≡/ : {ρ : Sub Fin m n} {t} → t /Var ρ ≡ t T./ map T.var ρ + sub-renaming-commutes : {ρ : Sub T m n} → + t /Var VarSubst.sub x T./ ρ ≡ t T./ ρ T.↑ T./ T.sub (lookup ρ x) + sub-commutes-with-renaming : {ρ : Sub Fin m n} → + t T./ T.sub t′ /Var ρ ≡ t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) ``` * Added new functions in `Data.Integer.Base`: From c39207348c21ce200c3e35aabe32117f7a02ba82 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 17 Aug 2023 12:45:49 +0100 Subject: [PATCH 4/5] fixing whitespace per library convention --- src/Data/Fin/Substitution/Lemmas.agda | 42 +++++++++++---------------- 1 file changed, 17 insertions(+), 25 deletions(-) diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda index fc1bc66036..23ae56566d 100644 --- a/src/Data/Fin/Substitution/Lemmas.agda +++ b/src/Data/Fin/Substitution/Lemmas.agda @@ -528,11 +528,12 @@ record TermLemmas (T : ℕ → Set) : Set₁ where open Lemmas₅ lemmas₅ public hiding (lemmas₃) wk-⊙-∷ : ∀ {m n} (t : T n) (ρ : Sub T m n) → (T.wk T.⊙ (t ∷ ρ)) ≡ ρ - wk-⊙-∷ t ρ = extensionality (λ x → begin + wk-⊙-∷ t ρ = extensionality λ x → begin lookup (T.wk T.⊙ (t ∷ ρ)) x ≡⟨ L₃.lookup-wk-↑⋆-⊙ 0 {ρ = t ∷ ρ} ⟩ - lookup ρ x ∎) + lookup ρ x ∎ - weaken-∷ : ∀ {k n} (t₁ : T k) {t₂ : T n} {ρ : Sub T k n} → T.weaken t₁ T./ (t₂ ∷ ρ) ≡ t₁ T./ ρ + weaken-∷ : ∀ {k n} (t₁ : T k) {t₂ : T n} {ρ : Sub T k n} → + T.weaken t₁ T./ (t₂ ∷ ρ) ≡ t₁ T./ ρ weaken-∷ t₁ {t₂} {ρ} = begin T.weaken t₁ T./ (t₂ ∷ ρ) ≡⟨ cong (T._/ (t₂ ∷ ρ)) (sym /-wk) ⟩ (t₁ T./ T.wk) T./ (t₂ ∷ ρ) ≡⟨ ⨀→/✶ ((t₂ ∷ ρ) ◅ T.wk ◅ ε) (ρ ◅ ε) (wk-⊙-∷ t₂ ρ) t₁ ⟩ @@ -546,11 +547,10 @@ record TermLemmas (T : ℕ → Set) : Set₁ where -- Lemmas relating renamings to substitutions. - map-var≡ : - ∀ {m n} {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → - (∀ x → lookup ρ₁ x ≡ f x) → - (∀ x → lookup ρ₂ x ≡ T.var (f x)) → - map T.var ρ₁ ≡ ρ₂ + map-var≡ : ∀ {m n} {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → + (∀ x → lookup ρ₁ x ≡ f x) → + (∀ x → lookup ρ₂ x ≡ T.var (f x)) → + map T.var ρ₁ ≡ ρ₂ map-var≡ {ρ₁ = ρ₁} {ρ₂ = ρ₂} {f = f} hyp₁ hyp₂ = extensionality λ x → lookup (map T.var ρ₁) x ≡⟨ VecProp.lookup-map x _ ρ₁ ⟩ T.var (lookup ρ₁ x) ≡⟨ cong T.var $ hyp₁ x ⟩ @@ -563,21 +563,17 @@ record TermLemmas (T : ℕ → Set) : Set₁ where id≡id : ∀ {n} → map T.var VarSubst.id ≡ T.id {n = n} id≡id = map-var≡ VarLemmas.lookup-id lookup-id - sub≡sub : - ∀ {n} {x : Fin n} → - map T.var (VarSubst.sub x) ≡ T.sub (T.var x) + sub≡sub : ∀ {n} {x : Fin n} → + map T.var (VarSubst.sub x) ≡ T.sub (T.var x) sub≡sub = cong (_ ∷_) id≡id - ↑≡↑ : - ∀ {m n} {ρ : Sub Fin m n} → - map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ + ↑≡↑ : ∀ {m n} {ρ : Sub Fin m n} → + map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ ↑≡↑ {ρ = ρ} = map-var≡ (VarLemmas.lookup-↑⋆ (lookup ρ) (λ _ → refl) 1) (lookup-↑⋆ (lookup ρ) (λ _ → VecProp.lookup-map _ _ ρ) 1) - /Var≡/ : - ∀ {m n} {ρ : Sub Fin m n} {t} → - t /Var ρ ≡ t T./ map T.var ρ + /Var≡/ : ∀ {m n} {ρ : Sub Fin m n} {t} → t /Var ρ ≡ t T./ map T.var ρ /Var≡/ {ρ = ρ} {t = t} = /✶-↑✶ (ε ▻ ρ) (ε ▻ map T.var ρ) (λ k x → @@ -588,10 +584,8 @@ record TermLemmas (T : ℕ → Set) : Set₁ where T.var x T./ map T.var ρ T.↑⋆ k ∎) zero t - sub-renaming-commutes : - ∀ {m n t x} {ρ : Sub T m n} → - t /Var VarSubst.sub x T./ ρ ≡ - t T./ ρ T.↑ T./ T.sub (lookup ρ x) + sub-renaming-commutes : ∀ {m n t x} {ρ : Sub T m n} → + t /Var VarSubst.sub x T./ ρ ≡ t T./ ρ T.↑ T./ T.sub (lookup ρ x) sub-renaming-commutes {t = t} {x = x} {ρ = ρ} = t /Var VarSubst.sub x T./ ρ ≡⟨ cong (T._/ ρ) /Var≡/ ⟩ t T./ map T.var (VarSubst.sub x) T./ ρ ≡⟨ cong (λ ρ′ → t T./ ρ′ T./ ρ) sub≡sub ⟩ @@ -599,10 +593,8 @@ record TermLemmas (T : ℕ → Set) : Set₁ where t T./ ρ T.↑ T./ T.sub (T.var x T./ ρ) ≡⟨ cong (λ t′ → t T./ ρ T.↑ T./ T.sub t′) app-var ⟩ t T./ ρ T.↑ T./ T.sub (lookup ρ x) ∎ - sub-commutes-with-renaming : - ∀ {m n} {t t′} {ρ : Sub Fin m n} → - t T./ T.sub t′ /Var ρ ≡ - t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) + sub-commutes-with-renaming : ∀ {m n} {t t′} {ρ : Sub Fin m n} → + t T./ T.sub t′ /Var ρ ≡ t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) sub-commutes-with-renaming {t = t} {t′ = t′} {ρ = ρ} = t T./ T.sub t′ /Var ρ ≡⟨ /Var≡/ ⟩ t T./ T.sub t′ T./ map T.var ρ ≡⟨ sub-commutes _ ⟩ From 6123b7dfd784cfcd670f8d80b7f0cab7787c8703 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 4 Sep 2023 10:15:26 +0100 Subject: [PATCH 5/5] cosmetic, but significant, overhaul after review comments --- CHANGELOG.md | 1604 ++++++++++++++++- .../Data/Fin/Substitution/UntypedLambda.agda | 103 ++ src/Data/Fin/Substitution.agda | 56 +- src/Data/Fin/Substitution/Example.agda | 14 +- src/Data/Fin/Substitution/Lemmas.agda | 162 +- src/Data/Fin/Substitution/List.agda | 22 +- 6 files changed, 1742 insertions(+), 219 deletions(-) create mode 100644 README/Data/Fin/Substitution/UntypedLambda.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 76ee6f5f5b..627ae25064 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ Version 2.0-dev =============== -The library has been tested using Agda 2.6.2. +The library has been tested using Agda 2.6.3. Highlights ---------- @@ -19,9 +19,109 @@ Highlights * Improved the `solve` tactic in `Tactic.RingSolver` to work in a much wider range of situations. +* Added `⌊log₂_⌋` and `⌈log₂_⌉` on Natural Numbers. + +* A massive refactoring of the unindexed Functor/Applicative/Monad hierarchy + and the MonadReader / MonadState type classes. These are now usable with + instance arguments as demonstrated in the tests/monad examples. + + Bug-fixes --------- +* The following operators were missing a fixity declaration, which has now + been fixed - + ``` + infixr 5 _∷_ (Codata.Guarded.Stream) + infix 4 _[_] (Codata.Guarded.Stream) + infixr 5 _∷_ (Codata.Guarded.Stream.Relation.Binary.Pointwise) + infix 4 _≈∞_ (Codata.Guarded.Stream.Relation.Binary.Pointwise) + infixr 5 _∷_ (Codata.Musical.Colist) + infix 4 _≈_ (Codata.Musical.Conat) + infixr 5 _∷_ (Codata.Musical.Colist.Bisimilarity) + infixr 5 _∷_ (Codata.Musical.Colist.Relation.Unary.All) + infixr 5 _∷_ (Codata.Sized.Colist) + infixr 5 _∷_ (Codata.Sized.Covec) + infixr 5 _∷_ (Codata.Sized.Cowriter) + infixl 1 _>>=_ (Codata.Sized.Cowriter) + infixr 5 _∷_ (Codata.Sized.Stream) + infixr 5 _∷_ (Codata.Sized.Colist.Bisimilarity) + infix 4 _ℕ≤?_ (Codata.Sized.Conat.Properties) + infixr 5 _∷_ (Codata.Sized.Covec.Bisimilarity) + infixr 5 _∷_ (Codata.Sized.Cowriter.Bisimilarity) + infixr 5 _∷_ (Codata.Sized.Stream.Bisimilarity) + infixr 8 _⇒_ _⊸_ (Data.Container.Core) + infixr -1 _<$>_ _<*>_ (Data.Container.FreeMonad) + infixl 1 _>>=_ (Data.Container.FreeMonad) + infix 5 _▷_ (Data.Container.Indexed) + infix 4 _≈_ (Data.Float.Base) + infixl 7 _⊓′_ (Data.Nat.Base) + infixl 6 _⊔′_ (Data.Nat.Base) + infixr 8 _^_ (Data.Nat.Base) + infix 4 _!≢0 _!*_!≢0 (Data.Nat.Properties) + infix 4 _≃?_ (Data.Rational.Unnormalised.Properties) + infix 4 _≈ₖᵥ_ (Data.Tree.AVL.Map.Membership.Propositional) + infix 4 _<_ (Induction.WellFounded) + infix -1 _$ⁿ_ (Data.Vec.N-ary) + infix 4 _≋_ (Data.Vec.Functional.Relation.Binary.Equality.Setoid) + infix 4 _≟_ (Reflection.AST.Definition) + infix 4 _≡ᵇ_ (Reflection.AST.Literal) + infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Meta) + infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Name) + infix 4 _≟-Telescope_ (Reflection.AST.Term) + infix 4 _≟_ (Reflection.AST.Argument.Information) + infix 4 _≟_ (Reflection.AST.Argument.Modality) + infix 4 _≟_ (Reflection.AST.Argument.Quantity) + infix 4 _≟_ (Reflection.AST.Argument.Relevance) + infix 4 _≟_ (Reflection.AST.Argument.Visibility) + infixr 8 _^_ (Function.Endomorphism.Propositional) + infixr 8 _^_ (Function.Endomorphism.Setoid) + infix 4 _≃_ (Function.HalfAdjointEquivalence) + infix 4 _≈_ _≈ᵢ_ _≤_ (Function.Metric.Bundles) + infixl 6 _∙_ (Function.Metric.Bundles) + infix 4 _≈_ (Function.Metric.Nat.Bundles) + infix 3 _←_ _↢_ (Function.Related) + infix 4 _ℕ<_ _ℕ≤infinity _ℕ≤_ (Codata.Sized.Conat) + infix 6 _ℕ+_ _+ℕ_ (Codata.Sized.Conat) + infixl 4 _+ _* (Data.List.Kleene.Base) + infixr 4 _++++_ _+++*_ _*+++_ _*++*_ (Data.List.Kleene.Base) + infix 4 _[_]* _[_]+ (Data.List.Kleene.Base) + infix 4 _≢∈_ (Data.List.Membership.Propositional) + infixr 5 _`∷_ (Data.List.Reflection) + infix 4 _≡?_ (Data.List.Relation.Binary.Equality.DecPropositional) + infixr 5 _++ᵖ_ (Data.List.Relation.Binary.Prefix.Heterogeneous) + infixr 5 _++ˢ_ (Data.List.Relation.Binary.Suffix.Heterogeneous) + infixr 5 _++_ _++[] (Data.List.Relation.Ternary.Appending.Propositional) + infixr 5 _∷=_ (Data.List.Relation.Unary.Any) + infixr 5 _++_ (Data.List.Ternary.Appending) + infixr 2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_ _×-cong_ (Data.Product.Function.NonDependent.Propositional) + infixr 2 _×-⟶_ (Data.Product.Function.NonDependent.Setoid) + infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_ (Data.Product.Function.NonDependent.Setoid) + infixr 2 _×-surjection_ _×-inverse_ (Data.Product.Function.NonDependent.Setoid) + infixr 1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_ _⊎-cong_ (Data.Sum.Function.Propositional) + infixr 1 _⊎-⟶_ (Data.Sum.Function.Setoid) + infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_ (Data.Sum.Function.Setoid) + infixr 1 _⊎-surjection_ _⊎-inverse_ (Data.Sum.Function.Setoid) + infix 8 _⁻¹ (Data.Parity.Base) + infixr 5 _`∷_ (Data.Vec.Reflection) + infixr 5 _∷=_ (Data.Vec.Membership.Setoid) + infix 4 _≟H_ _≟N_ (Algebra.Solver.Ring) + infix 4 _≈_ (Relation.Binary.Bundles) + infixl 6 _∩_ (Relation.Binary.Construct.Intersection) + infix 4 _<₋_ (Relation.Binary.Construct.Add.Infimum.Strict) + infix 4 _≈∙_ (Relation.Binary.Construct.Add.Point.Equality) + infix 4 _≤⁺_ _≤⊤⁺ (Relation.Binary.Construct.Add.Supremum.NonStrict) + infixr 5 _∷ʳ_ (Relation.Binary.Construct.Closure.Transitive) + infixr 5 _∷_ (Codata.Guarded.Stream.Relation.Unary.All) + infixr 5 _∷_ (Foreign.Haskell.List.NonEmpty) + infix 4 _≈_ (Function.Metric.Rational.Bundles) + infixl 6 _ℕ+_ (Level.Literals) + infixr 6 _∪_ (Relation.Binary.Construct.Union) + infixl 6 _+ℤ_ (Relation.Binary.HeterogeneousEquality.Quotients.Examples) + infix 4 _≉_ _≈ᵢ_ _≤ᵢ_ (Relation.Binary.Indexed.Homogeneous.Bundles) + infixr 5 _∷ᴹ_ _∷⁻¹ᴹ_ (Text.Regex.Search) + ``` + * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer rather than a natural. The previous binding was incorrectly assuming that all exit codes where non-negative. @@ -40,8 +140,23 @@ Bug-fixes * Add module `Algebra.Module` that re-exports the contents of `Algebra.Module.(Definitions/Structures/Bundles)` +* Various module-like bundles in `Algebra.Module.Bundles` were missing a fixity + declaration for `_*ᵣ_`. This has been fixed. + * In `Algebra.Definitions.RawSemiring` the record `prime` add `p∤1 : p ∤ 1#` to the field. +* In `Data.List.Relation.Ternary.Appending.Setoid` we re-export specialised versions of + the constructors using the setoid's carrier set. Prior to that, the constructor were + re-exported in their full generality which would lead to unsolved meta variables at + their use sites. + +* In `Data.Container.FreeMonad`, we give a direct definition of `_⋆_` as an inductive + type rather than encoding it as an instance of `μ`. This ensures Agda notices that + `C ⋆ X` is strictly positive in `X` which in turn allows us to use the free monad + when defining auxiliary (co)inductive types (cf. the `Tap` example in + `README.Data.Container.FreeMonad`). + +* In `Data.Maybe.Base` the fixity declaration of `_<∣>_` was missing. This has been fixed. Non-backwards compatible changes -------------------------------- @@ -66,8 +181,7 @@ Non-backwards compatible changes such as `Monad`, `Applicative`, `Functor`, etc, under `Category.*`, as this obstructs the importing of the `agda-categories` development into the Standard Library, and moreover needlessly restricts the applicability of categorical concepts to this - (highly specific) mode of use. Correspondingly, modules grouped under `*.Categorical.*` - which exploited these structures for effectful programming have been renamed `*.Effectful`. + (highly specific) mode of use. Correspondingly, client modules grouped under `*.Categorical.*` which exploit such structure for effectful programming have been renamed `*.Effectful`, with the originals being deprecated. ### Improvements to pretty printing and regexes @@ -158,10 +272,14 @@ Non-backwards compatible changes * Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice` which can be used to indicate meet/join-ness of the original structures. -#### Function hierarchy +#### Removal of the old function hierarchy * The switch to the new function hierarchy is complete and the following definitions now use the new definitions instead of the old ones: + * `Algebra.Lattice.Properties.BooleanAlgebra` + * `Algebra.Properties.CommutativeMonoid.Sum` + * `Algebra.Properties.Lattice` + * `replace-equality` * `Data.Fin.Properties` * `∀-cons-⇔` * `⊎⇔∃` @@ -180,6 +298,7 @@ Non-backwards compatible changes * `empty` * `Data.List.Fresh.Relation.Unary.Any` * `⊎⇔Any` + * `Data.List.NonEmpty` * `Data.List.Relation.Binary.Lex` * `[]<[]-⇔` * `∷<∷-⇔` @@ -191,6 +310,7 @@ Non-backwards compatible changes * `∷⁻¹` * `∷ʳ⁻¹` * `[x]⊆xs⤖x∈xs` + * `Data.List.Relation.Unary.Grouped.Properties` * `Data.Maybe.Relation.Binary.Connected` * `just-equivalence` * `Data.Maybe.Relation.Binary.Pointwise` @@ -203,6 +323,9 @@ Non-backwards compatible changes * `m%n≡0⇔n∣m` * `Data.Nat.Properties` * `eq?` + * `Data.Vec.N-ary` + * `uncurry-∀ⁿ` + * `uncurry-∃ⁿ` * `Data.Vec.Relation.Binary.Lex.Core` * `P⇔[]<[]` * `∷<∷-⇔` @@ -211,16 +334,52 @@ Non-backwards compatible changes * `Pointwise-≡↔≡` * `Data.Vec.Relation.Binary.Pointwise.Inductive` * `Pointwise-≡↔≡` + * `Effect.Monad.Partiality` + * `correct` * `Relation.Binary.Construct.Closure.Reflexive.Properties` * `⊎⇔Refl` * `Relation.Binary.Construct.Closure.Transitive` * `equivalent` + * `Relation.Binary.Reflection` + * `solve₁` * `Relation.Nullary.Decidable` * `map` -* The names of the fields in the records of the new hierarchy have been - changed from `f`, `g`, `cong₁`, `cong₂` to `to`, `from`, `to-cong`, `from-cong`. +#### Changes to the new function hierarchy + +* The names of the fields in `Function.Bundles` have been + changed from `f`, `g`, `cong₁` and `cong₂` to `to`, `from`, `to-cong`, `from-cong`. + +* The module `Function.Definitions` no longer has two equalities as module arguments, as + they did not interact as intended with the re-exports from `Function.Definitions.(Core1/Core2)`. + The latter have been removed and their definitions folded into `Function.Definitions`. + +* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective` + have been changed from: + ``` + Surjective f = ∀ y → ∃ λ x → f x ≈₂ y + Inverseˡ f g = ∀ y → f (g y) ≈₂ y + Inverseʳ f g = ∀ x → g (f x) ≈₁ x + ``` + to: + ``` + Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y + Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x + Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x + ``` + This is for several reasons: i) the new definitions compose much more easily, ii) Agda + can better infer the equalities used. + + To ease backwards compatibility: + - the old definitions have been moved to the new names `StrictlySurjective`, + `StrictlyInverseˡ` and `StrictlyInverseʳ`. + - The records in `Function.Structures` and `Function.Bundles` export proofs + of these under the names `strictlySurjective`, `strictlyInverseˡ` and + `strictlyInverseʳ`, + - Conversion functions have been added in both directions to + `Function.Consequences(.Propositional)`. + #### Proofs of non-zeroness/positivity/negativity as instance arguments * Many numeric operations in the library require their arguments to be non-zero, @@ -244,42 +403,42 @@ Non-backwards compatible changes `m / n` without having to explicitly provide a proof, as instance search will fill it in for you. The full list of such operations changed is as follows: - In `Data.Nat.DivMod`: `_/_`, `_%_`, `_div_`, `_mod_` - - In `Data.Nat.Pseudorandom.LCG`: `Generator` - - In `Data.Integer.DivMod`: `_divℕ_`, `_div_`, `_modℕ_`, `_mod_` - - In `Data.Rational`: `mkℚ+`, `normalize`, `_/_`, `1/_` - - In `Data.Rational.Unnormalised`: `_/_`, `1/_`, `_÷_` + - In `Data.Nat.Pseudorandom.LCG`: `Generator` + - In `Data.Integer.DivMod`: `_divℕ_`, `_div_`, `_modℕ_`, `_mod_` + - In `Data.Rational`: `mkℚ+`, `normalize`, `_/_`, `1/_` + - In `Data.Rational.Unnormalised`: `_/_`, `1/_`, `_÷_` * At the moment, there are 4 different ways such instance arguments can be provided, listed in order of convenience and clarity: 1. *Automatic basic instances* - the standard library provides instances based on the constructors of each - numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constains an instance of `NonZero (suc n)` for any `n` - and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. Consequently, - if the argument is of the required form, these instances will always be filled in by instance search - automatically, e.g. - ``` - 0/n≡0 : 0 / suc n ≡ 0 - ``` - 2. *Take the instance as an argument* - You can provide the instance argument as a parameter to your function - and Agda's instance search will automatically use it in the correct place without you having to - explicitly pass it, e.g. - ``` - 0/n≡0 : .{{_ : NonZero n}} → 0 / n ≡ 0 - ``` - 3. *Define the instance locally* - You can define an instance argument in scope (e.g. in a `where` clause) - and Agda's instance search will again find it automatically, e.g. - ``` - instance - n≢0 : NonZero n - n≢0 = ... - - 0/n≡0 : 0 / n ≡ 0 - ``` - 4. *Pass the instance argument explicitly* - Finally, if all else fails you can pass the - instance argument explicitly into the function using `{{ }}`, e.g. - ``` - 0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0 - ``` - Suitable constructors for `NonZero`/`Positive` etc. can be found in `Data.X.Base`. + numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constains an instance of `NonZero (suc n)` for any `n` + and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. Consequently, + if the argument is of the required form, these instances will always be filled in by instance search + automatically, e.g. + ``` + 0/n≡0 : 0 / suc n ≡ 0 + ``` + 2. *Take the instance as an argument* - You can provide the instance argument as a parameter to your function + and Agda's instance search will automatically use it in the correct place without you having to + explicitly pass it, e.g. + ``` + 0/n≡0 : .{{_ : NonZero n}} → 0 / n ≡ 0 + ``` + 3. *Define the instance locally* - You can define an instance argument in scope (e.g. in a `where` clause) + and Agda's instance search will again find it automatically, e.g. + ``` + instance + n≢0 : NonZero n + n≢0 = ... + + 0/n≡0 : 0 / n ≡ 0 + ``` + 4. *Pass the instance argument explicitly* - Finally, if all else fails you can pass the + instance argument explicitly into the function using `{{ }}`, e.g. + ``` + 0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0 + ``` + Suitable constructors for `NonZero`/`Positive` etc. can be found in `Data.X.Base`. * A full list of proofs that have changed to use instance arguments is available at the end of this file. Notable changes to proofs are now discussed below. @@ -306,6 +465,71 @@ Non-backwards compatible changes ∣↥p∣≢0⇒p≄0 : ∀ p → ℤ.∣ (↥ p) ∣ ≢0 → p ≠ 0ℚᵘ ``` +### Change in reduction behaviour of rationals + +* Currently arithmetic expressions involving rationals (both normalised and + unnormalised) undergo disastrous exponential normalisation. For example, + `p + q` would often be normalised by Agda to + `(↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)`. While the normalised form + of `p + q + r + s + t + u + v` would be ~700 lines long. This behaviour + often chokes both type-checking and the display of the expressions in the IDE. + +* To avoid this expansion and make non-trivial reasoning about rationals actually feasible: + 1. the records `ℚᵘ` and `ℚ` have both had the `no-eta-equality` flag enabled + 2. definition of arithmetic operations have trivial pattern matching added to + prevent them reducing, e.g. + ```agda + p + q = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q) + ``` + has been changed to + ``` + p@record{} + q@record{} = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q) + ``` + +* As a consequence of this, some proofs that relied on this reduction behaviour + or on eta-equality may no longer go through. There are several ways to fix this: + 1. The principled way is to not rely on this reduction behaviour in the first place. + The `Properties` files for rational numbers have been greatly expanded in `v1.7` + and `v2.0`, and we believe most proofs should be able to be built up from existing + proofs contained within these files. + 2. Alternatively, annotating any rational arguments to a proof with either + `@record{}` or `@(mkℚ _ _ _)` should restore the old reduction behaviour for any + terms involving those parameters. + 3. Finally, if the above approaches are not viable then you may be forced to explicitly + use `cong` combined with a lemma that proves the old reduction behaviour. + +### Change to the definition of `LeftCancellative` and `RightCancellative` + +* 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 + 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` + - To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z` + + - `RightCancellative _•_` + - From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z` + - To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z` + + - `AlmostLeftCancellative e _•_` + - From: `∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` + - To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` + + - `AlmostRightCancellative e _•_` + - From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` + - 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. + - `∙-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: @@ -424,8 +648,130 @@ Non-backwards compatible changes ↦ ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y ``` +### Reorganisation of the `Relation.Nullary` hierarchy + +* It was very difficult to use the `Relation.Nullary` modules, as `Relation.Nullary` + contained the basic definitions of negation, decidability etc., and the operations and + proofs were smeared over `Relation.Nullary.(Negation/Product/Sum/Implication etc.)`. + +* In order to fix this: + - the definition of `Dec` and `recompute` have been moved to `Relation.Nullary.Decidable.Core` + - the definition of `Reflects` has been moved to `Relation.Nullary.Reflects` + - the definition of `¬_` has been moved to `Relation.Nullary.Negation.Core` + +* Backwards compatibility has been maintained, as `Relation.Nullary` still re-exports these publicly. + +* The modules: + ``` + Relation.Nullary.Product + Relation.Nullary.Sum + Relation.Nullary.Implication + ``` + have been deprecated and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)` + however all their contents is re-exported by `Relation.Nullary` which is the easiest way to access + it now. + +* In order to facilitate this reorganisation the following breaking moves have occured: + - `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core` + - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`. + - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation` + to `Relation.Nullary.Decidable`. + - `fromDec` and `toDec` have been mvoed from `Data.Sum.Base` to `Data.Sum`. + +### Refactoring of the unindexed Functor/Applicative/Monad hiearchy + +* The unindexed versions are not defined in terms of the named versions anymore + +* The `RawApplicative` and `RawMonad` type classes have been relaxed so that the underlying + functors do not need their domain and codomain to live at the same Set level. + This is needed for level-increasing functors like `IO : Set l → Set (suc l)`. + +* `RawApplicative` is now `RawFunctor + pure + _<*>_` and `RawMonad` is now + `RawApplicative` + `_>>=_` and so `return` is not used anywhere anymore. + This fixes the conflict with `case_return_of` (#356) + This reorganisation means in particular that the functor/applicative of a monad + are not computed using `_>>=_`. This may break proofs. + +* We now have `RawEmpty` and `RawChoice` respectively packing `empty : M A` and + `(<|>) : M A → M A → M A`. `RawApplicativeZero`, `RawAlternative`, `RawMonadZero`, + `RawMonadPlus` are all defined in terms of these. + +* `MonadT T` now returns a `MonadTd` record that packs both a proof that the + `Monad M` transformed by `T` is a monad and that we can `lift` a computation + `M A` to a trasnformed computation `T M A`. + +* The monad transformer are not mere aliases anymore, they are record-wrapped + which allows constraints such as `MonadIO (StateT S (ReaderT R IO))` to be + discharged by instance arguments. + +* The mtl-style type classes (`MonadState`, `MonadReader`) do not contain a proof + that the underlying functor is a `Monad` anymore. This ensures we do not have + conflicting `Monad M` instances from a pair of `MonadState S M` & `MonadReader R M` + constraints. + +* `MonadState S M` is now defined in terms of + ```agda + gets : (S → A) → M A + modify : (S → S) → M ⊤ + ``` + with `get` and `put` defined as derived notions. + This is needed because `MonadState S M` does not pack a `Monad M` instance anymore + and so we cannot define `modify f` as `get >>= λ s → put (f s)`. + +* `MonadWriter 𝕎 M` is defined similarly: + ```agda + writer : W × A → M A + listen : M A → M (W × A) + pass : M ((W → W) × A) → M A + ``` + with `tell` defined as a derived notion. + Note that `𝕎` is a `RawMonoid`, not a `Set` and `W` is the carrier of the monoid. + +* New modules: + ``` + Algebra.Construct.Initial + Algebra.Construct.Terminal + Data.List.Effectful.Transformer + Data.List.NonEmpty.Effectful.Transformer + Data.Maybe.Effectful.Transformer + Data.Sum.Effectful.Left.Transformer + Data.Sum.Effectful.Right.Transformer + Data.Vec.Effectful.Transformer + Effect.Empty + Effect.Choice + Effect.Monad.Error.Transformer + Effect.Monad.Identity + Effect.Monad.IO + Effect.Monad.IO.Instances + Effect.Monad.Reader.Indexed + Effect.Monad.Reader.Instances + Effect.Monad.Reader.Transformer + Effect.Monad.Reader.Transformer.Base + Effect.Monad.State.Indexed + Effect.Monad.State.Instances + Effect.Monad.State.Transformer + Effect.Monad.State.Transformer.Base + Effect.Monad.Writer + Effect.Monad.Writer.Indexed + Effect.Monad.Writer.Instances + Effect.Monad.Writer.Transformer + Effect.Monad.Writer.Transformer.Base + IO.Effectful + IO.Instances + ``` + ### Other +* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used + the `--without-K` flag now use the `--cubical-compatible` flag instead. + +* To avoid _large indices_ that are by default no longer allowed in Agda 2.6.4, + universe levels have been increased in the following definitions: + - `Data.Star.Decoration.DecoratedWith` + - `Data.Star.Pointer.Pointer` + - `Reflection.AnnotatedAST.Typeₐ` + - `Reflection.AnnotatedAST.AnnotationFun` + * The first two arguments of `m≡n⇒m-n≡0` (now `i≡j⇒i-j≡0`) in `Data.Integer.Base` have been made implicit. @@ -467,6 +813,22 @@ Non-backwards compatible changes exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)` directly to use them. +* The names of the (in)equational reasoning combinators defined in the internal + modules `Data.Rational(.Unnormalised).Properties.≤-Reasoning` have been renamed + (issue #1437) to conform with the defined setoid equality `_≃_` on `Rational`s: + ```agda + step-≈ ↦ step-≃ + step-≃˘ ↦ step-≃˘ + ``` + with corresponding associated syntax: + ```agda + _≈⟨_⟩_ ↦ _≃⟨_⟩_ + _≈˘⟨_⟩_ ↦ _≃˘⟨_⟩_ + ``` + NB. It is not possible to rename or deprecate `syntax` declarations, so Agda will + only issue a "Could not parse the application `begin ...` when scope checking" + warning if the old combinators are used. + * The types of the proofs `pos⇒1/pos`/`1/pos⇒pos` and `neg⇒1/neg`/`1/neg⇒neg` in `Data.Rational(.Unnormalised).Properties` have been switched, as the previous naming scheme didn't correctly generalise to e.g. `pos+pos⇒pos`. For example @@ -494,12 +856,66 @@ Non-backwards compatible changes + `pigeonhole` has been strengthened: wlog, we return a proof that `i < j` rather than a mere `i ≢ j`. +* In `Data.Sum.Base` the definitions `fromDec` and `toDec` have been moved to `Data.Sum`. + * In `Codata.Guarded.Stream` the following functions have been modified to have simpler definitions: * `cycle` * `interleave⁺` * `cantor` Furthermore, the direction of interleaving of `cantor` has changed. Precisely, suppose `pair` is the cantor pairing function, then `lookup (pair i j) (cantor xss)` according to the old definition corresponds to `lookup (pair j i) (cantor xss)` according to the new definition. For a concrete example see the one included at the end of the module. +* Removed `m/n/o≡m/[n*o]` from `Data.Nat.Divisibility` and added a more general + `m/n/o≡m/[n*o]` to `Data.Nat.DivMod` that doesn't require `n * o ∣ m`. + +* Updated `lookup` functions (and variants) to match the conventions adopted in the + `List` module i.e. `lookup` takes its container first and the index (whose type may + depend on the container value) second. + This affects modules: + ``` + Codata.Guarded.Stream + Codata.Guarded.Stream.Relation.Binary.Pointwise + Codata.Musical.Colist.Base + Codata.Musical.Colist.Relation.Unary.Any.Properties + Codata.Musical.Covec + Codata.Musical.Stream + Codata.Sized.Colist + Codata.Sized.Covec + Codata.Sized.Stream + Data.Vec.Relation.Unary.All + Data.Star.Environment + Data.Star.Pointer + Data.Star.Vec + Data.Trie + Data.Trie.NonEmpty + Data.Tree.AVL + Data.Tree.AVL.Indexed + Data.Tree.AVL.Map + Data.Tree.AVL.NonEmpty + Data.Vec.Recursive + Tactic.RingSolver + Tactic.RingSolver.Core.NatSet + ``` + * Moved & renamed from `Data.Vec.Relation.Unary.All` + to `Data.Vec.Relation.Unary.All.Properties`: + ``` + lookup ↦ lookup⁺ + tabulate ↦ lookup⁻ + ``` + * Renamed in `Data.Vec.Relation.Unary.Linked.Properties` + and `Codata.Guarded.Stream.Relation.Binary.Pointwise`: + ``` + lookup ↦ lookup⁺ + ``` + * Added the following new definitions to `Data.Vec.Relation.Unary.All`: + ``` + lookupAny : All P xs → (i : Any Q xs) → (P ∩ Q) (Any.lookup i) + lookupWith : ∀[ P ⇒ Q ⇒ R ] → All P xs → (i : Any Q xs) → R (Any.lookup i) + lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x) + lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) + ``` + * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to + `¬¬-excluded-middle`. + Major improvements ------------------ @@ -507,13 +923,13 @@ Major improvements * The ring solver tactic has been greatly improved. In particular: 1. When the solver is used for concrete ring types, e.g. ℤ, the equality can now use - all the ring operations defined natively for that type, rather than having - to use the operations defined in `AlmostCommutativeRing`. For example - previously you could not use `Data.Integer.Base._*_` but instead had to - use `AlmostCommutativeRing._*_`. + all the ring operations defined natively for that type, rather than having + to use the operations defined in `AlmostCommutativeRing`. For example + previously you could not use `Data.Integer.Base._*_` but instead had to + use `AlmostCommutativeRing._*_`. 2. The solver now supports use of the subtraction operator `_-_` whenever it is defined immediately in terms of `_+_` and `-_`. This is the case for - `Data.Integer` and `Data.Rational`. + `Data.Integer` and `Data.Rational`. ### Moved `_%_` and `_/_` operators to `Data.Nat.Base` @@ -525,12 +941,46 @@ Major improvements for them still live in `Data.Nat.DivMod` (which also publicly re-exports them to provide backwards compatability). -* Beneficieries of this change include `Data.Rational.Unnormalised.Base` whose +* Beneficiaries of this change include `Data.Rational.Unnormalised.Base` whose dependencies are now significantly smaller. +### Moved raw bundles from Data.X.Properties to Data.X.Base + +* As mentioned by MatthewDaggitt in Issue #1755, Raw bundles defined in Data.X.Properties + should be defined in Data.X.Base as they don't require any properties. + * Moved raw bundles From `Data.Nat.Properties` to `Data.Nat.Base` + * Moved raw bundles From `Data.Nat.Binary.Properties` to `Data.Nat.Binary.Base` + * Moved raw bundles From `Data.Rational.Properties` to `Data.Rational.Base` + * Moved raw bundles From `Data.Rational.Unnormalised.Properties` to `Data.Rational.Unnormalised.Base` + +### Moved the definition of RawX from `Algebra.X.Bundles` to `Algebra.X.Bundles.Raw` + +* A new module `Algebra.Bundles.Raw` containing the definitions of the raw bundles + can be imported at much lower cost from `Data.X.Base`. + The following definitions have been moved: + * `RawMagma` + * `RawMonoid` + * `RawGroup` + * `RawNearSemiring` + * `RawSemiring` + * `RawRingWithoutOne` + * `RawRing` + * `RawQuasigroup` + * `RawLoop` +* A new module `Algebra.Lattice.Bundles.Raw` is also introduced. + * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module. + Deprecated modules ------------------ +### Moving `Relation.Binary.Construct.(Converse/Flip)` + +* The following files have been moved: + ```agda + Relation.Binary.Construct.Converse ↦ Relation.Binary.Construct.Flip.EqAndOrd + Relation.Binary.Construct.Flip ↦ Relation.Binary.Construct.Flip.Ord + ``` + ### Deprecation of old function hierarchy * The module `Function.Related` has been deprecated in favour of `Function.Related.Propositional` @@ -561,6 +1011,43 @@ Deprecated modules Algebra.Morphism.LatticeMonomorphism ↦ Algebra.Lattice.Morphism.LatticeMonomorphism ``` +### Moving `*.Catgeorical.*` files + +* As discussed above the following files have been moved: + ```agda + Codata.Sized.Colist.Categorical ↦ Codata.Sized.Colist.Effectful + Codata.Sized.Covec.Categorical ↦ Codata.Sized.Covec.Effectful + Codata.Sized.Delay.Categorical ↦ Codata.Sized.Delay.Effectful + Codata.Sized.Stream.Categorical ↦ Codata.Sized.Stream.Effectful + Data.List.Categorical ↦ Data.List.Effectful + Data.List.Categorical.Transformer ↦ Data.List.Effectful.Transformer + Data.List.NonEmpty.Categorical ↦ Data.List.NonEmpty.Effectful + Data.List.NonEmpty.Categorical.Transformer ↦ Data.List.NonEmpty.Effectful.Transformer + Data.Maybe.Categorical ↦ Data.Maybe.Effectful + Data.Maybe.Categorical.Transformer ↦ Data.Maybe.Effectful.Transformer + Data.Product.Categorical.Examples ↦ Data.Product.Effectful.Examples + Data.Product.Categorical.Left ↦ Data.Product.Effectful.Left + Data.Product.Categorical.Left.Base ↦ Data.Product.Effectful.Left.Base + Data.Product.Categorical.Right ↦ Data.Product.Effectful.Right + Data.Product.Categorical.Right.Base ↦ Data.Product.Effectful.Right.Base + Data.Sum.Categorical.Examples ↦ Data.Sum.Effectful.Examples + Data.Sum.Categorical.Left ↦ Data.Sum.Effectful.Left + Data.Sum.Categorical.Left.Transformer ↦ Data.Sum.Effectful.Left.Transformer + Data.Sum.Categorical.Right ↦ Data.Sum.Effectful.Right + Data.Sum.Categorical.Right.Transformer ↦ Data.Sum.Effectful.Right.Transformer + Data.These.Categorical.Examples ↦ Data.These.Effectful.Examples + Data.These.Categorical.Left ↦ Data.These.Effectful.Left + Data.These.Categorical.Left.Base ↦ Data.These.Effectful.Left.Base + Data.These.Categorical.Right ↦ Data.These.Effectful.Right + Data.These.Categorical.Right.Base ↦ Data.These.Effectful.Right.Base + Data.Vec.Categorical ↦ Data.Vec.Effectful + Data.Vec.Categorical.Transformer ↦ Data.Vec.Effectful.Transformer + Data.Vec.Recursive.Categorical ↦ Data.Vec.Recursive.Effectful + Function.Identity.Categorical ↦ Function.Identity.Effectful + IO.Categorical ↦ IO.Effectful + Reflection.TCM.Categorical ↦ Reflection.TCM.Effectful + ``` + ### Moving `Relation.Binary.Properties.XLattice` files * The following files have been moved: @@ -578,9 +1065,57 @@ Deprecated modules * The module `Data.Nat.Properties.Core` has been deprecated, and its one entry moved to `Data.Nat.Properties` +### Deprecation of `Data.Fin.Substitution.Example` + +* The module `Data.Fin.Substitution.Example` has been deprecated, and moved to `README.Data.Fin.Substitution.UntypedLambda` + Deprecated names ---------------- +* In `Algebra.Construct.Zero`: + ```agda + rawMagma ↦ Algebra.Construct.Terminal.rawMagma + magma ↦ Algebra.Construct.Terminal.magma + semigroup ↦ Algebra.Construct.Terminal.semigroup + band ↦ Algebra.Construct.Terminal.band + ``` + +* In `Codata.Guarded.Stream.Properties`: + ```agda + map-identity ↦ map-id + map-fusion ↦ map-∘ + ``` + +* In `Codata.Sized.Colist.Properties`: + ```agda + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + ``` + +* In `Codata.Sized.Covec.Properties`: + ```agda + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + ``` + +* In `Codata.Sized.Delay.Properties`: + ```agda + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + map-unfold-fusion ↦ map-unfold + ``` + +* In `Codata.Sized.M.Properties`: + ```agda + map-compose ↦ map-∘ + ``` + +* In `Codata.Sized.Stream.Properties`: + ```agda + map-identity ↦ map-id + map-map-fusion ↦ map-∘ + ``` + * In `Data.Fin.Base`: two new, hopefully more memorable, names `↑ˡ` `↑ʳ` for the 'left', resp. 'right' injection of a Fin m into a 'larger' type, `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the @@ -590,6 +1125,24 @@ Deprecated names raise ↦ _↑ʳ_ ``` + Issue #1726: the relation `_≺_` and its single constructor `_≻toℕ_` + have been deprecated in favour of their extensional equivalent `_<_` + but omitting the inversion principle which pattern matching on `_≻toℕ_` + would achieve; this instead is proxied by the property `Data.Fin.Properties.toℕ<`. + +* In `Data.Fin.Induction`: + ``` + ≺-Rec + ≺-wellFounded + ≺-recBuilder + ≺-rec + ``` + + As with Issue #1726 above: the deprecation of relation `_≺_` means that these definitions + associated with wf-recursion are deprecated in favour of their `_<_` counterparts. + But it's not quite sensible to say that these definiton should be *renamed* to *anything*, + least of all those counterparts... the type confusion would be intolerable. + * In `Data.Fin.Properties`: ``` toℕ-raise ↦ toℕ-↑ʳ @@ -600,6 +1153,9 @@ Deprecated names eq? ↦ inj⇒≟ ``` + Likewise under issue #1726: the properties `≺⇒<′` and `<′⇒≺` have been deprecated + in favour of their proxy counterparts `<⇒<′` and `<′⇒<`. + * In `Data.Fin.Permutation.Components`: ``` reverse ↦ Data.Fin.Base.opposite @@ -621,17 +1177,23 @@ Deprecated names been made consistent so that `m`, `n` always refer to naturals and `i` and `j` always refer to integers: ``` + ≤-steps ↦ i≤j⇒i≤k+j + ≤-step ↦ i≤j⇒i≤1+j + + ≤-steps-neg ↦ i≤j⇒i-k≤j + ≤-step-neg ↦ i≤j⇒pred[i]≤j + n≮n ↦ i≮i - ∣n∣≡0⇒n≡0 ↦ ∣i∣≡0⇒i≡0 - ∣-n∣≡∣n∣ ↦ ∣-i∣≡∣i∣ - 0≤n⇒+∣n∣≡n ↦ 0≤i⇒+∣i∣≡i - +∣n∣≡n⇒0≤n ↦ +∣i∣≡i⇒0≤i - +∣n∣≡n⊎+∣n∣≡-n ↦ +∣i∣≡i⊎+∣i∣≡-i - ∣m+n∣≤∣m∣+∣n∣ ↦ ∣i+j∣≤∣i∣+∣j∣ - ∣m-n∣≤∣m∣+∣n∣ ↦ ∣i-j∣≤∣i∣+∣j∣ - signₙ◃∣n∣≡n ↦ signᵢ◃∣i∣≡i + ∣n∣≡0⇒n≡0 ↦ ∣i∣≡0⇒i≡0 + ∣-n∣≡∣n∣ ↦ ∣-i∣≡∣i∣ + 0≤n⇒+∣n∣≡n ↦ 0≤i⇒+∣i∣≡i + +∣n∣≡n⇒0≤n ↦ +∣i∣≡i⇒0≤i + +∣n∣≡n⊎+∣n∣≡-n ↦ +∣i∣≡i⊎+∣i∣≡-i + ∣m+n∣≤∣m∣+∣n∣ ↦ ∣i+j∣≤∣i∣+∣j∣ + ∣m-n∣≤∣m∣+∣n∣ ↦ ∣i-j∣≤∣i∣+∣j∣ + signₙ◃∣n∣≡n ↦ signᵢ◃∣i∣≡i ◃-≡ ↦ ◃-cong - ∣m-n∣≡∣n-m∣ ↦ ∣i-j∣≡∣j-i∣ + ∣m-n∣≡∣n-m∣ ↦ ∣i-j∣≡∣j-i∣ m≡n⇒m-n≡0 ↦ i≡j⇒i-j≡0 m-n≡0⇒m≡n ↦ i-j≡0⇒i≡j m≤n⇒m-n≤0 ↦ i≤j⇒i-j≤0 @@ -644,7 +1206,7 @@ Deprecated names m-commute ↦ map-<∣> + +* In `Data.List.Relation.Binary.Subset.Propositional.Properties`: + ``` + map-with-∈⁺ ↦ mapWith∈⁺ + ``` + +* In `Data.List.Relation.Unary.Any.Properties`: + ``` + map-with-∈⁺ ↦ mapWith∈⁺ + map-with-∈⁻ ↦ mapWith∈⁻ + map-with-∈↔ ↦ mapWith∈↔ + ``` + * In `Data.Nat.Properties`: ``` suc[pred[n]]≡n ↦ suc-pred + ≤-step ↦ m≤n⇒m≤1+n + ≤-stepsˡ ↦ m≤n⇒m≤o+n + ≤-stepsʳ ↦ m≤n⇒m≤n+o + <-step ↦ m-idem : Idempotent _<∣>_ + ``` + * The module `Algebra` now publicly re-exports the contents of `Algebra.Structures.Biased`. @@ -955,10 +1767,21 @@ Other minor changes record RawLoop c ℓ : Set (suc (c ⊔ ℓ)) record Loop c ℓ : Set (suc (c ⊔ ℓ)) record RingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) + record IdempotentSemiring c ℓ : Set (suc (c ⊔ ℓ)) record KleeneAlgebra c ℓ : Set (suc (c ⊔ ℓ)) record RawRingWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) record Quasiring c ℓ : Set (suc (c ⊔ ℓ)) where record Nearring c ℓ : Set (suc (c ⊔ ℓ)) where + record IdempotentMagma c ℓ : Set (suc (c ⊔ ℓ)) + record AlternateMagma c ℓ : Set (suc (c ⊔ ℓ)) + record FlexibleMagma c ℓ : Set (suc (c ⊔ ℓ)) + record MedialMagma c ℓ : Set (suc (c ⊔ ℓ)) + record SemimedialMagma c ℓ : Set (suc (c ⊔ ℓ)) + record LeftBolLoop c ℓ : Set (suc (c ⊔ ℓ)) + record RightBolLoop c ℓ : Set (suc (c ⊔ ℓ)) + record MoufangLoop c ℓ : Set (suc (c ⊔ ℓ)) + record NonAssociativeRing c ℓ : Set (suc (c ⊔ ℓ)) + record MiddleBolLoop c ℓ : Set (suc (c ⊔ ℓ)) ``` and the existing record `Lattice` now provides ```agda @@ -967,8 +1790,45 @@ Other minor changes ``` and their corresponding algebraic subbundles. +* Added new proofs to `Algebra.Consequences.Base`: + ```agda + reflexive+selfInverse⇒involutive : Reflexive _≈_ → + SelfInverse _≈_ f → + Involutive _≈_ f + ``` + +* Added new proofs to `Algebra.Consequences.Propositional`: + ```agda + comm+assoc⇒middleFour : Commutative _•_ → + Associative _•_ → + _•_ MiddleFourExchange _•_ + identity+middleFour⇒assoc : Identity e _•_ → + _•_ MiddleFourExchange _•_ → + Associative _•_ + identity+middleFour⇒comm : Identity e _+_ → + _•_ MiddleFourExchange _+_ → + Commutative _•_ + ``` + * Added new proofs to `Algebra.Consequences.Setoid`: ```agda + comm+assoc⇒middleFour : Congruent₂ _•_ → Commutative _•_ → Associative _•_ → + _•_ MiddleFourExchange _•_ + identity+middleFour⇒assoc : Congruent₂ _•_ → Identity e _•_ → + _•_ MiddleFourExchange _•_ → + Associative _•_ + identity+middleFour⇒comm : Congruent₂ _•_ → Identity e _+_ → + _•_ MiddleFourExchange _+_ → + Commutative _•_ + + involutive⇒surjective : Involutive f → Surjective f + selfInverse⇒involutive : SelfInverse f → Involutive f + selfInverse⇒congruent : SelfInverse f → Congruent f + selfInverse⇒inverseᵇ : SelfInverse f → Inverseᵇ f f + selfInverse⇒surjective : SelfInverse f → Surjective f + selfInverse⇒injective : SelfInverse f → Injective f + selfInverse⇒bijective : SelfInverse f → Bijective f + comm+idˡ⇒id : Commutative _•_ → LeftIdentity e _•_ → Identity e _•_ comm+idʳ⇒id : Commutative _•_ → RightIdentity e _•_ → Identity e _•_ comm+zeˡ⇒ze : Commutative _•_ → LeftZero e _•_ → Zero e _•_ @@ -1004,12 +1864,30 @@ Other minor changes InvertibleUnitalMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂) loop : Loop a ℓ₁ → Loop b ℓ₂ → Loop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) - kleeneAlgebra : KleeneAlgebra a ℓ₁ → KleeneAlgebra b ℓ₂ → - KleeneAlgebra (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + idempotentSemiring : IdempotentSemiring a ℓ₁ → IdempotentSemiring b ℓ₂ → + IdempotentSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + idempotentMagma : IdempotentMagma a ℓ₁ → IdempotentMagma b ℓ₂ → + IdempotentMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + alternativeMagma : AlternativeMagma a ℓ₁ → AlternativeMagma b ℓ₂ → + AlternativeMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + flexibleMagma : FlexibleMagma a ℓ₁ → FlexibleMagma b ℓ₂ → + FlexibleMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + medialMagma : MedialMagma a ℓ₁ → MedialMagma b ℓ₂ → MedialMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + semimedialMagma : SemimedialMagma a ℓ₁ → SemimedialMagma b ℓ₂ → + SemimedialMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + kleeneAlgebra : KleeneAlgebra a ℓ₁ → KleeneAlgebra b ℓ₂ → KleeneAlgebra (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + leftBolLoop : LeftBolLoop a ℓ₁ → LeftBolLoop b ℓ₂ → LeftBolLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + rightBolLoop : RightBolLoop a ℓ₁ → RightBolLoop b ℓ₂ → RightBolLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + middleBolLoop : MiddleBolLoop a ℓ₁ → MiddleBolLoop b ℓ₂ → MiddleBolLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) + moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂) ``` * Added new definition to `Algebra.Definitions`: ```agda + _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _ + + SelfInverse : Op₁ A → Set _ + LeftDividesˡ : Op₂ A → Op₂ A → Set _ LeftDividesʳ : Op₂ A → Op₂ A → Set _ RightDividesˡ : Op₂ A → Op₂ A → Set _ @@ -1020,6 +1898,23 @@ Other minor changes LeftInvertible e _∙_ x = ∃[ x⁻¹ ] (x⁻¹ ∙ x) ≈ e RightInvertible e _∙_ x = ∃[ x⁻¹ ] (x ∙ x⁻¹) ≈ e Invertible e _∙_ x = ∃[ x⁻¹ ] ((x⁻¹ ∙ x) ≈ e) × ((x ∙ x⁻¹) ≈ e) + StarRightExpansive e _+_ _∙_ _⁻* = ∀ x → (e + (x ∙ (x ⁻*))) ≈ (x ⁻*) + StarLeftExpansive e _+_ _∙_ _⁻* = ∀ x → (e + ((x ⁻*) ∙ x)) ≈ (x ⁻*) + StarExpansive e _+_ _∙_ _* = (StarLeftExpansive e _+_ _∙_ _*) × (StarRightExpansive e _+_ _∙_ _*) + StarLeftDestructive _+_ _∙_ _* = ∀ a b x → (b + (a ∙ x)) ≈ x → ((a *) ∙ b) ≈ x + StarRightDestructive _+_ _∙_ _* = ∀ a b x → (b + (x ∙ a)) ≈ x → (b ∙ (a *)) ≈ x + StarDestructive _+_ _∙_ _* = (StarLeftDestructive _+_ _∙_ _*) × (StarRightDestructive _+_ _∙_ _*) + LeftAlternative _∙_ = ∀ x y → ((x ∙ x) ∙ y) ≈ (x ∙ (y ∙ y)) + RightAlternative _∙_ = ∀ x y → (x ∙ (y ∙ y)) ≈ ((x ∙ y) ∙ y) + Alternative _∙_ = (LeftAlternative _∙_ ) × (RightAlternative _∙_) + Flexible _∙_ = ∀ x y → ((x ∙ y) ∙ x) ≈ (x ∙ (y ∙ x)) + Medial _∙_ = ∀ x y u z → ((x ∙ y) ∙ (u ∙ z)) ≈ ((x ∙ u) ∙ (y ∙ z)) + LeftSemimedial _∙_ = ∀ x y z → ((x ∙ x) ∙ (y ∙ z)) ≈ ((x ∙ y) ∙ (x ∙ z)) + RightSemimedial _∙_ = ∀ x y z → ((y ∙ z) ∙ (x ∙ x)) ≈ ((y ∙ x) ∙ (z ∙ x)) + Semimedial _∙_ = (LeftSemimedial _∙_) × (RightSemimedial _∙_) + LeftBol _∙_ = ∀ x y z → (x ∙ (y ∙ (x ∙ z))) ≈ ((x ∙ (y ∙ z)) ∙ z ) + RightBol _∙_ = ∀ x y z → (((z ∙ x) ∙ y) ∙ x) ≈ (z ∙ ((x ∙ y) ∙ x)) + MiddleBol _∙_ _\\_ _//_ = ∀ x y z → (x ∙ ((y ∙ z) \\ x)) ≈ ((x // z) ∙ (y \\ x)) ``` * Added new functions to `Algebra.Definitions.RawSemiring`: @@ -1028,9 +1923,55 @@ Other minor changes _^ᵗ_ : A → ℕ → A ``` +* `Algebra.Properties.Magma.Divisibility` now re-exports operations + `_∣ˡ_`, `_∤ˡ_`, `_∣ʳ_`, `_∤ʳ_` from `Algebra.Definitions.Magma`. + * Added new proofs to `Algebra.Properties.CommutativeSemigroup`: - ``` + ```agda interchange : Interchangable _∙_ _∙_ + xy∙xx≈x∙yxx : ∀ x y → (x ∙ y) ∙ (x ∙ x) ≈ x ∙ (y ∙ (x ∙ x)) + leftSemimedial : LeftSemimedial _∙_ + rightSemimedial : RightSemimedial _∙_ + middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x) + semimedial : Semimedial _∙_ + ``` +* Added new proof to `Algebra.Properties.Monoid.Mult`: + ```agda + ×-congˡ : ∀ {x} → (_× x) Preserves _≡_ ⟶ _≈_ + ``` + +* Added new proof to `Algebra.Properties.Monoid.Sum`: + ```agda + sum-init-last : ∀ {n} (t : Vector _ (suc n)) → sum t ≈ sum (init t) + last t + ``` + +* Added new proofs to `Algebra.Properties.Semigroup`: + ```agda + leftAlternative : LeftAlternative _∙_ + rightAlternative : RightAlternative _∙_ + alternative : Alternative _∙_ + flexible : Flexible _∙_ + ``` + +* Added new proofs to `Algebra.Properties.Semiring.Exp`: + ```agda + ^-congʳ : (x ^_) Preserves _≡_ ⟶ _≈_ + y*x^m*y^n≈x^m*y^[n+1] : (x * y ≈ y * x) → y * (x ^ m * y ^ n) ≈ x ^ m * y ^ suc n + ``` + +* Added new proofs to `Algebra.Properties.Semiring.Mult`: + ```agda + 1×-identityʳ : 1 × x ≈ x + ×-comm-* : x * (n × y) ≈ n × (x * y) + ×-assoc-* : (n × x) * y ≈ n × (x * y) + ``` + +* Added new proofs to `Algebra.Properties.Ring`: + ```agda + -1*x≈-x : ∀ x → - 1# * x ≈ - x + x+x≈x⇒x≈0 : ∀ x → x + x ≈ x → x ≈ 0# + x[y-z]≈xy-xz : ∀ x y z → x * (y - z) ≈ x * y - x * z + [y-z]x≈yx-zx : ∀ x y z → (y - z) * x ≈ (y * x) - (z * x) ``` * Added new definitions to `Algebra.Structures`: @@ -1041,9 +1982,20 @@ Other minor changes record IsQuasigroup (∙ \\ // : Op₂ A) : Set (a ⊔ ℓ) record IsLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) record IsRingWithoutOne (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) - record IsKleeneAlgebra (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) + record IsIdempotentSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) + record IsKleeneAlgebra (+ * : Op₂ A) (⋆ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) record IsQuasiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where record IsNearring (+ * : Op₂ A) (0# 1# : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where + record IsIdempotentMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) + record IsAlternativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) + record IsFlexibleMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) + record IsMedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) + record IsSemimedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) + record IsLeftBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) + record IsRightBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) + record IsMoufangLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) + record IsNonAssociativeRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) + record IsMiddleBolLoop (∙ \\ // : Op₂ A) (ε : A) : Set (a ⊔ ℓ) ``` and the existing record `IsLattice` now provides ``` @@ -1065,16 +2017,32 @@ Other minor changes record IsRingWithoutOneIsoMorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) ``` -* Added new functions in `Category.Monad.State`: - ``` - runState : State s a → s → a × s - evalState : State s a → s → a - execState : State s a → s → s - ``` - * Added new proofs in `Data.Bool.Properties`: ```agda <-wellFounded : WellFounded _<_ + ∨-conicalˡ : LeftConical false _∨_ + ∨-conicalʳ : RightConical false _∨_ + ∨-conical : Conical false _∨_ + ∧-conicalˡ : LeftConical true _∧_ + ∧-conicalʳ : RightConical true _∧_ + ∧-conical : Conical true _∧_ + + true-xor : true xor x ≡ not x + xor-same : x xor x ≡ false + not-distribˡ-xor : not (x xor y) ≡ (not x) xor y + not-distribʳ-xor : not (x xor y) ≡ x xor (not y) + xor-assoc : Associative _xor_ + xor-comm : Commutative _xor_ + xor-identityˡ : LeftIdentity false _xor_ + xor-identityʳ : RightIdentity false _xor_ + xor-identity : Identity false _xor_ + xor-inverseˡ : LeftInverse true not _xor_ + xor-inverseʳ : RightInverse true not _xor_ + xor-inverse : Inverse true not _xor_ + ∧-distribˡ-xor : _∧_ DistributesOverˡ _xor_ + ∧-distribʳ-xor : _∧_ DistributesOverʳ _xor_ + ∧-distrib-xor : _∧_ DistributesOver _xor_ + xor-annihilates-not : (not x) xor (not y) ≡ x xor y ``` * Added new functions in `Data.Fin.Base`: @@ -1124,6 +2092,9 @@ Other minor changes toℕ-cancel-≤ : toℕ i ℕ.≤ toℕ j → i ≤ j toℕ-cancel-< : toℕ i ℕ.< toℕ j → i < j + splitAt⁻¹-↑ˡ : splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i + splitAt⁻¹-↑ʳ : splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i + toℕ-combine : toℕ (combine i j) ≡ k ℕ.* toℕ i ℕ.+ toℕ j combine-injectiveˡ : combine i j ≡ combine k l → i ≡ k combine-injectiveʳ : combine i j ≡ combine k l → j ≡ l @@ -1131,6 +2102,8 @@ Other minor changes combine-surjective : ∀ i → ∃₂ λ j k → combine j k ≡ i combine-monoˡ-< : i < j → combine i k < combine j l + ℕ-ℕ≡toℕ‿ℕ- : n ℕ-ℕ i ≡ toℕ (n ℕ- i) + lower₁-injective : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j pinch-injective : suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k @@ -1140,44 +2113,43 @@ 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 ``` * Changed the fixity of `Data.Fin.Substitution.TermSubst._/Var_`. + ```agda + infix 8 ↦ infixl 8 + ``` * Added new lemmas in `Data.Fin.Substitution.Lemmas.TermLemmas`: ``` - map-var≡ : - ∀ {m n} {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → - (∀ x → lookup ρ₁ x ≡ f x) → - (∀ x → lookup ρ₂ x ≡ T.var (f x)) → - map T.var ρ₁ ≡ ρ₂ - wk≡wk : - ∀ {n} → map T.var VarSubst.wk ≡ T.wk {n = n} - id≡id : - ∀ {n} → map T.var VarSubst.id ≡ T.id {n = n} - sub≡sub : - ∀ {n} {x : Fin n} → - map T.var (VarSubst.sub x) ≡ T.sub (T.var x) - ↑≡↑ : - ∀ {m n} {ρ : Sub Fin m n} → - map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ - /Var≡/ : - ∀ {m n} {ρ : Sub Fin m n} {t} → - t /Var ρ ≡ t T./ map T.var ρ - sub-renaming-commutes : - ∀ {m n t x} {ρ : Sub T m n} → - t /Var VarSubst.sub x T./ ρ ≡ - t T./ ρ T.↑ T./ T.sub (lookup ρ x) - sub-commutes-with-renaming : - ∀ {m n} {t t′} {ρ : Sub Fin m n} → - t T./ T.sub t′ /Var ρ ≡ - t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) + map-var≡ : {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → + (∀ x → lookup ρ₁ x ≡ f x) → + (∀ x → lookup ρ₂ x ≡ T.var (f x)) → + map T.var ρ₁ ≡ ρ₂ + wk≡wk : map T.var VarSubst.wk ≡ T.wk {n = n} + id≡id : map T.var VarSubst.id ≡ T.id {n = n} + sub≡sub : {x : Fin n} → map T.var (VarSubst.sub x) ≡ T.sub (T.var x) + ↑≡↑ : {ρ : Sub Fin m n} → map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ + /Var≡/ : {ρ : Sub Fin m n} {t} → t /Var ρ ≡ t T./ map T.var ρ + sub-renaming-commutes : {ρ : Sub T m n} → + t /Var VarSubst.sub x T./ ρ ≡ t T./ ρ T.↑ T./ T.sub (lookup ρ x) + sub-commutes-with-renaming : {ρ : Sub Fin m n} → + t T./ T.sub t′ /Var ρ ≡ t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) ``` * Added new functions in `Data.Integer.Base`: ``` _^_ : ℤ → ℕ → ℤ - ``` + + +-0-rawGroup : Rawgroup 0ℓ 0ℓ + + *-rawMagma : RawMagma 0ℓ 0ℓ + *-1-rawMonoid : RawMonoid 0ℓ 0ℓ + ``` * Added new proofs in `Data.Integer.Properties`: ```agda @@ -1192,13 +2164,18 @@ Other minor changes ^-*-assoc : (i ^ m) ^ n ≡ i ^ (m ℕ.* n) ^-distribˡ-+-* : i ^ (m ℕ.+ n) ≡ i ^ m * i ^ n - *-rawMagma : RawMagma 0ℓ 0ℓ - *-1-rawMonoid : RawMonoid 0ℓ 0ℓ - ^-isMagmaHomomorphism : IsMagmaHomomorphism ℕ.+-rawMagma *-rawMagma (i ^_) ^-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid *-1-rawMonoid (i ^_) ``` +* Added new proofs in `Data.Integer.GCD`: + ```agda + gcd-assoc : Associative gcd + gcd-zeroˡ : LeftZero 1ℤ gcd + gcd-zeroʳ : RightZero 1ℤ gcd + gcd-zero : Zero 1ℤ gcd + ``` + * Added new functions in `Data.List`: ```agda takeWhileᵇ : (A → Bool) → List A → List A @@ -1213,11 +2190,25 @@ Other minor changes deduplicateᵇ : (A → A → Bool) → List A → List A ``` +* Added new functions and definitions to `Data.List.Base`: + ```agda + catMaybes : List (Maybe A) → List A + ap : List (A → B) → List A → List B + ++-rawMagma : Set a → RawMagma a _ + ++-[]-rawMonoid : Set a → RawMonoid a _ + ``` + * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`: ```agda xs≮[] : ¬ xs < [] ``` +* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`: + ```agda + Any-resp-[σ⁻¹∘σ] : (σ : xs ↭ ys) → (ix : Any P xs) → Any-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix + ∈-resp-[σ⁻¹∘σ] : (σ : xs ↭ ys) → (ix : x ∈ xs) → ∈-resp-↭ (trans σ (↭-sym σ)) ix ≡ ix + ``` + * Added new functions in `Data.List.Relation.Unary.All`: ``` decide : Π[ P ∪ Q ] → Π[ All P ∪ Any Q ] @@ -1228,10 +2219,47 @@ Other minor changes decide : Π[ P ∪ Q ] → Π[ All {R = R} P ∪ Any Q ] ``` +* Added new proofs to `Data.List.Membership.Propositional.Properties`: + ```agda + mapWith∈-id : mapWith∈ xs (λ {x} _ → x) ≡ xs + map-mapWith∈ : map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f) + ``` + +* Added new proofs to `Data.List.Membership.Setoid.Properties`: + ```agda + mapWith∈-id : mapWith∈ xs (λ {x} _ → x) ≡ xs + map-mapWith∈ : map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f) + index-injective : index x₁∈xs ≡ index x₂∈xs → x₁ ≈ x₂ + ``` + * Add new proofs in `Data.List.Properties`: ```agda ∈⇒∣product : n ∈ ns → n ∣ product ns ∷ʳ-++ : xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys + + concatMap-cong : f ≗ g → concatMap f ≗ concatMap g + concatMap-pure : concatMap [_] ≗ id + concatMap-map : concatMap g (map f xs) ≡ concatMap (g ∘′ f) xs + map-concatMap : map f ∘′ concatMap g ≗ concatMap (map f ∘′ g) + + length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length + length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length + + take-map : take n (map f xs) ≡ map f (take n xs) + drop-map : drop n (map f xs) ≡ map f (drop n xs) + head-map : head (map f xs) ≡ Maybe.map f (head xs) + + take-suc : (o : Fin (length xs)) → let m = toℕ o in take (suc m) xs ≡ take m xs ∷ʳ lookup xs o + take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o + drop-take-suc : (o : Fin (length xs)) → let m = toℕ o in drop m (take (suc m) xs) ≡ [ lookup xs o ] + drop-take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in drop m (take (suc m) (tabulate f)) ≡ [ f o ] + + take-all : n ≥ length xs → take n xs ≡ xs + + take-[] : ∀ m → take m [] ≡ [] + drop-[] : ∀ m → drop m [] ≡ [] + + map-replicate : map f (replicate n x) ≡ replicate n (f x) ``` * Added new patterns and definitions to `Data.Nat.Base`: @@ -1241,8 +2269,34 @@ Other minor changes pattern <′-base = ≤′-refl pattern <′-step {n} m<′n = ≤′-step {n} m<′n + + _⊔′_ : ℕ → ℕ → ℕ + _⊓′_ : ℕ → ℕ → ℕ + ∣_-_∣′ : ℕ → ℕ → ℕ + _! : ℕ → ℕ + + parity : ℕ → Parity + + +-rawMagma : RawMagma 0ℓ 0ℓ + +-0-rawMonoid : RawMonoid 0ℓ 0ℓ + *-rawMagma : RawMagma 0ℓ 0ℓ + *-1-rawMonoid : RawMonoid 0ℓ 0ℓ + +-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ + +-*-rawSemiring : RawSemiring 0ℓ 0ℓ + ``` + +* Added a new proof to `Data.Nat.Binary.Properties`: + ```agda + suc-injective : Injective _≡_ _≡_ suc + toℕ-inverseˡ : Inverseˡ _≡_ _≡_ toℕ fromℕ + toℕ-inverseʳ : Inverseʳ _≡_ _≡_ toℕ fromℕ + toℕ-inverseᵇ : Inverseᵇ _≡_ _≡_ toℕ fromℕ ``` +* Added a new pattern synonym to `Data.Nat.Divisibility.Core`: + ```agda + pattern divides-refl q = divides q refl + ``` * Added new definitions and proofs to `Data.Nat.Primality`: ```agda @@ -1277,23 +2331,82 @@ Other minor changes <⇒<′ : m < n → m <′ n <′⇒< : m <′ n → m < n + m+n≤p⇒m≤p∸n : m + n ≤ p → m ≤ p ∸ n + m≤p∸n⇒m+n≤p : n ≤ p → m ≤ p ∸ n → m + n ≤ p + 1≤n! : 1 ≤ n ! _!≢0 : NonZero (n !) _!*_!≢0 : NonZero (m ! * n !) anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n) allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n) + + n≤1⇒n≡0∨n≡1 : n ≤ 1 → n ≡ 0 ⊎ n ≡ 1 + + m^n>0 : ∀ m .{{_ : NonZero m}} n → m ^ n > 0 + + ^-monoˡ-≤ : ∀ n → (_^ n) Preserves _≤_ ⟶ _≤_ + ^-monoʳ-≤ : ∀ m .{{_ : NonZero m}} → (m ^_) Preserves _≤_ ⟶ _≤_ + ^-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_^ n) Preserves _<_ ⟶ _<_ + ^-monoʳ-< : ∀ m → 1 < m → (m ^_) Preserves _<_ ⟶ _<_ + + n≡⌊n+n/2⌋ : n ≡ ⌊ n + n /2⌋ + n≡⌈n+n/2⌉ : n ≡ ⌈ n + n /2⌉ + + m-connex : Connex _≥_ _>_ + <-≤-connex : Connex _<_ _≤_ + >-≥-connex : Connex _>_ _≥_ + <-cmp : Trichotomous _≡_ _<_ + anyUpTo? : (P? : Decidable P) → ∀ v → Dec (∃ λ n → n < v × P n) + allUpTo? : (P? : Decidable P) → ∀ v → Dec (∀ {n} → n < v → P n) + ``` + +* Added new proofs in `Data.Nat.Combinatorics`: + ```agda + [n-k]*[n-k-1]!≡[n-k]! : k < n → (n ∸ k) * (n ∸ suc k) ! ≡ (n ∸ k) ! + [n-k]*d[k+1]≡[k+1]*d[k] : k < n → (n ∸ k) * ((suc k) ! * (n ∸ suc k) !) ≡ (suc k) * (k ! * (n ∸ k) !) + k![n∸k]!∣n! : k ≤ n → k ! * (n ∸ k) ! ∣ n ! + nP1≡n : n P 1 ≡ n + nC1≡n : n C 1 ≡ n + nCk+nC[k+1]≡[n+1]C[k+1] : n C k + n C (suc k) ≡ suc n C suc k ``` * Added new proofs in `Data.Nat.DivMod`: ```agda - m%n≤n : .{{_ : NonZero n}} → m % n ≤ n + m%n≤n : .{{_ : NonZero n}} → m % n ≤ n m*n/m!≡n/[m∸1]! : .{{_ : NonZero m}} → m * n / m ! ≡ n / (pred m) ! + + %-congˡ : .⦃ _ : NonZero o ⦄ → m ≡ n → m % o ≡ n % o + %-congʳ : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ≡ n → o % m ≡ o % n + m≤n⇒[n∸m]%m≡n%m : .⦃ _ : NonZero m ⦄ → m ≤ n → (n ∸ m) % m ≡ n % m + m*n≤o⇒[o∸m*n]%n≡o%n : .⦃ _ : NonZero n ⦄ → m * n ≤ o → (o ∸ m * n) % n ≡ o % n + m∣n⇒o%n%m≡o%m : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ∣ n → o % n % m ≡ o % m + m?_ : Decidable _>_ + +-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ +-*-rawSemiring : RawSemiring 0ℓ 0ℓ toℚᵘ-isNearSemiringHomomorphism-+-* : IsNearSemiringHomomorphism +-*-rawNearSemiring ℚᵘ.+-*-rawNearSemiring toℚᵘ @@ -1345,6 +2486,9 @@ Other minor changes ≰⇒≥ : _≰_ ⇒ _≥_ + _≥?_ : Decidable _≥_ + _>?_ : Decidable _>_ + *-mono-≤-nonNeg : .{{_ : NonNegative p}} .{{_ : NonNegative r}} → p ≤ q → r ≤ s → p * r ≤ q * s *-mono-<-nonNeg : .{{_ : NonNegative p}} .{{_ : NonNegative r}} → p < q → r < s → p * r < q * s 1/-antimono-≤-pos : .{{_ : Positive p}} .{{_ : Positive q}} → p ≤ q → 1/ q ≤ 1/ p @@ -1362,6 +2506,12 @@ Other minor changes 1/nonZero⇒nonZero : .{{_ : NonZero p}} → NonZero (1/ p) ``` +* Added new functions to `Data.Product.Nary.NonDependent`: + ```agda + zipWith : (∀ k → Projₙ as k → Projₙ bs k → Projₙ cs k) → + Product n as → Product n bs → Product n cs + ``` + * Added new proof to `Data.Product.Properties`: ```agda map-cong : f ≗ g → h ≗ i → map f h ≗ map g i @@ -1376,6 +2526,23 @@ Other minor changes ×-≡,≡←≡ : p₁ ≡ p₂ → (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ``` +* Added new proof to `Data.Product.Relation.Binary.Lex.Strict` + ```agda + ×-respectsʳ : Transitive _≈₁_ → + _<₁_ Respectsʳ _≈₁_ → _<₂_ Respectsʳ _≈₂_ → _<ₗₑₓ_ Respectsʳ _≋_ + ×-respectsˡ : Symmetric _≈₁_ → Transitive _≈₁_ → + _<₁_ Respectsˡ _≈₁_ → _<₂_ Respectsˡ _≈₂_ → _<ₗₑₓ_ Respectsˡ _≋_ + ×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ → _<₁_ Respectsʳ _≈₁_ → + WellFounded _<₁_ → WellFounded _<₂_ → WellFounded _<ₗₑₓ_ + ``` + +* Added new definitions to `Data.Sign.Base`: + ```agda + *-rawMagma : RawMagma 0ℓ 0ℓ + *-1-rawMonoid : RawMonoid 0ℓ 0ℓ + *-1-rawGroup : RawGroup 0ℓ 0ℓ + ``` + * Added new proofs to `Data.Sign.Properties`: ```agda *-inverse : Inverse + id _*_ @@ -1387,6 +2554,7 @@ Other minor changes *-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ *-group : Group 0ℓ 0ℓ *-abelianGroup : AbelianGroup 0ℓ 0ℓ + ≡-isDecEquivalence : IsDecEquivalence _≡_ ``` * Added new functions in `Data.String.Base`: @@ -1413,6 +2581,8 @@ Other minor changes map f (map g h) ∘ assocʳ ≗ assocʳ ∘ map (map f g) h ``` +* Made `Map` public in `Data.Tree.AVL.IndexedMap` + * Added new definitions in `Data.Vec.Base`: ```agda truncate : m ≤ n → Vec A n → Vec A m @@ -1429,7 +2599,11 @@ Other minor changes diagonal : Vec (Vec A n) n → Vec A n DiagonalBind._>>=_ : Vec A n → (A → Vec B n) → Vec B n + join : Vec (Vec A n) n → Vec A 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`: @@ -1454,8 +2628,13 @@ Other minor changes map-∷ʳ : map f (xs ∷ʳ x) ≡ (map f xs) ∷ʳ (f x) map-reverse : map f (reverse xs) ≡ reverse (map f xs) map-ʳ++ : map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys + map-insert : map f (insert xs i x) ≡ insert (map f xs) i (f x) + toList-map : toList (map f xs) ≡ List.map f (toList xs) + + lookup-concat : lookup (concat xss) (combine i j) ≡ lookup (lookup xss i) j ⊛-is->>= : fs ⊛ xs ≡ fs >>= flip map xs + lookup-⊛* : lookup (fs ⊛* xs) (combine i j) ≡ (lookup fs i $ lookup xs j) ++-is-foldr : xs ++ ys ≡ foldr ((Vec A) ∘ (_+ n)) _∷_ ys xs []≔-++-↑ʳ : (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y) unfold-ʳ++ : xs ʳ++ ys ≡ reverse xs ++ ys @@ -1485,11 +2664,46 @@ Other minor changes reverse-injective : reverse xs ≡ reverse ys → xs ≡ ys transpose-replicate : transpose (replicate xs) ≡ map replicate xs + toList-replicate : toList (replicate {n = n} a) ≡ List.replicate n a + + toList-++ : toList (xs ++ ys) ≡ toList xs List.++ toList ys + + 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 + + zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys' + ``` + +* Added new proofs in `Data.Vec.Membership.Propositional.Properties`: + ```agda + index-∈-fromList⁺ : Any.index (∈-fromList⁺ v∈xs) ≡ indexₗ v∈xs + ``` + +* Added new proofs in `Data.Vec.Functional.Properties`: + ``` + map-updateAt : f ∘ g ≗ h ∘ f → map f (updateAt i g xs) ≗ updateAt i h (map f xs) ``` * Added new proofs in `Data.Vec.Relation.Binary.Lex.Strict`: ```agda xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < [] + <-respectsˡ : IsPartialEquivalence _≈_ → _≺_ Respectsˡ _≈_ → + ∀ {m n} → _Respectsˡ_ (_<_ {m} {n}) _≋_ + <-respectsʳ : IsPartialEquivalence _≈_ → _≺_ Respectsʳ _≈_ → + ∀ {m n} → _Respectsʳ_ (_<_ {m} {n}) _≋_ + <-wellFounded : Symmetric _≈_ → Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ → + ∀ {n} → WellFounded (_<_ {n}) +``` + +* Added new functions in `Data.Vec.Relation.Unary.Any`: + ``` + lookup : Any P xs → A ``` * Added new functions in `Data.Vec.Relation.Unary.All`: @@ -1502,6 +2716,13 @@ Other minor changes ++-assoc : (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs) ``` +* Added new functions in `Effect.Monad.State`: + ``` + runState : State s a → s → a × s + evalState : State s a → s → a + execState : State s a → s → s + ``` + * Added new proofs in `Function.Construct.Symmetry`: ``` bijective : Bijective ≈₁ ≈₂ f → Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹ @@ -1545,6 +2766,7 @@ Other minor changes whenJust : Maybe A → (A → IO ⊤) → IO ⊤ untilJust : IO (Maybe A) → IO A + untilRight : (A → IO (A ⊎ B)) → A → IO B ``` * Added new functions in `Reflection.AST.Term`: @@ -1575,10 +2797,18 @@ Other minor changes * Added new proofs to `Relation.Binary.Lattice.Properties.{Join,Meet}Semilattice`: ```agda + isPosemigroup : IsPosemigroup _≈_ _≤_ _∨_ + posemigroup : Posemigroup c ℓ₁ ℓ₂ ≈-dec⇒≤-dec : Decidable _≈_ → Decidable _≤_ ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_ ``` +* Added new proofs to `Relation.Binary.Lattice.Properties.Bounded{Join,Meet}Semilattice`: + ```agda + isCommutativePomonoid : IsCommutativePomonoid _≈_ _≤_ _∨_ ⊥ + commutativePomonoid : CommutativePomonoid c ℓ₁ ℓ₂ + ``` + * Added new proofs to `Relation.Binary.Properties.Poset`: ```agda ≤-dec⇒≈-dec : Decidable _≤_ → Decidable _≈_ @@ -1675,6 +2905,14 @@ Other minor changes ``` Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y) Tight _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y) + + Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_ + Antitonic₁ _≤_ _⊑_ f = f Preserves (flip _≤_) ⟶ _⊑_ + Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_ + MonotonicAntitonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ (flip _⊑_) ⟶ _≼_ + AntitonicMonotonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ _⊑_ ⟶ _≼_ + Antitonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ (flip _⊑_) ⟶ _≼_ + Adjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y) ``` * Added new definitions in `Relation.Binary.Bundles`: @@ -1692,6 +2930,9 @@ Other minor changes sym⇒¬-sym : Symmetric _∼_ → Symmetric _≁_ cotrans⇒¬-trans : Cotransitive _∼_ → Transitive _≁_ irrefl⇒¬-refl : Reflexive _≈_ → Irreflexive _≈_ _∼_ → Reflexive _≁_ + mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → + f Preserves₂ ≤₁ ⟶ ≤₁ ⟶ ≤₂ → + f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂ ``` * Added new operations in `Relation.Binary.PropositionalEquality.Properties`: @@ -1727,6 +2968,50 @@ Other minor changes lookup-transpose⁺ : ∀ n (ass : List⁺ (Stream A)) → lookup n (transpose⁺ ass) ≡ List⁺.map (lookup n) ass ``` +* Added new corollaries in `Data.List.Membership.Setoid.Properties`: + ``` + ∈-++⁺∘++⁻ : ∀ {v} xs {ys} (p : v ∈ xs ++ ys) → [ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]′ (∈-++⁻ xs p) ≡ p + ∈-++⁻∘++⁺ : ∀ {v} xs {ys} (p : v ∈ xs ⊎ v ∈ ys) → ∈-++⁻ xs ([ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]′ p) ≡ p + ∈-++↔ : ∀ {v xs ys} → (v ∈ xs ⊎ v ∈ ys) ↔ v ∈ xs ++ ys + ∈-++-comm : ∀ {v} xs ys → v ∈ xs ++ ys → v ∈ ys ++ xs + ∈-++-comm∘++-comm : ∀ {v} xs {ys} (p : v ∈ xs ++ ys) → ∈-++-comm ys xs (∈-++-comm xs ys p) ≡ p + ∈-++↔++ : ∀ {v} xs ys → v ∈ xs ++ ys ↔ v ∈ ys ++ xs + ``` + +* Exposed container combinator conversion functions from `Data.Container.Combinator.Properties` separate from their correctness proofs in `Data.Container.Combinator`: + ``` + to-id : F.id A → ⟦ id ⟧ A + from-id : ⟦ id ⟧ A → F.id A + to-const : (A : Set s) → A → ⟦ const A ⟧ B + from-const : (A : Set s) → ⟦ const A ⟧ B → A + to-∘ : (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A) → ⟦ C₁ ∘ C₂ ⟧ A + from-∘ : (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) → ⟦ C₁ ∘ C₂ ⟧ A → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A) + to-× : (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) → ⟦ C₁ ⟧ A P.× ⟦ C₂ ⟧ A → ⟦ C₁ × C₂ ⟧ A + from-× : (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) → ⟦ C₁ × C₂ ⟧ A → ⟦ C₁ ⟧ A P.× ⟦ C₂ ⟧ A + to-Π : (I : Set i) (Cᵢ : I → Container s p) → (∀ i → ⟦ Cᵢ i ⟧ A) → ⟦ Π I Cᵢ ⟧ A + from-Π : (I : Set i) (Cᵢ : I → Container s p) → ⟦ Π I Cᵢ ⟧ A → ∀ i → ⟦ Cᵢ i ⟧ A + to-⊎ : (C₁ : Container s₁ p) (C₂ : Container s₂ p) → ⟦ C₁ ⟧ A S.⊎ ⟦ C₂ ⟧ A → ⟦ C₁ ⊎ C₂ ⟧ A + from-⊎ : (C₁ : Container s₁ p) (C₂ : Container s₂ p) → ⟦ C₁ ⊎ C₂ ⟧ A → ⟦ C₁ ⟧ A S.⊎ ⟦ C₂ ⟧ A + to-Σ : (I : Set i) (C : I → Container s p) → (∃ λ i → ⟦ C i ⟧ A) → ⟦ Σ I C ⟧ A + from-Σ : (I : Set i) (C : I → Container s p) → ⟦ Σ I C ⟧ A → ∃ λ i → ⟦ C i ⟧ A + ``` + +* Added a non-dependent version of `Function.Base.flip` due to an issue noted in + Pull Request #1812: + ```agda + flip′ : (A → B → C) → (B → A → C) + ``` + +* Added new proofs to `Data.List.Properties` + ```agda + cartesianProductWith-zeroˡ : cartesianProductWith f [] ys ≡ [] + cartesianProductWith-zeroʳ : cartesianProductWith f xs [] ≡ [] + cartesianProductWith-distribʳ-++ : cartesianProductWith f (xs ++ ys) zs ≡ + cartesianProductWith f xs zs ++ cartesianProductWith f ys zs + foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs + foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs + ``` + NonZero/Positive/Negative changes --------------------------------- @@ -1971,4 +3256,125 @@ This is a full list of proofs that have changed form to use irrelevant instance ```agda Inverse⇒Injection : Inverse S T → Injection S T ↔⇒↣ : A ↔ B → A ↣ B - ``` \ No newline at end of file + ``` + +* Added a new isomorphism to `Data.Fin.Properties`: + ```agda + 2↔Bool : Fin 2 ↔ Bool + ``` + +* Added new isomorphisms to `Data.Unit.Polymorphic.Properties`: + ```agda + ⊤↔⊤* : ⊤ {ℓ} ↔ ⊤* + ``` + +* Added new isomorphisms to `Data.Vec.N-ary`: + ```agda + Vec↔N-ary : ∀ n → (Vec A n → B) ↔ N-ary n A B + ``` + +* Added new isomorphisms to `Data.Vec.Recursive`: + ```agda + lift↔ : ∀ n → A ↔ B → A ^ n ↔ B ^ n + Fin[m^n]↔Fin[m]^n : ∀ m n → Fin (m ^ n) ↔ Fin m Vec.^ n + ``` + +* Added new functions to `Function.Properties.Inverse`: + ```agda + ↔-refl : Reflexive _↔_ + ↔-sym : Symmetric _↔_ + ↔-trans : Transitive _↔_ + ``` + +* Added new isomorphisms to `Function.Properties.Inverse`: + ```agda + ↔-fun : A ↔ B → C ↔ D → (A → C) ↔ (B → D) + ``` + +* Added new function to `Data.Fin.Properties` + ```agda + i≤inject₁[j]⇒i≤1+j : i ≤ inject₁ j → i ≤ suc j + ``` + +* Added new function to `Data.Fin.Induction` + ```agda + <-weakInduction-startingFrom : P i → (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j + ``` + +* Added new module to `Data.Rational.Unnormalised.Properties` + ```agda + module ≃-Reasoning = SetoidReasoning ≃-setoid + ``` + +* Added new functions to `Data.Rational.Unnormalised.Properties` + ```agda + 0≠1 : 0ℚᵘ ≠ 1ℚᵘ + ≃-≠-irreflexive : Irreflexive _≃_ _≠_ + ≠-symmetric : Symmetric _≠_ + ≠-cotransitive : Cotransitive _≠_ + ≠⇒invertible : p ≠ q → Invertible _≃_ 1ℚᵘ _*_ (p - q) + ``` + +* Added new structures to `Data.Rational.Unnormalised.Properties` + ```agda + +-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ + +-*-isHeytingField : IsHeytingField _≃_ _≠_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ + ``` + +* Added new bundles to `Data.Rational.Unnormalised.Properties` + ```agda + +-*-heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ + +-*-heytingField : HeytingField 0ℓ 0ℓ 0ℓ + ``` + +* Added new function to `Data.Vec.Relation.Binary.Pointwise.Inductive` + ```agda + cong-[_]≔ : Pointwise _∼_ xs ys → Pointwise _∼_ (xs [ i ]≔ p) (ys [ i ]≔ p) + ``` + +* Added new function to `Data.Vec.Relation.Binary.Equality.Setoid` + ```agda + map-[]≔ : map f (xs [ i ]≔ p) ≋ map f xs [ i ]≔ f p + ``` + +* Added new function to `Data.List.Relation.Binary.Permutation.Propositional.Properties` + ```agda + ↭-reverse : (xs : List A) → reverse xs ↭ xs + ``` + +* Added new functions to `Algebra.Properties.CommutativeMonoid` + ```agda + invertibleˡ⇒invertibleʳ : LeftInvertible _≈_ 0# _+_ x → RightInvertible _≈_ 0# _+_ x + invertibleʳ⇒invertibleˡ : RightInvertible _≈_ 0# _+_ x → LeftInvertible _≈_ 0# _+_ x + invertibleˡ⇒invertible : LeftInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x + invertibleʳ⇒invertible : RightInvertible _≈_ 0# _+_ x → Invertible _≈_ 0# _+_ x + ``` + +* Added new functions to `Algebra.Apartness.Bundles` + ```agda + invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y + invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y + x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0# + #-sym : Symmetric _#_ + #-congʳ : x ≈ y → x # z → y # z + #-congˡ : y ≈ z → x # y → x # z + ``` + +* Added new proofs to `Data.List.Relation.Binary.Sublist.Setoid.Properties` + and `Data.List.Relation.Unary.Sorted.TotalOrder.Properties`. + ```agda + ⊆-mergeˡ : ∀ xs ys → xs ⊆ merge _≤?_ xs ys + ⊆-mergeʳ : ∀ xs ys → ys ⊆ merge _≤?_ xs ys + ``` + +* Added new file `Relation.Binary.Reasoning.Base.Apartness` + + This is how to use it: + ```agda + _ : a # d + _ = begin-apartness + a ≈⟨ a≈b ⟩ + b #⟨ b#c ⟩ + c ≈⟨ c≈d ⟩ + d ∎ + ``` diff --git a/README/Data/Fin/Substitution/UntypedLambda.agda b/README/Data/Fin/Substitution/UntypedLambda.agda new file mode 100644 index 0000000000..126959958f --- /dev/null +++ b/README/Data/Fin/Substitution/UntypedLambda.agda @@ -0,0 +1,103 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- An example of how Data.Fin.Substitution can be used: a definition +-- of substitution for the untyped λ-calculus, along with some lemmas +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Data.Fin.Substitution.UntypedLambda where + +open import Data.Fin.Substitution +open import Data.Fin.Substitution.Lemmas +open import Data.Nat.Base hiding (_/_) +open import Data.Fin.Base using (Fin) +open import Data.Vec.Base +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning) +open import Relation.Binary.Construct.Closure.ReflexiveTransitive + using (Star; ε; _◅_) + +open ≡-Reasoning + +private + variable + m n : ℕ + +------------------------------------------------------------------------ +-- A representation of the untyped λ-calculus. Uses de Bruijn indices. + +infixl 9 _·_ + +data Lam (n : ℕ) : Set where + var : (x : Fin n) → Lam n + ƛ : (t : Lam (suc n)) → Lam n + _·_ : (t₁ t₂ : Lam n) → Lam n + +------------------------------------------------------------------------ +-- Code for applying substitutions. + +module LamApp {ℓ} {T : ℕ → Set ℓ} (l : Lift T Lam) where + open Lift l hiding (var) + + -- Applies a substitution to a term. + + infixl 8 _/_ + + _/_ : Lam m → Sub T m n → Lam n + var x / ρ = lift (lookup ρ x) + ƛ t / ρ = ƛ (t / ρ ↑) + t₁ · t₂ / ρ = (t₁ / ρ) · (t₂ / ρ) + + open Application (record { _/_ = _/_ }) using (_/✶_) + + -- Some lemmas about _/_. + + ƛ-/✶-↑✶ : ∀ k {t} (ρs : Subs T m n) → + ƛ t /✶ ρs ↑✶ k ≡ ƛ (t /✶ ρs ↑✶ suc k) + ƛ-/✶-↑✶ k ε = refl + ƛ-/✶-↑✶ k (ρ ◅ ρs) = cong (_/ _) (ƛ-/✶-↑✶ k ρs) + + ·-/✶-↑✶ : ∀ k {t₁ t₂} (ρs : Subs T m n) → + t₁ · t₂ /✶ ρs ↑✶ k ≡ (t₁ /✶ ρs ↑✶ k) · (t₂ /✶ ρs ↑✶ k) + ·-/✶-↑✶ k ε = refl + ·-/✶-↑✶ k (ρ ◅ ρs) = cong (_/ _) (·-/✶-↑✶ k ρs) + +lamSubst : TermSubst Lam +lamSubst = record { var = var; app = LamApp._/_ } + +open TermSubst lamSubst hiding (var) + +------------------------------------------------------------------------ +-- Substitution lemmas. + +lamLemmas : TermLemmas Lam +lamLemmas = record + { termSubst = lamSubst + ; app-var = refl + ; /✶-↑✶ = Lemma./✶-↑✶ + } + where + module Lemma {T₁ T₂} {lift₁ : Lift T₁ Lam} {lift₂ : Lift T₂ Lam} where + + open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_) + open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_) + + /✶-↑✶ : (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) → + (∀ k x → var x /✶₁ ρs₁ ↑✶₁ k ≡ var x /✶₂ ρs₂ ↑✶₂ k) → + ∀ k t → t /✶₁ ρs₁ ↑✶₁ k ≡ t /✶₂ ρs₂ ↑✶₂ k + /✶-↑✶ ρs₁ ρs₂ hyp k (var x) = hyp k x + /✶-↑✶ ρs₁ ρs₂ hyp k (ƛ t) = begin + ƛ t /✶₁ ρs₁ ↑✶₁ k ≡⟨ LamApp.ƛ-/✶-↑✶ _ k ρs₁ ⟩ + ƛ (t /✶₁ ρs₁ ↑✶₁ suc k) ≡⟨ cong ƛ (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) t) ⟩ + ƛ (t /✶₂ ρs₂ ↑✶₂ suc k) ≡⟨ sym (LamApp.ƛ-/✶-↑✶ _ k ρs₂) ⟩ + ƛ t /✶₂ ρs₂ ↑✶₂ k ∎ + /✶-↑✶ ρs₁ ρs₂ hyp k (t₁ · t₂) = begin + t₁ · t₂ /✶₁ ρs₁ ↑✶₁ k ≡⟨ LamApp.·-/✶-↑✶ _ k ρs₁ ⟩ + (t₁ /✶₁ ρs₁ ↑✶₁ k) · (t₂ /✶₁ ρs₁ ↑✶₁ k) ≡⟨ cong₂ _·_ (/✶-↑✶ ρs₁ ρs₂ hyp k t₁) + (/✶-↑✶ ρs₁ ρs₂ hyp k t₂) ⟩ + (t₁ /✶₂ ρs₂ ↑✶₂ k) · (t₂ /✶₂ ρs₂ ↑✶₂ k) ≡⟨ sym (LamApp.·-/✶-↑✶ _ k ρs₂) ⟩ + t₁ · t₂ /✶₂ ρs₂ ↑✶₂ k ∎ + +open TermLemmas lamLemmas public hiding (var) diff --git a/src/Data/Fin/Substitution.agda b/src/Data/Fin/Substitution.agda index 809b235dd4..84a4484715 100644 --- a/src/Data/Fin/Substitution.agda +++ b/src/Data/Fin/Substitution.agda @@ -4,14 +4,14 @@ -- Substitutions ------------------------------------------------------------------------ --- Uses a variant of Conor McBride's technique from "Type-Preserving --- Renaming and Substitution". +-- Uses a variant of Conor McBride's technique from his paper +-- "Type-Preserving Renaming and Substitution". --- See Data.Fin.Substitution.Example for an example of how this module --- can be used: a definition of substitution for the untyped --- λ-calculus. +-- See README.Data.Fin.Substitution.UntypedLambda for an example +-- of how this module can be used: a definition of substitution for +-- the untyped λ-calculus. -{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Substitution where @@ -24,23 +24,29 @@ open import Relation.Binary.Construct.Closure.ReflexiveTransitive open import Level using (Level; _⊔_; 0ℓ) open import Relation.Unary using (Pred) +private + variable + ℓ ℓ₁ ℓ₂ : Level + k m n o : ℕ + + ------------------------------------------------------------------------ -- General functionality -- A Sub T m n is a substitution which, when applied to something with -- at most m variables, yields something with at most n variables. -Sub : ∀ {ℓ} → Pred ℕ ℓ → ℕ → ℕ → Set ℓ +Sub : Pred ℕ ℓ → ℕ → ℕ → Set ℓ Sub T m n = Vec (T n) m -- A /reversed/ sequence of matching substitutions. -Subs : ∀ {ℓ} → Pred ℕ ℓ → ℕ → ℕ → Set ℓ +Subs : Pred ℕ ℓ → ℕ → ℕ → Set ℓ Subs T = flip (Star (flip (Sub T))) -- Some simple substitutions. -record Simple {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where +record Simple (T : Pred ℕ ℓ) : Set ℓ where infix 10 _↑ infixl 10 _↑⋆_ _↑✶_ @@ -50,40 +56,39 @@ record Simple {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where -- Lifting. - _↑ : ∀ {m n} → Sub T m n → Sub T (suc m) (suc n) + _↑ : Sub T m n → Sub T (suc m) (suc n) ρ ↑ = var zero ∷ map weaken ρ - _↑⋆_ : ∀ {m n} → Sub T m n → ∀ k → Sub T (k + m) (k + n) + _↑⋆_ : Sub T m n → ∀ k → Sub T (k + m) (k + n) ρ ↑⋆ zero = ρ ρ ↑⋆ suc k = (ρ ↑⋆ k) ↑ - _↑✶_ : ∀ {m n} → Subs T m n → ∀ k → Subs T (k + m) (k + n) + _↑✶_ : Subs T m n → ∀ k → Subs T (k + m) (k + n) ρs ↑✶ k = Star.gmap (_+_ k) (λ ρ → ρ ↑⋆ k) ρs -- The identity substitution. - id : ∀ {n} → Sub T n n + id : Sub T n n id {zero} = [] id {suc n} = id ↑ -- Weakening. - wk⋆ : ∀ k {n} → Sub T n (k + n) + wk⋆ : ∀ k → Sub T n (k + n) wk⋆ zero = id wk⋆ (suc k) = map weaken (wk⋆ k) - wk : ∀ {n} → Sub T n (suc n) + wk : Sub T n (suc n) wk = wk⋆ 1 -- A substitution which only replaces the first variable. - sub : ∀ {n} → T n → Sub T (suc n) n + sub : T n → Sub T (suc n) n sub t = t ∷ id -- Application of substitutions. -record Application {ℓ₁ ℓ₂ : Level} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : - Set (ℓ₁ ⊔ ℓ₂) where +record Application (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where infixl 8 _/_ _/✶_ infixl 9 _⊙_ @@ -93,17 +98,17 @@ record Application {ℓ₁ ℓ₂ : Level} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred -- Reverse composition. (Fits well with post-application.) - _⊙_ : ∀ {m n k} → Sub T₁ m n → Sub T₂ n k → Sub T₁ m k - ρ₁ ⊙ ρ₂ = map (λ t → t / ρ₂) ρ₁ + _⊙_ : Sub T₁ m n → Sub T₂ n o → Sub T₁ m o + ρ₁ ⊙ ρ₂ = map (_/ ρ₂) ρ₁ -- Application of multiple substitutions. - _/✶_ : ∀ {m n} → T₁ m → Subs T₂ m n → T₁ n + _/✶_ : T₁ m → Subs T₂ m n → T₁ n _/✶_ = Star.gfold Fun.id _ (flip _/_) {k = zero} -- A combination of the two records above. -record Subst {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where +record Subst (T : Pred ℕ ℓ) : Set ℓ where field simple : Simple T application : Application T T @@ -113,7 +118,7 @@ record Subst {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where -- Composition of multiple substitutions. - ⨀ : ∀ {m n} → Subs T m n → Sub T m n + ⨀ : Subs T m n → Sub T m n ⨀ ε = id ⨀ (ρ ◅ ε) = ρ -- Convenient optimisation; simplifies some proofs. ⨀ (ρ ◅ ρs) = ⨀ ρs ⊙ ρ @@ -123,8 +128,7 @@ record Subst {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where -- Liftings from T₁ to T₂. -record Lift {ℓ₁ ℓ₂ : Level} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : - Set (ℓ₁ ⊔ ℓ₂) where +record Lift (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where field simple : Simple T₁ lift : ∀ {n} → T₁ n → T₂ n @@ -162,7 +166,7 @@ record TermSubst (T : Pred ℕ 0ℓ) : Set₁ where infixl 8 _/Var_ - _/Var_ : ∀ {m n} → T m → Sub Fin m n → T n + _/Var_ : T m → Sub Fin m n → T n _/Var_ = app varLift simple : Simple T diff --git a/src/Data/Fin/Substitution/Example.agda b/src/Data/Fin/Substitution/Example.agda index 44427c8bea..02c98c539f 100644 --- a/src/Data/Fin/Substitution/Example.agda +++ b/src/Data/Fin/Substitution/Example.agda @@ -1,20 +1,26 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- An example of how Data.Fin.Substitution can be used: a definition --- of substitution for the untyped λ-calculus, along with some lemmas +-- This module is DEPRECATED. Please see +-- `README.Data.Nat.Fin.Substitution.UntypedLambda` instead. +-- ------------------------------------------------------------------------ -{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Substitution.Example where +{-# WARNING_ON_IMPORT +"Data.Fin.Substitution.Example was deprecated in v2.0. +Please see README.Data.Nat.Fin.Substitution.UntypedLambda instead." +#-} + open import Data.Fin.Substitution open import Data.Fin.Substitution.Lemmas open import Data.Nat.Base hiding (_/_) open import Data.Fin.Base using (Fin) open import Data.Vec.Base -open import Relation.Binary.PropositionalEquality as PropEq +open import Relation.Binary.PropositionalEquality.Core as PropEq using (_≡_; refl; sym; cong; cong₂) open PropEq.≡-Reasoning open import Relation.Binary.Construct.Closure.ReflexiveTransitive diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda index fc1bc66036..ffa26e64fb 100644 --- a/src/Data/Fin/Substitution/Lemmas.agda +++ b/src/Data/Fin/Substitution/Lemmas.agda @@ -4,18 +4,17 @@ -- Substitution lemmas ------------------------------------------------------------------------ -{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Substitution.Lemmas where -import Effect.Applicative.Indexed as Applicative open import Data.Fin.Substitution open import Data.Nat hiding (_⊔_; _/_) open import Data.Fin.Base using (Fin; zero; suc; lift) open import Data.Vec.Base import Data.Vec.Properties as VecProp -open import Function as Fun using (_∘_; _$_) -open import Relation.Binary.PropositionalEquality as PropEq +open import Function.Base as Fun using (_∘_; _$_; flip) +open import Relation.Binary.PropositionalEquality.Core as PropEq using (_≡_; refl; sym; cong; cong₂) open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; ε; _◅_; _▻_) @@ -23,25 +22,32 @@ open PropEq.≡-Reasoning open import Level using (Level; _⊔_) open import Relation.Unary using (Pred) +private + variable + ℓ ℓ₁ ℓ₂ : Level + m n o p : ℕ + +------------------------------------------------------------------------ -- A lemma which does not refer to any substitutions. -lift-commutes : ∀ {n} k j (x : Fin (j + (k + n))) → +lift-commutes : ∀ k j (x : Fin (j + (k + n))) → lift j suc (lift j (lift k suc) x) ≡ lift j (lift (suc k) suc) (lift j suc x) lift-commutes k zero x = refl lift-commutes k (suc j) zero = refl lift-commutes k (suc j) (suc x) = cong suc (lift-commutes k j x) +------------------------------------------------------------------------ -- The modules below prove a number of substitution lemmas, on the -- assumption that the underlying substitution machinery satisfies -- certain properties. -record Lemmas₀ {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₀ (T : Pred ℕ ℓ) : Set ℓ where field simple : Simple T open Simple simple - extensionality : ∀ {m n} {ρ₁ ρ₂ : Sub T m n} → + extensionality : {ρ₁ ρ₂ : Sub T m n} → (∀ x → lookup ρ₁ x ≡ lookup ρ₂ x) → ρ₁ ≡ ρ₂ extensionality {ρ₁ = []} {[]} hyp = refl extensionality {ρ₁ = t₁ ∷ ρ₁} { t₂ ∷ ρ₂} hyp with hyp zero @@ -54,7 +60,7 @@ record Lemmas₀ {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where (id ↑⋆ k) ↑ ≡⟨ cong _↑ (id-↑⋆ k) ⟩ id ↑ ∎ - lookup-map-weaken-↑⋆ : ∀ {m n} k x {ρ : Sub T m n} → + lookup-map-weaken-↑⋆ : ∀ k x {ρ : Sub T m n} → lookup (map weaken ρ ↑⋆ k) x ≡ lookup ((ρ ↑) ↑⋆ k) (lift k suc x) lookup-map-weaken-↑⋆ zero x = refl @@ -65,7 +71,7 @@ record Lemmas₀ {ℓ : Level} (T : Pred ℕ ℓ) : Set ℓ where weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x)) ≡⟨ sym $ VecProp.lookup-map (lift k suc x) weaken ((ρ ↑) ↑⋆ k) ⟩ lookup (map weaken ((ρ ↑) ↑⋆ k)) (lift k suc x) ∎ -record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₁ (T : Pred ℕ ℓ) : Set ℓ where field lemmas₀ : Lemmas₀ T open Lemmas₀ lemmas₀ @@ -73,7 +79,7 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where field weaken-var : ∀ {n} {x : Fin n} → weaken (var x) ≡ var (suc x) - lookup-map-weaken : ∀ {m n} x {y} {ρ : Sub T m n} → + lookup-map-weaken : ∀ x {y} {ρ : Sub T m n} → lookup ρ x ≡ var y → lookup (map weaken ρ) x ≡ var (suc y) lookup-map-weaken x {y} {ρ} hyp = begin @@ -84,14 +90,14 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where mutual - lookup-id : ∀ {n} (x : Fin n) → lookup id x ≡ var x + lookup-id : (x : Fin n) → lookup id x ≡ var x lookup-id zero = refl lookup-id (suc x) = lookup-wk x - lookup-wk : ∀ {n} (x : Fin n) → lookup wk x ≡ var (suc x) + lookup-wk : (x : Fin n) → lookup wk x ≡ var (suc x) lookup-wk x = lookup-map-weaken x {ρ = id} (lookup-id x) - lookup-↑⋆ : ∀ {m n} (f : Fin m → Fin n) {ρ : Sub T m n} → + lookup-↑⋆ : (f : Fin m → Fin n) {ρ : Sub T m n} → (∀ x → lookup ρ x ≡ var (f x)) → ∀ k x → lookup (ρ ↑⋆ k) x ≡ var (lift k f x) lookup-↑⋆ f hyp zero x = hyp x @@ -99,7 +105,7 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) = lookup-map-weaken x {ρ = ρ ↑⋆ k} (lookup-↑⋆ f hyp k x) - lookup-lift-↑⋆ : ∀ {m n} (f : Fin n → Fin m) {ρ : Sub T m n} → + lookup-lift-↑⋆ : (f : Fin n → Fin m) {ρ : Sub T m n} → (∀ x → lookup ρ (f x) ≡ var x) → ∀ k x → lookup (ρ ↑⋆ k) (lift k f x) ≡ var x lookup-lift-↑⋆ f hyp zero x = hyp x @@ -107,22 +113,22 @@ record Lemmas₁ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup-lift-↑⋆ f {ρ = ρ} hyp (suc k) (suc x) = lookup-map-weaken (lift k f x) {ρ = ρ ↑⋆ k} (lookup-lift-↑⋆ f hyp k x) - lookup-wk-↑⋆ : ∀ {n} k (x : Fin (k + n)) → + lookup-wk-↑⋆ : ∀ k (x : Fin (k + n)) → lookup (wk ↑⋆ k) x ≡ var (lift k suc x) lookup-wk-↑⋆ = lookup-↑⋆ suc lookup-wk - lookup-wk-↑⋆-↑⋆ : ∀ {n} k j (x : Fin (j + (k + n))) → + lookup-wk-↑⋆-↑⋆ : ∀ k j (x : Fin (j + (k + n))) → lookup (wk ↑⋆ k ↑⋆ j) x ≡ var (lift j (lift k suc) x) lookup-wk-↑⋆-↑⋆ k = lookup-↑⋆ (lift k suc) (lookup-wk-↑⋆ k) - lookup-sub-↑⋆ : ∀ {n t} k (x : Fin (k + n)) → + lookup-sub-↑⋆ : ∀ {t} k (x : Fin (k + n)) → lookup (sub t ↑⋆ k) (lift k suc x) ≡ var x lookup-sub-↑⋆ = lookup-lift-↑⋆ suc lookup-id open Lemmas₀ lemmas₀ public -record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₂ (T : Pred ℕ ℓ) : Set ℓ where field lemmas₁ : Lemmas₁ T application : Application T T @@ -136,18 +142,18 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where field var-/ : ∀ {m n x} {ρ : Sub T m n} → var x / ρ ≡ lookup ρ x - suc-/-sub : ∀ {n x} {t : T n} → var (suc x) / sub t ≡ var x + suc-/-sub : ∀ {x} {t : T n} → var (suc x) / sub t ≡ var x suc-/-sub {x = x} {t} = begin var (suc x) / sub t ≡⟨ var-/ ⟩ lookup (sub t) (suc x) ≡⟨ refl ⟩ lookup id x ≡⟨ lookup-id x ⟩ var x ∎ - lookup-⊙ : ∀ {m n k} x {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} → + lookup-⊙ : ∀ x {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → lookup (ρ₁ ⊙ ρ₂) x ≡ lookup ρ₁ x / ρ₂ lookup-⊙ x {ρ₁} {ρ₂} = VecProp.lookup-map x (λ t → t / ρ₂) ρ₁ - lookup-⨀ : ∀ {m n} x (ρs : Subs T m n) → + lookup-⨀ : ∀ x (ρs : Subs T m n) → lookup (⨀ ρs) x ≡ var x /✶ ρs lookup-⨀ x ε = lookup-id x lookup-⨀ x (ρ ◅ ε) = sym var-/ @@ -158,14 +164,14 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where var x /✶ ρs / ρ ∎ where ρs = ρ′ ◅ ρs′ - id-⊙ : ∀ {m n} {ρ : Sub T m n} → id ⊙ ρ ≡ ρ + id-⊙ : {ρ : Sub T m n} → id ⊙ ρ ≡ ρ id-⊙ {ρ = ρ} = extensionality λ x → begin lookup (id ⊙ ρ) x ≡⟨ lookup-⊙ x {ρ₁ = id} ⟩ lookup id x / ρ ≡⟨ cong₂ _/_ (lookup-id x) refl ⟩ var x / ρ ≡⟨ var-/ ⟩ lookup ρ x ∎ - lookup-wk-↑⋆-⊙ : ∀ {m n} k {x} {ρ : Sub T (k + suc m) n} → + lookup-wk-↑⋆-⊙ : ∀ k {x} {ρ : Sub T (k + suc m) n} → lookup (wk ↑⋆ k ⊙ ρ) x ≡ lookup ρ (lift k suc x) lookup-wk-↑⋆-⊙ k {x} {ρ} = begin lookup (wk ↑⋆ k ⊙ ρ) x ≡⟨ lookup-⊙ x {ρ₁ = wk ↑⋆ k} ⟩ @@ -173,14 +179,14 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where var (lift k suc x) / ρ ≡⟨ var-/ ⟩ lookup ρ (lift k suc x) ∎ - wk-⊙-sub′ : ∀ {n} {t : T n} k → wk ↑⋆ k ⊙ sub t ↑⋆ k ≡ id + wk-⊙-sub′ : ∀ {t : T n} k → wk ↑⋆ k ⊙ sub t ↑⋆ k ≡ id wk-⊙-sub′ {t = t} k = extensionality λ x → begin lookup (wk ↑⋆ k ⊙ sub t ↑⋆ k) x ≡⟨ lookup-wk-↑⋆-⊙ k ⟩ lookup (sub t ↑⋆ k) (lift k suc x) ≡⟨ lookup-sub-↑⋆ k x ⟩ var x ≡⟨ sym (lookup-id x) ⟩ lookup id x ∎ - wk-⊙-sub : ∀ {n} {t : T n} → wk ⊙ sub t ≡ id + wk-⊙-sub : {t : T n} → wk ⊙ sub t ≡ id wk-⊙-sub = wk-⊙-sub′ zero var-/-wk-↑⋆ : ∀ {n} k (x : Fin (k + n)) → @@ -190,7 +196,7 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup (wk ↑⋆ k) x ≡⟨ lookup-wk-↑⋆ k x ⟩ var (lift k suc x) ∎ - wk-↑⋆-⊙-wk : ∀ {n} k j → + wk-↑⋆-⊙-wk : ∀ k j → wk {n} ↑⋆ k ↑⋆ j ⊙ wk ↑⋆ j ≡ wk ↑⋆ j ⊙ wk ↑⋆ suc k ↑⋆ j wk-↑⋆-⊙-wk k j = extensionality λ x → begin @@ -207,7 +213,7 @@ record Lemmas₂ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where open Subst subst public hiding (simple; application) open Lemmas₁ lemmas₁ public -record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₃ (T : Pred ℕ ℓ) : Set ℓ where field lemmas₂ : Lemmas₂ T open Lemmas₂ lemmas₂ @@ -217,19 +223,19 @@ record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where (∀ k x → var x /✶ ρs₁ ↑✶ k ≡ var x /✶ ρs₂ ↑✶ k) → ∀ k t → t /✶ ρs₁ ↑✶ k ≡ t /✶ ρs₂ ↑✶ k - /✶-↑✶′ : ∀ {m n} (ρs₁ ρs₂ : Subs T m n) → + /✶-↑✶′ : (ρs₁ ρs₂ : Subs T m n) → (∀ k → ⨀ (ρs₁ ↑✶ k) ≡ ⨀ (ρs₂ ↑✶ k)) → ∀ k t → t /✶ ρs₁ ↑✶ k ≡ t /✶ ρs₂ ↑✶ k /✶-↑✶′ ρs₁ ρs₂ hyp = /✶-↑✶ ρs₁ ρs₂ (λ k x → begin var x /✶ ρs₁ ↑✶ k ≡⟨ sym (lookup-⨀ x (ρs₁ ↑✶ k)) ⟩ - lookup (⨀ (ρs₁ ↑✶ k)) x ≡⟨ cong (Fun.flip lookup x) (hyp k) ⟩ + lookup (⨀ (ρs₁ ↑✶ k)) x ≡⟨ cong (flip lookup x) (hyp k) ⟩ lookup (⨀ (ρs₂ ↑✶ k)) x ≡⟨ lookup-⨀ x (ρs₂ ↑✶ k) ⟩ var x /✶ ρs₂ ↑✶ k ∎) - id-vanishes : ∀ {n} (t : T n) → t / id ≡ t + id-vanishes : (t : T n) → t / id ≡ t id-vanishes = /✶-↑✶′ (ε ▻ id) ε id-↑⋆ zero - ⊙-id : ∀ {m n} {ρ : Sub T m n} → ρ ⊙ id ≡ ρ + ⊙-id : {ρ : Sub T m n} → ρ ⊙ id ≡ ρ ⊙-id {ρ = ρ} = begin map (λ t → t / id) ρ ≡⟨ VecProp.map-cong id-vanishes ρ ⟩ map Fun.id ρ ≡⟨ VecProp.map-id ρ ⟩ @@ -237,7 +243,7 @@ record Lemmas₃ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where open Lemmas₂ lemmas₂ public hiding (wk-⊙-sub′) -record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where +record Lemmas₄ (T : Pred ℕ ℓ) : Set ℓ where field lemmas₃ : Lemmas₃ T open Lemmas₃ lemmas₃ @@ -246,7 +252,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where private - ↑-distrib′ : ∀ {m n k} {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} → + ↑-distrib′ : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → (∀ t → t / ρ₂ / wk ≡ t / wk / ρ₂ ↑) → (ρ₁ ⊙ ρ₂) ↑ ≡ ρ₁ ↑ ⊙ ρ₂ ↑ ↑-distrib′ {ρ₁ = ρ₁} {ρ₂} hyp = begin @@ -265,7 +271,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where map (λ t → weaken t / ρ₂ ↑) ρ₁ ≡⟨ VecProp.map-∘ _ _ _ ⟩ map (λ t → t / ρ₂ ↑) (map weaken ρ₁) ∎ - ↑⋆-distrib′ : ∀ {m n o} {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → + ↑⋆-distrib′ : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → (∀ k t → t / ρ₂ ↑⋆ k / wk ≡ t / wk / ρ₂ ↑⋆ suc k) → ∀ k → (ρ₁ ⊙ ρ₂) ↑⋆ k ≡ ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k ↑⋆-distrib′ hyp zero = refl @@ -274,7 +280,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where (ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k) ↑ ≡⟨ ↑-distrib′ (hyp k) ⟩ ρ₁ ↑⋆ suc k ⊙ ρ₂ ↑⋆ suc k ∎ - map-weaken : ∀ {m n} {ρ : Sub T m n} → map weaken ρ ≡ ρ ⊙ wk + map-weaken : {ρ : Sub T m n} → map weaken ρ ≡ ρ ⊙ wk map-weaken {ρ = ρ} = begin map weaken ρ ≡⟨ VecProp.map-cong (λ _ → sym /-wk) ρ ⟩ map (λ t → t / wk) ρ ≡⟨ refl ⟩ @@ -282,7 +288,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where private - ⊙-wk′ : ∀ {m n} {ρ : Sub T m n} k → + ⊙-wk′ : ∀ {ρ : Sub T m n} k → ρ ↑⋆ k ⊙ wk ↑⋆ k ≡ wk ↑⋆ k ⊙ ρ ↑ ↑⋆ k ⊙-wk′ {ρ = ρ} k = sym (begin wk ↑⋆ k ⊙ ρ ↑ ↑⋆ k ≡⟨ lemma ⟩ @@ -297,31 +303,30 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where lookup (ρ ↑ ↑⋆ k) (lift k suc x) ≡⟨ sym (lookup-map-weaken-↑⋆ k x) ⟩ lookup (map weaken ρ ↑⋆ k) x ∎ - ⊙-wk : ∀ {m n} {ρ : Sub T m n} → ρ ⊙ wk ≡ wk ⊙ ρ ↑ + ⊙-wk : {ρ : Sub T m n} → ρ ⊙ wk ≡ wk ⊙ ρ ↑ ⊙-wk = ⊙-wk′ zero - wk-commutes : ∀ {m n} {ρ : Sub T m n} t → + wk-commutes : ∀ {ρ : Sub T m n} t → t / ρ / wk ≡ t / wk / ρ ↑ wk-commutes {ρ = ρ} = /✶-↑✶′ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ ρ ↑) ⊙-wk′ zero - ↑⋆-distrib : ∀ {m n o} {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → + ↑⋆-distrib : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} → ∀ k → (ρ₁ ⊙ ρ₂) ↑⋆ k ≡ ρ₁ ↑⋆ k ⊙ ρ₂ ↑⋆ k ↑⋆-distrib = ↑⋆-distrib′ (λ _ → wk-commutes) - /-⊙ : ∀ {m n k} {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} t → + /-⊙ : ∀ {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} t → t / ρ₁ ⊙ ρ₂ ≡ t / ρ₁ / ρ₂ /-⊙ {ρ₁ = ρ₁} {ρ₂} t = /✶-↑✶′ (ε ▻ ρ₁ ⊙ ρ₂) (ε ▻ ρ₁ ▻ ρ₂) ↑⋆-distrib zero t - ⊙-assoc : ∀ {m n k o} - {ρ₁ : Sub T m n} {ρ₂ : Sub T n k} {ρ₃ : Sub T k o} → + ⊙-assoc : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} {ρ₃ : Sub T o p} → ρ₁ ⊙ (ρ₂ ⊙ ρ₃) ≡ (ρ₁ ⊙ ρ₂) ⊙ ρ₃ ⊙-assoc {ρ₁ = ρ₁} {ρ₂} {ρ₃} = begin map (λ t → t / ρ₂ ⊙ ρ₃) ρ₁ ≡⟨ VecProp.map-cong /-⊙ ρ₁ ⟩ map (λ t → t / ρ₂ / ρ₃) ρ₁ ≡⟨ VecProp.map-∘ _ _ _ ⟩ map (λ t → t / ρ₃) (map (λ t → t / ρ₂) ρ₁) ∎ - map-weaken-⊙-sub : ∀ {m n} {ρ : Sub T m n} {t} → map weaken ρ ⊙ sub t ≡ ρ + map-weaken-⊙-sub : ∀ {ρ : Sub T m n} {t} → map weaken ρ ⊙ sub t ≡ ρ map-weaken-⊙-sub {ρ = ρ} {t} = begin map weaken ρ ⊙ sub t ≡⟨ cong₂ _⊙_ map-weaken refl ⟩ ρ ⊙ wk ⊙ sub t ≡⟨ sym ⊙-assoc ⟩ @@ -329,7 +334,7 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where ρ ⊙ id ≡⟨ ⊙-id ⟩ ρ ∎ - sub-⊙ : ∀ {m n} {ρ : Sub T m n} t → sub t ⊙ ρ ≡ ρ ↑ ⊙ sub (t / ρ) + sub-⊙ : ∀ {ρ : Sub T m n} t → sub t ⊙ ρ ≡ ρ ↑ ⊙ sub (t / ρ) sub-⊙ {ρ = ρ} t = begin sub t ⊙ ρ ≡⟨ refl ⟩ t / ρ ∷ id ⊙ ρ ≡⟨ cong (_∷_ (t / ρ)) id-⊙ ⟩ @@ -337,16 +342,16 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where t / ρ ∷ map weaken ρ ⊙ sub (t / ρ) ≡⟨ cong₂ _∷_ (sym var-/) refl ⟩ ρ ↑ ⊙ sub (t / ρ) ∎ - suc-/-↑ : ∀ {m n} {ρ : Sub T m n} x → + suc-/-↑ : ∀ {ρ : Sub T m n} x → var (suc x) / ρ ↑ ≡ var x / ρ / wk suc-/-↑ {ρ = ρ} x = begin var (suc x) / ρ ↑ ≡⟨ var-/ ⟩ - lookup (map weaken ρ) x ≡⟨ cong (Fun.flip lookup x) (map-weaken {ρ = ρ}) ⟩ + lookup (map weaken ρ) x ≡⟨ cong (flip lookup x) (map-weaken {ρ = ρ}) ⟩ lookup (ρ ⊙ wk) x ≡⟨ lookup-⊙ x {ρ₁ = ρ} ⟩ lookup ρ x / wk ≡⟨ cong₂ _/_ (sym var-/) refl ⟩ var x / ρ / wk ∎ - weaken-↑ : ∀ {k n} t {ρ : Sub T k n} → weaken t / (ρ ↑) ≡ weaken (t / ρ) + weaken-↑ : ∀ t {ρ : Sub T m n} → weaken t / (ρ ↑) ≡ weaken (t / ρ) weaken-↑ t {ρ} = begin weaken t / (ρ ↑) ≡⟨ cong (_/ ρ ↑) (sym /-wk) ⟩ t / wk / ρ ↑ ≡⟨ sym (wk-commutes t) ⟩ @@ -357,10 +362,11 @@ record Lemmas₄ {ℓ} (T : Pred ℕ ℓ) : Set ℓ where hiding (/✶-↑✶; /✶-↑✶′; wk-↑⋆-⊙-wk; lookup-wk-↑⋆-⊙; lookup-map-weaken-↑⋆) +------------------------------------------------------------------------ -- For an example of how AppLemmas can be used, see -- Data.Fin.Substitution.List. -record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where +record AppLemmas (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where field application : Application T₁ T₂ lemmas₄ : Lemmas₄ T₂ @@ -376,7 +382,7 @@ record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ private module L₄ = Lemmas₄ lemmas₄ - /-⨀ : ∀ {m n} t (ρs : Subs T₂ m n) → t / ⨀ ρs ≡ t /✶ ρs + /-⨀ : ∀ t (ρs : Subs T₂ m n) → t / ⨀ ρs ≡ t /✶ ρs /-⨀ t ε = id-vanishes t /-⨀ t (ρ ◅ ε) = refl /-⨀ t (ρ ◅ (ρ′ ◅ ρs′)) = begin @@ -385,7 +391,7 @@ record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ t /✶ ρs / ρ ∎ where ρs = ρ′ ◅ ρs′ - ⨀→/✶ : ∀ {m n} (ρs₁ ρs₂ : Subs T₂ m n) → + ⨀→/✶ : (ρs₁ ρs₂ : Subs T₂ m n) → ⨀ ρs₁ ≡ ⨀ ρs₂ → ∀ t → t /✶ ρs₁ ≡ t /✶ ρs₂ ⨀→/✶ ρs₁ ρs₂ hyp t = begin t /✶ ρs₁ ≡⟨ sym (/-⨀ t ρs₁) ⟩ @@ -393,19 +399,19 @@ record AppLemmas {ℓ₁ ℓ₂} (T₁ : Pred ℕ ℓ₁) (T₂ : Pred ℕ ℓ t / ⨀ ρs₂ ≡⟨ /-⨀ t ρs₂ ⟩ t /✶ ρs₂ ∎ - wk-commutes : ∀ {m n} {ρ : Sub T₂ m n} t → + wk-commutes : ∀ {ρ : Sub T₂ m n} t → t / ρ / wk ≡ t / wk / ρ ↑ wk-commutes {ρ = ρ} = ⨀→/✶ (ε ▻ ρ ▻ wk) (ε ▻ wk ▻ ρ ↑) L₄.⊙-wk - sub-commutes : ∀ {m n} {t′} {ρ : Sub T₂ m n} t → + sub-commutes : ∀ {t′} {ρ : Sub T₂ m n} t → t / sub t′ / ρ ≡ t / ρ ↑ / sub (t′ ⊘ ρ) sub-commutes {t′ = t′} {ρ} = ⨀→/✶ (ε ▻ sub t′ ▻ ρ) (ε ▻ ρ ↑ ▻ sub (t′ ⊘ ρ)) (L₄.sub-⊙ t′) - wk-sub-vanishes : ∀ {n t′} (t : T₁ n) → t / wk / sub t′ ≡ t + wk-sub-vanishes : ∀ {t′} (t : T₁ n) → t / wk / sub t′ ≡ t wk-sub-vanishes {t′ = t′} = ⨀→/✶ (ε ▻ wk ▻ sub t′) ε L₄.wk-⊙-sub - /-weaken : ∀ {m n} {ρ : Sub T₂ m n} t → t / map weaken ρ ≡ t / ρ / wk + /-weaken : ∀ {ρ : Sub T₂ m n} t → t / map weaken ρ ≡ t / ρ / wk /-weaken {ρ = ρ} = ⨀→/✶ (ε ▻ map weaken ρ) (ε ▻ ρ ▻ wk) L₄.map-weaken open Application application public @@ -527,18 +533,19 @@ record TermLemmas (T : ℕ → Set) : Set₁ where open Lemmas₅ lemmas₅ public hiding (lemmas₃) - wk-⊙-∷ : ∀ {m n} (t : T n) (ρ : Sub T m n) → (T.wk T.⊙ (t ∷ ρ)) ≡ ρ - wk-⊙-∷ t ρ = extensionality (λ x → begin + wk-⊙-∷ : (t : T n) (ρ : Sub T m n) → (T.wk T.⊙ (t ∷ ρ)) ≡ ρ + wk-⊙-∷ t ρ = extensionality λ x → begin lookup (T.wk T.⊙ (t ∷ ρ)) x ≡⟨ L₃.lookup-wk-↑⋆-⊙ 0 {ρ = t ∷ ρ} ⟩ - lookup ρ x ∎) + lookup ρ x ∎ - weaken-∷ : ∀ {k n} (t₁ : T k) {t₂ : T n} {ρ : Sub T k n} → T.weaken t₁ T./ (t₂ ∷ ρ) ≡ t₁ T./ ρ + weaken-∷ : (t₁ : T m) {t₂ : T n} {ρ : Sub T m n} → + T.weaken t₁ T./ (t₂ ∷ ρ) ≡ t₁ T./ ρ weaken-∷ t₁ {t₂} {ρ} = begin T.weaken t₁ T./ (t₂ ∷ ρ) ≡⟨ cong (T._/ (t₂ ∷ ρ)) (sym /-wk) ⟩ (t₁ T./ T.wk) T./ (t₂ ∷ ρ) ≡⟨ ⨀→/✶ ((t₂ ∷ ρ) ◅ T.wk ◅ ε) (ρ ◅ ε) (wk-⊙-∷ t₂ ρ) t₁ ⟩ t₁ T./ ρ ∎ - weaken-sub : ∀ {n} (t₁ : T n) {t₂ : T n} → T.weaken t₁ T./ (T.sub t₂) ≡ t₁ + weaken-sub : (t₁ : T n) {t₂ : T n} → T.weaken t₁ T./ (T.sub t₂) ≡ t₁ weaken-sub t₁ {t₂} = begin T.weaken t₁ T./ (T.sub t₂) ≡⟨ weaken-∷ t₁ ⟩ t₁ T./ T.id ≡⟨ id-vanishes t₁ ⟩ @@ -546,38 +553,31 @@ record TermLemmas (T : ℕ → Set) : Set₁ where -- Lemmas relating renamings to substitutions. - map-var≡ : - ∀ {m n} {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → - (∀ x → lookup ρ₁ x ≡ f x) → - (∀ x → lookup ρ₂ x ≡ T.var (f x)) → - map T.var ρ₁ ≡ ρ₂ + map-var≡ : {ρ₁ : Sub Fin m n} {ρ₂ : Sub T m n} {f : Fin m → Fin n} → + (∀ x → lookup ρ₁ x ≡ f x) → + (∀ x → lookup ρ₂ x ≡ T.var (f x)) → + map T.var ρ₁ ≡ ρ₂ map-var≡ {ρ₁ = ρ₁} {ρ₂ = ρ₂} {f = f} hyp₁ hyp₂ = extensionality λ x → lookup (map T.var ρ₁) x ≡⟨ VecProp.lookup-map x _ ρ₁ ⟩ T.var (lookup ρ₁ x) ≡⟨ cong T.var $ hyp₁ x ⟩ T.var (f x) ≡⟨ sym $ hyp₂ x ⟩ lookup ρ₂ x ∎ - wk≡wk : ∀ {n} → map T.var VarSubst.wk ≡ T.wk {n = n} + wk≡wk : map T.var VarSubst.wk ≡ T.wk {n = n} wk≡wk = map-var≡ VarLemmas.lookup-wk lookup-wk - id≡id : ∀ {n} → map T.var VarSubst.id ≡ T.id {n = n} + id≡id : map T.var VarSubst.id ≡ T.id {n = n} id≡id = map-var≡ VarLemmas.lookup-id lookup-id - sub≡sub : - ∀ {n} {x : Fin n} → - map T.var (VarSubst.sub x) ≡ T.sub (T.var x) + sub≡sub : {x : Fin n} → map T.var (VarSubst.sub x) ≡ T.sub (T.var x) sub≡sub = cong (_ ∷_) id≡id - ↑≡↑ : - ∀ {m n} {ρ : Sub Fin m n} → - map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ + ↑≡↑ : {ρ : Sub Fin m n} → map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑ ↑≡↑ {ρ = ρ} = map-var≡ (VarLemmas.lookup-↑⋆ (lookup ρ) (λ _ → refl) 1) (lookup-↑⋆ (lookup ρ) (λ _ → VecProp.lookup-map _ _ ρ) 1) - /Var≡/ : - ∀ {m n} {ρ : Sub Fin m n} {t} → - t /Var ρ ≡ t T./ map T.var ρ + /Var≡/ : ∀ {ρ : Sub Fin m n} {t} → t /Var ρ ≡ t T./ map T.var ρ /Var≡/ {ρ = ρ} {t = t} = /✶-↑✶ (ε ▻ ρ) (ε ▻ map T.var ρ) (λ k x → @@ -588,10 +588,8 @@ record TermLemmas (T : ℕ → Set) : Set₁ where T.var x T./ map T.var ρ T.↑⋆ k ∎) zero t - sub-renaming-commutes : - ∀ {m n t x} {ρ : Sub T m n} → - t /Var VarSubst.sub x T./ ρ ≡ - t T./ ρ T.↑ T./ T.sub (lookup ρ x) + sub-renaming-commutes : ∀ {t x} {ρ : Sub T m n} → + t /Var VarSubst.sub x T./ ρ ≡ t T./ ρ T.↑ T./ T.sub (lookup ρ x) sub-renaming-commutes {t = t} {x = x} {ρ = ρ} = t /Var VarSubst.sub x T./ ρ ≡⟨ cong (T._/ ρ) /Var≡/ ⟩ t T./ map T.var (VarSubst.sub x) T./ ρ ≡⟨ cong (λ ρ′ → t T./ ρ′ T./ ρ) sub≡sub ⟩ @@ -599,10 +597,8 @@ record TermLemmas (T : ℕ → Set) : Set₁ where t T./ ρ T.↑ T./ T.sub (T.var x T./ ρ) ≡⟨ cong (λ t′ → t T./ ρ T.↑ T./ T.sub t′) app-var ⟩ t T./ ρ T.↑ T./ T.sub (lookup ρ x) ∎ - sub-commutes-with-renaming : - ∀ {m n} {t t′} {ρ : Sub Fin m n} → - t T./ T.sub t′ /Var ρ ≡ - t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) + sub-commutes-with-renaming : ∀ {t t′} {ρ : Sub Fin m n} → + t T./ T.sub t′ /Var ρ ≡ t /Var ρ VarSubst.↑ T./ T.sub (t′ /Var ρ) sub-commutes-with-renaming {t = t} {t′ = t′} {ρ = ρ} = t T./ T.sub t′ /Var ρ ≡⟨ /Var≡/ ⟩ t T./ T.sub t′ T./ map T.var ρ ≡⟨ sub-commutes _ ⟩ diff --git a/src/Data/Fin/Substitution/List.agda b/src/Data/Fin/Substitution/List.agda index 1ce9ee7340..ce5ff3e27c 100644 --- a/src/Data/Fin/Substitution/List.agda +++ b/src/Data/Fin/Substitution/List.agda @@ -7,7 +7,7 @@ -- This module illustrates how Data.Fin.Substitution.Lemmas.AppLemmas -- can be used. -{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} open import Data.Fin.Substitution.Lemmas open import Data.Nat.Base using (ℕ) @@ -17,19 +17,27 @@ module Data.Fin.Substitution.List {ℓ} {T : ℕ → Set ℓ} (lemmas₄ : Lemma open import Data.List.Base open import Data.List.Properties open import Data.Fin.Substitution -import Function as Fun +import Function.Base as Fun open import Relation.Binary.PropositionalEquality -open ≡-Reasoning private + variable + m n : ℕ + + ListT : ℕ → Set ℓ + ListT = List Fun.∘ T + open module L = Lemmas₄ lemmas₄ using (_/_; id; _⊙_) +------------------------------------------------------------------------ +-- Listwise application of a substitution, plus lemmas about it + infixl 8 _//_ -_//_ : ∀ {m n} → List (T m) → Sub T m n → List (T n) +_//_ : ListT m → Sub T m n → ListT n ts // ρ = map (λ σ → σ / ρ) ts -appLemmas : AppLemmas (λ n → List (T n)) T +appLemmas : AppLemmas ListT T appLemmas = record { application = record { _/_ = _//_ } ; lemmas₄ = lemmas₄ @@ -39,9 +47,9 @@ appLemmas = record ts ∎ ; /-⊙ = λ {_ _ _ ρ₁ ρ₂} ts → begin ts // ρ₁ ⊙ ρ₂ ≡⟨ map-cong L./-⊙ ts ⟩ - map (λ σ → σ / ρ₁ / ρ₂) ts ≡⟨ map-compose ts ⟩ + map (λ σ → σ / ρ₁ / ρ₂) ts ≡⟨ map-∘ ts ⟩ ts // ρ₁ // ρ₂ ∎ - } + } where open ≡-Reasoning open AppLemmas appLemmas public hiding (_/_) renaming (_/✶_ to _//✶_)