Documentation

Lean.Elab.Tactic.NormCast

The norm_cast family of tactics. #

A full description of the tactic, and the use of each theorem category, can be found at https://arxiv.org/abs/2001.10594.

Proves a = b using the given simp set.

Equations
    Instances For

      Proves a = b by simplifying using move and squash lemmas.

      Equations
        Instances For

          Constructs the expression (e : ty).

          Equations
            Instances For

              Checks whether an expression is the coercion of some other expression, and if so returns that expression.

              Equations
                Instances For

                  Checks whether an expression is a numeral in some type, and if so returns that type and the natural number.

                  Equations
                    Instances For

                      This is the main heuristic used alongside the elim and move lemmas. The goal is to help casts move past operators by adding intermediate casts. An expression of the shape:

                      op (↑(x : α) : γ) (↑(y : β) : γ)
                      

                      is rewritten to:

                      op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ)
                      

                      when

                      (↑(↑(x : α) : β) : γ) = (↑(x : α) : γ)
                      

                      can be proven with a squash lemma

                      Equations
                        Instances For

                          Discharging function used during simplification in the "squash" step.

                          Equations
                            Instances For

                              Core rewriting function used in the "squash" step, which moves casts upwards and eliminates them.

                              It tries to rewrite an expression using the elim and move lemmas. On failure, it calls the splitting procedure heuristic.

                              Equations
                                Instances For

                                  If possible, rewrites (n : α) to (Nat.cast n : α) where n is a numeral and α ≠ ℕ. Returns a pair of the new expression and proof that they are equal.

                                  Equations
                                    Instances For

                                      The core simplification routine of normCast.

                                      Equations
                                        Instances For

                                          Implementation of the norm_cast tactic when operating on the main goal.

                                          Equations
                                            Instances For

                                              Implementation of the norm_cast tactic when operating on a hypothesis.

                                              Equations
                                                Instances For