v3.3.0

Lean version 3.3.0

Features

• In addition to user-defined notation parsers introduced in Lean 3.2.0, users may now also define top-level commands in Lean. For an example, see the coinductive command that has been ported to the new model.

• Add new simplifier configuration option simp_config.single_pass. It is useful for simplification rules that may produce non-termination.
  Example: simp {single_pass := tt}

• The rewrite tactic has support for equational lemmas. Example: Given a definition f, rw [f] will try to rewrite the goal using the equational lemmas for f.
  The tactic fails if none of the equational lemmas can be used.

• Add simp * at * variant. It acts on all (non dependent propositional) hypotheses.
  Simplified hypotheses are automatically inserted into the simplification set
  as additional simplification rules.

• Add «id» notation that can be used to declare and refer to identifiers containing prohibited characters.
  For example, a.«b.c» is a two-part identifier with parts a and b.c.

• simp tactic now handles lemmas with metavariables. Example simp [add_comm _ b].

• conv { ... } tactic for applying simplification and rewriting steps.
  In the block {...}, we can use tactics from conv.interactive.
  Examples:

  • conv at h in (f _ _) { simp } applies simp to first subterm matching f _ _ at hypothesis h.
  • conv in (_ = _) { to_lhs, whnf } replace the left-hand-side of the equality in target with its weak-head-normal-form.
  • conv at h in (0 + _) { rw [zero_add] }
  • conv { for (f _ _) [1, 3] {rw [h]}, simp }, first execute rw[h] to the first and third occurrences of an f-application,
    and then execute simp.

• simp tactics in interactive mode have a new configuration parameter (discharger : tactic unit)
  a tactic for discharging subgoals created by the simplifier. If the tactic fails, the simplifier
  tries to discharge the subgoal by reducing it to true.
  Example: simp {discharger := assumption}.

• simp and dsimp can be used to unfold projection applications when the argument is a type class instance.
  Example: simp [has_add.add] will replace @has_add.add nat nat.has_add a b with nat.add a b

• dsimp has several new configuration options to control reduction (e.g., iota, beta, zeta, ...).

• Non-exhaustive pattern matches now show missing cases.

• induction e now also works on non-variable e. Unlike ginduction, it will not introduce equalities relating e to the inductive cases.

• Add notation #[a, b, c, d] for bin_tree.node (bin_tree.node (bin_tree.leaf a) (bin_tree.leaf b)) (bin_tree.node (bin_tree.leaf c) (bin_tree.leaf d)).
  There is a coercion from bin_tree to list. The new notation allows to input long sequences efficiently.
  It also prevents system stack overflows.

• Tactics that accept a location parameter, like rw thm at h, may now use ⊢ or the ASCII version |-
  to select the goal as well as any hypotheses, for example rw thm at h1 h2 ⊢.

• Add user_attribute.after_set/before_unset handlers that can be used for validation as well as side-effecting attributes.

• Field notation can now be used to make recursive calls.

def list.append : list α → list α → list α
| []       l := l
| (h :: s) t := h :: s.append t

• leanpkg now stores the intended Lean version in the leanpkg.toml file and reports a warning if the version does not match the installed Lean version.

• simp and dsimp can now unfold let-bindings in the local context. Use dsimp [x] or simp [x] to unfold the let-binding x : nat := 3.

• User-defined attributes can now take parameters parsed by a lean.parser. A [derive] attribute that can derive typeclasses such as decidable_eq and inhabited has been implemented on top of this.

Changes

• We now have two type classes for converting to string: has_to_string and has_repr.
  The has_to_string type class in v3.2.0 is roughly equivalent to has_repr.
  For more details, see discussion here.

• Merged assert and note tactics and renamed -> have.

• Renamed pose tactic -> let

• assume is now a real tactic that does not exit tactic mode.

• Modified apply tactic configuration object, and implemented RFC #1342. It now has support for auto_param and opt_param. The new eapply tactic only creates subgoals for non dependent premises, and it simulates the behavior of the apply tactic in version 3.2.0.

