[Agda] Why disallow case splits that involve impossible unification

[James Wood]

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