-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor: induction₂_symm: Be more explicit in the case variables #11023
Conversation
and in `setToL1_mono_left`, instantiate the induction theorem explicitly. In leanprover/lean4#3505 I am fixing a big where `induction` will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for `forall`s; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now.
…rs (#3505) Else the `case` will now allow introducing all necessary variables. Induction principles with `let` in the types of the cases will be more common with #3432. This implementation no longer reduces the type as it goes, but really only counts manifest foralls and lets. I find this more sensible and predictable: If you have ``` theorem induction₂_symm {P : EReal → EReal → Prop} (symm : Symmetric P) … ``` then previously, writing ``` case symm => ``` would actually bring a fresh `x` and `y` and variable `h : P x y` into scope and produce a goal of `P y x`, because `Symmetric P` happens to be ``` def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x ``` After this change, after `case symm =>` will leave `Symmetric P` as the goal. This gives more control to the author of the induction hypothesis about the actual goal of the cases. This shows up in mathlib in two places; fixes in leanprover-community/mathlib4#11023. I consider these improvements.
The Lean PR has been merged; ideally we merge this into |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I do not fully understand the implications of the change, but it looks good to me!
and in `setToL1_mono_left`, instantiate the induction theorem explicitly. In leanprover/lean4#3505 I am fixing a big where `induction` will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for `forall`s; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now. (cherry picked from commit #11023, needed for nightly 2024-02-29)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…1023) and in `setToL1_mono_left`, instantiate the induction theorem explicitly. In leanprover/lean4#3505 I am fixing a big where `induction` will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for `forall`s; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now.
Pull request successfully merged into master. Build succeeded: |
…1023) and in `setToL1_mono_left`, instantiate the induction theorem explicitly. In leanprover/lean4#3505 I am fixing a big where `induction` will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for `forall`s; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now.
…1023) and in `setToL1_mono_left`, instantiate the induction theorem explicitly. In leanprover/lean4#3505 I am fixing a big where `induction` will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for `forall`s; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now.
…1023) and in `setToL1_mono_left`, instantiate the induction theorem explicitly. In leanprover/lean4#3505 I am fixing a big where `induction` will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for `forall`s; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now.
…1023) and in `setToL1_mono_left`, instantiate the induction theorem explicitly. In leanprover/lean4#3505 I am fixing a big where `induction` will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for `forall`s; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now.
…1023) and in `setToL1_mono_left`, instantiate the induction theorem explicitly. In leanprover/lean4#3505 I am fixing a big where `induction` will assume the wrong number of parameters for a case when there are let-bindings in the type involved. As part of this I am no longer reducing definitions when looking for `forall`s; this is arguably more predictable and more likely what the user wants. There are two breakages in mathlib due to this, and the fix can already be applied now.
and in
setToL1_mono_left
, instantiate the induction theoremexplicitly.
In leanprover/lean4#3505 I am fixing a big where
induction
will assume the wrong number of parameters for a case whenthere are let-bindings in the type involved. As part of this I am no
longer reducing definitions when looking for
forall
s; this is arguablymore predictable and more likely what the user wants.
There are two breakages in mathlib due to this, and the fix can already
be applied now.