Rewriting and automation
Rewrite in both directions and inside hypotheses, give simp the lemmas it needs, decide finite facts, solve linear arithmetic with omega, and write calc chains that show each step.
Progress is kept in this browser until you sign in
- Rewrite with an equalityrw [h] replaces the left side of h by its right side everywhere.9 min
- Rewrite in the other directionrw [← h] uses an equation right-to-left. Chain rewrites in one call.10 min
- Rewrite inside a hypothesisrw [h] at h2 changes a hypothesis instead of the goal.9 min
- Simplify a goalsimp normalizes with hundreds of known lemmas.8 min
- Point simp and rw at the right lemmasLibrary lemmas about lists and arithmetic, used by name.12 min
- Decide a finite factdecide evaluates a decidable proposition and produces a proof.8 min
- Linear arithmetic with omegaInequalities and natural-number subtraction, solved automatically.9 min
- Chain equalities with calcA readable proof that shows each rewriting step and its justification.12 min