[Agda] trivial lemma of `with'

[Andreas Abel]

Irrelevant arguments (a bit unluckily marked by a dot) can only be used 
in irrelevant positions.  Thus, if you want to use _divMod_ of the 
std-lib, you will run into trouble (as you describe below).

Nisse does not make use of irrelevance, so there are no uses of it in 
the standard library.

As an alternative to irrelevance, you can claim proof irrelevance 
manually, e.g. by adding a field

   dRemIrr : (x y : C) (p q : \neg (y \approx 0#)) ->
     dRem x y p == dRem x y q

for a suitable notion of equality ==.

Then, of course, you have to prove it for each instance of Foo.

Cheers,
Andreas

On 02.01.2014 15:35, Sergei Meshveliani wrote:
> On Tue, 2013-12-31 at 01:02 +0100, Andreas Abel wrote:
>> 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
>>
>
> !!
> Thank you. This dot usage is new for me.
>
> 1. Is it explained in some manual?
>
> 2. For example,  Data.Nat.DivMod._divMod_  of  lib-0.7  has signature
>
>     (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
>     DivMod dividend divisor
>
> Will there arise difficulties in proofs caused by that  ≢0  is not
> dotted here?
>
> 3. In my real program, I have
>
>     field eucNorm : EuclideanNorm
>           divRem  : (x y : C) → (y≉0 : y ≉ 0#) → DivRem eucNorm x y y≉0
>
> Setting dot on the first "y≉0" causes an error report. So, I try this:
>
>           divRem  : (x y : C) → .(y≉0 : y ≉ 0#) → DivRem eucNorm x y _
>
>
> in a hope that the checker knows what to put for `_'.
> Is this a regular solution?
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
>
>


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