diff options
Diffstat (limited to 'CHANGELOG/v0.14.md')
| -rw-r--r-- | CHANGELOG/v0.14.md | 772 |
1 files changed, 772 insertions, 0 deletions
diff --git a/CHANGELOG/v0.14.md b/CHANGELOG/v0.14.md new file mode 100644 index 0000000..9cd0154 --- /dev/null +++ b/CHANGELOG/v0.14.md @@ -0,0 +1,772 @@ +Version 0.14 +============ + +The library has been tested using Agda version 2.5.3. + +Non-backwards compatible changes +-------------------------------- + +#### 1st stage of overhaul of list membership + +* The current setup for list membership is difficult to work with as both setoid membership + and propositional membership exist as internal modules of `Data.Any`. Furthermore the + top-level module `Data.List.Any.Membership` actually contains properties of propositional + membership rather than the membership relation itself as its name would suggest. + Consequently this leaves no place to reason about the properties of setoid membership. + + Therefore the two internal modules `Membership` and `Membership-≡` have been moved out + of `Data.List.Any` into top-level `Data.List.Any.Membership` and + `Data.List.Any.Membership.Propositional` respectively. The previous module + `Data.List.Any.Membership` has been renamed + `Data.List.Any.Membership.Propositional.Properties`. + + Accordingly some lemmas have been moved to more logical locations: + - `lift-resp` has been moved from `Data.List.Any.Membership` to `Data.List.Any.Properties` + - `∈-resp-≈`, `⊆-preorder` and `⊆-Reasoning` have been moved from `Data.List.Any.Membership` + to `Data.List.Any.Membership.Properties`. + - `∈-resp-list-≈` has been moved from `Data.List.Any.Membership` to + `Data.List.Any.Membership.Properties` and renamed `∈-resp-≋`. + - `swap` in `Data.List.Any.Properties` has been renamed `swap↔` and made more generic with + respect to levels. + +#### Moving `decTotalOrder` and `decSetoid` from `Data.X` to `Data.X.Properties` + +* Currently the library does not directly expose proofs of basic properties such as reflexivity, + transitivity etc. for `_≤_` in numeric datatypes such as `Nat`, `Integer` etc. In order to use these + properties it was necessary to first import the `decTotalOrder` proof from `Data.X` and then + separately open it, often having to rename the proofs as well. This adds unneccessary lines of + code to the import statements for what are very commonly used properties. + + These basic proofs have now been added in `Data.X.Properties` along with proofs that they form + pre-orders, partial orders and total orders. This should make them considerably easier to work with + and simplify files' import preambles. However consequently the records `decTotalOrder` and + `decSetoid` have been moved from `Data.X` to `≤-decTotalOrder` and `≡-decSetoid` in + `Data.X.Properties`. + + The numeric datatypes for which this has been done are `Nat`, `Integer`, `Rational` and `Bin`. + + As a consequence the module `≤-Reasoning` has also had to have been moved from `Data.Nat` to + `Data.Nat.Properties`. + +#### New well-founded induction proofs for `Data.Nat` + +* Currently `Induction.Nat` only proves that the non-standard `_<′_`relation over `ℕ` is + well-founded. Unfortunately these existing proofs are named `<-Rec` and `<-well-founded` + which clash with the sensible names for new proofs over the standard `_<_` relation. + + Therefore `<-Rec` and `<-well-founded` have been renamed to `<′-Rec` and `<′-well-founded` + respectively. The original names `<-Rec` and `<-well-founded` now refer to new + corresponding proofs for `_<_`. + +#### Other + +* Changed the implementation of `map` and `zipWith` in `Data.Vec` to use native + (pattern-matching) definitions. Previously they were defined using the + `applicative` operations of `Vec`. The new definitions can be converted back + to the old using the new proofs `⊛-is-zipWith`, `map-is-⊛` and `zipWith-is-⊛` + in `Data.Vec.Properties`. It has been argued that `zipWith` is fundamental than `_⊛_` + and this change allows better printing of goals involving `map` or `zipWith`. + +* Changed the implementation of `All₂` in `Data.Vec.All` to a native datatype. This + improved improves pattern matching on terms and allows the new datatype to be more + generic with respect to types and levels. + +* Changed the implementation of `downFrom` in `Data.List` to a native + (pattern-matching) definition. Previously it was defined using a private + internal module which made pattern matching difficult. + +* The arguments of `≤pred⇒≤` and `≤⇒pred≤` in `Data.Nat.Properties` are now implicit + rather than explicit (was `∀ m n → m ≤ pred n → m ≤ n` and is now + `∀ {m n} → m ≤ pred n → m ≤ n`). This makes it consistent with `<⇒≤pred` which + already used implicit arguments, and shouldn't introduce any significant problems + as both parameters can be inferred by Agda. + +* Moved `¬∀⟶∃¬` from `Relation.Nullary.Negation` to `Data.Fin.Dec`. Its old + location was causing dependency cyles to form between `Data.Fin.Dec`, + `Relation.Nullary.Negation` and `Data.Fin`. + +* Moved `fold`, `add` and `mul` from `Data.Nat` to new module `Data.Nat.GeneralisedArithmetic`. + +* Changed type of second parameter of `Relation.Binary.StrictPartialOrderReasoning._<⟨_⟩_` + from `x < y ⊎ x ≈ y` to `x < y`. `_≈⟨_⟩_` is left unchanged to take a value with type `x ≈ y`. + Old code may be fixed by prefixing the contents of `_<⟨_⟩_` with `inj₁`. + +Deprecated features +------------------- + +Deprecated features still exist and therefore existing code should still work +but they may be removed in some future release of the library. + +* The module `Data.Nat.Properties.Simple` is now deprecated. All proofs + have been moved to `Data.Nat.Properties` where they should be used directly. + The `Simple` file still exists for backwards compatability reasons and + re-exports the proofs from `Data.Nat.Properties` but will be removed in some + future release. + +* The modules `Data.Integer.Addition.Properties` and + `Data.Integer.Multiplication.Properties` are now deprecated. All proofs + have been moved to `Data.Integer.Properties` where they should be used + directly. The `Addition.Properties` and `Multiplication.Properties` files + still exist for backwards compatability reasons and re-exports the proofs from + `Data.Integer.Properties` but will be removed in some future release. + +* The following renaming has occured in `Data.Nat.Properties` + ```agda + _+-mono_ ↦ +-mono-≤ + _*-mono_ ↦ *-mono-≤ + + +-right-identity ↦ +-identityʳ + *-right-zero ↦ *-zeroʳ + distribʳ-*-+ ↦ *-distribʳ-+ + *-distrib-∸ʳ ↦ *-distribʳ-∸ + cancel-+-left ↦ +-cancelˡ-≡ + cancel-+-left-≤ ↦ +-cancelˡ-≤ + cancel-*-right ↦ *-cancelʳ-≡ + cancel-*-right-≤ ↦ *-cancelʳ-≤ + + strictTotalOrder ↦ <-strictTotalOrder + isCommutativeSemiring ↦ *-+-isCommutativeSemiring + commutativeSemiring ↦ *-+-commutativeSemiring + isDistributiveLattice ↦ ⊓-⊔-isDistributiveLattice + distributiveLattice ↦ ⊓-⊔-distributiveLattice + ⊔-⊓-0-isSemiringWithoutOne ↦ ⊔-⊓-isSemiringWithoutOne + ⊔-⊓-0-isCommutativeSemiringWithoutOne ↦ ⊔-⊓-isCommutativeSemiringWithoutOne + ⊔-⊓-0-commutativeSemiringWithoutOne ↦ ⊔-⊓-commutativeSemiringWithoutOne + ``` + +* The following renaming has occurred in `Data.Nat.Divisibility`: + ```agda + ∣-* ↦ n|m*n + ∣-+ ↦ ∣m∣n⇒∣m+n + ∣-∸ ↦ ∣m+n|m⇒|n + ``` + +Backwards compatible changes +---------------------------- + +* Added support for GHC 8.0.2 and 8.2.1. + +* Removed the empty `Irrelevance` module + +* Added `Category.Functor.Morphism` and module `Category.Functor.Identity`. + +* `Data.Container` and `Data.Container.Indexed` now allow for different + levels in the container and in the data it contains. + +* Made `Data.BoundedVec` polymorphic with respect to levels. + +* Access to `primForce` and `primForceLemma` has been provided via the new + top-level module `Strict`. + +* New call-by-value application combinator `_$!_` in `Function`. + +* Added properties to `Algebra.FunctionProperties`: + ```agda + LeftCancellative _•_ = ∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z + RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z + Cancellative _•_ = LeftCancellative _•_ × RightCancellative _•_ + ``` + +* Added new module `Algebra.FunctionProperties.Consequences` for basic causal relationships between + properties, containing: + ```agda + comm+idˡ⇒idʳ : Commutative _•_ → LeftIdentity e _•_ → RightIdentity e _•_ + comm+idʳ⇒idˡ : Commutative _•_ → RightIdentity e _•_ → LeftIdentity e _•_ + comm+zeˡ⇒zeʳ : Commutative _•_ → LeftZero e _•_ → RightZero e _•_ + comm+zeʳ⇒zeˡ : Commutative _•_ → RightZero e _•_ → LeftZero e _•_ + comm+invˡ⇒invʳ : Commutative _•_ → LeftInverse e _⁻¹ _•_ → RightInverse e _⁻¹ _•_ + comm+invʳ⇒invˡ : Commutative _•_ → RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_ + comm+distrˡ⇒distrʳ : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_ + comm+distrʳ⇒distrˡ : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_ + comm+cancelˡ⇒cancelʳ : Commutative _•_ → LeftCancellative _•_ → RightCancellative _•_ + comm+cancelˡ⇒cancelʳ : Commutative _•_ → LeftCancellative _•_ → RightCancellative _•_ + sel⇒idem : Selective _•_ → Idempotent _•_ + ``` + +* Added proofs to `Algebra.Properties.BooleanAlgebra`: + ```agda + ∨-complementˡ : LeftInverse ⊤ ¬_ _∨_ + ∧-complementˡ : LeftInverse ⊥ ¬_ _∧_ + + ∧-identityʳ : RightIdentity ⊤ _∧_ + ∧-identityˡ : LeftIdentity ⊤ _∧_ + ∧-identity : Identity ⊤ _∧_ + + ∨-identityʳ : RightIdentity ⊥ _∨_ + ∨-identityˡ : LeftIdentity ⊥ _∨_ + ∨-identity : Identity ⊥ _∨_ + + ∧-zeroʳ : RightZero ⊥ _∧_ + ∧-zeroˡ : LeftZero ⊥ _∧_ + ∧-zero : Zero ⊥ _∧_ + + ∨-zeroʳ : RightZero ⊤ _∨_ + ∨-zeroˡ : LeftZero ⊤ _∨_ + ∨-zero : Zero ⊤ _∨_ + + ⊕-identityˡ : LeftIdentity ⊥ _⊕_ + ⊕-identityʳ : RightIdentity ⊥ _⊕_ + ⊕-identity : Identity ⊥ _⊕_ + + ⊕-inverseˡ : LeftInverse ⊥ id _⊕_ + ⊕-inverseʳ : RightInverse ⊥ id _⊕_ + ⊕-inverse : Inverse ⊥ id _⊕_ + + ⊕-cong : Congruent₂ _⊕_ + ⊕-comm : Commutative _⊕_ + ⊕-assoc : Associative _⊕_ + + ∧-distribˡ-⊕ : _∧_ DistributesOverˡ _⊕_ + ∧-distribʳ-⊕ : _∧_ DistributesOverʳ _⊕_ + ∧-distrib-⊕ : _∧_ DistributesOver _⊕_ + + ∨-isSemigroup : IsSemigroup _≈_ _∨_ + ∧-isSemigroup : IsSemigroup _≈_ _∧_ + ∨-⊥-isMonoid : IsMonoid _≈_ _∨_ ⊥ + ∧-⊤-isMonoid : IsMonoid _≈_ _∧_ ⊤ + ∨-⊥-isCommutativeMonoid : IsCommutativeMonoid _≈_ _∨_ ⊥ + ∧-⊤-isCommutativeMonoid : IsCommutativeMonoid _≈_ _∧_ ⊤ + + ⊕-isSemigroup : IsSemigroup _≈_ _⊕_ + ⊕-⊥-isMonoid : IsMonoid _≈_ _⊕_ ⊥ + ⊕-⊥-isGroup : IsGroup _≈_ _⊕_ ⊥ id + ⊕-⊥-isAbelianGroup : IsAbelianGroup _≈_ _⊕_ ⊥ id + ⊕-∧-isRing : IsRing _≈_ _⊕_ _∧_ id ⊥ ⊤ + ``` + +* Added proofs to `Algebra.Properties.DistributiveLattice`: + ```agda + ∨-∧-distribˡ : _∨_ DistributesOverˡ _∧_ + ∧-∨-distribˡ : _∧_ DistributesOverˡ _∨_ + ∧-∨-distribʳ : _∧_ DistributesOverʳ _∨_ + ``` + +* Added pattern synonyms to `Data.Bin` to improve readability: + ```agda + pattern 0b = zero + pattern 1b = 1+ zero + pattern ⊥b = 1+ 1+ () + ``` + +* A new module `Data.Bin.Properties` has been added, containing proofs: + ```agda + 1#-injective : as 1# ≡ bs 1# → as ≡ bs + _≟_ : Decidable {A = Bin} _≡_ + ≡-isDecEquivalence : IsDecEquivalence _≡_ + ≡-decSetoid : DecSetoid _ _ + + <-trans : Transitive _<_ + <-asym : Asymmetric _<_ + <-irrefl : Irreflexive _≡_ _<_ + <-cmp : Trichotomous _≡_ _<_ + <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_ + + <⇒≢ : a < b → a ≢ b + 1<[23] : [] 1# < (b ∷ []) 1# + 1<2+ : [] 1# < (b ∷ bs) 1# + 0<1+ : 0# < bs 1# + ``` + +* Added functions to `Data.BoundedVec`: + ```agda + toInefficient : BoundedVec A n → Ineff.BoundedVec A n + fromInefficient : Ineff.BoundedVec A n → BoundedVec A n + ``` + +* Added the following to `Data.Digit`: + ```agda + Expansion : ℕ → Set + Expansion base = List (Fin base) + ``` + +* Added new module `Data.Empty.Irrelevant` containing an irrelevant version of `⊥-elim`. + +* Added functions to `Data.Fin`: + ```agda + punchIn i j ≈ if j≥i then j+1 else j + punchOut i j ≈ if j>i then j-1 else j + ``` + +* Added proofs to `Data.Fin.Properties`: + ```agda + isDecEquivalence : ∀ {n} → IsDecEquivalence (_≡_ {A = Fin n}) + + ≤-reflexive : ∀ {n} → _≡_ ⇒ (_≤_ {n}) + ≤-refl : ∀ {n} → Reflexive (_≤_ {n}) + ≤-trans : ∀ {n} → Transitive (_≤_ {n}) + ≤-antisymmetric : ∀ {n} → Antisymmetric _≡_ (_≤_ {n}) + ≤-total : ∀ {n} → Total (_≤_ {n}) + ≤-isPreorder : ∀ {n} → IsPreorder _≡_ (_≤_ {n}) + ≤-isPartialOrder : ∀ {n} → IsPartialOrder _≡_ (_≤_ {n}) + ≤-isTotalOrder : ∀ {n} → IsTotalOrder _≡_ (_≤_ {n}) + + _<?_ : ∀ {n} → Decidable (_<_ {n}) + <-trans : ∀ {n} → Transitive (_<_ {n}) + <-isStrictTotalOrder : ∀ {n} → IsStrictTotalOrder _≡_ (_<_ {n}) + + punchOut-injective : punchOut i≢j ≡ punchOut i≢k → j ≡ k + punchIn-injective : punchIn i j ≡ punchIn i k → j ≡ k + punchIn-punchOut : punchIn i (punchOut i≢j) ≡ j + punchInᵢ≢i : punchIn i j ≢ i + ``` + +* Added proofs to `Data.Fin.Subset.Properties`: + ```agda + x∈⁅x⁆ : x ∈ ⁅ x ⁆ + x∈⁅y⁆⇒x≡y : x ∈ ⁅ y ⁆ → x ≡ y + + ∪-assoc : Associative _≡_ _∪_ + ∩-assoc : Associative _≡_ _∩_ + ∪-comm : Commutative _≡_ _∪_ + ∩-comm : Commutative _≡_ _∩_ + + p⊆p∪q : p ⊆ p ∪ q + q⊆p∪q : q ⊆ p ∪ q + x∈p∪q⁻ : x ∈ p ∪ q → x ∈ p ⊎ x ∈ q + x∈p∪q⁺ : x ∈ p ⊎ x ∈ q → x ∈ p ∪ q + + p∩q⊆p : p ∩ q ⊆ p + p∩q⊆q : p ∩ q ⊆ q + x∈p∩q⁺ : x ∈ p × x ∈ q → x ∈ p ∩ q + x∈p∩q⁻ : x ∈ p ∩ q → x ∈ p × x ∈ q + ∩⇔× : x ∈ p ∩ q ⇔ (x ∈ p × x ∈ q) + ``` + +* Added relations to `Data.Integer` + ```agda + _≥_ : Rel ℤ _ + _<_ : Rel ℤ _ + _>_ : Rel ℤ _ + _≰_ : Rel ℤ _ + _≱_ : Rel ℤ _ + _≮_ : Rel ℤ _ + _≯_ : Rel ℤ _ + ``` + +* Added proofs to `Data.Integer.Properties` + ```agda + +-injective : + m ≡ + n → m ≡ n + -[1+-injective : -[1+ m ] ≡ -[1+ n ] → m ≡ n + + doubleNeg : - - n ≡ n + neg-injective : - m ≡ - n → m ≡ n + + ∣n∣≡0⇒n≡0 : ∣ n ∣ ≡ 0 → n ≡ + 0 + ∣-n∣≡∣n∣ : ∣ - n ∣ ≡ ∣ n ∣ + + +◃n≡+n : Sign.+ ◃ n ≡ + n + -◃n≡-n : Sign.- ◃ n ≡ - + n + signₙ◃∣n∣≡n : sign n ◃ ∣ n ∣ ≡ n + ∣s◃m∣*∣t◃n∣≡m*n : ∣ s ◃ m ∣ ℕ* ∣ t ◃ n ∣ ≡ m ℕ* n + + ⊖-≰ : n ≰ m → m ⊖ n ≡ - + (n ∸ m) + ∣⊖∣-≰ : n ≰ m → ∣ m ⊖ n ∣ ≡ n ∸ m + sign-⊖-≰ : n ≰ m → sign (m ⊖ n) ≡ Sign.- + -[n⊖m]≡-m+n : - (m ⊖ n) ≡ (- (+ m)) + (+ n) + + +-identity : Identity (+ 0) _+_ + +-inverse : Inverse (+ 0) -_ _+_ + +-0-isMonoid : IsMonoid _≡_ _+_ (+ 0) + +-0-isGroup : IsGroup _≡_ _+_ (+ 0) (-_) + +-0-abelianGroup : AbelianGroup _ _ + + n≢1+n : n ≢ suc n + 1-[1+n]≡-n : suc -[1+ n ] ≡ - (+ n) + neg-distrib-+ : - (m + n) ≡ (- m) + (- n) + ◃-distrib-+ : s ◃ (m + n) ≡ (s ◃ m) + (s ◃ n) + + *-identityʳ : RightIdentity (+ 1) _*_ + *-identity : Identity (+ 1) _*_ + *-zeroˡ : LeftZero (+ 0) _*_ + *-zeroʳ : RightZero (+ 0) _*_ + *-zero : Zero (+ 0) _*_ + *-1-isMonoid : IsMonoid _≡_ _*_ (+ 1) + -1*n≡-n : -[1+ 0 ] * n ≡ - n + ◃-distrib-* : (s 𝕊* t) ◃ (m ℕ* n) ≡ (s ◃ m) * (t ◃ n) + + +-*-isRing : IsRing _≡_ _+_ _*_ -_ (+ 0) (+ 1) + +-*-isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (+ 0) (+ 1) + + ≤-reflexive : _≡_ ⇒ _≤_ + ≤-refl : Reflexive _≤_ + ≤-trans : Transitive _≤_ + ≤-antisym : Antisymmetric _≡_ _≤_ + ≤-total : Total _≤_ + + ≤-isPreorder : IsPreorder _≡_ _≤_ + ≤-isPartialOrder : IsPartialOrder _≡_ _≤_ + ≤-isTotalOrder : IsTotalOrder _≡_ _≤_ + ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_ + + ≤-step : n ≤ m → n ≤ suc m + n≤1+n : n ≤ + 1 + n + + <-irrefl : Irreflexive _≡_ _<_ + <-asym : Asymmetric _<_ + <-trans : Transitive _<_ + <-cmp : Trichotomous _≡_ _<_ + <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_ + + n≮n : n ≮ n + -<+ : -[1+ m ] < + n + <⇒≤ : m < n → m ≤ n + ≰→> : x ≰ y → x > y + ``` + +* Added functions to `Data.List` + ```agda + applyUpTo f n ≈ f[0] ∷ f[1] ∷ ... ∷ f[n-1] ∷ [] + upTo n ≈ 0 ∷ 1 ∷ ... ∷ n-1 ∷ [] + applyDownFrom f n ≈ f[n-1] ∷ f[n-2] ∷ ... ∷ f[0] ∷ [] + tabulate f ≈ f[0] ∷ f[1] ∷ ... ∷ f[n-1] ∷ [] + allFin n ≈ 0f ∷ 1f ∷ ... ∷ n-1f ∷ [] + ``` + +* Added proofs to `Data.List.Properties` + ```agda + map-id₂ : All (λ x → f x ≡ x) xs → map f xs ≡ xs + map-cong₂ : All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs + foldr-++ : foldr f x (ys ++ zs) ≡ foldr f (foldr f x zs) ys + foldl-++ : foldl f x (ys ++ zs) ≡ foldl f (foldl f x ys) zs + foldr-∷ʳ : foldr f x (ys ∷ʳ y) ≡ foldr f (f y x) ys + foldl-∷ʳ : foldl f x (ys ∷ʳ y) ≡ f (foldl f x ys) y + reverse-foldr : foldr f x (reverse ys) ≡ foldl (flip f) x ys + reverse-foldr : foldl f x (reverse ys) ≡ foldr (flip f) x ys + length-reverse : length (reverse xs) ≡ length xs + ``` + +* Added proofs to `Data.List.All.Properties` + ```agda + All-universal : Universal P → All P xs + + ¬Any⇒All¬ : ¬ Any P xs → All (¬_ ∘ P) xs + All¬⇒¬Any : All (¬_ ∘ P) xs → ¬ Any P xs + ¬All⇒Any¬ : Decidable P → ¬ All P xs → Any (¬_ ∘ P) xs + + ++⁺ : All P xs → All P ys → All P (xs ++ ys) + ++⁻ˡ : All P (xs ++ ys) → All P xs + ++⁻ʳ : All P (xs ++ ys) → All P ys + ++⁻ : All P (xs ++ ys) → All P xs × All P ys + + concat⁺ : All (All P) xss → All P (concat xss) + concat⁻ : All P (concat xss) → All (All P) xss + + drop⁺ : All P xs → All P (drop n xs) + take⁺ : All P xs → All P (take n xs) + + tabulate⁺ : (∀ i → P (f i)) → All P (tabulate f) + tabulate⁻ : All P (tabulate f) → (∀ i → P (f i)) + + applyUpTo⁺₁ : (∀ {i} → i < n → P (f i)) → All P (applyUpTo f n) + applyUpTo⁺₂ : (∀ i → P (f i)) → All P (applyUpTo f n) + applyUpTo⁻ : All P (applyUpTo f n) → ∀ {i} → i < n → P (f i) + ``` + +* Added proofs to `Data.List.Any.Properties` + ```agda + lose∘find : uncurry′ lose (proj₂ (find p)) ≡ p + find∘lose : find (lose x∈xs pp) ≡ (x , x∈xs , pp) + + swap : Any (λ x → Any (P x) ys) xs → Any (λ y → Any (flip P y) xs) ys + swap-invol : swap (swap any) ≡ any + + ∃∈-Any : (∃ λ x → x ∈ xs × P x) → Any P xs + + Any-⊎⁺ : Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs + Any-⊎⁻ : Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs + Any-×⁺ : Any P xs × Any Q ys → Any (λ x → Any (λ y → P x × Q y) ys) xs + Any-×⁻ : Any (λ x → Any (λ y → P x × Q y) ys) xs → Any P xs × Any Q ys + + map⁺ : Any (P ∘ f) xs → Any P (map f xs) + map⁻ : Any P (map f xs) → Any (P ∘ f) xs + + ++⁺ˡ : Any P xs → Any P (xs ++ ys) + ++⁺ʳ : Any P ys → Any P (xs ++ ys) + ++⁻ : Any P (xs ++ ys) → Any P xs ⊎ Any P ys + + concat⁺ : Any (Any P) xss → Any P (concat xss) + concat⁻ : Any P (concat xss) → Any (Any P) xss + + applyUpTo⁺ : P (f i) → i < n → Any P (applyUpTo f n) + applyUpTo⁻ : Any P (applyUpTo f n) → ∃ λ i → i < n × P (f i) + + tabulate⁺ : P (f i) → Any P (tabulate f) + tabulate⁻ : Any P (tabulate f) → ∃ λ i → P (f i) + + map-with-∈⁺ : (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) → Any P (map-with-∈ xs f) + map-with-∈⁻ : Any P (map-with-∈ xs f) → ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs) + + return⁺ : P x → Any P (return x) + return⁻ : Any P (return x) → P x + ``` + +* Added proofs to `Data.List.Any.Membership.Properties` + ```agda + ∈-map⁺ : x ∈ xs → f x ∈ map f xs + ∈-map⁻ : y ∈ map f xs → ∃ λ x → x ∈ xs × y ≈ f x + ``` + +* Added proofs to `Data.List.Any.Membership.Propositional.Properties` + ```agda + ∈-map⁺ : x ∈ xs → f x ∈ map f xs + ∈-map⁻ : y ∈ map f xs → ∃ λ x → x ∈ xs × y ≈ f x + ``` + +* Added proofs to `Data.Maybe`: + ```agda + Eq-refl : Reflexive _≈_ → Reflexive (Eq _≈_) + Eq-sym : Symmetric _≈_ → Symmetric (Eq _≈_) + Eq-trans : Transitive _≈_ → Transitive (Eq _≈_) + Eq-dec : Decidable _≈_ → Decidable (Eq _≈_) + Eq-isEquivalence : IsEquivalence _≈_ → IsEquivalence (Eq _≈_) + Eq-isDecEquivalence : IsDecEquivalence _≈_ → IsDecEquivalence (Eq _≈_) + ``` + +* Added exponentiation operator `_^_` to `Data.Nat.Base` + +* Added proofs to `Data.Nat.Properties`: + ```agda + suc-injective : suc m ≡ suc n → m ≡ n + ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ}) + ≡-decSetoid : DecSetoid _ _ + + ≤-reflexive : _≡_ ⇒ _≤_ + ≤-refl : Reflexive _≤_ + ≤-trans : Antisymmetric _≡_ _≤_ + ≤-antisymmetric : Transitive _≤_ + ≤-total : Total _≤_ + ≤-isPreorder : IsPreorder _≡_ _≤_ + ≤-isPartialOrder : IsPartialOrder _≡_ _≤_ + ≤-isTotalOrder : IsTotalOrder _≡_ _≤_ + ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_ + + _<?_ : Decidable _<_ + <-irrefl : Irreflexive _≡_ _<_ + <-asym : Asymmetric _<_ + <-transʳ : Trans _≤_ _<_ _<_ + <-transˡ : Trans _<_ _≤_ _<_ + <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_ + <⇒≤ : _<_ ⇒ _≤_ + <⇒≢ : _<_ ⇒ _≢_ + <⇒≱ : _<_ ⇒ _≱_ + <⇒≯ : _<_ ⇒ _≯_ + ≰⇒≮ : _≰_ ⇒ _≮_ + ≰⇒≥ : _≰_ ⇒ _≥_ + ≮⇒≥ : _≮_ ⇒ _≥_ + ≤+≢⇒< : m ≤ n → m ≢ n → m < n + + +-identityˡ : LeftIdentity 0 _+_ + +-identity : Identity 0 _+_ + +-cancelʳ-≡ : RightCancellative _≡_ _+_ + +-cancel-≡ : Cancellative _≡_ _+_ + +-cancelʳ-≤ : RightCancellative _≤_ _+_ + +-cancel-≤ : Cancellative _≤_ _+_ + +-isSemigroup : IsSemigroup _≡_ _+_ + +-monoˡ-< : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_ + +-monoʳ-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_ + +-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_ + m+n≤o⇒m≤o : m + n ≤ o → m ≤ o + m+n≤o⇒n≤o : m + n ≤ o → n ≤ o + m+n≮n : m + n ≮ n + + *-zeroˡ : LeftZero 0 _*_ + *-zero : Zero 0 _*_ + *-identityˡ : LeftIdentity 1 _*_ + *-identityʳ : RightIdentity 1 _*_ + *-identity : Identity 1 _*_ + *-distribˡ-+ : _*_ DistributesOverˡ _+_ + *-distrib-+ : _*_ DistributesOver _+_ + *-isSemigroup : IsSemigroup _≡_ _*_ + *-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_ + *-monoˡ-< : (_* suc n) Preserves _<_ ⟶ _<_ + *-monoʳ-< : (suc n *_) Preserves _<_ ⟶ _<_ + *-cancelˡ-≡ : suc k * i ≡ suc k * j → i ≡ j + + ^-distribˡ-+-* : m ^ (n + p) ≡ m ^ n * m ^ p + i^j≡0⇒i≡0 : i ^ j ≡ 0 → i ≡ 0 + i^j≡1⇒j≡0∨i≡1 : i ^ j ≡ 1 → j ≡ 0 ⊎ i ≡ 1 + + ⊔-assoc : Associative _⊔_ + ⊔-comm : Commutative _⊔_ + ⊔-idem : Idempotent _⊔_ + ⊔-identityˡ : LeftIdentity 0 _⊔_ + ⊔-identityʳ : RightIdentity 0 _⊔_ + ⊔-identity : Identity 0 _⊔_ + ⊓-assoc : Associative _⊓_ + ⊓-comm : Commutative _⊓_ + ⊓-idem : Idempotent _⊓_ + ⊓-zeroˡ : LeftZero 0 _⊓_ + ⊓-zeroʳ : RightZero 0 _⊓_ + ⊓-zero : Zero 0 _⊓_ + ⊓-distribʳ-⊔ : _⊓_ DistributesOverʳ _⊔_ + ⊓-distribˡ-⊔ : _⊓_ DistributesOverˡ _⊔_ + ⊔-abs-⊓ : _⊔_ Absorbs _⊓_ + ⊓-abs-⊔ : _⊓_ Absorbs _⊔_ + m⊓n≤n : m ⊓ n ≤ n + m≤m⊔n : m ≤ m ⊔ n + m⊔n≤m+n : m ⊔ n ≤ m + n + m⊓n≤m+n : m ⊓ n ≤ m + n + m⊓n≤m⊔n : m ⊔ n ≤ m ⊔ n + ⊔-mono-≤ : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ + ⊔-mono-< : _⊔_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_ + ⊓-mono-≤ : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ + ⊓-mono-< : _⊓_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_ + +-distribˡ-⊔ : _+_ DistributesOverˡ _⊔_ + +-distribʳ-⊔ : _+_ DistributesOverʳ _⊔_ + +-distrib-⊔ : _+_ DistributesOver _⊔_ + +-distribˡ-⊓ : _+_ DistributesOverˡ _⊓_ + +-distribʳ-⊓ : _+_ DistributesOverʳ _⊓_ + +-distrib-⊓ : _+_ DistributesOver _⊓_ + ⊔-isSemigroup : IsSemigroup _≡_ _⊔_ + ⊓-isSemigroup : IsSemigroup _≡_ _⊓_ + ⊓-⊔-isLattice : IsLattice _≡_ _⊓_ _⊔_ + + ∸-distribʳ-⊔ : _∸_ DistributesOverʳ _⊔_ + ∸-distribʳ-⊓ : _∸_ DistributesOverʳ _⊓_ + +-∸-comm : o ≤ m → (m + n) ∸ o ≡ (m ∸ o) + n + ``` + +* Added decidability relation to `Data.Nat.GCD` + ```agda + gcd? : (m n d : ℕ) → Dec (GCD m n d) + ``` + +* Added "not-divisible-by" relation to `Data.Nat.Divisibility` + ```agda + m ∤ n = ¬ (m ∣ n) + ``` + +* Added proofs to `Data.Nat.Divisibility` + ```agda + ∣-reflexive : _≡_ ⇒ _∣_ + ∣-refl : Reflexive _∣_ + ∣-trans : Transitive _∣_ + ∣-antisym : Antisymmetric _≡_ _∣_ + ∣-isPreorder : IsPreorder _≡_ _∣_ + ∣-isPartialOrder : IsPartialOrder _≡_ _∣_ + + n∣n : n ∣ n + ∣m∸n∣n⇒∣m : n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m + ``` + +* Added proofs to `Data.Nat.GeneralisedArithmetic`: + ```agda + fold-+ : fold z s (m + n) ≡ fold (fold z s n) s m + fold-k : fold k (s ∘′_) m z ≡ fold (k z) s m + fold-* : fold z s (m * n) ≡ fold z (fold id (s ∘_) n) m + fold-pull : fold p s m ≡ g (fold z s m) p + + id-is-fold : fold zero suc m ≡ m + +-is-fold : fold n suc m ≡ m + n + *-is-fold : fold zero (n +_) m ≡ m * n + ^-is-fold : fold 1 (m *_) n ≡ m ^ n + *+-is-fold : fold p (n +_) m ≡ m * n + p + ^*-is-fold : fold p (m *_) n ≡ m ^ n * p + ``` + +* Added syntax for existential quantifiers in `Data.Product`: + ```agda + ∃-syntax (λ x → B) = ∃[ x ] B + ∄-syntax (λ x → B) = ∄[ x ] B + ``` + +* A new module `Data.Rational.Properties` has been added, containing proofs: + ```agda + ≤-reflexive : _≡_ ⇒ _≤_ + ≤-refl : Reflexive _≤_ + ≤-trans : Transitive _≤_ + ≤-antisym : Antisymmetric _≡_ _≤_ + ≤-total : Total _≤_ + + ≤-isPreorder : IsPreorder _≡_ _≤_ + ≤-isPartialOrder : IsPartialOrder _≡_ _≤_ + ≤-isTotalOrder : IsTotalOrder _≡_ _≤_ + ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_ + ``` + +* Added proofs to `Data.Sign.Properties`: + ```agda + opposite-cong : opposite s ≡ opposite t → s ≡ t + + *-identityˡ : LeftIdentity + _*_ + *-identityʳ : RightIdentity + _*_ + *-identity : Identity + _*_ + *-comm : Commutative _*_ + *-assoc : Associative _*_ + cancel-*-left : LeftCancellative _*_ + *-cancellative : Cancellative _*_ + s*s≡+ : s * s ≡ + + ``` + +* Added definitions to `Data.Sum`: + ```agda + From-inj₁ : ∀ {a b} {A : Set a} {B : Set b} → A ⊎ B → Set a + from-inj₁ : ∀ {a b} {A : Set a} {B : Set b} (x : A ⊎ B) → From-inj₁ x + From-inj₂ : ∀ {a b} {A : Set a} {B : Set b} → A ⊎ B → Set b + from-inj₂ : ∀ {a b} {A : Set a} {B : Set b} (x : A ⊎ B) → From-inj₂ x + ``` + +* Added a functor encapsulating `map` in `Data.Vec`: + ```agda + functor = record { _<$>_ = map} + ``` + +* Added proofs to `Data.Vec.Equality` + ```agda + to-≅ : xs ≈ ys → xs ≅ ys + xs++[]≈xs : xs ++ [] ≈ xs + xs++[]≅xs : xs ++ [] ≅ xs + ``` + +* Added proofs to `Data.Vec.Properties` + ```agda + lookup-map : lookup i (map f xs) ≡ f (lookup i xs) + lookup-functor-morphism : Morphism functor IdentityFunctor + map-replicate : map f (replicate x) ≡ replicate (f x) + + ⊛-is-zipWith : fs ⊛ xs ≡ zipWith _$_ fs xs + map-is-⊛ : map f xs ≡ replicate f ⊛ xs + zipWith-is-⊛ : zipWith f xs ys ≡ replicate f ⊛ xs ⊛ ys + + zipWith-replicate₁ : zipWith _⊕_ (replicate x) ys ≡ map (x ⊕_) ys + zipWith-replicate₂ : zipWith _⊕_ xs (replicate y) ≡ map (_⊕ y) xs + zipWith-map₁ : zipWith _⊕_ (map f xs) ys ≡ zipWith (λ x y → f x ⊕ y) xs ys + zipWith-map₂ : zipWith _⊕_ xs (map f ys) ≡ zipWith (λ x y → x ⊕ f y) xs ys + ``` + +* Added proofs to `Data.Vec.All.Properties` + ```agda + All-++⁺ : All P xs → All P ys → All P (xs ++ ys) + All-++ˡ⁻ : All P (xs ++ ys) → All P xs + All-++ʳ⁻ : All P (xs ++ ys) → All P ys + All-++⁻ : All P (xs ++ ys) → All P xs × All P ys + + All₂-++⁺ : All₂ _~_ ws xs → All₂ _~_ ys zs → All₂ _~_ (ws ++ ys) (xs ++ zs) + All₂-++ˡ⁻ : All₂ _~_ (ws ++ ys) (xs ++ zs) → All₂ _~_ ws xs + All₂-++ʳ⁻ : All₂ _~_ (ws ++ ys) (xs ++ zs) → All₂ _~_ ys zs + All₂-++⁻ : All₂ _~_ (ws ++ ys) (xs ++ zs) → All₂ _~_ ws xs × All₂ _~_ ys zs + + All-concat⁺ : All (All P) xss → All P (concat xss) + All-concat⁻ : All P (concat xss) → All (All P) xss + + All₂-concat⁺ : All₂ (All₂ _~_) xss yss → All₂ _~_ (concat xss) (concat yss) + All₂-concat⁻ : All₂ _~_ (concat xss) (concat yss) → All₂ (All₂ _~_) xss yss + ``` + +* Added non-dependant versions of the application combinators in `Function` for use + cases where the most general one leads to unsolved meta variables: + ```agda + _$′_ : (A → B) → (A → B) + _$!′_ : (A → B) → (A → B) + ``` + +* Added proofs to `Relation.Binary.Consequences` + ```agda + P-resp⟶¬P-resp : Symmetric _≈_ → P Respects _≈_ → (¬_ ∘ P) Respects _≈_ + ``` + +* Added conversion lemmas to `Relation.Binary.HeterogeneousEquality` + ```agda + ≅-to-type-≡ : {x : A} {y : B} → x ≅ y → A ≡ B + ≅-to-subst-≡ : (p : x ≅ y) → subst (λ x → x) (≅-to-type-≡ p) x ≡ y + ``` |