[Agda] (s ◃ m ) * (s' ◃ n)

[Sergei Meshveliani]

See the attached   Integer2.agda
(about 150 lines).

My implementation for 

  s◃m*s'◃n : (s s' : Sign) → (m n : ℕ) →
                             (s ◃ m ) * (s' ◃ n) ≡ (s *s s') ◃ (m *n n)

takes about 30 lines (not counting import declarations and comments). 
1/3 of it take 5 lemmata (which probably need to be in the library). 

These 30 line size looks a bit strange for such a trivial thing.

About termination, emacs colors, and reports under emacs:
I never tried anything special for adga-mode, it just happen to set so.

Regards,

------
Sergei




On Fri, 2014-01-10 at 23:32 +0100, Andreas Abel wrote:
> As always, if you want a more thorough investigation of your case, 
> provide self-contained Agda code.
> 
> Best,
> Andreas
> 
> On 10.01.2014 16:36, Sergei Meshveliani wrote:
> > On Fri, 2014-01-10 at 14:13 +0100, Andreas Abel wrote:
> >> On 10.01.2014 13:30, Sergei Meshveliani wrote:
> >>> 1) The part
> >>>
> >>>         e
> >>>      where
> >>>      e : ....
> >>>      e =
> >>>
> >>> needs to be skipped (as I usually do), so that the RHS to be just
> >>> (begin ... end).
> >>> But the checker   (MAlonzo of January 8, 2014)
> >>>
> >>> does not allow this, showing      [ lemma s' s 0 m ]   with yellow
> >>> (probably a termination problem).
> >>> So that I have avoided a termination problem by a lucky occasion with
> >>> extra  "e : ...".
> >>
> >> Termination errors have red background.  Yellow is for unsolved
> >> meta-variables.  By giving the type signature for e you probably helped
> >> Agda to solve some meta-variables.
> >
> >
> > I tried compilation from the command line, and it reports a termination
> > check fail
> > (see my respond to my letter).
> >
> > In _my_ emacs setting, a  termination check fail  looks as follows:
> >
> > several calls of the same function are shown _yellow_, and nothing is
> > reported
> > (in the case of unsolved meta, it usually reports something).
> >
> > Concerning emacs:
> > in command line, I see the reports in full. May be, it is also possible
> > in emacs -- if I knew how to scroll the lower part, in which the report
> > is shown.
> >
> > Regards,
> >
> > ------
> > Sergei
> >
> >
> 
> 

-------------- next part --------------
module Integer2 where

open import Level    using () renaming (zero to 0ℓ)
open import Function using (_$_; case_of_)
open import Algebra.FunctionProperties as FuncProp using ()
open import Algebra using (CommutativeSemiring; module CommutativeSemiring;
                           CommutativeRing; module CommutativeRing)
open import Algebra.Structures using (IsAbelianGroup; module IsAbelianGroup)  
import Algebra.Props.Ring 
open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Relation.Binary using (Setoid; DecSetoid; DecTotalOrder; 
                                                         module DecTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
                                                       _∎ to _≡end)
open import Data.Empty   using (⊥-elim) 
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Nat as Nat using (ℕ; _>_; s≤s; z≤n) 
                            renaming (suc to sucN; _+_ to _+n_; _*_ to _*n_)
open import Data.Nat.Properties as NatProp using ()
open import Data.Sign    as Sign using (Sign) renaming (_*_ to _*s_)
open import Data.Integer as Int using (ℤ; module ℤ; sign; _◃_; ∣_∣)
open import Data.Integer.Properties as IntProp using 
                                              (commutativeRing; sign-◃; abs-◃)



------------------------------------------------------------------------------
natDTO       = Nat.decTotalOrder
natDecSetoid = DecTotalOrder.Eq.decSetoid natDTO    -- for ℕ           
natSetoid    = DecSetoid.setoid natDecSetoid
natEquiv     = Setoid.isEquivalence natSetoid

intSetoid : Setoid 0ℓ 0ℓ 
intSetoid = DecSetoid.setoid Int.decSetoid 

intDTO = Int.decTotalOrder 

natCommSemir = NatProp.commutativeSemiring
open CommutativeSemiring natCommSemir using () renaming (*-comm to *n-comm)

intCommRing = IntProp.commutativeRing
open CommutativeRing intCommRing 
               using (+-isAbelianGroup; _+_; -_; _-_; _*_; +-assoc; 
                      +-comm; *-assoc; *-comm; distrib; *-identity; *-cong)
               renaming (ring to intRing)

module FPs  = FuncProp (_≡_ {A = Sign})

open ℤ
open IsAbelianGroup +-isAbelianGroup using () 
                              renaming (identity to zero; inverse to opposite) 

------------------------------------------------------------------------------
*n-0 : (n : ℕ) → (n *n 0) ≡ 0
*n-0 n =  PE.trans (*n-comm n 0) PE.refl

*0 : (x : ℤ) → x * (+ 0) ≡ + 0     
*0 x =  
       ≡begin  x * (+ 0)          ≡[ PE.refl ] 
               sg ◃ (∣ x ∣ *n 0)  ≡[ PE.cong (_◃_ sg) $ *n-0 ∣ x ∣ ]
               sg ◃ 0             ≡[ PE.refl ]
               + 0
       ≡end 
       where   sg = (sign x) *s Sign.+

0* :  (x : ℤ) → (+ 0) * x ≡ + 0     
0* x =  PE.trans (*-comm (+ 0) x) $ *0 x

◃-0 : (s : Sign) → s ◃ 0 ≡ + 0 
◃-0 _ = PE.refl            

*s-comm : FPs.Commutative _*s_
*s-comm Sign.+ Sign.+ = PE.refl
*s-comm Sign.+ Sign.- = PE.refl
*s-comm Sign.- Sign.+ = PE.refl
*s-comm Sign.- Sign.- = PE.refl

------------------------------------------------------------------------------
s◃m*s'◃n : (s s' : Sign) → (m n : ℕ) → 
                           (s ◃ m ) * (s' ◃ n) ≡ (s *s s') ◃ (m *n n)
