Rewriting, simplification, automation
Most proof steps in practice are rewrites and simplifications. You will rewrite in both directions and inside hypotheses, drive the simplifier with your own lemmas, decide finite facts, dispatch arithmetic with omega, and write readable calc chains.
Sign in to track your progress
- 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