Documentation

Mathlib.Tactic.Conv

Additional conv tactics.

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

        conv in pat => cs runs the conv tactic sequence cs on the first subexpression matching the pattern pat in the target. The converted expression becomes the new target subgoal, like conv => cs.

        The arguments in are the same as those as the in pattern. In fact, conv in pat => cs is a macro for conv => pattern pat; cs.

        The syntax also supports the occs clause. Example:

        conv in (occs := *) x + y => rw [add_comm]
        
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          • discharge => tac is a conv tactic which rewrites target p to True if tac is a tactic which proves the goal ⊢ p.
          • discharge without argument returns ⊢ p as a subgoal.
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Elaborator for the discharge tactic.

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

              Use refine in conv mode.

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

                The command #conv tac => e will run a conv tactic tac on e, and display the resulting expression (discarding the proof). For example, #conv rw [true_and] => TrueFalse displays False. There are also shorthand commands for several common conv tactics:

                • #whnf e is short for #conv whnf => e
                • #simp e is short for #conv simp => e
                • #norm_num e is short for #conv norm_num => e
                • #push_neg e is short for #conv push_neg => e
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  with_reducible tacs excutes tacs using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

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

                    The command #whnf e evaluates e to Weak Head Normal Form, which means that the "head" of the expression is reduced to a primitive - a lambda or forall, or an axiom or inductive type. It is similar to #reduce e, but it does not reduce the expression completely, only until the first constructor is exposed. For example:

                    open Nat List
                    set_option pp.notation false
                    #whnf [1, 2, 3].map succ
                    -- cons (succ 1) (map succ (cons 2 (cons 3 nil)))
                    #reduce [1, 2, 3].map succ
                    -- cons 2 (cons 3 (cons 4 nil))
                    

                    The head of this expression is the List.cons constructor, so we can see from this much that the list is not empty, but the subterms Nat.succ 1 and List.map Nat.succ (List.cons 2 (List.cons 3 List.nil)) are still unevaluated. #reduce is equivalent to using #whnf on every subexpression.

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

                      The command #whnfR e evaluates e to Weak Head Normal Form with Reducible transparency, that is, it uses whnf but only unfolding reducible definitions.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        • #simp => e runs simp on the expression e and displays the resulting expression after simplification.
                        • #simp only [lems] => e runs simp only [lems] on e.
                        • The => is optional, so #simp e and #simp only [lems] e have the same behavior. It is mostly useful for disambiguating the expression e from the lemmas.
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For