[Agda] trivial lemma of `with'

[Andreas Abel]

See below...

On 04.01.2014 10:47, Sergei Meshveliani wrote:
> On Fri, 2014-01-03 at 18:25 +0100, Andreas Abel wrote:
>> 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.
>
> The thing is so important that, probably, it needs to become a part of
> the (future) Agda standard.
> Without the irrelevance annotation many proofs will be difficult to
> write.
>
>> 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.
>
>
> But this relies on  _==_.

I should have been more clear: _==_ here is Leibniz-equality.  (The 
\equiv of Relation.Binary.PropositionalEquality).

> (I suspect that I misuse irrelevance in my examples in the Bug tracker
> 1013).
>
> My real application has
>
>     divRem  : (x y : C) → .(nz : y ≉ 0#) → DivRem eucNorm x y _,      (1)
>
> where  DivRem  is a certain record, and these records are not at all
> expected to be compared for equality.
>
> What kind of irrelevance means this   .(nz : y ≉ 0#)
> ?
> I find the 'Irrelevance' topic in the online manual.
> And it is not clear from it of whether the usage (1) of irrelevance is
> correct. The manual says in the beginning
>               "... f  does not depend computationally on its argument".
>
> What kind of _==_ is presumed in this sentence?

Definitional equality.  That would be Leibniz-equalities which can be 
proved by "refl".


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