<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&#39;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&#39;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&#39;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&#39;s simply a matter 
of specifying variables in different places. I now learn 
that one definition is more &quot;unification-friendly&quot;.</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">&lt;<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>&gt;</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&#39;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&#39;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 &lt; 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′ &lt; 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>
&lt;<a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a>&gt; wrote:<br>
&gt; NB Crossposted to <a href="http://stackoverflow.com/q/32021121/1312174" rel="noreferrer" target="_blank">http://stackoverflow.com/q/32021121/1312174</a>.<br>
&gt;<br>
&gt; This question is about<br>
&gt;<br>
&gt; * how to help Agda get unstuck when solving unification problems, and<br>
&gt; * how to convince Agda to solve a &quot;heterogeneous constraint&quot; (whatever that<br>
&gt; means)<br>
&gt;<br>
&gt; The complete code for my question can be found<br>
&gt; [here](<a href="http://lpaste.net/138853" rel="noreferrer" target="_blank">http://lpaste.net/138853</a>). I&#39;ll lay out my code and eventually get to<br>
&gt; the question. My project concerns proving things in Data.AVL, so I start<br>
&gt; with some boilerplate for that:<br>
&gt;<br>
&gt;     open import Data.Product<br>
&gt;     open import Level<br>
&gt;     open import Relation.Binary<br>
&gt;     open import Relation.Binary.PropositionalEquality as P using (_≡_)<br>
&gt;<br>
&gt;     module Data.AVL.Properties-Refuse<br>
&gt;       {k v ℓ}<br>
&gt;       {Key : Set k} (Value : Key → Set v)<br>
&gt;       {_&lt;_ : Rel Key ℓ}<br>
&gt;       (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _&lt;_) where<br>
&gt;<br>
&gt;       open import Data.AVL Value isStrictTotalOrder using (KV; module<br>
&gt; Extended-key; module Height-invariants; module Indexed)<br>
&gt;       import Data.AVL Value isStrictTotalOrder as AVL<br>
&gt;       open Extended-key<br>
&gt;       open Height-invariants<br>
&gt;       open Indexed<br>
&gt;<br>
&gt;       open IsStrictTotalOrder isStrictTotalOrder<br>
&gt;<br>
&gt; I then borrow [an idea from<br>
&gt; Vitus](<a href="http://stackoverflow.com/a/21083647/1312174" rel="noreferrer" target="_blank">http://stackoverflow.com/a/21083647/1312174</a>) to represent membership:<br>
&gt;<br>
&gt;       data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ)<br>
&gt; where<br>
&gt;         here : ∀ {hˡ hʳ} V<br>
&gt;           {l : Tree lb [ K ] hˡ}<br>
&gt;           {r : Tree [ K ] ub hʳ}<br>
&gt;           {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>
&gt;           K ∈ node (K , V) l r (proj₂ b)<br>
&gt;         left : ∀ {hˡ hʳ K′} {V : Value K′}<br>
&gt;           {l : Tree lb [ K′ ] hˡ}<br>
&gt;           {r : Tree [ K′ ] ub hʳ}<br>
&gt;           {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>
&gt;           K &lt; K′ →<br>
&gt;           K ∈ l →<br>
&gt;           K ∈ node (K′ , V) l r (proj₂ b)<br>
&gt;         right : ∀ {hˡ hʳ K′} {V : Value K′}<br>
&gt;           {l : Tree lb [ K′ ] hˡ}<br>
&gt;           {r : Tree [ K′ ] ub hʳ}<br>
&gt;           {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>
&gt;           K′ &lt; K →<br>
&gt;           K ∈ r →<br>
&gt;           K ∈ node (K′ , V) l r (proj₂ b)<br>
&gt;<br>
&gt; I then declare a function (whose meaning is irrelevant -- this is a<br>
&gt; contrived and simple version of a more meaningful function not shown here):<br>
&gt;<br>
&gt;       refuse1 : ∀ {kₗ kᵤ h}<br>
&gt;                 ( t : Tree kₗ kᵤ h )<br>
&gt;                 ( k : Key )<br>
&gt;                 ( k∈t : k ∈ t ) →<br>
&gt;                 Set<br>
&gt;       refuse1 = {!!}<br>
&gt;<br>
&gt; So far, so good. Now, I case split on the default variables:<br>
&gt;<br>
&gt;       refuse2 : ∀ {kₗ kᵤ h}<br>
&gt;                 ( t : Tree kₗ kᵤ h )<br>
&gt;                 ( k : Key )<br>
&gt;                 ( k∈t : k ∈ t ) →<br>
&gt;                 Set<br>
&gt;       refuse2 t k₁ k∈t = {!!}<br>
&gt;<br>
&gt; And now I split on `t`:<br>
&gt;<br>
&gt;       refuse3 : ∀ {kₗ kᵤ h}<br>
&gt;                 ( t : Tree kₗ kᵤ h )<br>
&gt;                 ( k : Key )<br>
&gt;                 ( k∈t : k ∈ t ) →<br>
&gt;                 Set<br>
&gt;       refuse3 (leaf l&lt;u) k₁ k∈t = {!!}<br>
&gt;       refuse3 (node k₁ t t₁ bal) k₂ k∈t = {!!}<br>
&gt;<br>
&gt; And now on `bal`:<br>
&gt;<br>
&gt;       refuse4 : ∀ {kₗ kᵤ h}<br>
&gt;                 ( t : Tree kₗ kᵤ h )<br>
&gt;                 ( k : Key )<br>
&gt;                 ( k∈t : k ∈ t ) →<br>
&gt;                 Set<br>
&gt;       refuse4 (leaf l&lt;u) k₁ k∈t = {!!}<br>
&gt;       refuse4 (node k₁ t t₁ ∼+) k₂ k∈t = {!!}<br>
&gt;       refuse4 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}<br>
&gt;       refuse4 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}<br>
&gt;<br>
&gt; The first error comes when I try to case split on `k∈t` of the equation<br>
&gt; including `(node ... ∼+)`:<br>
&gt;<br>
&gt;       refuse5 : ∀ {kₗ kᵤ h}<br>
&gt;                 ( t : Tree kₗ kᵤ h )<br>
&gt;                 ( k : Key )<br>
&gt;                 ( k∈t : k ∈ t ) →<br>
&gt;                 Set<br>
&gt;       refuse5 (leaf l&lt;u) k₁ k∈t = {!!}<br>
&gt;       refuse5 (node k₁ t t₁ ∼+) k₂ k∈t = {!k∈t!}<br>
&gt;       {- ERROR<br>
&gt;         I&#39;m not sure if there should be a case for the constructor here,<br>
&gt;         because I get stuck when trying to solve the following unification<br>
&gt;         problems (inferred index ≟ expected index):<br>
&gt;           {_} ≟ {_}<br>
&gt;           node (k₅ , V) l r (proj₂ b) ≟ node k₄<br>
&gt;                                         t₂ t₃ ∼+<br>
&gt;         when checking that the expression ? has type Set<br>
&gt;       -}<br>
&gt;       refuse5 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}<br>
&gt;       refuse5 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}<br>
&gt;<br>
&gt; Agda tells me it gets stuck doing the unification, but it&#39;s not clear to me<br>
&gt; why or how to help. In [a response to a similar<br>
&gt; question](<a href="http://stackoverflow.com/q/30951993/1312174" rel="noreferrer" target="_blank">http://stackoverflow.com/q/30951993/1312174</a>), Ulf suggested first<br>
&gt; case-splitting on another variable. So, now working by hand, I focus on<br>
&gt; case-splitting the `∼+` line from `refuse5` and include many of the implicit<br>
&gt; variables:<br>
&gt;<br>
&gt;       open import Data.Nat.Base as ℕ<br>
&gt;<br>
&gt;       refuse6 : ∀ {kₗ kᵤ h}<br>
&gt;                 ( t : Tree kₗ kᵤ h )<br>
&gt;                 ( k : Key )<br>
&gt;                 ( k∈t : k ∈ t ) →<br>
&gt;                 Set<br>
&gt;       refuse6 {h = ℕ.suc .hˡ}<br>
&gt;               (node (k , V) lk ku (∼+ {n = hˡ}))<br>
&gt;               .k<br>
&gt;               (here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku} {b =<br>
&gt; (ℕ.suc .hˡ , ∼+ {n = .hˡ})}) = {!!}<br>
&gt;       {- ERROR<br>
&gt;         Refuse to solve heterogeneous constraint proj₂ b :<br>
&gt;         n ∼ hʳ ⊔ proj₁ b =?=<br>
&gt;         ∼+ : n ∼ ℕ.suc n ⊔ ℕ.suc n<br>
&gt;         when checking that the pattern<br>
&gt;         here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku}<br>
&gt;           {b = ℕ.suc .hˡ , ∼+ {n = .hˡ}}<br>
&gt;         has type<br>
&gt;         k₂ ∈ node (k₁ , V) lk ku ∼+<br>
&gt;       -}<br>
&gt;       refuse6 _ _ _ = ?<br>
&gt;<br>
&gt; Oops. Now Agda goes from complaining that it&#39;s stuck to downright refusing<br>
&gt; to solve. What&#39;s going on here? Is it possible to specify the lhs of the<br>
&gt; equations with at least as much detail as in refuse5 **and also** case split<br>
&gt; on `k∈t`? If so, how?<br>
&gt; --<br>
&gt; Martin Stone Davis<br>
&gt;<br>
&gt; Postal/Residential:<br>
&gt; 1223 Ferry St<br>
&gt; Apt 5<br>
&gt; Eugene, OR 97401<br>
&gt; Talk / Text / Voicemail: <a href="tel:%28310%29%20699-3578" value="+13106993578">(310) 699-3578</a><br>
&gt; Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a><br>
&gt; Website: <a href="http://martinstonedavis.com" rel="noreferrer" target="_blank">martinstonedavis.com</a><br>
&gt;<br>
</div></div>&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
</blockquote></div><br></div>