lean4-htt/RELEASES.md

v4.0.0-m4 (WIP)

• Support notation let <pattern> := <expr> | <else-case> in do blocks.

• Remove support for "auto" pure. In the Zulip thread, the consensus seemed to be that "auto" pure is more confusing than it's worth.

• Remove restriction in congr theorems that all function arguments on the left-hand-side must be free variables. For example, the following theorem is now a valid congr theorem.

@[congr]
theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] :
                  ∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩ :=

• Partially applied congruence theorems.

• Improve elaboration postponement heuristic when expected type is a metavariable. Lean now reduces the expected type before performing the test.

• Remove deprecated leanpkg in favor of Lake now bundled with Lean.

• Various improvements to go-to-definition & find-all-references accuracy.

• Auto generated congruence lemmas with support for casts on proofs and Decidable instances (see whishlist).

• Rename option autoBoundImplicitLocal => autoImplicit.

• Relax auto-implicit restrictions. The command set_option relaxedAutoImplicit false disables the relaxations.

• contradiction tactic now closes the goal if there is a False.elim application in the target.

• Renamed tatic byCases => by_cases (motivation: enforcing naming convention).

• Local instances occurring in patterns are now considered by the type class resolution procedure. Example:

def concat : List ((α : Type) × ToString α × α) → String
  | [] => ""
  | ⟨_, _, a⟩ :: as => toString a ++ concat as

• Notation for providing the motive for match expressions has changed. Before:

match x, rfl : (y : Nat) → x = y → Nat with
| 0,   h => ...
| x+1, h => ...

Now:

match (motive := (y : Nat) → x = y → Nat) x, rfl with
| 0,   h => ...
| x+1, h => ...

With this change, the notation for giving names to equality proofs in match-expressions is not whitespace sensitive anymore. That is, we can now write

match h : sort.swap a b with
| (r₁, r₂) => ... -- `h : sort.swap a b = (r₁, r₂)`

• (generalizing := true) is the default behavior for match expressions even if the expected type is not a proposition. In the following example, we used to have to include (generalizing := true) manually.

inductive Fam : Type → Type 1 where
  | any : Fam α
  | nat : Nat → Fam Nat

example (a : α) (x : Fam α) : α :=
  match x with
  | Fam.any   => a
  | Fam.nat n => n

• We now use PSum (instead of Sum) when compiling mutually recursive definitions using well-founded recursion.

• Better support for parametric well-founded relations. See issue #1017. This change affects the low-level termination_by' hint because the fixed prefix of the function parameters in not "packed" anymore when constructing the well-founded relation type. For example, in the following definition, as is part of the fixed prefix, and is not packed anymore. In previous versions, the termination_by' term would be written as measure fun ⟨as, i, _⟩ => as.size - i

def sum (as : Array Nat) (i : Nat) (s : Nat) : Nat :=
  if h : i < as.size then
    sum as (i+1) (s + as.get ⟨i, h⟩)
  else
    s
termination_by' measure fun ⟨i, _⟩ => as.size - i

• Add while <cond> do <do-block>, repeat <do-block>, and repeat <do-block> until <cond> macros for do-block. These macros are based on partial definitions, and consequently are useful only for writing programs we don't want to prove anything about.

• Add arith option to Simp.Config, the macro simp_arith expands to simp (config := { arith := true }). Only Nat and linear arithmetic is currently supported.

• Add fail msg? tactic that always fail.

• Add support for acyclicity at dependent elimination. See issue #1022.

• Add trace <string> tactic for debugging purposes.