[Agda] using inspect is tricky

[Andreas Abel]

Hi Florent,

did you try Josh Ko's pattern? (see below)

Andreas

Begin forwarded message:

> From: Shin-Cheng Mu <scm at iis.sinica.edu.tw>
> Date: March 28, 2008 5:25:36 AM GMT+01:00
> To: agda at lists.chalmers.se
> Subject: [Agda] Magic-with and inspect -- can I have both?
>
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
On Jan 5, 2010, at 7:08 PM, Florent Balestrieri wrote:

> Hello,
>
> I have the following problem:
>
> Given two functions `f' and `g' such that the type of `g x'
> depend on the expression `f x'.
>
> I'm defining a function `p':
>
>> p x with f x | g x
>>
>> ... | .a | h a = ?
>
> In the body, I need the equality proof that:
>
>> f x == a
>
> alas, I cannot manage to use inspect: it just won't be
> instantiated, and I get:
>
>> p x with f x | inspect (f x) | g x
>>
>> ... | .a | i | h a = ?
>
> which is not very helpful.
>
> I then tried to instantiate `g x' but for some typing reason,
> agda refuses to inspect `g x' when `f x' is also in the
> `with' clause (It is still a bit unclear why exactly).
>
> That is, I can write
>
>> p x with inspect (g x)
>
> but not
>
>> p x with f x | inspect (g x)
>
> Many thanks for the helpful people here!
> -- Florent
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41