[Agda] A sticky refusal
Andrea Vezzosi
sanzhiyan at gmail.com
Sat Aug 15 21:16:16 CEST 2015
Well, you could still work around this by defining a view over _∈_ I
suppose, and pattern match on that.
In this case Agda's unifier could maybe be a bit smarter and do the
eta-expansion of the existential on the fly, but in general there are
always going to be unification constraints that cannot be solved nor
refuted.
However the current situation where Agda cannot cope with a stuck
unification problem could be avoided.
If we get rid of "indexes" and desugar them into parameters+proofs of
equality we could fail more gracefully by exposing such proofs to the
RHS when they cannot be eliminated.
This would also interact better with other notions of propositional
equality, like the ones in OTT or HoTT, because coe/transport could
compute more.
On Sat, Aug 15, 2015 at 8:38 PM, Martin Stone Davis
<martin.stone.davis at gmail.com> wrote:
> 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
> 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
>> >
>
>
More information about the Agda
mailing list