[ refactor ] Data.Fin.Properties of decidable equality, plus knock-ons (#2740)

* add: lemmas for decidable equality on `Fin`, plus backport to `Nat`

* refactor: knock-ons

* fix: `import`s

* tighten up

* refactor: add new lemmas, simplify old proof

* refactor: additional instantiated lemmas

* refactor: further streamlining of proofs and `import`s

* `CHANGELOG`

* whitespace

* fix: #2743

* fix: deprecation bug

* fix: equational reaosning layout

* fix: merge conflicts

* fix: equation alignment

* fix: equation alignment

* refactor: `yes` and `no`

* fix\; remove Fairbairn violation

* rename: `transpose` lemmas

* rename: decidable equality lemmas

* fix: use of new names

* restore: original alignment

* fix: `CHANGELOG`

Author: jamesmckinna

CHANGELOG.md

@@ -56,7 +56,24 @@ Additions to existing modules
   [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y
   ```
 
+* In `Data.Fin.Permutation.Components`:
+  ```agda
+  transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j
+  transpose[i,j,j]≡i  : (i j : Fin n) → transpose i j j ≡ i
+  transpose[i,j,i]≡j  : (i j : Fin n) → transpose i j i ≡ j
+  transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k
+  ```
+
+* In `Data.Fin.Properties`:
+  ```agda
+  ≡-irrelevant : Irrelevant {A = Fin n} _≡_
+  ≟-≡          : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
+  ≟-≡-refl     : (i : Fin n) → (i ≟ i) ≡ yes refl
+  ≟-≢          : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
+  ```
+
 * In `Data.Nat.Properties`:
   ```agda
+  ≟-≢   : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
   ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
   ```

src/Data/Fin/Permutation.agda

@@ -11,9 +11,11 @@ module Data.Fin.Permutation where
 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
-  ; _≟_; ¬Fin0; cast-involutive; opposite-involutive)
+open import Data.Fin.Properties
+  using (¬Fin0; _≟_; ≟-≡-refl; ≟-≢
+        ; cast-involutive; opposite-involutive
+        ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut
+        ; 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₂)
@@ -26,9 +28,8 @@ open import Function.Properties.Inverse using (↔⇒↣)
 open import Function.Base using (_∘_; _∘′_)
 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.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -167,19 +168,19 @@ 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} {πˡ (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                                                               ∎
 
   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 _)) ⟩
+    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _ ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
+    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _ ≡⟨ punchOut-punchIn (πʳ i) ⟩
+    j                                                                ∎
 
 ------------------------------------------------------------------------
 -- Lifting
@@ -228,23 +229,23 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ k with i ≟ k
-  ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k
+  ... | yes i≡k rewrite ≟-≡-refl j = i≡k
   ... | no  i≢k
     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
+    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 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
-  ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k
+  ... | yes j≡k rewrite ≟-≡-refl i = j≡k
   ... | no  j≢k
     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
+    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) ⟩
@@ -339,12 +340,7 @@ insert-remove {m = m} {n = n} i π j with i ≟ j
   π ⟨$⟩ʳ j ∎
 
 remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π
-remove-insert i j π k with i ≟ i
-... | no i≢i = contradiction refl i≢i
-... | yes _ = begin
-  punchOut {i = j} _
-    ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩
-  punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym)
-    ≡⟨ punchOut-punchIn j ⟩
-  π ⟨$⟩ʳ k
-    ∎
+remove-insert i j π k rewrite ≟-≡-refl i = begin
+  punchOut {i = j} _                               ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩
+  punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) ≡⟨ punchOut-punchIn j ⟩
+  π ⟨$⟩ʳ k                                         ∎

src/Data/Fin/Permutation/Components.agda

@@ -11,25 +11,17 @@ module Data.Fin.Permutation.Components where
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Fin.Base using (Fin; suc; opposite; toℕ)
 open import Data.Fin.Properties
-  using (_≟_; opposite-prop; opposite-involutive; opposite-suc)
-open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
-open import Data.Product.Base using (proj₂)
-open import Function.Base using (_∘_)
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (does; _because_; yes; no)
-open import Relation.Nullary.Decidable using (dec-true; dec-false)
+  using (_≟_; ≟-≡; ≟-≡-refl
+        ; opposite-prop; opposite-involutive; opposite-suc)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; sym; trans)
-open import Relation.Binary.PropositionalEquality.Properties
-  using (module ≡-Reasoning)
-open import Algebra.Definitions using (Involutive)
-open ≡-Reasoning
+  using (_≡_; refl; sym)
 
 ------------------------------------------------------------------------
 --  Functions
 ------------------------------------------------------------------------
 
--- 'tranpose i j' swaps the places of 'i' and 'j'.
+-- 'transpose i j' swaps the places of 'i' and 'j'.
 
 transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
 transpose i j k with does (k ≟ i)
@@ -42,17 +34,31 @@ transpose i j k with does (k ≟ i)
 --  Properties
 ------------------------------------------------------------------------
 
+transpose[i,i,j]≡j : ∀ {n} (i j : Fin n) → transpose i i j ≡ j
+transpose[i,i,j]≡j i j with j ≟ i in j≟i
+... | yes j≡i           = sym j≡i
+... | no  _ rewrite j≟i = refl
+
+transpose[i,j,j]≡i : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
+transpose[i,j,j]≡i i j with j ≟ i
+... | yes j≡i                     = j≡i
+... | no  _ rewrite ≟-≡-refl j = refl
+
+transpose[i,j,i]≡j : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
+transpose[i,j,i]≡j i j rewrite ≟-≡-refl i = refl
+
+transpose-transpose : ∀ {n} {i j k l : Fin n} →
+                      transpose i j k ≡ l → transpose j i l ≡ k
+transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i
+... | yes k≡i rewrite ≟-≡ (sym eq) = sym k≡i
+... | no k≢i with k ≟ j in k≟j
+...   | yes k≡j rewrite eq | transpose[i,j,j]≡i j l = sym k≡j
+...   | no  k≢j rewrite eq | k≟j | k≟i = refl
+
 transpose-inverse : ∀ {n} (i j : Fin n) {k} →
                     transpose i j (transpose j i k) ≡ k
-transpose-inverse i j {k} with k ≟ j
-... | true  because [k≡j] rewrite dec-true (i ≟ i) refl = sym (invert [k≡j])
-... | false because [k≢j] with k ≟ i
-...   | true  because [k≡i]
-        rewrite dec-false (j ≟ i) (invert [k≢j] ∘ trans (invert [k≡i]) ∘ sym)
-                | dec-true (j ≟ j) refl
-                = sym (invert [k≡i])
-...   | false because [k≢i] rewrite dec-false (k ≟ i) (invert [k≢i])
-                                  | dec-false (k ≟ j) (invert [k≢j]) = refl
+transpose-inverse i j = transpose-transpose refl
+
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

src/Data/Fin/Properties.agda

@@ -11,6 +11,7 @@
 module Data.Fin.Properties where
 
 open import Axiom.Extensionality.Propositional
+open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP)
 open import Algebra.Definitions using (Involutive)
 open import Effect.Applicative using (RawApplicative)
 open import Effect.Functor using (RawFunctor)
@@ -44,10 +45,12 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
   using (module ≡-Reasoning)
+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.Reflects using (Reflects; invert)
+open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
 open import Relation.Unary.Properties using (U?)
@@ -100,6 +103,18 @@ zero  ≟ suc y = no λ()
 suc x ≟ zero  = no λ()
 suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y)
 
+≡-irrelevant : Irrelevant {A = Fin n} _≡_
+≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_
+
+≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
+≟-≡ = ≡-≟-identity _≟_
+
+≟-≡-refl : (i : Fin n)  → (i ≟ i) ≡ yes refl
+≟-≡-refl _ = ≟-≡ refl
+
+≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
+≟-≢ = ≢-≟-identity _≟_
+
 ------------------------------------------------------------------------
 -- Structures
 

src/Data/Nat/Properties.agda

@@ -114,6 +114,9 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq
 ≟-diag = ≡-≟-identity _≟_
 
+≟-≡ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
+≟-≡ = ≢-≟-identity _≟_
+
 ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
 ≡-isDecEquivalence = record
   { isEquivalence = isEquivalence