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