From 2b210caba30b3ce95f46228ab93b48666f32a155 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 10 Sep 2023 10:09:23 +0100 Subject: [PATCH 01/20] fixes #2083 --- CHANGELOG.md | 16 ++++++ README/Data/Nat/Induction.agda | 16 +++--- src/Codata/Musical/Colist/Infinite-merge.agda | 4 +- src/Data/Bool/Properties.agda | 4 +- src/Data/Digit.agda | 7 ++- src/Data/Fin/Induction.agda | 12 ++--- src/Data/Graph/Acyclic.agda | 2 +- .../Binary/Permutation/Setoid/Properties.agda | 17 +++--- src/Data/List/Sort/MergeSort.agda | 12 ++--- src/Data/Nat/DivMod.agda | 2 +- src/Data/Nat/GCD.agda | 26 +++++----- src/Data/Nat/Induction.agda | 10 ++-- src/Data/Nat/Logarithm/Core.agda | 4 +- src/Data/Nat/Properties.agda | 2 +- .../Product/Relation/Binary/Lex/Strict.agda | 8 +-- src/Data/Vec/Relation/Binary/Lex/Strict.agda | 2 +- src/Induction/WellFounded.agda | 51 +++++++++--------- .../Binary/Construct/Closure/Transitive.agda | 8 +-- src/Relation/Binary/Construct/On.agda | 2 +- src/Relation/Binary/Rewriting.agda | 6 +-- .../RingSolver/Core/Polynomial/Base.agda | 14 ++--- .../Homomorphism/Multiplication.agda | 52 +++++++++---------- .../Polynomial/Homomorphism/Negation.agda | 8 +-- 23 files changed, 151 insertions(+), 134 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 812fe00b6c..972091eb83 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -551,6 +551,22 @@ 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-aways-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 + ``` + ### Renaming of `Reflection` modules * Under the `Reflection` module, there were various impending name clashes diff --git a/README/Data/Nat/Induction.agda b/README/Data/Nat/Induction.agda index 52b802b2b8..b96b75baaf 100644 --- a/README/Data/Nat/Induction.agda +++ b/README/Data/Nat/Induction.agda @@ -46,7 +46,7 @@ mutual half₂-step = λ { zero _ → zero ; (suc zero) _ → zero - ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl)) + ; (suc (suc n)) rec → suc (rec (≤′-step ≤′-refl)) } half₂ : ℕ → ℕ @@ -92,21 +92,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) (≤′-step ≤′-refl) ≡⟨⟩ 1 + Some.wfRecBuilder _ half₂-step (2 + n) - (<′-wellFounded (2 + n)) n (≤′-step ≤′-refl) ≡⟨⟩ + (<′-wellFounded (2 + n)) (≤′-step ≤′-refl) ≡⟨⟩ 1 + Some.wfRecBuilder _ half₂-step (2 + n) - (acc (<′-wellFounded′ (2 + n))) n (≤′-step ≤′-refl) ≡⟨⟩ + (acc (<′-wellFounded′ (2 + n))) (≤′-step ≤′-refl) ≡⟨⟩ 1 + half₂-step n (Some.wfRecBuilder _ half₂-step n - (<′-wellFounded′ (2 + n) n (≤′-step ≤′-refl))) ≡⟨⟩ + (<′-wellFounded′ (2 + n) (≤′-step ≤′-refl))) ≡⟨⟩ 1 + half₂-step n (Some.wfRecBuilder _ half₂-step n - (<′-wellFounded′ (1 + n) n ≤′-refl)) ≡⟨⟩ + (<′-wellFounded′ (1 + n) ≤′-refl)) ≡⟨⟩ 1 + half₂-step n (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩ @@ -146,7 +146,7 @@ half₁-+₂ = <′-rec _ λ { zero _ → refl ; (suc zero) _ → refl ; (suc (suc n)) rec → - cong (suc ∘ suc) (rec n (≤′-step ≤′-refl)) + cong (suc ∘ suc) (rec (≤′-step ≤′-refl)) } half₂-+₂ : ∀ n → half₂ (twice n) ≡ n @@ -154,6 +154,6 @@ half₂-+₂ = <′-rec _ λ { zero _ → refl ; (suc zero) _ → refl ; (suc (suc n)) rec → - cong (suc ∘ suc) (rec n (≤′-step ≤′-refl)) + cong (suc ∘ suc) (rec (≤′-step ≤′-refl)) } diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda index eb06c3b9cc..00448c5cd0 100644 --- a/src/Codata/Musical/Colist/Infinite-merge.agda +++ b/src/Codata/Musical/Colist/Infinite-merge.agda @@ -178,7 +178,7 @@ module _ {a p} {A : Set a} {P : A → Set p} where to : ∀ xss p → Pred (xss , p) to = λ xss p → - WF.All.wfRec (On.wellFounded size <′-wellFounded) _ + WF.All.wfRec (On.wellFounded size <′-wellFounded) Pred step (xss , p) where size : Input → ℕ @@ -195,7 +195,7 @@ module _ {a p} {A : Set a} {P : A → Set p} where ... | 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 {♭ xss , q} (s≤′s q≤p)) to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p))) diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index ea22a37f68..0d799bb3e5 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -197,8 +197,8 @@ true _ x - acc-map {n} (acc rs) = acc λ y y>x → - acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y))) + acc-map {n} (acc rs) = acc λ {y} y>x → + acc-map (rs {n ∸ toℕ y} (ℕ.∸-monoʳ-< y>x (toℕ≤n y))) >-wellFounded : WellFounded {A = Fin n} _>_ >-wellFounded {n} x = acc-map (ℕ.<-wellFounded (n ∸ toℕ x)) @@ -94,7 +94,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 @@ -118,7 +118,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where ((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 (suc m) i k = acc λ {j} j⊏i → go m j (λ xs i∷xs↑ → k (j ∷ xs) (j⊏i ∷ i∷xs↑)) pigeon : (xs : Vec (Fin n) n) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_ pigeon xs i∷xs↑ = @@ -159,7 +159,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where ≺-wellFounded = Subrelation.wellFounded ≺⇒<′ ℕ.<′-wellFounded module _ {ℓ} where - open WF.All ≺-wellFounded ℓ public + open WF.All ≺-wellFounded {ℓ} public renaming ( wfRecBuilder to ≺-recBuilder ; wfRec to ≺-rec diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda index d40d078bd3..662cd8420c 100644 --- a/src/Data/Graph/Acyclic.agda +++ b/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 {n - suc i} (lemma n i) (g [ i ]))) (successors c)) -- Performs the toTree expansion once for each node. diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 57233a7b2a..5d3f43a1ff 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -384,15 +384,18 @@ 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) - ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂ + helper (a ∷ as) bs (prep eq as↭xs) (acc rec) + with ps , qs , eq₂ ← helper as bs as↭xs (rec (n<1+n _)) + = 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) - ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq - helper as bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec _ (m Date: Sun, 10 Sep 2023 11:09:24 +0100 Subject: [PATCH 02/20] almost removed one more instance: up to coupling with #2085 --- src/Data/Vec/Relation/Binary/Lex/Strict.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda index eba959ae43..d74ca541dd 100644 --- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda @@ -128,7 +128,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where where <-wellFounded : ∀ {n} → WellFounded (_<_ {n}) - <-wellFounded {0} [] = acc λ {ys} ys<[] → ⊥-elim (xs≮[] ys ys<[]) + <-wellFounded {0} [] = acc λ ys<[] → ⊥-elim (xs≮[] _ ys<[]) <-wellFounded {suc n} xs = Subrelation.wellFounded <⇒uncons-Lex uncons-Lex-wellFounded xs where <⇒uncons-Lex : {xs ys : Vec A (suc n)} → xs < ys → (×-Lex _≈_ _≺_ _<_ on uncons) xs ys From 41810268e95c7000a48d6f8c9e9b9db13137fff1 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 10 Sep 2023 19:00:47 +0100 Subject: [PATCH 03/20] typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 972091eb83..b1493a3244 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -559,7 +559,7 @@ Non-backwards compatible changes WfRec _<_ P x = ∀ y → y < x → P y ``` with the consequence that all arguments involving about accesibility and - wellfoundedness proofs were polluted by almost-aways-inferrable explicit + 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 From da9289e11adaa786043f0bc46b2ed3cf7a9b4859 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 10 Sep 2023 19:01:18 +0100 Subject: [PATCH 04/20] added more explanatory lemma --- README/Data/Nat/Induction.agda | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/README/Data/Nat/Induction.agda b/README/Data/Nat/Induction.agda index b96b75baaf..b4ebf081a9 100644 --- a/README/Data/Nat/Induction.agda +++ b/README/Data/Nat/Induction.agda @@ -14,6 +14,11 @@ open import Function.Base using (_∘_) open import Induction.WellFounded open import Relation.Binary.PropositionalEquality +private + + n<′2+n : ∀ {n} → n <′ suc (suc n) + n<′2+n = ≤′-step ≤′-refl + -- Doubles its input. twice : ℕ → ℕ @@ -46,7 +51,7 @@ mutual half₂-step = λ { zero _ → zero ; (suc zero) _ → zero - ; (suc (suc n)) rec → suc (rec (≤′-step ≤′-refl)) + ; (suc (suc n)) rec → suc (rec n<′2+n) } half₂ : ℕ → ℕ @@ -92,17 +97,17 @@ half₂-2+ n = begin half₂-step (2 + n) (<′-recBuilder _ half₂-step (2 + n)) ≡⟨⟩ - 1 + <′-recBuilder _ half₂-step (2 + n) (≤′-step ≤′-refl) ≡⟨⟩ + 1 + <′-recBuilder _ half₂-step (2 + n) n<′2+n ≡⟨⟩ 1 + Some.wfRecBuilder _ half₂-step (2 + n) - (<′-wellFounded (2 + n)) (≤′-step ≤′-refl) ≡⟨⟩ + (<′-wellFounded (2 + n)) n<′2+n ≡⟨⟩ 1 + Some.wfRecBuilder _ half₂-step (2 + n) - (acc (<′-wellFounded′ (2 + n))) (≤′-step ≤′-refl) ≡⟨⟩ + (acc (<′-wellFounded′ (2 + n))) n<′2+n ≡⟨⟩ 1 + half₂-step n (Some.wfRecBuilder _ half₂-step n - (<′-wellFounded′ (2 + n) (≤′-step ≤′-refl))) ≡⟨⟩ + (<′-wellFounded′ (2 + n) n<′2+n)) ≡⟨⟩ 1 + half₂-step n (Some.wfRecBuilder _ half₂-step n @@ -146,7 +151,7 @@ half₁-+₂ = <′-rec _ λ { zero _ → refl ; (suc zero) _ → refl ; (suc (suc n)) rec → - cong (suc ∘ suc) (rec (≤′-step ≤′-refl)) + cong (suc ∘ suc) (rec n<′2+n) } half₂-+₂ : ∀ n → half₂ (twice n) ≡ n @@ -154,6 +159,6 @@ half₂-+₂ = <′-rec _ λ { zero _ → refl ; (suc zero) _ → refl ; (suc (suc n)) rec → - cong (suc ∘ suc) (rec (≤′-step ≤′-refl)) + cong (suc ∘ suc) (rec n<′2+n) } From 7e62e53f6ae155ee91b3d11062cd7b04ac0a12d7 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 10 Sep 2023 19:04:38 +0100 Subject: [PATCH 05/20] added another more explanatory lemma --- README/Data/Nat/Induction.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README/Data/Nat/Induction.agda b/README/Data/Nat/Induction.agda index b4ebf081a9..6f47ddc07f 100644 --- a/README/Data/Nat/Induction.agda +++ b/README/Data/Nat/Induction.agda @@ -16,6 +16,9 @@ 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 @@ -111,7 +114,7 @@ half₂-2+ n = begin 1 + half₂-step n (Some.wfRecBuilder _ half₂-step n - (<′-wellFounded′ (1 + n) ≤′-refl)) ≡⟨⟩ + (<′-wellFounded′ (1 + n) n<′1+n)) ≡⟨⟩ 1 + half₂-step n (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩ From 68759071ddb8f3ef5ac15a8da693dd972dd42303 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 11 Sep 2023 14:59:23 +0100 Subject: [PATCH 06/20] DRY: definitionally equivalent type for `acc-inverse` --- src/Induction/WellFounded.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda index 747afdb19f..d64fe1dcc8 100644 --- a/src/Induction/WellFounded.agda +++ b/src/Induction/WellFounded.agda @@ -51,7 +51,7 @@ WellFounded _<_ = ∀ x → Acc _<_ x -- Basic properties acc-inverse : ∀ {_<_ : Rel A ℓ} {x : A} (q : Acc _<_ x) → - ∀ {y} → y < x → Acc _<_ y + WfRec _<_ (Acc _<_) x acc-inverse (acc rs) y Date: Wed, 13 Sep 2023 08:13:30 +0100 Subject: [PATCH 07/20] this instance is also eliminable! --- src/Data/Product/Relation/Binary/Lex/Strict.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index ac2bc26ce8..96adc9b9e1 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda @@ -202,8 +202,8 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ ×-acc : ∀ {x y} → Acc _<₁_ x → Acc _<₂_ y → WfRec _<ₗₑₓ_ (Acc _<ₗₑₓ_) (x , y) - ×-acc (acc rec₁) acc₂ {u , v} (inj₁ u Date: Wed, 13 Sep 2023 08:33:12 +0100 Subject: [PATCH 08/20] this instance is also eliminable! --- src/Data/Fin/Induction.agda | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index f2d8f240ff..bbcaa08562 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -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 {n} (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)) @@ -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₁ Date: Wed, 13 Sep 2023 08:35:18 +0100 Subject: [PATCH 09/20] tidying up --- src/Data/Fin/Induction.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index bbcaa08562..88bbcc3227 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -80,7 +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>x → acc-map (rs (ℕ.∸-monoʳ-< y>x (toℕ≤n _))) + 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)) From bf85de408d3a309ffe5db64fe64aa1d4658f563c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 13 Sep 2023 08:40:00 +0100 Subject: [PATCH 10/20] tidying up: redundant parentheses --- src/Induction/WellFounded.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda index 9c75c864e7..a5b67051f8 100644 --- a/src/Induction/WellFounded.agda +++ b/src/Induction/WellFounded.agda @@ -75,7 +75,7 @@ module Some {_<_ : Rel A r} {ℓ} where wfRec = subsetBuild wfRecBuilder unfold-wfRec : (P : Pred A ℓ) (f : WfRec _<_ P ⊆′ P) {x : A} (q : Acc _<_ x) → - wfRec P f x q ≡ f x (λ y Date: Wed, 13 Sep 2023 08:51:50 +0100 Subject: [PATCH 11/20] easy pickings --- src/Data/Graph/Acyclic.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda index 662cd8420c..db9c7286fa 100644 --- a/src/Data/Graph/Acyclic.agda +++ b/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. From e8b6d2fb71123534f64688eae6497173bdde6d9b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 13 Sep 2023 08:52:22 +0100 Subject: [PATCH 12/20] this one, of all things, as wellgit add src/Codata/Musical/Colist/Infinite-merge.agda! --- src/Codata/Musical/Colist/Infinite-merge.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda index 00448c5cd0..aa3286eeb0 100644 --- a/src/Codata/Musical/Colist/Infinite-merge.agda +++ b/src/Codata/Musical/Colist/Infinite-merge.agda @@ -195,7 +195,7 @@ module _ {a p} {A : Set a} {P : A → Set p} where ... | 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 {- {♭ xss , q} -} (s≤′s q≤p)) to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p))) From 6ef65e750e4180ebac4a66252fba512cc2e64a93 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 13 Sep 2023 09:35:57 +0100 Subject: [PATCH 13/20] tidying up --- src/Data/List/Sort/MergeSort.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda index 089b7289dc..9abab0823e 100644 --- a/src/Data/List/Sort/MergeSort.agda +++ b/src/Data/List/Sort/MergeSort.agda @@ -48,7 +48,8 @@ mergePairs (xs ∷ ys ∷ yss) = merge _≤?_ xs ys ∷ mergePairs yss mergePairs xss = xss private - length-mergePairs : ∀ xs ys yss → length (mergePairs (xs ∷ ys ∷ yss)) < length (xs ∷ ys ∷ yss) + length-mergePairs : ∀ xs ys yss → let zss = xs ∷ ys ∷ yss in + length (mergePairs zss) < length zss length-mergePairs _ _ [] = s Date: Wed, 13 Sep 2023 09:37:43 +0100 Subject: [PATCH 14/20] tidying up --- src/Data/Nat/Induction.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Induction.agda b/src/Data/Nat/Induction.agda index e3ea9920a6..60076462a8 100644 --- a/src/Data/Nat/Induction.agda +++ b/src/Data/Nat/Induction.agda @@ -100,7 +100,7 @@ module _ {ℓ : Level} where <-wellFounded-skip : ∀ (k : ℕ) → WellFounded _<_ <-wellFounded-skip zero n = <-wellFounded n <-wellFounded-skip (suc k) zero = <-wellFounded 0 - <-wellFounded-skip (suc k) (suc n) = acc (λ {m} _ → <-wellFounded-skip k m) + <-wellFounded-skip (suc k) (suc n) = acc λ {m} _ → <-wellFounded-skip k m module _ {ℓ : Level} where open WF.All <-wellFounded {ℓ} public From 267821f706cdffc540e7baf66eb8425c3dd42766 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 09:40:26 +0100 Subject: [PATCH 15/20] cosmetic tidying; but further refactoring would possible between `Some`, `All`, and `FixPoint` --- src/Induction/WellFounded.agda | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda index a5b67051f8..c09ba57cb0 100644 --- a/src/Induction/WellFounded.agda +++ b/src/Induction/WellFounded.agda @@ -68,8 +68,7 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where module Some {_<_ : Rel A r} {ℓ} where wfRecBuilder : SubsetRecursorBuilder (Acc _<_) (WfRec _<_ {ℓ = ℓ}) - wfRecBuilder P f x (acc rs) = λ y Date: Sun, 1 Oct 2023 09:56:39 +0100 Subject: [PATCH 16/20] removed one final, hard-to-spot, explicit `_` argument --- src/Codata/Musical/Colist/Infinite-merge.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda index 639a7e5484..5cd694030e 100644 --- a/src/Codata/Musical/Colist/Infinite-merge.agda +++ b/src/Codata/Musical/Colist/Infinite-merge.agda @@ -178,7 +178,7 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂ to : ∀ xss p → InputPred (xss , p) to xss p = - WF.All.wfRec (On.wellFounded size <′-wellFounded) _ + WF.All.wfRec (On.wellFounded size <′-wellFounded) InputPred step (xss , p) where size : Input → ℕ From 983fb2487ae37a76e40ef2801e403459d0a7cd1b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Oct 2023 09:58:18 +0100 Subject: [PATCH 17/20] removed 'documentation' comment --- src/Codata/Musical/Colist/Infinite-merge.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda index 5cd694030e..2cb2359ff8 100644 --- a/src/Codata/Musical/Colist/Infinite-merge.agda +++ b/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))) From 78cc006e5c6760495369719cfbd431a605f73e19 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Oct 2023 10:08:04 +0100 Subject: [PATCH 18/20] restored old `with` usage --- .../Binary/Permutation/Setoid/Properties.agda | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index b157fc4dad..3ea0cbb3c0 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -384,17 +384,14 @@ 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 ps , qs , eq₂ ← helper as bs as↭xs (rec (n<1+n _)) - = a ∷ ps , qs , eq ∷ eq₂ + 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 ps , qs , eq ← helper as bs as↭xs (rec (n<1+n _)) - = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq - helper as bs (trans ↭₁ ↭₂) (acc rec) - with ps , qs , eq ← helper as bs ↭₂ (rec (m Date: Wed, 4 Oct 2023 10:21:00 +0100 Subject: [PATCH 19/20] restored old parametrisation of `All`for use in `FixPoint` --- src/Induction/WellFounded.agda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda index c09ba57cb0..61ba4ded19 100644 --- a/src/Induction/WellFounded.agda +++ b/src/Induction/WellFounded.agda @@ -82,7 +82,7 @@ module Some {_<_ : Rel A r} {ℓ} where -- Well-founded induction for all elements, assuming they are all -- accessible: -module All {_<_ : Rel A r} (wf : WellFounded _<_) {ℓ} where +module All {_<_ : Rel A r} (wf : WellFounded _<_) ℓ where wfRecBuilder : RecursorBuilder (WfRec _<_ {ℓ = ℓ}) wfRecBuilder P f x = Some.wfRecBuilder P f x (wf x) @@ -104,10 +104,11 @@ module FixPoint some-wfrec-Irrelevant x = ∀ q q′ → Some.wfRec P f x q ≡ Some.wfRec P f x q′ some-wfRec-irrelevant : ∀ x → some-wfrec-Irrelevant x - some-wfRec-irrelevant = All.wfRec wf some-wfrec-Irrelevant + some-wfRec-irrelevant = All.wfRec wf _ some-wfrec-Irrelevant λ { x IH (acc rs) (acc rs′) → f-ext x λ y Date: Wed, 4 Oct 2023 10:45:45 +0100 Subject: [PATCH 20/20] restored old parametrisation of `All` in client modules --- src/Codata/Musical/Colist/Infinite-merge.agda | 2 +- src/Data/Fin/Induction.agda | 2 +- src/Data/Nat/Induction.agda | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda index 2cb2359ff8..cbc142ff5a 100644 --- a/src/Codata/Musical/Colist/Infinite-merge.agda +++ b/src/Codata/Musical/Colist/Infinite-merge.agda @@ -178,7 +178,7 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂ to : ∀ xss p → InputPred (xss , p) to xss p = - WF.All.wfRec (On.wellFounded size <′-wellFounded) + WF.All.wfRec (On.wellFounded size <′-wellFounded) _ InputPred step (xss , p) where size : Input → ℕ diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index 88bbcc3227..47e37446bf 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -160,7 +160,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where ≺-wellFounded = Subrelation.wellFounded ≺⇒<′ ℕ.<′-wellFounded module _ {ℓ} where - open WF.All ≺-wellFounded {ℓ} public + open WF.All ≺-wellFounded ℓ public renaming ( wfRecBuilder to ≺-recBuilder ; wfRec to ≺-rec diff --git a/src/Data/Nat/Induction.agda b/src/Data/Nat/Induction.agda index 60076462a8..e1554074c4 100644 --- a/src/Data/Nat/Induction.agda +++ b/src/Data/Nat/Induction.agda @@ -71,7 +71,7 @@ cRec = build cRecBuilder <′-wellFounded′ (suc n) (<′-step m