Another attempt at deprecation of inspect

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

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

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

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 ∷ _)

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                                 ∎)

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

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

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)
 

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⁻ _ _)

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

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) →

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."
+#-}
+