Commit 2024-04-29 01:28 32616bea

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.)