s◃m*s'◃n _ _  0 _ =  PE.refl 
s◃m*s'◃n s s' m 0 =  e         
    where
    -- Reduce "m 0" to the case of "0 m".
    -- Note:  omitting  "e : ..."  leads to a termination problem.

    e : (s ◃ m) * (+ 0) ≡ (s *s s') ◃ (m *n 0)
    e = ≡begin   
            (s ◃ m) * (+ 0)        ≡[ *0 (s ◃ m) ]
            + 0                    ≡[ PE.sym $ 0* (s ◃ m) ]
            (+ 0) * (s ◃ m)        ≡[ PE.cong (\z → z * (s ◃ m)) $ ◃-0 s' ]
            (s' ◃ 0) * (s ◃ m)     ≡[ s◃m*s'◃n s' s 0 m ]
            (s' *s s) ◃ (0 *n m)   ≡[ PE.cong (_◃_ (s' *s s)) $ *n-comm 0 m ]
            (s' *s s) ◃ (m *n 0)   ≡[ PE.cong (\sg → sg ◃ (m *n 0)) $ 
                                                               *s-comm s' s ]
            (s *s s') ◃ (m *n 0)
        ≡end
                  
s◃m*s'◃n s s' (sucN m) (sucN n) = 
  ≡begin 
    (s ◃ m') * (s' ◃ n')                                          ≡[ PE.refl ]
    (sign (s ◃ m') *s sign (s' ◃ n')) ◃ ((∣ s ◃ m' ∣) *n (∣ s' ◃ n' ∣))

                           ≡[ PE.cong (\sg → sg ◃ part2) $ 
                                      PE.cong₂ _*s_ (sign-◃ s m) (sign-◃ s' n)
                            ]
    (s *s s') ◃ ((∣ s ◃ m' ∣) *n (∣ s' ◃ n' ∣))
                         ≡[ PE.cong (_◃_ (s *s s')) $ 
                                    PE.cong₂ _*n_ (abs-◃ s m') (abs-◃ s' n') ]
    (s *s s') ◃ (m' *n n')
  ≡end
  where
  m'    = sucN m
  n'    = sucN n
  part2 = (∣ s ◃ m' ∣) *n (∣ s' ◃ n' ∣)