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

[Sergei Meshveliani]

The below question of simplicity remains.

As to the question of omitting  "e : ...",  I suspect the following
effect, which may look natural.
The first clause proves the case of   0 m,
and the second clause reduces a proof for  m 0  to the case of  0 m
by applying commutativity of _*_ and by calling the same  lemma.
If the signature of  e  is omitted, the checker sees that  
(lemma ... m 0)  calls for  (lemma ... 0 m),  and does not see that the
argument pair has become smaller.
The signature for  e  is special, it contains `0'. 
And it is easier for the checker to see termination
(still, how does this occur?).  

------
Sergei


On Fri, 2014-01-10 at 16:30 +0400, Sergei Meshveliani wrote:
> People,
> I have a question about usage of Integer of Standard library.
> 
> Consider this trivial and naturally looking lemma: 
> 
>   lemma : (s s' : Sign) → (m n : ℕ) → 
>           (s ◃ m ) * (s' ◃ n) ≡ (s *s s') ◃ (m *n n), 
> 
> where  _*s_ = Sign._*_,  _*n_ = Nat._*_,  _*_ = Integer._*_. 
> 
> What can be a reasonably simple proof for it? 
> 
> This my proof is checked but looks rather complex:
> 
> ----------------------------------------------------------------
> lemma _ _  0 _ =  PE.refl
> lemma s s' m 0 =  e           -- reduce to  "0 m"
>   where
>   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)     ≡[ lemma 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
> 
> lemma 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' ∣)
> ------------------------------------------------------------------------
> 
> Also there are the two strange points. 
> 
> 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 : ...".
> 
> 
> 2) In     ≡[ PE.cong (\z → z * (s ◃ m)) $ ◃-0 s' ]
> 
>   "◃-0 s'"  is a lemma which maps to  s' ◃ 0 ≡ + 0.
> This is only by normalization, but the checker reports of unsolved metas
> when I set  PE.refl  directly to the place. I tried adding hidden args
> but failed.
> 
> Thank you in advance for your notes.
> 
> ------
> Sergei
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>