[Agda] Magic-with and inspect -- can I have both?

[Shin-Cheng Mu]

Hi,

Assuming that I am proving some property of a function f
that is inductively defined and returns a _⊎_ type :

   f [] = ...
   f (x ∷ xs) with f xs
   ... | inj₁ b = ..
   ... | inj₂ c = inj₂ d

The lemma I am proving mentions

   lemma : {a : Set}(xs : [ a ]) ... ->
              (f xs ≡ inj₂ e) -> ...
   lemma [] .. = ...
   lemma (x ∷ ys)... fx∷ys≡inj₂e ...

At this stage, fx∷ys≡inj₂e has type

        (f (x ∷ ys) | f x) ≡ inj₂ e

For further analysis, one may do a pattern match on f ys:

   lemma : {a : Set}(xs : [ a ]) ... ->
              (f xs ≡ inj₂ e) -> ...
   lemma [] .. = ...
   lemma (x ∷ ys)... fx∷ys≡inj₂e ...
     with f ys
   ...  | inj₁ b = ..
   ...  | inj₂ c = .. { }0

by the magic-with, the type of fx∷ys≡inj₂e at { }0 now gets
refined to:

        inj₂ d ≡ inj₂ e

which I may need in { }0.

However, I may also need to make an inductive call to
lemma, which demands an argument of type f ys ≡ inj₂ c:

   lemma : {a : Set}(xs : [ a ]) ... ->
              (f xs ≡ inj₂ e) -> ...
   lemma [] .. = ...
   lemma (x ∷ ys) ... fx∷ys≡inj₂e ...
     with f ys
   ...  | inj₁ b = ..
   ...  | inj₂ c  with lemma ys ... fys≡inj₂c
   ...     | something = { }0

To produce such a term fys≡inj₂c I need the inspect idiom:

   lemma : {a : Set}(xs : [ a ]) ... ->
              (f xs ≡ inj₂ e) -> ...
   lemma [] .. = ...
   lemma (x ∷ ys) ... fx∷ys≡inj₂e ...
     with inspect (f ys)
   ...  | inj₁ b with-≡ _ = ..
   ...  | inj₂ c with-≡ fys≡inj₂c
           with lemma ys ... fys≡inj₂c
   ...     | something = { }0

But if I do so, magic-with does not work and the type of
fx∷ys≡inj₂e remains to be (f (x ∷ ys) | f x) ≡ inj₂ e
at { }0

How can I have both?

Josh Ko came up with this solution:

   lemma : {a : Set}(xs : [ a ]) ... ->
              (f xs ≡ inj₂ e) -> ...
   lemma [] .. = ...
   lemma (x ∷ ys) ... fx∷ys≡inj₂e ...
     with inspect (f ys)
   ...  | z with-≡ z≡fys with f ys | z≡fys
   ...       | inj₁ b = ..
   ...       | inj₂ c | z≡inj₂ c =
                 with lemma ys ... (≡-trans (≡-sym z≡fys)  
z≡inj₂c)
   ...              | something = { }0


As the name suggests, z≡fys has type z ≡ f ys, while
z ≡ inj₂c has type z ≡ inj₂ c. Composing them together
using transitivity, I get a term having the type I want,
f ys ≡ inj₂ c.

Is there a better way, however? Or, am I on a wrong direction
in the first place if I need properties like this?

sincerely,
Shin