Documentation

Mathlib.Tactic.Push

The push, push_neg and pull tactics #

The push tactic pushes a given constant inside expressions: it can be applied to goals as well as local hypotheses and also works as a conv tactic. push_neg is a macro for push Not.

The pull tactic does the reverse: it pulls the given constant towards the head of the expression.

theorem Mathlib.Tactic.Push.not_exists {α : Sort u_1} (s : αProp) :
(¬ (x : α), s x) ∀ (x : α), binderNameHint x s ¬s x
theorem Mathlib.Tactic.Push.not_and_eq (p q : Prop) :
(¬(p q)) = (p¬q)
theorem Mathlib.Tactic.Push.not_forall_eq {α : Sort u_1} (s : αProp) :
(¬∀ (x : α), s x) = (x : α), ¬s x

The simp configuration used in push.

Equations
Instances For

    Try to rewrite using a push lemma.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Common entry point to the implementation of push.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Try to rewrite using a pull lemma.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Common entry point to the implementation of pull.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Return true if stx is an underscore, i.e. _ or fun $_ => _/fun $_ ↦ _.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              resolvePushId? is a version of resolveId? that also supports notations like _ ∈ _, ∃ x, _ and ∑ x, _.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Elaborator for the argument passed to push. It accepts a constant, or a function

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Elaborate the (disch := ...) syntax for a simp-like tactic.

                  Equations
                  Instances For

                    push pushes the given constant away from the head of the expression. For example

                    • push _ ∈ _ rewrites x ∈ {y} ∪ zᶜ into x = y ∨ ¬ x ∈ z.
                    • push (disch := positivity) Real.log rewrites log (a * b ^ 2) into log a + 2 * log b.
                    • push ¬ _ is the same as push_neg or push Not, and it rewrites ¬ ∀ ε > 0, ∃ δ > 0, δ < ε into ∃ ε > 0, ∀ δ > 0, ε ≤ δ.

                    In addition to constants, push can be used to push fun and binders:

                    • push fun _ ↦ _ rewrites fun x => f x ^ 2 + 5 into f ^ 2 + 5
                    • push ∀ _, _ rewrites ∀ a, p a ∧ q a into (∀ a, p a) ∧ (∀ a, q a).

                    The push tactic can be extended using the @[push] attribute.

                    To instead move a constant closer to the head of the expression, use the pull tactic.

                    To push a constant at a hypothesis, use the push ... at h or push ... at * syntax.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Push negations into the conclusion or a hypothesis. For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x. Binder names are preserved.

                      push_neg is a special case of the more general push tactic, namely push Not. The push tactic can be extended using the @[push] attribute. push has special-casing built in for push Not, so that it can preserve binder names, and so that ¬ (p ∧ q) can be transformed to either p → ¬ q (the default) or ¬ p ∨ ¬ q. To get ¬ p ∨ ¬ q, use set_option push_neg.use_distrib true.

                      Another example: given a hypothesis

                      h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε
                      

                      writing push_neg at h will turn h into

                      h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|
                      

                      Note that binder names are preserved by this tactic, contrary to what would happen with simp using the relevant lemmas. One can use this tactic at the goal using push_neg, at every hypothesis and the goal using push_neg at * or at selected hypotheses and the goal using say push_neg at h h' ⊢, as usual.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        pull is the inverse tactic to push. It pulls the given constant towards the head of the expression. For example

                        • pull _ ∈ _ rewrites x ∈ y ∨ ¬ x ∈ z into x ∈ y ∪ zᶜ.
                        • pull (disch := positivity) Real.log rewrites log a + 2 * log b into log (a * b ^ 2).
                        • pull fun _ ↦ _ rewrites f ^ 2 + 5 into fun x => f x ^ 2 + 5 where f is a function.

                        A lemma is considered a pull lemma if its reverse direction is a push lemma that actually moves the given constant away from the head. For example

                        • not_or : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q is a pull lemma, but not_not : ¬ ¬ p ↔ p is not.
                        • log_mul : log (x * y) = log x + log y is a pull lemma, but log_abs : log |x| = log x is not.
                        • Pi.mul_def : f * g = fun (i : ι) => f i * g i and Pi.one_def : 1 = fun (x : ι) => 1 are both pull lemmas for fun, because every push fun _ ↦ _ lemma is also considered a pull lemma.

                        TODO: define a @[pull] attribute for tagging pull lemmas that are not push lemmas.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          A simproc variant of push fun _ ↦ _, to be used as simp [↓pushFun].

                          Equations
                          Instances For

                            A simproc variant of pull fun _ ↦ _, to be used as simp [pullFun].

                            Equations
                            Instances For

                              push pushes the given constant away from the head of the expression. For example

                              • push _ ∈ _ rewrites x ∈ {y} ∪ zᶜ into x = y ∨ ¬ x ∈ z.
                              • push (disch := positivity) Real.log rewrites log (a * b ^ 2) into log a + 2 * log b.
                              • push ¬ _ is the same as push_neg or push Not, and it rewrites ¬ ∀ ε > 0, ∃ δ > 0, δ < ε into ∃ ε > 0, ∀ δ > 0, ε ≤ δ.

                              In addition to constants, push can be used to push fun and binders:

                              • push fun _ ↦ _ rewrites fun x => f x ^ 2 + 5 into f ^ 2 + 5
                              • push ∀ _, _ rewrites ∀ a, p a ∧ q a into (∀ a, p a) ∧ (∀ a, q a).

                              The push tactic can be extended using the @[push] attribute.

                              To instead move a constant closer to the head of the expression, use the pull tactic.

                              To push a constant at a hypothesis, use the push ... at h or push ... at * syntax.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Push negations into the conclusion or a hypothesis. For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x. Binder names are preserved.

                                push_neg is a special case of the more general push tactic, namely push Not. The push tactic can be extended using the @[push] attribute. push has special-casing built in for push Not, so that it can preserve binder names, and so that ¬ (p ∧ q) can be transformed to either p → ¬ q (the default) or ¬ p ∨ ¬ q. To get ¬ p ∨ ¬ q, use set_option push_neg.use_distrib true.

                                Another example: given a hypothesis

                                h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε
                                

                                writing push_neg at h will turn h into

                                h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|
                                

                                Note that binder names are preserved by this tactic, contrary to what would happen with simp using the relevant lemmas. One can use this tactic at the goal using push_neg, at every hypothesis and the goal using push_neg at * or at selected hypotheses and the goal using say push_neg at h h' ⊢, as usual.

                                Equations
                                Instances For

                                  The syntax is #push head e, where head is a constant and e is an expression, which will print the push head form of e.

                                  #push understands local variables, so you can use them to introduce parameters.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    The syntax is #push_neg e, where e is an expression, which will print the push_neg form of e.

                                    #push_neg understands local variables, so you can use them to introduce parameters.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      pull is the inverse tactic to push. It pulls the given constant towards the head of the expression. For example

                                      • pull _ ∈ _ rewrites x ∈ y ∨ ¬ x ∈ z into x ∈ y ∪ zᶜ.
                                      • pull (disch := positivity) Real.log rewrites log a + 2 * log b into log (a * b ^ 2).
                                      • pull fun _ ↦ _ rewrites f ^ 2 + 5 into fun x => f x ^ 2 + 5 where f is a function.

                                      A lemma is considered a pull lemma if its reverse direction is a push lemma that actually moves the given constant away from the head. For example

                                      • not_or : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q is a pull lemma, but not_not : ¬ ¬ p ↔ p is not.
                                      • log_mul : log (x * y) = log x + log y is a pull lemma, but log_abs : log |x| = log x is not.
                                      • Pi.mul_def : f * g = fun (i : ι) => f i * g i and Pi.one_def : 1 = fun (x : ι) => 1 are both pull lemmas for fun, because every push fun _ ↦ _ lemma is also considered a pull lemma.

                                      TODO: define a @[pull] attribute for tagging pull lemmas that are not push lemmas.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        The syntax is #pull head e, where head is a constant and e is an expression, which will print the pull head form of e.

                                        #pull understands local variables, so you can use them to introduce parameters.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          #push_discr_tree X shows the discrimination tree of all lemmas used by push X. This can be helpful when you are constructing a set of push lemmas for the constant X.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            #push_discr_tree X shows the discrimination tree of all lemmas used by push X. This can be helpful when you are constructing a set of push lemmas for the constant X.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For