From cba34c37619e050298e2cabfc2e86e694dd910b7 Mon Sep 17 00:00:00 2001
From: Guilherme <alvares@chalmers.se>
Date: Tue, 31 Oct 2023 11:28:17 +0100
Subject: [PATCH 1/2] added tabulate+<

---
 CHANGELOG.md                                   |  5 +++++
 .../Relation/Unary/AllPairs/Properties.agda    | 18 +++++++++++-------
 2 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9d9f403d64..ad0a40c9a2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3781,3 +3781,8 @@ This is a full list of proofs that have changed form to use irrelevant instance
   1/pos⇒pos : ∀ p .{{_ : NonZero p}} → (1/p : Positive (1/ p)) → Positive p
   1/neg⇒neg : ∀ p .{{_ : NonZero p}} → (1/p : Negative (1/ p)) → Negative p
   ```
+
+* In `Data.List.Relation.Unary.AllPairs.Properties`:
+  ```
+  tabulate⁺< : (∀ {i j} → i F.< j → R (f i) (f j)) → AllPairs R (tabulate f)
+  ```
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
index c116fcb00f..47465d10a0 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
@@ -13,9 +13,9 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base using (Fin)
-open import Data.Fin.Properties using (suc-injective)
-open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
+open import Data.Fin.Base as F using (Fin)
+open import Data.Fin.Properties using (suc-injective; <⇒≢)
+open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s; z<s; s<s)
 open import Data.Nat.Properties using (≤-refl; m<n⇒m<1+n)
 open import Function.Base using (_∘_; flip)
 open import Level using (Level)
@@ -115,12 +115,16 @@ module _ {R : Rel A ℓ} where
 
 module _ {R : Rel A ℓ} where
 
+  tabulate⁺< : ∀ {n} {f : Fin n → A} → (∀ {i j} → i F.< j → R (f i) (f j)) →
+              AllPairs R (tabulate f)
+  tabulate⁺< {zero}  fᵢ~fⱼ = AllPairs.[]
+  tabulate⁺< {suc n} fᵢ~fⱼ =
+    All.tabulate⁺ (λ _ → fᵢ~fⱼ z<s) AllPairs.∷
+    tabulate⁺< (fᵢ~fⱼ ∘ s<s)
+
   tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) →
               AllPairs R (tabulate f)
-  tabulate⁺ {zero}  fᵢ~fⱼ = []
-  tabulate⁺ {suc n} fᵢ~fⱼ =
-    All.tabulate⁺ (λ j → fᵢ~fⱼ λ()) ∷
-    tabulate⁺ (fᵢ~fⱼ ∘ (_∘ suc-injective))
+  tabulate⁺ fᵢ~fⱼ = tabulate⁺< (fᵢ~fⱼ ∘ <⇒≢)
 
 ------------------------------------------------------------------------
 -- filter

From 900c1de74ca2bd63c341289f68dadc3ce7069964 Mon Sep 17 00:00:00 2001
From: Guilherme <alvares@chalmers.se>
Date: Thu, 2 Nov 2023 09:20:31 +0100
Subject: [PATCH 2/2] renamed tabulate function

---
 CHANGELOG.md                                         |  2 +-
 .../List/Relation/Unary/AllPairs/Properties.agda     | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ad0a40c9a2..7f4eaf0c23 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3784,5 +3784,5 @@ This is a full list of proofs that have changed form to use irrelevant instance
 
 * In `Data.List.Relation.Unary.AllPairs.Properties`:
   ```
-  tabulate⁺< : (∀ {i j} → i F.< j → R (f i) (f j)) → AllPairs R (tabulate f)
+  tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f)
   ```
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
index 47465d10a0..027d9bb4cc 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
@@ -115,16 +115,16 @@ module _ {R : Rel A ℓ} where
 
 module _ {R : Rel A ℓ} where
 
-  tabulate⁺< : ∀ {n} {f : Fin n → A} → (∀ {i j} → i F.< j → R (f i) (f j)) →
+  tabulate⁺-< : ∀ {n} {f : Fin n → A} → (∀ {i j} → i F.< j → R (f i) (f j)) →
               AllPairs R (tabulate f)
-  tabulate⁺< {zero}  fᵢ~fⱼ = AllPairs.[]
-  tabulate⁺< {suc n} fᵢ~fⱼ =
-    All.tabulate⁺ (λ _ → fᵢ~fⱼ z<s) AllPairs.∷
-    tabulate⁺< (fᵢ~fⱼ ∘ s<s)
+  tabulate⁺-< {zero}  fᵢ~fⱼ = []
+  tabulate⁺-< {suc n} fᵢ~fⱼ =
+    All.tabulate⁺ (λ _ → fᵢ~fⱼ z<s) ∷
+    tabulate⁺-< (fᵢ~fⱼ ∘ s<s)
 
   tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → i ≢ j → R (f i) (f j)) →
               AllPairs R (tabulate f)
-  tabulate⁺ fᵢ~fⱼ = tabulate⁺< (fᵢ~fⱼ ∘ <⇒≢)
+  tabulate⁺ fᵢ~fⱼ = tabulate⁺-< (fᵢ~fⱼ ∘ <⇒≢)
 
 ------------------------------------------------------------------------
 -- filter