Skip to content

Commit c562cd8

Browse files
gallaisgallais
authored
[ re agda#523 ] Refactorings using wlog (agda#2577)
* [ refactor ] *-distribˡ-∣-∣ using wlog * [ admin ] reorganising proofs Preparing for a wlog result * [ refactor ] wlog for ∣m⊝n∣≤m⊔n
1 parent 94906c0 commit c562cd8

File tree

2 files changed

+149
-157
lines changed

2 files changed

+149
-157
lines changed

‎src/Data/Integer/Properties.agda

+141-139
Original file line numberDiff line numberDiff line change
@@ -25,17 +25,18 @@ open import Data.Product.Base using (proj₁; proj₂; _,_; _×_)
2525
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
2626
open import Data.Sign.Base as Sign using (Sign)
2727
import Data.Sign.Properties as Sign
28-
open import Function.Base using (_∘_; _$_; id)
28+
open import Function.Base using (_∘_; _$_; _$′_; id)
2929
open import Level using (0ℓ)
3030
open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
3131
open import Relation.Binary.Bundles using
3232
(Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
33+
open import Relation.Binary.Consequences using (wlog)
3334
open import Relation.Binary.Structures
3435
using (IsPreorder; IsTotalPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
3536
open import Relation.Binary.Definitions
3637
using (DecidableEquality; Reflexive; Transitive; Antisymmetric; Total; Decidable; Irrelevant; Irreflexive; Asymmetric; LeftTrans; RightTrans; Trichotomous; tri≈; tri<; tri>)
3738
open import Relation.Binary.PropositionalEquality.Core
38-
using (_≡_; refl; cong; cong₂; sym; _≢_; subst; resp₂; trans)
39+
using (_≡_; refl; cong; cong₂; sym; _≢_; subst; subst₂; resp₂; trans)
3940
open import Relation.Binary.PropositionalEquality.Properties
4041
using (module ≡-Reasoning; setoid; decSetoid; isEquivalence)
4142
open import Relation.Nullary.Decidable.Core using (yes; no)
@@ -45,6 +46,7 @@ import Relation.Nullary.Decidable as Dec
4546

4647
open import Algebra.Definitions {A = ℤ} _≡_
4748
open import Algebra.Consequences.Propositional
49+
using (comm∧idˡ⇒idʳ; comm∧invˡ⇒invʳ; comm∧zeˡ⇒zeʳ; comm∧distrʳ⇒distrˡ)
4850
open import Algebra.Structures {A = ℤ} _≡_
4951
module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_
5052
module ℕtoℤ = Morphism.Definitions ℕ ℤ _≡_
@@ -446,7 +448,7 @@ neg-cancel-< { -[1+ m ]} { +0} (+<+ ())
446448
neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ m<n) = -<- (s<s⁻¹ m<n)
447449

448450
------------------------------------------------------------------------
449-
-- Properties of ∣_∣
451+
-- Basic properties of ∣_∣
450452
------------------------------------------------------------------------
451453

452454
∣i∣≡0⇒i≡0 : ∣ i ∣ ≡ 0 → i ≡ + 0
@@ -457,142 +459,6 @@ neg-cancel-< { -[1+ m ]} { -[1+ n ]} (+<+ m<n) = -<- (s<s⁻¹ m<n)
457459
∣-i∣≡∣i∣ +0 = refl
458460
∣-i∣≡∣i∣ +[1+ n ] = refl
459461

460-
0≤i⇒+∣i∣≡i : 0ℤ ≤ i → + ∣ i ∣ ≡ i
461-
0≤i⇒+∣i∣≡i (+≤+ _) = refl
462-
463-
+∣i∣≡i⇒0≤i : + ∣ i ∣ ≡ i → 0ℤ ≤ i
464-
+∣i∣≡i⇒0≤i {+ n} _ = +≤+ z≤n
465-
466-
+∣i∣≡i⊎+∣i∣≡-i : ∀ i → + ∣ i ∣ ≡ i ⊎ + ∣ i ∣ ≡ - i
467-
+∣i∣≡i⊎+∣i∣≡-i (+ n) = inj₁ refl
468-
+∣i∣≡i⊎+∣i∣≡-i (-[1+ n ]) = inj₂ refl
469-
470-
∣m⊝n∣≤m⊔n : ∀ m n → ∣ m ⊖ n ∣ ℕ.≤ m ℕ.⊔ n
471-
∣m⊝n∣≤m⊔n m n with m ℕ.<ᵇ n
472-
... | true = begin
473-
∣ - + (n ℕ.∸ m) ∣ ≡⟨ ∣-i∣≡∣i∣ (+ (n ℕ.∸ m)) ⟩
474-
∣ + (n ℕ.∸ m) ∣ ≡⟨⟩
475-
n ℕ.∸ m ≤⟨ ℕ.m∸n≤m n m ⟩
476-
n ≤⟨ ℕ.m≤n⊔m m n ⟩
477-
m ℕ.⊔ n ∎
478-
where open ℕ.≤-Reasoning
479-
... | false = begin
480-
∣ + (m ℕ.∸ n) ∣ ≡⟨⟩
481-
m ℕ.∸ n ≤⟨ ℕ.m∸n≤m m n ⟩
482-
m ≤⟨ ℕ.m≤m⊔n m n ⟩
483-
m ℕ.⊔ n ∎
484-
where open ℕ.≤-Reasoning
485-
486-
∣i+j∣≤∣i∣+∣j∣ : ∀ i j → ∣ i + j ∣ ℕ.≤ ∣ i ∣ ℕ.+ ∣ j ∣
487-
∣i+j∣≤∣i∣+∣j∣ +[1+ m ] (+ n) = ℕ.≤-refl
488-
∣i+j∣≤∣i∣+∣j∣ +0 (+ n) = ℕ.≤-refl
489-
∣i+j∣≤∣i∣+∣j∣ +0 -[1+ n ] = ℕ.≤-refl
490-
∣i+j∣≤∣i∣+∣j∣ -[1+ m ] -[1+ n ] rewrite ℕ.+-suc (suc m) n = ℕ.≤-refl
491-
∣i+j∣≤∣i∣+∣j∣ +[1+ m ] -[1+ n ] = begin
492-
∣ suc m ⊖ suc n ∣ ≤⟨ ∣m⊝n∣≤m⊔n (suc m) (suc n) ⟩
493-
suc m ℕ.⊔ suc n ≤⟨ ℕ.m⊔n≤m+n (suc m) (suc n) ⟩
494-
suc m ℕ.+ suc n ∎
495-
where open ℕ.≤-Reasoning
496-
∣i+j∣≤∣i∣+∣j∣ -[1+ m ] (+ n) = begin
497-
∣ n ⊖ suc m ∣ ≤⟨ ∣m⊝n∣≤m⊔n n (suc m) ⟩
498-
n ℕ.⊔ suc m ≤⟨ ℕ.m⊔n≤m+n n (suc m) ⟩
499-
n ℕ.+ suc m ≡⟨ ℕ.+-comm n (suc m) ⟩
500-
suc m ℕ.+ n ∎
501-
where open ℕ.≤-Reasoning
502-
503-
∣i-j∣≤∣i∣+∣j∣ : ∀ i j → ∣ i - j ∣ ℕ.≤ ∣ i ∣ ℕ.+ ∣ j ∣
504-
∣i-j∣≤∣i∣+∣j∣ i j = begin
505-
∣ i - j ∣ ≤⟨ ∣i+j∣≤∣i∣+∣j∣ i (- j) ⟩
506-
∣ i ∣ ℕ.+ ∣ - j ∣ ≡⟨ cong (∣ i ∣ ℕ.+_) (∣-i∣≡∣i∣ j) ⟩
507-
∣ i ∣ ℕ.+ ∣ j ∣ ∎
508-
where open ℕ.≤-Reasoning
509-
510-
------------------------------------------------------------------------
511-
-- Properties of sign and _◃_
512-
513-
◃-nonZero : ∀ s n .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
514-
◃-nonZero Sign.- (ℕ.suc _) = _
515-
◃-nonZero Sign.+ (ℕ.suc _) = _
516-
517-
◃-inverse : ∀ i → sign i ◃ ∣ i ∣ ≡ i
518-
◃-inverse -[1+ n ] = refl
519-
◃-inverse +0 = refl
520-
◃-inverse +[1+ n ] = refl
521-
522-
◃-cong : sign i ≡ sign j → ∣ i ∣ ≡ ∣ j ∣ → i ≡ j
523-
◃-cong {+ m} {+ n } ≡-sign refl = refl
524-
◃-cong { -[1+ m ]} { -[1+ n ]} ≡-sign refl = refl
525-
526-
+◃n≡+n : ∀ n → Sign.+ ◃ n ≡ + n
527-
+◃n≡+n zero = refl
528-
+◃n≡+n (suc _) = refl
529-
530-
-◃n≡-n : ∀ n → Sign.- ◃ n ≡ - + n
531-
-◃n≡-n zero = refl
532-
-◃n≡-n (suc _) = refl
533-
534-
sign-◃ : ∀ s n .{{_ : ℕ.NonZero n}} → sign (s ◃ n) ≡ s
535-
sign-◃ Sign.- (suc _) = refl
536-
sign-◃ Sign.+ (suc _) = refl
537-
538-
abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n
539-
abs-◃ _ zero = refl
540-
abs-◃ Sign.- (suc n) = refl
541-
abs-◃ Sign.+ (suc n) = refl
542-
543-
signᵢ◃∣i∣≡i : ∀ i → sign i ◃ ∣ i ∣ ≡ i
544-
signᵢ◃∣i∣≡i (+ n) = +◃n≡+n n
545-
signᵢ◃∣i∣≡i -[1+ n ] = refl
546-
547-
sign-cong : .{{_ : ℕ.NonZero m}} .{{_ : ℕ.NonZero n}} →
548-
s ◃ m ≡ t ◃ n → s ≡ t
549-
sign-cong {n@(suc _)} {m@(suc _)} {s} {t} eq = begin
550-
s ≡⟨ sign-◃ s n ⟨
551-
sign (s ◃ n) ≡⟨ cong sign eq ⟩
552-
sign (t ◃ m) ≡⟨ sign-◃ t m ⟩
553-
t ∎ where open ≡-Reasoning
554-
555-
sign-cong′ : s ◃ m ≡ t ◃ n → s ≡ t ⊎ (m ≡ 0 × n ≡ 0)
556-
sign-cong′ {s} {zero} {t} {zero} eq = inj₂ (refl , refl)
557-
sign-cong′ {s} {zero} {Sign.- } {suc n} ()
558-
sign-cong′ {s} {zero} {Sign.+ } {suc n} ()
559-
sign-cong′ {Sign.- } {suc m} {t} {zero} ()
560-
sign-cong′ {Sign.+ } {suc m} {t} {zero} ()
561-
sign-cong′ {s} {suc m} {t} {suc n} eq = inj₁ (sign-cong eq)
562-
563-
abs-cong : s ◃ m ≡ t ◃ n → m ≡ n
564-
abs-cong {s} {m} {t} {n} eq = begin
565-
m ≡⟨ abs-◃ s m ⟨
566-
∣ s ◃ m ∣ ≡⟨ cong ∣_∣ eq ⟩
567-
∣ t ◃ n ∣ ≡⟨ abs-◃ t n ⟩
568-
n ∎ where open ≡-Reasoning
569-
570-
∣s◃m∣*∣t◃n∣≡m*n : ∀ s t m n → ∣ s ◃ m ∣ ℕ.* ∣ t ◃ n ∣ ≡ m ℕ.* n
571-
∣s◃m∣*∣t◃n∣≡m*n s t m n = cong₂ ℕ._*_ (abs-◃ s m) (abs-◃ t n)
572-
573-
+◃-mono-< : m ℕ.< n → Sign.+ ◃ m < Sign.+ ◃ n
574-
+◃-mono-< {zero} {suc n} m<n = +<+ m<n
575-
+◃-mono-< {suc m} {suc n} m<n = +<+ m<n
576-
577-
+◃-cancel-< : Sign.+ ◃ m < Sign.+ ◃ n → m ℕ.< n
578-
+◃-cancel-< {zero} {zero} (+<+ ())
579-
+◃-cancel-< {suc m} {zero} (+<+ ())
580-
+◃-cancel-< {zero} {suc n} (+<+ m<n) = m<n
581-
+◃-cancel-< {suc m} {suc n} (+<+ m<n) = m<n
582-
583-
neg◃-cancel-< : Sign.- ◃ m < Sign.- ◃ n → n ℕ.< m
584-
neg◃-cancel-< {zero} {zero} (+<+ ())
585-
neg◃-cancel-< {suc m} {zero} -<+ = z<s
586-
neg◃-cancel-< {suc m} {suc n} (-<- n<m) = s<s n<m
587-
588-
-◃<+◃ : ∀ m n .{{_ : ℕ.NonZero m}} → Sign.- ◃ m < Sign.+ ◃ n
589-
-◃<+◃ (suc _) zero = -<+
590-
-◃<+◃ (suc _) (suc _) = -<+
591-
592-
+◃≮-◃ : Sign.+ ◃ m ≮ Sign.- ◃ n
593-
+◃≮-◃ {zero} {zero} (+<+ ())
594-
+◃≮-◃ {suc m} {zero} (+<+ ())
595-
596462
------------------------------------------------------------------------
597463
-- Properties of _⊖_
598464
------------------------------------------------------------------------
@@ -798,6 +664,142 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒>
798664
suc o ⊖ n ≡⟨ [1+m]⊖[1+n]≡m⊖n (suc o) n ⟨
799665
suc (suc o) ⊖ suc n ∎ where open ≤-Reasoning
800666

667+
------------------------------------------------------------------------
668+
-- Properties of ∣_∣
669+
------------------------------------------------------------------------
670+
671+
0≤i⇒+∣i∣≡i : 0ℤ ≤ i → + ∣ i ∣ ≡ i
672+
0≤i⇒+∣i∣≡i (+≤+ _) = refl
673+
674+
+∣i∣≡i⇒0≤i : + ∣ i ∣ ≡ i → 0ℤ ≤ i
675+
+∣i∣≡i⇒0≤i {+ n} _ = +≤+ z≤n
676+
677+
+∣i∣≡i⊎+∣i∣≡-i : ∀ i → + ∣ i ∣ ≡ i ⊎ + ∣ i ∣ ≡ - i
678+
+∣i∣≡i⊎+∣i∣≡-i (+ n) = inj₁ refl
679+
+∣i∣≡i⊎+∣i∣≡-i (-[1+ n ]) = inj₂ refl
680+
681+
∣m⊝n∣≤m⊔n : ∀ m n → ∣ m ⊖ n ∣ ℕ.≤ m ℕ.⊔ n
682+
∣m⊝n∣≤m⊔n = wlog ℕ.≤-total
683+
(λ {m n} → subst₂ ℕ._≤_ (∣m⊖n∣≡∣n⊖m∣ m n) (ℕ.⊔-comm m n))
684+
$′ λ m n m≤n → begin
685+
∣ m ⊖ n ∣ ≡⟨ cong ∣_∣ (⊖-≤ m≤n) ⟩
686+
∣ - + (n ℕ.∸ m) ∣ ≡⟨ ∣-i∣≡∣i∣ (+ (n ℕ.∸ m)) ⟩
687+
∣ + (n ℕ.∸ m) ∣ ≡⟨⟩
688+
n ℕ.∸ m ≤⟨ ℕ.m∸n≤m n m ⟩
689+
n ≤⟨ ℕ.m≤n⊔m m n ⟩
690+
m ℕ.⊔ n ∎
691+
where open ℕ.≤-Reasoning
692+
693+
∣i+j∣≤∣i∣+∣j∣ : ∀ i j → ∣ i + j ∣ ℕ.≤ ∣ i ∣ ℕ.+ ∣ j ∣
694+
∣i+j∣≤∣i∣+∣j∣ +[1+ m ] (+ n) = ℕ.≤-refl
695+
∣i+j∣≤∣i∣+∣j∣ +0 (+ n) = ℕ.≤-refl
696+
∣i+j∣≤∣i∣+∣j∣ +0 -[1+ n ] = ℕ.≤-refl
697+
∣i+j∣≤∣i∣+∣j∣ -[1+ m ] -[1+ n ] rewrite ℕ.+-suc (suc m) n = ℕ.≤-refl
698+
∣i+j∣≤∣i∣+∣j∣ +[1+ m ] -[1+ n ] = begin
699+
∣ suc m ⊖ suc n ∣ ≤⟨ ∣m⊝n∣≤m⊔n (suc m) (suc n) ⟩
700+
suc m ℕ.⊔ suc n ≤⟨ ℕ.m⊔n≤m+n (suc m) (suc n) ⟩
701+
suc m ℕ.+ suc n ∎
702+
where open ℕ.≤-Reasoning
703+
∣i+j∣≤∣i∣+∣j∣ -[1+ m ] (+ n) = begin
704+
∣ n ⊖ suc m ∣ ≤⟨ ∣m⊝n∣≤m⊔n n (suc m) ⟩
705+
n ℕ.⊔ suc m ≤⟨ ℕ.m⊔n≤m+n n (suc m) ⟩
706+
n ℕ.+ suc m ≡⟨ ℕ.+-comm n (suc m) ⟩
707+
suc m ℕ.+ n ∎
708+
where open ℕ.≤-Reasoning
709+
710+
∣i-j∣≤∣i∣+∣j∣ : ∀ i j → ∣ i - j ∣ ℕ.≤ ∣ i ∣ ℕ.+ ∣ j ∣
711+
∣i-j∣≤∣i∣+∣j∣ i j = begin
712+
∣ i - j ∣ ≤⟨ ∣i+j∣≤∣i∣+∣j∣ i (- j) ⟩
713+
∣ i ∣ ℕ.+ ∣ - j ∣ ≡⟨ cong (∣ i ∣ ℕ.+_) (∣-i∣≡∣i∣ j) ⟩
714+
∣ i ∣ ℕ.+ ∣ j ∣ ∎
715+
where open ℕ.≤-Reasoning
716+
717+
------------------------------------------------------------------------
718+
-- Properties of sign and _◃_
719+
720+
◃-nonZero : ∀ s n .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n)
721+
◃-nonZero Sign.- (ℕ.suc _) = _
722+
◃-nonZero Sign.+ (ℕ.suc _) = _
723+
724+
◃-inverse : ∀ i → sign i ◃ ∣ i ∣ ≡ i
725+
◃-inverse -[1+ n ] = refl
726+
◃-inverse +0 = refl
727+
◃-inverse +[1+ n ] = refl
728+
729+
◃-cong : sign i ≡ sign j → ∣ i ∣ ≡ ∣ j ∣ → i ≡ j
730+
◃-cong {+ m} {+ n } ≡-sign refl = refl
731+
◃-cong { -[1+ m ]} { -[1+ n ]} ≡-sign refl = refl
732+
733+
+◃n≡+n : ∀ n → Sign.+ ◃ n ≡ + n
734+
+◃n≡+n zero = refl
735+
+◃n≡+n (suc _) = refl
736+
737+
-◃n≡-n : ∀ n → Sign.- ◃ n ≡ - + n
738+
-◃n≡-n zero = refl
739+
-◃n≡-n (suc _) = refl
740+
741+
sign-◃ : ∀ s n .{{_ : ℕ.NonZero n}} → sign (s ◃ n) ≡ s
742+
sign-◃ Sign.- (suc _) = refl
743+
sign-◃ Sign.+ (suc _) = refl
744+
745+
abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n
746+
abs-◃ _ zero = refl
747+
abs-◃ Sign.- (suc n) = refl
748+
abs-◃ Sign.+ (suc n) = refl
749+
750+
signᵢ◃∣i∣≡i : ∀ i → sign i ◃ ∣ i ∣ ≡ i
751+
signᵢ◃∣i∣≡i (+ n) = +◃n≡+n n
752+
signᵢ◃∣i∣≡i -[1+ n ] = refl
753+
754+
sign-cong : .{{_ : ℕ.NonZero m}} .{{_ : ℕ.NonZero n}} →
755+
s ◃ m ≡ t ◃ n → s ≡ t
756+
sign-cong {n@(suc _)} {m@(suc _)} {s} {t} eq = begin
757+
s ≡⟨ sign-◃ s n ⟨
758+
sign (s ◃ n) ≡⟨ cong sign eq ⟩
759+
sign (t ◃ m) ≡⟨ sign-◃ t m ⟩
760+
t ∎ where open ≡-Reasoning
761+
762+
sign-cong′ : s ◃ m ≡ t ◃ n → s ≡ t ⊎ (m ≡ 0 × n ≡ 0)
763+
sign-cong′ {s} {zero} {t} {zero} eq = inj₂ (refl , refl)
764+
sign-cong′ {s} {zero} {Sign.- } {suc n} ()
765+
sign-cong′ {s} {zero} {Sign.+ } {suc n} ()
766+
sign-cong′ {Sign.- } {suc m} {t} {zero} ()
767+
sign-cong′ {Sign.+ } {suc m} {t} {zero} ()
768+
sign-cong′ {s} {suc m} {t} {suc n} eq = inj₁ (sign-cong eq)
769+
770+
abs-cong : s ◃ m ≡ t ◃ n → m ≡ n
771+
abs-cong {s} {m} {t} {n} eq = begin
772+
m ≡⟨ abs-◃ s m ⟨
773+
∣ s ◃ m ∣ ≡⟨ cong ∣_∣ eq ⟩
774+
∣ t ◃ n ∣ ≡⟨ abs-◃ t n ⟩
775+
n ∎ where open ≡-Reasoning
776+
777+
∣s◃m∣*∣t◃n∣≡m*n : ∀ s t m n → ∣ s ◃ m ∣ ℕ.* ∣ t ◃ n ∣ ≡ m ℕ.* n
778+
∣s◃m∣*∣t◃n∣≡m*n s t m n = cong₂ ℕ._*_ (abs-◃ s m) (abs-◃ t n)
779+
780+
+◃-mono-< : m ℕ.< n → Sign.+ ◃ m < Sign.+ ◃ n
781+
+◃-mono-< {zero} {suc n} m<n = +<+ m<n
782+
+◃-mono-< {suc m} {suc n} m<n = +<+ m<n
783+
784+
+◃-cancel-< : Sign.+ ◃ m < Sign.+ ◃ n → m ℕ.< n
785+
+◃-cancel-< {zero} {zero} (+<+ ())
786+
+◃-cancel-< {suc m} {zero} (+<+ ())
787+
+◃-cancel-< {zero} {suc n} (+<+ m<n) = m<n
788+
+◃-cancel-< {suc m} {suc n} (+<+ m<n) = m<n
789+
790+
neg◃-cancel-< : Sign.- ◃ m < Sign.- ◃ n → n ℕ.< m
791+
neg◃-cancel-< {zero} {zero} (+<+ ())
792+
neg◃-cancel-< {suc m} {zero} -<+ = z<s
793+
neg◃-cancel-< {suc m} {suc n} (-<- n<m) = s<s n<m
794+
795+
-◃<+◃ : ∀ m n .{{_ : ℕ.NonZero m}} → Sign.- ◃ m < Sign.+ ◃ n
796+
-◃<+◃ (suc _) zero = -<+
797+
-◃<+◃ (suc _) (suc _) = -<+
798+
799+
+◃≮-◃ : Sign.+ ◃ m ≮ Sign.- ◃ n
800+
+◃≮-◃ {zero} {zero} (+<+ ())
801+
+◃≮-◃ {suc m} {zero} (+<+ ())
802+
801803
------------------------------------------------------------------------
802804
-- Properties of _+_
803805
------------------------------------------------------------------------

‎src/Data/Nat/Properties.agda

+8-18
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup;
1717
open import Algebra.Definitions.RawMagma using (_,_)
1818
open import Algebra.Morphism
1919
open import Algebra.Consequences.Propositional
20-
using (comm∧cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ)
20+
using (comm∧cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ; comm⇒sym[distribˡ])
2121
open import Algebra.Construct.NaturalChoice.Base
2222
using (MinOperator; MaxOperator)
2323
import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
@@ -39,7 +39,7 @@ open import Relation.Unary as U using (Pred)
3939
open import Relation.Binary.Core
4040
using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
4141
open import Relation.Binary
42-
open import Relation.Binary.Consequences using (flip-Connex)
42+
open import Relation.Binary.Consequences using (flip-Connex; wlog)
4343
open import Relation.Binary.PropositionalEquality
4444
open import Relation.Nullary hiding (Irrelevant)
4545
open import Relation.Nullary.Decidable using (True; via-injection; map′; recompute)
@@ -1847,23 +1847,13 @@ m∸n≤∣m-n∣ m n with ≤-total m n
18471847
∣ n - m ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m m≤n ⟩
18481848
n ∸ m ∎
18491849

1850-
private
1851-
1852-
*-distribˡ-∣-∣-aux : ∀ a m n → m ≤ n → a * ∣ n - m ∣ ≡ ∣ a * n - a * m ∣
1853-
*-distribˡ-∣-∣-aux a m n m≤n = begin-equality
1854-
a * ∣ n - m ∣ ≡⟨ cong (a *_) (m≤n⇒∣n-m∣≡n∸m m≤n) ⟩
1855-
a * (n ∸ m) ≡⟨ *-distribˡ-∸ a n m ⟩
1856-
a * n ∸ a * m ≡⟨ sym $′ m≤n⇒∣n-m∣≡n∸m (*-monoʳ-≤ a m≤n) ⟩
1857-
∣ a * n - a * m ∣ ∎
1858-
18591850
*-distribˡ-∣-∣ : _*_ DistributesOverˡ ∣_-_∣
1860-
*-distribˡ-∣-∣ a m n with ≤-total m n
1861-
... | inj₂ n≤m = *-distribˡ-∣-∣-aux a n m n≤m
1862-
... | inj₁ m≤n = begin-equality
1863-
a * ∣ m - n ∣ ≡⟨ cong (a *_) (∣-∣-comm m n) ⟩
1864-
a * ∣ n - m ∣ ≡⟨ *-distribˡ-∣-∣-aux a m n m≤n ⟩
1865-
∣ a * n - a * m ∣ ≡⟨ ∣-∣-comm (a * n) (a * m) ⟩
1866-
∣ a * m - a * n ∣ ∎
1851+
*-distribˡ-∣-∣ a = wlog ≤-total (comm⇒sym[distribˡ] {_◦_ = _*_} ∣-∣-comm a)
1852+
$′ λ m n m≤n → begin-equality
1853+
a * ∣ m - n ∣ ≡⟨ cong (a *_) (m≤n⇒∣m-n∣≡n∸m m≤n) ⟩
1854+
a * (n ∸ m) ≡⟨ *-distribˡ-∸ a n m ⟩
1855+
a * n ∸ a * m ≡⟨ m≤n⇒∣m-n∣≡n∸m (*-monoʳ-≤ a m≤n) ⟨
1856+
∣ a * m - a * n ∣ ∎
18671857

18681858
*-distribʳ-∣-∣ : _*_ DistributesOverʳ ∣_-_∣
18691859
*-distribʳ-∣-∣ = comm∧distrˡ⇒distrʳ *-comm *-distribˡ-∣-∣

0 commit comments

Comments
 (0)