Documentation

Init.Conv

conv is the syntax category for a "conv tactic", where "conv" is short for conversion. A conv tactic is a program which receives a target, printed as | a, and is tasked with coming up with some term b and a proof of a = b. It is mainly used for doing targeted term transformations, for example rewriting only on the left side of an equality.

Equations
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
        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

            The * occurrence list means to apply to all occurrences of the pattern.

            Equations
            Instances For

              A list 1 2 4 of occurrences means to apply to the first, second, and fourth occurrence of the pattern.

              Equations
              Instances For

                An occurrence specification, either * or a list of numbers. The default is [1].

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

                  with_annotate_state stx t annotates the lexical range of stx : Syntax with the initial and final state of running tactic t.

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

                    Traverses into the left subterm of a binary operator. (In general, for an n-ary operator, it traverses into the second to last argument.)

                    Equations
                    Instances For

                      Traverses into the right subterm of a binary operator. (In general, for an n-ary operator, it traverses into the last argument.)

                      Equations
                      Instances For

                        Reduces the target to Weak Head Normal Form. This reduces definitions in "head position" until a constructor is exposed. For example, List.map f [a, b, c] weak head normalizes to f a :: List.map f [b, c].

                        Equations
                        Instances For

                          Expands let-declarations and let-variables.

                          Equations
                          Instances For

                            Puts term in normal form, this tactic is meant for debugging purposes only.

                            Equations
                            Instances For

                              Performs one step of "congruence", which takes a term and produces subgoals for all the function arguments. For example, if the target is f x y then congr produces two subgoals, one for x and one for y.

                              Equations
                              Instances For
                                • arg i traverses into the i'th argument of the target. For example if the target is f a b c d then arg 1 traverses to a and arg 3 traverses to c.
                                • arg @i is the same as arg i but it counts all arguments instead of just the explicit arguments.
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  ext x traverses into a binder (a fun x => e or ∀ x, e expression) to target e, introducing name x in the process.

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

                                    change t' replaces the target t with t', assuming t and t' are definitionally equal.

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

                                      delta id1 id2 ... unfolds all occurrences of id1, id2, ... in the target. Like the delta tactic, this ignores any definitional equations and uses primitive delta-reduction instead, which may result in leaking implementation details. Users should prefer unfold for unfolding definitions.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        • unfold foo unfolds all occurrences of foo in the target.
                                        • unfold id1 id2 ... is equivalent to unfold id1; unfold id2; .... Like the unfold tactic, this uses equational lemmas for the chosen definition to rewrite the target. For recursive definitions, only one layer of unfolding is performed.
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          • pattern pat traverses to the first subterm of the target that matches pat.
                                          • pattern (occs := *) pat traverses to every subterm of the target that matches pat which is not contained in another match of pat. It generates one subgoal for each matching subterm.
                                          • pattern (occs := 1 2 4) pat matches occurrences 1, 2, 4 of pat and produces three subgoals. Occurrences are numbered left to right from the outside in.

                                          Note that skipping an occurrence of pat will traverse inside that subexpression, which means it may find more matches and this can affect the numbering of subsequent pattern matches. For example, if we are searching for f _ in f (f a) = f b:

                                          • occs := 1 2 (and occs := *) returns | f (f a) and | f b
                                          • occs := 2 returns | f a
                                          • occs := 2 3 returns | f a and | f b
                                          • occs := 1 3 is an error, because after skipping f b there is no third match.
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            rw [thm] rewrites the target using thm. See the rw tactic for more information.

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

                                              simp [thm] performs simplification using thm and marked @[simp] lemmas. See the simp tactic for more information.

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

                                                dsimp is the definitional simplifier in conv-mode. It differs from simp in that it only applies theorems that hold by reflexivity.

                                                Examples:

                                                example (a : Nat): (0 + 0) = a - a := by
                                                  conv =>
                                                    lhs
                                                    dsimp
                                                    rw [← Nat.sub_self a]
                                                
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  simp_match simplifies match expressions. For example,

                                                  match [a, b] with
                                                  | [] => 0
                                                  | hd :: tl => hd
                                                  

                                                  simplifies to a.

                                                  Equations
                                                  Instances For

                                                    Executes the given tactic block without converting conv goal into a regular goal.

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

                                                      Focuses, converts the conv goal lhs into a regular goal lhs = rhs, and then executes the given tactic block.

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

                                                        Executes the given conv block without converting regular goal into a conv goal.

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

                                                          { convs } runs the list of convs on the current target, and any subgoals that remain are trivially closed by skip.

                                                          Equations
                                                          Instances For

                                                            (convs) runs the convs in sequence on the current list of targets. This is pure grouping with no added effects.

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

                                                              rfl closes one conv goal "trivially", by using reflexivity (that is, no rewriting).

                                                              Equations
                                                              Instances For

                                                                done succeeds iff there are no goals remaining.

                                                                Equations
                                                                Instances For

                                                                  trace_state prints the current goal state.

                                                                  Equations
                                                                  Instances For

                                                                    all_goals tac runs tac on each goal, concatenating the resulting goals, if any.

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

                                                                      any_goals tac applies the tactic tac to every goal, and succeeds if at least one application succeeds.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        • case tag => tac focuses on the goal with case name tag and solves it using tac, or else fails.
                                                                        • case tag x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.
                                                                        • case tag₁ | tag₂ => tac is equivalent to (case tag₁ => tac); (case tag₂ => tac).
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          case' is similar to the case tag => tac tactic, but does not ensure the goal has been solved after applying tac, nor admits the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

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

                                                                            next => tac focuses on the next goal and solves it using tac, or else fails. next x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.

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

                                                                              focus tac focuses on the main goal, suppressing all other goals, and runs tac on it. Usually · tac, which enforces that the goal is closed by tac, should be preferred.

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

                                                                                conv => cs runs cs in sequence on the target t, resulting in t', which becomes the new target subgoal.

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

                                                                                  · conv focuses on the main conv goal and tries to solve it using s.

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

                                                                                    fail_if_success t fails if the tactic t succeeds.

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

                                                                                      rw [rules] applies the given list of rewrite rules to the target. See the rw tactic for more information.

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

                                                                                        erw [rules] is a shorthand for rw (config := { transparency := .default }) [rules]. This does rewriting up to unfolding of regular definitions (by comparison to regular rw which only unfolds @[reducible] definitions).

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

                                                                                          args traverses into all arguments. Synonym for congr.

                                                                                          Equations
                                                                                          Instances For

                                                                                            left traverses into the left argument. Synonym for lhs.

                                                                                            Equations
                                                                                            Instances For

                                                                                              right traverses into the right argument. Synonym for rhs.

                                                                                              Equations
                                                                                              Instances For

                                                                                                intro traverses into binders. Synonym for ext.

                                                                                                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

                                                                                                    enter [arg, ...] is a compact way to describe a path to a subterm. It is a shorthand for other conv tactics as follows:

                                                                                                    • enter [i] is equivalent to arg i.
                                                                                                    • enter [@i] is equivalent to arg @i.
                                                                                                    • enter [x] (where x is an identifier) is equivalent to ext x. For example, given the target f (g a (fun x => x b)), enter [1, 2, x, 1] will traverse to the subterm b.
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For

                                                                                                      The apply thm conv tactic is the same as apply thm the tactic. There are no restrictions on thm, but strange results may occur if thm cannot be reasonably interpreted as proving one equality from a list of others.

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

                                                                                                        first | conv | ... runs each conv until one succeeds, or else fails.

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

                                                                                                          try tac runs tac and succeeds even if tac failed.

                                                                                                          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

                                                                                                              repeat convs runs the sequence convs repeatedly until it fails to apply.

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

                                                                                                                conv => ... allows the user to perform targeted rewriting on a goal or hypothesis, by focusing on particular subexpressions.

                                                                                                                See https://lean-lang.org/theorem_proving_in_lean4/conv.html for more details.

                                                                                                                Basic forms:

                                                                                                                • conv => cs will rewrite the goal with conv tactics cs.
                                                                                                                • conv at h => cs will rewrite hypothesis h.
                                                                                                                • conv in pat => cs will rewrite the first subexpression matching pat (see pattern).
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For