Changes explicit argument y to implicit in Induction.WellFounded.WfRec (#2084)

Author: jamesmckinna

CHANGELOG.md

@@ -585,6 +585,21 @@ Non-backwards compatible changes
   Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
   ```
 
+### Change to the definition of `Induction.WellFounded.WfRec` (issue #2083)
+
+* Previously, the following definition was adopted
+  ```agda
+  WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
+  WfRec _<_ P x = ∀ y → y < x → P y
+  ```
+  with the consequence that all arguments involving about accesibility and
+  wellfoundedness proofs were polluted by almost-always-inferrable explicit
+  arguments for the `y` position. The definition has now been changed to
+  make that argument *implicit*, as 
+  ```agda
+  WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
+  WfRec _<_ P x = ∀ {y} → y < x → P y
+
 ### Change in the definition of `_≤″_` (issue #1919)
 
 * The definition of `_≤″_` in `Data.Nat.Base` was previously:

README/Data/Nat/Induction.agda

@@ -14,6 +14,14 @@ open import Function.Base using (_∘_)
 open import Induction.WellFounded
 open import Relation.Binary.PropositionalEquality
 
+private
+
+  n<′1+n : ∀ {n} → n <′ suc n
+  n<′1+n = ≤′-refl
+
+  n<′2+n : ∀ {n} → n <′ suc (suc n)
+  n<′2+n = ≤′-step ≤′-refl
+
 -- Doubles its input.
 
 twice : ℕ → ℕ
@@ -46,7 +54,7 @@ mutual
   half₂-step = λ
     { zero          _   → zero
     ; (suc zero)    _   → zero
-    ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl))
+    ; (suc (suc n)) rec → suc (rec n<′2+n)
     }
 
   half₂ : ℕ → ℕ
@@ -92,21 +100,21 @@ half₂-2+ n = begin
 
   half₂-step (2 + n) (<′-recBuilder _ half₂-step (2 + n))     ≡⟨⟩
 
-  1 + <′-recBuilder _ half₂-step (2 + n) n (≤′-step ≤′-refl)  ≡⟨⟩
+  1 + <′-recBuilder _ half₂-step (2 + n) n<′2+n  ≡⟨⟩
 
   1 + Some.wfRecBuilder _ half₂-step (2 + n)
-        (<′-wellFounded (2 + n)) n (≤′-step ≤′-refl)          ≡⟨⟩
+        (<′-wellFounded (2 + n)) n<′2+n          ≡⟨⟩
 
   1 + Some.wfRecBuilder _ half₂-step (2 + n)
-        (acc (<′-wellFounded′ (2 + n))) n (≤′-step ≤′-refl)   ≡⟨⟩
+        (acc (<′-wellFounded′ (2 + n))) n<′2+n   ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n
-           (<′-wellFounded′ (2 + n) n (≤′-step ≤′-refl)))     ≡⟨⟩
+           (<′-wellFounded′ (2 + n) n<′2+n))     ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n
-           (<′-wellFounded′ (1 + n) n ≤′-refl))               ≡⟨⟩
+           (<′-wellFounded′ (1 + n) n<′1+n))               ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩
@@ -146,14 +154,14 @@ half₁-+₂ = <′-rec _ λ
   { zero          _   → refl
   ; (suc zero)    _   → refl
   ; (suc (suc n)) rec →
-      cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
+      cong (suc ∘ suc) (rec n<′2+n)
   }
 
 half₂-+₂ : ∀ n → half₂ (twice n) ≡ n
 half₂-+₂ = <′-rec _ λ
   { zero          _   → refl
   ; (suc zero)    _   → refl
   ; (suc (suc n)) rec →
-      cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
+      cong (suc ∘ suc) (rec n<′2+n)
   }
 

src/Codata/Musical/Colist/Infinite-merge.agda

@@ -195,7 +195,7 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂
     ... | inj₂ q | P.refl | q≤p =
       Prod.map there
                (P.cong (there ∘ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
-               (rec (♭ xss , q) (s≤′s q≤p))
+               (rec (s≤′s q≤p))
 
   to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p)))
 

src/Data/Bool/Properties.agda

@@ -195,8 +195,8 @@ true  <? _     = no  (λ())
 <-wellFounded : WellFounded _<_
 <-wellFounded _ = acc <-acc
   where
-    <-acc : ∀ {x} y → y < x → Acc _<_ y
-    <-acc false f<t = acc (λ _ → λ())
+    <-acc : ∀ {x y} → y < x → Acc _<_ y
+    <-acc f<t = acc λ ()
 
 -- Structures
 

src/Data/Digit.agda

