[Agda] With and the inspect idiom

[Shin-Cheng Mu]

Hi,

I asked this question before but I probably have not made myself
understood. I recently encountered the same problem, so I would
like to bring up the topic again..

Suppose I am defining such a function:

     foo <something else> f b  with f b
     ...| (c , d) =3D { }0

by performing "with f b", the types of some arguments in
<something else> that involve (f b) would be refined to more
specific types.

Strangely, however, after "with f b", Agda does not seem to
have the knowledge that (f b) equals (c , d). If I need a term
of type f b =A1=DD (c , d) in { }0, I cannot simply use =A1=DD-refl.
To get such a term, I could use the "inspect idiom":

     foo <something else> f b with inspect (f b)
     ...| (c , d) with-=A1=DD fb=A1=DDcd =3D { }0

The type of fb=A1=DDcd is f b =A1=DD (c , d).

However, now the types of other arguments in <something else>
don't get refined! How do I achieve both?

We found this weird trick using "with" twice:

     foo <something else> with inspect (f b)
     ... | v with-=A1=DD v=A1=DDfb    with f b | v=A1=DDfb
     ...    | (c , d) | v=A1=DDcd =3D { }0

After "with f b", the types of arguments in <something else>
do get refined. Furthermore, we now have two proofs having type:

       v=A1=DDfb   : v =A1=DD f b
       v=A1=DDcd   : v =A1=DD (c , d)

So I get a proof of f b =A1=DD (c , d) by transitivity:

       =A1=DD-trans (=A1=DD-sym v=A1=DDfb) v=A1=DDcd   :   f b =A1=DD (c =
, d)

But is there a simpler way to achieve so?

sincerely,
Shin