[Agda] A sticky refusal
Martin Stone Davis
martin.stone.davis at gmail.com
Sat Aug 15 20:38:34 CEST 2015
Thanks, that works for my present purposes.
But suppose I had gotten the definition of _∈_ 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 _∈_? Or, in this case, would
you recommend the original author of _∈_ simply be taken out and shot?
Parenthetically, I would like to remark that 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". Should this
be considered a defect in Agda? Or in my way of thinking?
--
Martin Stone Davis
Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
On Sat, Aug 15, 2015 at 4:17 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> Hi Martin,
>
> I'd first split on k∈t so you get less cases, but if you need to match
> on the tree first for other reasons there's still a workaround.
>
> When unification gets stuck during pattern matching you have to change
> the expressions in the indexes to be more unifiable by turning more of
> them into variables, especially those that are not patterns
> themselves.
>
> In this case you want to change the side of the unification that comes
> from the definition of the datatype, the (proj₂ b) is your problem:
>
> data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where
> here : ∀ {hˡ hʳ} V
> {l : Tree lb [ K ] hˡ}
> {r : Tree [ K ] ub hʳ}
> {h : _}
> {b : hˡ ∼ hʳ ⊔ h} →
>
> K ∈ node (K , V) l r b
> left : ∀ {hˡ hʳ K′} {V : Value K′}
> {l : Tree lb [ K′ ] hˡ}
> {r : Tree [ K′ ] ub hʳ}
> {h : _}
> {b : hˡ ∼ hʳ ⊔ h} →
> K < K′ →
> K ∈ l →
> K ∈ node (K′ , V) l r b
> right : ∀ {hˡ hʳ K′} {V : Value K′}
> {l : Tree lb [ K′ ] hˡ}
> {r : Tree [ K′ ] ub hʳ}
> {h : _}
> {b : hˡ ∼ hʳ ⊔ h} →
> K′ < K →
> K ∈ r →
> K ∈ node (K′ , V) l r b
>
> Now you can pattern match. refuse6 still does not go through, but the
> following does
>
> refuse6 : ∀ {kₗ kᵤ h}
> ( t : Tree kₗ kᵤ h )
> ( k : Key )
> ( k∈t : k ∈ t ) →
> Set
> refuse6 (node (k , V) lk ku (∼+ {n = hˡ})) .k (here ._) = { }19
>
> Cheers,
> Andrea
>
>
> On Sat, Aug 15, 2015 at 5:10 AM, Martin Stone Davis
> <martin.stone.davis at gmail.com> wrote:
> > NB Crossposted to http://stackoverflow.com/q/32021121/1312174.
> >
> > This question is about
> >
> > * how to help Agda get unstuck when solving unification problems, and
> > * how to convince Agda to solve a "heterogeneous constraint" (whatever
> that
> > means)
> >
> > The complete code for my question can be found
> > [here](http://lpaste.net/138853). I'll lay out my code and eventually
> get to
> > the question. My project concerns proving things in Data.AVL, so I start
> > with some boilerplate for that:
> >
> > open import Data.Product
> > open import Level
> > open import Relation.Binary
> > open import Relation.Binary.PropositionalEquality as P using (_≡_)
> >
> > module Data.AVL.Properties-Refuse
> > {k v ℓ}
> > {Key : Set k} (Value : Key → Set v)
> > {_<_ : Rel Key ℓ}
> > (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _<_) where
> >
> > open import Data.AVL Value isStrictTotalOrder using (KV; module
> > Extended-key; module Height-invariants; module Indexed)
> > import Data.AVL Value isStrictTotalOrder as AVL
> > open Extended-key
> > open Height-invariants
> > open Indexed
> >
> > open IsStrictTotalOrder isStrictTotalOrder
> >
> > I then borrow [an idea from
> > Vitus](http://stackoverflow.com/a/21083647/1312174) to represent
> membership:
> >
> > data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ)
> > where
> > here : ∀ {hˡ hʳ} V
> > {l : Tree lb [ K ] hˡ}
> > {r : Tree [ K ] ub hʳ}
> > {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
> > K ∈ node (K , V) l r (proj₂ b)
> > left : ∀ {hˡ hʳ K′} {V : Value K′}
> > {l : Tree lb [ K′ ] hˡ}
> > {r : Tree [ K′ ] ub hʳ}
> > {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
> > K < K′ →
> > K ∈ l →
> > K ∈ node (K′ , V) l r (proj₂ b)
> > right : ∀ {hˡ hʳ K′} {V : Value K′}
> > {l : Tree lb [ K′ ] hˡ}
> > {r : Tree [ K′ ] ub hʳ}
> > {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
> > K′ < K →
> > K ∈ r →
> > K ∈ node (K′ , V) l r (proj₂ b)
> >
> > I then declare a function (whose meaning is irrelevant -- this is a
> > contrived and simple version of a more meaningful function not shown
> here):
> >
> > refuse1 : ∀ {kₗ kᵤ h}
> > ( t : Tree kₗ kᵤ h )
> > ( k : Key )
> > ( k∈t : k ∈ t ) →
> > Set
> > refuse1 = {!!}
> >
> > So far, so good. Now, I case split on the default variables:
> >
> > refuse2 : ∀ {kₗ kᵤ h}
> > ( t : Tree kₗ kᵤ h )
> > ( k : Key )
> > ( k∈t : k ∈ t ) →
> > Set
> > refuse2 t k₁ k∈t = {!!}
> >
> > And now I split on `t`:
> >
> > refuse3 : ∀ {kₗ kᵤ h}
> > ( t : Tree kₗ kᵤ h )
> > ( k : Key )
> > ( k∈t : k ∈ t ) →
> > Set
> > refuse3 (leaf l<u) k₁ k∈t = {!!}
> > refuse3 (node k₁ t t₁ bal) k₂ k∈t = {!!}
> >
> > And now on `bal`:
> >
> > refuse4 : ∀ {kₗ kᵤ h}
> > ( t : Tree kₗ kᵤ h )
> > ( k : Key )
> > ( k∈t : k ∈ t ) →
> > Set
> > refuse4 (leaf l<u) k₁ k∈t = {!!}
> > refuse4 (node k₁ t t₁ ∼+) k₂ k∈t = {!!}
> > refuse4 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}
> > refuse4 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}
> >
> > The first error comes when I try to case split on `k∈t` of the equation
> > including `(node ... ∼+)`:
> >
> > refuse5 : ∀ {kₗ kᵤ h}
> > ( t : Tree kₗ kᵤ h )
> > ( k : Key )
> > ( k∈t : k ∈ t ) →
> > Set
> > refuse5 (leaf l<u) k₁ k∈t = {!!}
> > refuse5 (node k₁ t t₁ ∼+) k₂ k∈t = {!k∈t!}
> > {- ERROR
> > I'm not sure if there should be a case for the constructor here,
> > because I get stuck when trying to solve the following
> unification
> > problems (inferred index ≟ expected index):
> > {_} ≟ {_}
> > node (k₅ , V) l r (proj₂ b) ≟ node k₄
> > t₂ t₃ ∼+
> > when checking that the expression ? has type Set
> > -}
> > refuse5 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}
> > refuse5 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}
> >
> > Agda tells me it gets stuck doing the unification, but it's not clear to
> me
> > why or how to help. In [a response to a similar
> > question](http://stackoverflow.com/q/30951993/1312174), Ulf suggested
> first
> > case-splitting on another variable. So, now working by hand, I focus on
> > case-splitting the `∼+` line from `refuse5` and include many of the
> implicit
> > variables:
> >
> > open import Data.Nat.Base as ℕ
> >
> > refuse6 : ∀ {kₗ kᵤ h}
> > ( t : Tree kₗ kᵤ h )
> > ( k : Key )
> > ( k∈t : k ∈ t ) →
> > Set
> > refuse6 {h = ℕ.suc .hˡ}
> > (node (k , V) lk ku (∼+ {n = hˡ}))
> > .k
> > (here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku}
> {b =
> > (ℕ.suc .hˡ , ∼+ {n = .hˡ})}) = {!!}
> > {- ERROR
> > Refuse to solve heterogeneous constraint proj₂ b :
> > n ∼ hʳ ⊔ proj₁ b =?=
> > ∼+ : n ∼ ℕ.suc n ⊔ ℕ.suc n
> > when checking that the pattern
> > here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku}
> > {b = ℕ.suc .hˡ , ∼+ {n = .hˡ}}
> > has type
> > k₂ ∈ node (k₁ , V) lk ku ∼+
> > -}
> > refuse6 _ _ _ = ?
> >
> > Oops. Now Agda goes from complaining that it's stuck to downright
> refusing
> > to solve. What's going on here? Is it possible to specify the lhs of the
> > equations with at least as much detail as in refuse5 **and also** case
> split
> > on `k∈t`? If so, how?
> > --
> > Martin Stone Davis
> >
> > Postal/Residential:
> > 1223 Ferry St
> > Apt 5
> > Eugene, OR 97401
> > Talk / Text / Voicemail: (310) 699-3578
> > Electronic Mail: martin.stone.davis at gmail.com
> > Website: martinstonedavis.com
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150815/9593ac84/attachment-0001.html
More information about the Agda
mailing list