Documentation

Std.Tactic.NormCast.Ext

Label is a type used to classify norm_cast lemmas.

  • elim lemma: LHS has 0 head coes and ≥ 1 internal coe
  • move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
  • squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
Instances For

    Assuming e is an application, returns the list of subterms that simp will rewrite in.

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

      Count how many coercions are at the top of the expression.

      Count how many coercions are inside the expression, including the top ones.

      Count how many coercions are inside the expression, excluding the top ones.

      Equations
      Instances For

        Classifies a declaration of type ty as a norm_cast rule.

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

          The norm_cast attribute stores three simp sets.

          Instances For

            addMove decl adds decl as a move lemma to the cache.

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

              addSquash decl adds decl as a squash lemma to the cache.

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

                addInfer decl infers the label of decl and adds it to the cache.

                • elim lemma: LHS has 0 head coes and ≥ 1 internal coe
                • move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
                • squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The possible norm_cast kinds: elim, move, or squash.

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

                    The norm_cast attribute should be given to lemmas that describe the behaviour of a coercion in regard to an operator, a relation, or a particular function.

                    It only concerns equality or iff lemmas involving , and , describing the behavior of the coercion functions. It does not apply to the explicit functions that define the coercions.

                    Examples:

                    @[norm_cast] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n
                    
                    @[norm_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1
                    
                    @[norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
                    
                    @[norm_cast] theorem coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n
                    
                    @[norm_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n
                    
                    @[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
                    

                    Lemmas tagged with @[norm_cast] are classified into three categories: move, elim, and squash. They are classified roughly as follows:

                    • elim lemma: LHS has 0 head coes and ≥ 1 internal coe
                    • move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
                    • squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes

                    norm_cast uses move and elim lemmas to factor coercions toward the root of an expression and to cancel them from both sides of an equation or relation. It uses squash lemmas to clean up the result.

                    Occasionally you may want to override the automatic classification. You can do this by giving an optional elim, move, or squash parameter to the attribute.

                    @[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n := by
                      rw [← of_real_nat_cast, of_real_re]
                    

                    Don't do this unless you understand what you are doing.

                    A full description of the tactic, and the use of each lemma category, can be found at .

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