The generalize_proofs
tactic #
Generalize any proofs occuring in the goal or in chosen hypotheses, replacing them by
named hypotheses so that they can be referred to later in the proof easily.
Commonly useful when dealing with functions like Classical.choose
that produce data from proofs.
For example:
example : list.nth_le [1, 2] 1 dec_trivial = 2 := by
-- ⊢ [1, 2].nth_le 1 _ = 2
generalize_proofs h,
-- h : 1 < [1, 2].length
-- ⊢ [1, 2].nth_le 1 h = 2
⊢ [1, 2].nth_le 1 _ = 2
generalize_proofs h,
-- h : 1 < [1, 2].length
-- ⊢ [1, 2].nth_le 1 h = 2
⊢ [1, 2].nth_le 1 h = 2
The user provided names, may be anonymous
nextIdx : List (Lean.TSyntax `Lean.binderIdent)The generalizations made so far
curIdx : Array Lean.Meta.GeneralizeArg
State for the generalize proofs tactic, contains the remaining names to be used and the list of generalizations so far
Instances For
@[inline]
Monad used by the generalizeProofs
tactic, carries an expr cache and state with
names to use and previous generalizations
Recursively generalize proofs occuring in e
Generalize proofs in the goal, naming them with the provided list.
For example:
example : list.nth_le [1, 2] 1 dec_trivial = 2 := by
-- ⊢ [1, 2].nth_le 1 _ = 2
generalize_proofs h,
-- h : 1 < [1, 2].length
-- ⊢ [1, 2].nth_le 1 h = 2
⊢ [1, 2].nth_le 1 _ = 2
generalize_proofs h,
-- h : 1 < [1, 2].length
-- ⊢ [1, 2].nth_le 1 h = 2
⊢ [1, 2].nth_le 1 h = 2
Equations
- One or more equations did not get rendered due to their size.