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 #
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,
has_lift_t ℤ ℕ
mk_instance_fast is used when we assume the type class search
should end instantly.
label is a type used to classify
- 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
The type of the
The optional label is used to overwrite the classifier.
push_cast rewrites the expression to move casts toward the leaf nodes.
↑(a + b) will be written to
↑a + ↑b.
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
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.