feat: initial commit, adapted from mathlib4

mathlib4 commit: 2e3cdfaaa8ba1639dc092757cee447e77591ad00

Author: digama0

.github/workflows/build.yml

@@ -0,0 +1,40 @@
+on:
+  push:
+    branches-ignore:
+      # ignore tmp branches used by bors
+      - 'staging.tmp*'
+      - 'trying.tmp*'
+      - 'staging*.tmp'
+  pull_request:
+
+name: ci
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.3.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - uses: actions/checkout@v2
+
+      - name: update Std.lean
+        run: |
+          find Std -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Std.lean
+
+      - name: build std
+        run: lake build
+
+      - name: test std
+        run: make test
+
+      - name: lint std
+        run: make lint
+
+      - name: check that all files are imported
+        run: git diff --exit-code

.gitignore

@@ -0,0 +1,2 @@
+/build
+/prelude/build

.vscode/copyright.code-snippets

@@ -0,0 +1,13 @@
+{
+	"Copyright header for std": {
+		"scope": "lean4",
+		"prefix": "copyright",
+		"body": [
+			"/-",
+			"Copyright (c) ${CURRENT_YEAR} $1. All rights reserved.",
+			"Released under Apache 2.0 license as described in the file LICENSE.",
+			"Authors: $1",
+			"-/"
+		]
+	}
+}

.vscode/settings.json

@@ -0,0 +1,11 @@
+{
+  "editor.insertSpaces": true,
+  "editor.tabSize": 2,
+  "editor.rulers" : [100],
+  "files.encoding": "utf8",
+  "files.eol": "\n",
+  "files.insertFinalNewline": true,
+  "files.trimFinalNewlines": true,
+  "files.trimTrailingWhitespace": true,
+  "search.usePCRE2": true
+}

GNUmakefile

