Merge branch 'master' into wojciech/treemap_beq

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/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

src/Init/Prelude.lean

@@ -1837,6 +1837,8 @@ def Nat.ble : @& Nat → @& Nat → Bool
   | succ _, zero   => false
   | succ n, succ m => ble n m
 
+attribute [gen_constructor_elims] Bool
+
 /--
 Non-strict, or weak, inequality of natural numbers, usually accessed via the `≤` operator.
 -/
@@ -1860,9 +1862,14 @@ protected def Nat.lt (n m : Nat) : Prop :=
 instance instLTNat : LT Nat where
   lt := Nat.lt
 
-theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
-  | 0      => nofun
-  | succ _ => nofun
+theorem Nat.not_succ_le_zero (n : Nat) : LE.le (succ n) 0 → False :=
+  -- No injectivity tactic until `attribute [gen_constructor_elims] Nat`
+  have : ∀ m, Eq m 0 → LE.le (succ n) m → False := fun _ hm hle =>
+    Nat.le.casesOn (motive := fun m _ => Eq m 0 → False) hle
+      (fun h => Nat.noConfusion h)
+      (fun _ h => Nat.noConfusion h)
+      hm
+  this 0 rfl
 
 theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
   not_succ_le_zero n
@@ -1999,10 +2006,12 @@ protected theorem Nat.lt_of_not_le {a b : Nat} (h : Not (LE.le a b)) : LT.lt b a
 
 protected theorem Nat.add_pos_right :
     {b : Nat} → (a : Nat) → (hb : LT.lt 0 b) → LT.lt 0 (HAdd.hAdd a b)
+  | zero, _, h => (Nat.not_succ_le_zero _ h).elim
   | succ _, _, _ => Nat.zero_lt_succ _
 
 protected theorem Nat.mul_pos :
     {n m : Nat} → (hn : LT.lt 0 n) → (hm : LT.lt 0 m) → LT.lt 0 (HMul.hMul n m)
+  | _, zero, _, hb => (Nat.not_succ_le_zero _ hb).elim
   | _, succ _, ha, _ => Nat.add_pos_right _ ha
 
 protected theorem Nat.pow_pos {a : Nat} : {n : Nat} → (h : LT.lt 0 a) → LT.lt 0 (HPow.hPow a n)
@@ -2059,6 +2068,8 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
   | a, 0      => a
   | a, succ b => pred (Nat.sub a b)
 
+attribute [gen_constructor_elims] Nat
+
 instance instSubNat : Sub Nat where
   sub := Nat.sub
 
@@ -2216,9 +2227,6 @@ theorem Nat.mod_lt : (x : Nat) →  {y : Nat} → (hy : LT.lt 0 y) → LT.lt (HM
       | .isTrue _ => Nat.modCore_lt hm
       | .isFalse h => Nat.lt_of_not_le h
 
-attribute [gen_constructor_elims] Nat
-attribute [gen_constructor_elims] Bool
-
 /--
 Gets the word size of the current platform. The word size may be 64 or 32 bits.