[Agda] struggling `with'

[Andrea Vezzosi]

It's really hard to see what's going on without being able to load the
code, and with a lot of it omitted.

We need at least the definition of "ins" and the original type of
"foo", then we might be able to figure out a better type for the two
alternatives, so that the splitting on (k ≟ k') only needs to be done
once.

Cheers,
Andrea


On Fri, Jan 2, 2015 at 2:40 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> People,
> After two days struggle against `with' in my example, I find the
> following way out:
>
>  ---------------------------------------------------------
>  foo ... =  prove (k ≟ k')
>    where
>    ...
>    case≈ : k ≈ k' →
>                ins kv (ins ku (k'w ∷ ps)) =pn ins (k , ckvu) (k'w ∷ ps)
>    case≈ k≈k' =
>       begin-pn
>         ins kv (ins ku (k'w ∷ ps))   =pn[ =pn-reflexive $
>                                           PE.cong (ins kv) e1 ]
>         ins kv ((k' , ckuw) ∷ ps)    =pn[ =pn-reflexive e2 ]
>         (k' , comb k v ckuw) ∷ ps    =pn[ e0 ∷pn =pn-refl ]
>         (k' , comb k ckvu w) ∷ ps    =pn[ =pn-reflexive $ PE.sym e3 ]
>         ins (k , ckvu) (k'w ∷ ps)
>       end-pn
>       where
>       e0 : (k' , comb k v ckuw) =p (k' , comb k ckvu w)
>       e0 = (≈refl , sym-assoc-comb)
>
>       e1 :  ins ku ((k' , w) ∷ ps) ≡ (k' , ckuw) ∷ ps
>       e1 with k ≟ k'
>       ... | yes _   = PE.refl
>       ... | no k≉k' = ⊥-elim $ k≉k' k≈k'
>
>       e2 :  ins kv ((k' , ckuw) ∷ ps) ≡ (k' , comb k v ckuw) ∷ ps
>       e2 with k ≟ k'
>       ... | yes _   = PE.refl
>       ... | no k≉k' = ⊥-elim $ k≉k' k≈k'
>
>       e3 :  k'w ∷ (ins (k , ckvu) ps) ≡ ins (k , ckvu) (k'w ∷ ps)
>       e3 with k ≟ k'
>       ... | no _     = PE.refl
>       ... | yes k≈k' = ⊥-elim $ k≉k' k≈k'
>
>    ------------------------------------------------
>    case≉ : ¬ k ≈ k' →
>            ins kv (ins ku (k'w ∷ ps))  =pn  ins (k , ckvu) (k'w ∷ ps)
>    case≉ k≉k' = ...
>                 -- a similar junk
>
>    ------------------------------------------------
>    prove : Dec (k ≈ k') → ins kv (ins ku (k'w ∷ ps)) =pn
>                           ins (k , comb k v u) (k'w ∷ ps)
>    prove (no k≉k')  = case≉ k≉k'
>    prove (yes k≈k') = case≈ k≈k'
>  ----------------------------------------------------------------------
>
>
> The code is type-checked, but looks ugly.
> For example,  e1, e2, e3  have the same implementation
> (each of them stupidly asking "k ≟ k'" despite that k≈k' is ready).
>
> I expected that  "with k ≟ k'"  needs to be asked not more than once in
> case≈. But I fail to arrange this.
> For example,
>
>    e00 :  ins kv (ins ku (k'w ∷ ps)) ≡ (k' , comb k v ckuw) ∷ ps
>    e00  with k ≟ k'
>    ... | yes _   = PE.refl
>    ... | no k≉k' = ⊥-elim $ k≉k' k≈k'
>
> presents the two steps of normalization for `ins' ('ins' is applied
> twice in the LHS, and its implmentation asks "k ≟ k'"),
> and the value  (k' , comb k v ckuw) ∷ ps
> is the normal form.
>
> But Agda-2.4.2.2 does not see this, and rejects this proof.
> To prove e00, I need to split it to the two equations, and to apply
> "with k ≟ k'"  for each equation.
>
> Can the goal be written in a nicer way?
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda