diff --git a/CHANGELOG.md b/CHANGELOG.md index ef9533efc6..2720bead21 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index c502512448..3486440c6a 100644 --- a/src/Data/Fin/Base.agda +++ b/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)) diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda index 078e53c3bb..7e52e2898f 100644 --- a/src/Data/Fin/Permutation.agda +++ b/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 ∎ diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 48bcf8a5ee..f402ea8252 100644 --- a/src/Data/Fin/Properties.agda +++ b/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