[ refactor ] make i ≢ j argument to Data.Fin.Base.punchOut irrelevant

CHANGELOG.md

@@ -21,6 +21,11 @@ Minor improvements
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
 
+* Similarly the type of `Data.Fin.Base.punchOut` has been weakened so that the
+  negated equational hypothesis `i ≢ j` is marked as irrelevant. This simplifies
+  some of the proofs of its properties, but also requires some slightly more
+  explicit instantiation in a couple of places.
+
 * Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
   ```agda
   README.Data.Fin.Relation.Unary.Top
@@ -39,6 +44,11 @@ Deprecated names
 * In `Algebra.Properties.CommutativeSemigroup`:
   ```agda
   interchange  ↦   medial
+ ```
+
+* In `Data.Fin.Properties`:
+  ```agda
+  punchOut-cong′  ↦  punchOut-cong
   ```
 
 New modules

src/Data/Fin/Base.agda

@@ -19,7 +19,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction-irr)
 
 private
   variable
@@ -252,8 +252,8 @@ opposite {suc n} (suc i) = inject₁ (opposite i)
 -- This is a variant of the thick function from Conor
 -- McBride's "First-order unification by structural recursion".
 
-punchOut : ∀ {i j : Fin (suc n)} → i ≢ j → Fin n
-punchOut {_}     {zero}   {zero}  i≢j = contradiction refl i≢j
+punchOut : ∀ {i j : Fin (suc n)} → .(i ≢ j) → Fin n
+punchOut {_}     {zero}   {zero}  i≢j = contradiction-irr 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/Permutation.agda

@@ -15,7 +15,7 @@ open import Data.Fin.Properties
   using (¬Fin0; _≟_; ≟-≡-refl; ≟-≢
         ; cast-involutive; opposite-involutive
         ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut
-        ; punchOut-cong; punchOut-cong′)
+        ; punchOut-cong)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero; 2+)
 open import Data.Product.Base using (_,_; proj₂)
@@ -29,7 +29,7 @@ open import Function.Base using (_∘_; _∘′_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Decidable.Core using (does; yes; no)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction-irr)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -168,19 +168,30 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ j = begin
-    from (to j)                                                     ≡⟨⟩
-    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
-    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _ ≡⟨ punchOut-cong i (inverseˡ π) ⟩
-    punchOut {i = i} {punchIn i j}                                _ ≡⟨ punchOut-punchIn i ⟩
-    j                                                               ∎
+    from (to j)        ≡⟨⟩
+    punchOut {i = i} _ ≡⟨ punchOut-cong i (cong πˡ eq) ⟩
+    punchOut neq       ≡⟨ punchOut-cong i (inverseˡ π) ⟩
+    punchOut {i = i} _ ≡⟨ punchOut-punchIn i ⟩
+    j                  ∎
+    where
+    eq : punchIn (πʳ i) (to j) ≡ πʳ (punchIn i j)
+    eq = punchIn-punchOut to-punchOut
+    neq : i ≢ πˡ (πʳ (punchIn i j))
+    neq eq = punchInᵢ≢i i j (sym (trans eq (inverseˡ π)))
+
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ j = begin
-    to (from j)                                                      ≡⟨⟩
-    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _ ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
-    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _ ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
-    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _ ≡⟨ punchOut-punchIn (πʳ i) ⟩
-    j                                                                ∎
+    to (from j)           ≡⟨⟩
+    punchOut {i = πʳ i} _ ≡⟨ punchOut-cong (πʳ i) (cong πʳ eq) ⟩
+    punchOut neq          ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
+    punchOut {i = πʳ i} _ ≡⟨ punchOut-punchIn (πʳ i) ⟩
+    j                     ∎
+    where
+    eq : punchIn i (from j) ≡ πˡ (punchIn (πʳ i) j)
+    eq = punchIn-punchOut from-punchOut
+    neq : πʳ i ≢ πʳ (πˡ (punchIn (πʳ i) j))
+    neq = permute-≢ from-punchOut
 
 ------------------------------------------------------------------------
 -- Lifting
@@ -234,8 +245,8 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
     rewrite ≟-≢ j≢punchInⱼπʳpunchOuti≢k
     = begin
-    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
-    punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
+    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨⟩
+    punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (punchIn i ∘ (π ⟨$⟩ˡ_)) (punchOut-punchIn j) ⟩
     punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))                               ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
     punchIn i (punchOut i≢k)                                               ≡⟨ punchIn-punchOut i≢k ⟩
     k                                                                      ∎
@@ -247,8 +258,8 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
     rewrite ≟-≢ i≢punchInᵢπˡpunchOutj≢k
     = begin
-    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
-    punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
+    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨⟩
+    punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (punchIn j ∘ (π ⟨$⟩ʳ_)) (punchOut-punchIn i) ⟩
     punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))                               ≡⟨ cong (punchIn j) (inverseʳ π) ⟩
     punchIn j (punchOut j≢k)                                               ≡⟨ punchIn-punchOut j≢k ⟩
     k                                                                      ∎
@@ -286,8 +297,9 @@ module _ (π : Permutation (suc m) (suc n)) where
   lift₀-remove p 0F      = sym p
   lift₀-remove p (suc i) = punchOut-zero (πʳ (suc i)) p
     where
-    punchOut-zero : ∀ {i} (j : Fin (suc n)) {neq} → i ≡ 0F → suc (punchOut {i = i} {j} neq) ≡ j
-    punchOut-zero 0F {neq} p = contradiction p neq
+    punchOut-zero : ∀ {i} (j : Fin (suc n)) .{neq} →
+                    i ≡ 0F → suc (punchOut {i = i} {j} neq) ≡ j
+    punchOut-zero 0F {neq} eq = contradiction-irr eq neq
     punchOut-zero (suc j) refl = refl
 
 ↔⇒≡ : Permutation m n → m ≡ n
@@ -323,19 +335,18 @@ lift₀-transpose i j (suc k) with does (k ≟ i)
 ...   | false = refl
 ...   | true = refl
 
-insert-punchIn : ∀ i j (π : Permutation m n) k → insert i j π ⟨$⟩ʳ punchIn i k ≡ punchIn j (π ⟨$⟩ʳ k)
+insert-punchIn : ∀ i j (π : Permutation m n) k →
+                 insert i j π ⟨$⟩ʳ punchIn i k ≡ punchIn j (π ⟨$⟩ʳ k)
 insert-punchIn i j π k with i ≟ punchIn i k
 ... | yes i≡punchInᵢk = contradiction (sym i≡punchInᵢk) (punchInᵢ≢i i k)
-... | no  i≢punchInᵢk = begin
-  punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk)            ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
-  punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
-  punchIn j (π ⟨$⟩ʳ k)                               ∎
+... | no  i≢punchInᵢk = cong (punchIn j ∘ (π ⟨$⟩ʳ_)) (punchOut-punchIn i)
 
-insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π
-insert-remove {m = m} {n = n} i π j with i ≟ j
+insert-remove : ∀ i (π : Permutation (suc m) (suc n)) →
+                insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π
+insert-remove i π j with i ≟ j
 ... | yes i≡j = cong (π ⟨$⟩ʳ_) i≡j
 ... | no  i≢j = begin
-  punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩
+  punchIn (π ⟨$⟩ʳ i) _            ≡⟨ punchIn-punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π)) ⟩
   π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩
   π ⟨$⟩ʳ j ∎
 

src/Data/Fin/Properties.agda

@@ -49,7 +49,8 @@ open import Relation.Binary.PropositionalEquality as ≡
   using (≡-≟-identity; ≢-≟-identity)
 open import Relation.Nullary.Decidable as Dec
   using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core
+  using (¬_; contradiction; contradiction-irr)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
@@ -902,27 +903,19 @@ punchIn-cancel-≤ (suc i) (suc j) (suc k) (s≤s ↑j≤↑k) = s≤s (punchIn-
 -- can be changed out arbitrarily (reflecting the proof-irrelevance of
 -- that argument).
 
-punchOut-cong : ∀ (i : Fin (suc n)) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} →
+punchOut-cong : ∀ (i : Fin (suc n)) {j k} .{i≢j : i ≢ j} .{i≢k : i ≢ k} →
                 j ≡ k → punchOut i≢j ≡ punchOut i≢k
-punchOut-cong {_}     zero    {zero}         {i≢j = 0≢0} = contradiction refl 0≢0
-punchOut-cong {_}     zero    {suc j} {zero} {i≢k = 0≢0} = contradiction refl 0≢0
+punchOut-cong {_}     zero    {zero}         {i≢j = 0≢0} = contradiction-irr refl 0≢0
+punchOut-cong {_}     zero    {suc j} {zero} {i≢k = 0≢0} = contradiction-irr refl 0≢0
 punchOut-cong {_}     zero    {suc j} {suc k}            = suc-injective
-punchOut-cong {suc n} (suc i) {zero}  {zero}   _ = refl
-punchOut-cong {suc n} (suc i) {suc j} {suc k}    = cong suc ∘ punchOut-cong i ∘ suc-injective
-
--- An alternative to 'punchOut-cong' in the which the new inequality
--- argument is specific. Useful for enabling the omission of that
--- argument during equational reasoning.
-
-punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
-                 punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
-punchOut-cong′ i q = punchOut-cong i q
+punchOut-cong {suc n} (suc i) {zero}  {zero}             = λ _ → refl
+punchOut-cong {suc n} (suc i) {suc j} {suc k}            = cong suc ∘ punchOut-cong i ∘ suc-injective
 
 punchOut-injective : ∀ {i j k : Fin (suc n)}
-                     (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                     .(i≢j : i ≢ j) .(i≢k : i ≢ k) →
                      punchOut i≢j ≡ punchOut i≢k → j ≡ k
-punchOut-injective {_}     {zero}   {zero}  {_}     0≢0 _   _     = contradiction refl 0≢0
-punchOut-injective {_}     {zero}   {_}     {zero}  _   0≢0 _     = contradiction refl 0≢0
+punchOut-injective {_}     {zero}   {zero}  {_}     0≢0 _   _     = contradiction-irr refl 0≢0
+punchOut-injective {_}     {zero}   {_}     {zero}  _   0≢0 _     = contradiction-irr refl 0≢0
 punchOut-injective {_}     {zero}   {suc j} {suc k} _   _   pⱼ≡pₖ = cong suc pⱼ≡pₖ
 punchOut-injective {suc n} {suc i}  {zero}  {zero}  _   _    _    = refl
 punchOut-injective {suc n} {suc i}  {suc j} {suc k} i≢j i≢k pⱼ≡pₖ =
@@ -944,9 +937,9 @@ punchOut-cancel-≤ {_    } {suc _} {zero } {_    } _   _   _           = z≤n
 punchOut-cancel-≤ {suc _} {suc _} {suc _} {zero } _   _   ()
 punchOut-cancel-≤ {suc _} {suc _} {suc _} {suc _} i≢j i≢k (s≤s pⱼ≤pₖ) = s≤s (punchOut-cancel-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) pⱼ≤pₖ)
 
-punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) →
+punchIn-punchOut : ∀ {i j : Fin (suc n)} .(i≢j : i ≢ j) →
                    punchIn i (punchOut i≢j) ≡ j
-punchIn-punchOut {_}     {zero}   {zero}  0≢0 = contradiction refl 0≢0
+punchIn-punchOut {_}     {zero}   {zero}  0≢0 = contradiction-irr refl 0≢0
 punchIn-punchOut {_}     {zero}   {suc j} _   = refl
 punchIn-punchOut {suc m} {suc i}  {zero}  i≢j = refl
 punchIn-punchOut {suc m} {suc i}  {suc j} i≢j =
@@ -955,11 +948,7 @@ punchIn-punchOut {suc m} {suc i}  {suc j} i≢j =
 punchOut-punchIn : ∀ i {j : Fin n} → punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j
 punchOut-punchIn zero    {j}     = refl
 punchOut-punchIn (suc i) {zero}  = refl
-punchOut-punchIn (suc i) {suc j} = cong suc (begin
-  punchOut (punchInᵢ≢i i j ∘ suc-injective ∘ sym ∘ cong suc)  ≡⟨ punchOut-cong i refl ⟩
-  punchOut (punchInᵢ≢i i j ∘ sym)                             ≡⟨ punchOut-punchIn i ⟩
-  j                                                           ∎)
-  where open ≡-Reasoning
+punchOut-punchIn (suc i) {suc j} = cong suc (punchOut-punchIn i)
 
 
 ------------------------------------------------------------------------
@@ -1076,9 +1065,12 @@ pigeonhole : m ℕ.< n → (f : Fin n → Fin m) → ∃₂ λ i j → i < j ×
 pigeonhole z<s               f = contradiction (f zero) λ()
 pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
 ... | yes (j , f₀≡fⱼ) = zero , suc j , z<s , f₀≡fⱼ
-... | no  f₀≢fₖ
-  with i , j , i<j , fᵢ≡fⱼ ← pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
-  = suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
+... | no  ¬∃[k]f₀≡fₛₖ =
+  let i , j , i<j , fᵢ≡fⱼ = pigeonhole m<n (λ k → punchOut (f₀≢fₛ k))
+  in suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₛ i) (f₀≢fₛ j) fᵢ≡fⱼ
+  where
+  f₀≢fₛ : ∀ k → f zero ≢ f (suc k)
+  f₀≢fₛ k = ¬∃[k]f₀≡fₛₖ ∘ (k ,_)
 
 injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
 injective⇒≤ {zero}  {_}     {f} _   = z≤n
@@ -1274,3 +1266,13 @@ Please use <⇒<′ instead."
 "Warning: <′⇒≺ was deprecated in v2.0.
 Please use <′⇒< instead."
 #-}
+
+-- Version 2.4
+
+punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
+                 punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
+punchOut-cong′ i q = punchOut-cong i q
+{-# WARNING_ON_USAGE punchOut-cong′
+"Warning: punchOut-cong′ was deprecated in v2.4.
+Please use punchOut-cong instead."
+#-}

src/Data/Vec/Functional/Properties.agda

@@ -29,7 +29,8 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; map′; _×-dec_)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation
+  using (contradiction; contradiction-irr)
 
 import Data.Fin.Properties as Finₚ
 
@@ -236,9 +237,9 @@ insertAt-punchIn {n = suc n} xs (suc i) v (suc j) = insertAt-punchIn (tail xs) i
 -- removeAt
 
 removeAt-punchOut : ∀ (xs : Vector A (suc n))
-                  {i : Fin (suc n)} {j : Fin (suc n)} (i≢j : i ≢ j) →
+                  {i : Fin (suc n)} {j : Fin (suc n)} .(i≢j : i ≢ j) →
                   removeAt xs i (punchOut i≢j) ≡ xs j
-removeAt-punchOut {n = n}     xs {zero}  {zero}  i≢j = contradiction refl i≢j
+removeAt-punchOut {n = n}     xs {zero}  {zero}  i≢j = contradiction-irr refl i≢j
 removeAt-punchOut {n = suc n} xs {zero}  {suc j} i≢j = refl
 removeAt-punchOut {n = suc n} xs {suc i} {zero}  i≢j = refl
 removeAt-punchOut {n = suc n} xs {suc i} {suc j} i≢j = removeAt-punchOut (tail xs) (i≢j ∘ cong suc)

src/Data/Vec/Properties.agda

@@ -37,7 +37,8 @@ open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Decidable.Core
   using (Dec; does; yes; _×-dec_; map′)
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation.Core
+  using (contradiction; contradiction-irr)
 import Data.Nat.GeneralisedArithmetic as ℕ
 
 private
@@ -1290,9 +1291,9 @@ toList-insertAt (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insertAt xs i
 ------------------------------------------------------------------------
 -- removeAt
 
-removeAt-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) →
+removeAt-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} .(i≢j : i ≢ j) →
                   lookup (removeAt xs i) (Fin.punchOut i≢j) ≡ lookup xs j
-removeAt-punchOut (x ∷ xs)     {zero}  {zero}  i≢j = contradiction refl i≢j
+removeAt-punchOut (x ∷ xs)     {zero}  {zero}  i≢j = contradiction-irr refl i≢j
 removeAt-punchOut (x ∷ xs)     {zero}  {suc j} i≢j = refl
 removeAt-punchOut (x ∷ y ∷ xs) {suc i} {zero}  i≢j = refl
 removeAt-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =