Compare commits

..

2 Commits

Author SHA1 Message Date
Leonardo de Moura
1b50af3e95 feat: give preference to case-splits with fewer cases 2025-01-11 20:00:26 -08:00
Leonardo de Moura
2d04171174 chore: increase default max number of splits 2025-01-11 20:00:26 -08:00
101 changed files with 787 additions and 3885 deletions

View File

@@ -33,9 +33,6 @@ Format of the commit message
- chore (maintain, ex: travis-ci)
- perf (performance improvement, optimization, ...)
Every `feat` or `fix` commit must have a `changelog-*` label, and a commit message
beginning with "This PR " that will be included in the changelog.
``<subject>`` has the following constraints:
- use imperative, present tense: "change" not "changed" nor "changes"
@@ -47,7 +44,6 @@ beginning with "This PR " that will be included in the changelog.
- just as in ``<subject>``, use imperative, present tense
- includes motivation for the change and contrasts with previous
behavior
- If a `changelog-*` label is present, the body must begin with "This PR ".
``<footer>`` is optional and may contain two items:
@@ -64,21 +60,17 @@ Examples
fix: add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel
This PR adds declarations `operator<<` for raw printing.
The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.
We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include 'library/printer.h',
kernel. They are implemented in the file 'library/printer.cpp'. We
declare them in the kernel to prevent the following problem. Suppose
there is a file 'foo.cpp' that does not include 'library/printer.h',
but contains
```cpp
expr a;
...
std::cout << a << "\n";
...
```
expr a;
...
std::cout << a << "\n";
...
The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.

View File

@@ -80,10 +80,3 @@ Unlike most Lean projects, all submodules of the `Lean` module begin with the
`prelude` keyword. This disables the automated import of `Init`, meaning that
developers need to figure out their own subset of `Init` to import. This is done
such that changing files in `Init` doesn't force a full rebuild of `Lean`.
### Testing against Mathlib/Batteries
You can test a Lean PR against Mathlib and Batteries by rebasing your PR
on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.)
CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.

View File

@@ -244,7 +244,8 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
def range (n : Nat) : Array Nat :=
ofFn fun (i : Fin n) => i
@[inline] protected def singleton (v : α) : Array α := #[v]
def singleton (v : α) : Array α :=
mkArray 1 v
def back! [Inhabited α] (a : Array α) : α :=
a[a.size - 1]!

View File

@@ -1504,311 +1504,11 @@ theorem filterMap_eq_push_iff {f : α → Option β} {l : Array α} {l' : Array
· rintro l₁, a, l₂, h₁, h₂, h₃, h₄
refine l₂.reverse, a, l₁.reverse, by simp_all
/-! ### singleton -/
@[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl
/-! ### append -/
@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
simp only [size, toList_append, List.length_append]
@[simp] theorem append_push {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).push a := by
cases as
cases bs
simp
@[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
xs.toArray = as ++ bs xs = as.toList ++ bs.toList := by
cases as
cases bs
simp
@[simp] theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} :
as ++ bs = xs.toArray as.toList ++ bs.toList = xs := by
cases as
cases bs
simp
/-! Content below this point has not yet been aligned with `List`. -/
theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
@[simp] theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
funext l
simp
@[simp] theorem mem_append {a : α} {s t : Array α} : a s ++ t a s a t := by
simp only [mem_def, toList_append, List.mem_append]
theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a l₁) : a l₁ ++ l₂ :=
mem_append.2 (Or.inl h)
theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a l₂) : a l₁ ++ l₂ :=
mem_append.2 (Or.inr h)
theorem not_mem_append {a : α} {s t : Array α} (h₁ : a s) (h₂ : a t) : a s ++ t :=
mt mem_append.1 $ not_or.mpr h₁, h₂
/--
See also `eq_push_append_of_mem`, which proves a stronger version
in which the initial array must not contain the element.
-/
theorem append_of_mem {a : α} {l : Array α} (h : a l) : s t : Array α, l = s.push a ++ t := by
obtain s, t, w := List.append_of_mem (l := l.toList) (by simpa using h)
replace w := congrArg List.toArray w
refine s.toArray, t.toArray, by simp_all
theorem mem_iff_append {a : α} {l : Array α} : a l s t : Array α, l = s.push a ++ t :=
append_of_mem, fun s, t, e => e by simp
theorem forall_mem_append {p : α Prop} {l₁ l₂ : Array α} :
( (x) (_ : x l₁ ++ l₂), p x) ( (x) (_ : x l₁), p x) ( (x) (_ : x l₂), p x) := by
simp only [mem_append, or_imp, forall_and]
theorem empty_append (as : Array α) : #[] ++ as = as := by simp
theorem append_empty (as : Array α) : as ++ #[] = as := by simp
theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
(as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
cases as; cases bs
simp [List.getElem_append]
theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
(as ++ bs)[i] = as[i] := by
simp only [ getElem_toList]
have h' : i < (as.toList ++ bs.toList).length := by rwa [ length_toList, toList_append] at h
conv => rhs; rw [ List.getElem_append_left (bs := bs.toList) (h' := h')]
apply List.get_of_eq; rw [toList_append]
theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size i) :
(as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. h)) := by
simp only [ getElem_toList]
have h' : i < (as.toList ++ bs.toList).length := by rwa [ length_toList, toList_append] at h
conv => rhs; rw [ List.getElem_append_right (h₁ := hle) (h₂ := h')]
apply List.get_of_eq; rw [toList_append]
theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
(as ++ bs)[i]? = as[i]? := by
have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
size_append .. Nat.le_add_right ..
simp_all [getElem?_eq_getElem, getElem_append]
theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size i) :
(as ++ bs)[i]? = bs[i - as.size]? := by
cases as
cases bs
simp at h
simp [List.getElem?_append_right, h]
theorem getElem?_append {as bs : Array α} {i : Nat} :
(as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]? := by
split <;> rename_i h
· exact getElem?_append_left h
· exact getElem?_append_right (by simpa using h)
/-- Variant of `getElem_append_left` useful for rewriting from the small array to the big array. -/
theorem getElem_append_left' (l₂ : Array α) {l₁ : Array α} {i : Nat} (hi : i < l₁.size) :
l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.size hi) := by
rw [getElem_append_left] <;> simp
/-- Variant of `getElem_append_right` useful for rewriting from the small array to the big array. -/
theorem getElem_append_right' (l₁ : Array α) {l₂ : Array α} {i : Nat} (hi : i < l₂.size) :
l₂[i] = (l₁ ++ l₂)[i + l₁.size]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _) := by
rw [getElem_append_right] <;> simp [*, Nat.le_add_left]
theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂) (h : l₁.size = i) :
l[i]'(eq h by simp_arith) = a := Option.some.inj <| by
rw [ getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), h]
simp
@[simp 1100] theorem append_singleton {a : α} {as : Array α} : as ++ #[a] = as.push a := by
cases as
simp
theorem append_inj {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) :
s₁ = s₂ t₁ = t₂ := by
rcases s₁ with s₁
rcases s₂ with s₂
rcases t₁ with t₁
rcases t₂ with t₂
simpa using List.append_inj (by simpa using h) (by simpa using hl)
theorem append_inj_right {s₁ s₂ t₁ t₂ : Array α}
(h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) : t₁ = t₂ :=
(append_inj h hl).right
theorem append_inj_left {s₁ s₂ t₁ t₂ : Array α}
(h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) : s₁ = s₂ :=
(append_inj h hl).left
/-- Variant of `append_inj` instead requiring equality of the sizes of the second arrays. -/
theorem append_inj' {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) :
s₁ = s₂ t₁ = t₂ :=
append_inj h <| @Nat.add_right_cancel _ t₁.size _ <| by
let hap := congrArg size h; simp only [size_append, hl] at hap; exact hap
/-- Variant of `append_inj_right` instead requiring equality of the sizes of the second arrays. -/
theorem append_inj_right' {s₁ s₂ t₁ t₂ : Array α}
(h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) : t₁ = t₂ :=
(append_inj' h hl).right
/-- Variant of `append_inj_left` instead requiring equality of the sizes of the second arrays. -/
theorem append_inj_left' {s₁ s₂ t₁ t₂ : Array α}
(h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) : s₁ = s₂ :=
(append_inj' h hl).left
theorem append_right_inj {t₁ t₂ : Array α} (s) : s ++ t₁ = s ++ t₂ t₁ = t₂ :=
fun h => append_inj_right h rfl, congrArg _
theorem append_left_inj {s₁ s₂ : Array α} (t) : s₁ ++ t = s₂ ++ t s₁ = s₂ :=
fun h => append_inj_left' h rfl, congrArg (· ++ _)
@[simp] theorem append_left_eq_self {x y : Array α} : x ++ y = y x = #[] := by
rw [ append_left_inj (s₁ := x), nil_append]
@[simp] theorem self_eq_append_left {x y : Array α} : y = x ++ y x = #[] := by
rw [eq_comm, append_left_eq_self]
@[simp] theorem append_right_eq_self {x y : Array α} : x ++ y = x y = #[] := by
rw [ append_right_inj (t₁ := y), append_nil]
@[simp] theorem self_eq_append_right {x y : Array α} : x = x ++ y y = #[] := by
rw [eq_comm, append_right_eq_self]
@[simp] theorem append_eq_empty_iff : p ++ q = #[] p = #[] q = #[] := by
cases p <;> simp
@[simp] theorem empty_eq_append_iff : #[] = a ++ b a = #[] b = #[] := by
rw [eq_comm, append_eq_empty_iff]
theorem append_ne_empty_of_left_ne_empty {s : Array α} (h : s #[]) (t : Array α) :
s ++ t #[] := by
simp_all
theorem append_ne_empty_of_right_ne_empty (s : Array α) : t #[] s ++ t #[] := by
simp_all
theorem append_eq_push_iff {a b c : Array α} {x : α} :
a ++ b = c.push x (b = #[] a = c.push x) ( b', b = b'.push x c = a ++ b') := by
rcases a with a
rcases b with b
rcases c with c
simp only [List.append_toArray, List.push_toArray, mk.injEq, List.append_eq_append_iff,
toArray_eq_append_iff]
constructor
· rintro (a', rfl, rfl | b', rfl, h)
· right; exact a', by simp
· rw [List.singleton_eq_append_iff] at h
obtain (rfl, rfl | rfl, rfl) := h
· right; exact #[], by simp
· left; simp
· rintro (rfl, rfl | b', h, rfl)
· right; exact [x], by simp
· left; refine b'.toList, ?_
replace h := congrArg Array.toList h
simp_all
theorem push_eq_append_iff {a b c : Array α} {x : α} :
c.push x = a ++ b (b = #[] a = c.push x) ( b', b = b'.push x c = a ++ b') := by
rw [eq_comm, append_eq_push_iff]
theorem append_eq_singleton_iff {a b : Array α} {x : α} :
a ++ b = #[x] (a = #[] b = #[x]) (a = #[x] b = #[]) := by
rcases a with a
rcases b with b
simp only [List.append_toArray, mk.injEq, List.append_eq_singleton_iff, toArray_eq_append_iff]
theorem singleton_eq_append_iff {a b : Array α} {x : α} :
#[x] = a ++ b (a = #[] b = #[x]) (a = #[x] b = #[]) := by
rw [eq_comm, append_eq_singleton_iff]
theorem append_eq_append_iff {a b c d : Array α} :
a ++ b = c ++ d ( a', c = a ++ a' b = a' ++ d) c', a = c ++ c' d = c' ++ b := by
rcases a with a
rcases b with b
rcases c with c
rcases d with d
simp only [List.append_toArray, mk.injEq, List.append_eq_append_iff, toArray_eq_append_iff]
constructor
· rintro (a', rfl, rfl | c', rfl, rfl)
· left; exact a', by simp
· right; exact c', by simp
· rintro (a', rfl, rfl | c', rfl, rfl)
· left; exact a'.toList, by simp
· right; exact c'.toList, by simp
theorem set_append {s t : Array α} {i : Nat} {x : α} (h : i < (s ++ t).size) :
(s ++ t).set i x =
if h' : i < s.size then
s.set i x ++ t
else
s ++ t.set (i - s.size) x (by simp at h; omega) := by
rcases s with s
rcases t with t
simp only [List.append_toArray, List.set_toArray, List.set_append]
split <;> simp
@[simp] theorem set_append_left {s t : Array α} {i : Nat} {x : α} (h : i < s.size) :
(s ++ t).set i x (by simp; omega) = s.set i x ++ t := by
simp [set_append, h]
@[simp] theorem set_append_right {s t : Array α} {i : Nat} {x : α}
(h' : i < (s ++ t).size) (h : s.size i) :
(s ++ t).set i x = s ++ t.set (i - s.size) x (by simp at h'; omega) := by
rw [set_append, dif_neg (by omega)]
theorem setIfInBounds_append {s t : Array α} {i : Nat} {x : α} :
(s ++ t).setIfInBounds i x =
if i < s.size then
s.setIfInBounds i x ++ t
else
s ++ t.setIfInBounds (i - s.size) x := by
rcases s with s
rcases t with t
simp only [List.append_toArray, List.setIfInBounds_toArray, List.set_append]
split <;> simp
@[simp] theorem setIfInBounds_append_left {s t : Array α} {i : Nat} {x : α} (h : i < s.size) :
(s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t := by
simp [setIfInBounds_append, h]
@[simp] theorem setIfInBounds_append_right {s t : Array α} {i : Nat} {x : α} (h : s.size i) :
(s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - s.size) x := by
rw [setIfInBounds_append, if_neg (by omega)]
theorem filterMap_eq_append_iff {f : α Option β} :
filterMap f l = L₁ ++ L₂ l₁ l₂, l = l₁ ++ l₂ filterMap f l₁ = L₁ filterMap f l₂ = L₂ := by
rcases l with l
rcases L₁ with L₁
rcases L₂ with L₂
simp only [size_toArray, List.filterMap_toArray', List.append_toArray, mk.injEq,
List.filterMap_eq_append_iff, toArray_eq_append_iff]
constructor
· rintro l₁, l₂, rfl, rfl, rfl
exact l₁, l₂, by simp
· rintro l₁, l₂, rfl, h₁, h₂
exact l₁, l₂, by simp_all
theorem append_eq_filterMap_iff {f : α Option β} :
L₁ ++ L₂ = filterMap f l
l₁ l₂, l = l₁ ++ l₂ filterMap f l₁ = L₁ filterMap f l₂ = L₂ := by
rw [eq_comm, filterMap_eq_append_iff]
@[simp] theorem map_append (f : α β) (l₁ l₂ : Array α) :
map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
cases l₁
cases l₂
simp
theorem map_eq_append_iff {f : α β} :
map f l = L₁ ++ L₂ l₁ l₂, l = l₁ ++ l₂ map f l₁ = L₁ map f l₂ = L₂ := by
rw [ filterMap_eq_map, filterMap_eq_append_iff]
theorem append_eq_map_iff {f : α β} :
L₁ ++ L₂ = map f l l₁ l₂, l = l₁ ++ l₂ map f l₁ = L₁ map f l₂ = L₂ := by
rw [eq_comm, map_eq_append_iff]
/-! Content below this point has not yet been aligned with `List`. -/
@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
-- This is a duplicate of `List.toArray_toList`.
-- It's confusing to guess which namespace this theorem should live in,
@@ -2422,6 +2122,74 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : αα} {j : Nat} :
theorem size_empty : (#[] : Array α).size = 0 := rfl
/-! ### append -/
@[simp] theorem mem_append {a : α} {s t : Array α} : a s ++ t a s a t := by
simp only [mem_def, toList_append, List.mem_append]
theorem mem_append_left {a : α} {l₁ : Array α} (l₂ : Array α) (h : a l₁) : a l₁ ++ l₂ :=
mem_append.2 (Or.inl h)
theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a l₂) : a l₁ ++ l₂ :=
mem_append.2 (Or.inr h)
@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
simp only [size, toList_append, List.length_append]
theorem empty_append (as : Array α) : #[] ++ as = as := by simp
theorem append_empty (as : Array α) : as ++ #[] = as := by simp
theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
(as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
cases as; cases bs
simp [List.getElem_append]
theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) :
(as ++ bs)[i] = as[i] := by
simp only [ getElem_toList]
have h' : i < (as.toList ++ bs.toList).length := by rwa [ length_toList, toList_append] at h
conv => rhs; rw [ List.getElem_append_left (bs := bs.toList) (h' := h')]
apply List.get_of_eq; rw [toList_append]
theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size i) :
(as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. h)) := by
simp only [ getElem_toList]
have h' : i < (as.toList ++ bs.toList).length := by rwa [ length_toList, toList_append] at h
conv => rhs; rw [ List.getElem_append_right (h₁ := hle) (h₂ := h')]
apply List.get_of_eq; rw [toList_append]
theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
(as ++ bs)[i]? = as[i]? := by
have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
size_append .. Nat.le_add_right ..
simp_all [getElem?_eq_getElem, getElem_append]
theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size i) :
(as ++ bs)[i]? = bs[i - as.size]? := by
cases as
cases bs
simp at h
simp [List.getElem?_append_right, h]
theorem getElem?_append {as bs : Array α} {i : Nat} :
(as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]? := by
split <;> rename_i h
· exact getElem?_append_left h
· exact getElem?_append_right (by simpa using h)
@[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} :
xs.toArray = as ++ bs xs = as.toList ++ bs.toList := by
cases as
cases bs
simp
@[simp] theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} :
as ++ bs = xs.toArray as.toList ++ bs.toList = xs := by
cases as
cases bs
simp
/-! ### flatten -/
@[simp] theorem toList_flatten {l : Array (Array α)} :

View File

@@ -1494,34 +1494,6 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
@[simp] theorem cons_append_fun (a : α) (as : List α) :
(fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
@[simp] theorem mem_append {a : α} {s t : List α} : a s ++ t a s a t := by
induction s <;> simp_all [or_assoc]
theorem not_mem_append {a : α} {s t : List α} (h₁ : a s) (h₂ : a t) : a s ++ t :=
mt mem_append.1 $ not_or.mpr h₁, h₂
@[deprecated mem_append (since := "2025-01-13")]
theorem mem_append_eq (a : α) (s t : List α) : (a s ++ t) = (a s a t) :=
propext mem_append
@[deprecated mem_append_left (since := "2024-11-20")] abbrev mem_append_of_mem_left := @mem_append_left
@[deprecated mem_append_right (since := "2024-11-20")] abbrev mem_append_of_mem_right := @mem_append_right
/--
See also `eq_append_cons_of_mem`, which proves a stronger version
in which the initial list must not contain the element.
-/
theorem append_of_mem {a : α} {l : List α} : a l s t : List α, l = s ++ a :: t
| .head l => [], l, rfl
| .tail b h => let s, t, h' := append_of_mem h; b::s, t, by rw [h', cons_append]
theorem mem_iff_append {a : α} {l : List α} : a l s t : List α, l = s ++ a :: t :=
append_of_mem, fun s, t, e => e by simp
theorem forall_mem_append {p : α Prop} {l₁ l₂ : List α} :
( (x) (_ : x l₁ ++ l₂), p x) ( (x) (_ : x l₁), p x) ( (x) (_ : x l₂), p x) := by
simp only [mem_append, or_imp, forall_and]
theorem getElem_append {l₁ l₂ : List α} (i : Nat) (h : i < (l₁ ++ l₂).length) :
(l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
split <;> rename_i h'
@@ -1589,6 +1561,14 @@ theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.lengt
l.get i, get_of_append_proof eq h = a := Option.some.inj <| by
rw [ get?_eq_get, eq, get?_append_right (h Nat.le_refl _), h, Nat.sub_self]; rfl
/--
See also `eq_append_cons_of_mem`, which proves a stronger version
in which the initial list must not contain the element.
-/
theorem append_of_mem {a : α} {l : List α} : a l s t : List α, l = s ++ a :: t
| .head l => [], l, rfl
| .tail b h => let s, t, h' := append_of_mem h; b::s, t, by rw [h', cons_append]
@[simp 1100] theorem singleton_append : [x] ++ l = x :: l := rfl
theorem append_inj :
@@ -1605,8 +1585,8 @@ theorem append_inj_left (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length s₁ = le
/-- Variant of `append_inj` instead requiring equality of the lengths of the second lists. -/
theorem append_inj' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : s₁ = s₂ t₁ = t₂ :=
append_inj h <| @Nat.add_right_cancel _ t₁.length _ <| by
let hap := congrArg length h; simp only [length_append, hl] at hap; exact hap
append_inj h <| @Nat.add_right_cancel _ (length t₁) _ <| by
let hap := congrArg length h; simp only [length_append, hl] at hap; exact hap
/-- Variant of `append_inj_right` instead requiring equality of the lengths of the second lists. -/
theorem append_inj_right' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : t₁ = t₂ :=
@@ -1634,6 +1614,9 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s
@[simp] theorem self_eq_append_right {x y : List α} : x = x ++ y y = [] := by
rw [eq_comm, append_right_eq_self]
@[simp] theorem append_eq_nil : p ++ q = [] p = [] q = [] := by
cases p <;> simp
theorem getLast_concat {a : α} : (l : List α), getLast (l ++ [a]) (by simp) = a
| [] => rfl
| a::t => by
@@ -1659,54 +1642,6 @@ theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
(l₁ ++ l₂).get? n = l₁.get? n := by
simp [getElem?_append_left hn]
@[simp] theorem append_eq_nil_iff : p ++ q = [] p = [] q = [] := by
cases p <;> simp
@[deprecated append_eq_nil_iff (since := "2025-01-13")] abbrev append_eq_nil := @append_eq_nil_iff
@[simp] theorem nil_eq_append_iff : [] = a ++ b a = [] b = [] := by
rw [eq_comm, append_eq_nil_iff]
@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff
theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s []) (t : List α) : s ++ t [] := by simp_all
theorem append_ne_nil_of_right_ne_nil (s : List α) : t [] s ++ t [] := by simp_all
@[deprecated append_ne_nil_of_left_ne_nil (since := "2024-07-24")]
theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s []) (t : List α) : s ++ t [] := by simp_all
@[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")]
theorem append_ne_nil_of_ne_nil_right (s : List α) : t [] s ++ t [] := by simp_all
theorem append_eq_cons_iff :
a ++ b = x :: c (a = [] b = x :: c) ( a', a = x :: a' c = a' ++ b) := by
cases a with simp | cons a as => ?_
exact fun h => as, by simp [h], fun a', aeq, aseq, h => aeq, by rw [aseq, h]
@[deprecated append_eq_cons_iff (since := "2024-07-24")] abbrev append_eq_cons := @append_eq_cons_iff
theorem cons_eq_append_iff :
x :: c = a ++ b (a = [] b = x :: c) ( a', a = x :: a' c = a' ++ b) := by
rw [eq_comm, append_eq_cons_iff]
@[deprecated cons_eq_append_iff (since := "2024-07-24")] abbrev cons_eq_append := @cons_eq_append_iff
theorem append_eq_singleton_iff :
a ++ b = [x] (a = [] b = [x]) (a = [x] b = []) := by
cases a <;> cases b <;> simp
theorem singleton_eq_append_iff :
[x] = a ++ b (a = [] b = [x]) (a = [x] b = []) := by
cases a <;> cases b <;> simp [eq_comm]
theorem append_eq_append_iff {a b c d : List α} :
a ++ b = c ++ d ( a', c = a ++ a' b = a' ++ d) c', a = c ++ c' d = c' ++ b := by
induction a generalizing c with
| nil => simp_all
| cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]
@[deprecated append_inj (since := "2024-07-24")] abbrev append_inj_of_length_left := @append_inj
@[deprecated append_inj' (since := "2024-07-24")] abbrev append_inj_of_length_right := @append_inj'
@[simp] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) :
head (l ++ l') w₁ = head l w₂ := by
match l, w₂ with
@@ -1756,6 +1691,60 @@ theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tai
@[deprecated tail_append_of_ne_nil (since := "2024-07-24")] abbrev tail_append_left := @tail_append_of_ne_nil
theorem nil_eq_append_iff : [] = a ++ b a = [] b = [] := by
rw [eq_comm, append_eq_nil]
@[deprecated nil_eq_append_iff (since := "2024-07-24")] abbrev nil_eq_append := @nil_eq_append_iff
theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s []) (t : List α) : s ++ t [] := by simp_all
theorem append_ne_nil_of_right_ne_nil (s : List α) : t [] s ++ t [] := by simp_all
@[deprecated append_ne_nil_of_left_ne_nil (since := "2024-07-24")]
theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s []) (t : List α) : s ++ t [] := by simp_all
@[deprecated append_ne_nil_of_right_ne_nil (since := "2024-07-24")]
theorem append_ne_nil_of_ne_nil_right (s : List α) : t [] s ++ t [] := by simp_all
theorem append_eq_cons_iff :
a ++ b = x :: c (a = [] b = x :: c) ( a', a = x :: a' c = a' ++ b) := by
cases a with simp | cons a as => ?_
exact fun h => as, by simp [h], fun a', aeq, aseq, h => aeq, by rw [aseq, h]
@[deprecated append_eq_cons_iff (since := "2024-07-24")] abbrev append_eq_cons := @append_eq_cons_iff
theorem cons_eq_append_iff :
x :: c = a ++ b (a = [] b = x :: c) ( a', a = x :: a' c = a' ++ b) := by
rw [eq_comm, append_eq_cons_iff]
@[deprecated cons_eq_append_iff (since := "2024-07-24")] abbrev cons_eq_append := @cons_eq_append_iff
theorem append_eq_append_iff {a b c d : List α} :
a ++ b = c ++ d ( a', c = a ++ a' b = a' ++ d) c', a = c ++ c' d = c' ++ b := by
induction a generalizing c with
| nil => simp_all
| cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]
@[deprecated append_inj (since := "2024-07-24")] abbrev append_inj_of_length_left := @append_inj
@[deprecated append_inj' (since := "2024-07-24")] abbrev append_inj_of_length_right := @append_inj'
@[simp] theorem mem_append {a : α} {s t : List α} : a s ++ t a s a t := by
induction s <;> simp_all [or_assoc]
theorem not_mem_append {a : α} {s t : List α} (h₁ : a s) (h₂ : a t) : a s ++ t :=
mt mem_append.1 $ not_or.mpr h₁, h₂
theorem mem_append_eq (a : α) (s t : List α) : (a s ++ t) = (a s a t) :=
propext mem_append
@[deprecated mem_append_left (since := "2024-11-20")] abbrev mem_append_of_mem_left := @mem_append_left
@[deprecated mem_append_right (since := "2024-11-20")] abbrev mem_append_of_mem_right := @mem_append_right
theorem mem_iff_append {a : α} {l : List α} : a l s t : List α, l = s ++ a :: t :=
append_of_mem, fun s, t, e => e by simp
theorem forall_mem_append {p : α Prop} {l₁ l₂ : List α} :
( (x) (_ : x l₁ ++ l₂), p x) ( (x) (_ : x l₁), p x) ( (x) (_ : x l₂), p x) := by
simp only [mem_append, or_imp, forall_and]
theorem set_append {s t : List α} :
(s ++ t).set i x = if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x := by
induction s generalizing i with
@@ -1985,8 +1974,8 @@ theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
constructor
· induction xs generalizing ys with
| nil =>
simp only [flatten_nil, nil_eq, append_eq_nil_iff, and_false, cons_append, false_and,
exists_const, exists_false, or_false, and_imp, List.cons_ne_nil]
simp only [flatten_nil, nil_eq, append_eq_nil, and_false, cons_append, false_and, exists_const,
exists_false, or_false, and_imp, List.cons_ne_nil]
rintro rfl rfl
exact [], [], by simp
| cons x xs ih =>

View File

@@ -46,7 +46,7 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
cases l <;> simp [Array.isEmpty]
@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.singleton a := rfl
@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]

View File

@@ -203,11 +203,11 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : Li
cases l₂ with
| nil =>
constructor
· simp only [zipWith_nil_right, nil_eq, append_eq_nil_iff, exists_and_left, and_imp]
· simp only [zipWith_nil_right, nil_eq, append_eq_nil, exists_and_left, and_imp]
rintro rfl rfl
exact [], x₁ :: l₁, [], by simp
· rintro w, x, y, z, h₁, _, h₃, rfl, rfl
simp only [nil_eq, append_eq_nil_iff] at h₃
simp only [nil_eq, append_eq_nil] at h₃
obtain rfl, rfl := h₃
simp
| cons x₂ l₂ =>

View File

@@ -13,12 +13,6 @@ macro "declare_bitwise_uint_theorems" typeName:ident bits:term:arg : command =>
`(
namespace $typeName
@[simp] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := rfl
@[simp] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := rfl
@[simp] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := rfl
@[simp] protected theorem toBitVec_div {a b : $typeName} : (a / b).toBitVec = a.toBitVec / b.toBitVec := rfl
@[simp] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec % b.toBitVec := rfl
@[simp] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl
@[simp] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
@[simp] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
@[simp] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
@@ -43,31 +37,3 @@ declare_bitwise_uint_theorems UInt16 16
declare_bitwise_uint_theorems UInt32 32
declare_bitwise_uint_theorems UInt64 64
declare_bitwise_uint_theorems USize System.Platform.numBits
@[simp]
theorem Bool.toBitVec_toUInt8 {b : Bool} :
b.toUInt8.toBitVec = (BitVec.ofBool b).setWidth 8 := by
cases b <;> simp [toUInt8]
@[simp]
theorem Bool.toBitVec_toUInt16 {b : Bool} :
b.toUInt16.toBitVec = (BitVec.ofBool b).setWidth 16 := by
cases b <;> simp [toUInt16]
@[simp]
theorem Bool.toBitVec_toUInt32 {b : Bool} :
b.toUInt32.toBitVec = (BitVec.ofBool b).setWidth 32 := by
cases b <;> simp [toUInt32]
@[simp]
theorem Bool.toBitVec_toUInt64 {b : Bool} :
b.toUInt64.toBitVec = (BitVec.ofBool b).setWidth 64 := by
cases b <;> simp [toUInt64]
@[simp]
theorem Bool.toBitVec_toUSize {b : Bool} :
b.toUSize.toBitVec = (BitVec.ofBool b).setWidth System.Platform.numBits := by
cases b
· simp [toUSize]
· apply BitVec.eq_of_toNat_eq
simp [toUSize]

View File

@@ -693,24 +693,6 @@ theorem forall_getElem {l : Vector α n} {p : α → Prop} :
rcases l with l, rfl
simp [Array.forall_getElem]
/-! ### cast -/
@[simp] theorem getElem_cast (a : Vector α n) (h : n = m) (i : Nat) (hi : i < m) :
(a.cast h)[i] = a[i] := by
cases a
simp
@[simp] theorem getElem?_cast {l : Vector α n} {m : Nat} {w : n = m} {i : Nat} :
(l.cast w)[i]? = l[i]? := by
rcases l with l, rfl
simp
@[simp] theorem mem_cast {a : α} {l : Vector α n} {m : Nat} {w : n = m} :
a l.cast w a l := by
rcases l with l, rfl
simp
/-! ### Decidability of bounded quantifiers -/
instance {xs : Vector α n} {p : α Prop} [DecidablePred p] :
@@ -1185,227 +1167,6 @@ theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} :
cases as
simp
/-! ### singleton -/
@[simp] theorem singleton_def (v : α) : Vector.singleton v = #v[v] := rfl
/-! ### append -/
@[simp] theorem append_push {as : Vector α n} {bs : Vector α m} {a : α} :
as ++ bs.push a = (as ++ bs).push a := by
cases as
cases bs
simp
theorem singleton_eq_toVector_singleton (a : α) : #v[a] = #[a].toVector := rfl
@[simp] theorem mem_append {a : α} {s : Vector α n} {t : Vector α m} :
a s ++ t a s a t := by
cases s
cases t
simp
theorem mem_append_left {a : α} {s : Vector α n} {t : Vector α m} (h : a s) : a s ++ t :=
mem_append.2 (Or.inl h)
theorem mem_append_right {a : α} {s : Vector α n} {t : Vector α m} (h : a t) : a s ++ t :=
mem_append.2 (Or.inr h)
theorem not_mem_append {a : α} {s : Vector α n} {t : Vector α m} (h₁ : a s) (h₂ : a t) :
a s ++ t :=
mt mem_append.1 $ not_or.mpr h₁, h₂
/--
See also `eq_push_append_of_mem`, which proves a stronger version
in which the initial array must not contain the element.
-/
theorem append_of_mem {a : α} {l : Vector α n} (h : a l) :
(m k : Nat) (w : m + 1 + k = n) (s : Vector α m) (t : Vector α k),
l = (s.push a ++ t).cast w := by
rcases l with l, rfl
obtain s, t, rfl := Array.append_of_mem (by simpa using h)
refine _, _, by simp, s.toVector, t.toVector, by simp_all
theorem mem_iff_append {a : α} {l : Vector α n} :
a l (m k : Nat) (w : m + 1 + k = n) (s : Vector α m) (t : Vector α k),
l = (s.push a ++ t).cast w :=
append_of_mem, by rintro m, k, rfl, s, t, rfl; simp
theorem forall_mem_append {p : α Prop} {l₁ : Vector α n} {l₂ : Vector α m} :
( (x) (_ : x l₁ ++ l₂), p x) ( (x) (_ : x l₁), p x) ( (x) (_ : x l₂), p x) := by
simp only [mem_append, or_imp, forall_and]
theorem empty_append (as : Vector α n) : (#v[] : Vector α 0) ++ as = as.cast (by omega) := by
rcases as with as, rfl
simp
theorem append_empty (as : Vector α n) : as ++ (#v[] : Vector α 0) = as := by
rw [ toArray_inj, toArray_append, Array.append_nil]
theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) :
(a ++ b)[i] = if h : i < n then a[i] else b[i - n] := by
rcases a with a, rfl
rcases b with b, rfl
simp [Array.getElem_append, hi]
theorem getElem_append_left {a : Vector α n} {b : Vector α m} {i : Nat} (hi : i < n) :
(a ++ b)[i] = a[i] := by simp [getElem_append, hi]
theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : i < n + m) (hi : n i) :
(a ++ b)[i] = b[i - n] := by
rw [getElem_append, dif_neg (by omega)]
theorem getElem?_append_left {as : Vector α n} {bs : Vector α m} {i : Nat} (hn : i < n) :
(as ++ bs)[i]? = as[i]? := by
have hn' : i < n + m := by omega
simp_all [getElem?_eq_getElem, getElem_append]
theorem getElem?_append_right {as : Vector α n} {bs : Vector α m} {i : Nat} (h : n i) :
(as ++ bs)[i]? = bs[i - n]? := by
rcases as with as, rfl
rcases bs with bs, rfl
simp [Array.getElem?_append_right, h]
theorem getElem?_append {as : Vector α n} {bs : Vector α m} {i : Nat} :
(as ++ bs)[i]? = if i < n then as[i]? else bs[i - n]? := by
split <;> rename_i h
· exact getElem?_append_left h
· exact getElem?_append_right (by simpa using h)
/-- Variant of `getElem_append_left` useful for rewriting from the small array to the big array. -/
theorem getElem_append_left' (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < m) :
l₁[i] = (l₁ ++ l₂)[i] := by
rw [getElem_append_left] <;> simp
/-- Variant of `getElem_append_right` useful for rewriting from the small array to the big array. -/
theorem getElem_append_right' (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < n) :
l₂[i] = (l₁ ++ l₂)[i + m] := by
rw [getElem_append_right] <;> simp [*, Nat.le_add_left]
theorem getElem_of_append {l : Vector α n} {l₁ : Vector α m} {l₂ : Vector α k}
(w : m + 1 + k = n) (eq : l = (l₁.push a ++ l₂).cast w) :
l[m] = a := Option.some.inj <| by
rw [ getElem?_eq_getElem, eq, getElem?_cast, getElem?_append_left (by simp)]
simp
@[simp 1100] theorem append_singleton {a : α} {as : Vector α n} : as ++ #v[a] = as.push a := by
cases as
simp
theorem append_inj {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m} (h : s₁ ++ t₁ = s₂ ++ t₂) :
s₁ = s₂ t₁ = t₂ := by
rcases s₁ with s₁, rfl
rcases s₂ with s₂, hs
rcases t₁ with t₁, rfl
rcases t₂ with t₂, ht
simpa using Array.append_inj (by simpa using h) (by omega)
theorem append_inj_right {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m}
(h : s₁ ++ t₁ = s₂ ++ t₂) : t₁ = t₂ :=
(append_inj h).right
theorem append_inj_left {s₁ s₂ : Vector α n} {t₁ t₂ : Vector α m}
(h : s₁ ++ t₁ = s₂ ++ t₂) : s₁ = s₂ :=
(append_inj h).left
theorem append_right_inj {t₁ t₂ : Vector α m} (s : Vector α n) : s ++ t₁ = s ++ t₂ t₁ = t₂ :=
fun h => append_inj_right h, congrArg _
theorem append_left_inj {s₁ s₂ : Vector α n} (t : Vector α m) : s₁ ++ t = s₂ ++ t s₁ = s₂ :=
fun h => append_inj_left h, congrArg (· ++ _)
theorem append_eq_append_iff {a : Vector α n} {b : Vector α m} {c : Vector α k} {d : Vector α l}
(w : k + l = n + m) :
a ++ b = (c ++ d).cast w
if h : n k then
a' : Vector α (k - n), c = (a ++ a').cast (by omega) b = (a' ++ d).cast (by omega)
else
c' : Vector α (n - k), a = (c ++ c').cast (by omega) d = (c' ++ b).cast (by omega) := by
rcases a with a, rfl
rcases b with b, rfl
rcases c with c, rfl
rcases d with d, rfl
simp only [mk_append_mk, Array.append_eq_append_iff, mk_eq, toArray_cast]
constructor
· rintro (a', rfl, rfl | c', rfl, rfl)
· rw [dif_pos (by simp)]
exact a'.toVector.cast (by simp; omega), by simp
· split <;> rename_i h
· have hc : c'.size = 0 := by simp at h; omega
simp at hc
exact #v[].cast (by simp; omega), by simp_all
· exact c'.toVector.cast (by simp; omega), by simp
· split <;> rename_i h
· rintro a', hc, rfl
left
refine a'.toArray, hc, rfl
· rintro c', ha, rfl
right
refine c'.toArray, ha, rfl
theorem set_append {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n + m) :
(s ++ t).set i x =
if h' : i < n then
s.set i x ++ t
else
s ++ t.set (i - n) x := by
rcases s with s, rfl
rcases t with t, rfl
simp only [mk_append_mk, set_mk, Array.set_append]
split <;> simp
@[simp] theorem set_append_left {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n) :
(s ++ t).set i x = s.set i x ++ t := by
simp [set_append, h]
@[simp] theorem set_append_right {s : Vector α n} {t : Vector α m} {i : Nat} {x : α}
(h' : i < n + m) (h : n i) :
(s ++ t).set i x = s ++ t.set (i - n) x := by
rw [set_append, dif_neg (by omega)]
theorem setIfInBounds_append {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} :
(s ++ t).setIfInBounds i x =
if i < n then
s.setIfInBounds i x ++ t
else
s ++ t.setIfInBounds (i - n) x := by
rcases s with s, rfl
rcases t with t, rfl
simp only [mk_append_mk, setIfInBounds_mk, Array.setIfInBounds_append]
split <;> simp
@[simp] theorem setIfInBounds_append_left {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n) :
(s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t := by
simp [setIfInBounds_append, h]
@[simp] theorem setIfInBounds_append_right {s : Vector α n} {t : Vector α m} {i : Nat} {x : α}
(h : n i) :
(s ++ t).setIfInBounds i x = s ++ t.setIfInBounds (i - n) x := by
rw [setIfInBounds_append, if_neg (by omega)]
@[simp] theorem map_append (f : α β) (l₁ : Vector α n) (l₂ : Vector α m) :
map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
rcases l₁ with l₁, rfl
rcases l₂ with l₂, rfl
simp
theorem map_eq_append_iff {f : α β} :
map f l = L₁ ++ L₂ l₁ l₂, l = l₁ ++ l₂ map f l₁ = L₁ map f l₂ = L₂ := by
rcases l with l, h
rcases L₁ with L₁, rfl
rcases L₂ with L₂, rfl
simp only [map_mk, mk_append_mk, eq_mk, Array.map_eq_append_iff, mk_eq, toArray_append,
toArray_map]
constructor
· rintro l₁, l₂, rfl, rfl, rfl
exact l₁.toVector.cast (by simp), l₂.toVector.cast (by simp), by simp
· rintro l₁, l₂, rfl, h₁, h₂
exact l₁, l₂, by simp_all
theorem append_eq_map_iff {f : α β} :
L₁ ++ L₂ = map f l l₁ l₂, l = l₁ ++ l₂ map f l₁ = L₁ map f l₂ = L₂ := by
rw [eq_comm, map_eq_append_iff]
/-! Content below this point has not yet been aligned with `List` and `Array`. -/
@[simp] theorem getElem_ofFn {α n} (f : Fin n α) (i : Nat) (h : i < n) :
@@ -1436,6 +1197,28 @@ defeq issues in the implicit size argument.
subst h
simp [pop, back, back!, Array.eq_push_pop_back!_of_size_ne_zero]
/-! ### append -/
theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) :
(a ++ b)[i] = if h : i < n then a[i] else b[i - n] := by
rcases a with a, rfl
rcases b with b, rfl
simp [Array.getElem_append, hi]
theorem getElem_append_left {a : Vector α n} {b : Vector α m} {i : Nat} (hi : i < n) :
(a ++ b)[i] = a[i] := by simp [getElem_append, hi]
theorem getElem_append_right {a : Vector α n} {b : Vector α m} {i : Nat} (h : i < n + m) (hi : n i) :
(a ++ b)[i] = b[i - n] := by
rw [getElem_append, dif_neg (by omega)]
/-! ### cast -/
@[simp] theorem getElem_cast (a : Vector α n) (h : n = m) (i : Nat) (hi : i < m) :
(a.cast h)[i] = a[i] := by
cases a
simp
/-! ### extract -/
@[simp] theorem getElem_extract (a : Vector α n) (start stop) (i : Nat) (hi : i < min stop n - start) :

View File

@@ -11,4 +11,3 @@ import Init.Grind.Cases
import Init.Grind.Propagator
import Init.Grind.Util
import Init.Grind.Offset
import Init.Grind.PP

View File

@@ -12,9 +12,6 @@ import Init.Grind.Util
namespace Lean.Grind
theorem rfl_true : true = true :=
rfl
theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' q) : p q :=
fun hp => h (he.mp hp)

View File

@@ -46,12 +46,6 @@ attribute [grind_norm] not_false_eq_true
theorem imp_eq (p q : Prop) : (p q) = (¬ p q) := by
by_cases p <;> by_cases q <;> simp [*]
@[grind_norm] theorem true_imp_eq (p : Prop) : (True p) = p := by simp
@[grind_norm] theorem false_imp_eq (p : Prop) : (False p) = True := by simp
@[grind_norm] theorem imp_true_eq (p : Prop) : (p True) = True := by simp
@[grind_norm] theorem imp_false_eq (p : Prop) : (p False) = ¬p := by simp
@[grind_norm] theorem imp_self_eq (p : Prop) : (p p) = True := by simp
-- And
@[grind_norm] theorem not_and (p q : Prop) : (¬(p q)) = (¬p ¬q) := by
by_cases p <;> by_cases q <;> simp [*]

View File

@@ -7,77 +7,159 @@ prelude
import Init.Core
import Init.Omega
namespace Lean.Grind
abbrev isLt (x y : Nat) : Bool := x < y
abbrev isLE (x y : Nat) : Bool := x y
namespace Lean.Grind.Offset
/-! Theorems for transitivity. -/
theorem Nat.le_ro (u w v k : Nat) : u w w v + k u v + k := by
omega
theorem Nat.le_lo (u w v k : Nat) : u w w + k v u + k v := by
omega
theorem Nat.lo_le (u w v k : Nat) : u + k w w v u + k v := by
omega
theorem Nat.lo_lo (u w v k₁ k₂ : Nat) : u + k₁ w w + k₂ v u + (k₁ + k₂) v := by
omega
theorem Nat.lo_ro_1 (u w v k₁ k₂ : Nat) : isLt k₂ k₁ = true u + k₁ w w v + k₂ u + (k₁ - k₂) v := by
simp [isLt]; omega
theorem Nat.lo_ro_2 (u w v k₁ k₂ : Nat) : u + k₁ w w v + k₂ u v + (k₂ - k₁) := by
omega
theorem Nat.ro_le (u w v k : Nat) : u w + k w v u v + k := by
omega
theorem Nat.ro_lo_1 (u w v k₁ k₂ : Nat) : u w + k₁ w + k₂ v u v + (k₁ - k₂) := by
omega
theorem Nat.ro_lo_2 (u w v k₁ k₂ : Nat) : isLt k₁ k₂ = true u w + k₁ w + k₂ v u + (k₂ - k₁) v := by
simp [isLt]; omega
theorem Nat.ro_ro (u w v k₁ k₂ : Nat) : u w + k₁ w v + k₂ u v + (k₁ + k₂) := by
omega
abbrev Var := Nat
abbrev Context := Lean.RArray Nat
/-! Theorems for negating constraints. -/
theorem Nat.of_le_eq_false (u v : Nat) : ((u v) = False) v + 1 u := by
simp; omega
theorem Nat.of_lo_eq_false_1 (u v : Nat) : ((u + 1 v) = False) v u := by
simp; omega
theorem Nat.of_lo_eq_false (u v k : Nat) : ((u + k v) = False) v u + (k-1) := by
simp; omega
theorem Nat.of_ro_eq_false (u v k : Nat) : ((u v + k) = False) v + (k+1) u := by
simp; omega
def fixedVar := 100000000 -- Any big number should work here
/-! Theorems for closing a goal. -/
theorem Nat.unsat_le_lo (u v k : Nat) : isLt 0 k = true u v v + k u False := by
simp [isLt]; omega
theorem Nat.unsat_lo_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁+k₂) = true u + k₁ v v + k₂ u False := by
simp [isLt]; omega
theorem Nat.unsat_lo_ro (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true u + k₁ v v u + k₂ False := by
simp [isLt]; omega
def Var.denote (ctx : Context) (v : Var) : Nat :=
bif v == fixedVar then 1 else ctx.get v
/-! Theorems for propagating constraints to `True` -/
theorem Nat.lo_eq_true_of_lo (u v k₁ k₂ : Nat) : isLE k₂ k₁ = true u + k₁ v (u + k₂ v) = True :=
by simp [isLt]; omega
theorem Nat.le_eq_true_of_lo (u v k : Nat) : u + k v (u v) = True :=
by simp; omega
theorem Nat.le_eq_true_of_le (u v : Nat) : u v (u v) = True :=
by simp
theorem Nat.ro_eq_true_of_lo (u v k₁ k₂ : Nat) : u + k₁ v (u v + k₂) = True :=
by simp; omega
theorem Nat.ro_eq_true_of_le (u v k : Nat) : u v (u v + k) = True :=
by simp; omega
theorem Nat.ro_eq_true_of_ro (u v k₁ k₂ : Nat) : isLE k₁ k₂ = true u v + k₁ (u v + k₂) = True :=
by simp [isLE]; omega
structure Cnstr where
x : Var
y : Var
k : Nat := 0
l : Bool := true
deriving Repr, DecidableEq, Inhabited
/-!
Theorems for propagating constraints to `False`.
They are variants of the theorems for closing a goal.
-/
theorem Nat.lo_eq_false_of_le (u v k : Nat) : isLt 0 k = true u v (v + k u) = False := by
simp [isLt]; omega
theorem Nat.le_eq_false_of_lo (u v k : Nat) : isLt 0 k = true u + k v (v u) = False := by
simp [isLt]; omega
theorem Nat.lo_eq_false_of_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁+k₂) = true u + k₁ v (v + k₂ u) = False := by
simp [isLt]; omega
theorem Nat.ro_eq_false_of_lo (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true u + k₁ v (v u + k₂) = False := by
simp [isLt]; omega
theorem Nat.lo_eq_false_of_ro (u v k₁ k₂ : Nat) : isLt k₁ k₂ = true u v + k₁ (v + k₂ u) = False := by
simp [isLt]; omega
def Cnstr.denote (c : Cnstr) (ctx : Context) : Prop :=
if c.l then
c.x.denote ctx + c.k c.y.denote ctx
else
c.x.denote ctx c.y.denote ctx + c.k
end Lean.Grind
def trivialCnstr : Cnstr := { x := 0, y := 0, k := 0, l := true }
@[simp] theorem denote_trivial (ctx : Context) : trivialCnstr.denote ctx := by
simp [Cnstr.denote, trivialCnstr]
def Cnstr.trans (c₁ c₂ : Cnstr) : Cnstr :=
if c₁.y = c₂.x then
let { x, k := k₁, l := l₁, .. } := c₁
let { y, k := k₂, l := l₂, .. } := c₂
match l₁, l₂ with
| false, false =>
{ x, y, k := k₁ + k₂, l := false }
| false, true =>
if k₁ < k₂ then
{ x, y, k := k₂ - k₁, l := true }
else
{ x, y, k := k₁ - k₂, l := false }
| true, false =>
if k₁ < k₂ then
{ x, y, k := k₂ - k₁, l := false }
else
{ x, y, k := k₁ - k₂, l := true }
| true, true =>
{ x, y, k := k₁ + k₂, l := true }
else
trivialCnstr
@[simp] theorem Cnstr.denote_trans_easy (ctx : Context) (c₁ c₂ : Cnstr) (h : c₁.y c₂.x) : (c₁.trans c₂).denote ctx := by
simp [*, Cnstr.trans]
@[simp] theorem Cnstr.denote_trans (ctx : Context) (c₁ c₂ : Cnstr) : c₁.denote ctx c₂.denote ctx (c₁.trans c₂).denote ctx := by
by_cases c₁.y = c₂.x
case neg => simp [*]
simp [trans, *]
let { x, k := k₁, l := l₁, .. } := c₁
let { y, k := k₂, l := l₂, .. } := c₂
simp_all; split
· simp [denote]; omega
· split <;> simp [denote] <;> omega
· split <;> simp [denote] <;> omega
· simp [denote]; omega
def Cnstr.isTrivial (c : Cnstr) : Bool := c.x == c.y && c.k == 0
theorem Cnstr.of_isTrivial (ctx : Context) (c : Cnstr) : c.isTrivial = true c.denote ctx := by
cases c; simp [isTrivial]; intros; simp [*, denote]
def Cnstr.isFalse (c : Cnstr) : Bool := c.x == c.y && c.k != 0 && c.l == true
theorem Cnstr.of_isFalse (ctx : Context) {c : Cnstr} : c.isFalse = true ¬c.denote ctx := by
cases c; simp [isFalse]; intros; simp [*, denote]; omega
def Cnstrs := List Cnstr
def Cnstrs.denoteAnd' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : Prop :=
match c₂ with
| [] => c₁.denote ctx
| c::cs => c₁.denote ctx Cnstrs.denoteAnd' ctx c cs
theorem Cnstrs.denote'_trans (ctx : Context) (c₁ c : Cnstr) (cs : Cnstrs) : c₁.denote ctx denoteAnd' ctx c cs denoteAnd' ctx (c₁.trans c) cs := by
induction cs
next => simp [denoteAnd', *]; apply Cnstr.denote_trans
next c cs ih => simp [denoteAnd']; intros; simp [*]
def Cnstrs.trans' (c₁ : Cnstr) (c₂ : Cnstrs) : Cnstr :=
match c₂ with
| [] => c₁
| c::c₂ => trans' (c₁.trans c) c₂
@[simp] theorem Cnstrs.denote'_trans' (ctx : Context) (c₁ : Cnstr) (c₂ : Cnstrs) : denoteAnd' ctx c₁ c₂ (trans' c₁ c₂).denote ctx := by
induction c₂ generalizing c₁
next => intros; simp_all [trans', denoteAnd']
next c cs ih => simp [denoteAnd']; intros; simp [trans']; apply ih; apply denote'_trans <;> assumption
def Cnstrs.denoteAnd (ctx : Context) (c : Cnstrs) : Prop :=
match c with
| [] => True
| c::cs => denoteAnd' ctx c cs
def Cnstrs.trans (c : Cnstrs) : Cnstr :=
match c with
| [] => trivialCnstr
| c::cs => trans' c cs
theorem Cnstrs.of_denoteAnd_trans {ctx : Context} {c : Cnstrs} : c.denoteAnd ctx c.trans.denote ctx := by
cases c <;> simp [*, trans, denoteAnd] <;> intros <;> simp [*]
def Cnstrs.isFalse (c : Cnstrs) : Bool :=
c.trans.isFalse
theorem Cnstrs.unsat' (ctx : Context) (c : Cnstrs) : c.isFalse = true ¬ c.denoteAnd ctx := by
simp [isFalse]; intro h₁ h₂
have := of_denoteAnd_trans h₂
have := Cnstr.of_isFalse ctx h₁
contradiction
/-- `denote ctx [c_1, ..., c_n] C` is `c_1.denote ctx → ... → c_n.denote ctx → C` -/
def Cnstrs.denote (ctx : Context) (cs : Cnstrs) (C : Prop) : Prop :=
match cs with
| [] => C
| c::cs => c.denote ctx denote ctx cs C
theorem Cnstrs.not_denoteAnd'_eq (ctx : Context) (c : Cnstr) (cs : Cnstrs) (C : Prop) : (denoteAnd' ctx c cs C) = denote ctx (c::cs) C := by
simp [denote]
induction cs generalizing c
next => simp [denoteAnd', denote]
next c' cs ih =>
simp [denoteAnd', denote, *]
theorem Cnstrs.not_denoteAnd_eq (ctx : Context) (cs : Cnstrs) (C : Prop) : (denoteAnd ctx cs C) = denote ctx cs C := by
cases cs
next => simp [denoteAnd, denote]
next c cs => apply not_denoteAnd'_eq
def Cnstr.isImpliedBy (cs : Cnstrs) (c : Cnstr) : Bool :=
cs.trans == c
/-! Main theorems used by `grind`. -/
/-- Auxiliary theorem used by `grind` to prove that a system of offset inequalities is unsatisfiable. -/
theorem Cnstrs.unsat (ctx : Context) (cs : Cnstrs) : cs.isFalse = true cs.denote ctx False := by
intro h
rw [ not_denoteAnd_eq]
apply unsat'
assumption
/-- Auxiliary theorem used by `grind` to prove an implied offset inequality. -/
theorem Cnstrs.imp (ctx : Context) (cs : Cnstrs) (c : Cnstr) (h : c.isImpliedBy cs = true) : cs.denote ctx (c.denote ctx) := by
rw [ eq_of_beq h]
rw [ not_denoteAnd_eq]
apply of_denoteAnd_trans
end Lean.Grind.Offset

View File

@@ -1,30 +0,0 @@
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.NotationExtra
namespace Lean.Grind
/-!
This is a hackish module for hovering node information in the `grind` tactic state.
-/
inductive NodeDef where
| unit
set_option linter.unusedVariables false in
def node_def (_ : Nat) {α : Sort u} {a : α} : NodeDef := .unit
@[app_unexpander node_def]
def nodeDefUnexpander : PrettyPrinter.Unexpander := fun stx => do
match stx with
| `($_ $id:num) => return mkIdent <| Name.mkSimple $ "#" ++ toString id.getNat
| _ => throw ()
@[app_unexpander NodeDef]
def NodeDefUnexpander : PrettyPrinter.Unexpander := fun _ => do
return mkIdent <| Name.mkSimple "NodeDef"
end Lean.Grind

View File

@@ -9,7 +9,7 @@ import Init.Core
namespace Lean.Grind
/-- A helper gadget for annotating nested proofs in goals. -/
def nestedProof (p : Prop) {h : p} : p := h
def nestedProof (p : Prop) (h : p) : p := h
/--
Gadget for marking terms that should not be normalized by `grind`s simplifier.
@@ -28,7 +28,7 @@ When `EqMatch a b origin` is `True`, we mark `origin` as a resolved case-split.
-/
def EqMatch (a b : α) {_origin : α} : Prop := a = b
theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nestedProof p hp) (@nestedProof q hq) := by
theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (nestedProof p hp) (nestedProof q hq) := by
subst h; apply HEq.refl
end Lean.Grind

View File

@@ -21,6 +21,11 @@ def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration
else
addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration)
(cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment := do
let env addDecl env opts decl cancelTk?
compileDecl env opts decl
def addDecl (decl : Declaration) : CoreM Unit := do
profileitM Exception "type checking" ( getOptions) do
withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do

View File

@@ -144,7 +144,11 @@ def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do
let type := mkApp (mkConst `IO) (mkConst `Unit)
let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.safe }
addAndCompile decl
IO.ofExcept (setBuiltinInitAttr ( getEnv) name) >>= setEnv
match ( getEnv).addAndCompile {} decl with
-- TODO: pretty print error
| Except.error e => do
let msg (e.toMessageData {}).toString
throwError "failed to emit registration code for builtin '{forDecl}': {msg}"
| Except.ok env => IO.ofExcept (setBuiltinInitAttr env name) >>= setEnv
end Lean

View File

@@ -53,3 +53,18 @@ def isUnsafeRecName? : Name → Option Name
| _ => none
end Compiler
namespace Environment
/--
Compile the given block of mutual declarations.
Assumes the declarations have already been added to the environment using `addDecl`.
-/
@[extern "lean_compile_decls"]
opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment
/-- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/
def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
end Environment

View File

@@ -514,16 +514,13 @@ register_builtin_option compiler.enableNew : Bool := {
@[extern "lean_lcnf_compile_decls"]
opaque compileDeclsNew (declNames : List Name) : CoreM Unit
@[extern "lean_compile_decls"]
opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment
def compileDecl (decl : Declaration) : CoreM Unit := do
let opts getOptions
let decls := Compiler.getDeclNamesForCodeGen decl
if compiler.enableNew.get opts then
compileDeclsNew decls
let res withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do
return compileDeclsOld ( getEnv) opts decls
return ( getEnv).compileDecl opts decl
match res with
| Except.ok env => setEnv env
| Except.error (KernelException.other msg) =>
@@ -536,7 +533,7 @@ def compileDecls (decls : List Name) : CoreM Unit := do
let opts getOptions
if compiler.enableNew.get opts then
compileDeclsNew decls
match compileDeclsOld ( getEnv) opts decls with
match ( getEnv).compileDecls opts decls with
| Except.ok env => setEnv env
| Except.error (KernelException.other msg) =>
throwError msg

View File

@@ -24,7 +24,7 @@ abbrev empty : AssocList α β :=
instance : EmptyCollection (AssocList α β) := empty
abbrev insertNew (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
abbrev insert (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
m.cons k v
def isEmpty : AssocList α β Bool
@@ -77,12 +77,6 @@ def replace [BEq α] (a : α) (b : β) : AssocList α β → AssocList α β
| true => cons a b es
| false => cons k v (replace a b es)
def insert [BEq α] (m : AssocList α β) (k : α) (v : β) : AssocList α β :=
if m.contains k then
m.replace k v
else
m.insertNew k v
def erase [BEq α] (a : α) : AssocList α β AssocList α β
| nil => nil
| cons k v es => match k == a with

View File

@@ -1474,7 +1474,7 @@ where
| field::fields, false => .fieldName field field.getId.getString! none fIdent :: toLVals fields false
/-- Resolve `(.$id:ident)` using the expected type to infer namespace. -/
private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : TermElabM Name := do
tryPostponeIfNoneOrMVar expectedType?
let some expectedType := expectedType?
| throwError "invalid dotted identifier notation, expected type must be known"
@@ -1489,7 +1489,7 @@ where
withForallBody body k
else
k body
go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM Expr := do
go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM Name := do
let resultType instantiateMVars resultType
let resultTypeFn := resultType.cleanupAnnotations.getAppFn
try
@@ -1497,12 +1497,9 @@ where
let .const declName .. := resultTypeFn.cleanupAnnotations
| throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
let idNew := declName ++ id.getId.eraseMacroScopes
if ( getEnv).contains idNew then
mkConst idNew
else if let some (fvar, []) resolveLocalName idNew then
return fvar
else
unless ( getEnv).contains idNew do
throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
return idNew
catch
| ex@(.error ..) =>
match ( unfoldDefinition? resultType) with
@@ -1551,7 +1548,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
| `(_) => throwError "placeholders '_' cannot be used where a function is expected"
| `(.$id:ident) =>
addCompletionInfo <| CompletionInfo.dotId f id.getId ( getLCtx) expectedType?
let fConst resolveDotName id expectedType?
let fConst mkConst ( resolveDotName id expectedType?)
let s observing do
-- Use (force := true) because we want to record the result of .ident resolution even in patterns
let fConst addTermInfo f fConst expectedType? (force := true)

View File

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.Parser.Module
import Lean.Util.Paths
import Lean.Data.Json
namespace Lean.Elab
@@ -42,12 +42,4 @@ def printImports (input : String) (fileName : Option String) : IO Unit := do
let fname findOLean dep.module
IO.println fname
@[export lean_print_import_srcs]
def printImportSrcs (input : String) (fileName : Option String) : IO Unit := do
let sp initSrcSearchPath
let (deps, _, _) parseImports input fileName
for dep in deps do
let fname findLean sp dep.module
IO.println fname
end Lean.Elab

View File

@@ -35,9 +35,9 @@ def elabGrindPattern : CommandElab := fun stx => do
| _ => throwUnsupportedSyntax
def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
let goals Grind.main mvarId config mainDeclName fallback
unless goals.isEmpty do
throwError "`grind` failed\n{← Grind.goalsToMessageData goals}"
let mvarIds Grind.main mvarId config mainDeclName fallback
unless mvarIds.isEmpty do
throwError "`grind` failed\n{goalsToMessageData mvarIds}"
private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
let some fallback := fallback? | return (pure ())

View File

@@ -11,14 +11,14 @@ import Lean.Meta.DecLevel
namespace Lean.Meta
/-- Returns `id e` -/
/-- Return `id e` -/
def mkId (e : Expr) : MetaM Expr := do
let type inferType e
let u getLevel type
return mkApp2 (mkConst ``id [u]) type e
/--
Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, returns
Given `e` s.t. `inferType e` is definitionally equal to `expectedType`, return
term `@id expectedType e`. -/
def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
let u getLevel expectedType
@@ -38,13 +38,13 @@ def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
let u2 getLevel ety
return mkAppN (.const ``letFun [u1, u2]) #[α, β, v, f]
/-- Returns `a = b`. -/
/-- Return `a = b`. -/
def mkEq (a b : Expr) : MetaM Expr := do
let aType inferType a
let u getLevel aType
return mkApp3 (mkConst ``Eq [u]) aType a b
/-- Returns `HEq a b`. -/
/-- Return `HEq a b`. -/
def mkHEq (a b : Expr) : MetaM Expr := do
let aType inferType a
let bType inferType b
@@ -52,7 +52,7 @@ def mkHEq (a b : Expr) : MetaM Expr := do
return mkApp4 (mkConst ``HEq [u]) aType a bType b
/--
If `a` and `b` have definitionally equal types, returns `Eq a b`, otherwise returns `HEq a b`.
If `a` and `b` have definitionally equal types, return `Eq a b`, otherwise return `HEq a b`.
-/
def mkEqHEq (a b : Expr) : MetaM Expr := do
let aType inferType a
@@ -63,25 +63,25 @@ def mkEqHEq (a b : Expr) : MetaM Expr := do
else
return mkApp4 (mkConst ``HEq [u]) aType a bType b
/-- Returns a proof of `a = a`. -/
/-- Return a proof of `a = a`. -/
def mkEqRefl (a : Expr) : MetaM Expr := do
let aType inferType a
let u getLevel aType
return mkApp2 (mkConst ``Eq.refl [u]) aType a
/-- Returns a proof of `HEq a a`. -/
/-- Return a proof of `HEq a a`. -/
def mkHEqRefl (a : Expr) : MetaM Expr := do
let aType inferType a
let u getLevel aType
return mkApp2 (mkConst ``HEq.refl [u]) aType a
/-- Given `hp : P` and `nhp : Not P`, returns an instance of type `e`. -/
/-- Given `hp : P` and `nhp : Not P` returns an instance of type `e`. -/
def mkAbsurd (e : Expr) (hp hnp : Expr) : MetaM Expr := do
let p inferType hp
let u getLevel e
return mkApp4 (mkConst ``absurd [u]) p e hp hnp
/-- Given `h : False`, returns an instance of type `e`. -/
/-- Given `h : False`, return an instance of type `e`. -/
def mkFalseElim (e : Expr) (h : Expr) : MetaM Expr := do
let u getLevel e
return mkApp2 (mkConst ``False.elim [u]) e h
@@ -108,7 +108,7 @@ def mkEqSymm (h : Expr) : MetaM Expr := do
return mkApp4 (mkConst ``Eq.symm [u]) α a b h
| none => throwAppBuilderException ``Eq.symm ("equality proof expected" ++ hasTypeMsg h hType)
/-- Given `h₁ : a = b` and `h₂ : b = c`, returns a proof of `a = c`. -/
/-- Given `h₁ : a = b` and `h₂ : b = c` returns a proof of `a = c`. -/
def mkEqTrans (h₁ h₂ : Expr) : MetaM Expr := do
if h₁.isAppOf ``Eq.refl then
return h₂
@@ -185,7 +185,7 @@ def mkHEqOfEq (h : Expr) : MetaM Expr := do
return mkApp4 (mkConst ``heq_of_eq [u]) α a b h
/--
If `e` is `@Eq.refl α a`, returns `a`.
If `e` is `@Eq.refl α a`, return `a`.
-/
def isRefl? (e : Expr) : Option Expr := do
if e.isAppOfArity ``Eq.refl 2 then
@@ -194,7 +194,7 @@ def isRefl? (e : Expr) : Option Expr := do
none
/--
If `e` is `@congrArg α β a b f h`, returns `α`, `f` and `h`.
If `e` is `@congrArg α β a b f h`, return `α`, `f` and `h`.
Also works if `e` can be turned into such an application (e.g. `congrFun`).
-/
def congrArg? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
@@ -336,14 +336,13 @@ private def withAppBuilderTrace [ToMessageData α] [ToMessageData β]
throw ex
/--
Returns the application `constName xs`.
Return the application `constName xs`.
It tries to fill the implicit arguments before the last element in `xs`.
Remark:
``mkAppM `arbitrary #[α]`` returns `@arbitrary.{u} α` without synthesizing
the implicit argument occurring after `α`.
Given a `x : ([Decidable p] → Bool) × Nat`, ``mkAppM `Prod.fst #[x]``,
returns `@Prod.fst ([Decidable p] → Bool) Nat x`.
Given a `x : ([Decidable p] → Bool) × Nat`, ``mkAppM `Prod.fst #[x]`` returns `@Prod.fst ([Decidable p] → Bool) Nat x`.
-/
def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := do
withAppBuilderTrace constName xs do withNewMCtxDepth do
@@ -466,9 +465,8 @@ def mkPure (monad : Expr) (e : Expr) : MetaM Expr :=
mkAppOptM ``Pure.pure #[monad, none, none, e]
/--
`mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
Remark: `fieldName` may be a subfield of `s`.
-/
`mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
Remark: `fieldName` may be a subfield of `s`. -/
partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
let type inferType s
let type whnf type
@@ -522,11 +520,11 @@ def mkSome (type value : Expr) : MetaM Expr := do
let u getDecLevel type
return mkApp2 (mkConst ``Option.some [u]) type value
/-- Returns `Decidable.decide p` -/
/-- Return `Decidable.decide p` -/
def mkDecide (p : Expr) : MetaM Expr :=
mkAppOptM ``Decidable.decide #[p, none]
/-- Returns a proof for `p : Prop` using `decide p` -/
/-- Return a proof for `p : Prop` using `decide p` -/
def mkDecideProof (p : Expr) : MetaM Expr := do
let decP mkDecide p
let decEqTrue mkEq decP (mkConst ``Bool.true)
@@ -534,75 +532,59 @@ def mkDecideProof (p : Expr) : MetaM Expr := do
let h mkExpectedTypeHint h decEqTrue
mkAppM ``of_decide_eq_true #[h]
/-- Returns `a < b` -/
/-- Return `a < b` -/
def mkLt (a b : Expr) : MetaM Expr :=
mkAppM ``LT.lt #[a, b]
/-- Returns `a <= b` -/
/-- Return `a <= b` -/
def mkLe (a b : Expr) : MetaM Expr :=
mkAppM ``LE.le #[a, b]
/-- Returns `Inhabited.default α` -/
/-- Return `Inhabited.default α` -/
def mkDefault (α : Expr) : MetaM Expr :=
mkAppOptM ``Inhabited.default #[α, none]
/-- Returns `@Classical.ofNonempty α _` -/
/-- Return `@Classical.ofNonempty α _` -/
def mkOfNonempty (α : Expr) : MetaM Expr := do
mkAppOptM ``Classical.ofNonempty #[α, none]
/-- Returns `funext h` -/
/-- Return `funext h` -/
def mkFunExt (h : Expr) : MetaM Expr :=
mkAppM ``funext #[h]
/-- Returns `propext h` -/
/-- Return `propext h` -/
def mkPropExt (h : Expr) : MetaM Expr :=
mkAppM ``propext #[h]
/-- Returns `let_congr h₁ h₂` -/
/-- Return `let_congr h₁ h₂` -/
def mkLetCongr (h₁ h₂ : Expr) : MetaM Expr :=
mkAppM ``let_congr #[h₁, h₂]
/-- Returns `let_val_congr b h` -/
/-- Return `let_val_congr b h` -/
def mkLetValCongr (b h : Expr) : MetaM Expr :=
mkAppM ``let_val_congr #[b, h]
/-- Returns `let_body_congr a h` -/
/-- Return `let_body_congr a h` -/
def mkLetBodyCongr (a h : Expr) : MetaM Expr :=
mkAppM ``let_body_congr #[a, h]
/-- Returns `@of_eq_true p h` -/
def mkOfEqTrueCore (p : Expr) (h : Expr) : Expr :=
match_expr h with
| eq_true _ h => h
| _ => mkApp2 (mkConst ``of_eq_true) p h
/-- Return `of_eq_true h` -/
def mkOfEqTrue (h : Expr) : MetaM Expr :=
mkAppM ``of_eq_true #[h]
/-- Returns `of_eq_true h` -/
def mkOfEqTrue (h : Expr) : MetaM Expr := do
match_expr h with
| eq_true _ h => return h
| _ => mkAppM ``of_eq_true #[h]
/-- Returns `eq_true h` -/
def mkEqTrueCore (p : Expr) (h : Expr) : Expr :=
match_expr h with
| of_eq_true _ h => h
| _ => mkApp2 (mkConst ``eq_true) p h
/-- Returns `eq_true h` -/
def mkEqTrue (h : Expr) : MetaM Expr := do
match_expr h with
| of_eq_true _ h => return h
| _ => return mkApp2 (mkConst ``eq_true) ( inferType h) h
/-- Return `eq_true h` -/
def mkEqTrue (h : Expr) : MetaM Expr :=
mkAppM ``eq_true #[h]
/--
Returns `eq_false h`
Return `eq_false h`
`h` must have type definitionally equal to `¬ p` in the current
reducibility setting. -/
def mkEqFalse (h : Expr) : MetaM Expr :=
mkAppM ``eq_false #[h]
/--
Returns `eq_false' h`
Return `eq_false' h`
`h` must have type definitionally equal to `p → False` in the current
reducibility setting. -/
def mkEqFalse' (h : Expr) : MetaM Expr :=
@@ -620,7 +602,7 @@ def mkImpDepCongrCtx (h₁ h₂ : Expr) : MetaM Expr :=
def mkForallCongr (h : Expr) : MetaM Expr :=
mkAppM ``forall_congr #[h]
/-- Returns instance for `[Monad m]` if there is one -/
/-- Return instance for `[Monad m]` if there is one -/
def isMonad? (m : Expr) : MetaM (Option Expr) :=
try
let monadType mkAppM `Monad #[m]
@@ -631,52 +613,52 @@ def isMonad? (m : Expr) : MetaM (Option Expr) :=
catch _ =>
pure none
/-- Returns `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n` -/
/-- Return `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n` -/
def mkNumeral (type : Expr) (n : Nat) : MetaM Expr := do
let u getDecLevel type
let inst synthInstance (mkApp2 (mkConst ``OfNat [u]) type (mkRawNatLit n))
return mkApp3 (mkConst ``OfNat.ofNat [u]) type (mkRawNatLit n) inst
/--
Returns `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.
This method assumes `a` and `b` have the same type, and typeclass `className` is heterogeneous.
Examples of supported classes: `HAdd`, `HSub`, `HMul`.
We use heterogeneous operators to ensure we have a uniform representation.
-/
Return `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.
This method assumes `a` and `b` have the same type, and typeclass `className` is heterogeneous.
Examples of supported classes: `HAdd`, `HSub`, `HMul`.
We use heterogeneous operators to ensure we have a uniform representation.
-/
private def mkBinaryOp (className : Name) (opName : Name) (a b : Expr) : MetaM Expr := do
let aType inferType a
let u getDecLevel aType
let inst synthInstance (mkApp3 (mkConst className [u, u, u]) aType aType aType)
return mkApp6 (mkConst opName [u, u, u]) aType aType aType inst a b
/-- Returns `a + b` using a heterogeneous `+`. This method assumes `a` and `b` have the same type. -/
/-- Return `a + b` using a heterogeneous `+`. This method assumes `a` and `b` have the same type. -/
def mkAdd (a b : Expr) : MetaM Expr := mkBinaryOp ``HAdd ``HAdd.hAdd a b
/-- Returns `a - b` using a heterogeneous `-`. This method assumes `a` and `b` have the same type. -/
/-- Return `a - b` using a heterogeneous `-`. This method assumes `a` and `b` have the same type. -/
def mkSub (a b : Expr) : MetaM Expr := mkBinaryOp ``HSub ``HSub.hSub a b
/-- Returns `a * b` using a heterogeneous `*`. This method assumes `a` and `b` have the same type. -/
/-- Return `a * b` using a heterogeneous `*`. This method assumes `a` and `b` have the same type. -/
def mkMul (a b : Expr) : MetaM Expr := mkBinaryOp ``HMul ``HMul.hMul a b
/--
Returns `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
This method assumes `a` and `b` have the same type.
Examples of supported classes: `LE` and `LT`.
We use heterogeneous operators to ensure we have a uniform representation.
-/
Return `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
This method assumes `a` and `b` have the same type.
Examples of supported classes: `LE` and `LT`.
We use heterogeneous operators to ensure we have a uniform representation.
-/
private def mkBinaryRel (className : Name) (rName : Name) (a b : Expr) : MetaM Expr := do
let aType inferType a
let u getDecLevel aType
let inst synthInstance (mkApp (mkConst className [u]) aType)
return mkApp4 (mkConst rName [u]) aType inst a b
/-- Returns `a ≤ b`. This method assumes `a` and `b` have the same type. -/
/-- Return `a ≤ b`. This method assumes `a` and `b` have the same type. -/
def mkLE (a b : Expr) : MetaM Expr := mkBinaryRel ``LE ``LE.le a b
/-- Returns `a < b`. This method assumes `a` and `b` have the same type. -/
/-- Return `a < b`. This method assumes `a` and `b` have the same type. -/
def mkLT (a b : Expr) : MetaM Expr := mkBinaryRel ``LT ``LT.lt a b
/-- Given `h : a = b`, returns a proof for `a ↔ b`. -/
/-- Given `h : a = b`, return a proof for `a ↔ b`. -/
def mkIffOfEq (h : Expr) : MetaM Expr := do
if h.isAppOfArity ``propext 3 then
return h.appArg!

View File

@@ -35,7 +35,7 @@ def insert (s : FVarSubst) (fvarId : FVarId) (v : Expr) : FVarSubst :=
if s.contains fvarId then s
else
let map := s.map.mapVal fun e => e.replaceFVarId fvarId v;
{ map := map.insertNew fvarId v }
{ map := map.insert fvarId v }
def erase (s : FVarSubst) (fvarId : FVarId) : FVarSubst :=
{ map := s.map.erase fvarId }

View File

@@ -24,7 +24,6 @@ import Lean.Meta.Tactic.Grind.EMatchTheorem
import Lean.Meta.Tactic.Grind.EMatch
import Lean.Meta.Tactic.Grind.Main
import Lean.Meta.Tactic.Grind.CasesMatch
import Lean.Meta.Tactic.Grind.Arith
namespace Lean
@@ -43,11 +42,6 @@ builtin_initialize registerTraceClass `grind.simp
builtin_initialize registerTraceClass `grind.split
builtin_initialize registerTraceClass `grind.split.candidate
builtin_initialize registerTraceClass `grind.split.resolved
builtin_initialize registerTraceClass `grind.offset
builtin_initialize registerTraceClass `grind.offset.dist
builtin_initialize registerTraceClass `grind.offset.internalize
builtin_initialize registerTraceClass `grind.offset.internalize.term (inherited := true)
builtin_initialize registerTraceClass `grind.offset.propagate
/-! Trace options for `grind` developers -/
builtin_initialize registerTraceClass `grind.debug
@@ -60,6 +54,4 @@ builtin_initialize registerTraceClass `grind.debug.final
builtin_initialize registerTraceClass `grind.debug.forallPropagator
builtin_initialize registerTraceClass `grind.debug.split
builtin_initialize registerTraceClass `grind.debug.canon
builtin_initialize registerTraceClass `grind.debug.offset
builtin_initialize registerTraceClass `grind.debug.offset.proof
end Lean

View File

@@ -1,10 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Tactic.Grind.Arith.Util
import Lean.Meta.Tactic.Grind.Arith.Types
import Lean.Meta.Tactic.Grind.Arith.Offset
import Lean.Meta.Tactic.Grind.Arith.Main

View File

@@ -1,14 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Tactic.Grind.Arith.Offset
namespace Lean.Meta.Grind.Arith
def internalize (e : Expr) : GoalM Unit := do
Offset.internalizeCnstr e
end Lean.Meta.Grind.Arith

View File

@@ -1,14 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Tactic.Grind.Arith.Offset
namespace Lean.Meta.Grind.Arith
def checkInvariants : GoalM Unit :=
Offset.checkInvariants
end Lean.Meta.Grind.Arith

View File

@@ -1,34 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Tactic.Grind.PropagatorAttr
import Lean.Meta.Tactic.Grind.Arith.Offset
namespace Lean.Meta.Grind.Arith
namespace Offset
def isCnstr? (e : Expr) : GoalM (Option (Cnstr NodeId)) :=
return ( get).arith.offset.cnstrs.find? { expr := e }
def assertTrue (c : Cnstr NodeId) (p : Expr) : GoalM Unit := do
addEdge c.u c.v c.k ( mkOfEqTrue p)
def assertFalse (c : Cnstr NodeId) (p : Expr) : GoalM Unit := do
let p := mkOfNegEqFalse ( get').nodes c p
let c := c.neg
addEdge c.u c.v c.k p
end Offset
builtin_grind_propagator propagateLE LE.le := fun e => do
if ( isEqTrue e) then
if let some c Offset.isCnstr? e then
Offset.assertTrue c ( mkEqTrueProof e)
if ( isEqFalse e) then
if let some c Offset.isCnstr? e then
Offset.assertFalse c ( mkEqFalseProof e)
end Lean.Meta.Grind.Arith

View File

@@ -1,39 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.Basic
import Lean.Meta.Tactic.Grind.Types
namespace Lean.Meta.Grind.Arith.Offset
/-- Construct a model that statisfies all offset constraints -/
def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do
let s := goal.arith.offset
let nodes := s.nodes
let mut pre : Array (Option Int) := mkArray nodes.size none
for u in [:nodes.size] do
let val? := s.sources[u]!.foldl (init := @none Int) fun val? v k => Id.run do
let some va := pre[v]! | return val?
let val' := va - k
let some val := val? | return val'
if val' > val then return val' else val?
let val? := s.targets[u]!.foldl (init := val?) fun val? v k => Id.run do
let some va := pre[v]! | return val?
let val' := va + k
let some val := val? | return val'
if val' < val then return val' else val?
let val := val?.getD 0
pre := pre.set! u (some val)
let min := pre.foldl (init := 0) fun min val? => Id.run do
let some val := val? | return min
if val < min then val else min
let mut r := {}
for u in [:nodes.size] do
let some val := pre[u]! | unreachable!
let val := (val - min).toNat
r := r.push (nodes[u]!, val)
return r
end Lean.Meta.Grind.Arith.Offset

View File

@@ -1,255 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Grind.Offset
import Lean.Meta.Tactic.Grind.Types
import Lean.Meta.Tactic.Grind.Arith.ProofUtil
namespace Lean.Meta.Grind.Arith.Offset
/-!
This module implements a decision procedure for offset constraints of the form:
```
x + k ≤ y
x ≤ y + k
```
where `k` is a numeral.
Each constraint is represented as an edge in a weighted graph.
The constraint `x + k ≤ y` is represented as a negative edge.
The shortest path between two nodes in the graph corresponds to an implied inequality.
When adding a new edge, the state is considered unsatisfiable if the new edge creates a negative cycle.
An incremental Floyd-Warshall algorithm is used to find the shortest paths between all nodes.
This module can also handle offset equalities of the form `x + k = y` by representing them with two edges:
```
x + k ≤ y
y ≤ x + k
```
The main advantage of this module over a full linear integer arithmetic procedure is
its ability to efficiently detect all implied equalities and inequalities.
-/
def get' : GoalM State := do
return ( get).arith.offset
@[inline] def modify' (f : State State) : GoalM Unit := do
modify fun s => { s with arith.offset := f s.arith.offset }
def mkNode (expr : Expr) : GoalM NodeId := do
if let some nodeId := ( get').nodeMap.find? { expr } then
return nodeId
let nodeId : NodeId := ( get').nodes.size
trace[grind.offset.internalize.term] "{expr} ↦ #{nodeId}"
modify' fun s => { s with
nodes := s.nodes.push expr
nodeMap := s.nodeMap.insert { expr } nodeId
sources := s.sources.push {}
targets := s.targets.push {}
proofs := s.proofs.push {}
}
return nodeId
private def getExpr (u : NodeId) : GoalM Expr := do
return ( get').nodes[u]!
private def getDist? (u v : NodeId) : GoalM (Option Int) := do
return ( get').targets[u]!.find? v
private def getProof? (u v : NodeId) : GoalM (Option ProofInfo) := do
return ( get').proofs[u]!.find? v
/--
Returns a proof for `u + k ≤ v` (or `u ≤ v + k`) where `k` is the
shortest path between `u` and `v`.
-/
private partial def mkProofForPath (u v : NodeId) : GoalM Expr := do
go ( getProof? u v).get!
where
go (p : ProofInfo) : GoalM Expr := do
if u == p.w then
return p.proof
else
let p' := ( getProof? u p.w).get!
go (mkTrans ( get').nodes p' p v)
/--
Given a new edge edge `u --(kuv)--> v` justified by proof `huv` s.t.
it creates a negative cycle with the existing path `v --{kvu}-->* u`, i.e., `kuv + kvu < 0`,
this function closes the current goal by constructing a proof of `False`.
-/
private def setUnsat (u v : NodeId) (kuv : Int) (huv : Expr) (kvu : Int) : GoalM Unit := do
assert! kuv + kvu < 0
let hvu mkProofForPath v u
let u getExpr u
let v getExpr v
closeGoal (mkUnsatProof u v kuv huv kvu hvu)
/-- Sets the new shortest distance `k` between nodes `u` and `v`. -/
private def setDist (u v : NodeId) (k : Int) : GoalM Unit := do
trace[grind.offset.dist] "{({ u, v, k : Cnstr NodeId})}"
modify' fun s => { s with
targets := s.targets.modify u fun es => es.insert v k
sources := s.sources.modify v fun es => es.insert u k
}
private def setProof (u v : NodeId) (p : ProofInfo) : GoalM Unit := do
modify' fun s => { s with
proofs := s.proofs.modify u fun es => es.insert v p
}
@[inline]
private def forEachSourceOf (u : NodeId) (f : NodeId Int GoalM Unit) : GoalM Unit := do
( get').sources[u]!.forM f
@[inline]
private def forEachTargetOf (u : NodeId) (f : NodeId Int GoalM Unit) : GoalM Unit := do
( get').targets[u]!.forM f
/-- Returns `true` if `k` is smaller than the shortest distance between `u` and `v` -/
private def isShorter (u v : NodeId) (k : Int) : GoalM Bool := do
if let some k' getDist? u v then
return k < k'
else
return true
/--
Tries to assign `e` to `True`, which is represented by constraint `c` (from `u` to `v`), using the
path `u --(k)--> v`.
-/
private def propagateTrue (u v : NodeId) (k : Int) (c : Cnstr NodeId) (e : Expr) : GoalM Bool := do
if k c.k then
trace[grind.offset.propagate] "{{ u, v, k : Cnstr NodeId}} ==> {e} = True"
let kuv mkProofForPath u v
let u getExpr u
let v getExpr v
pushEqTrue e <| mkPropagateEqTrueProof u v k kuv c.k
return true
return false
example (x y : Nat) : x + 2 y ¬ (y x + 1) := by omega
/--
Tries to assign `e` to `False`, which is represented by constraint `c` (from `v` to `u`), using the
path `u --(k)--> v`.
-/
private def propagateFalse (u v : NodeId) (k : Int) (c : Cnstr NodeId) (e : Expr) : GoalM Bool := do
if k + c.k < 0 then
trace[grind.offset.propagate] "{{ u, v, k : Cnstr NodeId}} ==> {e} = False"
let kuv mkProofForPath u v
let u getExpr u
let v getExpr v
pushEqFalse e <| mkPropagateEqFalseProof u v k kuv c.k
return false
/--
Auxiliary function for implementing `propagateAll`.
Traverses the constraints `c` (representing an expression `e`) s.t.
`c.u = u` and `c.v = v`, it removes `c` from the list of constraints
associated with `(u, v)` IF
- `e` is already assigned, or
- `f c e` returns true
-/
@[inline]
private def updateCnstrsOf (u v : NodeId) (f : Cnstr NodeId Expr GoalM Bool) : GoalM Unit := do
if let some cs := ( get').cnstrsOf.find? (u, v) then
let cs' cs.filterM fun (c, e) => do
if ( isEqTrue e <||> isEqFalse e) then
return false -- constraint was already assigned
else
return !( f c e)
modify' fun s => { s with cnstrsOf := s.cnstrsOf.insert (u, v) cs' }
/-- Performs constraint propagation. -/
private def propagateAll (u v : NodeId) (k : Int) : GoalM Unit := do
updateCnstrsOf u v fun c e => return !( propagateTrue u v k c e)
updateCnstrsOf v u fun c e => return !( propagateFalse u v k c e)
/--
If `isShorter u v k`, updates the shortest distance between `u` and `v`.
`w` is the penultimate node in the path from `u` to `v`.
-/
private def updateIfShorter (u v : NodeId) (k : Int) (w : NodeId) : GoalM Unit := do
if ( isShorter u v k) then
setDist u v k
setProof u v ( getProof? w v).get!
propagateAll u v k
/--
Adds an edge `u --(k) --> v` justified by the proof term `p`, and then
if no negative cycle was created, updates the shortest distance of affected
node pairs.
-/
def addEdge (u : NodeId) (v : NodeId) (k : Int) (p : Expr) : GoalM Unit := do
if ( isInconsistent) then return ()
if let some k' getDist? v u then
if k'+k < 0 then
setUnsat u v k p k'
return ()
if ( isShorter u v k) then
setDist u v k
setProof u v { w := u, k, proof := p }
propagateAll u v k
update
where
update : GoalM Unit := do
forEachTargetOf v fun j k₂ => do
/- Check whether new path: `u -(k)-> v -(k₂)-> j` is shorter -/
updateIfShorter u j (k+k₂) v
forEachSourceOf u fun i k₁ => do
/- Check whether new path: `i -(k₁)-> u -(k)-> v` is shorter -/
updateIfShorter i v (k₁+k) u
forEachTargetOf v fun j k₂ => do
/- Check whether new path: `i -(k₁)-> u -(k)-> v -(k₂) -> j` is shorter -/
updateIfShorter i j (k₁+k+k₂) v
def internalizeCnstr (e : Expr) : GoalM Unit := do
let some c := isNatOffsetCnstr? e | return ()
let u mkNode c.u
let v mkNode c.v
let c := { c with u, v }
if let some k getDist? u v then
if ( propagateTrue u v k c e) then
return ()
if let some k getDist? v u then
if ( propagateFalse v u k c e) then
return ()
trace[grind.offset.internalize] "{e} ↦ {c}"
modify' fun s => { s with
cnstrs := s.cnstrs.insert { expr := e } c
cnstrsOf :=
let cs := if let some cs := s.cnstrsOf.find? (u, v) then (c, e) :: cs else [(c, e)]
s.cnstrsOf.insert (u, v) cs
}
def traceDists : GoalM Unit := do
let s get'
for u in [:s.targets.size], es in s.targets.toArray do
for (v, k) in es do
trace[grind.offset.dist] "#{u} -({k})-> #{v}"
def Cnstr.toExpr (c : Cnstr NodeId) : GoalM Expr := do
let u := ( get').nodes[c.u]!
let v := ( get').nodes[c.v]!
let mk := if c.le then mkNatLE else mkNatEq
if c.k == 0 then
return mk u v
else if c.k < 0 then
return mk (mkNatAdd u (Lean.toExpr ((-c.k).toNat))) v
else
return mk u (mkNatAdd v (Lean.toExpr c.k.toNat))
def checkInvariants : GoalM Unit := do
let s get'
for u in [:s.targets.size], es in s.targets.toArray do
for (v, k) in es do
let c : Cnstr NodeId := { u, v, k }
trace[grind.debug.offset] "{c}"
let p mkProofForPath u v
trace[grind.debug.offset.proof] "{p} : {← inferType p}"
check p
unless ( withDefault <| isDefEq ( inferType p) ( Cnstr.toExpr c)) do
trace[grind.debug.offset.proof] "failed: {← inferType p} =?= {← Cnstr.toExpr c}"
unreachable!
end Lean.Meta.Grind.Arith.Offset

View File

@@ -1,168 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Grind.Offset
import Init.Grind.Lemmas
import Lean.Meta.Tactic.Grind.Types
namespace Lean.Meta.Grind.Arith
/-!
Helper functions for constructing proof terms in the arithmetic procedures.
-/
namespace Offset
/-- Returns a proof for `true = true` -/
def rfl_true : Expr := mkConst ``Grind.rfl_true
private def toExprN (n : Int) :=
assert! n >= 0
toExpr n.toNat
open Lean.Grind in
/--
Assume `pi₁` is `{ w := u, k := k₁, proof := p₁ }` and `pi₂` is `{ w := w, k := k₂, proof := p₂ }`
`p₁` is the proof for edge `u -(k₁) → w` and `p₂` the proof for edge `w -(k₂)-> v`.
Then, this function returns a proof for edge `u -(k₁+k₂) -> v`.
-/
def mkTrans (nodes : PArray Expr) (pi₁ : ProofInfo) (pi₂ : ProofInfo) (v : NodeId) : ProofInfo :=
let { w := u, k := k₁, proof := p₁ } := pi₁
let { w, k := k₂, proof := p₂ } := pi₂
let u := nodes[u]!
let w := nodes[w]!
let v := nodes[v]!
let p := if k₁ == 0 then
if k₂ == 0 then
-- u ≤ w, w ≤ v
mkApp5 (mkConst ``Nat.le_trans) u w v p₁ p₂
else if k₂ > 0 then
-- u ≤ v, w ≤ v + k₂
mkApp6 (mkConst ``Nat.le_ro) u w v (toExprN k₂) p₁ p₂
else
let k₂ := - k₂
-- u ≤ w, w + k₂ ≤ v
mkApp6 (mkConst ``Nat.le_lo) u w v (toExprN k₂) p₁ p₂
else if k₁ < 0 then
let k₁ := -k₁
if k₂ == 0 then
mkApp6 (mkConst ``Nat.lo_le) u w v (toExprN k₁) p₁ p₂
else if k₂ < 0 then
let k₂ := -k₂
mkApp7 (mkConst ``Nat.lo_lo) u w v (toExprN k₁) (toExprN k₂) p₁ p₂
else
let ke₁ := toExprN k₁
let ke₂ := toExprN k₂
if k₁ > k₂ then
mkApp8 (mkConst ``Nat.lo_ro_1) u w v ke₁ ke₂ rfl_true p₁ p₂
else
mkApp7 (mkConst ``Nat.lo_ro_2) u w v ke₁ ke₂ p₁ p₂
else
let ke₁ := toExprN k₁
if k₂ == 0 then
mkApp6 (mkConst ``Nat.ro_le) u w v ke₁ p₁ p₂
else if k₂ < 0 then
let k₂ := -k₂
let ke₂ := toExprN k₂
if k₂ > k₁ then
mkApp8 (mkConst ``Nat.ro_lo_2) u w v ke₁ ke₂ rfl_true p₁ p₂
else
mkApp7 (mkConst ``Nat.ro_lo_1) u w v ke₁ ke₂ p₁ p₂
else
let ke₂ := toExprN k₂
mkApp7 (mkConst ``Nat.ro_ro) u w v ke₁ ke₂ p₁ p₂
{ w := pi₁.w, k := k₁+k₂, proof := p }
open Lean.Grind in
def mkOfNegEqFalse (nodes : PArray Expr) (c : Cnstr NodeId) (h : Expr) : Expr :=
let u := nodes[c.u]!
let v := nodes[c.v]!
if c.k == 0 then
mkApp3 (mkConst ``Nat.of_le_eq_false) u v h
else if c.k == -1 && c.le then
mkApp3 (mkConst ``Nat.of_lo_eq_false_1) u v h
else if c.k < 0 then
mkApp4 (mkConst ``Nat.of_lo_eq_false) u v (toExprN (-c.k)) h
else
mkApp4 (mkConst ``Nat.of_ro_eq_false) u v (toExprN c.k) h
/--
Returns a proof of `False` using a negative cycle composed of
- `u --(kuv)--> v` with proof `huv`
- `v --(kvu)--> u` with proof `hvu`
-/
def mkUnsatProof (u v : Expr) (kuv : Int) (huv : Expr) (kvu : Int) (hvu : Expr) : Expr :=
if kuv == 0 then
assert! kvu < 0
mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) u v (toExprN (-kvu)) rfl_true huv hvu
else if kvu == 0 then
mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) v u (toExprN (-kuv)) rfl_true hvu huv
else if kuv < 0 then
if kvu > 0 then
mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) u v (toExprN (-kuv)) (toExprN kvu) rfl_true huv hvu
else
assert! kvu < 0
mkApp7 (mkConst ``Grind.Nat.unsat_lo_lo) u v (toExprN (-kuv)) (toExprN (-kvu)) rfl_true huv hvu
else
assert! kuv > 0 && kvu < 0
mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) v u (toExprN (-kvu)) (toExprN kuv) rfl_true hvu huv
/--
Given a path `u --(kuv)--> v` justified by proof `huv`,
construct a proof of `e = True` where `e` is a term corresponding to the edgen `u --(k') --> v`
s.t. `k ≤ k'`
-/
def mkPropagateEqTrueProof (u v : Expr) (k : Int) (huv : Expr) (k' : Int) : Expr :=
if k == 0 then
if k' == 0 then
mkApp3 (mkConst ``Grind.Nat.le_eq_true_of_le) u v huv
else
assert! k' > 0
mkApp4 (mkConst ``Grind.Nat.ro_eq_true_of_le) u v (toExprN k') huv
else if k < 0 then
let k := -k
if k' == 0 then
mkApp4 (mkConst ``Grind.Nat.le_eq_true_of_lo) u v (toExprN k) huv
else if k' < 0 then
let k' := -k'
mkApp6 (mkConst ``Grind.Nat.lo_eq_true_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
else
assert! k' > 0
mkApp5 (mkConst ``Grind.Nat.ro_eq_true_of_lo) u v (toExprN k) (toExprN k') huv
else
assert! k > 0
assert! k' > 0
mkApp6 (mkConst ``Grind.Nat.ro_eq_true_of_ro) u v (toExprN k) (toExprN k') rfl_true huv
/--
Given a path `u --(kuv)--> v` justified by proof `huv`,
construct a proof of `e = False` where `e` is a term corresponding to the edgen `v --(k') --> u`
s.t. `k+k' < 0`
-/
def mkPropagateEqFalseProof (u v : Expr) (k : Int) (huv : Expr) (k' : Int) : Expr :=
if k == 0 then
assert! k' < 0
let k' := -k'
mkApp5 (mkConst ``Grind.Nat.lo_eq_false_of_le) u v (toExprN k') rfl_true huv
else if k < 0 then
let k := -k
if k' == 0 then
mkApp5 (mkConst ``Grind.Nat.le_eq_false_of_lo) u v (toExprN k) rfl_true huv
else if k' < 0 then
let k' := -k'
mkApp6 (mkConst ``Grind.Nat.lo_eq_false_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
else
assert! k' > 0
mkApp6 (mkConst ``Grind.Nat.ro_eq_false_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
else
assert! k > 0
assert! k' < 0
let k' := -k'
mkApp6 (mkConst ``Grind.Nat.lo_eq_false_of_ro) u v (toExprN k) (toExprN k') rfl_true huv
end Offset
end Lean.Meta.Grind.Arith

View File

@@ -1,66 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Data.PersistentArray
import Lean.Meta.Tactic.Grind.ENodeKey
import Lean.Meta.Tactic.Grind.Arith.Util
namespace Lean.Meta.Grind.Arith
namespace Offset
abbrev NodeId := Nat
instance : ToMessageData (Offset.Cnstr NodeId) where
toMessageData c := Offset.toMessageData (α := NodeId) (inst := { toMessageData n := m!"#{n}" }) c
/-- Auxiliary structure used for proof extraction. -/
structure ProofInfo where
w : NodeId
k : Int
proof : Expr
deriving Inhabited
/-- State of the constraint offset procedure. -/
structure State where
/-- Mapping from `NodeId` to the `Expr` represented by the node. -/
nodes : PArray Expr := {}
/-- Mapping from `Expr` to a node representing it. -/
nodeMap : PHashMap ENodeKey NodeId := {}
/-- Mapping from `Expr` representing inequalites to constraints. -/
cnstrs : PHashMap ENodeKey (Cnstr NodeId) := {}
/--
Mapping from pairs `(u, v)` to a list of offset constraints on `u` and `v`.
We use this mapping to implement exhaustive constraint propagation.
-/
cnstrsOf : PHashMap (NodeId × NodeId) (List (Cnstr NodeId × Expr)) := {}
/--
For each node with id `u`, `sources[u]` contains
pairs `(v, k)` s.t. there is a path from `v` to `u` with weight `k`.
-/
sources : PArray (AssocList NodeId Int) := {}
/--
For each node with id `u`, `targets[u]` contains
pairs `(v, k)` s.t. there is a path from `u` to `v` with weight `k`.
-/
targets : PArray (AssocList NodeId Int) := {}
/--
Proof reconstruction information. For each node with id `u`, `proofs[u]` contains
pairs `(v, { w, proof })` s.t. there is a path from `u` to `v`, and
`w` is the penultimate node in the path, and `proof` is the justification for
the last edge.
-/
proofs : PArray (AssocList NodeId ProofInfo) := {}
deriving Inhabited
end Offset
/-- State for the arithmetic procedures. -/
structure State where
offset : Offset.State := {}
deriving Inhabited
end Lean.Meta.Grind.Arith

View File

@@ -1,89 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Expr
import Lean.Message
namespace Lean.Meta.Grind.Arith
/-- Returns `true` if `e` is of the form `Nat` -/
def isNatType (e : Expr) : Bool :=
e.isConstOf ``Nat
/-- Returns `true` if `e` is of the form `@instHAdd Nat instAddNat` -/
def isInstAddNat (e : Expr) : Bool :=
let_expr instHAdd a b := e | false
isNatType a && b.isConstOf ``instAddNat
/-- Returns `true` if `e` is `instLENat` -/
def isInstLENat (e : Expr) : Bool :=
e.isConstOf ``instLENat
/--
Returns `some (a, b)` if `e` is of the form
```
@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) a b
```
-/
def isNatAdd? (e : Expr) : Option (Expr × Expr) :=
let_expr HAdd.hAdd _ _ _ i a b := e | none
if isInstAddNat i then some (a, b) else none
/-- Returns `some k` if `e` `@OfNat.ofNat Nat _ (instOfNatNat k)` -/
def isNatNum? (e : Expr) : Option Nat := Id.run do
let_expr OfNat.ofNat _ _ inst := e | none
let_expr instOfNatNat k := inst | none
let .lit (.natVal k) := k | none
some k
/-- Returns `some (a, k)` if `e` is of the form `a + k`. -/
def isNatOffset? (e : Expr) : Option (Expr × Nat) := Id.run do
let some (a, b) := isNatAdd? e | none
let some k := isNatNum? b | none
some (a, k)
/-- An offset constraint. -/
structure Offset.Cnstr (α : Type) where
u : α
v : α
k : Int := 0
le : Bool := true
deriving Inhabited
def Offset.Cnstr.neg : Cnstr α Cnstr α
| { u, v, k, le } => { u := v, v := u, le, k := -k - 1 }
example (c : Offset.Cnstr α) : c.neg.neg = c := by
cases c; simp [Offset.Cnstr.neg]; omega
def Offset.toMessageData [inst : ToMessageData α] (c : Offset.Cnstr α) : MessageData :=
match c.k, c.le with
| .ofNat 0, true => m!"{c.u} ≤ {c.v}"
| .ofNat 0, false => m!"{c.u} = {c.v}"
| .ofNat k, true => m!"{c.u} ≤ {c.v} + {k}"
| .ofNat k, false => m!"{c.u} = {c.v} + {k}"
| .negSucc k, true => m!"{c.u} + {k + 1} ≤ {c.v}"
| .negSucc k, false => m!"{c.u} + {k + 1} = {c.v}"
instance : ToMessageData (Offset.Cnstr Expr) where
toMessageData c := Offset.toMessageData c
/-- Returns `some cnstr` if `e` is offset constraint. -/
def isNatOffsetCnstr? (e : Expr) : Option (Offset.Cnstr Expr) :=
match_expr e with
| LE.le _ inst a b => if isInstLENat inst then go a b true else none
| Eq α a b => if isNatType α then go a b false else none
| _ => none
where
go (u v : Expr) (le : Bool) :=
if let some (u, k) := isNatOffset? u then
some { u, k := - k, v, le }
else if let some (v, k) := isNatOffset? v then
some { u, v, k := k, le }
else
some { u, v, le }
end Lean.Meta.Grind.Arith

View File

@@ -118,7 +118,7 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
unless ( isInconsistent) do
if valueInconsistency then
closeGoalWithValuesEq lhsRoot.self rhsRoot.self
trace_goal[grind.debug] "after addEqStep, {← (← get).ppState}"
trace_goal[grind.debug] "after addEqStep, {← ppState}"
checkInvariants
where
go (lhs rhs : Expr) (lhsNode rhsNode lhsRoot rhsRoot : ENode) (flipped : Bool) : GoalM Unit := do
@@ -141,7 +141,6 @@ where
updateRoots lhs rhsNode.root
trace_goal[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
reinsertParents parents
propagateEqcDown lhs
setENode lhsNode.root { ( getENode lhsRoot.self) with -- We must retrieve `lhsRoot` since it was updated.
next := rhsRoot.next
}
@@ -159,13 +158,14 @@ where
updateMT rhsRoot.self
updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
traverseEqc lhs fun n =>
setENode n.self { n with root := rootNew }
propagateEqcDown (lhs : Expr) : GoalM Unit := do
traverseEqc lhs fun n =>
let rec loop (e : Expr) : GoalM Unit := do
let n getENode e
setENode e { n with root := rootNew }
unless ( isInconsistent) do
propagateDown n.self
propagateDown e
if isSameExpr lhs n.next then return ()
loop n.next
loop lhs
/-- Ensures collection of equations to be processed is empty. -/
private def resetNewEqs : GoalM Unit :=
@@ -192,27 +192,22 @@ where
processTodo
/-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
private def addEq (lhs rhs proof : Expr) : GoalM Unit := do
def addEq (lhs rhs proof : Expr) : GoalM Unit := do
addEqCore lhs rhs proof false
/-- Adds a new heterogeneous equality `HEq lhs rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
private def addHEq (lhs rhs proof : Expr) : GoalM Unit := do
addEqCore lhs rhs proof true
/-- Save asserted facts for pretty printing goal. -/
private def storeFact (fact : Expr) : GoalM Unit := do
modify fun s => { s with facts := s.facts.push fact }
/-- Adds a new heterogeneous equality `HEq lhs rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
def addHEq (lhs rhs proof : Expr) : GoalM Unit := do
addEqCore lhs rhs proof true
/-- Internalizes `lhs` and `rhs`, and then adds equality `lhs = rhs`. -/
def addNewEq (lhs rhs proof : Expr) (generation : Nat) : GoalM Unit := do
storeFact ( mkEq lhs rhs)
internalize lhs generation
internalize rhs generation
addEq lhs rhs proof
/-- Adds a new `fact` justified by the given proof and using the given generation. -/
def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
storeFact fact
trace_goal[grind.assert] "{fact}"
if ( isInconsistent) then return ()
resetNewEqs

View File

@@ -170,43 +170,11 @@ private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTh
initial := {}
}
/--
Symbols with built-in support in `grind` are unsuitable as pattern candidates for E-matching.
This is because `grind` performs normalization operations and uses specialized data structures
to implement these symbols, which may interfere with E-matching behavior.
-/
-- TODO: create attribute?
private def forbiddenDeclNames := #[``Eq, ``HEq, ``Iff, ``And, ``Or, ``Not]
private def isForbidden (declName : Name) := forbiddenDeclNames.contains declName
/--
Auxiliary function to expand a pattern containing forbidden application symbols
into a multi-pattern.
This function enhances the usability of the `[grind =]` attribute by automatically handling
forbidden pattern symbols. For example, consider the following theorem tagged with this attribute:
```
getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]
```
Here, the selected pattern is `xs.getLast? = some a`, but `Eq` is a forbidden pattern symbol.
Instead of producing an error, this function converts the pattern into a multi-pattern,
allowing the attribute to be used conveniently.
The function recursively expands patterns with forbidden symbols by splitting them
into their sub-components. If the pattern does not contain forbidden symbols,
it is returned as-is.
-/
partial def splitWhileForbidden (pat : Expr) : List Expr :=
match_expr pat with
| Not p => splitWhileForbidden p
| And p₁ p₂ => splitWhileForbidden p₁ ++ splitWhileForbidden p₂
| Or p₁ p₂ => splitWhileForbidden p₁ ++ splitWhileForbidden p₂
| Eq _ lhs rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
| Iff lhs rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
| HEq _ lhs _ rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
| _ => [pat]
private def dontCare := mkConst (Name.mkSimple "[grind_dontcare]")
def mkGroundPattern (e : Expr) : Expr :=
@@ -500,8 +468,7 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
| _ => throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}"
let pat := if useLhs then lhs else rhs
let pat preprocessPattern pat normalizePattern
let pats := splitWhileForbidden (pat.abstract xs)
return (xs.size, pats)
return (xs.size, [pat.abstract xs])
mkEMatchTheoremCore origin levelParams numParams proof patterns
/--

View File

@@ -1,30 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Expr
namespace Lean.Meta.Grind
@[inline] def isSameExpr (a b : Expr) : Bool :=
-- It is safe to use pointer equality because we hashcons all expressions
-- inserted into the E-graph
unsafe ptrEq a b
/--
Key for the `ENodeMap` and `ParentMap` map.
We use pointer addresses and rely on the fact all internalized expressions
have been hash-consed, i.e., we have applied `shareCommon`.
-/
structure ENodeKey where
expr : Expr
instance : Hashable ENodeKey where
hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
instance : BEq ENodeKey where
beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
end Lean.Meta.Grind

View File

@@ -24,7 +24,7 @@ def propagateForallPropUp (e : Expr) : GoalM Unit := do
unless ( isEqTrue p) do return
trace_goal[grind.debug.forallPropagator] "isEqTrue, {e}"
let h₁ mkEqTrueProof p
let qh₁ := q.instantiate1 (mkOfEqTrueCore p h₁)
let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
let r simp qh₁
let q := mkLambda n bi p q
let q' := r.expr
@@ -65,7 +65,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
else
let idx modifyGet fun s => (s.nextThmIdx, { s with nextThmIdx := s.nextThmIdx + 1 })
pure <| .local ((`local).appendIndexAfter idx)
let proof := mkOfEqTrueCore e proof
let proof := mkApp2 (mkConst ``of_eq_true) e proof
let size := ( get).newThms.size
let gen getGeneration e
-- TODO: we should have a flag for collecting all unary patterns in a local theorem

View File

@@ -11,7 +11,6 @@ import Lean.Meta.Match.MatcherInfo
import Lean.Meta.Match.MatchEqsExt
import Lean.Meta.Tactic.Grind.Types
import Lean.Meta.Tactic.Grind.Util
import Lean.Meta.Tactic.Grind.Arith.Internalize
namespace Lean.Meta.Grind
@@ -197,7 +196,6 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
mkENode e generation
addCongrTable e
updateAppMap e
Arith.internalize e
propagateUp e
end

View File

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
prelude
import Lean.Meta.Tactic.Grind.Types
import Lean.Meta.Tactic.Grind.Proof
import Lean.Meta.Tactic.Grind.Arith.Inv
namespace Lean.Meta.Grind
@@ -59,12 +58,9 @@ private def checkParents (e : Expr) : GoalM Unit := do
found := true
break
-- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
if let .forallE _ d b _ := parent then
if let .forallE _ d _ _ := parent then
if ( checkChild d) then
found := true
unless b.hasLooseBVars do
if ( checkChild b) then
found := true
unless found do
assert! ( checkChild parent.getAppFn)
else
@@ -104,7 +100,6 @@ def checkInvariants (expensive := false) : GoalM Unit := do
checkEqc node
if expensive then
checkPtrEqImpliesStructEq
Arith.checkInvariants
if expensive && grind.debug.proofs.get ( getOptions) then
checkProofs

View File

@@ -72,8 +72,8 @@ def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goa
private def simple (goals : List Goal) : GrindM (List Goal) := do
applyToAll (assertAll >> ematchStar >> (splitNext >> assertAll >> ematchStar).iterate) goals
def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List Goal) := do
let go : GrindM (List Goal) := do
def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Fallback) : MetaM (List MVarId) := do
let go : GrindM (List MVarId) := do
let goals initCore mvarId
let goals simple goals
let goals goals.filterMapM fun goal => do
@@ -83,7 +83,7 @@ def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallba
if ( goal.mvarId.isAssigned) then return none
return some goal
trace[grind.debug.final] "{← ppGoals goals}"
return goals
return goals.map (·.mvarId)
go.run mainDeclName config fallback
end Lean.Meta.Grind

View File

@@ -5,132 +5,62 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Grind.Util
import Init.Grind.PP
import Lean.Meta.Tactic.Grind.Types
import Lean.Meta.Tactic.Grind.Arith.Model
namespace Lean.Meta.Grind
/-- Helper function for pretty printing the state for debugging purposes. -/
def Goal.ppENodeRef (goal : Goal) (e : Expr) : MetaM MessageData := do
let some n := goal.getENode? e | return "_"
let type inferType e
let u getLevel type
let d := mkApp3 (mkConst ``Grind.node_def [u]) (toExpr n.idx) type e
return m!"{d}"
@[inherit_doc Goal.ppENodeRef]
def ppENodeRef (e : Expr) : GoalM MessageData := do
( get).ppENodeRef e
def ppENodeRef (e : Expr) : GoalM Format := do
let some n getENode? e | return "_"
return f!"#{n.idx}"
/-- Helper function for pretty printing the state for debugging purposes. -/
private def Goal.ppENodeDeclValue (goal : Goal) (e : Expr) : MetaM MessageData := do
def ppENodeDeclValue (e : Expr) : GoalM Format := do
if e.isApp && !( isLitValue e) then
e.withApp fun f args => do
let r if f.isConst then
pure m!"{f}"
ppExpr f
else
goal.ppENodeRef f
ppENodeRef f
let mut r := r
for arg in args do
r := r ++ " " ++ ( goal.ppENodeRef arg)
r := r ++ " " ++ ( ppENodeRef arg)
return r
else
ppExpr e
/-- Helper function for pretty printing the state for debugging purposes. -/
private def Goal.ppENodeDecl (goal : Goal) (e : Expr) : MetaM MessageData := do
let mut r := m!"{← goal.ppENodeRef e} := {← goal.ppENodeDeclValue e}"
let n goal.getENode e
def ppENodeDecl (e : Expr) : GoalM Format := do
let mut r := f!"{← ppENodeRef e} := {← ppENodeDeclValue e}"
let n getENode e
unless isSameExpr e n.root do
r := r ++ m!" ↦ {← goal.ppENodeRef n.root}"
r := r ++ f!" ↦ {← ppENodeRef n.root}"
if n.interpreted then
r := r ++ ", [val]"
if n.ctor then
r := r ++ ", [ctor]"
if grind.debug.get ( getOptions) then
if let some target := goal.getTarget? e then
r := r ++ m!" ↝ {← goal.ppENodeRef target}"
if let some target getTarget? e then
r := r ++ f!" ↝ {← ppENodeRef target}"
return r
/-- Pretty print goal state for debugging purposes. -/
def Goal.ppState (goal : Goal) : MetaM MessageData := do
let mut r := m!"Goal:"
let nodes := goal.getENodes
def ppState : GoalM Format := do
let mut r := f!"Goal:"
let nodes getENodes
for node in nodes do
r := r ++ "\n" ++ ( goal.ppENodeDecl node.self)
let eqcs := goal.getEqcs
r := r ++ "\n" ++ ( ppENodeDecl node.self)
let eqcs getEqcs
for eqc in eqcs do
if eqc.length > 1 then
r := r ++ "\n" ++ "{" ++ (MessageData.joinSep ( eqc.mapM goal.ppENodeRef) ", ") ++ "}"
r := r ++ "\n" ++ "{" ++ (Format.joinSep ( eqc.mapM ppENodeRef) ", ") ++ "}"
return r
def ppGoals (goals : List Goal) : MetaM MessageData := do
let mut r := m!""
def ppGoals (goals : List Goal) : GrindM Format := do
let mut r := f!""
for goal in goals do
let m goal.ppState
r := r ++ Format.line ++ m
let (f, _) GoalM.run goal ppState
r := r ++ Format.line ++ f
return r
private def ppExprArray (cls : Name) (header : String) (es : Array Expr) (clsElem : Name := Name.mkSimple "_") : MessageData :=
let es := es.map fun e => .trace { cls := clsElem} m!"{e}" #[]
.trace { cls } header es
private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
let mut trueEqc? : Option MessageData := none
let mut falseEqc? : Option MessageData := none
let mut otherEqcs : Array MessageData := #[]
for eqc in goal.getEqcs do
if Option.isSome <| eqc.find? (·.isTrue) then
let eqc := eqc.filter fun e => !e.isTrue
unless eqc.isEmpty do
trueEqc? := ppExprArray `eqc "True propositions" eqc.toArray `prop
else if Option.isSome <| eqc.find? (·.isFalse) then
let eqc := eqc.filter fun e => !e.isFalse
unless eqc.isEmpty do
falseEqc? := ppExprArray `eqc "False propositions" eqc.toArray `prop
else if let e :: _ :: _ := eqc then
-- We may want to add a flag to pretty print equivalence classes of nested proofs
unless ( isProof e) do
otherEqcs := otherEqcs.push <| .trace { cls := `eqc } (.group ("{" ++ (MessageData.joinSep (eqc.map toMessageData) ("," ++ Format.line)) ++ "}")) #[]
let mut result := #[]
if let some trueEqc := trueEqc? then result := result.push trueEqc
if let some falseEqc := falseEqc? then result := result.push falseEqc
unless otherEqcs.isEmpty do
result := result.push <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
return result
private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
let m := m!"{← thm.origin.pp}\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
return .trace { cls := `thm } m #[]
private def ppActiveTheorems (goal : Goal) : MetaM MessageData := do
let m goal.thms.toArray.mapM ppEMatchTheorem
let m := m ++ ( goal.newThms.toArray.mapM ppEMatchTheorem)
if m.isEmpty then
return ""
else
return .trace { cls := `ematch } "E-matching" m
def ppOffset (goal : Goal) : MetaM MessageData := do
let s := goal.arith.offset
let nodes := s.nodes
if nodes.isEmpty then return ""
let model Arith.Offset.mkModel goal
let mut ms := #[]
for (e, val) in model do
ms := ms.push <| .trace { cls := `assign } m!"{e} := {val}" #[]
return .trace { cls := `offset } "Assignment satisfying offset contraints" ms
def goalToMessageData (goal : Goal) : MetaM MessageData := goal.mvarId.withContext do
let mut m : Array MessageData := #[.ofGoal goal.mvarId]
m := m.push <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
m := m ++ ( ppEqcs goal)
m := m.push ( ppActiveTheorems goal)
m := m.push ( ppOffset goal)
addMessageContextFull <| MessageData.joinSep m.toList ""
def goalsToMessageData (goals : List Goal) : MetaM MessageData :=
return MessageData.joinSep ( goals.mapM goalToMessageData) m!"\n"
end Lean.Meta.Grind

View File

@@ -126,32 +126,32 @@ builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
else if ( isEqTrue b) then
pushEq e a <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_right) a b ( mkEqTrueProof b)
else if ( isEqv a b) then
pushEqTrue e <| mkEqTrueCore e ( mkEqProof a b)
pushEqTrue e <| mkApp2 (mkConst ``eq_true) e ( mkEqProof a b)
/-- Propagates `Eq` downwards -/
builtin_grind_propagator propagateEqDown Eq := fun e => do
if ( isEqTrue e) then
let_expr Eq _ a b := e | return ()
pushEq a b <| mkOfEqTrueCore e ( mkEqTrueProof e)
pushEq a b <| mkApp2 (mkConst ``of_eq_true) e ( mkEqTrueProof e)
/-- Propagates `EqMatch` downwards -/
builtin_grind_propagator propagateEqMatchDown Grind.EqMatch := fun e => do
if ( isEqTrue e) then
let_expr Grind.EqMatch _ a b origin := e | return ()
markCaseSplitAsResolved origin
pushEq a b <| mkOfEqTrueCore e ( mkEqTrueProof e)
pushEq a b <| mkApp2 (mkConst ``of_eq_true) e ( mkEqTrueProof e)
/-- Propagates `HEq` downwards -/
builtin_grind_propagator propagateHEqDown HEq := fun e => do
if ( isEqTrue e) then
let_expr HEq _ a _ b := e | return ()
pushHEq a b <| mkOfEqTrueCore e ( mkEqTrueProof e)
pushHEq a b <| mkApp2 (mkConst ``of_eq_true) e ( mkEqTrueProof e)
/-- Propagates `HEq` upwards -/
builtin_grind_propagator propagateHEqUp HEq := fun e => do
let_expr HEq _ a _ b := e | return ()
if ( isEqv a b) then
pushEqTrue e <| mkEqTrueCore e ( mkHEqProof a b)
pushEqTrue e <| mkApp2 (mkConst ``eq_true) e ( mkHEqProof a b)
/-- Propagates `ite` upwards -/
builtin_grind_propagator propagateIte ite := fun e => do
@@ -166,7 +166,7 @@ builtin_grind_propagator propagateDIte ↑dite := fun e => do
let_expr f@dite α c h a b := e | return ()
if ( isEqTrue c) then
let h₁ mkEqTrueProof c
let ah₁ := mkApp a (mkOfEqTrueCore c h₁)
let ah₁ := mkApp a (mkApp2 (mkConst ``of_eq_true) c h₁)
let p simp ah₁
let r := p.expr
let h₂ p.getProof

View File

@@ -17,70 +17,43 @@ inductive CaseSplitStatus where
| ready (numCases : Nat) (isRec := false)
deriving Inhabited, BEq
/-- Given `c`, the condition of an `if-then-else`, check whether we need to case-split on the `if-then-else` or not -/
private def checkIteCondStatus (c : Expr) : GoalM CaseSplitStatus := do
if ( isEqTrue c <||> isEqFalse c) then
return .resolved
else
return .ready 2
/--
Given `e` of the form `a b`, check whether we are ready to case-split on `e`.
That is, `e` is `True`, but neither `a` nor `b` is `True`."
-/
private def checkDisjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
if ( isEqTrue e) then
if ( isEqTrue a <||> isEqTrue b) then
return .resolved
else
return .ready 2
else if ( isEqFalse e) then
return .resolved
else
return .notReady
/--
Given `e` of the form `a ∧ b`, check whether we are ready to case-split on `e`.
That is, `e` is `False`, but neither `a` nor `b` is `False`.
-/
private def checkConjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
if ( isEqTrue e) then
return .resolved
else if ( isEqFalse e) then
if ( isEqFalse a <||> isEqFalse b) then
return .resolved
else
return .ready 2
else
return .notReady
/--
Given `e` of the form `@Eq Prop a b`, check whether we are ready to case-split on `e`.
There are two cases:
1- `e` is `True`, but neither both `a` and `b` are `True`, nor both `a` and `b` are `False`.
2- `e` is `False`, but neither `a` is `True` and `b` is `False`, nor `a` is `False` and `b` is `True`.
-/
private def checkIffStatus (e a b : Expr) : GoalM CaseSplitStatus := do
if ( isEqTrue e) then
if ( (isEqTrue a <&&> isEqTrue b) <||> (isEqFalse a <&&> isEqFalse b)) then
return .resolved
else
return .ready 2
else if ( isEqFalse e) then
if ( (isEqTrue a <&&> isEqFalse b) <||> (isEqFalse a <&&> isEqTrue b)) then
return .resolved
else
return .ready 2
else
return .notReady
private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
match_expr e with
| Or a b => checkDisjunctStatus e a b
| And a b => checkConjunctStatus e a b
| Eq _ a b => checkIffStatus e a b
| ite _ c _ _ _ => checkIteCondStatus c
| dite _ c _ _ _ => checkIteCondStatus c
| Or a b =>
if ( isEqTrue e) then
if ( isEqTrue a <||> isEqTrue b) then
return .resolved
else
return .ready 2
else if ( isEqFalse e) then
return .resolved
else
return .notReady
| And a b =>
if ( isEqTrue e) then
return .resolved
else if ( isEqFalse e) then
if ( isEqFalse a <||> isEqFalse b) then
return .resolved
else
return .ready 2
else
return .notReady
| Eq _ _ _ =>
if ( isEqTrue e <||> isEqFalse e) then
return .ready 2
else
return .notReady
| ite _ c _ _ _ =>
if ( isEqTrue c <||> isEqFalse c) then
return .resolved
else
return .ready 2
| dite _ c _ _ _ =>
if ( isEqTrue c <||> isEqFalse c) then
return .resolved
else
return .ready 2
| _ =>
if ( isResolvedCaseSplit e) then
trace[grind.debug.split] "split resolved: {e}"
@@ -145,7 +118,7 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b ( mkEqTrueProof c)
else
return mkApp3 (mkConst ``Grind.of_eq_eq_false) a b ( mkEqFalseProof c)
| _ => return mkOfEqTrueCore c ( mkEqTrueProof c)
| _ => return mkApp2 (mkConst ``of_eq_true) c ( mkEqTrueProof c)
/-- Introduces new hypotheses in each goal. -/
private def introNewHyp (goals : List Goal) (acc : List Goal) (generation : Nat) : GrindM (List Goal) := do

View File

@@ -13,14 +13,17 @@ import Lean.Meta.CongrTheorems
import Lean.Meta.AbstractNestedProofs
import Lean.Meta.Tactic.Simp.Types
import Lean.Meta.Tactic.Util
import Lean.Meta.Tactic.Grind.ENodeKey
import Lean.Meta.Tactic.Grind.Canon
import Lean.Meta.Tactic.Grind.Attr
import Lean.Meta.Tactic.Grind.Arith.Types
import Lean.Meta.Tactic.Grind.EMatchTheorem
namespace Lean.Meta.Grind
@[inline] def isSameExpr (a b : Expr) : Bool :=
-- It is safe to use pointer equality because we hashcons all expressions
-- inserted into the E-graph
unsafe ptrEq a b
/-- We use this auxiliary constant to mark delayed congruence proofs. -/
def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]")
@@ -221,6 +224,20 @@ structure NewEq where
proof : Expr
isHEq : Bool
/--
Key for the `ENodeMap` and `ParentMap` map.
We use pointer addresses and rely on the fact all internalized expressions
have been hash-consed, i.e., we have applied `shareCommon`.
-/
private structure ENodeKey where
expr : Expr
instance : Hashable ENodeKey where
hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
instance : BEq ENodeKey where
beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
abbrev ENodeMap := PHashMap ENodeKey ENode
/--
@@ -351,8 +368,6 @@ structure Goal where
gmt : Nat := 0
/-- Next unique index for creating ENodes -/
nextIdx : Nat := 0
/-- State of arithmetic procedures -/
arith : Arith.State := {}
/-- Active theorems that we have performed ematching at least once. -/
thms : PArray EMatchTheorem := {}
/-- Active theorems that we have not performed any round of ematching yet. -/
@@ -380,8 +395,6 @@ structure Goal where
resolvedSplits : PHashSet ENodeKey := {}
/-- Next local E-match theorem idx. -/
nextThmIdx : Nat := 0
/-- Asserted facts -/
facts : PArray Expr := {}
deriving Inhabited
def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -450,25 +463,14 @@ def checkMaxEmatchExceeded : GoalM Bool := do
Returns `some n` if `e` has already been "internalized" into the
Otherwise, returns `none`s.
-/
def Goal.getENode? (goal : Goal) (e : Expr) : Option ENode :=
goal.enodes.find? { expr := e }
@[inline, inherit_doc Goal.getENode?]
def getENode? (e : Expr) : GoalM (Option ENode) :=
return ( get).getENode? e
def throwNonInternalizedExpr (e : Expr) : CoreM α :=
throwError "internal `grind` error, term has not been internalized{indentExpr e}"
return ( get).enodes.find? { expr := e }
/-- Returns node associated with `e`. It assumes `e` has already been internalized. -/
def Goal.getENode (goal : Goal) (e : Expr) : CoreM ENode := do
let some n := goal.enodes.find? { expr := e }
| throwNonInternalizedExpr e
return n
@[inline, inherit_doc Goal.getENode]
def getENode (e : Expr) : GoalM ENode := do
( get).getENode e
let some n := ( get).enodes.find? { expr := e }
| throwError "internal `grind` error, term has not been internalized{indentExpr e}"
return n
/-- Returns the generation of the given term. Is assumes it has been internalized -/
def getGeneration (e : Expr) : GoalM Nat :=
@@ -499,53 +501,30 @@ def isRoot (e : Expr) : GoalM Bool := do
return isSameExpr n.root e
/-- Returns the root element in the equivalence class of `e` IF `e` has been internalized. -/
def Goal.getRoot? (goal : Goal) (e : Expr) : Option Expr := Id.run do
let some n goal.getENode? e | return none
def getRoot? (e : Expr) : GoalM (Option Expr) := do
let some n getENode? e | return none
return some n.root
@[inline, inherit_doc Goal.getRoot?]
def getRoot? (e : Expr) : GoalM (Option Expr) := do
return ( get).getRoot? e
/-- Returns the root element in the equivalence class of `e`. -/
def Goal.getRoot (goal : Goal) (e : Expr) : CoreM Expr :=
return ( goal.getENode e).root
@[inline, inherit_doc Goal.getRoot]
def getRoot (e : Expr) : GoalM Expr := do
( get).getRoot e
def getRoot (e : Expr) : GoalM Expr :=
return ( getENode e).root
/-- Returns the root enode in the equivalence class of `e`. -/
def getRootENode (e : Expr) : GoalM ENode := do
getENode ( getRoot e)
/--
Returns the next element in the equivalence class of `e`
if `e` has been internalized in the given goal.
-/
def Goal.getNext? (goal : Goal) (e : Expr) : Option Expr := Id.run do
let some n goal.getENode? e | return none
return some n.next
/-- Returns the next element in the equivalence class of `e`. -/
def Goal.getNext (goal : Goal) (e : Expr) : CoreM Expr :=
return ( goal.getENode e).next
@[inline, inherit_doc Goal.getRoot]
def getNext (e : Expr) : GoalM Expr := do
( get).getNext e
def getNext (e : Expr) : GoalM Expr :=
return ( getENode e).next
/-- Returns `true` if `e` has already been internalized. -/
def alreadyInternalized (e : Expr) : GoalM Bool :=
return ( get).enodes.contains { expr := e }
def Goal.getTarget? (goal : Goal) (e : Expr) : Option Expr := Id.run do
let some n goal.getENode? e | return none
def getTarget? (e : Expr) : GoalM (Option Expr) := do
let some n getENode? e | return none
return n.target?
@[inline] def getTarget? (e : Expr) : GoalM (Option Expr) := do
return ( get).getTarget? e
/--
If `isHEq` is `false`, it pushes `lhs = rhs` with `proof` to `newEqs`.
Otherwise, it pushes `HEq lhs rhs`.
@@ -717,23 +696,11 @@ def closeGoal (falseProof : Expr) : GoalM Unit := do
else
mvarId.assign ( mkFalseElim target falseProof)
def Goal.getENodes (goal : Goal) : Array ENode :=
-- We must sort because we are using pointer addresses as keys in `enodes`
let nodes := goal.enodes.toArray.map (·.2)
nodes.qsort fun a b => a.idx < b.idx
/-- Returns all enodes in the goal -/
def getENodes : GoalM (Array ENode) := do
return ( get).getENodes
/-- Executes `f` to each term in the equivalence class containing `e` -/
@[inline] def traverseEqc (e : Expr) (f : ENode GoalM Unit) : GoalM Unit := do
let mut curr := e
repeat
let n getENode curr
f n
if isSameExpr n.next e then return ()
curr := n.next
-- We must sort because we are using pointer addresses as keys in `enodes`
let nodes := ( get).enodes.toArray.map (·.2)
return nodes.qsort fun a b => a.idx < b.idx
def forEachENode (f : ENode GoalM Unit) : GoalM Unit := do
let nodes getENodes
@@ -747,7 +714,7 @@ def filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode) := do
ref.modify (·.push n)
ref.get
def forEachEqcRoot (f : ENode GoalM Unit) : GoalM Unit := do
def forEachEqc (f : ENode GoalM Unit) : GoalM Unit := do
let nodes getENodes
for n in nodes do
if isSameExpr n.self n.root then
@@ -782,34 +749,26 @@ def applyFallback : GoalM Unit := do
fallback
/-- Returns expressions in the given expression equivalence class. -/
partial def Goal.getEqc (goal : Goal) (e : Expr) : List Expr :=
partial def getEqc (e : Expr) : GoalM (List Expr) :=
go e e []
where
go (first : Expr) (e : Expr) (acc : List Expr) : List Expr := Id.run do
let some next goal.getNext? e | acc
go (first : Expr) (e : Expr) (acc : List Expr) : GoalM (List Expr) := do
let next getNext e
let acc := e :: acc
if isSameExpr first next then
return acc
else
go first next acc
@[inline, inherit_doc Goal.getEqc]
partial def getEqc (e : Expr) : GoalM (List Expr) :=
return ( get).getEqc e
/-- Returns all equivalence classes in the current goal. -/
partial def Goal.getEqcs (goal : Goal) : List (List Expr) := Id.run do
let mut r : List (List Expr) := []
let nodes goal.getENodes
partial def getEqcs : GoalM (List (List Expr)) := do
let mut r := []
let nodes getENodes
for node in nodes do
if isSameExpr node.root node.self then
r := goal.getEqc node.self :: r
r := ( getEqc node.self) :: r
return r
@[inline, inherit_doc Goal.getEqcs]
def getEqcs : GoalM (List (List Expr)) :=
return ( get).getEqcs
/-- Returns `true` if `e` is a case-split that does not need to be performed anymore. -/
def isResolvedCaseSplit (e : Expr) : GoalM Bool :=
return ( get).resolvedSplits.contains { expr := e }

View File

@@ -1583,8 +1583,8 @@ namespace TokenMap
def insert (map : TokenMap α) (k : Name) (v : α) : TokenMap α :=
match map.find? k with
| none => RBMap.insert map k [v]
| some vs => RBMap.insert map k (v::vs)
| none => .insert map k [v]
| some vs => .insert map k (v::vs)
instance : Inhabited (TokenMap α) where
default := RBMap.empty

View File

@@ -103,8 +103,11 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
name := c', levelParams := []
type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe
}
addAndCompile decl
modifyEnv (ctx.combinatorAttr.setDeclFor · c c')
let env getEnv
let env match env.addAndCompile {} decl with
| Except.ok env => pure env
| Except.error kex => do throwError ( (kex.toMessageData {}).toString)
setEnv <| ctx.combinatorAttr.setDeclFor env c c'
if cinfo.type.isConst then
if let some kind parserNodeKind? cinfo.value! then
-- If the parser is parameter-less and produces a node of kind `kind`,

View File

@@ -97,7 +97,7 @@ abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m
/-- Workers execute request handlers in this monad. -/
abbrev RequestM := ReaderT RequestContext <| EIO RequestError
abbrev RequestTask.pure (a : α) : RequestTask α := Task.pure (.ok a)
abbrev RequestTask.pure (a : α) : RequestTask α := .pure (.ok a)
instance : MonadLift IO RequestM where
monadLift x := do

View File

@@ -104,26 +104,17 @@ def initSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO Unit :
private def initSearchPathInternal : IO Unit := do
initSearchPath ( getBuildDir)
/-- Find the compiled `.olean` of a module in the `LEAN_PATH` search path. -/
partial def findOLean (mod : Name) : IO FilePath := do
let sp searchPathRef.get
if let some fname sp.findWithExt "olean" mod then
return fname
else
let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
throw <| IO.userError s!"unknown module prefix '{pkg}'\n\n\
No directory '{pkg}' or file '{pkg}.olean' in the search path entries:\n\
{"\n".intercalate <| sp.map (·.toString)}"
let mut msg := s!"unknown module prefix '{pkg}'
/-- Find the `.lean` source of a module in a `LEAN_SRC_PATH` search path. -/
partial def findLean (sp : SearchPath) (mod : Name) : IO FilePath := do
if let some fname sp.findWithExt "lean" mod then
return fname
else
let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
throw <| IO.userError s!"unknown module prefix '{pkg}'\n\n\
No directory '{pkg}' or file '{pkg}.lean' in the search path entries:\n\
{"\n".intercalate <| sp.map (·.toString)}"
No directory '{pkg}' or file '{pkg}.olean' in the search path entries:
{"\n".intercalate <| sp.map (·.toString)}"
throw <| IO.userError msg
/-- Infer module name of source file name. -/
@[export lean_module_name_of_file]

View File

@@ -207,9 +207,7 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
| .widget wi alt =>
return .tag (.widget wi ( fmtToTT alt col)) default
| .trace cls msg collapsed children => do
-- absolute column = request-level indentation (e.g. from nested lazy trace request) +
-- offset inside `fmt`
let col := indent + col
let col := col + tt.stripTags.length - 2
let children
match children with
| .lazy children => pure <| .lazy {indent := col+2, children := children.map .mk}

View File

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Std.Internal.Async
import Std.Internal.Parsec
import Std.Internal.UV
/-!
This directory is used for components of the standard library that are either considered

View File

@@ -1,8 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Std.Internal.Async.Basic
import Std.Internal.Async.Timer

View File

@@ -1,115 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Init.Core
import Init.System.IO
import Init.System.Promise
namespace Std
namespace Internal
namespace IO
namespace Async
/--
A `Task` that may resolve to a value or an `IO.Error`.
-/
def AsyncTask (α : Type u) : Type u := Task (Except IO.Error α)
namespace AsyncTask
/--
Construct an `AsyncTask` that is already resolved with value `x`.
-/
@[inline]
protected def pure (x : α) : AsyncTask α := Task.pure <| .ok x
instance : Pure AsyncTask where
pure := AsyncTask.pure
/--
Create a new `AsyncTask` that will run after `x` has finished.
If `x`:
- errors, return an `AsyncTask` that resolves to the error.
- succeeds, run `f` on the result of `x` and return the `AsyncTask` produced by `f`.
-/
@[inline]
protected def bind (x : AsyncTask α) (f : α AsyncTask β) : AsyncTask β :=
Task.bind x fun r =>
match r with
| .ok a => f a
| .error e => Task.pure <| .error e
/--
Create a new `AsyncTask` that will run after `x` has finished.
If `x`:
- errors, return an `AsyncTask` that reolves to the error.
- succeeds, return an `AsyncTask` that resolves to `f x`.
-/
@[inline]
def map (f : α β) (x : AsyncTask α) : AsyncTask β :=
Task.map (x := x) fun r =>
match r with
| .ok a => .ok (f a)
| .error e => .error e
/--
Similar to `bind`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
`AsyncTask` resolves to that error.
-/
@[inline]
def bindIO (x : AsyncTask α) (f : α IO (AsyncTask β)) : BaseIO (AsyncTask β) :=
IO.bindTask x fun r =>
match r with
| .ok a => f a
| .error e => .error e
/--
Similar to `bind`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
`AsyncTask` resolves to that error.
-/
@[inline]
def mapIO (f : α IO β) (x : AsyncTask α) : BaseIO (AsyncTask β) :=
IO.mapTask (t := x) fun r =>
match r with
| .ok a => f a
| .error e => .error e
/--
Block until the `AsyncTask` in `x` finishes.
-/
def block (x : AsyncTask α) : IO α := do
let res := x.get
match res with
| .ok a => return a
| .error e => .error e
/--
Create an `AsyncTask` that resolves to the value of `x`.
-/
@[inline]
def ofPromise (x : IO.Promise (Except IO.Error α)) : AsyncTask α :=
x.result
/--
Create an `AsyncTask` that resolves to the value of `x`.
-/
@[inline]
def ofPurePromise (x : IO.Promise α) : AsyncTask α :=
x.result.map pure
/--
Obtain the `IO.TaskState` of `x`.
-/
@[inline]
def getState (x : AsyncTask α) : BaseIO IO.TaskState :=
IO.getTaskState x
end AsyncTask
end Async
end IO
end Internal
end Std

View File

@@ -1,139 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
prelude
import Std.Time
import Std.Internal.UV
import Std.Internal.Async.Basic
namespace Std
namespace Internal
namespace IO
namespace Async
/--
`Sleep` can be used to sleep for some duration once.
The underlying timer has millisecond resolution.
-/
structure Sleep where
private ofNative ::
native : Internal.UV.Timer
namespace Sleep
/--
Set up a `Sleep` that waits for `duration` milliseconds.
This function only initializes but does not yet start the timer.
-/
@[inline]
def mk (duration : Std.Time.Millisecond.Offset) : IO Sleep := do
let native Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 false
return ofNative native
/--
If:
- `s` is not yet running start it and return an `AsyncTask` that will resolve once the previously
configured `duration` has run out.
- `s` is already or not anymore running return the same `AsyncTask` as the first call to `wait`.
-/
@[inline]
def wait (s : Sleep) : IO (AsyncTask Unit) := do
let promise s.native.next
return .ofPurePromise promise
/--
If:
- `s` is still running the timer restarts counting from now and finishes after `duration`
milliseconds.
- `s` is not yet or not anymore running this is a no-op.
-/
@[inline]
def reset (s : Sleep) : IO Unit :=
s.native.reset
/--
If:
- `s` is still running this stops `s` without resolving any remaining `AsyncTask`s that were created
through `wait`. Note that if another `AsyncTask` is binding on any of these it is going hang
forever without further intervention.
- `s` is not yet or not anymore running this is a no-op.
-/
@[inline]
def stop (s : Sleep) : IO Unit :=
s.native.stop
end Sleep
/--
Return an `AsyncTask` that resolves after `duration`.
-/
def sleep (duration : Std.Time.Millisecond.Offset) : IO (AsyncTask Unit) := do
let sleeper Sleep.mk duration
sleeper.wait
/--
`Interval` can be used to repeatedly wait for some duration like a clock.
The underlying timer has millisecond resolution.
-/
structure Interval where
private ofNative ::
native : Internal.UV.Timer
namespace Interval
/--
Setup up an `Interval` that waits for `duration` milliseconds.
This function only initializes but does not yet start the timer.
-/
@[inline]
def mk (duration : Std.Time.Millisecond.Offset) (_ : 0 < duration := by decide) : IO Interval := do
let native Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 true
return ofNative native
/--
If:
- `i` is not yet running start it and return an `AsyncTask` that resolves right away as the 0th
multiple of `duration` has elapsed.
- `i` is already running and:
- the tick from the last call of `i` has not yet finished return the same `AsyncTask` as the last
call
- the tick frrom the last call of `i` has finished return a new `AsyncTask` that waits for the
closest next tick from the time of calling this function.
- `i` is not running aymore this is a no-op.
-/
@[inline]
def tick (i : Interval) : IO (AsyncTask Unit) := do
let promise i.native.next
return .ofPurePromise promise
/--
If:
- `Interval.tick` was called on `i` before the timer restarts counting from now and the next tick
happens in `duration`.
- `i` is not yet or not anymore running this is a no-op.
-/
@[inline]
def reset (i : Interval) : IO Unit :=
i.native.reset
/--
If:
- `i` is still running this stops `i` without resolving any remaing `AsyncTask` that were created
through `tick`. Note that if another `AsyncTask` is binding on any of these it is going hang
forever without further intervention.
- `i` is not yet or not anymore running this is a no-op.
-/
@[inline]
def stop (i : Interval) : IO Unit :=
i.native.stop
end Interval
end Async
end IO
end Internal
end Std

View File

@@ -1,119 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sofia Rodrigues
-/
prelude
import Init.System.IO
import Init.System.Promise
namespace Std
namespace Internal
namespace UV
namespace Loop
/--
Options for configuring the event loop behavior.
-/
structure Loop.Options where
/--
Accumulate the amount of idle time the event loop spends in the event provider.
-/
accumulateIdleTime : Bool := False
/--
Block a SIGPROF signal when polling for new events. It's commonly used for unnecessary wakeups
when using a sampling profiler.
-/
blockSigProfSignal : Bool := False
/--
Configures the event loop with the specified options.
-/
@[extern "lean_uv_event_loop_configure"]
opaque configure (options : Loop.Options) : BaseIO Unit
/--
Checks if the event loop is still active and processing events.
-/
@[extern "lean_uv_event_loop_alive"]
opaque alive : BaseIO Bool
end Loop
private opaque TimerImpl : NonemptyType.{0}
/--
`Timer`s are used to generate `IO.Promise`s that resolve after some time.
A `Timer` can be in one of 3 states:
- Right after construction it's initial.
- While it is ticking it's running.
- If it has stopped for some reason it's finished.
This together with whether it was set up as `repeating` with `Timer.new` determines the behavior
of all functions on `Timer`s.
-/
def Timer : Type := TimerImpl.type
instance : Nonempty Timer := TimerImpl.property
namespace Timer
/--
This creates a `Timer` in the initial state and doesn't run it yet.
- If `repeating` is `false` this constructs a timer that resolves once after `durationMs`
milliseconds, counting from when it's run.
- If `repeating` is `true` this constructs a timer that resolves after multiples of `durationMs`
milliseconds, counting from when it's run. Note that this includes the 0th multiple right after
starting the timer. Furthermore a repeating timer will only be freed after `Timer.stop` is called.
-/
@[extern "lean_uv_timer_mk"]
opaque mk (timeout : UInt64) (repeating : Bool) : IO Timer
/--
This function has different behavior depending on the state and configuration of the `Timer`:
- if `repeating` is `false` and:
- it is initial, run it and return a new `IO.Promise` that is set to resolve once `durationMs`
milliseconds have elapsed. After this `IO.Promise` is resolved the `Timer` is finished.
- it is running or finished, return the same `IO.Promise` that the first call to `next` returned.
- if `repeating` is `true` and:
- it is initial, run it and return a new `IO.Promise` that resolves right away
(as it is the 0th multiple of `durationMs`).
- it is running, check whether the last returned `IO.Promise` is already resolved:
- If it is, return a new `IO.Promise` that resolves upon finishing the next cycle
- If it is not, return the last `IO.Promise`
This ensures that the returned `IO.Promise` resolves at the next repetition of the timer.
- if it is finished, return the last `IO.Promise` created by `next`. Notably this could be one
that never resolves if the timer was stopped before fulfilling the last one.
-/
@[extern "lean_uv_timer_next"]
opaque next (timer : @& Timer) : IO (IO.Promise Unit)
/--
This function has different behavior depending on the state and configuration of the `Timer`:
- If it is initial or finished this is a no-op.
- If it is running and `repeating` is `false` this will delay the resolution of the timer until
`durationMs` milliseconds after the call of this function.
- Delay the resolution of the next tick of the timer until `durationMs` milliseconds after the
call of this function, then continue normal ticking behavior from there.
-/
@[extern "lean_uv_timer_reset"]
opaque reset (timer : @& Timer) : IO Unit
/--
This function has different behavior depending on the state of the `Timer`:
- If it is initial or finished this is a no-op.
- If it is running the execution of the timer is stopped and it is put into the finished state.
Note that if the last `IO.Promise` generated by `next` is unresolved and being waited
on this creates a memory leak and the waiting task is not going to be awoken anymore.
-/
@[extern "lean_uv_timer_stop"]
opaque stop (timer : @& Timer) : IO Unit
end Timer
end UV
end Internal
end Std

View File

@@ -73,7 +73,7 @@ Creates an `Offset` from a natural number.
-/
@[inline]
def ofNat (data : Nat) : Offset :=
Int.ofNat data
.ofNat data
/--
Creates an `Offset` from an integer.

View File

@@ -56,7 +56,7 @@ Creates an `Offset` from a natural number.
-/
@[inline]
def ofNat (data : Nat) : Offset :=
Int.ofNat data
.ofNat data
/--
Creates an `Offset` from an integer.

View File

@@ -29,6 +29,7 @@ structure PlainDateTime where
The `Time` component of a `PlainTime`
-/
time : PlainTime
deriving Inhabited, BEq, Repr
namespace PlainDateTime
@@ -122,7 +123,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do
return {
date := PlainDate.ofYearMonthDayClip year hmon (Day.Ordinal.ofFin (Fin.succ mday))
time := PlainTime.ofHourMinuteSecondsNano (hour.expandTop (by decide)) minute (second.expandTop (by decide)) nano
time := PlainTime.ofHourMinuteSecondsNano (leap := false) (hour.expandTop (by decide)) minute second nano
}
/--
@@ -198,7 +199,7 @@ Creates a new `PlainDateTime` by adjusting the `hour` component of its `time` to
-/
@[inline]
def withHours (dt : PlainDateTime) (hour : Hour.Ordinal) : PlainDateTime :=
{ dt with time := { dt.time with hour } }
{ dt with time := { dt.time with hour := hour } }
/--
Creates a new `PlainDateTime` by adjusting the `minute` component of its `time` to the given value.
@@ -211,7 +212,7 @@ def withMinutes (dt : PlainDateTime) (minute : Minute.Ordinal) : PlainDateTime :
Creates a new `PlainDateTime` by adjusting the `second` component of its `time` to the given value.
-/
@[inline]
def withSeconds (dt : PlainDateTime) (second : Second.Ordinal true) : PlainDateTime :=
def withSeconds (dt : PlainDateTime) (second : Sigma Second.Ordinal) : PlainDateTime :=
{ dt with time := { dt.time with second := second } }
/--
@@ -456,8 +457,8 @@ def millisecond (dt : PlainDateTime) : Millisecond.Ordinal :=
Getter for the `Second` inside of a `PlainDateTime`.
-/
@[inline]
def second (dt : PlainDateTime) : Second.Ordinal true :=
dt.time.second
def second (dt : PlainDateTime) : Second.Ordinal dt.time.second.fst :=
dt.time.second.snd
/--
Getter for the `Nanosecond.Ordinal` inside of a `PlainDateTime`.

View File

@@ -37,10 +37,10 @@ instance : OfNat Timestamp n where
ofNat := OfNat.ofNat n
instance : ToString Timestamp where
toString s := toString s.val.toSeconds
toString s := toString s.val.toMilliseconds
instance : Repr Timestamp where
reprPrec s := Repr.addAppParen ("Timestamp.ofNanosecondsSinceUnixEpoch " ++ repr s.val.toNanoseconds)
reprPrec s := reprPrec (toString s)
namespace Timestamp

View File

@@ -280,7 +280,7 @@ def format (time : PlainTime) (format : String) : String :=
Parses a time string in the 24-hour format (`HH:mm:ss`) and returns a `PlainTime`.
-/
def fromTime24Hour (input : String) : Except String PlainTime :=
Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s)) input
Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s.snd)) input
/--
Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`).
@@ -292,8 +292,8 @@ def toTime24Hour (input : PlainTime) : String :=
Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`.
-/
def fromLeanTime24Hour (input : String) : Except String PlainTime :=
Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| PlainTime.ofHourMinuteSecondsNano h m s n) input
<|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some <| PlainTime.ofHourMinuteSecondsNano h m s 0) input
Formats.leanTime24Hour.parseBuilder (fun h m s n => some (PlainTime.ofHourMinuteSecondsNano h m s.snd n)) input
<|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSecondsNano h m s.snd 0)) input
/--
Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`).
@@ -307,7 +307,7 @@ Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainT
def fromTime12Hour (input : String) : Except String PlainTime := do
let builder h m s a : Option PlainTime := do
let value Internal.Bounded.ofInt? h.val
some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s
some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s.snd
Formats.time12Hour.parseBuilder builder input

View File

@@ -741,7 +741,7 @@ private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bo
let data := s!"{sign}{pad time.hour.val}"
let data := if withMinutes then s!"{data}{if colon then ":" else ""}{pad time.minute.val}" else data
let data := if withSeconds ∧ time.second.val ≠ 0 then s!"{data}{if colon then ":" else ""}{pad time.second.val}" else data
let data := if withSeconds ∧ time.second.snd.val ≠ 0 then s!"{data}{if colon then ":" else ""}{pad time.second.snd.val}" else data
data
@@ -764,7 +764,7 @@ private def TypeFormat : Modifier → Type
| .k _ => Bounded.LE 1 24
| .H _ => Hour.Ordinal
| .m _ => Minute.Ordinal
| .s _ => Second.Ordinal true
| .s _ => Sigma Second.Ordinal
| .S _ => Nanosecond.Ordinal
| .A _ => Millisecond.Offset
| .n _ => Nanosecond.Ordinal
@@ -835,10 +835,10 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin
| .narrow => formatMarkerNarrow data
| .h format => pad format.padding (data.val % 12)
| .K format => pad format.padding (data.val % 12)
| .k format => pad format.padding data.val
| .H format => pad format.padding data.val
| .m format => pad format.padding data.val
| .s format => pad format.padding data.val
| .k format => pad format.padding (data.val)
| .H format => pad format.padding (data.val)
| .m format => pad format.padding (data.val)
| .s format => pad format.padding (data.snd.val)
| .S format =>
match format with
| .nano => pad 9 data.val
@@ -1167,7 +1167,7 @@ private def parseWith : (mod : Modifier) → Parser (TypeFormat mod)
| .k format => parseNatToBounded (parseAtLeastNum format.padding)
| .H format => parseNatToBounded (parseAtLeastNum format.padding)
| .m format => parseNatToBounded (parseAtLeastNum format.padding)
| .s format => parseNatToBounded (parseAtLeastNum format.padding)
| .s format => Sigma.mk true <$> (parseNatToBounded (parseAtLeastNum format.padding))
| .S format =>
match format with
| .nano => parseNatToBounded (parseAtLeastNum 9)
@@ -1249,7 +1249,7 @@ private structure DateBuilder where
k : Option (Bounded.LE 1 24) := none
H : Option Hour.Ordinal := none
m : Option Minute.Ordinal := none
s : Option (Second.Ordinal true) := none
s : Option (Sigma Second.Ordinal) := none
S : Option Nanosecond.Ordinal := none
A : Option Millisecond.Offset := none
n : Option Nanosecond.Ordinal := none
@@ -1335,10 +1335,10 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
|>.getD ⟨0, by decide⟩
let minute := builder.m |>.getD 0
let second := builder.s |>.getD 0
let second := builder.s |>.getD ⟨false, 0⟩
let nano := (builder.n <|> builder.S) |>.getD 0
let time
let time : PlainTime
:= PlainTime.ofNanoseconds <$> builder.N
<|> PlainTime.ofMilliseconds <$> builder.A
|>.getD (PlainTime.mk hour minute second nano)

View File

@@ -126,7 +126,7 @@ private def convertPlainDate (d : Std.Time.PlainDate) : MacroM (TSyntax `term) :
`(Std.Time.PlainDate.ofYearMonthDayClip $( syntaxInt d.year) $( syntaxBounded d.month.val) $( syntaxBounded d.day.val))
private def convertPlainTime (d : Std.Time.PlainTime) : MacroM (TSyntax `term) := do
`(Std.Time.PlainTime.mk $( syntaxBounded d.hour.val) $( syntaxBounded d.minute.val) $( syntaxBounded d.second.val) $( syntaxBounded d.nanosecond.val))
`(Std.Time.PlainTime.mk $( syntaxBounded d.hour.val) $( syntaxBounded d.minute.val) true, $( syntaxBounded d.second.snd.val) $( syntaxBounded d.nanosecond.val))
private def convertPlainDateTime (d : Std.Time.PlainDateTime) : MacroM (TSyntax `term) := do
`(Std.Time.PlainDateTime.mk $( convertPlainDate d.date) $( convertPlainTime d.time))

View File

@@ -30,7 +30,7 @@ structure PlainTime where
/--
`Second` component of the `PlainTime`
-/
second : Second.Ordinal true
second : Sigma Second.Ordinal
/--
`Nanoseconds` component of the `PlainTime`
@@ -39,11 +39,11 @@ structure PlainTime where
deriving Repr
instance : Inhabited PlainTime where
default := 0, 0, 0, 0, by decide
default := 0, 0, Sigma.mk false 0, 0, by decide
instance : BEq PlainTime where
beq x y := x.hour.val == y.hour.val && x.minute == y.minute
&& x.second.val == y.second.val && x.nanosecond == y.nanosecond
&& x.second.snd.val == y.second.snd.val && x.nanosecond == y.nanosecond
namespace PlainTime
@@ -51,20 +51,20 @@ namespace PlainTime
Creates a `PlainTime` value representing midnight (00:00:00.000000000).
-/
def midnight : PlainTime :=
0, 0, 0, 0
0, 0, true, 0, 0
/--
Creates a `PlainTime` value from the provided hours, minutes, seconds and nanoseconds components.
-/
@[inline]
def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) (nano : Nanosecond.Ordinal) : PlainTime :=
hour, minute, second, nano
def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) (nano : Nanosecond.Ordinal) : PlainTime :=
hour, minute, Sigma.mk leap second, nano
/--
Creates a `PlainTime` value from the provided hours, minutes, and seconds.
-/
@[inline]
def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) : PlainTime :=
def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) : PlainTime :=
ofHourMinuteSecondsNano hour minute second 0
/--
@@ -73,7 +73,7 @@ Converts a `PlainTime` value to the total number of milliseconds.
def toMilliseconds (time : PlainTime) : Millisecond.Offset :=
time.hour.toOffset.toMilliseconds +
time.minute.toOffset.toMilliseconds +
time.second.toOffset.toMilliseconds +
time.second.snd.toOffset.toMilliseconds +
time.nanosecond.toOffset.toMilliseconds
/--
@@ -82,7 +82,7 @@ Converts a `PlainTime` value to the total number of nanoseconds.
def toNanoseconds (time : PlainTime) : Nanosecond.Offset :=
time.hour.toOffset.toNanoseconds +
time.minute.toOffset.toNanoseconds +
time.second.toOffset.toNanoseconds +
time.second.snd.toOffset.toNanoseconds +
time.nanosecond.toOffset
/--
@@ -91,7 +91,7 @@ Converts a `PlainTime` value to the total number of seconds.
def toSeconds (time : PlainTime) : Second.Offset :=
time.hour.toOffset.toSeconds +
time.minute.toOffset.toSeconds +
time.second.toOffset
time.second.snd.toOffset
/--
Converts a `PlainTime` value to the total number of minutes.
@@ -99,7 +99,7 @@ Converts a `PlainTime` value to the total number of minutes.
def toMinutes (time : PlainTime) : Minute.Offset :=
time.hour.toOffset.toMinutes +
time.minute.toOffset +
time.second.toOffset.toMinutes
time.second.snd.toOffset.toMinutes
/--
Converts a `PlainTime` value to the total number of hours.
@@ -115,12 +115,9 @@ def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime :=
have remainingNanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide)
have hours := Bounded.LE.byEmod (totalSeconds.val / 3600) 24 (by decide)
have minutes := (Bounded.LE.byEmod totalSeconds.val 3600 (by decide)).ediv 60 (by decide)
have seconds := Bounded.LE.byEmod totalSeconds.val 60 (by decide)
have seconds := seconds.expandTop (by decide)
let nanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide)
PlainTime.mk hours minutes seconds nanos
PlainTime.mk hours minutes (Sigma.mk false seconds) nanos
/--
Creates a `PlainTime` value from a total number of millisecond.
@@ -225,7 +222,7 @@ def subMilliseconds (time : PlainTime) (millisToSub : Millisecond.Offset) : Plai
Creates a new `PlainTime` by adjusting the `second` component to the given value.
-/
@[inline]
def withSeconds (pt : PlainTime) (second : Second.Ordinal true) : PlainTime :=
def withSeconds (pt : PlainTime) (second : Sigma Second.Ordinal) : PlainTime :=
{ pt with second := second }
/--

View File

@@ -30,7 +30,7 @@ instance : LE (Ordinal leap) where
instance : LT (Ordinal leap) where
lt x y := LT.lt x.val y.val
instance : Repr (Ordinal leap) where
instance : Repr (Ordinal l) where
reprPrec r := reprPrec r.val
instance : OfNat (Ordinal leap) n := by
@@ -39,10 +39,10 @@ instance : OfNat (Ordinal leap) n := by
· exact inst
· exact inst.ofNat.expandTop (by decide)
instance {x y : Ordinal leap} : Decidable (x y) :=
instance {x y : Ordinal l} : Decidable (x y) :=
inferInstanceAs (Decidable (x.val y.val))
instance {x y : Ordinal leap} : Decidable (x < y) :=
instance {x y : Ordinal l} : Decidable (x < y) :=
inferInstanceAs (Decidable (x.val < y.val))
/--

View File

@@ -71,7 +71,12 @@ def idFromPath (path : System.FilePath) : Option String := do
Retrieves the timezone rules from the local timezone data file.
-/
def localRules (path : System.FilePath) : IO ZoneRules := do
let localTimePath IO.FS.realPath path
let localTimePath
try
IO.Process.run { cmd := "readlink", args := #["-f", path.toString] }
catch _ =>
throw <| IO.userError "cannot find the local timezone database"
if let some id := idFromPath localTimePath
then parseTZIfFromDisk path id
else throw (IO.userError "cannot read the id of the path.")

View File

@@ -305,7 +305,7 @@ def withMinutes (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz :=
Creates a new `DateTime tz` by adjusting the `second` component.
-/
@[inline]
def withSeconds (dt : DateTime tz) (second : Second.Ordinal true) : DateTime tz :=
def withSeconds (dt : DateTime tz) (second : Sigma Second.Ordinal) : DateTime tz :=
ofPlainDateTime (dt.date.get.withSeconds second) tz
/--
@@ -368,7 +368,7 @@ def minute (dt : DateTime tz) : Minute.Ordinal :=
Getter for the `Second` inside of a `DateTime`
-/
@[inline]
def second (dt : DateTime tz) : Second.Ordinal true :=
def second (dt : DateTime tz) : Second.Ordinal dt.date.get.time.second.fst :=
dt.date.get.second
/--

View File

@@ -179,8 +179,8 @@ def minute (zdt : ZonedDateTime) : Minute.Ordinal :=
Getter for the `Second` inside of a `ZonedDateTime`
-/
@[inline]
def second (zdt : ZonedDateTime) : Second.Ordinal true :=
zdt.date.get.time.second
def second (zdt : ZonedDateTime) : Second.Ordinal zdt.date.get.time.second.fst :=
zdt.date.get.time.second.snd
/--
Getter for the `Millisecond` inside of a `ZonedDateTime`.
@@ -491,7 +491,7 @@ def withMinutes (dt : ZonedDateTime) (minute : Minute.Ordinal) : ZonedDateTime :
Creates a new `ZonedDateTime` by adjusting the `second` component.
-/
@[inline]
def withSeconds (dt : ZonedDateTime) (second : Second.Ordinal true) : ZonedDateTime :=
def withSeconds (dt : ZonedDateTime) (second : Sigma Second.Ordinal) : ZonedDateTime :=
let date := dt.date.get
ZonedDateTime.ofPlainDateTime (date.withSeconds second) dt.rules

View File

@@ -88,17 +88,6 @@ def compileStaticLib
args := #["rcs", libFile.toString] ++ oFiles.map toString
}
private def getMacOSXDeploymentEnv : BaseIO (Array (String × Option String)) := do
-- It is difficult to identify the correct minor version here, leading to linking warnings like:
-- `ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0`
-- In order to suppress these we set the MACOSX_DEPLOYMENT_TARGET variable into the far future.
if System.Platform.isOSX then
match ( IO.getEnv "MACOSX_DEPLOYMENT_TARGET") with
| some _ => return #[]
| none => return #[("MACOSX_DEPLOYMENT_TARGET", some "99.0")]
else
return #[]
def compileSharedLib
(libFile : FilePath) (linkArgs : Array String)
(linker : FilePath := "cc")
@@ -107,7 +96,6 @@ def compileSharedLib
proc {
cmd := linker.toString
args := #["-shared", "-o", libFile.toString] ++ linkArgs
env := getMacOSXDeploymentEnv
}
def compileExe
@@ -118,7 +106,16 @@ def compileExe
proc {
cmd := linker.toString
args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
env := getMacOSXDeploymentEnv
env := do
-- It is difficult to identify the correct minor version here, leading to linking warnings like:
-- `ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0`
-- In order to suppress these we set the MACOSX_DEPLOYMENT_TARGET variable into the far future.
if System.Platform.isOSX then
match ( IO.getEnv "MACOSX_DEPLOYMENT_TARGET") with
| some _ => pure #[]
| none => pure #[("MACOSX_DEPLOYMENT_TARGET", some "99.0")]
else
pure #[]
}
/-- Download a file using `curl`, clobbering any existing file. -/

View File

@@ -265,7 +265,7 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
/-- Merges this job with another, discarding its output and trace. -/
def add (self : Job α) (other : Job β) : Job α :=
self.zipResultWith (other := other) fun
| .ok a sa, .ok _ sb => .ok a {sa.merge sb with trace := sa.trace}
| .ok a sa, .ok _ sb => .ok a (sa.merge sb)
| ra, rb => .error 0 {ra.state.merge rb.state with trace := ra.state.trace}
/-- Merges this job with another, discarding both outputs. -/

View File

@@ -2,8 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp
uv/timer.cpp)
process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp)
add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
set_target_properties(leanrt_initial-exec PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})

View File

@@ -13,7 +13,6 @@ Author: Leonardo de Moura
#include "runtime/process.h"
#include "runtime/mutex.h"
#include "runtime/init_module.h"
#include "runtime/libuv.h"
namespace lean {
extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
@@ -25,7 +24,6 @@ extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
initialize_mutex();
initialize_process();
initialize_stack_overflow();
initialize_libuv();
}
void initialize_runtime_module() {
lean_initialize_runtime_module();

View File

@@ -2,36 +2,21 @@
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Markus Himmel, Sofia Rodrigues
*/
#include <pthread.h>
Author: Markus Himmel
*/
#include "runtime/libuv.h"
#include "runtime/object.h"
namespace lean {
#ifndef LEAN_EMSCRIPTEN
#include <uv.h>
extern "C" void initialize_libuv() {
initialize_libuv_timer();
initialize_libuv_loop();
lthread([]() { event_loop_run_loop(&global_ev); });
}
/* Lean.libUVVersionFn : Unit → Nat */
extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
return lean_unsigned_to_nat(uv_version());
}
#else
extern "C" void initialize_libuv() {}
extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg o) {
return lean_box(0);
}
#endif
}

View File

@@ -2,29 +2,9 @@
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Markus Himmel, Sofia Rodrigues
Author: Markus Himmel
*/
#pragma once
#include <lean/lean.h>
#include "runtime/uv/event_loop.h"
#include "runtime/uv/timer.h"
#include "runtime/alloc.h"
#include "runtime/io.h"
#include "runtime/utf8.h"
#include "runtime/object.h"
#include "runtime/thread.h"
#include "runtime/allocprof.h"
#include "runtime/object.h"
namespace lean {
#ifndef LEAN_EMSCRIPTEN
#include <uv.h>
#endif
extern "C" void initialize_libuv();
// =======================================
// General LibUV functions.
extern "C" LEAN_EXPORT lean_obj_res lean_libuv_version(lean_obj_arg);
}

View File

@@ -467,11 +467,6 @@ inline obj_res st_ref_set(b_obj_arg r, obj_arg v, obj_arg w) { return lean_st_re
inline obj_res st_ref_reset(b_obj_arg r, obj_arg w) { return lean_st_ref_reset(r, w); }
inline obj_res st_ref_swap(b_obj_arg r, obj_arg v, obj_arg w) { return lean_st_ref_swap(r, v, w); }
extern "C" LEAN_EXPORT obj_res lean_io_promise_new(obj_arg);
extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise, obj_arg);
extern "C" LEAN_EXPORT obj_res lean_io_promise_result(obj_arg promise);
// =======================================
// Module initialization/finalization
void initialize_object();

View File

@@ -1,143 +0,0 @@
/*
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sofia Rodrigues, Henrik Böving
*/
#include "runtime/uv/event_loop.h"
/*
This file builds a thread safe event loop on top of the thread unsafe libuv event loop.
We achieve this by always having a `uv_async_t` associated with the libuv event loop.
As `uv_async_t` are a thread safe primitive it is safe to send a notification to it from another
thread. Once this notification arrives the event loop suspends its own execution and unlocks a mutex
that protects it. This mutex can then be taken by another thread that wants to work with the event
loop. After that work is done it signals a condition variable that the event loop is waiting on
to continue its execution.
*/
namespace lean {
#ifndef LEAN_EMSCRIPTEN
using namespace std;
event_loop_t global_ev;
// Utility function for error checking. This function is only used inside the
// initializition of the event loop.
static void check_uv(int result, const char * msg) {
if (result != 0) {
std::string err_message = std::string(msg) + ": " + uv_strerror(result);
lean_internal_panic(err_message.c_str());
}
}
// The callback that stops the loop when it's called.
void async_callback(uv_async_t * handle) {
uv_stop(handle->loop);
}
// Interrupts the event loop and stops it so it can receive future requests.
void event_loop_interrupt(event_loop_t * event_loop) {
int result = uv_async_send(&event_loop->async);
(void)result;
lean_assert(result == 0);
}
// Initializes the event loop
void event_loop_init(event_loop_t * event_loop) {
event_loop->loop = uv_default_loop();
check_uv(uv_mutex_init_recursive(&event_loop->mutex), "Failed to initialize mutex");
check_uv(uv_cond_init(&event_loop->cond_var), "Failed to initialize condition variable");
check_uv(uv_async_init(event_loop->loop, &event_loop->async, NULL), "Failed to initialize async");
event_loop->n_waiters = 0;
}
// Locks the event loop for the side of the requesters.
void event_loop_lock(event_loop_t * event_loop) {
if (uv_mutex_trylock(&event_loop->mutex) != 0) {
event_loop->n_waiters++;
event_loop_interrupt(event_loop);
uv_mutex_lock(&event_loop->mutex);
event_loop->n_waiters--;
}
}
// Unlock event loop
void event_loop_unlock(event_loop_t * event_loop) {
if (event_loop->n_waiters == 0) {
uv_cond_signal(&event_loop->cond_var);
}
uv_mutex_unlock(&event_loop->mutex);
}
// Runs the loop and stops when it needs to register new requests.
void event_loop_run_loop(event_loop_t * event_loop) {
while (uv_loop_alive(event_loop->loop)) {
uv_mutex_lock(&event_loop->mutex);
while (event_loop->n_waiters != 0) {
uv_cond_wait(&event_loop->cond_var, &event_loop->mutex);
}
uv_run(event_loop->loop, UV_RUN_ONCE);
/*
* We leave `uv_run` only when `uv_stop` is called as there is always the `uv_async_t` so
* we can never run out of things to wait on. `uv_stop` is only called from `async_callback`
* when another thread wants to work with the event loop so we need to give up the mutex.
*/
uv_mutex_unlock(&event_loop->mutex);
}
}
/* Std.Internal.UV.Loop.configure (options : Loop.Options) : BaseIO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ ) {
bool accum = lean_ctor_get_uint8(options, 0);
bool block = lean_ctor_get_uint8(options, 1);
event_loop_lock(&global_ev);
if (accum && uv_loop_configure(global_ev.loop, UV_METRICS_IDLE_TIME) != 0) {
return io_result_mk_error("failed to configure global_ev.loop with UV_METRICS_IDLE_TIME");
}
#if!defined(WIN32) && !defined(_WIN32)
if (block && uv_loop_configure(global_ev.loop, UV_LOOP_BLOCK_SIGNAL, SIGPROF) != 0) {
return io_result_mk_error("failed to configure global_ev.loop with UV_LOOP_BLOCK_SIGNAL");
}
#endif
event_loop_unlock(&global_ev);
return lean_io_result_mk_ok(lean_box(0));
}
/* Std.Internal.UV.Loop.alive : BaseIO UInt64 */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ ) {
event_loop_lock(&global_ev);
int is_alive = uv_loop_alive(global_ev.loop);
event_loop_unlock(&global_ev);
return lean_io_result_mk_ok(lean_box(is_alive));
}
void initialize_libuv_loop() {
event_loop_init(&global_ev);
}
#else
/* Std.Internal.UV.Loop.configure (options : Loop.Options) : BaseIO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ ) {
return io_result_mk_error("lean_uv_event_loop_configure is not supported");
}
/* Std.Internal.UV.Loop.alive : BaseIO UInt64 */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ ) {
return io_result_mk_error("lean_uv_event_loop_alive is not supported");
}
#endif
}

