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

[Andreas Abel]

The full code would be helpful to answer your question. --Andreas

On 26.09.2013 13:29, Sergei Meshveliani wrote:
> 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)
>           ∎
> -}
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/