Refactor some lookup and truncation lemmas (#2101)

Author: jamesmckinna

CHANGELOG.md

@@ -1464,6 +1464,8 @@ Deprecated names
   sum-++-commute  ↦ sum-++
 
   take-drop-id ↦ take++drop≡id
+
+  lookup-inject≤-take ↦ lookup-take-inject≤
   ```
   and the type of the proof `zipWith-comm` has been generalised from:
   ```
@@ -2193,6 +2195,9 @@ Additions to existing modules
   cast-trans    : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k
 
   fromℕ≢inject₁      : {i : Fin n} → fromℕ n ≢ inject₁ i
+
+  inject≤-trans      : inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i (≤-trans m≤n n≤o)
+  inject≤-irrelevant : inject≤ i m≤n ≡ inject≤ i m≤n′
   ```
 
 * Added new functions in `Data.Integer.Base`:
@@ -2738,12 +2743,13 @@ Additions to existing modules
 
   cast-is-id    : cast eq xs ≡ xs
   subst-is-cast : subst (Vec A) eq xs ≡ cast eq xs
+  cast-sym      : cast eq xs ≡ ys → cast (sym eq) ys ≡ xs
   cast-trans    : cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
   map-cast      : map f (cast eq xs) ≡ cast eq (map f xs)
   lookup-cast   : lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
-  cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq
+  cast-reverse  : cast eq ∘ reverse ≗ reverse ∘ cast eq
 
   zipwith-++ : zipWith f (xs ++ ys) (xs' ++ ys') ≡ zipWith f xs xs' ++ zipWith f ys ys'
 
@@ -2757,6 +2763,11 @@ Additions to existing modules
   cast-fromList : cast _ (fromList xs) ≡ fromList ys
   fromList-map  : cast _ (fromList (List.map f xs)) ≡ map f (fromList xs)
   fromList-++   : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys
+
+  truncate≡take       : .(eq : n ≡ m + o) → truncate m≤n xs ≡ take m (cast eq xs)
+  take≡truncate       : take m xs ≡ truncate (m≤m+n m n) xs
+  lookup-truncate     : lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n)
+  lookup-take-inject≤ : lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n))
   ```
 
 * Added new proofs in `Data.Vec.Membership.Propositional.Properties`:

src/Data/Fin/Base.agda

@@ -12,7 +12,6 @@
 module Data.Fin.Base where
 
 open import Data.Bool.Base using (Bool; true; false; T; not)
-open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
 open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
@@ -115,13 +114,13 @@ inject₁ zero    = zero
 inject₁ (suc i) = suc (inject₁ i)
 
 inject≤ : Fin m → m ℕ.≤ n → Fin n
-inject≤ {_} {suc n} zero    _        = zero
+inject≤ {_} {suc n} zero    _         =  zero
 inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
 
 -- lower₁ "i" _ = "i".
 
 lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
-lower₁ {zero}  zero    ne = ⊥-elim (ne refl)
+lower₁ {zero}  zero    ne = contradiction refl ne
 lower₁ {suc n} zero    _  = zero
 lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc))
 
@@ -252,7 +251,7 @@ opposite {suc n} (suc i) = inject₁ (opposite i)
 -- McBride's "First-order unification by structural recursion".
 
 punchOut : ∀ {i j : Fin (suc n)} → i ≢ j → Fin n
-punchOut {_}     {zero}   {zero}  i≢j = ⊥-elim (i≢j refl)
+punchOut {_}     {zero}   {zero}  i≢j = contradiction refl i≢j
 punchOut {_}     {zero}   {suc j} _   = j
 punchOut {suc _} {suc i}  {zero}  _   = zero
 punchOut {suc _} {suc i}  {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))

src/Data/Fin/Properties.agda

@@ -547,12 +547,20 @@ inject≤-idempotent {_} {suc n} {suc o} zero    _   _   _ = refl
 inject≤-idempotent {_} {suc n} {suc o} (suc i) (s≤s m≤n) (s≤s n≤o) (s≤s m≤o) =
   cong suc (inject≤-idempotent i m≤n n≤o m≤o)
 
