Merge branch 'leanprover:master' into master

.github/workflows/nix-ci.yml

@@ -78,8 +78,7 @@ jobs:
       - name: Build
         run: |
           # .o files are not a runtime dependency on macOS because of lack of thin archives
-          # leanc_src is required for building Leanc-deps
-          nix build $NIX_BUILD_ARGS .#stage0 .#stage1.lean-all .#lean-bin-tools-unwrapped.leanc_src .#Lean.oTree .#iTree .#modDepsFiles -o push-build
+          nix build $NIX_BUILD_ARGS .#stage0 .#stage1.lean-all .#Lean.oTree .#iTree .#modDepsFiles -o push-build
       - name: Test
         run: |
           nix build $NIX_BUILD_ARGS .#test -o push-test

doc/declarations.md

@@ -74,7 +74,7 @@ Lean provides ways of adding new objects to the environment. The following provi
 * ``axiom c : α`` :  declare a constant named ``c`` of type ``α``, it is postulating that `α` is not an empty type.
 * ``def c : α := v`` : defines ``c`` to denote ``v``, which should have type ``α``.
 * ``theorem c : p := v`` : similar to ``def``, but intended to be used when ``p`` is a proposition.
-* ``constant c : α (:= v)?`` : declares a opaque constant named ``c`` of type ``α``, the optional value `v` is must have type `α`
+* ``opaque c : α (:= v)?`` : declares a opaque constant named ``c`` of type ``α``, the optional value `v` is must have type `α`
   and can be viewed as a certificate that ``α`` is not an empty type. If the value is not provided, Lean tries to find one
   using a proceture based on type class resolution. The value `v` is hidden from the type checker. You can assume that
   Lean "forgets" `v` after type checking this kind of declaration.
