v3.4.0

Features

• Implement RFC #1820

• Add string.iterator abstraction for traversing strings.
  The VM contains an efficient implementation of this type.

• Add support for non-ASCII char literals. Example: 'α'.

• Unicode escape characters in string and char literals. For example, '\u03B1' is equivalent to 'α'.

• Predictable runtime cost model for recursive functions. The equation compiler uses
  different techniques for converting recursive equations into recursors and/or
  well-founded fixed points. The new approach used in the code generator ignores
  these encoding tricks when producing byte code. So, the runtime cost model
  is identical to the one in regular strict functional languages.

• Add d_array n α (array type where value type may depend on index),
  where (α : fin n → Type u).

• Add instance for decidable_eq (d_array n α) and decidable_eq (array n α).
  The new instance is more efficient than the one in mathlib because it doesn't
  convert the array into a list.

• Add aliasing pattern syntax id@pat, which introduces the name id for the value matched by
  the pattern pat.

• Add alternative syntax {..., ..s} for the structure update {s with ...}.
  Multiple fallback sources can be given: {..., ..s, ..t} will fall back to
  searching a field in s, then in t. The last component can also be ..,
  which will replace any missing fields with a placeholder.
  The old notation will be removed in the future.

• Add support for structure instance notation {...} in patterns. Use .. to ignore
  unmatched fields.

• Type class has_equiv for ≈ notation.

• Add funext ids* tactic for applying the funext lemma.

• Add iterate n { t } for applying tactic t n times.
  Remark: iterate { t } applies t until it fails.

• Add with_cases { t }. This tactic applies t to the main goal,
  and reverts any new hypothesis in the resulting subgoals. with_cases also enable "goal tagging".
  Remark: induction and cases tag goals using constructor names. apply and constructor tag goals
  using parameter names. The case tactic can select goals using tags.

• Add cases_matching p tactic for applying the cases tactic to a hypothesis h : t s.t.
  t matches the pattern p. Alternative versions: cases_matching* p and cases_matching [p_1, ..., p_n].
  Example: cases_matching* [_ ∨ _, _ ∧ _] destructs all conjunctions and disjunctions in the main goal.

• Add cases_type I tactic for applying the cases tactic to a hypothesis h : I ....
  cases_type! I only succeeds when the number of resulting goals is <= 1.
  Alternative versions: cases_type I_1 ... I_n, cases_type* I, cases_type!* I.
  Example: cases_type* and or destructs all conjunctions and disjunctions in the main goal.

• Add constructor_matching p tactic. It is syntax sugar for match_target p; constructor.
  The variant constructor_matching* p is more efficient than focus1 { repeat { match_target p; constructor } }
  because the patterns are compiled only once.

• injection h now supports nested and mutually recursive datatypes.

• Display number of goals in the *Lean Goal* buffer (if number of goals > 1).

• hide id* command for hiding aliases.
  The following command hides the alias is_true for decidable.is_true.

  hide is_true
  

• Add abbreviation declaration command. abbreviation d : t := v is equivalent to
  @[reducible, inline] def d : t := v and a kernel reducibility hint.
  Before this command, we had to use meta programming for setting the kernel reducibility hint.
  This was problematic because we could only define abbreviations after the meta programming
  framework was defined.

• Add "smart unfolding". The idea is to prevent internal compilation details
  used by the equation compiler to "leak" during unification, tactic execution and
  reduction. With "smart unfolding", the term nat.add a (nat.succ b) reduces
  to nat.succ (nat.add a b) instead of nat.succ (... incomprehensible mess ...).
  This feature addresses a problem reported by many users.
  See issue #1794.
  The command set_option type_context.smart_unfolding false disables this feature.

• Add support for "auto params" at simp tactic. Example: given

  @[simp] lemma fprop1 (x : nat) (h : x > 0 . tactic.assumption) : f x = x := ...
  

  The simplifier will try to use tactic assumption to synthesize parameter h.

• Add interactive sorry tactic (alias for admit).

• simp now reduces equalities c_1 ... = c_2 ... to false if c_1 and c_2 are distinct
  constructors. This feature can be disabled using simp {constructor_eq := ff}.

• simp now reduces equalities c a_1 ... a_n = c b_1 ... b_n to a_1 = b_1 /\ ... /\ a_n = b_n if c is a constructor.
  This feature can be disabled using simp {constructor_eq := ff}.

• subst and subst_vars now support heterogeneous equalities that are actually homogeneous
  (i.e., @heq α a β b where α and β are definitionally equal).

• Add interactive subst_vars tactic.

• Add leanpkg add foo/bar as a shorthand for leanpkg add https://github.com/foo/bar.

• Add leanpkg help <command>.

• Add [norm] simp set. It contains all lemmas tagged with [simp] plus any
  lemma tagged with [norm].
  These rules are used to produce normal forms and/or reduce the
  number of constants used in a goal. For example, we plan to
  add the lemma f <$> x = x >>= pure ∘ f to [norm].

• Add iota_eqn : bool field to simp_config. simp {iota_eqn := tt} uses
  all non trivial equation lemmas generated by equation/pattern-matching compiler.
  A lemma is considered non trivial if it is not of the form forall x_1 ... x_n, f x_1 ... x_n = t and
  a proof by reflexivity. simp! is a shorthand for simp {iota_eqn := tt}.
  For example, given the goal ... |- [1,2].map nat.succ = t, simp! reduces the left-hand-side
  of the equation to [nat.succ 1, nat.succ 2]. In this example, simp! is equivalent to
  simp [list.map].

• Allow the Script, Double-struck, and Fractur symbols from
  Mathematical Alphanumeric Symbols: https://unicode.org/charts/PDF/U1D400.pdf
  to be used as variables Example: variables 𝓞 : Prop.