View File

@@ -1,47 +0,0 @@
/*
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sofia Rodrigues
*/
#pragma once
#include <lean/lean.h>
#include "runtime/io.h"
#include "runtime/object.h"
namespace lean {
void initialize_libuv_loop();
#ifndef LEAN_EMSCRIPTEN
using namespace std;
#include <uv.h>
// Event loop structure for managing asynchronous events and synchronization across multiple threads.
typedef struct {
uv_loop_t * loop; // The libuv event loop.
uv_mutex_t mutex; // Mutex for protecting `loop`.
uv_cond_t cond_var; // Condition variable for signaling that `loop` is free.
uv_async_t async; // Async handle to interrupt `loop`.
_Atomic(int) n_waiters; // Atomic counter for managing waiters for `loop`.
} event_loop_t;
// The multithreaded event loop object for all tasks in the task manager.
extern event_loop_t global_ev;
// =======================================
// Event loop manipulation functions.
void event_loop_init(event_loop_t *event_loop);
void event_loop_cleanup(event_loop_t *event_loop);
void event_loop_lock(event_loop_t *event_loop);
void event_loop_unlock(event_loop_t *event_loop);
void event_loop_run_loop(event_loop_t *event_loop);
#endif
// =======================================
// Global event loop manipulation functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ );
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ );
}