• Add configuration object rewrite_cfg to rw/rewrite tactic. It now has support for auto_param and opt_param.
  The new goals are ordered using the same strategies available for apply.

• All dsimp tactics fail if they did not change anything.
  We can simulate the v3.2.0 using dsimp {fail_if_unchaged := ff} or try dsimp.

• dsimp does not unfold reducible definitions by default anymore.
  Example: function.comp applications will not be unfolded by default.
  We should use dsimp [f] if we want to reduce a reducible definition f.
  Another option is to use the new configuration parameter unfold_reducible.
  Example dsimp {unfold_reducible := tt}

• All dunfold and unfold tactics fail if they did not unfold anything.
  We can simulate the v3.2.0 using unfold f {fail_if_unchaged := ff} or try {unfold f}.

• dunfold_occs was deleted, the new conv tactical should be used instead.

• unfold tactic is now implemented on top of the simp tactics. So, we can use it to unfold
  declarations defined using well founded recursion. The unfold1 variant does not unfold recursively,
  and it is shorthand for unfold f {single_pass := tt}.
  Remark: in v3.2.0, unfold was just an alias for the dunfold tactic.

• Deleted simph and simp_using_hs tactics. We should use simp [*] instead.

• Use simp [-h] and dsimp [-h] instead of simp without h and dsimp without h.
  Moreover, simp [*, -h] if h is a hypothesis, we are adding all hypotheses but h
  as additional simplification lemmas.

• Changed notation rw [-h] to rw [← h] to avoid confusion with the new simp [-h] notation.
  The ASCII version rw [<- h] is also supported.

• rw [t] at * now skips any hypothesis used by t. See discussion here.

• Removed the redundant keywords take (replace with assume) and suppose (replace with the new anonymous assume :)

• Universes max u v + 1 and imax u v + 1 are now parsed as (max u v) + 1 and (imax u v) + 1.

• Merged generalize and generalize2 tactics into new generalize id? : expr = id tactic

• standard.lean has been removed. Any files that import standard can simply remove the line as
  most things that were once imported by this are now imported by default.

• The type classes for orders have been refactored to combine both the (<)
  and (≤) operations. The new classes are preorder, partial_order, and
  linear_order. The partial_order class corresponds to weak_order,
  strict_order, order_pair, and strong_order_pair. The linear_order
  class corresponds to linear_order_pair, and linear_strong_order_pair.

• injection and injections tactics generate fresh names when user does not provide names.
  The fresh names are of the form h_<idx>. See discussion here.

• Use structure to declare and. This change allows us to use h.1 and h.2 as shorthand for h.left and h.right.

• Add attribute [pp_using_anonymous_constructor] to and. Now, and.intro h1 h2 is pretty printed as
  ⟨h1, h2⟩. This change is motivated by the previous one. Without it, and.intro h1 h2 would be
  pretty printed as {left := h1, right := h2}.

• User attributes can no longer be set with set_basic_attribute. You need to use user_attribute.set now.

API name changes

• list.dropn => list.drop
• list.taken => list.take
• tactic.dsimp and tactic.dsimp_core => tactic.dsimp_target
• tactic.dsimp_at_core and tactic.dsimp_at => tactic.dsimp_hyp
• tactic.delta_expr => tactic.delta
• tactic.delta => tactic.delta_target
• tactic.delta_at => tactic.delta_hyp
• tactic.simplify_goal => tactic.simp_target
• tactic.unfold_projection => tactic.unfold_proj
• tactic.unfold_projections_core => tactic.unfold_projs
• tactic.unfold_projections => tactic.unfold_projs_target
• tactic.unfold_projections_at => tactic.unfold_projs_hyp
• tactic.simp_intros_using, tactic.simph_intros_using, tactic.simp_intro_lst_using, tactic.simph_intro_lst_using => tactic.simp_intros
• tactic.simp_at => tactic.simp_hyp
• deleted tactic.simp_at_using
• deleted tactic.simph_at