@@ -89,8 +89,8 @@ Any of ``def``, ``theorem``, ``axiom``, or ``example`` can take a list of argume
 is interpreted as ``def foo : (a : α) → β := fun a : α => t``. Similarly, a theorem ``theorem foo (a : α) : p := t`` is interpreted as ``theorem foo : ∀ a : α, p := fun a : α => t``.
 
 ```lean
-constant c : Nat
-constant d : Nat
+opaque c : Nat
+opaque d : Nat
 axiom cd_eq : c = d
 
 def foo : Nat := 5

doc/dev/ffi.md

@@ -43,6 +43,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   * it is none of the types described above
   * it is not marked `unsafe`
   * it has a single constructor with a single parameter of *relevant* type
+
   is represented by the representation of that parameter's type.
   
   For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.

doc/examples/ICERM2022/ctor.lean

@@ -0,0 +1,46 @@
+import Lean
+
+open Lean Meta
+
+def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
+  /- Set `MetaM` context using `mvarId` -/
+  withMVarContext mvarId do 
+    /- Fail if the metavariable is already assigned. -/
+    checkNotAssigned mvarId `ctor
+    /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
+    let target ← getMVarType' mvarId
+    let .const declName us := target.getAppFn
+      | throwTacticEx `ctor mvarId "target is not an inductive datatype"
+    let .inductInfo { ctors, .. } ← getConstInfo declName
+      | throwTacticEx `ctor mvarId "target is not an inductive datatype"
+    if idx = 0 then
+      throwTacticEx `ctor mvarId "invalid index, it must be > 0"  
+    else if h : idx - 1 < ctors.length then
+      apply mvarId (.const ctors[idx - 1] us)
+    else
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"  
+
+open Elab Tactic
+
+elab "ctor" idx:num : tactic => 
+  liftMetaTactic (ctor · idx.getNat)
+
+example (p : Prop) : p := by 
+  ctor 1 -- Error
+
+example (h : q) : p ∨ q := by 
+  ctor 0 -- Error
+  exact h
+
+example (h : q) : p ∨ q := by 
+  ctor 3 -- Error
+  exact h
+
+example (h : q) : p ∨ q := by 
+  ctor 2
+  exact h
+
+example (h : q) : p ∨ q := by 
+  ctor 1
+  exact h -- Error 
+

doc/examples/ICERM2022/meta.lean

@@ -0,0 +1,80 @@
+import Lean
+
+open Lean Meta
+
+def ex1 (declName : Name) : MetaM Unit := do
+  let info ← getConstInfo declName
+  IO.println s!"{declName} : {← ppExpr info.type}"
+  if let some val := info.value? then 
+    IO.println s!"{declName} : {← ppExpr val}"
+
+#eval ex1 ``Nat
+
+def ex2 (declName : Name) : MetaM Unit := do
+  let info ← getConstInfo declName
+  trace[Meta.debug] "{declName} : {info.type}"
+  if let some val := info.value? then 
+    trace[Meta.debug] "{declName} : {val}"
+
+#eval ex2 ``Add.add
+
+set_option trace.Meta.debug true in
+#eval ex2 ``Add.add
+
+def ex3 (declName : Name) : MetaM Unit := do
+  let info ← getConstInfo declName
+  forallTelescope info.type fun xs type => do
+    trace[Meta.debug] "hypotheses : {xs}"
+    trace[Meta.debug] "resultType : {type}"
+    for x in xs do
+      trace[Meta.debug] "{x} : {← inferType x}"
+
+def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
+  if a < b then 
+    a
+  else 
+    b
+
+set_option trace.Meta.debug true in
+#eval ex3 ``myMin
+
+def ex4 : MetaM Unit := do
+  let nat := mkConst ``Nat
+  withLocalDeclD `a nat fun a => 
+  withLocalDeclD `b nat fun b => do
+    let e ← mkAppM ``HAdd.hAdd #[a, b]
+    trace[Meta.debug] "{e} : {← inferType e}"
+    let e ← mkAdd a (mkNatLit 5)
+    trace[Meta.debug] "added 5: {e}"
+    let e ← whnf e
+    trace[Meta.debug] "whnf: {e}"
+    let e ← reduce e
+    trace[Meta.debug] "reduced: {e}"
+    let a_plus_1 ← mkAdd a (mkNatLit 1)
+    let succ_a   := mkApp (mkConst ``Nat.succ) a
+    trace[Meta.debug] "({a_plus_1} =?= {succ_a}) == {← isDefEq a_plus_1 succ_a}"
+    let m ← mkFreshExprMVar nat
+    let m_plus_1 ← mkAdd m (mkNatLit 1)
+    trace[Meta.debug] "m_plus_1: {m_plus_1}"
+    unless (← isDefEq m_plus_1 succ_a) do throwError "isDefEq failed"
+    trace[Meta.debug] "m_plus_1: {m_plus_1}"
+
+set_option trace.Meta.debug true in
+#eval ex4
+
+open Elab Term
+
+def ex5 : TermElabM Unit := do
+  let nat := Lean.mkConst ``Nat
+  withLocalDeclD `a nat fun a => do 
+  withLocalDeclD `b nat fun b => do
+    let ab ← mkAppM ``HAdd.hAdd #[a, b]
+    let stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
+    let e ← elabTerm stx none
+    trace[Meta.debug] "{e} : {← inferType e}"
+    let e := mkApp e (mkNatLit 5)
+    let e ← whnf e
+    trace[Meta.debug] "{e}"
+
+set_option trace.Meta.debug true in
+#eval ex5

doc/examples/ICERM2022/notation.lean

@@ -0,0 +1,49 @@
+import Lean
+
+def f (x y : Nat) := x * y + 1
+
+infixl:65 " *' " => f
+
+#check 2 *' 3
+
+notation "unitTest " x => Prod.mk x ()
+
+#check unitTest 42
+
+notation "parenthesisTest " x => Nat.sub (x)
+#check parenthesisTest 12
+
+def Set (α : Type u) := α → Prop
+def setOf {α : Type} (p : α → Prop) : Set α := p
+notation "{ " x " | " p " }" => setOf (fun x => p)
+
+#check { x | x ≤ 1 }
+
+notation "cdotTest " "(" x ", " y ")" => Prod.map (· + 1) (1 + ·) (x, y)
+
+#check cdotTest (13, 12)
+
+notation "tupleFunctionTest " "(" x ", " y ")"=> Prod.map (Nat.add 1) (Nat.add 2) (x, y)
+
+#check tupleFunctionTest (15, 12)
+
+notation "diag " x => Prod.mk x x
+
+#check diag 12
+
+open Lean Meta PrettyPrinter Delaborator SubExpr in
+@[delab app.Prod.mk] def delabDoubleRhsTest : Delab := do
+   let e ← getExpr
+   let #[_, _, x, y] := e.getAppArgs | failure
+   guard (← isDefEq x y) 
+   let stx ← withAppArg delab
+   `(diag $stx)     
+
+#check diag 3
+#check (3, 3)
+#check (3, 4)
+#check (2+1, 3)
+#check (true, true)
+
+
+