View File

@@ -1,254 +0,0 @@
/*
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sofia Rodrigues, Henrik Böving
*/
#include "runtime/uv/timer.h"
namespace lean {
#ifndef LEAN_EMSCRIPTEN
using namespace std;
// The finalizer of the `Timer`.
void lean_uv_timer_finalizer(void* ptr) {
lean_uv_timer_object * timer = (lean_uv_timer_object*) ptr;
if (timer->m_promise != NULL) {
lean_dec(timer->m_promise);
}
event_loop_lock(&global_ev);
uv_close((uv_handle_t*)timer->m_uv_timer, [](uv_handle_t* handle) {
free(handle);
});
event_loop_unlock(&global_ev);
free(timer);
}
void initialize_libuv_timer() {
g_uv_timer_external_class = lean_register_external_class(lean_uv_timer_finalizer, [](void* obj, lean_object* f) {
if (((lean_uv_timer_object*)obj)->m_promise != NULL) {
lean_inc(f);
lean_apply_1(f, ((lean_uv_timer_object*)obj)->m_promise);
}
});
}
void handle_timer_event(uv_timer_t* handle) {
lean_object * obj = (lean_object*)handle->data;
lean_uv_timer_object * timer = lean_to_uv_timer(obj);
// handle_timer_event may only be called while the timer is running, this means the promise must
// not be NULL.
lean_assert(timer->m_state == TIMER_STATE_RUNNING);
lean_assert(timer->m_promise != NULL);
if (timer->m_repeating) {
if (lean_io_get_task_state_core(timer->m_promise) != 2) {
lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise, lean_io_mk_world());
lean_dec(res);
}
} else {
lean_assert(lean_io_get_task_state_core(timer->m_promise) != 2);
uv_timer_stop(timer->m_uv_timer);
timer->m_state = TIMER_STATE_FINISHED;
lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise, lean_io_mk_world());
lean_dec(res);
// The loop does not need to keep the timer alive anymore.
lean_dec(obj);
}
}
/* Std.Internal.UV.Timer.mk (timeout : UInt64) (repeating : Bool) : IO Timer */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */) {
lean_uv_timer_object * timer = (lean_uv_timer_object*)malloc(sizeof(lean_uv_timer_object));
timer->m_timeout = timeout;
timer->m_repeating = repeating;
timer->m_state = TIMER_STATE_INITIAL;
timer->m_promise = NULL;
uv_timer_t * uv_timer = (uv_timer_t*)malloc(sizeof(uv_timer_t));
event_loop_lock(&global_ev);
int result = uv_timer_init(global_ev.loop, uv_timer);
event_loop_unlock(&global_ev);
if (result != 0) {
free(uv_timer);
free(timer);
std::string err = std::string("failed to initialize timer: ") + uv_strerror(result);
return io_result_mk_error(err.c_str());
}
timer->m_uv_timer = uv_timer;
lean_object * obj = lean_uv_timer_new(timer);
lean_mark_mt(obj);
timer->m_uv_timer->data = obj;
return lean_io_result_mk_ok(obj);
}
/* Std.Internal.UV.Timer.next (timer : @& Timer) : IO (IO.Promise Unit) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg obj, obj_arg /* w */ ) {
lean_uv_timer_object * timer = lean_to_uv_timer(obj);
auto create_promise = []() {
lean_object * prom_res = lean_io_promise_new(lean_io_mk_world());
lean_object * promise = lean_ctor_get(prom_res, 0);
lean_inc(promise);
lean_dec(prom_res);
return promise;
};
auto setup_timer = [create_promise, obj, timer]() {
lean_assert(timer->m_promise == NULL);
timer->m_promise = create_promise();
timer->m_state = TIMER_STATE_RUNNING;
// The event loop must keep the timer alive for the duration of the run time.
lean_inc(obj);
event_loop_lock(&global_ev);
int result = uv_timer_start(
timer->m_uv_timer,
handle_timer_event,
timer->m_repeating ? 0 : timer->m_timeout,
timer->m_repeating ? timer->m_timeout : 0
);
event_loop_unlock(&global_ev);
if (result != 0) {
lean_dec(obj);
std::string err = std::string("failed to initialize timer: ") + uv_strerror(result);
return io_result_mk_error(err.c_str());
} else {
lean_inc(timer->m_promise);
return lean_io_result_mk_ok(timer->m_promise);
}
};
if (timer->m_repeating) {
switch (timer->m_state) {
case TIMER_STATE_INITIAL:
{
return setup_timer();
}
case TIMER_STATE_RUNNING:
{
lean_assert(timer->m_promise != NULL);
// 2 indicates finished
if (lean_io_get_task_state_core(timer->m_promise) == 2) {
lean_dec(timer->m_promise);
timer->m_promise = create_promise();
lean_inc(timer->m_promise);
return lean_io_result_mk_ok(timer->m_promise);
} else {
lean_inc(timer->m_promise);
return lean_io_result_mk_ok(timer->m_promise);
}
}
case TIMER_STATE_FINISHED:
{
lean_assert(timer->m_promise != NULL);
lean_inc(timer->m_promise);
return lean_io_result_mk_ok(timer->m_promise);
}
}
} else {
if (timer->m_state == TIMER_STATE_INITIAL) {
return setup_timer();
} else {
lean_assert(timer->m_promise != NULL);
lean_inc(timer->m_promise);
return lean_io_result_mk_ok(timer->m_promise);
}
}
}
/* Std.Internal.UV.Timer.reset (timer : @& Timer) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg obj, obj_arg /* w */ ) {
lean_uv_timer_object * timer = lean_to_uv_timer(obj);
if (timer->m_state == TIMER_STATE_RUNNING) {
lean_assert(timer->m_promise != NULL);
event_loop_lock(&global_ev);
uv_timer_stop(timer->m_uv_timer);
int result = uv_timer_start(
timer->m_uv_timer,
handle_timer_event,
timer->m_timeout,
timer->m_repeating ? timer->m_timeout : 0
);
event_loop_unlock(&global_ev);
if (result != 0) {
return io_result_mk_error("failed to restart uv_timer");
} else {
return lean_io_result_mk_ok(lean_box(0));
}
} else {
return lean_io_result_mk_ok(lean_box(0));
}
}
/* Std.Internal.UV.Timer.stop (timer : @& Timer) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg obj, obj_arg /* w */) {
lean_uv_timer_object * timer = lean_to_uv_timer(obj);
if (timer->m_state == TIMER_STATE_RUNNING) {
lean_assert(timer->m_promise != NULL);
event_loop_lock(&global_ev);
uv_timer_stop(timer->m_uv_timer);
event_loop_unlock(&global_ev);
timer->m_state = TIMER_STATE_FINISHED;
// The loop does not need to keep the timer alive anymore.
lean_dec(obj);
return lean_io_result_mk_ok(lean_box(0));
} else {
return lean_io_result_mk_ok(lean_box(0));
}
}
#else
void lean_uv_timer_finalizer(void* ptr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */) {
return io_result_mk_error("lean_uv_timer_mk is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer, obj_arg /* w */ ) {
return io_result_mk_error("lean_uv_timer_next is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer, obj_arg /* w */ ) {
return io_result_mk_error("lean_uv_timer_reset is not supported");
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer, obj_arg /* w */ ) {
return io_result_mk_error("lean_uv_timer_stop is not supported");
}
#endif
}

View File

@@ -1,54 +0,0 @@
/*
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sofia Rodrigues, Henrik Böving
*/
#pragma once
#include <lean/lean.h>
#include "runtime/uv/event_loop.h"
namespace lean {
static lean_external_class * g_uv_timer_external_class = NULL;
void initialize_libuv_timer();
#ifndef LEAN_EMSCRIPTEN
using namespace std;
#include <uv.h>
enum uv_timer_state {
TIMER_STATE_INITIAL,
TIMER_STATE_RUNNING,
TIMER_STATE_FINISHED,
};
// Structure for managing a single UV timer object, including promise handling, timeout, and
// repeating behavior.
typedef struct {
uv_timer_t * m_uv_timer; // LibUV timer handle.
lean_object * m_promise; // The associated promise for asynchronous results.
uint64_t m_timeout; // Timeout duration in milliseconds.
bool m_repeating; // Flag indicating if the timer is repeating.
uv_timer_state m_state; // The state of the timer. Beyond the API description on the Lean
// side this state has the invariant:
// `m_state != TIMER_STATE_INITIAL` -> `m_promise != NULL`
} lean_uv_timer_object;
// =======================================
// Timer object manipulation functions.
static inline lean_object* lean_uv_timer_new(lean_uv_timer_object * s) { return lean_alloc_external(g_uv_timer_external_class, s); }
static inline lean_uv_timer_object* lean_to_uv_timer(lean_object * o) { return (lean_uv_timer_object*)(lean_get_external_data(o)); }
#else
// =======================================
// Timer manipulation functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer, obj_arg /* w */);
#endif
}

View File

@@ -225,7 +225,6 @@ static void display_help(std::ostream & out) {
std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n";
std::cout << " -E --error=kind report Lean messages of kind as errors\n";
std::cout << " --deps just print dependencies of a Lean input\n";
std::cout << " --src-deps just print dependency sources of a Lean input\n";
std::cout << " --print-prefix print the installation prefix for Lean and exit\n";
std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n";
std::cout << " --profile display elaboration/type checking time for each definition/theorem\n";
@@ -236,7 +235,6 @@ static void display_help(std::ostream & out) {
std::cout << " -D name=value set a configuration option (see set_option command)\n";
}
static int only_src_deps = 0;
static int print_prefix = 0;
static int print_libdir = 0;
static int json_output = 0;
@@ -257,7 +255,6 @@ static struct option g_long_options[] = {
{"stats", no_argument, 0, 'a'},
{"quiet", no_argument, 0, 'q'},
{"deps", no_argument, 0, 'd'},
{"src-deps", no_argument, &only_src_deps, 1},
{"deps-json", no_argument, 0, 'J'},
{"timeout", optional_argument, 0, 'T'},
{"c", optional_argument, 0, 'c'},
@@ -402,12 +399,6 @@ void print_imports(std::string const & input, std::string const & fname) {
consume_io_result(lean_print_imports(mk_string(input), mk_option_some(mk_string(fname)), io_mk_world()));
}
/* def printImportSrcs (input : String) (fileName : Option String := none) : IO Unit */
extern "C" object* lean_print_import_srcs(object* input, object* file_name, object* w);
void print_import_srcs(std::string const & input, std::string const & fname) {
consume_io_result(lean_print_import_srcs(mk_string(input), mk_option_some(mk_string(fname)), io_mk_world()));
}
/* def printImportsJson (fileNames : Array String) : IO Unit */
extern "C" object* lean_print_imports_json(object * file_names, object * w);
void print_imports_json(array_ref<string_ref> const & fnames) {
@@ -706,11 +697,6 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
return 0;
}
if (only_src_deps) {
print_import_srcs(contents, mod_fn);
return 0;
}
// Quick and dirty `#lang` support
// TODO: make it extensible, and add `lean4md`
if (contents.compare(0, 5, "#lang") == 0) {

View File

@@ -1,26 +0,0 @@
/-! Dot ident notation should resolve mutual definitions -/
mutual
inductive Even
| zero
| succ (n : Odd)
deriving Inhabited
inductive Odd
| succ (n : Even)
deriving Inhabited
end
mutual
def Even.ofNat : Nat Even
| 0 => .zero
| n + 1 => .succ (.ofNat n)
def Odd.ofNat : Nat Odd
| 0 => panic! "invalid input"
| n + 1 => .succ (.ofNat n)
end

View File

@@ -1,219 +0,0 @@
import Std.Internal.UV
open Std.Internal.UV
def assertElapsed (t1 t2 : Nat) (should : Nat) (eps : Nat) : IO Unit := do
let dur := t2 - t1
if (Int.ofNat dur - Int.ofNat should).natAbs > eps then
throw <| .userError s!"elapsed time was too different, measured {dur}, should: {should}, tolerance: {eps}"
def assertDuration (should : Nat) (eps : Nat) (x : IO α) : IO α := do
let t1 IO.monoMsNow
let res x
let t2 IO.monoMsNow
assertElapsed t1 t2 should eps
return res
def BASE_DURATION : Nat := 1000
-- generous tolerance for slow CI systems
def EPS : Nat := 150
def await (x : Task α) : IO α := pure x.get
namespace SleepTest
def oneShotSleep : IO Unit := do
assertDuration BASE_DURATION EPS do
let timer Timer.mk BASE_DURATION.toUInt64 false
let p timer.next
await p.result
def promiseBehavior1 : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 false
let p timer.next
let r := p.result
assert! ( IO.getTaskState r) != .finished
IO.sleep (BASE_DURATION + EPS).toUInt32
assert! ( IO.getTaskState r) == .finished
def promiseBehavior2 : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 false
let p1 timer.next
let p2 timer.next
assert! ( IO.getTaskState p1.result) != .finished
assert! ( IO.getTaskState p2.result) != .finished
IO.sleep (BASE_DURATION + EPS).toUInt32
assert! ( IO.getTaskState p1.result) == .finished
assert! ( IO.getTaskState p2.result) == .finished
def promiseBehavior3 : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 false
let p1 timer.next
assert! ( IO.getTaskState p1.result) != .finished
IO.sleep (BASE_DURATION + EPS).toUInt32
assert! ( IO.getTaskState p1.result) == .finished
let p3 timer.next
assert! ( IO.getTaskState p3.result) == .finished
def resetBehavior : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 false
let p timer.next
assert! ( IO.getTaskState p.result) != .finished
IO.sleep (BASE_DURATION / 2).toUInt32
assert! ( IO.getTaskState p.result) != .finished
timer.reset
IO.sleep (BASE_DURATION / 2).toUInt32
assert! ( IO.getTaskState p.result) != .finished
IO.sleep ((BASE_DURATION / 2) + EPS).toUInt32
assert! ( IO.getTaskState p.result) == .finished
#eval oneShotSleep
#eval promiseBehavior1
#eval promiseBehavior2
#eval promiseBehavior3
#eval resetBehavior
#eval oneShotSleep
end SleepTest
namespace IntervalTest
def sleepFirst : IO Unit := do
assertDuration 0 EPS go
where
go : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 true
let prom timer.next
await prom.result
timer.stop
def sleepSecond : IO Unit := do
discard <| assertDuration BASE_DURATION EPS go
where
go : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 true
let task
IO.bindTask ( timer.next).result fun _ => do
IO.bindTask ( timer.next).result fun _ => pure (Task.pure (.ok 2))
discard <| await task
timer.stop
def promiseBehavior1 : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 true
let p1 timer.next
IO.sleep EPS.toUInt32
assert! ( IO.getTaskState p1.result) == .finished
let p2 timer.next
assert! ( IO.getTaskState p2.result) != .finished
IO.sleep (BASE_DURATION + EPS).toUInt32
assert! ( IO.getTaskState p2.result) == .finished
timer.stop
def promiseBehavior2 : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 true
let p1 timer.next
IO.sleep EPS.toUInt32
assert! ( IO.getTaskState p1.result) == .finished
let prom1 timer.next
let prom2 timer.next
assert! ( IO.getTaskState prom1.result) != .finished
assert! ( IO.getTaskState prom2.result) != .finished
IO.sleep (BASE_DURATION + EPS).toUInt32
assert! ( IO.getTaskState prom1.result) == .finished
assert! ( IO.getTaskState prom2.result) == .finished
timer.stop
def promiseBehavior3 : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 true
let p1 timer.next
IO.sleep EPS.toUInt32
assert! ( IO.getTaskState p1.result) == .finished
let prom1 timer.next
assert! ( IO.getTaskState prom1.result) != .finished
IO.sleep (BASE_DURATION + EPS).toUInt32
assert! ( IO.getTaskState prom1.result) == .finished
let prom2 timer.next
assert! ( IO.getTaskState prom2.result) != .finished
IO.sleep (BASE_DURATION + EPS).toUInt32
assert! ( IO.getTaskState prom2.result) == .finished
timer.stop
def delayedTickBehavior : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 true
let p1 timer.next
IO.sleep EPS.toUInt32
assert! ( IO.getTaskState p1.result) == .finished
IO.sleep (BASE_DURATION / 2).toUInt32
let p2 timer.next
assert! ( IO.getTaskState p2.result) != .finished
IO.sleep ((BASE_DURATION / 2) + EPS).toUInt32
assert! ( IO.getTaskState p2.result) == .finished
timer.stop
def skippedTickBehavior : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 true
let p1 timer.next
IO.sleep EPS.toUInt32
assert! ( IO.getTaskState p1.result) == .finished
IO.sleep (2 * BASE_DURATION + BASE_DURATION / 2).toUInt32
let p2 timer.next
assert! ( IO.getTaskState p2.result) != .finished
IO.sleep ((BASE_DURATION / 2) + EPS).toUInt32
assert! ( IO.getTaskState p2.result) == .finished
timer.stop
def resetBehavior : IO Unit := do
let timer Timer.mk BASE_DURATION.toUInt64 true
let p1 timer.next
IO.sleep EPS.toUInt32
assert! ( IO.getTaskState p1.result) == .finished
let prom timer.next
assert! ( IO.getTaskState prom.result) != .finished
IO.sleep (BASE_DURATION / 2).toUInt32
assert! ( IO.getTaskState prom.result) != .finished
timer.reset
IO.sleep (BASE_DURATION / 2).toUInt32
assert! ( IO.getTaskState prom.result) != .finished
IO.sleep ((BASE_DURATION / 2) + EPS).toUInt32
assert! ( IO.getTaskState prom.result) == .finished
timer.stop
def sequentialSleep : IO Unit := do
discard <| assertDuration BASE_DURATION EPS go
where
go : IO Unit := do
let timer Timer.mk (BASE_DURATION / 2).toUInt64 true
-- 0th interval ticks instantly
let task
IO.bindTask ( timer.next).result fun _ => do
IO.bindTask ( timer.next).result fun _ => do
IO.bindTask ( timer.next).result fun _ => pure (Task.pure (.ok 2))
discard <| await task
timer.stop
#eval sleepFirst
#eval sleepSecond
#eval promiseBehavior1
#eval promiseBehavior2
#eval promiseBehavior3
#eval delayedTickBehavior
#eval skippedTickBehavior
#eval resetBehavior
#eval sequentialSleep
end IntervalTest

View File

@@ -1,99 +0,0 @@
import Std.Internal.Async.Timer
/-
these tests are just some preliminary ones as `async_sleep.lean` already contains extensive tests
for the entire timer state machine and `Async.Timer` is merely a light wrapper around it.
-/
open Std.Internal.IO.Async
def BASE_DURATION : Std.Time.Millisecond.Offset := 10
namespace SleepTest
def oneSleep : IO Unit := do
let task go
assert! ( task.block) == 37
where
go : IO (AsyncTask Nat) := do
let sleep Sleep.mk BASE_DURATION
( sleep.wait).mapIO fun _ =>
return 37
def doubleSleep : IO Unit := do
let task go
assert! ( task.block) == 37
where
go : IO (AsyncTask Nat) := do
let sleep Sleep.mk BASE_DURATION
( sleep.wait).bindIO fun _ => do
( sleep.wait).mapIO fun _ =>
return 37
def resetSleep : IO Unit := do
let task go
assert! ( task.block) == 37
where
go : IO (AsyncTask Nat) := do
let sleep Sleep.mk BASE_DURATION
let waiter sleep.wait
sleep.reset
waiter.mapIO fun _ =>
return 37
def simpleSleep : IO Unit := do
let task go
assert! ( task.block) == 37
where
go : IO (AsyncTask Nat) := do
( sleep BASE_DURATION).mapIO fun _ =>
return 37
#eval oneSleep
#eval doubleSleep
#eval resetSleep
#eval simpleSleep
end SleepTest
namespace IntervalTest
def oneSleep : IO Unit := do
let task go
assert! ( task.block) == 37
where
go : IO (AsyncTask Nat) := do
let interval Interval.mk BASE_DURATION
( interval.tick).mapIO fun _ => do
interval.stop
return 37
def doubleSleep : IO Unit := do
let task go
assert! ( task.block) == 37
where
go : IO (AsyncTask Nat) := do
let interval Interval.mk BASE_DURATION
( interval.tick).bindIO fun _ => do
( interval.tick).mapIO fun _ => do
interval.stop
return 37
def resetSleep : IO Unit := do
let task go
assert! ( task.block) == 37
where
go : IO (AsyncTask Nat) := do
let interval Interval.mk BASE_DURATION
( interval.tick).bindIO fun _ => do
let waiter interval.tick
interval.reset
waiter.mapIO fun _ => do
interval.stop
return 37
#eval oneSleep
#eval doubleSleep
#eval resetSleep
end IntervalTest

View File

@@ -53,13 +53,11 @@ theorem left_comm [CommMonoid α] (a b c : α) : a * (b * c) = b * (a * c) := by
open Lean Meta Elab Tactic Grind in
def fallback : Fallback := do
let nodes filterENodes fun e => return e.self.isAppOf ``HMul.hMul
trace[Meta.debug] "{nodes.toList.map (·.self)}"
logInfo (nodes.toList.map (·.self))
( get).mvarId.admit
set_option trace.Meta.debug true
/--
info: [Meta.debug] [b * c, a * (b * c), d * (b * c)]
info: [b * c, a * (b * c), d * (b * c)]
-/
#guard_msgs (info) in
example (a b c d : Nat) : b * (a * c) = d * (b * c) False := by
@@ -70,8 +68,7 @@ example (a b c d : Nat) : b * (a * c) = d * (b * c) → False := by
set_option pp.notation false in
set_option pp.explicit true in
/--
info: [Meta.debug] [@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a,
@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b d]
info: [@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a, @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b d]
-/
#guard_msgs (info) in
example (a b c d : Nat) : b * a = d * b False := by

View File

@@ -6,13 +6,12 @@ def f (a : α) := a
open Lean Meta Grind in
def fallback : Fallback := do
let nodes filterENodes fun e => return e.self.isAppOf ``f
trace[Meta.debug] "{nodes.toList.map (·.self)}"
logInfo (nodes.toList.map (·.self))
( get).mvarId.admit
set_option trace.Meta.debug true
set_option pp.explicit true
/--
info: [Meta.debug] [@f Nat a, @f Nat b]
info: [@f Nat a, @f Nat b]
-/
#guard_msgs (info) in
example (a b c d : Nat) : @f Nat a = b @f (g Nat) a = c @f (g Nat) b = d a = b False := by

View File

@@ -8,36 +8,35 @@ open Lean Meta Grind in
def fallback : Fallback := do
let #[n, _] filterENodes fun e => return e.self.isAppOf ``f | unreachable!
let eqc getEqc n.self
trace[Meta.debug] eqc
logInfo eqc
( get).mvarId.admit
set_option trace.Meta.debug true
set_option grind.debug true
set_option grind.debug.proofs true
/--
info: [Meta.debug] [d, f b, c, f a]
info: [d, f b, c, f a]
-/
#guard_msgs (info) in
example (a b c d : Nat) : a = b f a = c f b = d False := by
grind on_failure fallback
/--
info: [Meta.debug] [d, f b, c, f a]
info: [d, f b, c, f a]
-/
#guard_msgs (info) in
example (a b c d : Nat) : f a = c f b = d a = b False := by
grind on_failure fallback
/--
info: [Meta.debug] [d, f (g b), c, f (g a)]
info: [d, f (g b), c, f (g a)]
-/
#guard_msgs (info) in
example (a b c d e : Nat) : f (g a) = c f (g b) = d a = e b = e False := by
grind on_failure fallback
/--
info: [Meta.debug] [d, f (g b), c, f v]
info: [d, f (g b), c, f v]
-/
#guard_msgs (info) in
example (a b c d e v : Nat) : f v = c f (g b) = d a = e b = e v = g a False := by

View File

@@ -1,22 +0,0 @@
attribute [grind] List.append_ne_nil_of_left_ne_nil
attribute [grind] List.append_ne_nil_of_right_ne_nil
/--
info: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some ? #0]
-/
#guard_msgs (info) in
set_option trace.grind.ematch.pattern true in
attribute [grind =] List.getLast?_eq_some_iff
/--
info: [grind.assert] xs.getLast? = b?
[grind.assert] b? = some 10
[grind.assert] xs = []
[grind.assert] (xs.getLast? = some 10) = ∃ ys, xs = ys ++ [10]
[grind.assert] xs = w ++ [10]
[grind.assert] ¬w = [] → ¬w ++ [10] = []
[grind.assert] ¬w ++ [10] = []
-/
#guard_msgs (info) in
set_option trace.grind.assert true in
example (xs : List Nat) : xs.getLast? = b? b? = some 10 xs [] := by
grind

View File

@@ -24,15 +24,17 @@ example : f (f (f a)) = f a := by
attribute [-grind] fthm
/--
error: unsolved goals
error: `grind` failed
case grind
a : Nat
f (f (f a)) = f a
x✝ : ¬f (f (f a)) = f a
⊢ False
---
info: [grind.assert] ¬f (f (f a)) = f a
-/
#guard_msgs (info, error) in
example : f (f (f a)) = f a := by
fail_if_success grind
grind
/--
error: `fthm` is not marked with the `[grind]` attribute
@@ -58,9 +60,13 @@ example : g a = b → a = 0 → b = 1 := by
attribute [-grind] g
/--
error: unsolved goals
error: `grind` failed
case grind
a b : Nat
⊢ g a = b → a = 0 → b = 1
a✝¹ : g a = b
a✝ : a = 0
x✝ : ¬b = 1
⊢ False
---
info: [grind.assert] g a = b
[grind.assert] a = 0
@@ -68,7 +74,7 @@ info: [grind.assert] g a = b
-/
#guard_msgs (info, error) in
example : g a = b a = 0 b = 1 := by
fail_if_success grind
grind
/--
error: `g` is not marked with the `[grind]` attribute

View File

@@ -5,13 +5,12 @@ def f (α : Type) [Add α] (a : α) := a + a + a
open Lean Meta Grind in
def fallback : Fallback := do
let nodes filterENodes fun e => return e.self.isAppOf ``Lean.Grind.nestedProof
trace[Meta.debug] "{nodes.toList.map (·.self)}"
logInfo (nodes.toList.map (·.self))
let nodes filterENodes fun e => return e.self.isAppOf ``GetElem.getElem
let [_, n, _] := nodes.toList | unreachable!
trace[Meta.debug] "{← getEqc n.self}"
logInfo ( getEqc n.self)
( get).mvarId.admit
set_option trace.Meta.debug true
set_option grind.debug true
set_option grind.debug.proofs true
@@ -21,21 +20,26 @@ The following test relies on `grind` `nestedProof` wrapper to
detect equalities between array access terms.
-/
/--
info: [Meta.debug] [Lean.Grind.nestedProof (i < a.toList.length),
Lean.Grind.nestedProof (j < a.toList.length),
Lean.Grind.nestedProof (j < b.toList.length)]
[Meta.debug] [a[i], b[j], a[j]]
/-
info: [Lean.Grind.nestedProof (i < a.toList.length) (_example.proof_1 i j a b h1 h2),
Lean.Grind.nestedProof (j < a.toList.length) h1,
Lean.Grind.nestedProof (j < b.toList.length) h]
---
info: [a[i], b[j], a[j]]
---
warning: declaration uses 'sorry'
-/
#guard_msgs (info) in
-- #guard_msgs in
example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i j) : a[i] < a[j] + b[j] i = j a = b False := by
grind on_failure fallback
/--
info: [Meta.debug] [Lean.Grind.nestedProof (i < a.toList.length),
Lean.Grind.nestedProof (j < a.toList.length),
Lean.Grind.nestedProof (j < b.toList.length)]
[Meta.debug] [a[i], a[j]]
info: [Lean.Grind.nestedProof (i < a.toList.length) (_example.proof_1 i j a b h1 h2),
Lean.Grind.nestedProof (j < a.toList.length) h1,
Lean.Grind.nestedProof (j < b.toList.length) h]
---
info: [a[i], a[j]]
-/
#guard_msgs (info) in
example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i j) : a[i] < a[j] + b[j] i = j False := by

View File

@@ -5,13 +5,12 @@ def g {α : Sort u} (a : α) := a
open Lean Meta Grind in
def fallback : Fallback := do
let nodes filterENodes fun e => return e.self.isAppOf ``g
trace[Meta.debug] "{nodes.toList.map (·.self)}"
logInfo (nodes.toList.map (·.self))
( get).mvarId.admit
-- `grind` final state must contain only two `g`-applications
set_option trace.Meta.debug true in
/--
info: [Meta.debug] [g (a, b), g (g (a, b))]
info: [g (a, b), g (g (a, b))]
-/
#guard_msgs (info) in
example {β : Type v} {α : Type u} (a c : α) (b d : β) : g.{max u v + 1} (a, b) = (c, d) g (g.{max (u+1) (v+1)} (a, b)) = (c, d) False := by

View File

@@ -1,354 +0,0 @@
set_option grind.debug true
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.internalize] a1 + 1 ≤ a2 ↦ #0 + 1 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.internalize] a2 ≤ a3 + 2 ↦ #1 ≤ #2 + 2
[grind.offset.internalize.term] a4 ↦ #3
[grind.offset.internalize] a3 ≤ a4 ↦ #2 ≤ #3
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize true in
example (a1 a2 a3) :
a1 + 1 a2 a2 a3 + 2 a3 a4 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 + 1 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2
[grind.offset.dist] #0 + 1 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 + 1 a2 a2 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 + 1 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 + 2 ≤ #2
[grind.offset.dist] #0 + 3 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 + 1 a2 a2 + 2 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 + 1 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2 + 2
[grind.offset.dist] #0 ≤ #2 + 1
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 + 1 a2 a2 a3 + 2 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2
[grind.offset.dist] #0 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 a2 a2 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 + 2 ≤ #2
[grind.offset.dist] #0 + 2 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 a2 a2 + 2 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2 + 5
[grind.offset.dist] #0 ≤ #2 + 5
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 a2 a2 a3 + 5 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1 + 5
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2
[grind.offset.dist] #0 ≤ #2 + 5
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 a2 + 5 a2 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1 + 5
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 + 2 ≤ #2
[grind.offset.dist] #0 ≤ #2 + 3
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 a2 + 5 a2 + 2 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1 + 5
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2 + 2
[grind.offset.dist] #0 ≤ #2 + 7
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
a1 a2 + 5 a2 a3 + 2 False := by
fail_if_success grind
sorry
set_option trace.grind.debug.offset.proof true in
example (a1 a2 a3 : Nat) :
a1 a2 + 5 a2 a3 + 2 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1 + 2
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 + 3 ≤ #2
[grind.offset.dist] #0 + 1 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) : a1 a2 + 2 a2 + 3 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a2 ↦ #0
[grind.offset.internalize.term] a1 ↦ #1
[grind.offset.dist] #1 + 3 ≤ #0
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #0 + 3 ≤ #2
[grind.offset.dist] #1 + 6 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (p : Prop) (a1 a2 a3 : Nat) : (p a2 a1 + 2) ¬p a2 + 3 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a2 ↦ #0
[grind.offset.internalize.term] a1 ↦ #1
[grind.offset.dist] #1 ≤ #0 + 1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #0 + 3 ≤ #2
[grind.offset.dist] #1 + 2 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (p : Prop) (a1 a2 a3 : Nat) : (p a2 + 2 a1) ¬p a2 + 3 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a2 ↦ #0
[grind.offset.internalize.term] a1 ↦ #1
[grind.offset.dist] #1 + 1 ≤ #0
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #0 + 3 ≤ #2
[grind.offset.dist] #1 + 4 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (p : Prop) (a1 a2 a3 : Nat) : (p a2 a1) ¬p a2 + 3 a3 False := by
fail_if_success grind
sorry
/--
info: [grind.offset.internalize.term] a2 ↦ #0
[grind.offset.internalize.term] a1 ↦ #1
[grind.offset.dist] #1 ≤ #0
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #0 + 3 ≤ #2
[grind.offset.dist] #1 + 3 ≤ #2
-/
#guard_msgs (info) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (p : Prop) (a1 a2 a3 : Nat) : (p a2 + 1 a1) ¬p a2 + 3 a3 False := by
fail_if_success grind
sorry
example (a b c : Nat) : a b b + 2 c a + 1 c := by
grind
example (a b c : Nat) : a b b c a c := by
grind
example (a b c : Nat) : a + 1 b b + 1 c a + 2 c := by
grind
example (a b c : Nat) : a + 1 b b + 1 c a + 1 c := by
grind
example (a b c : Nat) : a + 1 b b c + 2 a c + 1 := by
grind
example (a b c : Nat) : a + 2 b b c + 2 a c := by
grind
theorem ex1 (p : Prop) (a1 a2 a3 : Nat) : (p a2 a1) ¬p a2 + 3 a3 (p a4 a3 + 2) a1 a4 := by
grind
/--
info: theorem ex1 : ∀ {a4 : Nat} (p : Prop) (a1 a2 a3 : Nat),
(p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 :=
fun {a4} p a1 a2 a3 =>
intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4) (iff_eq p (a2 ≤ a1))
fun a a_1 a_2 =>
intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun a_3 =>
Classical.byContradiction
(intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun x =>
Nat.unsat_lo_lo a4 a1 1 7 rfl_true x
(Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm a) (eq_false a_1)))
(Nat.lo_lo a2 a3 a4 3 3 a_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm a_3) (eq_false a_1))))))
-/
#guard_msgs (info) in
open Lean Grind in
#print ex1
/-! Propagate `cnstr = False` tests -/
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p q r s : Prop) (a b : Nat) : a b b + 2 c (a + 1 c p) (a + 2 c s) (a c q) (a c + 4 r) p q r s := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p q : Prop) (a b : Nat) : a b b c (a c p) (a c + 1 q) p q := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p q : Prop) (a b : Nat) : a b b c + 1 (a c + 1 p) (a c + 2 q) p q := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p r s : Prop) (a b : Nat) : a b b + 2 c (c a p) (c a + 1 s) (c + 1 a r) ¬p ¬r ¬s := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p r : Prop) (a b : Nat) : a b b c (c + 1 a p) (c + 2 a + 1 r) ¬p ¬r := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p r : Prop) (a b : Nat) : a b b c + 3 (c + 5 a p) (c + 4 a r) ¬p ¬r := by
grind (splits := 0)
/-! Propagate `cnstr = False` tests, but with different internalization order -/
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p q r s : Prop) (a b : Nat) : (a + 1 c p) (a + 2 c s) (a c q) (a c + 4 r) a b b + 2 c p q r s := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p q : Prop) (a b : Nat) : (a c p) (a c + 1 q) a b b c p q := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p q : Prop) (a b : Nat) : (a c + 1 p) (a c + 2 q) a b b c + 1 p q := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p r s : Prop) (a b : Nat) : (c a p) (c a + 1 s) (c + 1 a r) a b b + 2 c ¬p ¬r ¬s := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p r : Prop) (a b : Nat) : (c + 1 a p) (c + 2 a + 1 r) a b b c ¬p ¬r := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
set_option trace.grind.split true in
example (p r : Prop) (a b : Nat) : (c + 5 a p) (c + 4 a r) a b b c + 3 ¬p ¬r := by
grind (splits := 0)

