From b888b5e57a3fb8853e2390027b1193aa9612c6af Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 7 Feb 2025 14:19:01 +0000 Subject: [PATCH 1/3] =?UTF-8?q?[=20refactor=20]=20*-distrib=CB=A1-?= =?UTF-8?q?=E2=88=A3-=E2=88=A3=20using=20wlog?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Properties.agda | 26 ++++++++------------------ 1 file changed, 8 insertions(+), 18 deletions(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index e2d667f3e9..60c4d5adc0 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -17,7 +17,7 @@ open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup; open import Algebra.Definitions.RawMagma using (_,_) open import Algebra.Morphism open import Algebra.Consequences.Propositional - using (comm∧cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ) + using (comm∧cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ; comm⇒sym[distribˡ]) open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator) import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp @@ -39,7 +39,7 @@ open import Relation.Unary as U using (Pred) open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary -open import Relation.Binary.Consequences using (flip-Connex) +open import Relation.Binary.Consequences using (flip-Connex; wlog) open import Relation.Binary.PropositionalEquality open import Relation.Nullary hiding (Irrelevant) open import Relation.Nullary.Decidable using (True; via-injection; map′; recompute) @@ -1845,23 +1845,13 @@ m∸n≤∣m-n∣ m n with ≤-total m n ∣ n - m ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m m≤n ⟩ n ∸ m ∎ -private - - *-distribˡ-∣-∣-aux : ∀ a m n → m ≤ n → a * ∣ n - m ∣ ≡ ∣ a * n - a * m ∣ - *-distribˡ-∣-∣-aux a m n m≤n = begin-equality - a * ∣ n - m ∣ ≡⟨ cong (a *_) (m≤n⇒∣n-m∣≡n∸m m≤n) ⟩ - a * (n ∸ m) ≡⟨ *-distribˡ-∸ a n m ⟩ - a * n ∸ a * m ≡⟨ sym $′ m≤n⇒∣n-m∣≡n∸m (*-monoʳ-≤ a m≤n) ⟩ - ∣ a * n - a * m ∣ ∎ - *-distribˡ-∣-∣ : _*_ DistributesOverˡ ∣_-_∣ -*-distribˡ-∣-∣ a m n with ≤-total m n -... | inj₂ n≤m = *-distribˡ-∣-∣-aux a n m n≤m -... | inj₁ m≤n = begin-equality - a * ∣ m - n ∣ ≡⟨ cong (a *_) (∣-∣-comm m n) ⟩ - a * ∣ n - m ∣ ≡⟨ *-distribˡ-∣-∣-aux a m n m≤n ⟩ - ∣ a * n - a * m ∣ ≡⟨ ∣-∣-comm (a * n) (a * m) ⟩ - ∣ a * m - a * n ∣ ∎ +*-distribˡ-∣-∣ a = wlog ≤-total (comm⇒sym[distribˡ] {_◦_ = _*_} ∣-∣-comm a) + $′ λ m n m≤n → begin-equality + a * ∣ m - n ∣ ≡⟨ cong (a *_) (m≤n⇒∣m-n∣≡n∸m m≤n) ⟩ + a * (n ∸ m) ≡⟨ *-distribˡ-∸ a n m ⟩ + a * n ∸ a * m ≡⟨ m≤n⇒∣m-n∣≡n∸m (*-monoʳ-≤ a m≤n) ⟨ + ∣ a * m - a * n ∣ ∎ *-distribʳ-∣-∣ : _*_ DistributesOverʳ ∣_-_∣ *-distribʳ-∣-∣ = comm∧distrˡ⇒distrʳ *-comm *-distribˡ-∣-∣ From c21d6147e65df1614d1f66c6b079ec0d504218ad Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 7 Feb 2025 15:46:09 +0000 Subject: [PATCH 2/3] [ admin ] reorganising proofs Preparing for a wlog result --- src/Data/Integer/Properties.agda | 284 ++++++++++++++++--------------- 1 file changed, 145 insertions(+), 139 deletions(-) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index f89d3164f6..d3bbd8b0cf 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -25,17 +25,18 @@ open import Data.Product.Base using (proj₁; proj₂; _,_; _×_) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′) open import Data.Sign.Base as Sign using (Sign) import Data.Sign.Properties as Sign -open import Function.Base using (_∘_; _$_; id) +open import Function.Base using (_∘_; _$_; _$′_; id) open import Level using (0ℓ) open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder) +open import Relation.Binary.Consequences using (wlog) open import Relation.Binary.Structures using (IsPreorder; IsTotalPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder) open import Relation.Binary.Definitions using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri<; tri>) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; cong; cong₂; sym; _≢_; subst; resp₂; trans) + using (_≡_; refl; cong; cong₂; sym; _≢_; subst; subst₂; resp₂; trans) open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning; setoid; decSetoid; isEquivalence) open import Relation.Nullary.Decidable.Core using (yes; no) @@ -45,6 +46,7 @@ import Relation.Nullary.Decidable as Dec open import Algebra.Definitions {A = ℤ} _≡_ open import Algebra.Consequences.Propositional + using (comm∧idˡ⇒idʳ; comm∧invˡ⇒invʳ; comm∧zeˡ⇒zeʳ; comm∧distrʳ⇒distrˡ) open import Algebra.Structures {A = ℤ} _≡_ module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_ module ℕtoℤ = Morphism.Definitions ℕ ℤ _≡_ @@ -446,7 +448,7 @@ neg-cancel-< { -[1+ m ]} { +0} (+<+ ()) neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ m suc o ⊖ n ≡⟨ [1+m]⊖[1+n]≡m⊖n (suc o) n ⟨ suc (suc o) ⊖ suc n ∎ where open ≤-Reasoning +------------------------------------------------------------------------ +-- Properties of ∣_∣ +------------------------------------------------------------------------ + +0≤i⇒+∣i∣≡i : 0ℤ ≤ i → + ∣ i ∣ ≡ i +0≤i⇒+∣i∣≡i (+≤+ _) = refl + ++∣i∣≡i⇒0≤i : + ∣ i ∣ ≡ i → 0ℤ ≤ i ++∣i∣≡i⇒0≤i {+ n} _ = +≤+ z≤n + ++∣i∣≡i⊎+∣i∣≡-i : ∀ i → + ∣ i ∣ ≡ i ⊎ + ∣ i ∣ ≡ - i ++∣i∣≡i⊎+∣i∣≡-i (+ n) = inj₁ refl ++∣i∣≡i⊎+∣i∣≡-i (-[1+ n ]) = inj₂ refl + +∣m⊝n∣≤m⊔n : ∀ m n → ∣ m ⊖ n ∣ ℕ.≤ m ℕ.⊔ n +∣m⊝n∣≤m⊔n m n with m ℕ.<ᵇ n +... | true = begin + ∣ - + (n ℕ.∸ m) ∣ ≡⟨ ∣-i∣≡∣i∣ (+ (n ℕ.∸ m)) ⟩ + ∣ + (n ℕ.∸ m) ∣ ≡⟨⟩ + n ℕ.∸ m ≤⟨ ℕ.m∸n≤m n m ⟩ + n ≤⟨ ℕ.m≤n⊔m m n ⟩ + m ℕ.⊔ n ∎ + where open ℕ.≤-Reasoning +... | false = begin + ∣ + (m ℕ.∸ n) ∣ ≡⟨⟩ + m ℕ.∸ n ≤⟨ ℕ.m∸n≤m m n ⟩ + m ≤⟨ ℕ.m≤m⊔n m n ⟩ + m ℕ.⊔ n ∎ + where open ℕ.≤-Reasoning + +∣i+j∣≤∣i∣+∣j∣ : ∀ i j → ∣ i + j ∣ ℕ.≤ ∣ i ∣ ℕ.+ ∣ j ∣ +∣i+j∣≤∣i∣+∣j∣ +[1+ m ] (+ n) = ℕ.≤-refl +∣i+j∣≤∣i∣+∣j∣ +0 (+ n) = ℕ.≤-refl +∣i+j∣≤∣i∣+∣j∣ +0 -[1+ n ] = ℕ.≤-refl +∣i+j∣≤∣i∣+∣j∣ -[1+ m ] -[1+ n ] rewrite ℕ.+-suc (suc m) n = ℕ.≤-refl +∣i+j∣≤∣i∣+∣j∣ +[1+ m ] -[1+ n ] = begin + ∣ suc m ⊖ suc n ∣ ≤⟨ ∣m⊝n∣≤m⊔n (suc m) (suc n) ⟩ + suc m ℕ.⊔ suc n ≤⟨ ℕ.m⊔n≤m+n (suc m) (suc n) ⟩ + suc m ℕ.+ suc n ∎ + where open ℕ.≤-Reasoning +∣i+j∣≤∣i∣+∣j∣ -[1+ m ] (+ n) = begin + ∣ n ⊖ suc m ∣ ≤⟨ ∣m⊝n∣≤m⊔n n (suc m) ⟩ + n ℕ.⊔ suc m ≤⟨ ℕ.m⊔n≤m+n n (suc m) ⟩ + n ℕ.+ suc m ≡⟨ ℕ.+-comm n (suc m) ⟩ + suc m ℕ.+ n ∎ + where open ℕ.≤-Reasoning + +∣i-j∣≤∣i∣+∣j∣ : ∀ i j → ∣ i - j ∣ ℕ.≤ ∣ i ∣ ℕ.+ ∣ j ∣ +∣i-j∣≤∣i∣+∣j∣ i j = begin + ∣ i - j ∣ ≤⟨ ∣i+j∣≤∣i∣+∣j∣ i (- j) ⟩ + ∣ i ∣ ℕ.+ ∣ - j ∣ ≡⟨ cong (∣ i ∣ ℕ.+_) (∣-i∣≡∣i∣ j) ⟩ + ∣ i ∣ ℕ.+ ∣ j ∣ ∎ + where open ℕ.≤-Reasoning + +------------------------------------------------------------------------ +-- Properties of sign and _◃_ + +◃-nonZero : ∀ s n .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n) +◃-nonZero Sign.- (ℕ.suc _) = _ +◃-nonZero Sign.+ (ℕ.suc _) = _ + +◃-inverse : ∀ i → sign i ◃ ∣ i ∣ ≡ i +◃-inverse -[1+ n ] = refl +◃-inverse +0 = refl +◃-inverse +[1+ n ] = refl + +◃-cong : sign i ≡ sign j → ∣ i ∣ ≡ ∣ j ∣ → i ≡ j +◃-cong {+ m} {+ n } ≡-sign refl = refl +◃-cong { -[1+ m ]} { -[1+ n ]} ≡-sign refl = refl + ++◃n≡+n : ∀ n → Sign.+ ◃ n ≡ + n ++◃n≡+n zero = refl ++◃n≡+n (suc _) = refl + +-◃n≡-n : ∀ n → Sign.- ◃ n ≡ - + n +-◃n≡-n zero = refl +-◃n≡-n (suc _) = refl + +sign-◃ : ∀ s n .{{_ : ℕ.NonZero n}} → sign (s ◃ n) ≡ s +sign-◃ Sign.- (suc _) = refl +sign-◃ Sign.+ (suc _) = refl + +abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n +abs-◃ _ zero = refl +abs-◃ Sign.- (suc n) = refl +abs-◃ Sign.+ (suc n) = refl + +signᵢ◃∣i∣≡i : ∀ i → sign i ◃ ∣ i ∣ ≡ i +signᵢ◃∣i∣≡i (+ n) = +◃n≡+n n +signᵢ◃∣i∣≡i -[1+ n ] = refl + +sign-cong : .{{_ : ℕ.NonZero m}} .{{_ : ℕ.NonZero n}} → + s ◃ m ≡ t ◃ n → s ≡ t +sign-cong {n@(suc _)} {m@(suc _)} {s} {t} eq = begin + s ≡⟨ sign-◃ s n ⟨ + sign (s ◃ n) ≡⟨ cong sign eq ⟩ + sign (t ◃ m) ≡⟨ sign-◃ t m ⟩ + t ∎ where open ≡-Reasoning + +sign-cong′ : s ◃ m ≡ t ◃ n → s ≡ t ⊎ (m ≡ 0 × n ≡ 0) +sign-cong′ {s} {zero} {t} {zero} eq = inj₂ (refl , refl) +sign-cong′ {s} {zero} {Sign.- } {suc n} () +sign-cong′ {s} {zero} {Sign.+ } {suc n} () +sign-cong′ {Sign.- } {suc m} {t} {zero} () +sign-cong′ {Sign.+ } {suc m} {t} {zero} () +sign-cong′ {s} {suc m} {t} {suc n} eq = inj₁ (sign-cong eq) + +abs-cong : s ◃ m ≡ t ◃ n → m ≡ n +abs-cong {s} {m} {t} {n} eq = begin + m ≡⟨ abs-◃ s m ⟨ + ∣ s ◃ m ∣ ≡⟨ cong ∣_∣ eq ⟩ + ∣ t ◃ n ∣ ≡⟨ abs-◃ t n ⟩ + n ∎ where open ≡-Reasoning + +∣s◃m∣*∣t◃n∣≡m*n : ∀ s t m n → ∣ s ◃ m ∣ ℕ.* ∣ t ◃ n ∣ ≡ m ℕ.* n +∣s◃m∣*∣t◃n∣≡m*n s t m n = cong₂ ℕ._*_ (abs-◃ s m) (abs-◃ t n) + ++◃-mono-< : m ℕ.< n → Sign.+ ◃ m < Sign.+ ◃ n ++◃-mono-< {zero} {suc n} m Date: Fri, 7 Feb 2025 15:46:43 +0000 Subject: [PATCH 3/3] =?UTF-8?q?[=20refactor=20]=20wlog=20for=20=E2=88=A3m?= =?UTF-8?q?=E2=8A=9Dn=E2=88=A3=E2=89=A4m=E2=8A=94n?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Integer/Properties.agda | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index d3bbd8b0cf..e136719f4a 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -679,19 +679,15 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> +∣i∣≡i⊎+∣i∣≡-i (-[1+ n ]) = inj₂ refl ∣m⊝n∣≤m⊔n : ∀ m n → ∣ m ⊖ n ∣ ℕ.≤ m ℕ.⊔ n -∣m⊝n∣≤m⊔n m n with m ℕ.<ᵇ n -... | true = begin - ∣ - + (n ℕ.∸ m) ∣ ≡⟨ ∣-i∣≡∣i∣ (+ (n ℕ.∸ m)) ⟩ - ∣ + (n ℕ.∸ m) ∣ ≡⟨⟩ - n ℕ.∸ m ≤⟨ ℕ.m∸n≤m n m ⟩ - n ≤⟨ ℕ.m≤n⊔m m n ⟩ - m ℕ.⊔ n ∎ - where open ℕ.≤-Reasoning -... | false = begin - ∣ + (m ℕ.∸ n) ∣ ≡⟨⟩ - m ℕ.∸ n ≤⟨ ℕ.m∸n≤m m n ⟩ - m ≤⟨ ℕ.m≤m⊔n m n ⟩ - m ℕ.⊔ n ∎ +∣m⊝n∣≤m⊔n = wlog ℕ.≤-total + (λ {m n} → subst₂ ℕ._≤_ (∣m⊖n∣≡∣n⊖m∣ m n) (ℕ.⊔-comm m n)) + $′ λ m n m≤n → begin + ∣ m ⊖ n ∣ ≡⟨ cong ∣_∣ (⊖-≤ m≤n) ⟩ + ∣ - + (n ℕ.∸ m) ∣ ≡⟨ ∣-i∣≡∣i∣ (+ (n ℕ.∸ m)) ⟩ + ∣ + (n ℕ.∸ m) ∣ ≡⟨⟩ + n ℕ.∸ m ≤⟨ ℕ.m∸n≤m n m ⟩ + n ≤⟨ ℕ.m≤n⊔m m n ⟩ + m ℕ.⊔ n ∎ where open ℕ.≤-Reasoning ∣i+j∣≤∣i∣+∣j∣ : ∀ i j → ∣ i + j ∣ ℕ.≤ ∣ i ∣ ℕ.+ ∣ j ∣