feat: heterogeneous noConfusion #11474
Conversation
|
!radar |
|
Benchmark results for 19a08bb against 5bd331e are in! @nomeata Minor changes (1)
|
| where `x1 x2 x3` and `x1' x2' x3'` are the fields of a constructor application of `ctorName`, | ||
| omitting equalities between propositions and using `HEq` where needed. | ||
| -/ | ||
| def mkNoConfusionCtorArg (ctorName : Name) (P : Expr) : MetaM Expr := do |
There was a problem hiding this comment.
Not necessarily related to this change, but this function is always used with beta directly after it, so why produce a lambda at all?
There was a problem hiding this comment.
So just passing in concrete xs, fs1, fs2 and skipping the forallBoundedTelescope isn't a good idea, probably because of this commit:
-- We bring the constructor's parameters into scope abstractly, this way
-- we can check if we need to use HEq. (The concrete fields could allow Eq)
Of course I could move the .beta into mkNoConfusionCtorArg, but it’s a private function, so not worth the bother.
Maybe this was only strictly needed before the present change? Anyways, feels safer this way.
There was a problem hiding this comment.
I mean we could at least do t.replaceFVars instead of mkLambdaFVars + beta. Anyways, I feel like this is in general a bit hacky, couldn't you just check hasLooseBVars on the forall domain? So to be precise we could start with let ctorType := instantiateForall ctorInfo.type params and then peel away the forall layers while deciding on Eq vs HEq using hasLooseBVars.
There was a problem hiding this comment.
Feel free to try and see if the resulting code is more elegant.
There was a problem hiding this comment.
And while you are at it, maybe you can come up with prettier tactic-free code for mkEqNDRecTelescope
github-actions
bot
added
the
toolchain-available
|
Reference manual CI status:
|
leanprover-community-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
builds-mathlib
This PR generalizes the `noConfusion` constructions to heterogeneous equalities (assuming propositional equalities between the indices). This lays ground work for better support for applying injection to heterogeneous equalities in grind. The `Meta.mkNoConfusion` app builder shields most of the code from these changes. Since the per-constructor noConfusion principles are now more expressive, `Meta.mkNoConfusion` no longer uses the general one. In `Init.Prelude` some proofs are more pedestrian because `injection` now needs a bit more machinery. This is a breaking change for whoever uses the `noConfusion` principle manually and explicitly for a type with indices. Fixes #11450.
This PR generalizes the
noConfusionconstructions to heterogeneous equalities (assuming propositional equalities between the indices). This lays ground work for better support for applying injection to heterogeneous equalities in grind.The
Meta.mkNoConfusionapp builder shields most of the code from these changes.Since the per-constructor noConfusion principles are now more expressive,
Meta.mkNoConfusionno longer uses the general one.In
Init.Preludesome proofs are more pedestrian becauseinjectionnow needs a bit more machinery.This is a breaking change for whoever uses the
noConfusionprinciple manually and explicitly for a type with indices.Fixes #11450.