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

CHANGELOG.md

@@ -15,6 +15,15 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
+  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 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.
+
 Deprecated 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

@@ -12,7 +12,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut)
 open import Data.Fin.Patterns using (0F; 1F)
 open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchIn-punchOut
+  punchOut-cong; punchIn-punchOut
   ; _≟_; ¬Fin0; cast-involutive; opposite-involutive)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero; 2+)
@@ -28,7 +28,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (does; ¬_; yes; no)
 open import Relation.Nullary.Decidable using (dec-yes; dec-no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation using (contradiction; contradiction-irr)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -167,19 +167,23 @@ 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} {j = πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong i (cong πˡ (punchIn-punchOut to-punchOut)) ⟩
+    punchOut {j = πˡ (πʳ (punchIn i j))} neq                             ≡⟨ punchOut-cong i (inverseˡ π) ⟩
+    punchOut {i = i} {j = punchIn i j}                            _      ≡⟨ punchOut-punchIn i ⟩
+    j                                                                    ∎
+    where
+    neq : _
+    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} {πʳ (punchIn i (punchOut from-punchOut))}  _    ≡⟨ punchOut-cong (πʳ i) (cong πʳ (punchIn-punchOut from-punchOut)) ⟩
+    punchOut {j = πʳ (πˡ (punchIn (πʳ i) j))} (permute-≢ from-punchOut) ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
+    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _    ≡⟨ punchOut-punchIn (πʳ i) ⟩
+    j                                                                   ∎
 
 ------------------------------------------------------------------------
 -- Lifting
@@ -233,11 +237,11 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
     rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k
     = begin
-    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
+    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨⟩
     punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
-    punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))                              ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
-    punchIn i (punchOut i≢k)                                              ≡⟨ punchIn-punchOut i≢k ⟩
-    k                                                                     ∎
+    punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))                               ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
+    punchIn i (punchOut i≢k)                                               ≡⟨ punchIn-punchOut i≢k ⟩
+    k                                                                      ∎
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ k with j ≟ k
@@ -246,7 +250,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
     rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k
     = begin
-    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
+    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨⟩
     punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
     punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))                               ≡⟨ cong (punchIn j) (inverseʳ π) ⟩
     punchIn j (punchOut j≢k)                                               ≡⟨ punchIn-punchOut j≢k ⟩
@@ -285,8 +289,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
@@ -326,7 +331,7 @@ insert-punchIn : ∀ i j (π : Permutation m n) k → insert i j π ⟨$⟩ʳ pu
 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 i≢punchInᵢk)            ≡⟨⟩
   punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
   punchIn j (π ⟨$⟩ʳ k)                               ∎
 

src/Data/Fin/Properties.agda

@@ -46,7 +46,8 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡
   using (module ≡-Reasoning)
 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 (Reflects; invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
@@ -877,35 +878,36 @@ punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective
 -- 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
+punchOut-cong {suc n} (suc i) {zero}  {zero}           _ = refl
+punchOut-cong {suc n} (suc i) {suc j} {suc k} {i≢j} {i≢k} j≡k   = cong suc (punchOut-cong i {i≢j = i≢j ∘ cong suc} {i≢k = i≢k ∘ cong suc} (suc-injective j≡k))
 
 -- 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′ i {p = p} q =
+  punchOut-cong i {i≢j = p} {i≢k = p ∘ sym ∘ trans q ∘ sym} q
 
 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ₖ =
   cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective 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 =
@@ -914,11 +916,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)
 
 
 ------------------------------------------------------------------------
@@ -1035,9 +1033,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

src/Relation/Nullary/Negation/Core.agda

@@ -47,11 +47,11 @@ _¬-⊎_ = [_,_]
 ------------------------------------------------------------------------
 -- Uses of negation
 
-contradiction-irr : .A → ¬ A → Whatever
+contradiction-irr : .A → .(¬ A) → Whatever
 contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
 
 contradiction : A → ¬ A → Whatever
-contradiction a = contradiction-irr a
+contradiction a ¬a = contradiction-irr a ¬a
 
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a