[Agda] trivial lemma of `with'

[Andreas Abel]

The problem is that in the last case, "| no _", you have two different 
proofs of y /= 0.  You probably intend that dRem is independent of the 
proof of y/=0.  One way is to state that using irrelevance, then your 
proof goes through:

   record Foo : Set (α ⊔ α=)
     where
     field  _≟_  : Decidable _≈_
            dRem : (x y : C) → .(y≉0 : ¬ y ≈ 0#) → C

     eQuot : C → C → C
     eQuot x y  with y ≟ 0#
     ...      | yes _  = 0#
     ...      | no y≉0 = dRem x y y≉0

     lemma : {x y : C} → (y≉0 : ¬ y ≈ 0#) → eQuot x y ≈ dRem x y y≉0
     lemma {x} {y} y≉0 with y ≟ 0#
     ...              | yes y=0 =  ⊥-elim (y≉0 y=0)
     ...              | no  y≠0 =  refl


On 30.12.13 6:23 PM, Sergei Meshveliani wrote:
> open import Level using (Level; _⊔_)
> open import Relation.Nullary using (¬_; yes; no)
> open import Relation.Binary using (IsEquivalence; module IsEquivalence;
>                                                             Decidable)
> open import Algebra    using (Semiring; module Semiring)
> open import Data.Empty using (⊥-elim)
>
> module _ {α α=} (R : Semiring α α=)
>    where
>    open Semiring R using (_≈_; 0#)
>                    renaming (Carrier to C; isEquivalence to ≈equiv)
>    open IsEquivalence ≈equiv using (refl)
>
>    record Foo : Set (α ⊔ α=)
>      where
>      field  _≟_  : Decidable _≈_
>             dRem : (x y : C) → (y≉0 : ¬ y ≈ 0#) → C
>
>      eQuot : C → C → C
>      eQuot x y  with y ≟ 0#
>      ...      | yes _  = 0#
>      ...      | no y≉0 = dRem x y y≉0
>
>      lemma : {x y : C} → (y≉0 : ¬ y ≈ 0#) → eQuot x y ≈ dRem x y y≉0
>      lemma {x} {y} y≉0 =  refl
>
> {-  with y ≟ 0#
>      ...              | yes y=0 =  ⊥-elim (y≉0 y=0)
>      ...              | no _    =  refl
> -}
>
> The  development Agda of November ~20 2013 MAlonzo
> reports
> eQuot  x y | y ≟ 0# != dRem x y y≉0 of type C
> when checking that the expression refl has type
> eQuot x y ≈ dRem x y y≉0
>

-- 
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/