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