[Agda] enigmatic `with'

[Andrea Vezzosi]

If you put a hole in place of "e" and ask for the goal type there
you'll see that some of the "ins" have reduced to something else,
because of the with match, and so the type of "e" is not the goal type
anymore.

You do need the "ins" to reduce in cases like this, otherwise you
would never be able to prove properties about it.

Though it is quite counterintuitive that the effect of "with", as
always, is limited to the current context and goal type: it doesn't
apply to anything in the right hand side of the definition, not even
where clauses.

A possible workaround is to change the type of "e" to the goal type I
mentioned above, modulo things that are not accepted as input like
(baz .. | ..).

Hopefully you can still do a proof of that.

Cheers,
Andrea






On Thu, Jan 1, 2015 at 7:04 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> I need to add the following.
> The signature for   e  needs a blank before  ∷ .
> But
> a) Agda understands this  ∷,  b) inserting a blank does not change the
> report.
>
>
> On Thu, 2015-01-01 at 21:57 +0400, Sergei Meshveliani wrote:
>> People,
>> I have
>>
>>   foo : ∀ k u v ps → ... →
>>         ins (k , v) (ins (k , u) ps)  =pn  ins (k , comb k v u) ps
>>
>>   foo k _ _ []    with k ≟ k
>>   ...                  | yes _  =  =pn-refl
>>   ...                  | no k≉k =  ⊥-elim $ k≉k ≈refl
>>
>>   foo k u v ((k' , w) ∷ ps)  with k ≟ k'
>>   ...
>>       | no k≉k'  =  anything   -- so far
>>   ... | yes k≈k' =  e
>>       where
>>       ...  -- a certain prelude
>>       ...
>>       e : ins (k , v) (ins (k , u) ((k' , w )∷ ps)) =pn
>>           ins (k , comb k v u) ((k' , w) ∷ ps)
>>       e =
>>         begin-pn
>>           ins kv (ins ku (k'w ∷ ps))    =pn[ =pn-reflexive e2 ]
>>           ins kv ((k' , ckuw) ∷ ps)     =pn[ =pn-reflexive e3 ]
>>           (k' , comb k v ckuw) ∷ ps     =pn[ e0 ∷pn =pn-refl ]
>>           (k' , comb k ckvu w) ∷ ps     =pn[ =pn-reflexive $ PE.sym e4 ]
>>           ins (k , ckvu) (k'w ∷ ps)
>>         end-pn
>>
>> 1) `e' itself is type-checked,
>> 2) the signature for  e  is exactly the one required in  foo,
>> 3) Agda-2.4.2.2  reports of a wrong type for  e  in the branch
>>    " yes k≈k' =  e".
>>
>> Why Adga is so? What may be a way out?
>>
>> 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