@@ -0,0 +1,16 @@
+TESTS = $(wildcard test/*.lean)
+
+.PHONY: all build test lint
+
+all: build test
+
+build:
+	lake build
+
+test: $(addsuffix .run, $(TESTS))
+
+test/%.run: build
+	lake env lean test/$*
+
+lint: build
+	./build/bin/runLinter

README.md

@@ -0,0 +1,20 @@
+# std4
+
+Work in progress standard library for Lean 4. This is a collection of data structures and tactics intended for use by both computer-science applications and mathematics applications of Lean 4.
+
+# Build instructions
+
+* Get the newest version of `elan`. If you already have installed a version of Lean, you can run
+  ```
+  elan self update
+  ```
+  If the above command fails, or if you need to install `elan`, run
+  ```
+  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
+  ```
+  If this also fails, follow the instructions under `Regular install` [here](https://leanprover-community.github.io/get_started.html).
+* To build `std4` run `lake build`. To build and run all tests, run `make`.
+* If you added a new file, run the following command to update `Std.lean`
+  ```
+  find Std -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Std.lean
+  ```

Std.lean

@@ -0,0 +1,10 @@
+import Std.Data.Array.Defs
+import Std.Lean.NameMapAttribute
+import Std.Tactic.Lint
+import Std.Tactic.Lint.Basic
+import Std.Tactic.Lint.Frontend
+import Std.Tactic.Lint.Misc
+import Std.Tactic.Lint.Simp
+import Std.Tactic.OpenPrivate
+import Std.Util.LibraryNote
+import Std.Util.TermUnsafe

Std/Data/Array/Defs.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2021 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur Paulino, Floris van Doorn
+-/
+
+/-!
+## Definitions on Arrays
+
+This file contains various definitions on `Array`. It does not contain
+proofs about these definitions, those are contained in other files in `Std.Data.Array`.
+-/
+
+namespace Array
+
+/-- The array `#[f 0, ..., f n]` -/
+def ofFn (n : Nat) (f : Fin n → α) : Array α :=
+  loop 0 (mkEmpty n)
+where
+  /-- Implementation detail of `Array.ofFn`. -/
+  loop (i : Nat) (acc : Array α) : Array α :=
+    if h : i < n then
+      let acc := acc.push (f ⟨i, h⟩)
+      loop (i + 1) acc
+    else
+      acc
+termination_by
+  loop i acc => n - i
+
+/-- The array `#[0, 1, ..., n - 1]`. -/
+def range (n : Nat) : Array Nat :=
+  n.fold (flip Array.push) #[]
+
+/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
+def reduceOption (l : Array (Option α)) : Array α :=
+  l.filterMap id
+
+/-- Turns `#[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` into `#[a₁, a₂, ⋯, b₁, b₂, ⋯]` -/
+def flatten (arr : Array (Array α)) : Array α :=
+  arr.foldl (init := #[]) fun acc a => acc.append a
+
+end Array

Std/Lean/NameMapAttribute.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2022 E.W.Ayers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: E.W.Ayers
+-/
+import Lean
+
+namespace Lean
+
+/-- Maps declaration names to α. -/
+def NameMapExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
+
+instance : Inhabited (NameMapExtension α) :=
+  inferInstanceAs <| Inhabited (SimplePersistentEnvExtension ..)
+
+def NameMapExtension.find? (ext : NameMapExtension α) (env : Environment) : Name → Option α :=
+  (SimplePersistentEnvExtension.getState ext env).find?
+
+/-- Add the given k,v pair to the NameMapExtension. -/
+def NameMapExtension.add [Monad M] [MonadEnv M] [MonadError M]
+  (ext : NameMapExtension α) (k : Name) (v : α) :  M Unit := do
+  if let some _ := ext.find? (←getEnv) k then
+    throwError "Already exists entry for {ext.name} {k}"
+  else
+     ext.addEntry (←getEnv) (k, v) |> setEnv
+
+def mkNameMapExtension (α) (name : Name): IO (NameMapExtension α) := do
+  registerSimplePersistentEnvExtension {
+    name          := name,
+    addImportedFn := fun ass => ass.foldl (init := ∅) fun
+                       | names, as => as.foldl (init := names) fun
+                         | names, (a,b) => names.insert a b,
+    addEntryFn    := fun s n => s.insert n.1 n.2 ,
+    toArrayFn     := fun es => es.toArray
+  }
+
+structure NameMapAttributeImpl (α : Type) where
+  name : Name
+  descr : String
+  add : (src : Name) → (stx : Syntax) →  AttrM α
+  deriving Inhabited
+
+/-- Similar to ParametricAttribute except that attributes do not
+have to be assigned in the same file as the declaration. -/
+structure NameMapAttribute (α) where
+  impl : NameMapAttributeImpl α
+  ext : NameMapExtension α
+  deriving Inhabited
+
+def NameMapAttribute.find? (attr : NameMapAttribute α)
+  : (env : Environment) → Name → Option α := attr.ext.find?
+
+def NameMapAttribute.add [Monad M] [MonadEnv M] [MonadError M]
+  (attr : NameMapAttribute α) (k : Name) (v : α) : M Unit :=
+  attr.ext.add k v
+
+def registerNameMapAttribute (impl : NameMapAttributeImpl α) : IO (NameMapAttribute α) := do
+  let ext ← mkNameMapExtension α impl.name
+  registerBuiltinAttribute {
+    name := impl.name
+    descr := impl.descr
+    add := fun src stx _kind => do
+      let a : α ← impl.add src stx
+      ext.add src a
+  }
+  return {
+    impl := impl
+    ext := ext
+  }
+
+
+end Lean

Std/Tactic/Lint.lean

@@ -0,0 +1,3 @@
+import Std.Tactic.Lint.Misc
+import Std.Tactic.Lint.Simp
+import Std.Tactic.Lint.Frontend

Std/Tactic/Lint/Basic.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+
+import Lean
+import Std.Util.TermUnsafe
+import Std.Lean.NameMapAttribute
+open Lean Meta
+
+namespace Std.Tactic.Lint
+
+/-!
+# Basic linter types and attributes
+
+This file defines the basic types and attributes used by the linting
+framework.  A linter essentially consists of a function
+`(declaration : Name) → MetaM (Option MessageData)`, this function together with some
+metadata is stored in the `Linter` structure. We define two attributes:
+
+ * `@[stdLinter]` applies to a declaration of type `Linter` and adds it to the default linter set.
+
+ * `@[nolint linterName]` omits the tagged declaration from being checked by
+   the linter with name `linterName`.
+-/
+
+syntax (name := nolint) "nolint" (ppSpace ident)+ : attr
+
+-- Defines the user attribute `nolint` for skipping `#lint`
+initialize nolintAttr : NameMapAttribute (Array Name) ←
+  registerNameMapAttribute {
+    name := `nolint
+    descr := "Do not report this declaration in any of the tests of `#lint`"
+    add := fun _decl stx =>
+      match stx with
+        -- TODO: validate linter names
+        | `(attr|nolint $[$ids]*) => pure $ ids.map (·.getId.eraseMacroScopes)
+        | _ => throwError "unexpected nolint syntax {stx}"
+  }
+
+/-- Returns true if `decl` should be checked
+using `linter`, i.e., if there is no `nolint` attribute. -/
+def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool :=
+  return !((nolintAttr.find? (← getEnv) decl).getD {}).contains linter
+
+/--
+Returns true if `decl` is an automatically generated declaration.
+
+Also returns true if `decl` is an internal name or created during macro
+expansion.
+-/
+def isAutoDecl (decl : Name) : CoreM Bool := do
+  if decl.hasMacroScopes then return true
+  if decl.isInternal then return true
+  if let Name.str n s := decl then
+    if s.startsWith "proof_" || s.startsWith "match_" then return true
+    if (← getEnv).isConstructor n && ["injEq", "inj", "sizeOf_spec"].any (· == s) then
+      return true
+    if let ConstantInfo.inductInfo _ := (← getEnv).find? n then
+      if [casesOnSuffix, recOnSuffix, brecOnSuffix, binductionOnSuffix, belowSuffix,
+          "ndrec", "ndrecOn", "noConfusionType", "noConfusion"].any (· == s) then
+        return true
+  pure false
+
+/--
+A linting test for the `#lint` command.
+
+`test` defines a test to perform on every declaration. It should never fail. Returning `none`
+signifies a passing test. Returning `some msg` reports a failing test with error `msg`.
+
+`noErrorsFound` is the message printed when all tests are negative, and `errorsFound` is printed
+when at least one test is positive.
+
+If `isFast` is false, this test will be omitted from `#lint-`.
+-/
+structure Linter where
+  test : Name → MetaM (Option MessageData)
+  noErrorsFound : MessageData
+  errorsFound : MessageData
+  isFast := true
+
+structure NamedLinter extends Linter where
+  declName : Name
+
+def NamedLinter.name (l : NamedLinter) : Name := l.declName.updatePrefix Name.anonymous
+
+def getLinter (declName : Name) : CoreM NamedLinter := unsafe
+  return { ← evalConstCheck Linter ``Linter declName with declName }
+
+/-- Takes a list of names that resolve to declarations of type `linter`,
+and produces a list of linters. -/
+def getLinters (l : List Name) : CoreM (List NamedLinter) :=
+  l.mapM getLinter
+
+-- Defines the user attribute `stdLinter` for adding a linter to the default set.
+initialize stdLinterAttr : TagAttribute ←
+  registerTagAttribute
+    (name := `stdLinter)
+    (descr := "Use this declaration as a linting test in #lint")
+    (validate := fun name => do
+      let constInfo ← getConstInfo name
+      unless ← (isDefEq constInfo.type (mkConst ``Linter)).run' do
+        throwError "must have type Linter, got {constInfo.type}")