mathlib3 documentation

tactic.norm_cast

A tactic for normalizing casts inside expressions #

This tactic normalizes casts inside expressions. It can be thought of as a call to the simplifier with a specific set of lemmas to move casts upwards in the expression. It has special handling of numerals and a simple heuristic to help moving casts "past" binary operators. Contrary to simp, it should be safe to use as a non-terminating tactic.

The algorithm implemented here is described in the paper https://lean-forward.github.io/norm_cast/norm_cast.pdf.

Important definitions #

source
meta def tactic.mk_instance_fast (e : expr) (timeout : ℕ := 1000) :
tactic expr

Runs mk_instance with a time limit.

This is a work around to the fact that in some cases mk_instance times out instead of failing, for example: has_lift_t ℤ ℕ

mk_instance_fast is used when we assume the type class search should end instantly.

source
meta def norm_cast.trace_norm_cast {α : Type u_1} [has_to_tactic_format α] (msg : string) (a : α) :
tactic unit

Output a trace message if trace.norm_cast is enabled.

source
@[protected, instance]
meta def norm_cast.label.has_reflect  :
has_reflect norm_cast.label
source
@[protected, instance]
def norm_cast.label.decidable_eq  :
decidable_eq norm_cast.label
source
inductive norm_cast.label  :
Type

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 norm_cast.label
source
@[protected, instance]
def norm_cast.label.inhabited  :
inhabited norm_cast.label
source
@[protected]
def norm_cast.label.to_string  :
norm_cast.label → string

Convert label into string.

Equations
source
@[protected, instance]
def norm_cast.label.has_to_string  :
has_to_string norm_cast.label
Equations
source
@[protected, instance]
def norm_cast.label.has_repr  :
has_repr norm_cast.label
Equations
source
@[protected, instance]
meta def norm_cast.label.has_to_format  :
has_to_format norm_cast.label
source
def norm_cast.label.of_string  :
string → option norm_cast.label

Convert string into label.

Equations
source
meta def norm_cast.count_head_coes  :
expr → ℕ

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

source
meta def norm_cast.count_coes  :
expr → tactic ℕ

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

source
meta def norm_cast.classify_type (ty : expr) :
tactic norm_cast.label

Classifies a declaration of type ty as a norm_cast rule.

source
meta structure norm_cast.norm_cast_cache  :
Type

The cache for norm_cast attribute stores three simp_lemma objects.

Instances for norm_cast.norm_cast_cache
source
meta def norm_cast.empty_cache  :
norm_cast.norm_cast_cache

Empty norm_cast_cache.

source
@[protected, instance]
meta def norm_cast.norm_cast_cache.inhabited  :
inhabited norm_cast.norm_cast_cache
source
meta def norm_cast.add_elim (cache : norm_cast.norm_cast_cache) (e : expr) :
tactic norm_cast.norm_cast_cache

add_elim cache e adds e as an elim lemma to cache.

source
meta def norm_cast.add_move (cache : norm_cast.norm_cast_cache) (e : expr) :
tactic norm_cast.norm_cast_cache

add_move cache e adds e as a move lemma to cache.

source
meta def norm_cast.add_squash (cache : norm_cast.norm_cast_cache) (e : expr) :
tactic norm_cast.norm_cast_cache

add_squash cache e adds e as an squash lemma to cache.

source
meta def norm_cast.norm_cast_attr_ty  :
Type

The type of the norm_cast attribute. The optional label is used to overwrite the classifier.

source
meta def norm_cast.get_label_param (attr : norm_cast.norm_cast_attr_ty) (decl : name) :
tactic (option norm_cast.label)

Efficient getter for the @[norm_cast] attribute parameter that does not call eval_expr.

See Note [user attribute parameters].

source
meta def norm_cast.add_lemma (attr : norm_cast.norm_cast_attr_ty) (cache : norm_cast.norm_cast_cache) (decl : name) :
tactic norm_cast.norm_cast_cache

add_lemma cache decl infers the proper norm_cast attribute for decl and adds it to cache.

source
meta def norm_cast.mk_cache (attr : thunk norm_cast.norm_cast_attr_ty) (names : list name) :
tactic norm_cast.norm_cast_cache

mk_cache names creates a norm_cast_cache. It infers the proper norm_cast attributes for names in names, and collects the lemmas attributed with specific norm_cast attributes.

source
meta def norm_cast.norm_cast_attr  :
user_attribute norm_cast.norm_cast_cache (option norm_cast.label)

The norm_cast attribute.

source
meta def norm_cast.make_guess (decl : name) :
tactic norm_cast.label

Classify a declaration as a norm_cast rule.

source
meta def norm_cast.get_label (decl : name) :
tactic norm_cast.label

Gets the norm_cast classification label for a declaration. Applies the override specified on the attribute, if necessary.

source
meta def tactic.interactive.push_cast (hs : interactive.parse tactic.simp_arg_list) (l : interactive.parse interactive.types.location) :
tactic unit

push_cast rewrites the expression to move casts toward the leaf nodes. For example, ↑(a + b) will be written to ↑a + ↑b. Equivalent to simp only with push_cast. Can also be used at hypotheses.

push_cast can also be used at hypotheses and with extra simp rules.

example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
  ((a + b : ℕ) : ℤ) = 10 :=
begin
  push_cast,
  push_cast at h1,
  push_cast [int.add_zero] at h2,
