It's just that I have a bunch of equalities x = a in my context where a is probably neutral but also x = a, x = b is a possible context, and I can't figure out how to decide a = b, if it is decideable at all
It should be since they're all just neutrals and no substitution is going on but my mental search engine isn't giving me any results for strategies

If it weren't for the fact that lambdas and case expressions can be neutral this would be the theory of uninterpreted functions with equality and I could just stick the whole thing in an SMT solver

It should be possible to commute case expressions

case of (case of a as ... b ...) as ... b' ...
= case of a as ... (case of b as ... b' ...)

Then a case expression would never be a neutral that gets stuck into the context equated to a variable

Although any propositional equality (x = a) gets stuck into the context and a could definitely be a case expression
That's very annoying

I think I will turn case expressions (case a of ...) into ((\case of ...) a) and then treat \case as a value
Then everything is either a constant or an application and it's now the theory of uninterpreted functions

https://hackage.haskell.org/package/EqualitySolver-0.1.0.2/docs/EqualitySolver-Solver.html
drat I need fixed arities for my functions
I don't necessarily have that information
Like if I have f = g a, h = f b, then h = g a b should hold, but I don't know that g is a two place function?

oh nooo I don't have constructor injectivity. UGH fine I'll oppen the nelson

Does SMT have a "theory of uninterpreted functions some of which are definitely injectivity"

I'm looking at Haskell's SBV and I can't tell how to add an equality between uninterpreted function applications lol

Oh it's a Haskell function
Well that's interesting

I'm still not sure what to do about binders
It seems unsatisfactory that I treat values as opaque
For instance if I end up with \x. a = \x. b, I would like to additionally assert that forall x, a = b
Same with (x: A) -> B, and if A -> B = A' -> B' then A = A' and B = B'
The problem with binders is that they can only be instantiated by non-value neutrals? Otherwise substituting x = \y. c might reduce after all

No you're right. I shouldn't mess with values. I think the solution would be let the user say they would like to prove \x. a = \y. b, find such an equation by magic, then let the user use this propositional equality to proceed

I'm unsure if pi-forall could prove constructor injectivity (I will have to try), but if you end up with an inductive X: * -> * and X A = X B and you want to show A = B I don't think that should be possible
Don't do that

lmao I've forgotten how to prove injectivity

oh. I congrue by projection

I think I have a good idea of how I want to implement this, I'm going to be turning the AST itself into uninterpreted functions and constants and terms with binders into lambda terms, which for some reason is possible with SMT. But I promise not to do it today I promise I will go outside for my health and wellbeing

@ionchy maybe you could pass stuff into the solver as `app(app(g,a),b)` etc so everything has arity 0 except for Syntax Stuff..?

@niss smort

@ionchy congrue: to do with grues

@chrisamaphone @ionchy strongly suggests the existence of progrue

@niss ooh that sounds like that night be it. I'll just convert values (and... neutral case expressions...) into opaque "constants" and then opp a nelson

@ionchy @niss Is this a possible siituation: x = (a, b), y = fst x?

@andrejbauer @niss no, there's a step that does reduction as far as possible first, so before fst y enters my context it gets reduced fst y -> fst (a, b) -> a, and then x = a gets added if a no longer reduces further

@ionchy @niss It sounds like you want to perform simple unification (maybe there are some complications regarding dependent types).