+inject≤-trans : ∀ (i : Fin m) (m≤n : m ℕ.≤ n) (n≤o : n ℕ.≤ o) →
+                inject≤ (inject≤ i m≤n) n≤o ≡ inject≤ i (ℕₚ.≤-trans m≤n n≤o)
+inject≤-trans i m≤n n≤o = inject≤-idempotent i m≤n n≤o _
+
 inject≤-injective : ∀ (m≤n m≤n′ : m ℕ.≤ n) i j →
                     inject≤ i m≤n ≡ inject≤ j m≤n′ → i ≡ j
 inject≤-injective (s≤s p) (s≤s q) zero    zero    eq = refl
 inject≤-injective (s≤s p) (s≤s q) (suc i) (suc j) eq =
   cong suc (inject≤-injective p q i j (suc-injective eq))
 
+inject≤-irrelevant : ∀ (m≤n m≤n′ : m ℕ.≤ n) i →
+                    inject≤ i m≤n ≡ inject≤ i m≤n′
+inject≤-irrelevant m≤n m≤n′ i =  cong (inject≤ i) (ℕₚ.≤-irrelevant m≤n m≤n′)
+
 ------------------------------------------------------------------------
 -- pred
 ------------------------------------------------------------------------

src/Data/Vec/Base.agda

@@ -290,7 +290,7 @@ uncons (x ∷ xs) = x , xs
 
 -- Take the first 'm' elements of a vector.
 truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m
-truncate z≤n      _        = []
+truncate {m = zero} _ _    = []
 truncate (s≤s le) (x ∷ xs) = x ∷ (truncate le xs)
 
 -- Pad out a vector with extra elements.

src/Data/Vec/Properties.agda

@@ -10,27 +10,27 @@ module Data.Vec.Properties where
 
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_)
+open import Data.Fin.Base as Fin
+  using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_)
 open import Data.List.Base as List using (List)
 import Data.List.Properties as Listₚ
 open import Data.Nat.Base
 open import Data.Nat.Properties
-  using (+-assoc; m≤n⇒m≤1+n; ≤-refl; ≤-trans; suc-injective; +-comm; +-suc)
+  using (+-assoc; m≤n⇒m≤1+n; m≤m+n; ≤-refl; ≤-trans; ≤-irrelevant; ≤⇒≤″; suc-injective; +-comm; +-suc)
 open import Data.Product.Base as Prod
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
 open import Data.Sum.Properties using ([,]-map)
 open import Data.Vec.Base
 open import Function.Base
--- open import Function.Inverse using (_↔_; inverse)
 open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (Level)
 open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (Dec; does; yes; no; _×-dec_; map′)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (Dec; does; yes; no; _×-dec_; map′)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 open ≡-Reasoning
 
@@ -122,6 +122,19 @@ truncate-trans : ∀ {p} (m≤n : m ≤ n) (n≤p : n ≤ p) (xs : Vec A p) →
 truncate-trans z≤n       n≤p       xs = refl
 truncate-trans (s≤s m≤n) (s≤s n≤p) (x ∷ xs) = cong (x ∷_) (truncate-trans m≤n n≤p xs)
 
+truncate-irrelevant : (m≤n₁ m≤n₂ : m ≤ n) → truncate {A = A} m≤n₁ ≗ truncate m≤n₂
+truncate-irrelevant m≤n₁ m≤n₂ xs = cong (λ m≤n → truncate m≤n xs) (≤-irrelevant m≤n₁ m≤n₂)
+
+truncate≡take : (m≤n : m ≤ n) (xs : Vec A n) .(eq : n ≡ m + o) →
+                truncate m≤n xs ≡ take m (cast eq xs)
+truncate≡take z≤n       _        eq = refl
+truncate≡take (s≤s m≤n) (x ∷ xs) eq = cong (x ∷_) (truncate≡take m≤n xs (suc-injective eq))
+
+take≡truncate : ∀ m (xs : Vec A (m + n)) →
+                take m xs ≡ truncate (m≤m+n m n) xs
+take≡truncate zero    _        = refl
+take≡truncate (suc m) (x ∷ xs) = cong (x ∷_) (take≡truncate m xs)
+
 ------------------------------------------------------------------------
 -- pad
 
@@ -171,10 +184,20 @@ lookup⇒[]= (suc i) (_ ∷ xs) p    = there (lookup⇒[]= i xs p)
   []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero    refl = refl
   []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p    = []=⇒lookup∘lookup⇒[]= xs i p
 
-lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
-                      lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
-lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs) = refl
-lookup-inject≤-take (suc m) (s≤s m≤m+n) (suc i) (x ∷ xs) = lookup-inject≤-take m m≤m+n i xs
+lookup-truncate : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) →
+                  lookup (truncate m≤n xs) i ≡ lookup xs (Fin.inject≤ i m≤n)
+lookup-truncate (s≤s m≤m+n) (_ ∷ _)  zero    = refl
+lookup-truncate (s≤s m≤m+n) (_ ∷ xs) (suc i) = lookup-truncate m≤m+n xs i
+
+lookup-take-inject≤ : (xs : Vec A (m + n)) (i : Fin m) →
+                      lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i (m≤m+n m n))
+lookup-take-inject≤ {m = m} {n = n} xs i = begin
+  lookup (take _ xs) i
+    ≡⟨ cong (λ ys → lookup ys i) (take≡truncate m xs) ⟩
+  lookup (truncate _ xs) i
+    ≡⟨ lookup-truncate (m≤m+n m n) xs i ⟩
+  lookup xs (Fin.inject≤ i (m≤m+n m n))
+    ∎ where open ≡-Reasoning
 
 ------------------------------------------------------------------------
 -- updateAt (_[_]%=_)
@@ -348,6 +371,13 @@ cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
 subst-is-cast refl xs = sym (cast-is-id refl xs)
 
+cast-sym : .(eq : m ≡ n) {xs : Vec A m} {ys : Vec A n} →
+           cast eq xs ≡ ys → cast (sym eq) ys ≡ xs
+cast-sym eq {xs = []}     {ys = []}     _ = refl
+cast-sym eq {xs = x ∷ xs} {ys = y ∷ ys} xxs[eq]≡yys =
+  let x≡y , xs[eq]≡ys = ∷-injective xxs[eq]≡yys
+  in cong₂ _∷_ (sym x≡y) (cast-sym (suc-injective eq) xs[eq]≡ys)
+
 cast-trans : .(eq₁ : m ≡ n) .(eq₂ : n ≡ o) (xs : Vec A m) →
              cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
 cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
@@ -399,9 +429,9 @@ map-updateAt (x ∷ xs) (suc i) eq = cong (_ ∷_) (map-updateAt xs i eq)
 
 map-insert : ∀ (f : A → B) (x : A) (xs : Vec A n) (i : Fin (suc n)) →
              map f (insert xs i x) ≡ insert (map f xs) i (f x)
-map-insert f _ []        Fin.zero = refl
-map-insert f _ (x' ∷ xs) Fin.zero = refl
-map-insert f x (x' ∷ xs) (Fin.suc i) = cong (_ ∷_) (map-insert f x xs i)
+map-insert f _ []        zero    = refl
+map-insert f _ (x' ∷ xs) zero    = refl
+map-insert f x (x' ∷ xs) (suc i) = cong (_ ∷_) (map-insert f x xs i)
 
 map-[]≔ : ∀ (f : A → B) (xs : Vec A n) (i : Fin n) →
           map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
@@ -1245,13 +1275,11 @@ sum-++-commute = sum-++
 "Warning: sum-++-commute was deprecated in v2.0.
 Please use sum-++ instead."
 #-}
-
 take-drop-id = take++drop≡id
 {-# WARNING_ON_USAGE take-drop-id
 "Warning: take-drop-id was deprecated in v2.0.
 Please use take++drop≡id instead."
 #-}
-
 take-distr-zipWith = take-zipWith
 {-# WARNING_ON_USAGE take-distr-zipWith
 "Warning: take-distr-zipWith was deprecated in v2.0.
@@ -1272,3 +1300,17 @@ drop-distr-map = drop-map
 "Warning: drop-distr-map was deprecated in v2.0.
 Please use drop-map instead."
 #-}
+lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
+                      lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
+lookup-inject≤-take m m≤m+n i xs = sym (begin
+  lookup (take m xs) i
+    ≡⟨ lookup-take-inject≤ xs i ⟩
+  lookup xs (Fin.inject≤ i _)
+    ≡⟨ cong ((lookup xs) ∘ (Fin.inject≤ i)) (≤-irrelevant _ _) ⟩
+  lookup xs (Fin.inject≤ i m≤m+n)
+    ∎) where open ≡-Reasoning
+{-# WARNING_ON_USAGE lookup-inject≤-take
+"Warning: lookup-inject≤-take was deprecated in v2.0.
+Please use lookup-take-inject≤ or lookup-truncate, take≡truncate instead."
+#-}
+