New issue 1342 [Re: [Agda] join 2 `with'|]
Andreas Abel
abela at chalmers.se
Wed Nov 5 09:39:54 CET 2014
Nice catch! To sum up, the following test case is accepted
open import Common.Prelude
open import Common.Equality
id : (A : Set) → A → A
id A x = x
f : Bool → Bool
f x = true where
z : Bool → Bool
z true = x
z false = x
y : ∀ q → x ≡ z q
y with x
y | true = id {!!} λ { true → refl ; false → refl }
y | false = id {!!} λ { true → refl ; false → refl }
The two holes are solved by Agda (C-c C-=)
?0 := (q : Bool) → true ≡ z q
?1 := (q : Bool) → false ≡ z q
But if you give the solution (C-c C-s), Agda complains!
https://code.google.com/p/agda/issues/detail?id=1342
On 05.11.2014 09:21, Arseniy Alekseyev wrote:
> Oh wow, I should have tried that. I don't understand why this works at
> all. Note that none of these compile for me:
>
> y | true = id {A = (q : Bool) → x ≡ z q} (λ { true → refl ; false
> → refl }) -- x != true of type Bool
>
> y | true = id {A = (q : Bool) → true ≡ z q} (λ { true → refl ;
> false → refl }) -- true != x of type Bool
>
> However, even more confusingly, this one does work:
>
> y | true = id {A = _} (λ { true → refl ; false → refl })
>
> So what's the value of underscore it infers then?
> Can anybody explain what's going on?
>
> As for the code smell part, I think you can only smell it on toy
> examples, not on the "real" ones.
>
> On 5 November 2014 01:28, Christopher Jenkins <cjenkin1 at trinity.edu> wrote:
>>
>>
>> On Tue, Nov 4, 2014 at 5:18 PM, Arseniy Alekseyev
>> <arseniy.alekseyev at gmail.com> wrote:
>>>
>>> That was not a genuine attempt to prove `y : ∀ q → x ≡ z q`. Instead
>>> that was an example of `with` rewriting the goal from (as you
>>> demonstrated!) provable one into (as I assert) non-provable one. I
>>> think that's the property of `with` that's causing you grief when you
>>> re-order or nest them in a bad way.
>>>
>> Ah, makes sense. Though of course you could probably continue on to prove
>> the goal by pattern-matching on a lambda argument introduced in both cases,
>> but by that point hopefully someone would see the code smell.
>>
>> Actually, decided to include it anyway, so you could smell the smelly code
>> smell:
>>
>> y : ∀ q → x ≡ z q
>> y with x
>> y | true = λ { true → refl ; false → refl }
>> y | false = λ { true → refl ; false → refl }
>>
>>>
>>> On 4 November 2014 22:43, Christopher Jenkins <cjenkin1 at trinity.edu>
>>> wrote:
>>>>
>>>>
>>>> On Mon, Nov 3, 2014 at 2:38 PM, Arseniy Alekseyev
>>>> <arseniy.alekseyev at gmail.com> wrote:
>>>>>
>>>>> You are right, there is not much point. I was trying to point out that
>>>>> it's the "proper expression" part that makes `with` complicated.
>>>>>
>>>>> Unfortunately, that's not even true. In the following example, I don't
>>>>> think you can fill the holes.
>>>>>
>>>>> f : Bool → Bool
>>>>> f x = true where
>>>>>
>>>>> z : Bool → Bool
>>>>> z true = x
>>>>> z false = x
>>>>>
>>>>> y : ∀ q → x ≡ z q
>>>>> y with x
>>>>> y | true = {!!}
>>>>> y | false = {!!}
>>>>>
>>>>>
>>>>
>>>> I'm not entirely sure why you would expect that approach to be fruitful.
>>>> Essentially, what you're trying to do is unwind the computational nature
>>>> of
>>>> `z', which is defined by case analysis on its argument (in this case q).
>>>> To
>>>> trigger the rules, you would have to bring q into scope and inspect q,
>>>> which
>>>> would then lead to `z true' and `z false' in the equations,
>>>> respectively,
>>>> and Agda will then go on to normalize the goals as `x \== x'
>>>>
>>>> f : Bool → Bool
>>>> f x = true where
>>>> z : Bool → Bool
>>>> z true = x
>>>> z false = x
>>>>
>>>> y : ∀ q → x ≡ z q
>>>> y true = {!!} -- Goal: x ≡ x
>>>> y false = {!!} -- Goal: x ≡ x
>>>>
>>>> I have actually been thinking about writing a blog post targeted at
>>>> newbies
>>>> (such as myself) on the sometimes unintuitive behaviour of `with' (and
>>>> in
>>>> particular, `rewrite'). Should anyone be interested I can send a link on
>>>> this email chain once I have written it.
>>>>
>>>>
>>>>>
>>>>> On 3 November 2014 10:59, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>>>>>> On 03.11.2014 09:47, Arseniy Alekseyev wrote:
>>>>>>> I think the problem goes away if you
>>>>>>> only use `with x` where `x` is a variable.
>>>>>>
>>>>>> Mmh, why use `with` at all then? You could directly split on the
>>>>>> variable
>>>>>> `x`. I thought the only reason to use `with` was when you wanted to
>>>>>> case on
>>>>>> a proper expression and refine your type in the with-branches...
>>>>>>
>>>>>>
>>>>>>
>>>>>> On 03.11.2014 09:47, Arseniy Alekseyev wrote:
>>>>>>>
>>>>>>> Indeed that's the usual Agda behaviour.
>>>>>>> Here the reason seems to be an additional occurrence of `lookup k
>>>>>>> ps`
>>>>>>> in the context produced by pattern-match on `no`.
>>>>>>> You see, `with expr` only rewrites the occurrences of `expr` present
>>>>>>> in the enclosing context, so the new occurrences inside the body of
>>>>>>> `with` don't get rewritten (and you do want it rewritten in this
>>>>>>> case).
>>>>>>>
>>>>>>> I do agree this is confusing. I think the problem goes away if you
>>>>>>> only use `with x` where `x` is a variable. That makes `with` much
>>>>>>> less
>>>>>>> useful though. You can also avoid `with` altogether and write the
>>>>>>> helper functions by hand (that's what `with` is doing after all!).
>>>>>>>
>>>>>>> On 2 November 2014 17:14, <mechvel at scico.botik.ru> wrote:
>>>>>>>>
>>>>>>>> People,
>>>>>>>>
>>>>>>>> Having the proof
>>>>>>>>
>>>>>>>> prove : (k∈ks : k ∈ ks) → proj₂ (lookupIf∈ k (p ∷ ps) k∈k':ks) ≡
>>>>>>>> proj₂ (lookupIf∈ k ps k∈ks)
>>>>>>>> prove k∈ks with k ≟ k'
>>>>>>>> --
>>>>>>>> (I)
>>>>>>>>
>>>>>>>> ... | yes k≡k' = ⊥-elim $ k≉k' k≡k'
>>>>>>>> ... | no _ with lookup k ps
>>>>>>>> ... | inj₁ _ = PE.refl
>>>>>>>> ... | inj₂ k∉ks = ⊥-elim $ k∉ks k∈ks
>>>>>>>>
>>>>>>>>
>>>>>>>> (I do not give the complete code),
>>>>>>>>
>>>>>>>> I try to rewrite it in a bit simpler way by joining it into one
>>>>>>>> `with'
>>>>>>>> clause:
>>>>>>>>
>>>>>>>>
>>>>>>>> prove k∈ks with k ≟ k' | lookup k ps
>>>>>>>> --
>>>>>>>> (II)
>>>>>>>>
>>>>>>>> ... | yes k≡k' | _ = ⊥-elim $ k≉k' k≡k'
>>>>>>>> ... | no _ | inj₁ _ = PE.refl
>>>>>>>> ... | no _ | inj₂ k∉ks = ⊥-elim $ k∉ks k∈ks
>>>>>>>>
>>>>>>>>
>>>>>>>> (I) is type-checked, and (II) is not.
>>>>>>>>
>>>>>>>> Is this natural for Agda to decide so?
>>>>>>>>
>>>>>>>> (I have spent 4 hours trying to prove a similar real and evident
>>>>>>>> example.
>>>>>>>> Then tried to split `with' into two, and this has succeeded).
>>>>>>>>
>>>>>>>> Thanks,
>>>>>>>>
>>>>>>>> ------
>>>>>>>> Sergei
>>>>>>>> _______________________________________________
>>>>>>>> Agda mailing list
>>>>>>>> Agda at lists.chalmers.se
>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>
>>>>>>> _______________________________________________
>>>>>>> Agda mailing list
>>>>>>> Agda at lists.chalmers.se
>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>
>>>>>>
>>>>>>
>>>>>> --
>>>>>> Andreas Abel <>< Du bist der geliebte Mensch.
>>>>>>
>>>>>> Department of Computer Science and Engineering
>>>>>> Chalmers and Gothenburg University, Sweden
>>>>>>
>>>>>> andreas.abel at gu.se
>>>>>> http://www2.tcs.ifi.lmu.de/~abel/
>>>>> _______________________________________________
>>>>> Agda mailing list
>>>>> Agda at lists.chalmers.se
>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>>
>>>>
>>>>
>>>> --
>>>> Christopher Jenkins
>>>> Computer Science 2013
>>>> Trinity University
>>
>>
>>
>>
>> --
>> Christopher Jenkins
>> Computer Science 2013
>> Trinity University
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list