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 #

• tactic.interactive.norm_cast
• tactic.interactive.push_cast
• tactic.interactive.exact_mod_cast
• tactic.interactive.apply_mod_cast
• tactic.interactive.rw_mod_cast
• tactic.interactive.assumption_mod_cast
meta def tactic.mk_instance_fast (e : expr) (timeout : := 1000) :

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.

meta def norm_cast.trace_norm_cast {α : Type u_1} (msg : string) (a : α) :

Output a trace message if trace.norm_cast is enabled.

meta def simp_attr.push_cast  :

The push_cast simp attribute uses norm_cast lemmas to move casts toward the leaf nodes of the expression.

@[protected, instance]
@[protected, instance]
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
@[protected, instance]
@[protected]

Convert label into string.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]

Convert string into label.

Equations

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

meta def norm_cast.count_coes  :

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

meta def norm_cast.classify_type (ty : expr) :

Classifies a declaration of type ty as a norm_cast rule.

meta structure norm_cast.norm_cast_cache  :
Type

The cache for norm_cast attribute stores three simp_lemma objects.

Empty norm_cast_cache.

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

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

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

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

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

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.

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

add_lemma cache decl infers the proper norm_cast attribute for decl and adds it to 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.

The norm_cast attribute.

meta def norm_cast.make_guess (decl : name) :

Classify a declaration as a norm_cast rule.

meta def norm_cast.get_label (decl : name) :

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

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,
end

meta def norm_cast.prove_eq_using (s : simp_lemmas) (a b : expr) :

Prove a = b using the given simp set.

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

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

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

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.

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.

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

meta def norm_cast.derive (e : expr) :

The core simplification routine of norm_cast.

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'.

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

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

meta def tactic.exact_mod_cast (e : expr) :

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

meta def tactic.apply_mod_cast (e : expr) :

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

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.

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

Rewrite with the given rules and normalize casts between steps.

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

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

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

the converter version of `norm_cast'

@[norm_cast]
theorem ite_cast {α : Sort u_1} {β : Sort u_2} [ β] {c : Prop} [decidable c] {a b : α} :
(ite c a b) = ite c a b
@[norm_cast]
theorem dite_cast {α : Sort u_1} {β : Sort u_2} [ β] {c : Prop} [decidable c] {a : c → α} {b : ¬c → α} :
(dite c a b) = dite c (λ (h : c), (a h)) (λ (h : ¬c), (b h))