[Agda] trivial lemma of `with'

[Sergei Meshveliani]

(I return to copying to the list after forgetting of this in my last
letter)

On Sun, 2014-01-05 at 20:29 +0100, Andreas Abel wrote:
> On 05.01.2014 18:10, Sergei Meshveliani wrote:
> > On Sun, 2014-01-05 at 16:52 +0100, Andreas Abel wrote:
> >> See below...
> >> [..]

> > I have
> >
> >    record DivRem (norm : EuclideanNorm) (a b : C) (nzb : b ≉ 0#) : Set _
> >      where
> >      ...
> >
> >    divRem : (x y : C) → (nz : y ≉ 0#) → DivRem eucNorm x y nz     -- (1)
> >
> > The result of divRem has a type which depends on the choice of
> >                                                              nz : y ≉ 0#.
> > Will the irrelevance denotation  .(...)  have a sense here:
> >
> >    divRem : (x y : C) → .(nz : y ≉ 0#) → DivRem eucNorm x y _    -- (1')
> > ?
> >
> > Does it mean that for  (x y : C), (nz nz' : y ≉ 0#),
> > the corresponding values  dr, dr'  of  divRem  belong to the same type
> > and  dr ≡ dr'
> > ?


> You will need irrelevance also in DivRem:
> 
>    record DivRem (norm : EuclideanNorm) (a b : C) .(nzb : b ≉ 0#) : Set _
> 
> Then this makes sense:
> 
>    divRem : (x y : C) → .(nz : y ≉ 0#) → DivRem eucNorm x y nz


1. The checker rejects the last occurrence of  nz  here,  but accepts
underscore instead.

2. This latter construct with  DivRem, divRem, and irrelevance in both,
is tried in  AlgClasses4.agda  in my last remark to the  ticket 1013.
And it is not type-checked.
Can you please, fix this code? Is it a checker bug?

The irrelevance annotation is a new feature, and it can be difficult to
implement (it needs to be used not only in function signatures).
But without this annotation some proofs are very difficult to compose.

Because in most applications a thing depends on a condition, but not on
the proof choice for this condition.

So, it is desirable to make irrelevance annotations work in a possibly
wide area.

Thanks,

------
Sergei