View File

@@ -0,0 +1,31 @@
import Lean
elab tk:"#R[" ts:term,* "]" : term => do
let ts : Array Lean.Syntax := ts
let es ts.mapM fun stx => Lean.Elab.Term.elabTerm stx none
if h : 0 < es.size then
return (Lean.RArray.toExpr ( Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h))
else
throwErrorAt tk "RArray cannot be empty"
open Lean.Grind.Offset
macro "C[" "#" x:term:max "" "#" y:term:max "]" : term => `({ x := $x, y := $y : Cnstr })
macro "C[" "#" x:term:max " + " k:term:max "" "#" y:term:max "]" : term => `({ x := $x, y := $y, k := $k : Cnstr })
macro "C[" "#" x:term:max "" "#"y:term:max " + " k:term:max "]" : term => `({ x := $x, y := $y, k := $k, l := false : Cnstr })
example (x y z : Nat) : x + 2 y y z z + 1 x False :=
Cnstrs.unsat #R[x, y, z] [
C[ #0 + 2 #1 ],
C[ #1 #2 ],
C[ #2 + 1 #0 ]
] rfl
example (x y z w : Nat) : x + 2 y y z z w + 7 x w + 5 :=
Cnstrs.imp #R[x, y, z, w] [
C[ #0 + 2 #1 ],
C[ #1 #2 ],
C[ #2 #3 + 7]
]
C[ #0 #3 + 5 ]
rfl

View File

@@ -9,27 +9,13 @@ case grind.1.2
a b c : Bool
p q : Prop
left✝ : a = true
right✝ : b = true c = true
left : p
right : q
x✝ : b = false a = false
h✝ : b = false
h : c = true
⊢ False[facts] Asserted facts
[prop] a = true
[prop] b = true c = true
[prop] p
[prop] q
[prop] b = false a = false
[prop] b = false
[prop] c = true[eqc] True propositions
[prop] b = true c = true
[prop] p
[prop] q
[prop] b = false a = false
[prop] b = false
[prop] c = true[eqc] Equivalence classes
[eqc] {b = true, a = false}
[eqc] {b, false}
[eqc] {a, c, true}
⊢ False
-/
#guard_msgs (error) in
theorem ex (h : (f a && (b || f (f c))) = true) (h' : p q) : b && a := by
@@ -46,16 +32,7 @@ h✝ : c = true
left : p
right : q
h : b = false
⊢ False[facts] Asserted facts
[prop] a = true
[prop] c = true
[prop] p
[prop] q
[prop] b = false[eqc] True propositions
[prop] p
[prop] q[eqc] Equivalence classes
[eqc] {b, false}
[eqc] {a, c, true}
⊢ False
-/
#guard_msgs (error) in
theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p q) : b && a := by
@@ -70,15 +47,7 @@ i j : Nat
h : j + 1 < i + 1
h✝ : j + 1 ≤ i
x✝ : ¬g (i + 1) j ⋯ = i + j + 1
⊢ False[facts] Asserted facts
[prop] j + 1 ≤ i
[prop] ¬g (i + 1) j ⋯ = i + j + 1[eqc] True propositions
[prop] j + 1 ≤ i[eqc] False propositions
[prop] g (i + 1) j ⋯ = i + j + 1[offset] Assignment satisfying offset contraints
[assign] j := 0
[assign] i := 1
[assign] g (i + 1) j ⋯ := 0
[assign] i + j := 0
⊢ False
-/
#guard_msgs (error) in
example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
@@ -103,15 +72,7 @@ head_eq : a₁ = b₁
x_eq : a₂ = b₂
y_eq : a₃ = b₃
tail_eq : as = bs
⊢ False[facts] Asserted facts
[prop] a₁ = b₁
[prop] a₂ = b₂
[prop] a₃ = b₃
[prop] as = bs[eqc] Equivalence classes
[eqc] {as, bs}
[eqc] {a₃, b₃}
[eqc] {a₂, b₂}
[eqc] {a₁, b₁}
⊢ False
-/
#guard_msgs (error) in
theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x := b₂, y := b₃} :: bs) : False := by
@@ -133,23 +94,10 @@ h₁ : HEq p a
h₂ : HEq q a
h₃ : p = r
left : ¬p r
right : ¬r p
h : ¬r
⊢ False[facts] Asserted facts
[prop] HEq p a
[prop] HEq q a
[prop] p = r
[prop] ¬p r
[prop] ¬r p
[prop] ¬r[eqc] True propositions
[prop] p = r
[prop] ¬p r
[prop] ¬r p
[prop] ¬p
[prop] ¬r[eqc] False propositions
[prop] a
[prop] p
[prop] q
[prop] r
⊢ False
case grind.2
α : Type
a : α
@@ -158,23 +106,9 @@ h₁ : HEq p a
h₂ : HEq q a
h₃ : p = r
left : ¬p r
right : ¬r p
h : p
⊢ False[facts] Asserted facts
[prop] HEq p a
[prop] HEq q a
[prop] p = r
[prop] ¬p r
[prop] ¬r p
[prop] p[eqc] True propositions
[prop] p = r
[prop] ¬p r
[prop] ¬r p
[prop] a
[prop] p
[prop] q
[prop] r[eqc] False propositions
[prop] ¬p
[prop] ¬r
⊢ False
-/
#guard_msgs (error) in
example (a : α) (p q r : Prop) : (h₁ : HEq p a) (h₂ : HEq q a) (h₃ : p = r) False := by

View File

@@ -1,25 +1,24 @@
import Lean.Meta.Tactic.Grind
set_option trace.Meta.debug true
open Lean Meta Grind in
def fallback : Fallback := do
let trueExprs := ( filterENodes fun e => return e.self.isFVar && ( isEqTrue e.self)).toList.map (·.self)
let falseExprs := ( filterENodes fun e => return e.self.isFVar && ( isEqFalse e.self)).toList.map (·.self)
trace[Meta.debug] "true: {trueExprs}"
trace[Meta.debug] "false: {falseExprs}"
forEachEqcRoot fun n => do
logInfo m!"true: {trueExprs}"
logInfo m!"false: {falseExprs}"
forEachEqc fun n => do
unless ( isProp n.self) || ( isType n.self) || n.size == 1 do
let eqc getEqc n.self
trace[Meta.debug] eqc
logInfo eqc
( get).mvarId.admit
set_option grind.debug true
set_option grind.debug.proofs true
/--
info: [Meta.debug] true: [q, w]
[Meta.debug] false: [p, r]
info: true: [q, w]
---
info: false: [p, r]
-/
#guard_msgs (info) in
example : (p (q ¬r w)) ¬p False := by
@@ -27,8 +26,9 @@ example : (p (q ∧ ¬r ∧ w)) → ¬p → False := by
/--
info: [Meta.debug] true: [r]
[Meta.debug] false: [p, q]
info: true: [r]
---
info: false: [p, q]
-/
#guard_msgs (info) in
example : (p q r) (p ¬q) ¬p False := by
@@ -36,63 +36,72 @@ example : (p q r) → (p ¬q) → ¬p → False := by
/--
info: [Meta.debug] true: [r]
[Meta.debug] false: [p₁, q]
info: true: [r]
---
info: false: [p₁, q]
-/
#guard_msgs (info) in
example : ((p₁ p₂) q r) (p₁ ¬q) p₁ = False False := by
grind on_failure fallback
/--
info: [Meta.debug] true: [r]
[Meta.debug] false: [p₂, q]
info: true: [r]
---
info: false: [p₂, q]
-/
#guard_msgs (info) in
example : ((p₁ p₂) q r) ((p₂ p₁) ¬q) p₂ = False False := by
grind on_failure fallback
/--
info: [Meta.debug] true: [q, r]
[Meta.debug] false: [p]
info: true: [q, r]
---
info: false: [p]
-/
#guard_msgs (info) in
example (p q r : Prop) : p (q r) p = False q False := by
grind on_failure fallback
/--
info: [Meta.debug] true: [r]
[Meta.debug] false: [p, s]
info: true: [r]
---
info: false: [p, s]
-/
#guard_msgs (info) in
example (p q r : Prop) : p ¬(s (p r)) p = False False := by
grind on_failure fallback
/--
info: [Meta.debug] true: [p]
[Meta.debug] false: []
[Meta.debug] [a, b]
info: true: [p]
---
info: false: []
---
info: [a, b]
-/
#guard_msgs (info) in
example (p : Prop) (a : Vector Nat 5) (b : Vector Nat 6) : (p HEq a b) p False := by
grind on_failure fallback
/--
info: [Meta.debug] true: [p, q]
[Meta.debug] false: [r]
info: true: [p, q]
---
info: false: [r]
-/
#guard_msgs (info) in
example (p q r : Prop) : p (q r) q ¬r False := by
grind on_failure fallback
/--
info: [Meta.debug] hello world
[Meta.debug] true: [p, q]
[Meta.debug] false: [r]
info: hello world
---
info: true: [p, q]
---
info: false: [r]
-/
#guard_msgs (info) in
example (p q r : Prop) : p (q r) ¬r q False := by
grind on_failure do
trace[Meta.debug] "hello world"
Lean.logInfo "hello world"
fallback
example (a b : Nat) : (a = b) = (b = a) := by

View File

@@ -0,0 +1,27 @@
import Lean
open Lean Elab Tactic in
elab "revert_all" : tactic => do
liftMetaTactic1 (·.revertAll)
open Lean Elab Tactic in
elab "ensure_no_mvar" : tactic => do
liftMetaTactic1 fun mvarId => do
mvarId.ensureNoMVar
return mvarId
example {α : Type u} [Inhabited α] (a : α) (f : α α) (h : f a = default) : default = f a := by
revert_all
ensure_no_mvar
guard_target = {α : Type u} [inst : Inhabited α] (a : α) (f : α α), f a = default default = f a
intro α inst a f h
exact h.symm
example (a b : α) (h₁ : a = b) (f g : α α) (h₂ : x, f x = x) (h₃ : x, g x = f x) : x : α, f x = a g x = b := by
apply Exists.intro
revert_all
fail_if_success ensure_no_mvar
intro β a₁ a₂ h f₁ f₂ h' h''
constructor
· exact h' a₁
· rw [h'', h]; exact h' a₂

View File

@@ -234,49 +234,3 @@ example {α} (a b c : α) [LE α] :
example {α} (a b c : α) [LE α] :
¬(¬a b a c ¬a c a b) a b a c ¬a c ¬a b := by
grind
example (x y : Bool) : ¬(x = true y = true) (¬(x = true) y = true) := by
grind
/--
error: `grind` failed
case grind
p q : Prop
a✝¹ : p = q
a✝ : p
⊢ False[facts] Asserted facts
[prop] p = q
[prop] p[eqc] True propositions
[prop] p = q
[prop] q
[prop] p
-/
#guard_msgs (error) in
set_option trace.grind.split true in
example (p q : Prop) : (p q) p False := by
grind -- should not split on (p ↔ q)
/--
error: `grind` failed
case grind
p q : Prop
a✝¹ : p = ¬q
a✝ : p
⊢ False[facts] Asserted facts
[prop] p = ¬q
[prop] p[eqc] True propositions
[prop] p = ¬q
[prop] ¬q
[prop] p[eqc] False propositions
[prop] q
-/
#guard_msgs (error) in
set_option trace.grind.split true in
example (p q : Prop) : ¬(p q) p False := by
grind -- should not split on (p ↔ q)
example {a b : Nat} (h : a < b) : ¬ b < a := by
grind
example {m n : Nat} : m < n m n ¬ n m := by
grind

View File

@@ -587,7 +587,7 @@ Std.Time.Weekday.friday
2023-06-09
2023-06-09
19517
1686268800
1686268800000
1970-01-02
-/
@@ -667,7 +667,7 @@ Std.Time.Weekday.tuesday
12
3
9938
858650584
858650584000
1970-01-02T00:00:00.000000000
-/
@@ -741,7 +741,7 @@ Std.Time.Weekday.thursday
37
2
19978
1726117262
1726117262000
1970-01-02T00:00:00.000000000Z
-/
@@ -816,7 +816,7 @@ Std.Time.Weekday.tuesday
12
3
9938
858661384
858661384000
-/
#guard_msgs in

View File

@@ -277,7 +277,7 @@ Format
def time₄ := time("23:13:12.324354679")
def date₄ := date("2002-07-14")
def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 12 0)
def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 false, 12 0)
def datetime₄ := datetime("2002-07-14T23:13:12.324354679")
def zoned₄ := zoned("2002-07-14T23:13:12.324354679+09:00")
def zoned₅ := zoned("2002-07-14T23:13:12.324354679+00:00")
@@ -806,7 +806,7 @@ info: ("19343232432-01-04T01:04:03.000000000",
-/
#guard_msgs in
#eval
let r := PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 3 0)
let r := (PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 true, 3 0))
let s := r.toLeanDateTimeString
let r := PlainDateTime.parse s
(s, r, datetime("1932-01-02T05:04:03.000000000"))

View File

@@ -91,7 +91,7 @@ info: zoned("2014-06-16T10:03:03.000000000-03:00")
info: zoned("2014-06-16T10:03:59.000000000-03:00")
-/
#guard_msgs in
#eval date₁.withSeconds 59
#eval date₁.withSeconds true, 59
/--
info: zoned("2014-06-16T10:03:03.000000002-03:00")

Some files were not shown because too many files have changed in this diff Show More