end
source
meta def norm_cast.prove_eq_using (s : simp_lemmas) (a b : expr) :
tactic expr

Prove a = b using the given simp set.

source
meta def norm_cast.prove_eq_using_down (a b : expr) :
tactic expr

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

source
meta def norm_cast.splitting_procedure  :
expr → tactic (expr × expr)

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

source
meta def norm_cast.upward_and_elim (s : simp_lemmas) (e : expr) :
tactic (expr × expr)

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.

The following auxiliary functions are used to handle numerals.

source
meta def norm_cast.numeral_to_coe (e : expr) :
tactic (expr × expr)

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

source
meta def norm_cast.coe_to_numeral (e : expr) :
tactic (expr × expr)

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

source
meta def norm_cast.derive (e : expr) :
tactic (expr × expr)

The core simplification routine of norm_cast.

source
meta def norm_cast.derive_push_cast (extra_lems : list tactic.simp_arg_type) (e : expr) :
tactic (expr × expr)

A small variant of push_cast suited for non-interactive use.

derive_push_cast extra_lems e returns an expression e' and a proof that e = e'.

source
meta def tactic.aux_mod_cast (e : expr) (include_goal : bool := bool.tt) :
tactic expr

aux_mod_cast e runs norm_cast on e and returns the result. If include_goal is true, it also normalizes the goal.

source
meta def tactic.exact_mod_cast (e : expr) :
tactic unit

exact_mod_cast e runs norm_cast on the goal and e, and tries to use e to close the goal.

source
meta def tactic.apply_mod_cast (e : expr) :
tactic (list (name × expr))

apply_mod_cast e runs norm_cast on the goal and e, and tries to apply e.

source
meta def tactic.assumption_mod_cast  :
tactic unit

assumption_mod_cast runs norm_cast on the goal. For each local hypothesis h, it also normalizes h and tries to use that to close the goal.

source
meta def tactic.interactive.norm_cast (loc : interactive.parse interactive.types.location) :
tactic unit

Normalize casts at the given locations by moving them "upwards". As opposed to simp, norm_cast can be used without necessarily closing the goal.

source
meta def tactic.interactive.rw_mod_cast (rs : interactive.parse tactic.interactive.rw_rules) (loc : interactive.parse interactive.types.location) :
tactic unit

Rewrite with the given rules and normalize casts between steps.

source
meta def tactic.interactive.exact_mod_cast (e : interactive.parse interactive.types.texpr) :
tactic unit

Normalize the goal and the given expression, then close the goal with exact.

source
meta def tactic.interactive.apply_mod_cast (e : interactive.parse interactive.types.texpr) :
tactic unit

Normalize the goal and the given expression, then apply the expression to the goal.

source
meta def tactic.interactive.assumption_mod_cast  :
tactic unit

Normalize the goal and every expression in the local context, then close the goal with assumption.

source
meta def conv.interactive.norm_cast  :
conv unit

the converter version of `norm_cast'

source
@[norm_cast]
theorem ite_cast {α : Sort u_1} {β : Sort u_2} [has_lift_t α β] {c : Prop} [decidable c] {a b : α} :
↑(ite c a b) = ite c ↑a ↑b
source
@[norm_cast]
theorem dite_cast {α : Sort u_1} {β : Sort u_2} [has_lift_t α β] {c : Prop} [decidable c] {a : c → α} {b : ¬c → α} :
↑(dite c a b) = dite c (λ (h : c), ↑(a h)) (λ (h : ¬c), ↑(b h))
source
def tactic_doc.tactic.norm_cast  :
tactic_doc_entry

The norm_cast family of tactics is used to normalize casts inside expressions. It is basically a simp tactic with a specific set of lemmas to move casts upwards in the expression. Therefore it can be used more safely as a non-terminating tactic. It also has special handling of numerals.

For instance, given an assumption

a b : ℤ
h : ↑a + ↑b < (10 : ℚ)

writing norm_cast at h will turn h into

h : a + b < 10

You can also use exact_mod_cast, apply_mod_cast, rw_mod_cast or assumption_mod_cast. Writing exact_mod_cast h and apply_mod_cast h will normalize the goal and h before using exact h or apply h. Writing assumption_mod_cast will normalize the goal and for every expression h in the context it will try to normalize h and use exact h. rw_mod_cast acts like the rw tactic but it applies norm_cast between steps.

push_cast rewrites the expression to move casts toward the leaf nodes. This uses norm_cast lemmas in the forward direction. For example, ↑(a + b) will be written to ↑a + ↑b. It is equivalent to simp only with push_cast. It can also be used at hypotheses with push_cast at h and with extra simp lemmas with push_cast [int.add_zero].

example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
  ((a + b : ℕ) : ℤ) = 10 :=
begin
  push_cast,
  push_cast at h1,
  push_cast [int.add_zero] at h2,
end

The implementation and behavior of the norm_cast family is described in detail at https://lean-forward.github.io/norm_cast/norm_cast.pdf.

source
def tactic_doc.attribute.norm_cast attributes  :
tactic_doc_entry

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_sub [add_group α] [has_one α] {m n} (h : m ≤ n) :
  ((n - m : ℕ) : α) = n - m

@[norm_cast] theorem coe_nat_bit0 (n : ℕ) : (↑(bit0 n) : ℤ) = bit0 ↑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 https://lean-forward.github.io/norm_cast/norm_cast.pdf.