@@ -56,7 +56,7 @@ toNatDigits base@(suc (suc _)) n = aux (<-wellFounded-fast n) []
   aux {zero}        _      xs =  (0 ∷ xs)
   aux {n@(suc _)} (acc wf) xs with does (0 <? n / base)
   ... | false = (n % base) ∷ xs
-  ... | true  = aux (wf (n / base) q<n) ((n % base) ∷ xs)
+  ... | true  = aux (wf q<n) ((n % base) ∷ xs)
     where
     q<n : n / base < n
     q<n = m/n<m n base (s<s z<s)
@@ -107,9 +107,8 @@ toDigits base@(suc (suc k)) n = <′-rec Pred helper n
 
   helper : ∀ n → <′-Rec Pred n → Pred n
   helper n                       rec with n divMod base
-  helper .(toℕ r + 0     * base) rec | result zero    r refl = ([ r ] , refl)
-  helper .(toℕ r + suc x * base) rec | result (suc x) r refl =
-    cons r (rec (suc x) (lem x k (toℕ r)))
+  ... | result zero    r eq = ([ r ] , P.sym eq)
+  ... | result (suc x) r refl = cons r (rec (lem x k (toℕ r)))
 
 ------------------------------------------------------------------------
 -- Showing digits

src/Data/Fin/Induction.agda

@@ -65,7 +65,7 @@ open WF public using (Acc; acc)
   induct {suc j} (acc rs) (tri< (s≤s i≤j) _ _) _ = Pᵢ⇒Pᵢ₊₁ j P[1+j]
     where
     toℕj≡toℕinjJ = sym $ toℕ-inject₁ j
-    P[1+j] = induct (rs _ (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
+    P[1+j] = induct (rs (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
       (<-cmp i $ inject₁ j) (subst (toℕ i ℕ.≤_) toℕj≡toℕinjJ i≤j)
 
 <-weakInduction : (P : Pred (Fin (suc n)) ℓ) →
@@ -80,8 +80,7 @@ open WF public using (Acc; acc)
 
 private
   acc-map : ∀ {x : Fin n} → Acc ℕ._<_ (n ∸ toℕ x) → Acc _>_ x
-  acc-map {n} (acc rs) = acc λ y y>x →
-    acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y)))
+  acc-map (acc rs) = acc λ y>x → acc-map (rs (ℕ.∸-monoʳ-< y>x (toℕ≤n _)))
 
 >-wellFounded : WellFounded {A = Fin n} _>_
 >-wellFounded {n} x = acc-map (ℕ.<-wellFounded (n ∸ toℕ x))
@@ -96,7 +95,7 @@ private
   induct {i} (acc rec) with n ℕ.≟ toℕ i
   ... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ
   ... | no  n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁)
-    where Pᵢ₊₁ = induct (rec _ (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
+    where Pᵢ₊₁ = induct (rec (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
 
 ------------------------------------------------------------------------
 -- Well-foundedness of other (strict) partial orders on Fin
@@ -112,20 +111,20 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
 
   spo-wellFounded : ∀ {r} {_⊏_ : Rel (Fin n) r} →
                     IsStrictPartialOrder _≈_ _⊏_ → WellFounded _⊏_
-  spo-wellFounded {_} {_⊏_} isSPO i = go n i pigeon where
+  spo-wellFounded {_} {_⊏_} isSPO i = go n pigeon where
 
     module ⊏ = IsStrictPartialOrder isSPO
 
-    go : ∀ m i →
-         ((xs : Vec (Fin n) m) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_) →
+    go : ∀ m {i} →
+         ({xs : Vec (Fin n) m} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_) →
          Acc _⊏_ i
-    go zero    i k = k [] [-] i
-    go (suc m) i k = acc $ λ j j⊏i → go m j (λ xs i∷xs↑ → k (j ∷ xs) (j⊏i ∷ i∷xs↑))
+    go zero    k = k [-] _
+    go (suc m) k = acc λ j⊏i → go m λ i∷xs↑ → k (j⊏i ∷ i∷xs↑)
 
-    pigeon : (xs : Vec (Fin n) n) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
-    pigeon xs i∷xs↑ =
+    pigeon : {xs : Vec (Fin n) n} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
+    pigeon {xs} i∷xs↑ =
       let (i₁ , i₂ , i₁<i₂ , xs[i₁]≡xs[i₂]) = pigeonhole (n<1+n n) (Vec.lookup (i ∷ xs)) in
-      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) {xs = i ∷ xs} i∷xs↑ i₁<i₂ in
+      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) i∷xs↑ i₁<i₂ in
       let xs[i₁]⊏xs[i₁] = ⊏.<-respʳ-≈ (⊏.Eq.reflexive xs[i₁]≡xs[i₂]) xs[i₁]⊏xs[i₂] in
       contradiction xs[i₁]⊏xs[i₁] (⊏.irrefl ⊏.Eq.refl)
 

src/Data/Graph/Acyclic.agda

@@ -313,7 +313,7 @@ module _ {ℓ e} {N : Set ℓ} {E : Set e} where
     expand n rec (c & g) =
       node (label c)
            (List.map
-              (Prod.map id (λ i → rec (n - suc i) (lemma n i) (g [ i ])))
+              (Prod.map id (λ i → rec (lemma n i) (g [ i ])))
               (successors c))
 
 -- Performs the toTree expansion once for each node.

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -384,15 +384,15 @@ split v as bs p = helper as bs p (<-wellFounded (steps p))
   helper (a ∷ [])     bs (refl eq)    _ = [ a ]      , bs , eq
   helper (a ∷ b ∷ as) bs (refl eq)    _ = a ∷ b ∷ as , bs , eq
   helper []           bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl
-  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
+  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
   ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂
   helper [] (b ∷ bs)     (swap x≈b y≈v _) _ = [ b ] , _     , x≈b ∷ y≈v ∷ ≋-refl
   helper (a ∷ [])     bs (swap x≈v y≈a ↭) _ = []    , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl
-  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
+  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
   ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq
-  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec _ (m<n+m (steps ↭₂) (0<steps ↭₁)))
+  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec (m<n+m (steps ↭₂) (0<steps ↭₁)))
   ... | (ps , qs , eq) = helper ps qs (↭-respʳ-≋ eq ↭₁)