doc/examples/palindromes.lean

@@ -48,7 +48,7 @@ Note that we use `(by simp)` to prove that `a₂ :: as ≠ []` in the recursive
 -/
 def List.last : (as : List α) → as ≠ [] → α
   | [a],         _ => a
-  | a₁::a₂:: as, _ => (a₂::as).last (by simp)
+  | _::a₂:: as, _ => (a₂::as).last (by simp)
 
 /-!
 We use the function `List.last` to prove the following theorem that says that if a list `as` is not empty,

doc/flake.nix

@@ -40,7 +40,7 @@
           # necessary for `additional-css`...?
           cp -r --no-preserve=mode $src/doc/* .
           # overwrite stub .lean.md files
-          cp -r ${examples}/* .
+          cp -r ${examples}/* examples/
           mdbook build -d $out
         '';
       };
@@ -78,16 +78,17 @@
           (with python3Packages; [ pygments dominate beautifulsoup4 docutils ]);
         doCheck = false;
       };
-      examples = let
-        renderLean = name: file: runCommandNoCC "${name}.md" { buildInputs = [ alectryon ]; } ''
-          mkdir -p $out/examples
-          alectryon --frontend lean4+markup ${file} --backend webpage -o $out/examples/${name}.md
-        '';
-        ents = builtins.readDir ./examples;
+      renderLean = name: file: runCommandNoCC "${name}.md" { buildInputs = [ alectryon ]; } ''
+        mkdir -p $out/examples
+        alectryon --frontend lean4+markup ${file} --backend webpage -o $out/${name}.md
+      '';
+      renderDir = name: dir: let
+        ents = builtins.readDir dir;
         inputs = lib.filterAttrs (n: t: builtins.match ".*\.lean" n != null && t == "regular") ents;
-        outputs = lib.mapAttrs (n: _: renderLean n ./examples/${n}) inputs;
+        outputs = lib.mapAttrs (n: _: renderLean n "${dir}/${n}") inputs;
       in
-        outputs // symlinkJoin { name = "examples"; paths = lib.attrValues outputs; };
+        outputs // symlinkJoin { inherit name; paths = lib.attrValues outputs; };
+      examples = renderDir "examples" ./examples;
       doc = book;
     };
     defaultPackage = self.packages.${system}.doc;

doc/metaprogramming-arith.lean

@@ -8,7 +8,7 @@ declare_syntax_cat arith
 
 syntax num : arith  -- int for Arith.int
 syntax str : arith  -- strings for Arith.symbol
-syntax:60  arith:60 "+" arith:61 : arith  -- Arith.add
+syntax:60 arith:60 "+" arith:61 : arith  -- Arith.add
 syntax:70 arith:70 "*" arith:71 : arith  -- Arith.mul
 syntax "(" arith ")" : arith  -- parenthesized expressions
 

nix/bootstrap.nix

@@ -104,7 +104,7 @@ rec {
       Std  = attachSharedLib leanshared Std'  // { allExternalDeps = [ Init ]; };
       Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init Std ]; };
       stdlib = [ Init Std Lean ];
-      modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) stdlib; };
+      modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       extlib = stdlib;  # TODO: add Lake
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; };

src/Init/Classical.lean

@@ -9,7 +9,7 @@ import Init.NotationExtra
 
 universe u v
 
-/- Classical reasoning support -/
+/-! # Classical reasoning support -/
 
 namespace Classical
 
@@ -65,7 +65,7 @@ noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabi
 noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
   inhabited_of_nonempty (Exists.elim h (fun w _ => ⟨w⟩))
 
-/- all propositions are Decidable -/
+/-- All propositions are `Decidable`. -/
 noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decidable a :=
   choice <| match em a with
     | Or.inl h => ⟨isTrue h⟩

src/Init/Coe.lean

@@ -15,11 +15,11 @@ class Coe (α : Sort u) (β : Sort v) where
 class CoeTC (α : Sort u) (β : Sort v) where
   coe : α → β
 
-/- Expensive coercion that can only appear at the beginning of a sequence of coercions. -/
+/-- Expensive coercion that can only appear at the beginning of a sequence of coercions. -/
 class CoeHead (α : Sort u) (β : Sort v) where
   coe : α → β
 
-/- Expensive coercion that can only appear at the end of a sequence of coercions. -/
+/-- Expensive coercion that can only appear at the end of a sequence of coercions. -/
 class CoeTail (α : Sort u) (β : Sort v) where
   coe : α → β
 
@@ -30,7 +30,7 @@ class CoeHTCT (α : Sort u) (β : Sort v) where
 class CoeDep (α : Sort u) (_ : α) (β : Sort v) where
   coe : β
 
-/- Combines CoeHead, CoeTC, CoeTail, CoeDep -/
+/-- Combines CoeHead, CoeTC, CoeTail, CoeDep -/
 class CoeT (α : Sort u) (_ : α) (β : Sort v) where
   coe : β
 
@@ -81,7 +81,7 @@ instance coeId {α : Sort u} (a : α) : CoeT α a α where
 instance coeSortToCoeTail [inst : CoeSort α β] : CoeTail α β where
   coe := inst.coe
 
-/- Basic instances -/
+/-! # Basic instances -/
 
 @[inline] instance boolToProp : Coe Bool Prop where
   coe b := Eq b true
@@ -98,7 +98,7 @@ instance optionCoe {α : Type u} : CoeTail α (Option α) where
 instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead (Subtype p) α where
   coe v := v.val
 
-/- Coe bridge -/
+/-! # Coe bridge -/
 
 -- Helper definition used by the elaborator. It is not meant to be used directly by users
 @[inline] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do

src/Init/Control/Basic.lean

@@ -217,7 +217,7 @@ def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n]
     (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
   controlAt m f
 
-/-
+/--
   Typeclass for the polymorphic `forM` operation described in the "do unchained" paper.
   Remark:
   - `γ` is a "container" type of elements of type `α`.

src/Init/Control/ExceptCps.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Control.Lawful
 
-/-
+/-!
 The Exception monad transformer using CPS style.
 -/
 

src/Init/Control/Lawful.lean

@@ -90,7 +90,7 @@ theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *>
 theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
   rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]
 
-/- Id -/
+/-! # Id -/
 
 namespace Id
 
@@ -103,7 +103,7 @@ instance : LawfulMonad Id := by
 
 end Id
 
-/- ExceptT -/
+/-! # ExceptT -/
 
 namespace ExceptT
 
@@ -179,7 +179,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 end ExceptT
 
-/- ReaderT -/
+/-! # ReaderT -/
 
 namespace ReaderT
 
@@ -225,12 +225,12 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
 
 end ReaderT
 
-/- StateRefT -/
+/-! # StateRefT -/
 
 instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
   inferInstanceAs (LawfulMonad (ReaderT (ST.Ref ω σ) m))
 
-/- StateT -/
+/-! # StateT -/
 
 namespace StateT