diff --git a/CHANGELOG.md b/CHANGELOG.md index 76ca38cd42..36f8ee04b5 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 ---------- @@ -1298,6 +1298,15 @@ Deprecated names * This fixes the fact we had picked the wrong name originally. The erased modality corresponds to @0 whereas the irrelevance one corresponds to `.`. +### Deprecated `Relation.Binary.PropositionalEquality.inspect` + in favour of `with ... in ...` syntax (issue #1580; PRs #1630, #1930) + +* In `Relation.Binary.PropositionalEquality` + both the record type `Reveal_·_is_` + and its principal mode of use, `inspect`, + have been deprecated in favour of the new `with ... in ...` syntax. + See the documentation of [with-abstraction equality](https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality) + New modules ----------- @@ -1855,6 +1864,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 diff --git a/README.agda b/README.agda index 2d87cb56d2..6fee0aeffa 100644 --- a/README.agda +++ b/README.agda @@ -12,13 +12,14 @@ module README where -- Liang-Ting Chen, Dominique Devriese, Dan Doel, Érdi Gergő, -- Zack Grannan, Helmut Grohne, Simon Foster, Liyang Hu, Jason Hu, -- Patrik Jansson, Alan Jeffrey, Wen Kokke, Evgeny Kotelnikov, --- Sergei Meshveliani, Eric Mertens, Darin Morrison, Guilhem Moulin, --- Shin-Cheng Mu, Ulf Norell, Noriyuki Ohkawa, Nicolas Pouillard, --- Andrés Sicard-Ramírez, Lex van der Stoep, Sandro Stucki, Milo Turner, --- Noam Zeilberger and other anonymous contributors. +-- James McKinna, Sergei Meshveliani, Eric Mertens, Darin Morrison, +-- Guilhem Moulin, Shin-Cheng Mu, Ulf Norell, Noriyuki Ohkawa, +-- Nicolas Pouillard, Andrés Sicard-Ramírez, Lex van der Stoep, +-- Sandro Stucki, Milo Turner, Noam Zeilberger +-- and other anonymous contributors. ------------------------------------------------------------------------ --- This version of the library has been tested using Agda 2.6.2. +-- This version of the library has been tested using Agda 2.6.3. -- The library comes with a .agda-lib file, for use with the library -- management system. @@ -236,11 +237,6 @@ import README.Debug.Trace import README.Nary --- Explaining the inspect idiom: use case, equivalent handwritten --- auxiliary definitions, and implementation details. - -import README.Inspect - -- Explaining how to use the automatic solvers import README.Tactic.MonoidSolver diff --git a/README/Inspect.agda b/README/Inspect.agda index e10877c44c..cff492d008 100644 --- a/README/Inspect.agda +++ b/README/Inspect.agda @@ -1,14 +1,17 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Explaining how to use the inspect idiom and elaborating on the way --- it is implemented in the standard library. +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module README.Inspect where +{-# WARNING_ON_IMPORT +"README.Inspect was deprecated in v2.0." +#-} + open import Data.Nat.Base open import Data.Nat.Properties open import Data.Product diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda index 3de56a756a..dea697b088 100644 --- a/src/Codata/Sized/Colist/Properties.agda +++ b/src/Codata/Sized/Colist/Properties.agda @@ -144,10 +144,10 @@ module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where scanl-unfold : ∀ nil a → i ⊢ scanl cons nil (unfold alg a) ≈ nil ∷ (λ where .force → unfold alg′ (a , nil)) - scanl-unfold nil a with alg a | Eq.inspect alg a - ... | nothing | [ eq ] = Eq.refl ∷ λ { .force → + scanl-unfold nil a with alg a in eq + ... | nothing = Eq.refl ∷ λ { .force → sym (fromEq (unfold-nothing (Maybeₚ.map-nothing eq))) } - ... | just (a′ , b) | [ eq ] = Eq.refl ∷ λ { .force → begin + ... | just (a′ , b) = Eq.refl ∷ λ { .force → begin scanl cons (cons nil b) (unfold alg a′) ≈⟨ scanl-unfold (cons nil b) a′ ⟩ (cons nil b ∷ _) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 232a44a7bb..d7a963f9fd 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -562,10 +562,20 @@ splitAt-↑ˡ : ∀ m i n → splitAt m (i ↑ˡ n) ≡ inj₁ i splitAt-↑ˡ (suc m) zero n = refl splitAt-↑ˡ (suc m) (suc i) n rewrite splitAt-↑ˡ m i n = refl +splitAt⁻¹-↑ˡ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₁ j → j ↑ˡ n ≡ i +splitAt⁻¹-↑ˡ {suc m} {n} {0F} {.0F} refl = refl +splitAt⁻¹-↑ˡ {suc m} {n} {suc i} {j} eq with splitAt m i in splitAt[m][i]≡inj₁[j] +... | inj₁ k with refl ← eq = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} splitAt[m][i]≡inj₁[j]) + splitAt-↑ʳ : ∀ m n i → splitAt m (m ↑ʳ i) ≡ inj₂ {B = Fin n} i splitAt-↑ʳ zero n i = refl splitAt-↑ʳ (suc m) n i rewrite splitAt-↑ʳ m n i = refl +splitAt⁻¹-↑ʳ : ∀ {m} {n} {i} {j} → splitAt m {n} i ≡ inj₂ j → m ↑ʳ j ≡ i +splitAt⁻¹-↑ʳ {zero} {n} {i} {j} refl = refl +splitAt⁻¹-↑ʳ {suc m} {n} {suc i} {j} eq with splitAt m i in splitAt[m][i]≡inj₂[k] +... | inj₂ k with refl ← eq = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} splitAt[m][i]≡inj₂[k]) + splitAt-join : ∀ m n i → splitAt m (join m n i) ≡ i splitAt-join m n (inj₁ x) = splitAt-↑ˡ m x n splitAt-join m n (inj₂ y) = splitAt-↑ʳ m n y @@ -612,13 +622,13 @@ remQuot-combine {suc n} {k} (suc i) j rewrite splitAt-↑ʳ k (n ℕ.* k) (com cong (Data.Product.map₁ suc) (remQuot-combine i j) combine-remQuot : ∀ {n} k (i : Fin (n ℕ.* k)) → uncurry combine (remQuot {n} k i) ≡ i -combine-remQuot {suc n} k i with splitAt k i | P.inspect (splitAt k) i -... | inj₁ j | P.[ eq ] = begin +combine-remQuot {suc n} k i with splitAt k i in eq +... | inj₁ j = begin join k (n ℕ.* k) (inj₁ j) ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩ join k (n ℕ.* k) (splitAt k i) ≡⟨ join-splitAt k (n ℕ.* k) i ⟩ i ∎ where open ≡-Reasoning -... | inj₂ j | P.[ eq ] = begin +... | inj₂ j = begin k ↑ʳ (uncurry combine (remQuot {n} k j)) ≡⟨ cong (k ↑ʳ_) (combine-remQuot {n} k j) ⟩ join k (n ℕ.* k) (inj₂ j) ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩ join k (n ℕ.* k) (splitAt k i) ≡⟨ join-splitAt k (n ℕ.* k) i ⟩ @@ -679,8 +689,8 @@ combine-injective i j k l cᵢⱼ≡cₖₗ = combine-injectiveʳ i j k l cᵢⱼ≡cₖₗ combine-surjective : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine j k ≡ i -combine-surjective {m} {n} i with remQuot {m} n i | P.inspect (remQuot {m} n) i -... | j , k | P.[ eq ] = j , k , (begin +combine-surjective {m} {n} i with remQuot {m} n i in eq +... | j , k = j , k , (begin combine j k ≡˘⟨ uncurry (cong₂ combine) (,-injective eq) ⟩ uncurry combine (remQuot {m} n i) ≡⟨ combine-remQuot {m} n i ⟩ i ∎) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index d4008fce07..46e7c3f780 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -854,9 +854,9 @@ module _ {P : Pred A p} (P? : Decidable P) where filter-idem : filter P? ∘ filter P? ≗ filter P? filter-idem [] = refl - filter-idem (x ∷ xs) with does (P? x) | inspect does (P? x) - ... | false | _ = filter-idem xs - ... | true | P.[ eq ] rewrite eq = cong (x ∷_) (filter-idem xs) + filter-idem (x ∷ xs) with does (P? x) in eq + ... | false = filter-idem xs + ... | true rewrite eq = cong (x ∷_) (filter-idem xs) filter-++ : ∀ xs ys → filter P? (xs ++ ys) ≡ filter P? xs ++ filter P? ys filter-++ [] ys = refl diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index c9a8048592..158ade9563 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -29,7 +29,7 @@ open import Level using (Level) open import Relation.Unary using (Pred) open import Relation.Binary open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_ ; refl ; cong; cong₂; _≢_; inspect) + using (_≡_ ; refl ; cong; cong₂; _≢_) open import Relation.Nullary open PermutationReasoning diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 79ccfaadef..3483323844 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -37,7 +37,7 @@ open import Level using (Level; _⊔_) open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Properties.Setoid S using (≉-resp₂) open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_; inspect) + using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_) open import Relation.Nullary.Decidable using (yes; no; does) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index abfc8f93f8..6ac93bc05e 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -42,7 +42,7 @@ open import Function.Related as Related using (Kind; Related; SK-sym) open import Level using (Level) open import Relation.Binary as B hiding (_⇔_) open import Relation.Binary.PropositionalEquality as P - using (_≡_; refl; inspect) + using (_≡_; refl) open import Relation.Unary as U using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_) open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no) @@ -172,9 +172,9 @@ any⁺ p (there {x = x} pxs) with p x ... | false = any⁺ p pxs any⁻ : ∀ (p : A → Bool) xs → T (any p xs) → Any (T ∘ p) xs -any⁻ p (x ∷ xs) px∷xs with p x | inspect p x -... | true | P.[ eq ] = here (Equivalence.from T-≡ ⟨$⟩ eq) -... | false | _ = there (any⁻ p xs px∷xs) +any⁻ p (x ∷ xs) px∷xs with p x in eq +... | true = here (Equivalence.from T-≡ ⟨$⟩ eq) +... | false = there (any⁻ p xs px∷xs) any⇔ : ∀ {p : A → Bool} → Any (T ∘ p) xs ⇔ T (any p xs) any⇔ = equivalence (any⁺ _) (any⁻ _ _) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index b9d18fab34..f564ffe835 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -1304,24 +1304,24 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i ------------------------------------------------------------------------ p≤q⇒p⊔q≡q : p ≤ q → p ⊔ q ≡ q -p≤q⇒p⊔q≡q {p@record{}} {q@record{}} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | _ = refl -... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) +p≤q⇒p⊔q≡q {p@record{}} {q@record{}} p≤q with p ≤ᵇ q in p≰q +... | true = refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) p≥q⇒p⊔q≡p : p ≥ q → p ⊔ q ≡ p -p≥q⇒p⊔q≡p {p@record{}} {q@record{}} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | [ p≤q ] = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _)) -... | false | [ p≤q ] = refl +p≥q⇒p⊔q≡p {p@record{}} {q@record{}} p≥q with p ≤ᵇ q in p≤q +... | true = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _)) +... | false = refl p≤q⇒p⊓q≡p : p ≤ q → p ⊓ q ≡ p -p≤q⇒p⊓q≡p {p@record{}} {q@record{}} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | _ = refl -... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) +p≤q⇒p⊓q≡p {p@record{}} {q@record{}} p≤q with p ≤ᵇ q in p≰q +... | true = refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) p≥q⇒p⊓q≡q : p ≥ q → p ⊓ q ≡ q -p≥q⇒p⊓q≡q {p@record{}} {q@record{}} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | [ p≤q ] = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q -... | false | [ p≤q ] = refl +p≥q⇒p⊓q≡q {p@record{}} {q@record{}} p≥q with p ≤ᵇ q in p≤q +... | true = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q +... | false = refl ⊓-operator : MinOperator ≤-totalPreorder ⊓-operator = record diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda index 060f917782..5b3eab5fa1 100644 --- a/src/Data/Vec/Relation/Unary/Any/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda @@ -333,12 +333,12 @@ module _ {P : Pred A p} where concat⁺∘concat⁻ : ∀ {n m} (xss : Vec (Vec A n) m) (p : Any P (concat xss)) → concat⁺ (concat⁻ xss p) ≡ p - concat⁺∘concat⁻ (xs ∷ xss) p with ++⁻ xs p | P.inspect (++⁻ xs) p - ... | inj₁ pxs | P.[ p=inj₁ ] - = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym p=inj₁)) + concat⁺∘concat⁻ (xs ∷ xss) p with ++⁻ xs p in eq + ... | inj₁ pxs + = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym eq)) $ ++⁺∘++⁻ xs p - ... | inj₂ pxss | P.[ p=inj₂ ] rewrite concat⁺∘concat⁻ xss pxss - = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym p=inj₂)) + ... | inj₂ pxss rewrite concat⁺∘concat⁻ xss pxss + = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym eq)) $ ++⁺∘++⁻ xs p concat⁻∘concat⁺ : ∀ {n m} {xss : Vec (Vec A n) m} (p : Any (Any P) xss) → diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index c9e2d102fd..4764635449 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -60,24 +60,6 @@ _≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B) (A → Setoid.Carrier B) → setoid A ⟶ B →-to-⟶ = :→-to-Π ------------------------------------------------------------------------- --- Inspect - --- Inspect can be used when you want to pattern match on the result r --- of some expression e, and you also need to "remember" that r ≡ e. - --- See README.Inspect for an explanation of how/why to use this. - -record Reveal_·_is_ {A : Set a} {B : A → Set b} - (f : (x : A) → B x) (x : A) (y : B x) : - Set (a ⊔ b) where - constructor [_] - field eq : f x ≡ y - -inspect : ∀ {A : Set a} {B : A → Set b} - (f : (x : A) → B x) (x : A) → Reveal f · x is f x -inspect f x = [ refl ] - ------------------------------------------------------------------------ -- Propositionality @@ -120,3 +102,34 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where ≢-≟-identity : (x≢y : x ≢ y) → x ≟ y ≡ no x≢y ≢-≟-identity = dec-no (x ≟ y) + + + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +record Reveal_·_is_ {A : Set a} {B : A → Set b} + (f : (x : A) → B x) (x : A) (y : B x) : + Set (a ⊔ b) where + constructor [_] + field eq : f x ≡ y + +inspect : ∀ {A : Set a} {B : A → Set b} + (f : (x : A) → B x) (x : A) → Reveal f · x is f x +inspect f x = [ refl ] + +{-# WARNING_ON_USAGE Reveal_·_is_ +"Warning: Reveal_·_is_ was deprecated in v2.0. +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead." +#-} +{-# WARNING_ON_USAGE inspect +"Warning: inspect was deprecated in v2.0. +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead." +#-} +