diff --git a/CHANGELOG.md b/CHANGELOG.md index b9dce3e816..3a4c39e948 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -231,6 +231,41 @@ Additions to existing modules inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x ``` +* Added new functions and proofs to `Algebra.Construct.Flip.Op`: + ```agda + zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙) + distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) + + isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# → + IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1# + isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1# + isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# → + IsCommutativeSemiring + (flip *) 0# 1# + isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# → + IsCancellativeCommutativeSemiring + (flip *) 0# 1# + isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → + IsIdempotentSemiring + (flip *) 0# 1# + isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1# + isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0# + isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# → + IsNonAssociativeRing + (flip *) - 0# 1# + isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1# + isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - + isCommutativeRing : IsCommutativeRing + * - 0# 1# → + IsCommutativeRing + (flip *) - 0# 1# + semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ → + SemiringWithoutAnnihilatingZero a ℓ + commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ + cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ → + CancellativeCommutativeSemiring a ℓ + idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ + quasiring : Quasiring a ℓ → Quasiring a ℓ + ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ + nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ + nearring : Nearring a ℓ → Nearring a ℓ + ring : Ring a ℓ → Ring a ℓ + commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ + ``` + * In `Algebra.Properties.Magma.Divisibility`: ```agda ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ @@ -355,7 +390,12 @@ Additions to existing modules ``` * In `Data.Fin.Properties`: + ```agda + punchIn-mono-≤ : ∀ i (j k : Fin n) → j ≤ k → punchIn i j ≤ punchIn i k + punchIn-cancel-≤ : ∀ i (j k : Fin n) → punchIn i j ≤ punchIn i k → j ≤ k + punchOut-mono-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → j ≤ k → punchOut i≢j ≤ punchOut i≢k + punchOut-cancel-≤ : (i≢j : i ≢ j) (i≢k : i ≢ k) → punchOut i≢j ≤ punchOut i≢k → j ≤ k cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k inject!-injective : Injective _≡_ _≡_ inject! inject!-< : (k : Fin′ i) → inject! k < i @@ -502,6 +542,16 @@ Additions to existing modules HomoProduct n A = HomoProduct′ n (const A) ``` +* In `Data.Sum.Relation.Binary.LeftOrder` : + ```agda + ⊎-<-wellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (∼₁ ⊎-< ∼₂) + ``` + +* in `Data.Sum.Relation.Binary.Pointwise` : + ```agda + ⊎-wellFounded : WellFounded ≈₁ → WellFounded ≈₂ → WellFounded (Pointwise ≈₁ ≈₂) + ``` + * In `Data.Vec.Properties`: ```agda toList-injective : .(m=n : m ≡ n) → (xs : Vec A m) (ys : Vec A n) → toList xs ≡ toList ys → xs ≈[ m=n ] ys diff --git a/src/Algebra/Construct/Flip/Op.agda b/src/Algebra/Construct/Flip/Op.agda index dd139e4ba1..9f2ca10c6d 100644 --- a/src/Algebra/Construct/Flip/Op.agda +++ b/src/Algebra/Construct/Flip/Op.agda @@ -9,9 +9,13 @@ module Algebra.Construct.Flip.Op where -open import Algebra -import Data.Product.Base as Product -import Data.Sum.Base as Sum +open import Algebra.Core +open import Algebra.Bundles +import Algebra.Definitions as Def +import Algebra.Structures as Str +import Algebra.Consequences.Setoid as Consequences +import Data.Product as Prod +import Data.Sum as Sum open import Function.Base using (flip) open import Level using (Level) open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_) @@ -33,136 +37,270 @@ preserves₂ : (∼ ≈ ≋ : Rel A ℓ) → ∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋ preserves₂ _ _ _ pres = flip pres -module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where +module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where - associative : Symmetric ≈ → Associative ≈ ∙ → Associative ≈ (flip ∙) + open Def ≈ + + associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙) associative sym assoc x y z = sym (assoc z y x) - identity : Identity ≈ ε ∙ → Identity ≈ ε (flip ∙) - identity id = Product.swap id + identity : Identity ε ∙ → Identity ε (flip ∙) + identity id = Prod.swap id - commutative : Commutative ≈ ∙ → Commutative ≈ (flip ∙) + commutative : Commutative ∙ → Commutative (flip ∙) commutative comm = flip comm - selective : Selective ≈ ∙ → Selective ≈ (flip ∙) + selective : Selective ∙ → Selective (flip ∙) selective sel x y = Sum.swap (sel y x) - idempotent : Idempotent ≈ ∙ → Idempotent ≈ (flip ∙) + idempotent : Idempotent ∙ → Idempotent (flip ∙) idempotent idem = idem - inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙) - inverse inv = Product.swap inv + inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙) + inverse inv = Prod.swap inv + + zero : Zero ε ∙ → Zero ε (flip ∙) + zero zer = Prod.swap zer + +module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where + + open Def ≈ + + distributes : * DistributesOver + → (flip *) DistributesOver + + distributes distrib = Prod.swap distrib ------------------------------------------------------------------------ -- Structures module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where - isMagma : IsMagma ≈ ∙ → IsMagma ≈ (flip ∙) + open Def ≈ + open Str ≈ + open ∙-Properties ≈ ∙ + + isMagma : IsMagma ∙ → IsMagma (flip ∙) isMagma m = record { isEquivalence = isEquivalence ; ∙-cong = preserves₂ ≈ ≈ ≈ ∙-cong } where open IsMagma m - isSelectiveMagma : IsSelectiveMagma ≈ ∙ → IsSelectiveMagma ≈ (flip ∙) + isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙) isSelectiveMagma m = record { isMagma = isMagma m.isMagma - ; sel = selective ≈ ∙ m.sel + ; sel = selective m.sel } where module m = IsSelectiveMagma m - isCommutativeMagma : IsCommutativeMagma ≈ ∙ → IsCommutativeMagma ≈ (flip ∙) + isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙) isCommutativeMagma m = record { isMagma = isMagma m.isMagma - ; comm = commutative ≈ ∙ m.comm + ; comm = commutative m.comm } where module m = IsCommutativeMagma m - isSemigroup : IsSemigroup ≈ ∙ → IsSemigroup ≈ (flip ∙) + isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙) isSemigroup s = record { isMagma = isMagma s.isMagma - ; assoc = associative ≈ ∙ s.sym s.assoc + ; assoc = associative s.sym s.assoc } where module s = IsSemigroup s - isBand : IsBand ≈ ∙ → IsBand ≈ (flip ∙) + isBand : IsBand ∙ → IsBand (flip ∙) isBand b = record { isSemigroup = isSemigroup b.isSemigroup ; idem = b.idem } where module b = IsBand b - isCommutativeSemigroup : IsCommutativeSemigroup ≈ ∙ → - IsCommutativeSemigroup ≈ (flip ∙) + isCommutativeSemigroup : IsCommutativeSemigroup ∙ → + IsCommutativeSemigroup (flip ∙) isCommutativeSemigroup s = record { isSemigroup = isSemigroup s.isSemigroup - ; comm = commutative ≈ ∙ s.comm + ; comm = commutative s.comm } where module s = IsCommutativeSemigroup s - isUnitalMagma : IsUnitalMagma ≈ ∙ ε → IsUnitalMagma ≈ (flip ∙) ε + isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε isUnitalMagma m = record { isMagma = isMagma m.isMagma - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsUnitalMagma m - isMonoid : IsMonoid ≈ ∙ ε → IsMonoid ≈ (flip ∙) ε + isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε isMonoid m = record { isSemigroup = isSemigroup m.isSemigroup - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsMonoid m - isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε → - IsCommutativeMonoid ≈ (flip ∙) ε + isCommutativeMonoid : IsCommutativeMonoid ∙ ε → + IsCommutativeMonoid (flip ∙) ε isCommutativeMonoid m = record { isMonoid = isMonoid m.isMonoid - ; comm = commutative ≈ ∙ m.comm + ; comm = commutative m.comm } where module m = IsCommutativeMonoid m - isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ≈ ∙ ε → - IsIdempotentCommutativeMonoid ≈ (flip ∙) ε + isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε → + IsIdempotentCommutativeMonoid (flip ∙) ε isIdempotentCommutativeMonoid m = record { isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid - ; idem = idempotent ≈ ∙ m.idem + ; idem = idempotent m.idem } where module m = IsIdempotentCommutativeMonoid m - isInvertibleMagma : IsInvertibleMagma ≈ ∙ ε ⁻¹ → - IsInvertibleMagma ≈ (flip ∙) ε ⁻¹ + isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ → + IsInvertibleMagma (flip ∙) ε ⁻¹ isInvertibleMagma m = record { isMagma = isMagma m.isMagma - ; inverse = inverse ≈ ∙ m.inverse + ; inverse = inverse m.inverse ; ⁻¹-cong = m.⁻¹-cong } where module m = IsInvertibleMagma m - isInvertibleUnitalMagma : IsInvertibleUnitalMagma ≈ ∙ ε ⁻¹ → - IsInvertibleUnitalMagma ≈ (flip ∙) ε ⁻¹ + isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ → + IsInvertibleUnitalMagma (flip ∙) ε ⁻¹ isInvertibleUnitalMagma m = record { isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma - ; identity = identity ≈ ∙ m.identity + ; identity = identity m.identity } where module m = IsInvertibleUnitalMagma m - isGroup : IsGroup ≈ ∙ ε ⁻¹ → IsGroup ≈ (flip ∙) ε ⁻¹ + isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹ isGroup g = record { isMonoid = isMonoid g.isMonoid - ; inverse = inverse ≈ ∙ g.inverse + ; inverse = inverse g.inverse ; ⁻¹-cong = g.⁻¹-cong } where module g = IsGroup g - isAbelianGroup : IsAbelianGroup ≈ ∙ ε ⁻¹ → IsAbelianGroup ≈ (flip ∙) ε ⁻¹ + isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹ isAbelianGroup g = record { isGroup = isGroup g.isGroup - ; comm = commutative ≈ ∙ g.comm + ; comm = commutative g.comm } where module g = IsAbelianGroup g +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} {0# 1# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero + * 0# 1# → + IsSemiringWithoutAnnihilatingZero + (flip *) 0# 1# + isSemiringWithoutAnnihilatingZero r = record + { +-isCommutativeMonoid = r.+-isCommutativeMonoid + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + } + where module r = IsSemiringWithoutAnnihilatingZero r + + isSemiring : IsSemiring + * 0# 1# → IsSemiring + (flip *) 0# 1# + isSemiring r = record + { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero + ; zero = zero r.zero + } + where module r = IsSemiring r + + isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# → + IsCommutativeSemiring + (flip *) 0# 1# + isCommutativeSemiring r = record + { isSemiring = isSemiring r.isSemiring + ; *-comm = commutative r.*-comm + } + where module r = IsCommutativeSemiring r + + isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring + * 0# 1# → + IsCancellativeCommutativeSemiring + (flip *) 0# 1# + isCancellativeCommutativeSemiring r = record + { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring + ; *-cancelˡ-nonZero = Consequences.comm∧almostCancelˡ⇒almostCancelʳ r.setoid r.*-comm r.*-cancelˡ-nonZero + } + where module r = IsCancellativeCommutativeSemiring r + + isIdempotentSemiring : IsIdempotentSemiring + * 0# 1# → + IsIdempotentSemiring + (flip *) 0# 1# + isIdempotentSemiring r = record + { isSemiring = isSemiring r.isSemiring + ; +-idem = r.+-idem + } + where module r = IsIdempotentSemiring r + + isQuasiring : IsQuasiring + * 0# 1# → IsQuasiring + (flip *) 0# 1# + isQuasiring r = record + { +-isMonoid = r.+-isMonoid + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + ; zero = zero r.zero + } + where module r = IsQuasiring r + +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isRingWithoutOne : IsRingWithoutOne + * - 0# → IsRingWithoutOne + (flip *) - 0# + isRingWithoutOne r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; distrib = distributes r.distrib + } + where module r = IsRingWithoutOne r + +module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where + + open Str ≈ + open ∙-Properties ≈ * + open *-Properties ≈ * + + + isNonAssociativeRing : IsNonAssociativeRing + * - 0# 1# → + IsNonAssociativeRing + (flip *) - 0# 1# + isNonAssociativeRing r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + ; zero = zero r.zero + } + where module r = IsNonAssociativeRing r + + isNearring : IsNearring + * 0# 1# - → IsNearring + (flip *) 0# 1# - + isNearring r = record + { isQuasiring = isQuasiring r.isQuasiring + ; +-inverse = r.+-inverse + ; ⁻¹-cong = r.⁻¹-cong + } + where module r = IsNearring r + + isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1# + isRing r = record + { +-isAbelianGroup = r.+-isAbelianGroup + ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong + ; *-assoc = associative r.sym r.*-assoc + ; *-identity = identity r.*-identity + ; distrib = distributes r.distrib + } + where module r = IsRing r + + isCommutativeRing : IsCommutativeRing + * - 0# 1# → + IsCommutativeRing + (flip *) - 0# 1# + isCommutativeRing r = record + { isRing = isRing r.isRing + ; *-comm = commutative r.*-comm + } + where module r = IsCommutativeRing r + + ------------------------------------------------------------------------ -- Bundles @@ -239,3 +377,54 @@ group g = record { isGroup = isGroup g.isGroup } abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup } where module g = AbelianGroup g + +semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ → + SemiringWithoutAnnihilatingZero a ℓ +semiringWithoutAnnihilatingZero r = record + { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero r.isSemiringWithoutAnnihilatingZero } + where module r = SemiringWithoutAnnihilatingZero r + +semiring : Semiring a ℓ → Semiring a ℓ +semiring r = record { isSemiring = isSemiring r.isSemiring } + where module r = Semiring r + +commutativeSemiring : CommutativeSemiring a ℓ → CommutativeSemiring a ℓ +commutativeSemiring r = record + { isCommutativeSemiring = isCommutativeSemiring r.isCommutativeSemiring } + where module r = CommutativeSemiring r + +cancellativeCommutativeSemiring : CancellativeCommutativeSemiring a ℓ → + CancellativeCommutativeSemiring a ℓ +cancellativeCommutativeSemiring r = record + { isCancellativeCommutativeSemiring = isCancellativeCommutativeSemiring r.isCancellativeCommutativeSemiring } + where module r = CancellativeCommutativeSemiring r + +idempotentSemiring : IdempotentSemiring a ℓ → IdempotentSemiring a ℓ +idempotentSemiring r = record + { isIdempotentSemiring = isIdempotentSemiring r.isIdempotentSemiring } + where module r = IdempotentSemiring r + +quasiring : Quasiring a ℓ → Quasiring a ℓ +quasiring r = record { isQuasiring = isQuasiring r.isQuasiring } + where module r = Quasiring r + +ringWithoutOne : RingWithoutOne a ℓ → RingWithoutOne a ℓ +ringWithoutOne r = record { isRingWithoutOne = isRingWithoutOne r.isRingWithoutOne } + where module r = RingWithoutOne r + +nonAssociativeRing : NonAssociativeRing a ℓ → NonAssociativeRing a ℓ +nonAssociativeRing r = record + { isNonAssociativeRing = isNonAssociativeRing r.isNonAssociativeRing } + where module r = NonAssociativeRing r + +nearring : Nearring a ℓ → Nearring a ℓ +nearring r = record { isNearring = isNearring r.isNearring } + where module r = Nearring r + +ring : Ring a ℓ → Ring a ℓ +ring r = record { isRing = isRing r.isRing } + where module r = Ring r + +commutativeRing : CommutativeRing a ℓ → CommutativeRing a ℓ +commutativeRing r = record { isCommutativeRing = isCommutativeRing r.isCommutativeRing } + where module r = CommutativeRing r diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 0f87eef534..f8c476139d 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -869,6 +869,16 @@ punchIn-injective (suc i) (suc j) (suc k) ↑j+1≡↑k+1 = punchInᵢ≢i : ∀ i (j : Fin n) → punchIn i j ≢ i punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective +punchIn-mono-≤ : ∀ i (j k : Fin n) → j ≤ k → punchIn i j ≤ punchIn i k +punchIn-mono-≤ zero _ _ j≤k = s≤s j≤k +punchIn-mono-≤ (suc _) zero _ z≤n = z≤n +punchIn-mono-≤ (suc i) (suc j) (suc k) (s≤s j≤k) = s≤s (punchIn-mono-≤ i j k j≤k) + +punchIn-cancel-≤ : ∀ i (j k : Fin n) → punchIn i j ≤ punchIn i k → j ≤ k +punchIn-cancel-≤ zero _ _ (s≤s j≤k) = j≤k +punchIn-cancel-≤ (suc _) zero _ z≤n = z≤n +punchIn-cancel-≤ (suc i) (suc j) (suc k) (s≤s ↑j≤↑k) = s≤s (punchIn-cancel-≤ i j k ↑j≤↑k) + ------------------------------------------------------------------------ -- punchOut ------------------------------------------------------------------------ @@ -903,6 +913,22 @@ 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ₖ)) +punchOut-mono-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → + j ≤ k → punchOut i≢j ≤ punchOut i≢k +punchOut-mono-≤ {_ } {zero } {zero } {_ } 0≢0 _ z≤n = contradiction refl 0≢0 +punchOut-mono-≤ {_ } {zero } {suc _} {suc _} _ _ (s≤s j≤k) = j≤k +punchOut-mono-≤ {suc _} {suc _} {zero } {_ } _ _ z≤n = z≤n +punchOut-mono-≤ {suc _} {suc _} {suc _} {suc _} i≢j i≢k (s≤s j≤k) = s≤s (punchOut-mono-≤ (i≢j ∘ cong suc) (i≢k ∘ cong suc) j≤k) + +punchOut-cancel-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) → + punchOut i≢j ≤ punchOut i≢k → j ≤ k +punchOut-cancel-≤ {_ } {zero } {zero } {_ } 0≢0 _ _ = contradiction refl 0≢0 +punchOut-cancel-≤ {_ } {zero } {suc _} {zero } _ 0≢0 _ = contradiction refl 0≢0 +punchOut-cancel-≤ {suc _} {zero } {suc _} {suc _} _ _ pⱼ≤pₖ = s≤s pⱼ≤pₖ +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 i (punchOut i≢j) ≡ j punchIn-punchOut {_} {zero} {zero} 0≢0 = contradiction refl 0≢0 diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda index ba80960eb1..f162dd56dc 100644 --- a/src/Data/Sum/Relation/Binary/LeftOrder.agda +++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda @@ -14,6 +14,7 @@ open import Data.Sum.Relation.Binary.Pointwise as PW open import Data.Product.Base using (_,_) open import Data.Empty using (⊥) open import Function.Base using (_$_; _∘_) +open import Induction.WellFounded open import Level using (Level; _⊔_) open import Relation.Nullary.Negation.Core using (¬_) open import Relation.Nullary.Decidable.Core using (yes; no) @@ -89,6 +90,20 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₁ y) = no λ() ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = Dec.map′ ₂∼₂ drop-inj₂ (dec₂ x y) + ⊎-<-wellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (∼₁ ⊎-< ∼₂) + ⊎-<-wellFounded wf₁ wf₂ x = acc (⊎-<-acc x) + where + ⊎-<-acc₁ : ∀ {x} → Acc ∼₁ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) (inj₁ x) + ⊎-<-acc₁ (acc rec) (₁∼₁ x∼₁y) = acc (⊎-<-acc₁ (rec x∼₁y)) + + ⊎-<-acc₂ : ∀ {x} → Acc ∼₂ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) (inj₂ x) + ⊎-<-acc₂ (acc rec) {inj₁ x} ₁∼₂ = acc (⊎-<-acc₁ (wf₁ x)) + ⊎-<-acc₂ (acc rec) (₂∼₂ x∼₂y) = acc (⊎-<-acc₂ (rec x∼₂y)) + + ⊎-<-acc : ∀ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) x + ⊎-<-acc (inj₁ x) = ⊎-<-acc₁ (wf₁ x) + ⊎-<-acc (inj₂ x) = ⊎-<-acc₂ (wf₂ x) + module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂} {ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄} diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index a52c37f876..6e65ba9691 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -10,6 +10,7 @@ module Data.Sum.Relation.Binary.Pointwise where open import Data.Product.Base using (_,_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) +open import Induction.WellFounded open import Level using (Level; _⊔_) open import Function.Base using (const; _∘_; id) open import Function.Bundles using (Inverse; mk↔) @@ -93,6 +94,19 @@ drop-inj₂ (inj₂ x) = x ⊎-irreflexive irrefl₁ irrefl₂ (inj₁ x) (inj₁ y) = irrefl₁ x y ⊎-irreflexive irrefl₁ irrefl₂ (inj₂ x) (inj₂ y) = irrefl₂ x y +⊎-wellFounded : WellFounded ≈₁ → WellFounded ≈₂ → WellFounded (Pointwise ≈₁ ≈₂) +⊎-wellFounded {≈₁ = ≈₁} {≈₂ = ≈₂} wf₁ wf₂ x = acc (⊎-acc x) + where + ⊎-acc₁ : ∀ {x} → Acc ≈₁ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) (inj₁ x) + ⊎-acc₁ (acc rec) (inj₁ x≈₁y) = acc (⊎-acc₁ (rec x≈₁y)) + + ⊎-acc₂ : ∀ {x} → Acc ≈₂ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) (inj₂ x) + ⊎-acc₂ (acc rec) (inj₂ x≈₂y) = acc (⊎-acc₂ (rec x≈₂y)) + + ⊎-acc : ∀ x → WfRec (Pointwise ≈₁ ≈₂) (Acc (Pointwise ≈₁ ≈₂)) x + ⊎-acc (inj₁ x) = ⊎-acc₁ (wf₁ x) + ⊎-acc (inj₂ x) = ⊎-acc₂ (wf₂ x) + ⊎-antisymmetric : Antisymmetric ≈₁ R → Antisymmetric ≈₂ S → Antisymmetric (Pointwise ≈₁ ≈₂) (Pointwise R S) ⊎-antisymmetric antisym₁ antisym₂ (inj₁ x) (inj₁ y) = inj₁ (antisym₁ x y)