Proved a property expanding on the relation between inject+, raise and splitAt (#1079)

Author: Octavian Mircea Sebe

CHANGELOG.md

@@ -389,9 +389,19 @@ Other major additions
 Other minor additions
 ---------------------
 
+* Added new proof to `Data.Fin.Properties`:
+  ```agda
+  inject+-raise-splitAt : [ inject+ n , raise {n} m ] (splitAt m i) ≡ i
+  ```
+
+* Added new proof to `Data.Sum.Properties`:
+  ```agda
+  [,]-∘-distr : f ∘ [ g , h ] ≗ [ f ∘ g , f ∘ h ]
+  ```
+
 * Added new proofs to `Data.Sum.Properties`:
   ```agda
-  [,]-map-commute : [ f′ , g′ ]′ ∘ (map f g) ≗ [ f′ ∘ f , g′ ∘ g ]′
+  [,]-map-commute : [ f′ , g′ ] ∘ (map f g) ≗ [ f′ ∘ f , g′ ∘ g ]
   map-commute     : ((map f′ g′) ∘ (map f g)) ≗ map (f′ ∘ f) (g′ ∘ g)
   ```
 

src/Data/Fin/Properties.agda

@@ -20,6 +20,7 @@ import Data.Nat.Properties as ℕₚ
 open import Data.Unit using (tt)
 open import Data.Product using (∃; ∃₂; ∄; _×_; _,_; map; proj₁; uncurry; <_,_>)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum.Properties using ([,]-map-commute; [,]-∘-distr)
 open import Function.Base using (_∘_; id; _$_)
 open import Function.Equivalence using (_⇔_; equivalence)
 open import Function.Injection using (_↣_)
@@ -422,9 +423,19 @@ splitAt-inject+ (suc m) n zero = refl
 splitAt-inject+ (suc m) n (suc i) rewrite splitAt-inject+ m n i = refl
 
 splitAt-raise : ∀ m n i → splitAt m (raise {n} m i) ≡ inj₂ i
-splitAt-raise zero n i = refl
+splitAt-raise zero    n i = refl
 splitAt-raise (suc m) n i rewrite splitAt-raise m n i = refl
 
+inject+-raise-splitAt : ∀ m n i → [ inject+ n , raise {n} m ] (splitAt m i) ≡ i
+inject+-raise-splitAt zero    n i       = refl
+inject+-raise-splitAt (suc m) n zero    = refl
+inject+-raise-splitAt (suc m) n (suc i) = begin
+  [ inject+ n , raise {n} (suc m) ] (splitAt (suc m) (suc i))  ≡⟨ [,]-map-commute (splitAt m i) ⟩
+  [ suc ∘ (inject+ n) , suc ∘ (raise {n} m) ] (splitAt m i)    ≡˘⟨ [,]-∘-distr {f = suc} (splitAt m i) ⟩
+  suc ([ inject+ n , raise {n} m ] (splitAt m i))              ≡⟨ cong suc (inject+-raise-splitAt m n i) ⟩
+  suc i                                                        ∎
+  where open ≡-Reasoning
+
 
 ------------------------------------------------------------------------
 -- lift

src/Data/Sum/Properties.agda

@@ -44,9 +44,15 @@ module _ (dec₁ : Decidable {A = A} {B = A} _≡_)
 swap-involutive : swap {A = A} {B = B} ∘ swap ≗ id
 swap-involutive = [ (λ _ → refl) , (λ _ → refl) ]
 
+[,]-∘-distr : {f : A → B}
+              {g : C → A} {h : D → A} →
+              f ∘ [ g , h ] ≗ [ f ∘ g , f ∘ h ]
+[,]-∘-distr (inj₁ _) = refl
+[,]-∘-distr (inj₂ _) = refl
+
 [,]-map-commute : {f : A → B}  {g : C → D}
                   {f′ : B → E} {g′ : D → E} →
-                  [ f′ , g′ ]′ ∘ (map f g) ≗ [ f′ ∘ f , g′ ∘ g ]′
+                  [ f′ , g′ ] ∘ (map f g) ≗ [ f′ ∘ f , g′ ∘ g ]
 [,]-map-commute (inj₁ _) = refl
 [,]-map-commute (inj₂ _) = refl