From 5388c685d1e0c83671c66126fcc1c8bd8f918c99 Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Tue, 12 Mar 2024 17:20:51 +0100
Subject: [PATCH] proper names for find-or-last lemmas

---
 src/Translation/Lang/2ADT-to-VariantList.agda | 10 ++++-----
 src/Util/List.agda                            | 22 +++++++++----------
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/Translation/Lang/2ADT-to-VariantList.agda b/src/Translation/Lang/2ADT-to-VariantList.agda
index 7fccbb7b..7f6d40ef 100644
--- a/src/Translation/Lang/2ADT-to-VariantList.agda
+++ b/src/Translation/Lang/2ADT-to-VariantList.agda
@@ -37,7 +37,7 @@ open import Lang.2ADT.Path F V _==_
 open import Translation.Lang.2ADT.DeadElim F V _==_ as DeadElim using (node; kill-dead; ⟦_⟧ᵤ)
 open import Translation.Lang.2ADT.WalkSemantics F V _==_ as Walk using ()
 
-open import Util.List using (find-or-last; ⁺++⁺-length; ⁺++⁺-length-≤; append-preserves; prepend-preserves-+; prepend-preserves-∸)
+open import Util.List using (find-or-last; ⁺++⁺-length; ⁺++⁺-length-≤; find-or-last-append; find-or-last-prepend-+; find-or-last-prepend-∸)
 open import Util.AuxProofs using (<-cong-+ˡ)
 
 {-
@@ -102,7 +102,7 @@ preservation-walk-to-list-conf (D ⟨ l , r ⟩) ((_ ∷ pl) is-valid walk-left
     walk l c
   ≡⟨ preservation-walk-to-list-conf l c ⟩
     ⟦ tr l ⟧ₗ (conf l c)
-  ≡˘⟨ append-preserves (tr l) (tr r) (conf-bounded l c) ⟩
+  ≡˘⟨ find-or-last-append (tr l) (tr r) (conf-bounded l c) ⟩
     ⟦ tr l ⁺++⁺ tr r ⟧ₗ (conf l c)
   ∎
 preservation-walk-to-list-conf (D ⟨ l , r ⟩) ((_ ∷ pr) is-valid walk-right t) =
@@ -112,7 +112,7 @@ preservation-walk-to-list-conf (D ⟨ l , r ⟩) ((_ ∷ pr) is-valid walk-right
     walk r c
   ≡⟨ preservation-walk-to-list-conf r c ⟩
     ⟦ tr r ⟧ₗ (conf r c)
-  ≡˘⟨ prepend-preserves-+ (conf r c) (tr l) (tr r) ⟩
+  ≡˘⟨ find-or-last-prepend-+ (conf r c) (tr l) (tr r) ⟩
     ⟦ tr l ⁺++⁺ tr r ⟧ₗ (length (tr l) + (conf r c))
   ∎
 
@@ -126,7 +126,7 @@ preservation-walk-to-list-fnoc (D ⟨ l , r ⟩) i with length (tr l) ≤? i
     ⟦ tr (D ⟨ l , r ⟩) ⟧ₗ i
   ≡⟨⟩
     find-or-last i ((tr l) ⁺++⁺ (tr r))
-  ≡⟨ append-preserves (tr l) (tr r) (≰⇒> ¬p) ⟩ -- this is satisfied by eq
+  ≡⟨ find-or-last-append (tr l) (tr r) (≰⇒> ¬p) ⟩ -- this is satisfied by eq
     find-or-last i (tr l)
   ≡⟨⟩
     ⟦ tr l ⟧ₗ i
@@ -138,7 +138,7 @@ preservation-walk-to-list-fnoc (D ⟨ l , r ⟩) i with length (tr l) ≤? i
     ⟦ tr (D ⟨ l , r ⟩) ⟧ₗ i
   ≡⟨⟩
     find-or-last i ((tr l) ⁺++⁺ (tr r))
-  ≡⟨ prepend-preserves-∸ (tr l) (tr r) len[tr-l]≤i ⟩
+  ≡⟨ find-or-last-prepend-∸ (tr l) (tr r) len[tr-l]≤i ⟩
     find-or-last (i ∸ length (tr l)) (tr r)
   ≡⟨⟩
     ⟦ tr r ⟧ₗ (i ∸ length (tr l))
diff --git a/src/Util/List.agda b/src/Util/List.agda
index 809a2e6d..d4fd027e 100644
--- a/src/Util/List.agda
+++ b/src/Util/List.agda
@@ -73,19 +73,19 @@ map-find-or-last f (suc i) (x ∷ y ∷ zs) =
     (find-or-last (suc i) ∘ map⁺ f) (x ∷ y ∷ zs)
   ∎
 
-append-preserves : ∀ {ℓ} {A : Set ℓ} {n : ℕ}
+find-or-last-append : ∀ {ℓ} {A : Set ℓ} {n : ℕ}
   → (xs ys : List⁺ A)
   → n < List⁺.length xs
   → find-or-last n (xs ⁺++⁺ ys) ≡ find-or-last n xs
-append-preserves {n = .zero} (x ∷ [])     (y ∷ ys) (s≤s z≤n) = refl
-append-preserves {n =  zero} (x ∷ z ∷ zs) (y ∷ ys) (s≤s le)  = refl
-append-preserves {n = suc n} (x ∷ z ∷ zs) (y ∷ ys) (s≤s (n≤zzs)) = append-preserves (z ∷ zs) (y ∷ ys) (n≤zzs)
+find-or-last-append {n = .zero} (x ∷ [])     (y ∷ ys) (s≤s z≤n) = refl
+find-or-last-append {n =  zero} (x ∷ z ∷ zs) (y ∷ ys) (s≤s le)  = refl
+find-or-last-append {n = suc n} (x ∷ z ∷ zs) (y ∷ ys) (s≤s (n≤zzs)) = find-or-last-append (z ∷ zs) (y ∷ ys) (n≤zzs)
 
-prepend-preserves-+ : ∀ {ℓ} {A : Set ℓ}
+find-or-last-prepend-+ : ∀ {ℓ} {A : Set ℓ}
   → (n : ℕ)
   → (xs ys : List⁺ A)
   → find-or-last (List⁺.length xs + n) (xs ⁺++⁺ ys) ≡ find-or-last n ys
-prepend-preserves-+ n (x ∷ xs) ys = ind n x xs ys
+find-or-last-prepend-+ n (x ∷ xs) ys = ind n x xs ys
   where
     -- We need this indirection for termination checking.
     -- We have to unpack the first list into two parameters.
@@ -98,18 +98,18 @@ prepend-preserves-+ n (x ∷ xs) ys = ind n x xs ys
     ind n x [] ys = refl
     ind n x (z ∷ zs) ys = ind n z zs ys
 
-prepend-preserves-∸ : ∀ {ℓ} {A : Set ℓ} {n : ℕ}
+find-or-last-prepend-∸ : ∀ {ℓ} {A : Set ℓ} {n : ℕ}
   → (xs ys : List⁺ A)
   → List⁺.length xs ≤ n
   → find-or-last n (xs ⁺++⁺ ys) ≡ find-or-last (n ∸ List⁺.length xs) ys
-prepend-preserves-∸ {n = zero} xs ys ()
-prepend-preserves-∸ {n = suc n} (x ∷ []) ys (s≤s z≤n) = refl
-prepend-preserves-∸ {n = suc n} (x ∷ z ∷ zs) ys (s≤s smol) =
+find-or-last-prepend-∸ {n = zero} xs ys ()
+find-or-last-prepend-∸ {n = suc n} (x ∷ []) ys (s≤s z≤n) = refl
+find-or-last-prepend-∸ {n = suc n} (x ∷ z ∷ zs) ys (s≤s smol) =
   begin
     find-or-last (suc n) ((x ∷ z ∷ zs) ⁺++⁺ ys)
   ≡⟨⟩
     find-or-last n ((z ∷ zs) ⁺++⁺ ys)
-  ≡⟨ prepend-preserves-∸ (z ∷ zs) ys smol ⟩
+  ≡⟨ find-or-last-prepend-∸ (z ∷ zs) ys smol ⟩
     find-or-last (n ∸ List⁺.length (z ∷ zs)) ys
   ≡⟨⟩
     find-or-last (suc n ∸ suc (List⁺.length (z ∷ zs))) ys