Merge branch 'master' into wojciech/extdtreemap_diff2

Author: wkrozowski

CMakeLists.txt

@@ -44,7 +44,9 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     set(CADICAL_CXX c++)
     if (CADICAL_USE_CUSTOM_CXX)
       set(CADICAL_CXX ${CMAKE_CXX_COMPILER})
-      set(CADICAL_CXXFLAGS "${LEAN_EXTRA_CXX_FLAGS}")
+      # Use same platform flags as for Lean executables, in particular from `prepare-llvm-linux.sh`,
+      # but not Lean-specific `LEAN_EXTRA_CXX_FLAGS` such as fsanitize.
+      set(CADICAL_CXXFLAGS "${CMAKE_CXX_FLAGS}")
       set(CADICAL_LDFLAGS "-Wl,-rpath=\\$$ORIGIN/../lib")
     endif()
     find_program(CCACHE ccache)

src/CMakeLists.txt

@@ -448,8 +448,8 @@ if(LLVM AND ${STAGE} GREATER 0)
     # - In particular, `host/bin/llvm-config` produces flags like `-Lllvm-host/lib/libLLVM`, while
     #   we need the path to be `-Lllvm/lib/libLLVM`. Thus, we perform this replacement here.
     string(REPLACE "llvm-host" "llvm" LEANSHARED_LINKER_FLAGS ${LEANSHARED_LINKER_FLAGS})
-    string(REPLACE "llvm-host" "llvm" LEAN_EXTRA_CXX_FLAGS ${LEAN_EXTRA_CXX_FLAGS})
-    message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${LEAN_EXTR_CXX_FLAGS}'")
+    string(REPLACE "llvm-host" "llvm" CMAKE_CXX_FLAGS ${CMAKE_CXX_FLAGS})
+    message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${CMAKE_CXX_FLAGS}'")
 endif()
 
 # get rid of unused parts of C++ stdlib

src/Init/Data/Int/Basic.lean

@@ -278,7 +278,11 @@ set_option bootstrap.genMatcherCode false in
 def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
   match m with
   | ofNat m => isTrue <| NonNeg.mk m
-  | -[_ +1] => isFalse <| fun h => nomatch h
+  | -[i +1] => isFalse <| fun h =>
+    have : ∀ j, (j = -[i +1]) → NonNeg j → False := fun _ hj hnn =>
+      Int.NonNeg.casesOn (motive := fun j _ => j = -[i +1] → False) hnn
+        (fun _ h => Int.noConfusion h) hj
+    this -[i +1] rfl h
 
 /-- Decides whether `a ≤ b`.
 

src/Init/Data/List/Nat/Perm.lean

@@ -60,14 +60,14 @@ theorem set_set_perm {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j
 
 namespace Perm
 
-/-- Variant of `List.Perm.take` specifying the the permutation is constant after `i` elementwise. -/
+/-- Variant of `List.Perm.take` specifying that the permutation is constant after `i` elementwise. -/
 theorem take_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, i ≤ j → l₁[j]? = l₂[j]?) :
     l₁.take i ~ l₂.take i := by
   refine h.take (Perm.of_eq ?_)
   ext1 j
   simpa using w (i + j) (by omega)
 
-/-- Variant of `List.Perm.drop` specifying the the permutation is constant before `i` elementwise. -/
+/-- Variant of `List.Perm.drop` specifying that the permutation is constant before `i` elementwise. -/
 theorem drop_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, j < i → l₁[j]? = l₂[j]?) :
     l₁.drop i ~ l₂.drop i := by
   refine h.drop (Perm.of_eq ?_)

src/Init/Data/Slice/Notation.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Range.Polymorphic.PRange
 
 set_option doc.verso true
+set_option linter.missingDocs true
 
 public section
 
@@ -30,6 +31,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
 The type of the resulting slices is {lit}`γ`.
 -/
 class Rcc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` from {lean}`range.lower` to {lean}`range.upper`, both inclusive.
+  -/
   mkSlice (carrier : α) (range : Rcc β) : γ
 
 /--
@@ -39,6 +43,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
 The type of resulting the slices is {lit}`γ`.
 -/
 class Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` from {lean}`range.lower` (inclusive) to {lean}`range.upper` (exclusive).
+  -/
   mkSlice (carrier : α) (range : Rco β) : γ
 
 /--
@@ -48,6 +55,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
 The type of the resulting slices is {lit}`γ`.
 -/
 class Rci.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` from {lean}`range.lower` (inclusive).
+  -/
   mkSlice (carrier : α) (range : Rci β) : γ
 
 /--
@@ -57,6 +67,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
 The type of the resulting slices is {lit}`γ`.
 -/
 class Roc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` from {lean}`range.lower` (exclusive) to {lean}`range.upper` (inclusive).
