[Agda] With and the inspect idiom

[Shin-Cheng Mu]

I just realised that my previous message was sent with wrong
encoding (Big5 rather than UTF-8). Hope this message could be
displayed correctly on your computer, if the previous one
did not. Sorry for duplicated posting.

     ----------

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) = { }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 ≡ (c , d) in { }0, I cannot simply use ≡-refl.
To get such a term, I could use the "inspect idiom":

    foo <something else> f b with inspect (f b)
    ...| (c , d) with-≡ fb≡cd = { }0

The type of fb≡cd is f b ≡ (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-≡ v≡fb    with f b | v≡fb
    ...    | (c , d) | v≡cd = { }0

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

      v≡fb   : v ≡ f b
      v≡cd   : v ≡ (c , d)

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

      ≡-trans (≡-sym v≡fb) v≡cd   :   f b ≡ (c , d)

But is there a simpler way to achieve so?

sincerely,
Shin