[Agda] Why disallow case splits that involve impossible unification

[James Smith]

Thank you, this is a helpful perspective.

w.r.t. being unable to pattern match on q : f n ≡ suc m, after posting I
was thinking about whether K/UIP would allow you simply decide it's refl,
and without K the RHS could be required to be proof irrelevant on q. But
the point about inspect and working with relations is well taken.

On Wed, Aug 11, 2021 at 12:59 AM James Wood <james.wood.100 at strath.ac.uk>
wrote:

>  > If the split were allowed instead, I could even imagine somehow getting
>  > to use f n ≡ ... on the right , something akin to a with_in_.
>
> One way to see this is that `with_in_` (AKA the inspect idiom) is just
> the syntax for this style of pattern matching. If you are to have a new
> assumption introduced by pattern matching, you also need the syntax to
> give it a name. Perhaps an improvement to interactive editing would be
> to automatically generate uses of the inspect idiom from a proposed
> pattern match.
>
> Still, there's a fundamental problem that persists even when we turn
> undetermined unification problems into propositional equations: if you
> get a variable `q : f n ≡ suc m`, it is still impossible to
> pattern-match on it for the same reason as before. The reason the
> technique of using relations rather than functions exists is because
> it's easier to work with relations fitting the shape of the problem than
> equations, subst, injectivity lemmas, &c.
>
> James
>
> On 11/08/2021 01:04, James Smith wrote:
> > CAUTION: This email originated outside the University. Check before
> > clicking links or attachments.
> > This is probably a dumb beginner question. Out of curiosity, I'm trying
> > to understand the "why" of the "I'm not sure if there should be a case
> > for the constructor" error.
> >
> > I found https://doisinkidney.com/posts/2018-09-20-agda-tips.html
> > <https://doisinkidney.com/posts/2018-09-20-agda-tips.html
> > and "How to Keep Your Neighbors In Order" which give the "what" of the
> > end-user solution, which seems to be to express desired relations purely
> > in datatype constructions/proofs rather than use functions. For example,
> > instead of:
> >
> > ...→ c {Δ₁} {Δ₂} (Δ₁ ++ Δ₂)
> >
> > prefer:
> >
> > ...→ c {Δ₁} {Δ₂} {Δ} (Appending Δ₁ Δ₂ Δ)
> >
> > I also found this passage from Ulf Norell's thesis
> > (http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf
> > <http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf
> > p.33–35) which I think is referring to this same issue: "If A = suc n 􏰂
> > suc m then the leqZero constructor cannot be used to construct an
> > element of A, so splitting only generates a single new context where x
> > has been instantiated with an application of leqSuc. If, on the other
> > hand, A = f n 􏰂 m for some defined function f we cannot tell which
> > constructors are legal and so splitting along x is not possible." ...
> > "In some cases it might be possible to tell, but rather than resorting
> > to complicated heuristics we chose the simpler approach of refusing to
> > split."
> >
> > Small example:
> >
> > open import Data.Nat
> >
> > postulate f : ℕ → ℕ
> >
> > data Ex : ℕ → Set where
> >    c : {n : ℕ} → Ex (f n)
> >
> > g : ∀ {A} → Ex A → ℕ
> > g {zero} ex = { }0
> > g {suc A} ex = { }1
> >
> > Case-split on ex gives the "I'm not sure..." with the unifier stuck on f
> > n ≟ zero orf n ≟ suc A₁.
> >
> > What goes wrong if I were allowed to split on ex to get (c {n})?  I can
> > see that I might be forced to write code to handle some impossible
> > cases, e.g. if f was equivalent to suc, I could be forced to either
> > extrinsically prove the zero case is impossible, or write some useless
> > code.
> >
> > If the split were allowed instead, I could even imagine somehow getting
> > to use f n ≡ ... on the right , something akin to a with_in_.
> >
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
> _______________________________________________
> 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/20210811/123b0c63/attachment.html>