+  -/
   mkSlice (carrier : α) (range : Roc β) : γ
 
 /--
@@ -66,6 +79,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
 The type of the resulting slices is {lit}`γ`.
 -/
 class Roo.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` from {lean}`range.lower` to {lean}`range.upper`, both exclusive.
+  -/
   mkSlice (carrier : α) (range : Roo β) : γ
 
 /--
@@ -75,6 +91,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
 The type of the resulting slices is {lit}`γ`.
 -/
 class Roi.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` from {lean}`range.lower` (exclusive).
+  -/
   mkSlice (carrier : α) (range : Roi β) : γ
 
 /--
@@ -84,6 +103,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
 The type of the resulting slices is {lit}`γ`.
 -/
 class Ric.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` up to {lean}`range.upper` (inclusive).
+  -/
   mkSlice (carrier : α) (range : Ric β) : γ
 
 /--
@@ -93,6 +115,9 @@ This typeclass indicates how to obtain slices of elements of {lit}`α` over rang
 The type of the resulting slices is {lit}`γ`.
 -/
 class Rio.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` up to {lean}`range.upper` (exclusive).
+  -/
   mkSlice (carrier : α) (range : Rio β) : γ
 
 /--
@@ -102,6 +127,9 @@ index type {lit}`β`.
 The type of the resulting slices is {lit}`γ`.
 -/
 class Rii.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where
+  /--
+  Slices {name}`carrier` with no bounds.
+  -/
   mkSlice (carrier : α) (range : Rii β) : γ
 
 macro_rules

src/Init/Data/String/Pattern/Pred.lean

@@ -79,9 +79,11 @@ instance : Std.Iterators.Finite (ForwardCharPredSearcher p s) Id :=
 instance : Std.Iterators.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
   .defaultImplementation
 
+@[default_instance]
 instance {p : Char → Bool} : ToForwardSearcher p (ForwardCharPredSearcher p) where
   toSearcher := iter p
 
+@[default_instance]
 instance {p : Char → Bool} : ForwardPattern p := .defaultImplementation
 
 instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ForwardCharPredSearcher p) where
@@ -153,9 +155,11 @@ instance : Std.Iterators.Finite (BackwardCharPredSearcher s) Id :=
 instance : Std.Iterators.IteratorLoop (BackwardCharPredSearcher s) Id Id :=
   .defaultImplementation
 
+@[default_instance]
 instance {p : Char → Bool} : ToBackwardSearcher p BackwardCharPredSearcher where
   toSearcher := iter p
 
+@[default_instance]
 instance {p : Char → Bool} : BackwardPattern p := ToBackwardSearcher.defaultImplementation
 
 instance {p : Char → Prop} [DecidablePred p] : ToBackwardSearcher p BackwardCharPredSearcher where

src/Init/Data/Sum/Basic.lean

@@ -13,7 +13,7 @@ public section
 /-!
 # Disjoint union of types
 
-This file defines basic operations on the the sum type `α ⊕ β`.
+This file defines basic operations on the sum type `α ⊕ β`.
 
 `α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
 

src/Init/GetElem.lean

@@ -240,6 +240,9 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
     {c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e :=
   getElem?_eq_some_iff.mp h
 
+theorem of_getElem_eq [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+    {c : cont} {i : idx} [Decidable (dom c i)] {h} (_ : c[i] = e) : dom c i := h
+
 @[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
     (some c[i] = c[i]?) ↔ True := by

src/Init/Grind/Config.lean

@@ -202,6 +202,15 @@ structure Config where
   ```
   -/
   funCC := true
+  /--
+  When `true`, use reducible transparency when trying to close goals.
+  In this setting, only declarations marked with `@[reducible]` are unfolded during
+  definitional equality tests.
+
+  This option does not affect the canonicalizer or how theorem patterns are internalized;
+  reducible declarations are always unfolded in those contexts.
+  -/
+  reducible := true
   deriving Inhabited, BEq
 
 /--

src/Init/Grind/Util.lean

@@ -122,4 +122,15 @@ See comment at `alreadyNorm`
 theorem em (p : Prop) : alreadyNorm p ∨ alreadyNorm (¬ p) :=
   Classical.em p
 
+/--
+Marker for grind-solved subproofs in `exact? +grind` suggestions.
+When `exact?` uses grind as a discharger, it wraps the proof in this marker
+so that the unexpander can replace it with `(by grind)` in the suggestion.
+-/
+@[inline] def Marker {α : Sort u} (a : α) : α := a
+
+@[app_unexpander Marker]
+meta def markerUnexpander : PrettyPrinter.Unexpander := fun _ => do
+  `(by grind)
+
 end Lean.Grind