Skip to content

nightly-2022-04-03

Pre-release
Pre-release
Compare
Choose a tag to compare
@leodemoura leodemoura released this 03 Apr 07:46
· 1 commit to main since this release
nightly-2022-04-03
ca9b494

Changes since nightly-2022-04-02:

  • Add support for for h : i in [start:stop] do .. where h : i ∈ [start:stop]. This feature is useful for proving
    termination of functions such as:
inductive Expr where
  | app (f : String) (args : Array Expr)

def Expr.size (e : Expr) : Nat := Id.run do
  match e with
  | app f args =>
    let mut sz := 1
    for h : i in [: args.size] do
      -- h.upper : i < args.size
      sz := sz + size (args.get ⟨i, h.upper⟩)
    return sz

  • Add tactic case'. It is similar to case, but does not admit the goal on failure.
    For example, the new tactic is useful when writing tactic scripts where we need to use case'
    at first | ... | ..., and we want to take the next alternative when case' fails.

  • Add tactic macro

macro "stop" s:tacticSeq : tactic => `(repeat sorry)

See discussion on Zulip.

  • When displaying goals, we do not display inaccessible proposition names
    if they do not have forward dependencies. We still display their types.
    For example, the goal
case node.inl.node
β : Type u_1
b : BinTree β
k : Nat
v : β
left : Tree β
key : Nat
value : β
right : Tree β
ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
h✝ : k < key
a✝³ : BST left
a✝² : ForallTree (fun k v => k < key) left
a✝¹ : BST right
a✝ : ForallTree (fun k v => key < k) right
⊢ BST left

is now displayed as

case node.inl.node
β : Type u_1
b : BinTree β
k : Nat
v : β
left : Tree β
key : Nat
value : β
right : Tree β
ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
 : k < key
 : BST left
 : ForallTree (fun k v => k < key) left
 : BST right
 : ForallTree (fun k v => key < k) right
⊢ BST left

Full commit log

  • ca9b494 chore: use specialize tactic
  • d7abecd test: addDecorations without partial
  • c873ad6 test: recursive function on Syntax without partial
  • 9d55d7b feat: add helper tactic for applying List.sizeOf_lt_of_mem in termination proofs
  • 64cfbc1 feat: add helper tactic for applying sizeOf (a.get i) < sizeOf a automatically in termination proofs
  • 562af50 feat: add ForIn' instance for Range
  • 2c7c747 feat: add case' tactic for writing macros
  • 443dd79 feat: sizeOf theorems for Lean.Name
  • 03ec8cb feat: missing sizeOf theorems for Array.get and List.get
  • 9f29d7e feat: add stop tactic macro
  • 3d4e628 chore: fix link to examples
  • 78007be test: for Lean 3 hover issue reported on Zulip
  • 4fa5f50 feat: implement TODO at "fixed indices to parameters"
  • 9fe5458 feat: do not display inaccessible proposition names if they do not have forward dependencies
  • 95bd55b chore: fix typo and remove unnecessary discriminant
  • 4fcc7c7 chore: update LeanInk
  • d65ceaf chore: break long lines
  • 9ee3cb6 chore: formatting
  • e4fb9c8 chore: break long lines
  • 375692c doc: explain attribute [local simp]
  • 16649be doc: explain details
  • dee5dbc chore: cleanup example
  • 7f00352 chore: backtick issue in documentation
Assets 12