• Structure instance notation now allows explicitly setting implicit structure fields

• Structure instance notation now falls back to type inference for inferring the
  value of a superclass. This change eliminates the need for most .. source specifiers
  in instance declarations.

• The --profile flag will now print cumulative profiling times at the end of execution

• do notation now uses the top-level, overloadable bind function instead of has_bind.bind,
  allowing binds with different type signatures

• Structures fields can now be defined with an implicitness infer annotation and parameters.

  class has_pure (f : Type u → Type v) :=
  -- make f implicit
  (pure {} {α : Type u} : α → f α)
  

• Add except_t and reader_t monad transformers

• Add monad_{except,reader,state} classes for accessing effects anywhere in a monad stack
  without the need for explicit lifting. Add analogous monad_{except,reader,state}_adapter
  classes for translating a monad stack into another one with the same shape but different
  parameter types.

Changes

• Command variable [io.interface] is not needed anymore to use the io monad.
  It is also easier to add new io primitives.

• Replace inout modifier in type class declarations with out_param modifier.
  Reason: counterintuitive behavior in the type class resolution procedure.
  The result could depend on partial information available in the inout
  parameter. Now a parameter (R : inout α → β → Prop) should be written
  as (R : out_param (α → β → Prop)) or (R : out_param $ α → β → Prop).
  Remark: users may define their own notation for declaring out_params.
  Example:

  notation `out`:1024 a:0 := out_param a
  

  We did not include this notation in core lib because out is frequently used to
  name parameters, local variables, etc.

• case tactic now supports the with_cases { t } tactic. See entry above about with_cases.
  The tag and new hypotheses are now separated with :. Example:

  • case pos { t }: execute tactic t to goal tagged pos
  • case pos neg { t }: execute tactic t to goal tagged pos neg
  • case : x y { t }: execute tactic t to main goal after renaming the first two hypotheses produced by preceding with_case { t' }.
  • case pos neg : x y { t } : execute tactic t to goal tagged pos neg after renaming the first two hypotheses produced by preceding with_case { t' }.

• cases h now also tries to clear h when performing dependent elimination.

• repeat { t } behavior changed. Now, it applies t to each goal. If the application succeeds,
  the tactic is applied recursively to all the generated subgoals until it eventually fails.
  The recursion stops in a subgoal when the tactic has failed to make progress.
  The previous repeat tactic was renamed to iterate.

• The automatically generated recursor C.rec for an inductive datatype
  now uses ih to name induction hypotheses instead of ih_1 if there is only one.
  If there is more than one induction hypotheses, the name is generated by concatenating ih_
  before the constructor field name. For example, for the constructor

  | node (left right : tree) (val : A) : tree
  

  The induction hypotheses are now named: ih_left and ih_right.
  This change only affects tactical proofs where explicit names are not provided
  to induction and cases tactics.

• induction h and cases h tactic use a new approach for naming new hypotheses.
  If names are not provided by the user, these tactics will create a "base" name
  by concatenating the input hypothesis name with the constructor field name.
  If there is only one field, the tactic simply reuses the hypothesis name.
  The final name is generated by making sure the "base" name is unique.
  Remarks:

  • If h is not a hypothesis, then no concatenation is performed.
  • The old behavior can be obtained by using the following command

  set_option tactic.induction.concat_names false
  

  This change was suggested by Tahina Ramananandro. The idea is to have more
  robust tactic scripts when helper tactics that destruct many hypotheses automatically
  are used.
  Remark: The new guard_names { t } tactical can be used to generate
  robust tactic scripts that are not sensitive to naming generation strategies used by t.

• Remove [simp] attribute from lemmas or.assoc, or.comm, or.left_comm, and.assoc, and.comm, and.left_comm, add_assoc, add_comm, add_left_com, mul_assoc, mul_comm and mul_left_comm.
  These lemmas were being used to "sort" arguments of AC operators: and, or, (+) and (*).
  This was producing unstable proofs. The old behavior can be retrieved by using the commands local attribute [simp] ... or attribute [simp] ... in the affected files.

• string is now a list of unicode scalar values. Moreover, in the VM,
  strings are implemented as an UTF-8 encoded array of bytes.

• array α n is now written array n α. Motivation: consistency d_array n α.

• Move rb_map and rb_tree to the native namespace. We will later add
  pure Lean implementations. Use open native to port files.

• apply t behavior changed when type of t is of the form forall (a_1 : A_1) ... (a_n : A_n), ?m ..., where ?m is an unassigned metavariable.
  In this case, apply t behaves as apply t _ ... _ where n _ have been added, independently of the goal target type.
  The new behavior is useful when using apply with eliminator-like definitions.

• ginduction t with h h1 h2 is now induction h : t with h1 h2.

• apply_core now also returns the parameter name associated with new metavariables.

• apply now also returns the new metavariables (and the parameter name associated with them). Even the assigned metavariables are returned.

• by_cases p with h ==> by_cases h : p

• leanpkg now always stores .lean package files in a separate src directory.

• Structure constructor parameters representing superclasses are now marked as instance implicit.
  Note: Instances using the {...} structure notation should not be affected by this change.

• The monad laws have been separated into new type classes is_lawful_{functor,applicative,monad}.

• unit is now an abbreviation of punit.{0}

API name changes

• monad.has_monad_lift(_t) ~> has_monad_lift(_t)
• monad.map_comp ~> comp_map
• state(_t).{read,write} ~> {get,put} (general operations defined on any monad_state)
• deleted monad.monad_transformer
• deleted monad.lift{n}. Use f <$> a1 <*> ... <*> an instead of monad.lift{n} f a1 ... an.
• merged has_map into functor
• unit_eq(_unit) ~> punit_eq(_punit)