<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>