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.2.2.
 
 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.
+
+
 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.2.2.
 
 -- 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
@@ -266,6 +262,11 @@ import README.Text.Regex
 
 import README.Text.Tabular
 
+-- Explaining the `with ... in ...` syntax: use case, equivalent handwritten
+-- auxiliary definitions, and implementation details.
+
+import README.WithIn
+
 ------------------------------------------------------------------------
 -- All library modules
 ------------------------------------------------------------------------

README/Inspect.agda → README/WithIn.agda

@@ -1,21 +1,20 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Explaining how to use the inspect idiom and elaborating on the way
--- it is implemented in the standard library.
+-- Explaining how to use the `with ... in ...` idiom.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module README.Inspect where
+module README.WithIn where
 
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product
 open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------
--- Using inspect
+-- Using `with ... in ...`
 
 -- We start with the definition of a (silly) predicate: `Plus m n p` states
 -- that `m + n` is equal to `p` in a rather convoluted way. Crucially, it
@@ -60,8 +59,8 @@ plus-eq-+ (suc m) n      = refl
 -- when we would have wanted a more precise type of the form:
 -- `plus-eq-aux : ∀ m n p → m + n ≡ p → Plus-eq m n p`.
 
--- This is where we can use `inspect`. By using `with f x | inspect f x`,
--- we get both a `y` which is the result of `f x` and a proof that `f x ≡ y`.
+-- This is where we can use `with ... in ...`. By using `with f x in eq`, we get
+-- *both* a `y` which is the result of `f x` *and* a proof `eq` that `f x ≡ y`.
 -- Splitting on the result of `m + n`, we get two cases:
 
 -- 1. `m ≡ 0 × n ≡ 0` under the assumption that `m + n ≡ zero`
@@ -70,18 +69,20 @@ plus-eq-+ (suc m) n      = refl
 -- The first one can be discharged using lemmas from Data.Nat.Properties and
 -- the second one is trivial.
 
-plus-eq-with : ∀ m n → Plus-eq m n (m + n)
-plus-eq-with m n with m + n | inspect (m +_) n
-... | zero  | [ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
-... | suc p | [ m+n≡1+p ] = m+n≡1+p
+plus-eq-with-in : ∀ m n → Plus-eq m n (m + n)
+plus-eq-with-in m n with m + n in eq
+... | zero  = m+n≡0⇒m≡0 m eq , m+n≡0⇒n≡0 m eq
+... | suc p = eq
 
+-- NB. What has been lost? the new syntax binds `eq` once and for all,
+-- whereas the old `with ... inspect` syntax allowed pattern-matching on
+-- *different names* for the equation in each possible branch after a `with`.
 
 ------------------------------------------------------------------------
--- Understanding the implementation of inspect
+-- Understanding the implementation of `with ... in ...`
 
--- So why is it that we have to go through the record type `Reveal_·_is_`
--- and the ̀inspect` function? The fact is: we don't have to if we write
--- our own auxiliary lemma:
+-- What happens if we try to avoid use of the ̀with ... in ...` syntax?
+-- The fact is: we don't have to if we write our own auxiliary lemma:
 
 plus-eq-aux : ∀ m n → Plus-eq m n (m + n)
 plus-eq-aux m n = aux m n (m + n) refl where
@@ -90,43 +91,19 @@ plus-eq-aux m n = aux m n (m + n) refl where
   aux m n zero    m+n≡0   = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
   aux m n (suc p) m+n≡1+p = m+n≡1+p
 
--- The problem is that when we write ̀with f x | pr`, `with` decides to call `y`
--- the result `f x` and to replace *all* of the occurences of `f x` in the type
--- of `pr` with `y`. That is to say that if we were to write:
+-- NB. Here we can choose alternative names in each branch of `aux`
+-- for the proof of the auxiliary hypothesis `m + n ≡ p`
 
--- plus-eq-naïve : ∀ m n → Plus-eq m n (m + n)
--- plus-eq-naïve m n with m + n | refl {x = m + n}
--- ... | p | eq = {!!}
+-- We could likewise emulate the general behaviour of `with ... in ...`
+-- using an auxiliary function as follows, using the `with p ← ...` syntax
+-- to bind the subexpression `m + n` to (pattern) variable `p`:
 
--- then `with` would abstract `m + n` as `p` on *both* sides of the equality
--- proven by `refl` thus giving us the following goal with an extra, useless,
--- assumption:
+plus-eq-with-in-aux : ∀ m n → Plus-eq m n (m + n)
+plus-eq-with-in-aux m n with p ← m + n in eq = aux m n p eq where
 
--- 1. `Plus-eq m n p` under the assumption that `p ≡ p`
-
--- So how does `inspect` work? The standard library uses a more general version
--- of the following type and function:
-
-record MyReveal_·_is_ (f : ℕ → ℕ) (x y : ℕ) : Set where
-  constructor [_]
-  field eq : f x ≡ y
-
-my-inspect : ∀ f n → MyReveal f · n is (f n)
-my-inspect f n = [ refl ]
-
--- Given that `inspect` has the type `∀ f n → Reveal f · n is (f n)`, when we
--- write `with f n | inspect f n`, the only `f n` that can be abstracted in the
--- type of `inspect f n` is the third argument to `Reveal_·_is_`.
-
--- That is to say that the auxiliary definition generated looks like this:
-
-plus-eq-reveal : ∀ m n → Plus-eq m n (m + n)
-plus-eq-reveal m n = aux m n (m + n) (my-inspect (m +_) n) where
-
-  aux : ∀ m n p → MyReveal (m +_) · n is p → Plus-eq m n p
-  aux m n zero    [ m+n≡0   ] = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
-  aux m n (suc p) [ m+n≡1+p ] = m+n≡1+p
+  aux : ∀ m n p → m + n ≡ p → Plus-eq m n p
+  aux m n zero    m+n≡0   = m+n≡0⇒m≡0 m m+n≡0 , m+n≡0⇒n≡0 m m+n≡0
+  aux m n (suc p) m+n≡1+p = m+n≡1+p
 
--- At the cost of having to unwrap the constructor `[_]` around the equality
--- we care about, we can keep relying on `with` and avoid having to roll out
--- handwritten auxiliary definitions.
+-- That is, more or less, what the Agda-generated definition corresponding to
+-- `plus-eq-with-in` would look like.

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 EQ
+... | inj₁ k with refl ← eq = cong suc (splitAt⁻¹-↑ˡ {i = i} {j = k} EQ)
+
 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 EQ
+... | inj₂ k with refl ← eq = cong suc (splitAt⁻¹-↑ʳ {i = i} {j = k} EQ)
+
 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,13 +689,20 @@ 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                                 ∎)
   where open ≡-Reasoning
 
+combine-surjectiveNEW : ∀ (i : Fin (m ℕ.* n)) → ∃₂ λ j k → combine {m} {n} j k ≡ i
+combine-surjectiveNEW {m = suc m} {n} i with splitAt n i in eq
+... | inj₁ j rewrite splitAt-↑ˡ _ j (m ℕ.* n)
+    = zero , j , splitAt⁻¹-↑ˡ eq
+... | inj₂ k with (j₁ , k₁ , refl) ← combine-surjectiveNEW {m} {n} k
+    = suc j₁ , k₁ , splitAt⁻¹-↑ʳ eq
+
 ------------------------------------------------------------------------
 -- Bundles
 

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