[Agda] Integer lemmata

[Arseniy Alekseyev]

It looks like the -* and *- lemmata correspond to
Algebra.Props.Ring.-‿*-distribˡ and Algebra.Props.Ring.-‿*-distribʳ.

On 8 January 2014 21:51, Sergei Meshveliani <mechvel at botik.ru> wrote:
> People,
>
> this is on  Standard library lib-0.7.
>
> I need to use 15-20 trivial lemmata for  Integer,  like these:
>
>        x * (+ 0) ≡ + 0
>        x * (- y) ≡ - (x * y)
>
> For this, I use  Data.Integer.Properties.commutativeRing,
> and still write the code shown below.
>
> I suspect that I write for this too much code of my own.
> Consider, for example,  `-*' below.
> Can this be simplified? (may be, by taking something from library).
>
> Thanks,
>
> ------
> Sergei
>
>
> -------------------------------------------------------------------------------
> open import Data.Integer as Int using (ℤ; module ℤ; sign; _◃_; ∣_∣)
> open import Data.Integer.Properties as IntProp using (commutativeRing)
> ...
> natCommSemir = NatProp.commutativeSemiring
> open CommutativeSemiring natCommSemir using ()
>                                  renaming (*-comm to *comm-nat)
> intCommRing = IntProp.commutativeRing
> open CommRing' intCommRing
>                using (+-isAbelianGroup; _+_; -_; _-_; _*_; +-assoc;
>                       +-comm; *-assoc; *-comm; distrib; *-identity)
>
> open IsAbelianGroup +-isAbelianGroup using ()
>                       renaming (identity to zero; inverse to opposite)
> open ℤ
>
> +0≢+m' : ∀ {m} → + 0 ≢ + (sucN m)
> +0≢+m' ()
>
> +m≢- : {m n : ℕ} → (+ m) ≢ -[1+ n ]
> +m≢- ()
>
> 0+ : (x : ℤ) → (+ 0) + x ≡ x
> 0+ = proj₁ zero
>
> +0 : (x : ℤ) → x + (+ 0) ≡ x
> +0 = proj₂ zero
>
> x+-x : (x : ℤ) → x + (- x) ≡ (+ 0)
> x+-x = proj₂ opposite
>
> -x+x : (x : ℤ) → (- x) + x ≡ (+ 0)
> -x+x = proj₁ opposite
>
> *1 : (x : ℤ) → x * (+ 1) ≡ x
> *1 = proj₂ *-identity
>
> *0 : (x : ℤ) → x * (+ 0) ≡ + 0   -- *** where to take it from?
> *0 x =
>        ≡begin  x * (+ 0)          ≡[ PE.refl ]
>                sg ◃ (∣ x ∣ *n 0)  ≡[ PE.cong (_◃_ sg) $ Nat2.*0 ∣ x ∣ ]
>                sg ◃ 0             ≡[ PE.refl ]
>                + 0
>        ≡end
>
> 0* :  (x : ℤ) → (+ 0) * x ≡ + 0
> 0* x =  PE.trans (*-comm (+ 0) x) $ *0 x
>
> +◃ : (m : ℕ) → (Sign.+ ◃ m) ≡ + m
> +◃ 0        = PE.refl
> +◃ (sucN _) = PE.refl
>
> -◃ : (m : ℕ) → (Sign.- ◃ m) ≡ - (+ m)
> -◃ 0        = PE.refl
> -◃ (sucN _) = PE.refl
>
> +m*+n= : (m n : ℕ) → (+ m) * (+ n) ≡ + (m *n n)
> +m*+n= m n =
>              ≡begin  (+ m) * (+ n)       ≡[ PE.refl ]
>                      Sign.+ ◃ (m *n n)   ≡[ +◃ (m *n n) ]
>                      + (m *n n)
>              ≡end
> --
> -- ** where to take them?
> --
> +m*-n'= :  (m n : ℕ) →  (+ m) * -[1+ n ] ≡ - (+ (m *n sucN n))
> +m*-n'= m n =
>              ≡begin  (+ m) * -[1+ n ]        ≡[ PE.refl ]
>                      Sign.- ◃ (m *n sucN n)  ≡[ -◃ (m *n sucN n) ]
>                      - (+ (m *n sucN n))
>              ≡end
>
> negneg : (x : ℤ) → - (- x) ≡ x   -- **
> negneg (+ 0)      = PE.refl
> negneg (+ sucN _) = PE.refl
> negneg -[1+ _ ]   = PE.refl
>
>
> -* : (x y : ℤ) → (- x) * y ≡ - (x * y)
>
> -* (+ 0)      _     =  PE.refl
> -* x          (+ 0) =
>                 ≡begin (- x) * (+ 0)    ≡[ *0 (- x) ]
>                        (+ 0)            ≡[ PE.refl ]
>                        - (+ 0)          ≡[ PE.cong -_ $ PE.sym $ *0 x ]
>                               - (x * (+ 0))
>                 ≡end
> -* (+ sucN _) (+ sucN _) =  PE.refl
> -* (+ sucN _) -[1+ _ ]   =  PE.refl
> -* -[1+ _ ]   (+ sucN _) =  PE.refl
> -* -[1+ _ ]   -[1+ _ ]   =  PE.refl
>
>
> *- : (x y : ℤ) → x * (- y) ≡ - (x * y)
> *- x y =
>          ≡begin  x * (- y)    ≡[ *-comm x (- y) ]
>                  (- y) * x    ≡[ -* y x ]
>                  - (y * x)    ≡[ PE.cong -_ $ *-comm y x ]
>                  - (x * y)
>          ≡end
>
> -*- : (x y : ℤ) → (- x) * (- y) ≡ x * y
> -*- x y =
>           ≡begin  (- x) * (- y)   ≡[ -* x (- y) ]
>                   - (x * (- y))   ≡[ PE.cong -_ $ *- x y ]
>                   - (- (x * y))   ≡[ negneg _ ]
>                   x * y
>           ≡end
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda