<div dir="ltr"><div>Thanks, that works for my present purposes.<br><br>But suppose I had gotten the definition of _<span class="im">∈_ from
someone's library, a lot of code had already been written, and I was now
in the position of trying to prove things about it. I wouldn't be able
to change the definition to make it more compatible with unification.
Would there then still be a way around the problem? Is there any way of
solving the original problem **without** changing the definition of </span><span class="im">_<span class="im">∈_?</span></span><span class="im"> Or, in this case, would you recommend the original author of </span><span class="im">_<span class="im">∈_</span> simply be taken out and shot?<br><br></span></div><div><span class="im">Parenthetically, I would like to remark that</span> <span class="im">I'm surprised. I had assumed that the two definitions were, for all
intents and purposes, equivalent. From the point of view of someone
writing a pattern match on the lhs of an equation, it's simply a matter
of specifying variables in different places. I now learn
that one definition is more "unification-friendly".</span> Should this be considered a defect in Agda? Or in my way of thinking?<br><span class="im"><br></span></div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website:Â </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br><div class="gmail_quote">On Sat, Aug 15, 2015 at 4:17 AM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Martin,<br>
<br>
I'd first split on k∈t so you get less cases, but if you need to match<br>
on the tree first for other reasons there's still a workaround.<br>
<br>
When unification gets stuck during pattern matching you have to change<br>
the expressions in the indexes to be more unifiable by turning more of<br>
them into variables, especially those that are not patterns<br>
themselves.<br>
<br>
In this case you want to change the side of the unification that comes<br>
from the definition of the datatype, the (projâ‚‚ b) is your problem:<br>
<span class=""><br>
 data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where<br>
  here : ∀ {hˡ hʳ} V<br>
   {l : Tree lb [ K ] hˡ}<br>
   {r : Tree [ K ] ub hʳ}<br>
</span>Â Â Â {h : _}<br>
   {b : hˡ ∼ hʳ ⊔ h} →<br>
<br>
   K ∈ node (K , V) l r b<br>
<span class="">  left : ∀ {hˡ hʳ K′} {V : Value K′}<br>
   {l : Tree lb [ K′ ] hˡ}<br>
   {r : Tree [ K′ ] ub hʳ}<br>
</span>Â Â Â {h : _}<br>
   {b : hˡ ∼ hʳ ⊔ h} →<br>
   K < K′ →<br>
   K ∈ l →<br>
   K ∈ node (K′ , V) l r b<br>
<span class="">  right : ∀ {hˡ hʳ K′} {V : Value K′}<br>
   {l : Tree lb [ K′ ] hˡ}<br>
   {r : Tree [ K′ ] ub hʳ}<br>
</span>Â Â Â {h : _}<br>
   {b : hˡ ∼ hʳ ⊔ h} →<br>
   K′ < K →<br>
   K ∈ r →<br>
   K ∈ node (K′ , V) l r b<br>
<br>
Now you can pattern match. refuse6 still does not go through, but the<br>
following does<br>
<span class=""><br>
 refuse6 : ∀ {kₗ kᵤ h}<br>
      ( t : Tree kₗ kᵤ h )<br>
      ( k : Key )<br>
      ( k∈t : k ∈ t ) →<br>
      Set<br>
</span> refuse6 (node (k , V) lk ku (∼+ {n = hˡ})) .k (here ._) = { }19<br>
<br>
Cheers,<br>
Andrea<br>
<div><div class="h5"><br>
<br>
On Sat, Aug 15, 2015 at 5:10 AM, Martin Stone Davis<br>
<<a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a>> wrote:<br>
> NB Crossposted to <a href="http://stackoverflow.com/q/32021121/1312174" rel="noreferrer" target="_blank">http://stackoverflow.com/q/32021121/1312174</a>.<br>
><br>
> This question is about<br>
><br>
> * how to help Agda get unstuck when solving unification problems, and<br>
> * how to convince Agda to solve a "heterogeneous constraint" (whatever that<br>
> means)<br>
><br>
> The complete code for my question can be found<br>
> [here](<a href="http://lpaste.net/138853" rel="noreferrer" target="_blank">http://lpaste.net/138853</a>). I'll lay out my code and eventually get to<br>
> the question. My project concerns proving things in Data.AVL, so I start<br>
> with some boilerplate for that:<br>
><br>
>Â Â Â open import Data.Product<br>
>Â Â Â open import Level<br>
>Â Â Â open import Relation.Binary<br>
>   open import Relation.Binary.PropositionalEquality as P using (_≡_)<br>
><br>
>Â Â Â module Data.AVL.Properties-Refuse<br>
>Â Â Â Â {k v â„“}<br>
>    {Key : Set k} (Value : Key → Set v)<br>
>Â Â Â Â {_<_ : Rel Key â„“}<br>
>    (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _<_) where<br>
><br>
>Â Â Â Â open import Data.AVL Value isStrictTotalOrder using (KV; module<br>
> Extended-key; module Height-invariants; module Indexed)<br>
>Â Â Â Â import Data.AVL Value isStrictTotalOrder as AVL<br>
>Â Â Â Â open Extended-key<br>
>Â Â Â Â open Height-invariants<br>
>Â Â Â Â open Indexed<br>
><br>
>Â Â Â Â open IsStrictTotalOrder isStrictTotalOrder<br>
><br>
> I then borrow [an idea from<br>
> Vitus](<a href="http://stackoverflow.com/a/21083647/1312174" rel="noreferrer" target="_blank">http://stackoverflow.com/a/21083647/1312174</a>) to represent membership:<br>
><br>
>    data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ)<br>
> where<br>
>     here : ∀ {hˡ hʳ} V<br>
>      {l : Tree lb [ K ] hˡ}<br>
>      {r : Tree [ K ] ub hʳ}<br>
>      {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>
>      K ∈ node (K , V) l r (proj₂ b)<br>
>     left : ∀ {hˡ hʳ K′} {V : Value K′}<br>
>      {l : Tree lb [ K′ ] hˡ}<br>
>      {r : Tree [ K′ ] ub hʳ}<br>
>      {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>
>      K < K′ →<br>
>      K ∈ l →<br>
>      K ∈ node (K′ , V) l r (proj₂ b)<br>
>     right : ∀ {hˡ hʳ K′} {V : Value K′}<br>
>      {l : Tree lb [ K′ ] hˡ}<br>
>      {r : Tree [ K′ ] ub hʳ}<br>
>      {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>
>      K′ < K →<br>
>      K ∈ r →<br>
>      K ∈ node (K′ , V) l r (proj₂ b)<br>
><br>
> I then declare a function (whose meaning is irrelevant -- this is a<br>
> contrived and simple version of a more meaningful function not shown here):<br>
><br>
>    refuse1 : ∀ {kₗ kᵤ h}<br>
>         ( t : Tree kₗ kᵤ h )<br>
>Â Â Â Â Â Â Â Â Â ( k : Key )<br>
>         ( k∈t : k ∈ t ) →<br>
>Â Â Â Â Â Â Â Â Â Set<br>
>Â Â Â Â refuse1 = {!!}<br>
><br>
> So far, so good. Now, I case split on the default variables:<br>
><br>
>    refuse2 : ∀ {kₗ kᵤ h}<br>
>         ( t : Tree kₗ kᵤ h )<br>
>Â Â Â Â Â Â Â Â Â ( k : Key )<br>
>         ( k∈t : k ∈ t ) →<br>
>Â Â Â Â Â Â Â Â Â Set<br>
>    refuse2 t k₠k∈t = {!!}<br>
><br>
> And now I split on `t`:<br>
><br>
>    refuse3 : ∀ {kₗ kᵤ h}<br>
>         ( t : Tree kₗ kᵤ h )<br>
>Â Â Â Â Â Â Â Â Â ( k : Key )<br>
>         ( k∈t : k ∈ t ) →<br>
>Â Â Â Â Â Â Â Â Â Set<br>
>    refuse3 (leaf l<u) k₠k∈t = {!!}<br>
>    refuse3 (node k₠t t₠bal) k₂ k∈t = {!!}<br>
><br>
> And now on `bal`:<br>
><br>
>    refuse4 : ∀ {kₗ kᵤ h}<br>
>         ( t : Tree kₗ kᵤ h )<br>
>Â Â Â Â Â Â Â Â Â ( k : Key )<br>
>         ( k∈t : k ∈ t ) →<br>
>Â Â Â Â Â Â Â Â Â Set<br>
>    refuse4 (leaf l<u) k₠k∈t = {!!}<br>
>    refuse4 (node k₠t t₠∼+) k₂ k∈t = {!!}<br>
>    refuse4 (node k₠t t₠∼0) k₂ k∈t = {!!}<br>
>    refuse4 (node k₠t t₠∼-) k₂ k∈t = {!!}<br>
><br>
> The first error comes when I try to case split on `k∈t` of the equation<br>
> including `(node ... ∼+)`:<br>
><br>
>    refuse5 : ∀ {kₗ kᵤ h}<br>
>         ( t : Tree kₗ kᵤ h )<br>
>Â Â Â Â Â Â Â Â Â ( k : Key )<br>
>         ( k∈t : k ∈ t ) →<br>
>Â Â Â Â Â Â Â Â Â Set<br>
>    refuse5 (leaf l<u) k₠k∈t = {!!}<br>
>    refuse5 (node k₠t t₠∼+) k₂ k∈t = {!k∈t!}<br>
>Â Â Â Â {- ERROR<br>
>Â Â Â Â Â I'm not sure if there should be a case for the constructor here,<br>
>Â Â Â Â Â because I get stuck when trying to solve the following unification<br>
>     problems (inferred index ≟ expected index):<br>
>      {_} ≟ {_}<br>
>      node (k₅ , V) l r (proj₂ b) ≟ node k₄<br>
>                     t₂ t₃ ∼+<br>
>Â Â Â Â Â when checking that the expression ? has type Set<br>
>Â Â Â Â -}<br>
>    refuse5 (node k₠t t₠∼0) k₂ k∈t = {!!}<br>
>    refuse5 (node k₠t t₠∼-) k₂ k∈t = {!!}<br>
><br>
> Agda tells me it gets stuck doing the unification, but it's not clear to me<br>
> why or how to help. In [a response to a similar<br>
> question](<a href="http://stackoverflow.com/q/30951993/1312174" rel="noreferrer" target="_blank">http://stackoverflow.com/q/30951993/1312174</a>), Ulf suggested first<br>
> case-splitting on another variable. So, now working by hand, I focus on<br>
> case-splitting the `∼+` line from `refuse5` and include many of the implicit<br>
> variables:<br>
><br>
>Â Â Â Â open import Data.Nat.Base as â„•<br>
><br>
>    refuse6 : ∀ {kₗ kᵤ h}<br>
>         ( t : Tree kₗ kᵤ h )<br>
>Â Â Â Â Â Â Â Â Â ( k : Key )<br>
>         ( k∈t : k ∈ t ) →<br>
>Â Â Â Â Â Â Â Â Â Set<br>
>    refuse6 {h = ℕ.suc .hˡ}<br>
>        (node (k , V) lk ku (∼+ {n = hˡ}))<br>
>Â Â Â Â Â Â Â Â .k<br>
>        (here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku} {b =<br>
> (ℕ.suc .hˡ , ∼+ {n = .hˡ})}) = {!!}<br>
>Â Â Â Â {- ERROR<br>
>Â Â Â Â Â Refuse to solve heterogeneous constraint projâ‚‚ b :<br>
>     n ∼ hʳ ⊔ proj₠b =?=<br>
>     ∼+ : n ∼ ℕ.suc n ⊔ ℕ.suc n<br>
>Â Â Â Â Â when checking that the pattern<br>
>     here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku}<br>
>      {b = ℕ.suc .hˡ , ∼+ {n = .hˡ}}<br>
>Â Â Â Â Â has type<br>
>     k₂ ∈ node (k₠, V) lk ku ∼+<br>
>Â Â Â Â -}<br>
>Â Â Â Â refuse6 _ _ _ = ?<br>
><br>
> Oops. Now Agda goes from complaining that it's stuck to downright refusing<br>
> to solve. What's going on here? Is it possible to specify the lhs of the<br>
> equations with at least as much detail as in refuse5 **and also** case split<br>
> on `k∈t`? If so, how?<br>
> --<br>
> Martin Stone Davis<br>
><br>
> Postal/Residential:<br>
> 1223 Ferry St<br>
> Apt 5<br>
> Eugene, OR 97401<br>
> Talk / Text / Voicemail: <a href="tel:%28310%29%20699-3578" value="+13106993578">(310) 699-3578</a><br>
> Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a><br>
> Website: <a href="http://martinstonedavis.com" rel="noreferrer" target="_blank">martinstonedavis.com</a><br>
><br>
</div></div>> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
</blockquote></div><br></div>