agda
Add Case Bash Tactic
Patch Description
This PR adds the case-bash! tactic, which automates the process of performing exhaustive case splits followed by refl.
This is best demonstrated with, well, a demo!
∧-comm : ∀ (x y : Bool) → x ∧ y ≡ y ∧ x
∧-comm = case-bash!
Details
The tactic begins by inspecting the current goal, which should be some pi type with a bunch of arguments that are non-implicit datatypes. It then walks down the pi type, hunting for visible datatype arguments. When we find one, grab all of it's constructor names, and push them onto a list that stores all possible constructor name combinations. This list is then used to generate a list of clauses whose bodies are all refl, which are finally used to construct a pattern lambda.
Limitations
This tactic is extremely brute force; it will case split on any datatype it finds, even if it doesn't show up in the goal whatsoever. Furthermore, it is not smart enough to insert absurd clauses, and thus will run straight into a type error when presented with indexed datatypes. Detecting when we need to insert absurd clauses is quite difficult though, and a tactic with limitations is better than no tactic at all.
Thanks, this looks really nice! And I agree, better basic tactics than non at all!
I know the code is already extremely well documented but can we add some examples of using it in README.Tactics.CaseBash? That way they'll function as tests as well to avoid us accidentally breaking this in future :+1:
Also unfortunately the tests appear to be failing with a parse error. What version of Agda are you using?
Also unfortunately the tests appear to be failing with a parse error. What version of Agda are you using?
Is this not due to the fact that I have retired return in favour of pure because
return used to clash with case_return_of_?
Edit: pushed a fix, there was also a discrepancy in the type of extendContext so there's
probably indeed an Agda version issue too.
Should we have a README with examples?
Sorry! I've been a bit busy this week so I hadn't been keeping an eye on this.
I did develop this against Agda HEAD and on experimental, which explains all of the silly mistakes 🙃.
I'll add a README later tonight, and then we should be good to go!
@TOTBWF any chance of that README appearing at some point so I can merge this in?
I was working on the README and found a couple of gnarly scoping bugs, currently working on fixing them!
If not, could you push the README file as is, and comment out the buggy examples with explanations?
Sorry, this fell off my radar for a bit: I'll refresh myself on the details tomorrow
Tried to add a README file to this, and have found that it has bit rotted massively... I now get the following error:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Unquote.hs:509:79 in Agda-2.6.4-e6510447f87a1a26375f0a932139120d3050d11d5f869249fbd6acc3a8abb596:Agda.TypeChecking.Unquote
It seems such a shame but I think I might be closing this next week unless we hear from @TOTBWF.