Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: make
generalize_proofs
handle proofs under binders (#12472)
The `generalize_proofs` tactic had a bug where it would not generalize proofs that appeared under binders correctly, creating terms with fvars from the wrong context. The tactic has been refactored, and it now abstracts the proofs (universally quantifying all the bound variables that appear in the proof) before lifting them to the local context. This feature can be controlled with the `abstract` option. Using `generalize_proofs (config := { abstract := false })` turns off proof abstraction and leaves alone those proofs that refer to bound variables. Other new features: - `generalize_proofs at h` for a let-bound local hypothesis `h` will clear its value. - `generalize_proofs at h` for a duplicate proposition will eliminate `h` from the local context. - Proofs are recursively generalized for each new local hypothesis. This can be turned off with `generalize_proofs (config := { maxDepth := 0 })`. - `generalize_proofs at h` will no longer generalize proofs from the goal. - The type of the generalized proof is carefully computed by propagating expected types, rather than by using `inferType`. This gives local hypotheses in more useful forms. (This PR serves as a followup to [this comment](#447 (comment)).)
- Loading branch information
Showing
7 changed files
with
592 additions
and
142 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.