-    (rec _ (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
+      (rec (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
 
 ------------------------------------------------------------------------
 -- filter

src/Data/List/Sort/MergeSort.agda

@@ -44,20 +44,21 @@ open PermutationReasoning
 -- Definition
 
 mergePairs : List (List A) → List (List A)
-mergePairs (xs ∷ ys ∷ xss) = merge _≤?_ xs ys ∷ mergePairs xss
+mergePairs (xs ∷ ys ∷ yss) = merge _≤?_ xs ys ∷ mergePairs yss
 mergePairs xss             = xss
 
 private
-  length-mergePairs : ∀ xs ys xss → length (mergePairs (xs ∷ ys ∷ xss)) < length (xs ∷ ys ∷ xss)
+  length-mergePairs : ∀ xs ys yss → let zss = xs ∷ ys ∷ yss in
+                      length (mergePairs zss) < length zss
   length-mergePairs _ _ []              = s<s z<s
-  length-mergePairs _ _ (xss ∷ [])      = s<s (s<s z<s)
-  length-mergePairs _ _ (xs ∷ ys ∷ xss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys xss))
+  length-mergePairs _ _ (xs ∷ [])       = s<s (s<s z<s)
+  length-mergePairs _ _ (xs ∷ ys ∷ yss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys yss))
 
 mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
 mergeAll []        _               = []
 mergeAll (xs ∷ []) _               = xs
-mergeAll (xs ∷ ys ∷ xss) (acc rec) = mergeAll
-  (mergePairs (xs ∷ ys ∷ xss)) (rec _ (length-mergePairs xs ys xss))
+mergeAll xss@(xs ∷ ys ∷ yss) (acc rec) = mergeAll
+  (mergePairs xss) (rec (length-mergePairs xs ys yss))
 
 sort : List A → List A
 sort xs = mergeAll (map [_] xs) (<-wellFounded-fast _)

src/Data/Nat/DivMod.agda

@@ -294,7 +294,7 @@ m*n/m*o≡n/o m@(suc _) n o = helper (<-wellFounded n)
   ... | no  n≮o = begin-equality
     (m * n) / (m * o)             ≡⟨  m/n≡1+[m∸n]/n (*-monoʳ-≤ m (≮⇒≥ n≮o)) ⟩
     1 + (m * n ∸ m * o) / (m * o) ≡˘⟨ cong (λ v → 1 + v / (m * o)) (*-distribˡ-∸ m n o) ⟩
-    1 + (m * (n ∸ o)) / (m * o)   ≡⟨  cong suc (helper (rec (n ∸ o) n∸o<n)) ⟩
+    1 + (m * (n ∸ o)) / (m * o)   ≡⟨  cong suc (helper (rec n∸o<n)) ⟩
     1 + (n ∸ o) / o               ≡˘⟨ cong₂ _+_ (n/n≡1 o) refl ⟩
     o / o + (n ∸ o) / o           ≡˘⟨ +-distrib-/-∣ˡ (n ∸ o) (divides 1 ((sym (*-identityˡ o)))) ⟩
     (o + (n ∸ o)) / o             ≡⟨  cong (_/ o) (m+[n∸m]≡n (≮⇒≥ n≮o)) ⟩