[Agda] `with' --> `case' fails

[Sergei Meshveliani]

Please how to rewrite the `with' program to the `case' one in the below
example?

The `with' variant has repetitions (of the  pp∙x=x∙pp  implementation
and others) in the two `with' branches. These unpleasant repetitions 
must (as I think) disappear in the `case' version.

The `with' version is type-cheked.
But my `case' version (obtained by the most natural conversion) is not.
The report is

  /home/mechvel/doconA/0.03/source/AlgClasses1.agda:382,39-56
  x != pow cnt x hf suc>0 of type C
  when checking that the expression <x∙pp>∙x=x∙<x∙pp> has type
  (p ∙ p) ∙ x ≈ x ∙ (p ∙ p)

The code is not full.
I can provide the full one -- if the below is not sufficient to tell.

Thank you in advance for explanation,

------
Sergei



---------------------------------------------------------------------------
module Power α α= (upSemig : UpSemigroup α α=)
  where
  semig = UpSemigroup.semigroup upSemig
  open Semigroup semig
           using (setoid; _≈_; _∙_; ∙assoc; ∙cong₁; ∙cong₂)
           renaming (Carrier to C; isEquivalence to ≈equiv)
  open IsEquivalence ≈equiv using ()
                            renaming (refl to ≈refl; sym to ≈sym)
  open DecTotalOrder natDTO using () renaming (trans to ≤trans)

  open module EqR-setoid = EqR setoid renaming (_≈⟨_⟩_ to _≈[_]_)
  open _≤_

  pow : ℕ → C → (e : ℕ) → e > 0 → C
                              -- Power  x  to  e  (return  x^e)   
                              -- by the binary method             
  pow 0         x  _            _  = x
  pow _         x  0            ()
  pow _         x (suc 0)       _  = x
  pow (suc cnt) x (suc (suc e)) _  = case  even? e  of \
                                     { (yes _) → p ∙ p
                                     ; _       → x ∙ (p ∙ p) }
                                     where
                                     hf = suc (half e)
                                     p  = pow cnt x hf suc>0

  -----------------------------------------------------------     
  comm-with-power :
              (cnt : ℕ) → (x : C) → (e : ℕ) → (e>0 : e > 0) →
              (pow cnt x e e>0) ∙ x ≈ x ∙ (pow cnt x e e>0)

  -- Prove  x ∙ x^e ≈ x^e ∙ x.                                    

  comm-with-power 0         x e             _     =  ≈refl
  comm-with-power _         x 0             ()
  comm-with-power (suc _)   x (suc 0)       _     =  ≈refl
  comm-with-power (suc cnt) x (suc (suc e)) e''>0

    with  even? e

    ... | yes _ = pp∙x=x∙pp
        where
        hf    = suc (half e)
        p     = pow cnt x hf suc>0
        px=xp = comm-with-power cnt x hf suc>0

        pp∙x=x∙pp : (p ∙ p) ∙ x ≈ x ∙ (p ∙ p)
        pp∙x=x∙pp =
             begin  (p ∙ p) ∙ x   ≈[ ∙assoc p p x ]
                    p ∙ (p ∙ x)   ≈[ ∙cong₂ px=xp ]
                    p ∙ (x ∙ p)   ≈[ ≈sym $ ∙assoc p x p ]
                    (p ∙ x) ∙ p   ≈[ ∙cong₁ px=xp ]
                    (x ∙ p) ∙ p   ≈[ ∙assoc x p p ]
                    x ∙ (p ∙ p)
             ∎

    ... | no _ = <x∙pp>∙x=x∙<x∙pp>
        where
        half-e = half e
        hf     = suc half-e
        p      = pow cnt x hf suc>0
        pp     = p ∙ p
        px=xp  = comm-with-power cnt x hf (suc>0 {half-e})

        pp∙x=x∙pp =
             begin  (p ∙ p) ∙ x   ≈[ ∙assoc p p x ]
                    p ∙ (p ∙ x)   ≈[ ∙cong₂ px=xp ]
                    p ∙ (x ∙ p)   ≈[ ≈sym $ ∙assoc p x p ]
                    (p ∙ x) ∙ p   ≈[ ∙cong₁ px=xp ]
                    (x ∙ p) ∙ p   ≈[ ∙assoc x p p ]
                    x ∙ (p ∙ p)
             ∎
        <x∙pp>∙x=x∙<x∙pp> : (x ∙ pp) ∙ x ≈ x ∙ (x ∙ pp)
        <x∙pp>∙x=x∙<x∙pp> =
               begin  (x ∙ pp) ∙ x   ≈[ ∙assoc x pp x ]
                      x ∙ (pp ∙ x)   ≈[ ∙cong₂ pp∙x=x∙pp ]
                      x ∙ (x ∙ pp)
               ∎
      
{- The `case' version -- to replace the last segment of  `with'  : 

    = case even? e of \ { (yes _) → pp∙x=x∙pp
                        ; (no _)  → <x∙pp>∙x=x∙<x∙pp> }
    where
    hf    = suc (half e)
    p     = pow cnt x hf suc>0
    pp    = p ∙ p
    px=xp = comm-with-power cnt x hf suc>0

    pp∙x=x∙pp : (p ∙ p) ∙ x ≈ x ∙ (p ∙ p)
    pp∙x=x∙pp =
         begin  (p ∙ p) ∙ x   ≈[ ∙assoc p p x ]
                p ∙ (p ∙ x)   ≈[ ∙cong₂ px=xp ]
                p ∙ (x ∙ p)   ≈[ ≈sym $ ∙assoc p x p ]
                (p ∙ x) ∙ p   ≈[ ∙cong₁ px=xp ]
                (x ∙ p) ∙ p   ≈[ ∙assoc x p p ]
                x ∙ (p ∙ p)
         ∎
    <x∙pp>∙x=x∙<x∙pp> : (x ∙ pp) ∙ x ≈ x ∙ (x ∙ pp)
    <x∙pp>∙x=x∙<x∙pp> =
         begin  (x ∙ pp) ∙ x   ≈[ ∙assoc x pp x ]
                x ∙ (pp ∙ x)   ≈[ ∙cong₂ pp∙x=x∙pp ]
                x ∙ (x ∙ pp)
         ∎
-}