fix: use dsimp to remove abstraction overhead of our parsing stage

[tobiasgrosser]

Our current approach, 'change_mlir_context', does this by forcing reduction but does not reach certain subproofs in the goal. As a result, we currently have three failing test cases. By using dsimp to remove abstraction overhead from the goal, these abstractions are known to be removed everywhere. While there remains a risk that we miss certain simp lemmas, these can be added as a need arises. @alexkeizer also works on an alternative approach (#247) which might supersede this PR in the future.

Interestingly, our alive_case_bash tactic an introduce multiple goals which not always can be closed in AliveStatements. Hence, we add for now a set of two try sorry to cover this case. This should be investigate further in subsequent PRs.

[tobiasgrosser]

I feel #226 will be useful to debug this test case further. Waiting until it is merged.

[alexkeizer]

@bollu and I were talking about this, and we are going to explore some alternative setups, probably some mix of simpprocs and custom meta-code, that is hopefully more robust.
Endlessly polishing the simp-sets feels like a bit of of a waste of time, given that our automation tends to break in inscrutable ways whenever we so much as sneeze near them.

Then again, if your happiness/sanity points can tolerate dealing with this mess: don't let me discourage you

[tobiasgrosser]

Endlessly polishing the simp-sets feels like a bit of a waste of time, given that our automation tends to break in inscrutable ways whenever we so much as sneeze near them.

Who said that things are broken because of simp-sets being wrong? This test case seems to be independent of the simp sets. I carefully debugged this and it seems this is more likely a lean bug, than a bug in the simp sets. That might be worth discussing, before you go ahead and implement a pile of meta-code. I feel we should first reduce the bug before building solutions to an unclear problem. I am happy to do the reduction.

[alexkeizer]

I'm not saying the simp set is wrong, this kind of error is frustrating exactly because we do have a simp-lemma that should have rewritten the goal, but hasn't.

This also isn't the first time we've had this kind of issue. We've run into Valuation.snoc V (toSnoc v) not simplifying before. That time, the bug was caused by the fact that the type of V was something like [.bitvec (.mvar 0), .bitvec (.mvar 0), ...].map <meta-var instantation code>, which is def-eq to [.bitvec <concrete-width>, .bitvec <concrete-width>], but simp apparently wasn't able to see this.
That is why we now have change_mlir_context, to first reduce the context in the type of the valuation.

It would be nice to know what is causing the current issue we have, and even more amazing if it can be fixed upstream, but I think that regardless, it makes a lot of sense to find a more robust solution. For example, we can have a simp-proc that matches an application of Valuation.toSnoc more loosely, and then tries the different possible rewrites we have a bit more aggressively. I suspect that will solve the issue we are seeing here, and hopefully save us from seeing yet another variation of it in the future.

I am happy to do the reduction.

Great! I wasn't suggesting you shouldn't, just wanted to make you aware of some thoughts we were having

[alexkeizer]

Suggested change

	stmt += " := by\n simp_alive_undef\n simp_alive_ops\n simp_alive_case_bash\n try alive_auto\n try sorry\n try sorry"
	stmt += " := by\n simp_alive_undef\n simp_alive_ops\n simp_alive_case_bash\n try alive_auto\n all_goals sorry"

I think all_goals should already be fine with the case of 0 goals, otherwise we might want all_goals (try sorry) or some variation thereof

[alexkeizer]

I still feel that mvar instantiation should never escape the elaborator. But, since #247 is at the moment still broken, let's merge this PR. Once the alternative does go through, we can deprecate this simp_alive_meta tactic