Added tabulate+<

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)
+  ```

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