Compare commits

..

1 Commits

Author SHA1 Message Date
Kim Morrison
efa1d162c8 chore: review Array operations argument order 2024-11-12 15:33:09 +11:00
826 changed files with 3348 additions and 21510 deletions

View File

@@ -1,7 +1,6 @@
name: Check PR body for changelog convention
on:
merge_group:
pull_request:
types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
@@ -10,7 +9,6 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Check PR body
if: github.event_name == 'pull_request'
uses: actions/github-script@v7
with:
script: |

View File

@@ -170,7 +170,7 @@ lib.warn "The Nix-based build is deprecated" rec {
ln -sf ${lean-all}/* .
'';
buildPhase = ''
ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi' -j$NIX_BUILD_CORES
'';
installPhase = ''
mkdir $out

View File

@@ -1922,12 +1922,12 @@ represents an element of `Squash α` the same as `α` itself
`Squash.lift` will extract a value in any subsingleton `β` from a function on `α`,
while `Nonempty.rec` can only do the same when `β` is a proposition.
-/
def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
def Squash (α : Type u) := Quot (fun (_ _ : α) => True)
/-- The canonical quotient map into `Squash α`. -/
def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x
def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x
theorem Squash.ind {α : Sort u} {motive : Squash α Prop} (h : (a : α), motive (Squash.mk a)) : (q : Squash α), motive q :=
theorem Squash.ind {α : Type u} {motive : Squash α Prop} (h : (a : α), motive (Squash.mk a)) : (q : Squash α), motive q :=
Quot.ind h
/-- If `β` is a subsingleton, then a function `α → β` lifts to `Squash α → β`. -/

View File

@@ -42,4 +42,3 @@ import Init.Data.PLift
import Init.Data.Zero
import Init.Data.NeZero
import Init.Data.Function
import Init.Data.RArray

View File

@@ -18,4 +18,3 @@ import Init.Data.Array.Bootstrap
import Init.Data.Array.GetLit
import Init.Data.Array.MapIdx
import Init.Data.Array.Set
import Init.Data.Array.Monadic

View File

@@ -10,17 +10,6 @@ import Init.Data.List.Attach
namespace Array
/--
`O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
`a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
but is defined only when all members of `l` satisfy `P`, using the proof
to apply `f`.
We replace this at runtime with a more efficient version via the `csimp` lemma `pmap_eq_pmapImpl`.
-/
def pmap {P : α Prop} (f : a, P a β) (l : Array α) (H : a l, P a) : Array β :=
(l.toList.pmap f (fun a m => H a (mem_def.mpr m))).toArray
/--
Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
`Array {x // P x}` is the same as the input `Array α`.
@@ -46,10 +35,6 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
l.toArray.attach = (l.attachWith (· l.toArray) (by simp)).toArray := by
simp [attach]
@[simp] theorem _root_.List.pmap_toArray {l : List α} {P : α Prop} {f : a, P a β} {H : a l.toArray, P a} :
l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray := by
simp [pmap]
@[simp] theorem toList_attachWith {l : Array α} {P : α Prop} {H : x l, P x} :
(l.attachWith P H).toList = l.toList.attachWith P (by simpa [mem_toList] using H) := by
simp [attachWith]
@@ -58,387 +43,6 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
l.attach.toList = l.toList.attachWith (· l) (by simp [mem_toList]) := by
simp [attach]
@[simp] theorem toList_pmap {l : Array α} {P : α Prop} {f : a, P a β} {H : a l, P a} :
(l.pmap f H).toList = l.toList.pmap f (fun a m => H a (mem_def.mpr m)) := by
simp [pmap]
/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
@[inline] private def pmapImpl {P : α Prop} (f : a, P a β) (l : Array α) (H : a l, P a) :
Array β := (l.attachWith _ H).map fun x, h' => f x h'
@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
funext α β p f L h'
cases L
simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith]
apply List.pmap_congr_left
intro a m h₁ h₂
congr
@[simp] theorem pmap_empty {P : α Prop} (f : a, P a β) : pmap f #[] (by simp) = #[] := rfl
@[simp] theorem pmap_push {P : α Prop} (f : a, P a β) (a : α) (l : Array α) (h : b l.push a, P b) :
pmap f (l.push a) h =
(pmap f l (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
simp [pmap]
@[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
@[simp] theorem attachWith_empty {P : α Prop} (H : x #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
@[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
l.attachWith (fun x => x l.toArray) (fun x h => by simpa using h) =
l.attach.map fun x, h => x, by simpa using h := by
simp only [List.attachWith, List.attach, List.map_pmap]
apply List.pmap_congr_left
simp
@[simp]
theorem pmap_eq_map (p : α Prop) (f : α β) (l : Array α) (H) :
@pmap _ _ p (fun a _ => f a) l H = map f l := by
cases l; simp
theorem pmap_congr_left {p q : α Prop} {f : a, p a β} {g : a, q a β} (l : Array α) {H₁ H₂}
(h : a l, (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂ := by
cases l
simp only [mem_toArray] at h
simp only [List.pmap_toArray, mk.injEq]
rw [List.pmap_congr_left _ h]
theorem map_pmap {p : α Prop} (g : β γ) (f : a, p a β) (l H) :
map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
cases l
simp [List.map_pmap]
theorem pmap_map {p : β Prop} (g : b, p b γ) (f : α β) (l H) :
pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h) := by
cases l
simp [List.pmap_map]
theorem attach_congr {l₁ l₂ : Array α} (h : l₁ = l₂) :
l₁.attach = l₂.attach.map (fun x => x.1, h x.2) := by
subst h
simp
theorem attachWith_congr {l₁ l₂ : Array α} (w : l₁ = l₂) {P : α Prop} {H : x l₁, P x} :
l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w h) := by
subst w
simp
@[simp] theorem attach_push {a : α} {l : Array α} :
(l.push a).attach =
(l.attach.map (fun x, h => x, mem_push_of_mem a h)).push a, by simp := by
cases l
rw [attach_congr (List.push_toArray _ _)]
simp [Function.comp_def]
@[simp] theorem attachWith_push {a : α} {l : Array α} {P : α Prop} {H : x l.push a, P x} :
(l.push a).attachWith P H =
(l.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push a, H a (by simp) := by
cases l
simp [attachWith_congr (List.push_toArray _ _)]
theorem pmap_eq_map_attach {p : α Prop} (f : a, p a β) (l H) :
pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
cases l
simp [List.pmap_eq_map_attach]
theorem attach_map_coe (l : Array α) (f : α β) :
(l.attach.map fun (i : {i // i l}) => f i) = l.map f := by
cases l
simp [List.attach_map_coe]
theorem attach_map_val (l : Array α) (f : α β) : (l.attach.map fun i => f i.val) = l.map f :=
attach_map_coe _ _
@[simp]
theorem attach_map_subtype_val (l : Array α) : l.attach.map Subtype.val = l := by
cases l; simp
theorem attachWith_map_coe {p : α Prop} (f : α β) (l : Array α) (H : a l, p a) :
((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
cases l; simp
theorem attachWith_map_val {p : α Prop} (f : α β) (l : Array α) (H : a l, p a) :
((l.attachWith p H).map fun i => f i.val) = l.map f :=
attachWith_map_coe _ _ _
@[simp]
theorem attachWith_map_subtype_val {p : α Prop} (l : Array α) (H : a l, p a) :
(l.attachWith p H).map Subtype.val = l := by
cases l; simp
@[simp]
theorem mem_attach (l : Array α) : x, x l.attach
| a, h => by
have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
rcases this with _, _, m, rfl
exact m
@[simp]
theorem mem_pmap {p : α Prop} {f : a, p a β} {l H b} :
b pmap f l H (a : _) (h : a l), f a (H a h) = b := by
simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
theorem mem_pmap_of_mem {p : α Prop} {f : a, p a β} {l H} {a} (h : a l) :
f a (H a h) pmap f l H := by
rw [mem_pmap]
exact a, h, rfl
@[simp]
theorem size_pmap {p : α Prop} {f : a, p a β} {l H} : (pmap f l H).size = l.size := by
cases l; simp
@[simp]
theorem size_attach {L : Array α} : L.attach.size = L.size := by
cases L; simp
@[simp]
theorem size_attachWith {p : α Prop} {l : Array α} {H} : (l.attachWith p H).size = l.size := by
cases l; simp
@[simp]
theorem pmap_eq_empty_iff {p : α Prop} {f : a, p a β} {l H} : pmap f l H = #[] l = #[] := by
cases l; simp
theorem pmap_ne_empty_iff {P : α Prop} (f : (a : α) P a β) {xs : Array α}
(H : (a : α), a xs P a) : xs.pmap f H #[] xs #[] := by
cases xs; simp
theorem pmap_eq_self {l : Array α} {p : α Prop} (hp : (a : α), a l p a)
(f : (a : α) p a α) : l.pmap f hp = l a (h : a l), f a (hp a h) = a := by
cases l; simp [List.pmap_eq_self]
@[simp]
theorem attach_eq_empty_iff {l : Array α} : l.attach = #[] l = #[] := by
cases l; simp
theorem attach_ne_empty_iff {l : Array α} : l.attach #[] l #[] := by
cases l; simp
@[simp]
theorem attachWith_eq_empty_iff {l : Array α} {P : α Prop} {H : a l, P a} :
l.attachWith P H = #[] l = #[] := by
cases l; simp
theorem attachWith_ne_empty_iff {l : Array α} {P : α Prop} {H : a l, P a} :
l.attachWith P H #[] l #[] := by
cases l; simp
@[simp]
theorem getElem?_pmap {p : α Prop} (f : a, p a β) {l : Array α} (h : a l, p a) (n : Nat) :
(pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
cases l; simp
@[simp]
theorem getElem_pmap {p : α Prop} (f : a, p a β) {l : Array α} (h : a l, p a) {n : Nat}
(hn : n < (pmap f l h).size) :
(pmap f l h)[n] =
f (l[n]'(@size_pmap _ _ p f l h hn))
(h _ (getElem_mem (@size_pmap _ _ p f l h hn))) := by
cases l; simp
@[simp]
theorem getElem?_attachWith {xs : Array α} {i : Nat} {P : α Prop} {H : a xs, P a} :
(xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
getElem?_pmap ..
@[simp]
theorem getElem?_attach {xs : Array α} {i : Nat} :
xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => mem_of_getElem? a) :=
getElem?_attachWith
@[simp]
theorem getElem_attachWith {xs : Array α} {P : α Prop} {H : a xs, P a}
{i : Nat} (h : i < (xs.attachWith P H).size) :
(xs.attachWith P H)[i] = xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h)) :=
getElem_pmap ..
@[simp]
theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
xs.attach[i] = xs[i]'(by simpa using h), getElem_mem (by simpa using h) :=
getElem_attachWith h
theorem foldl_pmap (l : Array α) {P : α Prop} (f : (a : α) P a β)
(H : (a : α), a l P a) (g : γ β γ) (x : γ) :
(l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
rw [pmap_eq_map_attach, foldl_map]
theorem foldr_pmap (l : Array α) {P : α Prop} (f : (a : α) P a β)
(H : (a : α), a l P a) (g : β γ γ) (x : γ) :
(l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
rw [pmap_eq_map_attach, foldr_map]
/--
If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.
This is useful when we need to use `attach` to show termination.
Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldl_subtype` below.
-/
theorem foldl_attach (l : Array α) (f : β α β) (b : β) :
l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
rcases l with l
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
congr
ext
simpa using fun a => List.mem_of_getElem? a
/--
If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.
This is useful when we need to use `attach` to show termination.
Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldr_subtype` below.
-/
theorem foldr_attach (l : Array α) (f : α β β) (b : β) :
l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
rcases l with l
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
congr
ext
simpa using fun a => List.mem_of_getElem? a
theorem attach_map {l : Array α} (f : α β) :
(l.map f).attach = l.attach.map (fun x, h => f x, mem_map_of_mem f h) := by
cases l
ext <;> simp
theorem attachWith_map {l : Array α} (f : α β) {P : β Prop} {H : (b : β), b l.map f P b} :
(l.map f).attachWith P H = (l.attachWith (P f) (fun _ h => H _ (mem_map_of_mem f h))).map
fun x, h => f x, h := by
cases l
ext
· simp
· simp only [List.map_toArray, List.attachWith_toArray, List.getElem_toArray,
List.getElem_attachWith, List.getElem_map, Function.comp_apply]
erw [List.getElem_attachWith] -- Why is `erw` needed here?
theorem map_attachWith {l : Array α} {P : α Prop} {H : (a : α), a l P a}
(f : { x // P x } β) :
(l.attachWith P H).map f =
l.pmap (fun a (h : a l P a) => f a, H _ h.1) (fun a h => h, H a h) := by
cases l
ext <;> simp
/-- See also `pmap_eq_map_attach` for writing `pmap` in terms of `map` and `attach`. -/
theorem map_attach {l : Array α} (f : { x // x l } β) :
l.attach.map f = l.pmap (fun a h => f a, h) (fun _ => id) := by
cases l
ext <;> simp
theorem attach_filterMap {l : Array α} {f : α Option β} :
(l.filterMap f).attach = l.attach.filterMap
fun x, h => (f x).pbind (fun b m => some b, mem_filterMap.mpr x, h, m) := by
cases l
rw [attach_congr (List.filterMap_toArray f _)]
simp [List.attach_filterMap, List.map_filterMap, Function.comp_def]
theorem attach_filter {l : Array α} (p : α Bool) :
(l.filter p).attach = l.attach.filterMap
fun x => if w : p x.1 then some x.1, mem_filter.mpr x.2, w else none := by
cases l
rw [attach_congr (List.filter_toArray p _)]
simp [List.attach_filter, List.map_filterMap, Function.comp_def]
-- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
-- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
theorem pmap_pmap {p : α Prop} {q : β Prop} (g : a, p a β) (f : b, q b γ) (l H₁ H₂) :
pmap f (pmap g l H₁) H₂ =
pmap (α := { x // x l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
(fun a _ => H₁ a a.2) := by
cases l
simp [List.pmap_pmap, List.pmap_map]
@[simp] theorem pmap_append {p : ι Prop} (f : a : ι, p a α) (l₁ l₂ : Array ι)
(h : a l₁ ++ l₂, p a) :
(l₁ ++ l₂).pmap f h =
(l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
l₂.pmap f fun a ha => h a (mem_append_right l₁ ha) := by
cases l₁
cases l₂
simp
theorem pmap_append' {p : α Prop} (f : a : α, p a β) (l₁ l₂ : Array α)
(h₁ : a l₁, p a) (h₂ : a l₂, p a) :
((l₁ ++ l₂).pmap f fun a ha => (mem_append.1 ha).elim (h₁ a) (h₂ a)) =
l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
pmap_append f l₁ l₂ _
@[simp] theorem attach_append (xs ys : Array α) :
(xs ++ ys).attach = xs.attach.map (fun x, h => x, mem_append_left ys h) ++
ys.attach.map fun x, h => x, mem_append_right xs h := by
cases xs
cases ys
rw [attach_congr (List.append_toArray _ _)]
simp [List.attach_append, Function.comp_def]
@[simp] theorem attachWith_append {P : α Prop} {xs ys : Array α}
{H : (a : α), a xs ++ ys P a} :
(xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
simp [attachWith, attach_append, map_pmap, pmap_append]
@[simp] theorem pmap_reverse {P : α Prop} (f : (a : α) P a β) (xs : Array α)
(H : (a : α), a xs.reverse P a) :
xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
induction xs <;> simp_all
theorem reverse_pmap {P : α Prop} (f : (a : α) P a β) (xs : Array α)
(H : (a : α), a xs P a) :
(xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
rw [pmap_reverse]
@[simp] theorem attachWith_reverse {P : α Prop} {xs : Array α}
{H : (a : α), a xs.reverse P a} :
xs.reverse.attachWith P H =
(xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
cases xs
simp
theorem reverse_attachWith {P : α Prop} {xs : Array α}
{H : (a : α), a xs P a} :
(xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
cases xs
simp
@[simp] theorem attach_reverse (xs : Array α) :
xs.reverse.attach = xs.attach.reverse.map fun x, h => x, by simpa using h := by
cases xs
rw [attach_congr (List.reverse_toArray _)]
simp
theorem reverse_attach (xs : Array α) :
xs.attach.reverse = xs.reverse.attach.map fun x, h => x, by simpa using h := by
cases xs
simp
@[simp] theorem back?_pmap {P : α Prop} (f : (a : α) P a β) (xs : Array α)
(H : (a : α), a xs P a) :
(xs.pmap f H).back? = xs.attach.back?.map fun a, m => f a (H a m) := by
cases xs
simp
@[simp] theorem back?_attachWith {P : α Prop} {xs : Array α}
{H : (a : α), a xs P a} :
(xs.attachWith P H).back? = xs.back?.pbind (fun a h => some a, H _ (mem_of_back?_eq_some h)) := by
cases xs
simp
@[simp]
theorem back?_attach {xs : Array α} :
xs.attach.back? = xs.back?.pbind fun a h => some a, mem_of_back?_eq_some h := by
cases xs
simp
/-! ## unattach
`Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -479,7 +83,7 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
@[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
cases l
simp only [List.attach_toArray, List.unattach_toArray, List.unattach_attachWith]
simp
@[simp] theorem unattach_attachWith {p : α Prop} {l : Array α}
{H : a l, p a} :
@@ -487,15 +91,6 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
cases l
simp
@[simp] theorem getElem?_unattach {p : α Prop} {l : Array { x // p x }} (i : Nat) :
l.unattach[i]? = l[i]?.map Subtype.val := by
simp [unattach]
@[simp] theorem getElem_unattach
{p : α Prop} {l : Array { x // p x }} (i : Nat) (h : i < l.unattach.size) :
l.unattach[i] = (l[i]'(by simpa using h)).1 := by
simp [unattach]
/-! ### Recognizing higher order functions using a function that only depends on the value. -/
/--

View File

@@ -247,7 +247,7 @@ def get? (a : Array α) (i : Nat) : Option α :=
if h : i < a.size then some a[i] else none
def back? (a : Array α) : Option α :=
a[a.size - 1]?
a.get? (a.size - 1)
@[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
let e := a[i]
@@ -442,8 +442,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
decreasing_by simp_wf; decreasing_trivial_pre_omega
map 0 (mkEmpty as.size)
@[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
/-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
@[inline]
def mapFinIdxM {α : Type u} {β : Type v} {m : Type v Type w} [Monad m]
@@ -613,15 +611,8 @@ def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
decreasing_by simp_wf; decreasing_trivial_pre_omega
loop 0
@[inline]
def findFinIdx? {α : Type u} (p : α Bool) (as : Array α) : Option (Fin as.size) :=
let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
loop (j : Nat) :=
if h : j < as.size then
if p as[j] then some j, h else loop (j + 1)
else none
decreasing_by simp_wf; decreasing_trivial_pre_omega
loop 0
def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
a.findIdx? fun a => a == v
@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
@@ -634,10 +625,6 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
indexOfAux a v 0
@[deprecated indexOf? (since := "2024-11-20")]
def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
a.findIdx? fun a => a == v
@[inline]
def any (as : Array α) (p : α Bool) (start := 0) (stop := as.size) : Bool :=
Id.run <| as.anyM p start stop
@@ -777,62 +764,48 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
decreasing_by simp_wf; decreasing_trivial_pre_omega
go 0 #[]
/--
Remove the element at a given index from an array without a runtime bounds checks,
using a `Nat` index and a tactic-provided bound.
/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
This function takes worst case O(n) time because
it has to backshift all elements at positions greater than `i`.-/
This function takes worst case O(n) time because
it has to backshift all elements at positions greater than `i`.-/
@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
def eraseIdx (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
if h' : i + 1 < a.size then
let a' := a.swap i + 1, h' i, h
a'.eraseIdx (i + 1) (by simp [a', h'])
def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
if h : i.val + 1 < a.size then
let a' := a.swap i.val + 1, h i
let i' : Fin a'.size := i.val + 1, by simp [a', h]
a'.feraseIdx i'
else
a.pop
termination_by a.size - i
decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
termination_by a.size - i.val
decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
-- This is required in `Lean.Data.PersistentHashMap`.
@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) (h) : (a.eraseIdx i h).size = a.size - 1 := by
induction a, i, h using Array.eraseIdx.induct with
| @case1 a i h h' a' ih =>
unfold eraseIdx
simp [h', a', ih]
| case2 a i h h' =>
unfold eraseIdx
simp [h']
@[simp] theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
induction a, i using Array.feraseIdx.induct with
| @case1 a i h a' _ ih =>
unfold feraseIdx
simp [h, a', ih]
| case2 a i h =>
unfold feraseIdx
simp [h]
/-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
This function takes worst case O(n) time because
it has to backshift all elements at positions greater than `i`.-/
def eraseIdxIfInBounds (a : Array α) (i : Nat) : Array α :=
if h : i < a.size then a.eraseIdx i h else a
/-- Remove the element at a given index from an array, or panic if the index is out of bounds.
This function takes worst case O(n) time because
it has to backshift all elements at positions greater than `i`. -/
def eraseIdx! (a : Array α) (i : Nat) : Array α :=
if h : i < a.size then a.eraseIdx i h else panic! "invalid index"
def eraseIdx (a : Array α) (i : Nat) : Array α :=
if h : i < a.size then a.feraseIdx i, h else a
def erase [BEq α] (as : Array α) (a : α) : Array α :=
match as.indexOf? a with
| none => as
| some i => as.eraseIdx i
/-- Erase the first element that satisfies the predicate `p`. -/
def eraseP (as : Array α) (p : α Bool) : Array α :=
match as.findIdx? p with
| none => as
| some i => as.eraseIdxIfInBounds i
| some i => as.feraseIdx i
/-- Insert element `a` at position `i`. -/
@[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i as.size := by get_elem_tactic) : Array α :=
@[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
loop (as : Array α) (j : Fin as.size) :=
if i < j then
if i.1 < j then
let j' := j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2
let as := as.swap j' j
loop as j', by rw [size_swap]; exact j'.2
@@ -843,23 +816,12 @@ def eraseP (as : Array α) (p : α → Bool) : Array α :=
let as := as.push a
loop as j, size_push .. j.lt_succ_self
@[deprecated insertIdx (since := "2024-11-20")] abbrev insertAt := @insertIdx
/-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/
def insertIdx! (as : Array α) (i : Nat) (a : α) : Array α :=
def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
if h : i as.size then
insertIdx as i a
insertAt as i, Nat.lt_succ_of_le h a
else panic! "invalid index"
@[deprecated insertIdx! (since := "2024-11-20")] abbrev insertAt! := @insertIdx!
/-- Insert element `a` at position `i`, or do nothing if `as.size < i`. -/
def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
if h : i as.size then
insertIdx as i a
else
as
@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size bs.size) (i : Nat) : Bool :=
if h : i < as.size then

View File

@@ -52,7 +52,7 @@ namespace Array
let mid := (lo + hi)/2
let midVal := as.get! mid
if lt midVal k then
if mid == lo then do let v add (); pure <| as.insertIdx! (lo+1) v
if mid == lo then do let v add (); pure <| as.insertAt! (lo+1) v
else binInsertAux lt merge add as k mid hi
else if lt k midVal then
binInsertAux lt merge add as k lo mid
@@ -67,7 +67,7 @@ namespace Array
(k : α) : m (Array α) :=
let _ := Inhabited.mk k
if as.isEmpty then do let v add (); pure <| as.push v
else if lt k (as.get! 0) then do let v add (); pure <| as.insertIdx! 0 v
else if lt k (as.get! 0) then do let v add (); pure <| as.insertAt! 0 v
else if !lt (as.get! 0) k then as.modifyM 0 <| merge
else if lt as.back! k then do let v add (); pure <| as.push v
else if !lt k as.back! then as.modifyM (as.size - 1) <| merge

View File

@@ -15,26 +15,26 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
namespace Array
theorem foldlM_toList.aux [Monad m]
theorem foldlM_eq_foldlM_toList.aux [Monad m]
(f : β α m β) (arr : Array α) (i j) (H : arr.size i + j) (b) :
foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
unfold foldlM.loop
split; split
· cases Nat.not_le_of_gt _ (Nat.zero_add _ H)
· rename_i i; rw [Nat.succ_add] at H
simp [foldlM_toList.aux f arr i (j+1) H]
simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
rw (occs := .pos [2]) [ List.getElem_cons_drop_succ_eq_drop _]
rfl
· rw [List.drop_of_length_le (Nat.ge_of_not_lt _)]; rfl
@[simp] theorem foldlM_toList [Monad m]
theorem foldlM_eq_foldlM_toList [Monad m]
(f : β α m β) (init : β) (arr : Array α) :
arr.toList.foldlM f init = arr.foldlM f init := by
simp [foldlM, foldlM_toList.aux]
arr.foldlM f init = arr.toList.foldlM f init := by
simp [foldlM, foldlM_eq_foldlM_toList.aux]
@[simp] theorem foldl_toList (f : β α β) (init : β) (arr : Array α) :
arr.toList.foldl f init = arr.foldl f init :=
List.foldl_eq_foldlM .. foldlM_toList ..
theorem foldl_eq_foldl_toList (f : β α β) (init : β) (arr : Array α) :
arr.foldl f init = arr.toList.foldl f init :=
List.foldl_eq_foldlM .. foldlM_eq_foldlM_toList ..
theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
(f : α β m β) (arr : Array α) (init : β) (i h) :
@@ -51,23 +51,23 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
simp [foldrM, h, foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
@[simp] theorem foldrM_toList [Monad m]
theorem foldrM_eq_foldrM_toList [Monad m]
(f : α β m β) (init : β) (arr : Array α) :
arr.toList.foldrM f init = arr.foldrM f init := by
arr.foldrM f init = arr.toList.foldrM f init := by
rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
@[simp] theorem foldr_toList (f : α β β) (init : β) (arr : Array α) :
arr.toList.foldr f init = arr.foldr f init :=
List.foldr_eq_foldrM .. foldrM_toList ..
theorem foldr_eq_foldr_toList (f : α β β) (init : β) (arr : Array α) :
arr.foldr f init = arr.toList.foldr f init :=
List.foldr_eq_foldrM .. foldrM_eq_foldrM_toList ..
@[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
simp [push, List.concat_eq_append]
@[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
simp [toListAppend, foldr_toList]
simp [toListAppend, foldr_eq_foldr_toList]
@[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
simp [toListImpl, foldr_toList]
simp [toListImpl, foldr_eq_foldr_toList]
@[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
@@ -76,7 +76,7 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
@[simp] theorem toList_append (arr arr' : Array α) :
(arr ++ arr').toList = arr.toList ++ arr'.toList := by
rw [ append_eq_append]; unfold Array.append
rw [ foldl_toList]
rw [foldl_eq_foldl_toList]
induction arr'.toList generalizing arr <;> simp [*]
@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
@@ -98,44 +98,20 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
rw [ appendList_eq_append]; unfold Array.appendList
induction l generalizing arr <;> simp [*]
@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
theorem foldrM_eq_foldrM_toList [Monad m]
(f : α β m β) (init : β) (arr : Array α) :
arr.foldrM f init = arr.toList.foldrM f init := by
simp
@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]
theorem foldlM_eq_foldlM_toList [Monad m]
(f : β α m β) (init : β) (arr : Array α) :
arr.foldlM f init = arr.toList.foldlM f init:= by
simp
@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]
theorem foldr_eq_foldr_toList
(f : α β β) (init : β) (arr : Array α) :
arr.foldr f init = arr.toList.foldr f init := by
simp
@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]
theorem foldl_eq_foldl_toList
(f : β α β) (init : β) (arr : Array α) :
arr.foldl f init = arr.toList.foldl f init:= by
simp
@[deprecated foldlM_toList (since := "2024-09-09")]
abbrev foldlM_eq_foldlM_data := @foldlM_toList
@[deprecated foldl_toList (since := "2024-09-09")]
abbrev foldl_eq_foldl_data := @foldl_toList
@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
@[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
@[deprecated foldrM_toList (since := "2024-09-09")]
abbrev foldrM_eq_foldrM_data := @foldrM_toList
@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
@[deprecated foldr_toList (since := "2024-09-09")]
abbrev foldr_eq_foldr_data := @foldr_toList
@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
@[deprecated push_toList (since := "2024-09-09")]
abbrev push_data := @push_toList

View File

@@ -1,281 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Init.Data.List.Find
import Init.Data.Array.Lemmas
import Init.Data.Array.Attach
/-!
# Lemmas about `Array.findSome?`, `Array.find?`.
-/
namespace Array
open Nat
/-! ### findSome? -/
@[simp] theorem findSomeRev?_push_of_isSome (l : Array α) (h : (f a).isSome) : (l.push a).findSomeRev? f = f a := by
cases l; simp_all
@[simp] theorem findSomeRev?_push_of_isNone (l : Array α) (h : (f a).isNone) : (l.push a).findSomeRev? f = l.findSomeRev? f := by
cases l; simp_all
theorem exists_of_findSome?_eq_some {f : α Option β} {l : Array α} (w : l.findSome? f = some b) :
a, a l f a = b := by
cases l; simp_all [List.exists_of_findSome?_eq_some]
@[simp] theorem findSome?_eq_none_iff : findSome? p l = none x l, p x = none := by
cases l; simp
@[simp] theorem findSome?_isSome_iff {f : α Option β} {l : Array α} :
(l.findSome? f).isSome x, x l (f x).isSome := by
cases l; simp
theorem findSome?_eq_some_iff {f : α Option β} {l : Array α} {b : β} :
l.findSome? f = some b (l₁ : Array α) (a : α) (l₂ : Array α), l = l₁.push a ++ l₂ f a = some b x l₁, f x = none := by
cases l
simp only [List.findSome?_toArray, List.findSome?_eq_some_iff]
constructor
· rintro l₁, a, l₂, rfl, h₁, h₂
exact l₁.toArray, a, l₂.toArray, by simp_all
· rintro l₁, a, l₂, h₀, h₁, h₂
exact l₁.toList, a, l₂.toList, by simpa using congrArg toList h₀, h₁, by simpa
@[simp] theorem findSome?_guard (l : Array α) : findSome? (Option.guard fun x => p x) l = find? p l := by
cases l; simp
@[simp] theorem getElem?_zero_filterMap (f : α Option β) (l : Array α) : (l.filterMap f)[0]? = l.findSome? f := by
cases l; simp [ List.head?_eq_getElem?]
@[simp] theorem getElem_zero_filterMap (f : α Option β) (l : Array α) (h) :
(l.filterMap f)[0] = (l.findSome? f).get (by cases l; simpa [List.length_filterMap_eq_countP] using h) := by
cases l; simp [ List.head_eq_getElem, getElem?_zero_filterMap]
@[simp] theorem back?_filterMap (f : α Option β) (l : Array α) : (l.filterMap f).back? = l.findSomeRev? f := by
cases l; simp
@[simp] theorem back!_filterMap [Inhabited β] (f : α Option β) (l : Array α) :
(l.filterMap f).back! = (l.findSomeRev? f).getD default := by
cases l; simp
@[simp] theorem map_findSome? (f : α Option β) (g : β γ) (l : Array α) :
(l.findSome? f).map g = l.findSome? (Option.map g f) := by
cases l; simp
theorem findSome?_map (f : β γ) (l : Array β) : findSome? p (l.map f) = l.findSome? (p f) := by
cases l; simp [List.findSome?_map]
theorem findSome?_append {l₁ l₂ : Array α} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f) := by
cases l₁; cases l₂; simp [List.findSome?_append]
theorem getElem?_zero_flatten (L : Array (Array α)) :
(flatten L)[0]? = L.findSome? fun l => l[0]? := by
cases L using array_array_induction
simp [ List.head?_eq_getElem?, List.head?_flatten, List.findSome?_map, Function.comp_def]
theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.size) :
(L.findSome? fun l => l[0]?).isSome := by
cases L using array_array_induction
simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
List.findSome?_isSome_iff, List.isSome_getElem?]
simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
Nat.sum_pos_iff_exists_pos, List.mem_map] at h
obtain _, xs, m, rfl, h := h
exact xs, m, by simpa using h
theorem getElem_zero_flatten {L : Array (Array α)} (h) :
(flatten L)[0] = (L.findSome? fun l => l[0]?).get (getElem_zero_flatten.proof h) := by
have t := getElem?_zero_flatten L
simp [getElem?_eq_getElem, h] at t
simp [ t]
theorem back?_flatten {L : Array (Array α)} :
(flatten L).back? = (L.findSomeRev? fun l => l.back?) := by
cases L using array_array_induction
simp [List.getLast?_flatten, List.map_reverse, List.findSome?_map, Function.comp_def]
theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
simp [mkArray_eq_toArray_replicate, List.findSome?_replicate]
@[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by
simp [findSome?_mkArray, Nat.ne_of_gt h]
-- Argument is unused, but used to decide whether `simp` should unfold.
@[simp] theorem findSome?_mkArray_of_isSome (_ : (f a).isSome) :
findSome? f (mkArray n a) = if n = 0 then none else f a := by
simp [findSome?_mkArray]
@[simp] theorem findSome?_mkArray_of_isNone (h : (f a).isNone) :
findSome? f (mkArray n a) = none := by
rw [Option.isNone_iff_eq_none] at h
simp [findSome?_mkArray, h]
/-! ### find? -/
@[simp] theorem find?_singleton (a : α) (p : α Bool) :
#[a].find? p = if p a then some a else none := by
simp [singleton_eq_toArray_singleton]
@[simp] theorem findRev?_push_of_pos (l : Array α) (h : p a) :
findRev? p (l.push a) = some a := by
cases l; simp [h]
@[simp] theorem findRev?_cons_of_neg (l : Array α) (h : ¬p a) :
findRev? p (l.push a) = findRev? p l := by
cases l; simp [h]
@[simp] theorem find?_eq_none : find? p l = none x l, ¬ p x := by
cases l; simp
theorem find?_eq_some_iff_append {xs : Array α} :
xs.find? p = some b p b (as bs : Array α), xs = as.push b ++ bs a as, !p a := by
rcases xs with xs
simp only [List.find?_toArray, List.find?_eq_some_iff_append, Bool.not_eq_eq_eq_not,
Bool.not_true, exists_and_right, and_congr_right_iff]
intro w
constructor
· rintro as, x, rfl, h
exact as.toArray, x.toArray, by simp , by simpa using h
· rintro as, x, h', h
exact as.toList, x.toList, by simpa using congrArg Array.toList h',
by simpa using h
@[simp]
theorem find?_push_eq_some {xs : Array α} :
(xs.push a).find? p = some b xs.find? p = some b (xs.find? p = none (p a a = b)) := by
cases xs; simp
@[simp] theorem find?_isSome {xs : Array α} {p : α Bool} : (xs.find? p).isSome x, x xs p x := by
cases xs; simp
theorem find?_some {xs : Array α} (h : find? p xs = some a) : p a := by
cases xs
simp at h
exact List.find?_some h
theorem mem_of_find?_eq_some {xs : Array α} (h : find? p xs = some a) : a xs := by
cases xs
simp at h
simpa using List.mem_of_find?_eq_some h
theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h xs := by
cases xs
simp [List.get_find?_mem]
@[simp] theorem find?_filter {xs : Array α} (p q : α Bool) :
(xs.filter p).find? q = xs.find? (fun a => p a q a) := by
cases xs; simp
@[simp] theorem getElem?_zero_filter (p : α Bool) (l : Array α) :
(l.filter p)[0]? = l.find? p := by
cases l; simp [ List.head?_eq_getElem?]
@[simp] theorem getElem_zero_filter (p : α Bool) (l : Array α) (h) :
(l.filter p)[0] =
(l.find? p).get (by cases l; simpa [ List.countP_eq_length_filter] using h) := by
cases l
simp [List.getElem_zero_eq_head]
@[simp] theorem back?_filter (p : α Bool) (l : Array α) : (l.filter p).back? = l.findRev? p := by
cases l; simp
@[simp] theorem back!_filter [Inhabited α] (p : α Bool) (l : Array α) :
(l.filter p).back! = (l.findRev? p).get! := by
cases l; simp [Option.get!_eq_getD]
@[simp] theorem find?_filterMap (xs : Array α) (f : α Option β) (p : β Bool) :
(xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by
cases xs; simp
@[simp] theorem find?_map (f : β α) (xs : Array β) :
find? p (xs.map f) = (xs.find? (p f)).map f := by
cases xs; simp
@[simp] theorem find?_append {l₁ l₂ : Array α} :
(l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
cases l₁
cases l₂
simp
@[simp] theorem find?_flatten (xs : Array (Array α)) (p : α Bool) :
xs.flatten.find? p = xs.findSome? (·.find? p) := by
cases xs using array_array_induction
simp [List.findSome?_map, Function.comp_def]
theorem find?_flatten_eq_none {xs : Array (Array α)} {p : α Bool} :
xs.flatten.find? p = none ys xs, x ys, !p x := by
simp
/--
If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
Moreover, no earlier array in `xs` has an element satisfying `p`.
-/
theorem find?_flatten_eq_some {xs : Array (Array α)} {p : α Bool} {a : α} :
xs.flatten.find? p = some a
p a (as : Array (Array α)) (ys zs : Array α) (bs : Array (Array α)),
xs = as.push (ys.push a ++ zs) ++ bs
( a as, x a, !p x) ( x ys, !p x) := by
cases xs using array_array_induction
simp only [flatten_toArray_map_toArray, List.find?_toArray, List.find?_flatten_eq_some]
simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
intro w
constructor
· rintro as, ys, zs, bs, rfl, h₁, h₂
exact as.toArray.map List.toArray, ys.toArray,
zs.toArray, bs.toArray.map List.toArray, by simp, by simpa using h₁, by simpa using h₂
· rintro as, ys, zs, bs, h, h₁, h₂
replace h := congrArg (·.map Array.toList) (congrArg Array.toList h)
simp [Function.comp_def] at h
exact as.toList.map Array.toList, ys.toList,
zs.toList, bs.toList.map Array.toList, by simpa using h,
by simpa using h₁, by simpa using h₂
@[simp] theorem find?_flatMap (xs : Array α) (f : α Array β) (p : β Bool) :
(xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
cases xs
simp [List.find?_flatMap, Array.flatMap_toArray]
theorem find?_flatMap_eq_none {xs : Array α} {f : α Array β} {p : β Bool} :
(xs.flatMap f).find? p = none x xs, y f x, !p y := by
simp
theorem find?_mkArray :
find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
simp [mkArray_eq_toArray_replicate, List.find?_replicate]
@[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) :
find? p (mkArray n a) = if p a then some a else none := by
simp [find?_mkArray, Nat.ne_of_gt h]
@[simp] theorem find?_mkArray_of_pos (h : p a) :
find? p (mkArray n a) = if n = 0 then none else some a := by
simp [find?_mkArray, h]
@[simp] theorem find?_mkArray_of_neg (h : ¬ p a) : find? p (mkArray n a) = none := by
simp [find?_mkArray, h]
-- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α Bool} :
(mkArray n a).find? p = none n = 0 !p a := by
simp [mkArray_eq_toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
@[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α Bool} :
(mkArray n a).find? p = some b n 0 p a a = b := by
simp [mkArray_eq_toArray_replicate]
@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α Bool) (h) :
((mkArray n a).find? p).get h = a := by
simp [mkArray_eq_toArray_replicate]
theorem find?_pmap {P : α Prop} (f : (a : α) P a β) (xs : Array α)
(H : (a : α), a xs P a) (p : β Bool) :
(xs.pmap f H).find? p = (xs.attach.find? (fun a, m => p (f a (H a m)))).map fun a, m => f a (H a m) := by
simp only [pmap_eq_map_attach, find?_map]
rfl
end Array

View File

@@ -23,9 +23,6 @@ import Init.TacticsExtra
namespace Array
@[simp] theorem mem_toArray {a : α} {l : List α} : a l.toArray a l := by
simp [mem_def]
@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := rfl
@@ -39,21 +36,12 @@ theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? =
· rw [getElem?_neg a i h]
simp_all
@[simp] theorem none_eq_getElem?_iff {a : Array α} {i : Nat} : none = a[i]? a.size i := by
simp [eq_comm (a := none)]
theorem getElem?_eq {a : Array α} {i : Nat} :
a[i]? = if h : i < a.size then some a[i] else none := by
split
· simp_all [getElem?_eq_getElem]
· simp_all
theorem getElem?_eq_some_iff {a : Array α} : a[i]? = some b h : i < a.size, a[i] = b := by
simp [getElem?_eq]
theorem some_eq_getElem?_iff {a : Array α} : some b = a[i]? h : i < a.size, a[i] = b := by
rw [eq_comm, getElem?_eq_some_iff]
theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[i]? := by
rw [getElem?_eq]
split <;> simp_all
@@ -78,35 +66,6 @@ theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size)
@[deprecated getElem_push_lt (since := "2024-10-21")] abbrev get_push_lt := @getElem_push_lt
@[deprecated getElem_push_eq (since := "2024-10-21")] abbrev get_push_eq := @getElem_push_eq
@[simp] theorem mem_push {a : Array α} {x y : α} : x a.push y x a x = y := by
simp [mem_def]
theorem mem_push_self {a : Array α} {x : α} : x a.push x :=
mem_push.2 (Or.inr rfl)
theorem mem_push_of_mem {a : Array α} {x : α} (y : α) (h : x a) : x a.push y :=
mem_push.2 (Or.inl h)
theorem getElem_of_mem {a} {l : Array α} (h : a l) : (n : Nat) (h : n < l.size), l[n]'h = a := by
cases l
simp [List.getElem_of_mem (by simpa using h)]
theorem getElem?_of_mem {a} {l : Array α} (h : a l) : n : Nat, l[n]? = some a :=
let n, _, e := getElem_of_mem h; n, e getElem?_eq_getElem _
theorem mem_of_getElem? {l : Array α} {n : Nat} {a : α} (e : l[n]? = some a) : a l :=
let _, e := getElem?_eq_some_iff.1 e; e getElem_mem ..
theorem mem_iff_getElem {a} {l : Array α} : a l (n : Nat) (h : n < l.size), l[n]'h = a :=
getElem_of_mem, fun _, _, e => e getElem_mem ..
theorem mem_iff_getElem? {a} {l : Array α} : a l n : Nat, l[n]? = some a := by
simp [getElem?_eq_some_iff, mem_iff_getElem]
theorem forall_getElem {l : Array α} {p : α Prop} :
( (n : Nat) h, p (l[n]'h)) a, a l p a := by
cases l; simp [List.forall_getElem]
@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
simp [getElem!_def, get!, getD]
split <;> rename_i h
@@ -117,8 +76,6 @@ theorem forall_getElem {l : Array α} {p : α → Prop} :
theorem singleton_inj : #[a] = #[b] a = b := by
simp
theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
end Array
namespace List
@@ -134,6 +91,9 @@ We prefer to pull `List.toArray` outwards.
(a.toArrayAux b).size = b.size + a.length := by
simp [size]
@[simp] theorem mem_toArray {a : α} {l : List α} : a l.toArray a l := by
simp [mem_def]
@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
apply ext'
simp
@@ -151,9 +111,6 @@ We prefer to pull `List.toArray` outwards.
@[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!]
@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
simp [back?, List.getLast?_eq_getElem?]
@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) a l.toArray β m (ForInStep β)) (i : Nat)
(h : i l.length) (b : β) :
Array.forIn'.loop l.toArray f i h b =
@@ -189,15 +146,15 @@ theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List
theorem foldlM_toArray [Monad m] (f : β α m β) (init : β) (l : List α) :
l.toArray.foldlM f init = l.foldlM f init := by
rw [foldlM_toList]
rw [foldlM_eq_foldlM_toList]
theorem foldr_toArray (f : α β β) (init : β) (l : List α) :
l.toArray.foldr f init = l.foldr f init := by
rw [foldr_toList]
rw [foldr_eq_foldr_toList]
theorem foldl_toArray (f : β α β) (init : β) (l : List α) :
l.toArray.foldl f init = l.foldl f init := by
rw [foldl_toList]
rw [foldl_eq_foldl_toList]
/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
@[simp] theorem foldrM_toArray' [Monad m] (f : α β m β) (init : β) (l : List α)
@@ -212,21 +169,21 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
(h : stop = l.toArray.size) :
l.toArray.foldlM f init 0 stop = l.foldlM f init := by
subst h
rw [foldlM_toList]
rw [foldlM_eq_foldlM_toList]
/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
@[simp] theorem foldr_toArray' (f : α β β) (init : β) (l : List α)
(h : start = l.toArray.size) :
l.toArray.foldr f init start 0 = l.foldr f init := by
subst h
rw [foldr_toList]
rw [foldr_eq_foldr_toList]
/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
@[simp] theorem foldl_toArray' (f : β α β) (init : β) (l : List α)
(h : stop = l.toArray.size) :
l.toArray.foldl f init 0 stop = l.foldl f init := by
subst h
rw [foldl_toList]
rw [foldl_eq_foldl_toList]
@[simp] theorem append_toArray (l₁ l₂ : List α) :
l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
@@ -240,9 +197,6 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
induction l generalizing as <;> simp [*]
@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
rw [foldr_eq_foldl_reverse, foldl_push]
@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α m (Option β)) (l : List α) :
l.toArray.findSomeM? f = l.findSomeM? f := by
rw [Array.findSomeM?]
@@ -403,8 +357,7 @@ namespace Array
theorem foldrM_push [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
simp [foldrM_eq_reverse_foldlM_toList, -size_push]
/--
Variant of `foldrM_push` with `h : start = arr.size + 1`
@@ -430,11 +383,11 @@ rather than `(arr.push a).size` as the argument.
@[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
@[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
rw [toListRev, foldl_toList, List.foldr_reverse, List.foldr_cons_nil]
rw [toListRev, foldl_eq_foldl_toList, List.foldr_reverse, List.foldr_cons_nil]
theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
rw [mapM, aux, foldlM_toList]; rfl
rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
where
aux (i r) :
mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
@@ -449,7 +402,7 @@ where
@[simp] theorem toList_map (f : α β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
rw [map, mapM_eq_foldlM]
apply congrArg toList (foldl_toList (fun bs a => push bs (f a)) #[] arr).symm |>.trans
apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = arr.toList ++ l.map f := by
induction l generalizing arr <;> simp [*]
simp [H]
@@ -621,15 +574,13 @@ theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
(ofFn f)[i]? = if h : i < n then some (f i, h) else none := by
simp [getElem?_def]
/-! # mkArray -/
/-- # mkArray -/
@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
List.length_replicate ..
@[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
theorem mkArray_eq_toArray_replicate (n : Nat) (v : α) : mkArray n v = (List.replicate n v).toArray := rfl
@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
(mkArray n v)[i] = v := by simp [Array.getElem_eq_getElem_toList]
@@ -637,29 +588,42 @@ theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
(mkArray n v)[i]? = if i < n then some v else none := by
simp [getElem?_def]
/-! # mem -/
/-- # mem -/
@[simp] theorem mem_toList {a : α} {l : Array α} : a l.toList a l := mem_def.symm
theorem mem_toList {a : α} {l : Array α} : a l.toList a l := mem_def.symm
theorem not_mem_nil (a : α) : ¬ a #[] := nofun
theorem getElem_of_mem {a : α} {as : Array α} :
a as ( (n : Nat) (h : n < as.size), as[n]'h = a) := by
intro ha
rcases List.getElem_of_mem ha.val with i, hbound, hi
exists i
exists hbound
theorem getElem?_of_mem {a : α} {as : Array α} :
a as (n : Nat), as[n]? = some a := by
intro ha
rcases List.getElem?_of_mem ha.val with i, hi
exists i
@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p Array α} :
(x if h : p then #[] else l h) h : ¬ p, x l h := by
split <;> simp_all
split <;> simp_all [mem_def]
@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p Array α} :
(x if h : p then l h else #[]) h : p, x l h := by
split <;> simp_all
split <;> simp_all [mem_def]
@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
(x if p then #[] else l) ¬ p x l := by
split <;> simp_all
split <;> simp_all [mem_def]
@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
(x if p then l else #[]) p x l := by
split <;> simp_all
split <;> simp_all [mem_def]
/-! # get lemmas -/
/-- # get lemmas -/
theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) :
idx < a.size :=
@@ -684,6 +648,10 @@ theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get?
theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
simp only [get!_eq_getElem?, get?_eq_getElem?]
theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a h : n < as.size, as[n] = a := by
cases as
simp [List.getElem?_eq_some_iff]
theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD default := by
simp only [back!, get!_eq_getElem?, get?_eq_getElem?, back?]
@@ -693,10 +661,6 @@ theorem back!_eq_back? [Inhabited α] (a : Array α) : a.back! = a.back?.getD de
@[simp] theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x := by
simp [back!_eq_back?]
theorem mem_of_back?_eq_some {xs : Array α} {a : α} (h : xs.back? = some a) : a xs := by
cases xs
simpa using List.mem_of_getLast?_eq_some (by simpa using h)
theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
(a.push x)[i]? = some a[i] := by
rw [getElem?_pos, getElem_push_lt]
@@ -1050,13 +1014,9 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
@[simp] theorem mem_map {f : α β} {l : Array α} : b l.map f a, a l f a = b := by
simp only [mem_def, toList_map, List.mem_map]
theorem exists_of_mem_map (h : b map f l) : a, a l f a = b := mem_map.1 h
theorem mem_map_of_mem (f : α β) (h : a l) : f a map f l := mem_map.2 _, h, rfl
theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α m β) (arr : Array α) :
arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
rw [mapM_eq_foldlM, foldlM_toList, List.foldrM_reverse]
rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, List.foldrM_reverse]
conv => rhs; rw [ List.reverse_reverse arr.toList]
induction arr.toList.reverse with
| nil => simp
@@ -1181,7 +1141,7 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : αα} {j : Nat} :
@[simp] theorem toList_filter (p : α Bool) (l : Array α) :
(l.filter p).toList = l.toList.filter p := by
dsimp only [filter]
rw [ foldl_toList]
rw [foldl_eq_foldl_toList]
generalize l.toList = l
suffices a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
a.toList ++ List.filter p l by
@@ -1212,7 +1172,7 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
@[simp] theorem toList_filterMap (f : α Option β) (l : Array α) :
(l.filterMap f).toList = l.toList.filterMap f := by
dsimp only [filterMap, filterMapM]
rw [ foldlM_toList]
rw [foldlM_eq_foldlM_toList]
generalize l.toList = l
have this : a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
a.toList ++ List.filterMap f l := ?_
@@ -1244,23 +1204,9 @@ theorem push_eq_append_singleton (as : Array α) (x) : as.push x = as ++ #[x] :=
@[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]
@[simp] theorem empty_append (as : Array α) : #[] ++ as = as := by
cases as
simp
@[simp] theorem append_empty (as : Array α) : as ++ #[] = as := by
cases as
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
@@ -1305,7 +1251,7 @@ theorem getElem?_append {as bs : Array α} {n : Nat} :
@[simp] theorem toList_flatten {l : Array (Array α)} :
l.flatten.toList = (l.toList.map toList).flatten := by
dsimp [flatten]
simp only [ foldl_toList]
simp only [foldl_eq_foldl_toList]
generalize l.toList = l
have : a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
exact this #[]
@@ -1637,9 +1583,9 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
/-! ### eraseIdx -/
theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) :
a.eraseIdx i h = a.eraseIdxIfInBounds i := by
simp [eraseIdxIfInBounds, h]
theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
a.feraseIdx i = a.eraseIdx i.1 := by
simp [eraseIdx]
/-! ### isPrefixOf -/
@@ -1869,15 +1815,16 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
l.toArray.takeWhile p = (l.takeWhile p).toArray := by
simp [Array.takeWhile, takeWhile_go_toArray]
@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
rw [Array.eraseIdx]
split <;> rename_i h'
· rw [eraseIdx_toArray]
@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
rw [feraseIdx]
split <;> rename_i h
· rw [feraseIdx_toArray]
simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
simp
· simp at h h'
· rcases i with i, w
simp at h w
have t : i = l.length - 1 := by omega
simp [t]
termination_by l.length - i
@@ -1887,9 +1834,9 @@ decreasing_by
simp
omega
@[simp] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray := by
rw [Array.eraseIdxIfInBounds]
@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
rw [Array.eraseIdx]
split
· simp
· simp_all [eraseIdx_eq_self.2]
@@ -1908,86 +1855,16 @@ namespace Array
(as.takeWhile p).toList = as.toList.takeWhile p := by
induction as; simp
@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) (h : i < as.size) :
(as.eraseIdx i h).toList = as.toList.eraseIdx i := by
@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
(as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
induction as
simp
@[simp] theorem toList_eraseIdxIfInBounds (as : Array α) (i : Nat) :
(as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i := by
@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
(as.eraseIdx i).toList = as.toList.eraseIdx i := by
induction as
simp
/-! ### map -/
@[simp] theorem map_map {f : α β} {g : β γ} {as : Array α} :
(as.map f).map g = as.map (g f) := by
cases as; simp
@[simp] theorem map_id_fun : map (id : α α) = id := by
funext l
induction l <;> simp_all
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`. -/
@[simp] theorem map_id_fun' : map (fun (a : α) => a) = id := map_id_fun
-- This is not a `@[simp]` lemma because `map_id_fun` will apply.
theorem map_id (as : Array α) : map (id : α α) as = as := by
cases as <;> simp_all
/-- `map_id'` differs from `map_id` by representing the identity function as a lambda, rather than `id`. -/
-- This is not a `@[simp]` lemma because `map_id_fun'` will apply.
theorem map_id' (as : Array α) : map (fun (a : α) => a) as = as := map_id as
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity. -/
theorem map_id'' {f : α α} (h : x, f x = x) (as : Array α) : map f as = as := by
simp [show f = id from funext h]
theorem array_array_induction (P : Array (Array α) Prop) (h : (xss : List (List α)), P (xss.map List.toArray).toArray)
(ass : Array (Array α)) : P ass := by
specialize h (ass.toList.map toList)
simpa [ toList_map, Function.comp_def, map_id] using h
theorem foldl_map (f : β₁ β₂) (g : α β₂ α) (l : Array β₁) (init : α) :
(l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
cases l; simp [List.foldl_map]
theorem foldr_map (f : α₁ α₂) (g : α₂ β β) (l : Array α₁) (init : β) :
(l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
cases l; simp [List.foldr_map]
theorem foldl_filterMap (f : α Option β) (g : γ β γ) (l : Array α) (init : γ) :
(l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
cases l
simp [List.foldl_filterMap]
rfl
theorem foldr_filterMap (f : α Option β) (g : β γ γ) (l : Array α) (init : γ) :
(l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
cases l
simp [List.foldr_filterMap]
rfl
/-! ### flatten -/
@[simp] theorem flatten_empty : flatten (#[] : Array (Array α)) = #[] := rfl
@[simp] theorem flatten_toArray_map_toArray (xss : List (List α)) :
(xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
simp [flatten]
suffices as, List.foldl (fun r a => r ++ a) as (List.map List.toArray xss) = as ++ xss.flatten.toArray by
simpa using this #[]
intro as
induction xss generalizing as with
| nil => simp
| cons xs xss ih => simp [ih]
/-! ### reverse -/
@[simp] theorem mem_reverse {x : α} {as : Array α} : x as.reverse x as := by
cases as
simp
/-! ### findSomeRevM?, findRevM?, findSomeRev?, findRev? -/
@[simp] theorem findSomeRevM?_eq_findSomeM?_reverse
@@ -2052,27 +1929,6 @@ namespace Array
cases as
simp
@[simp] theorem flatMap_empty {β} (f : α Array β) : (#[] : Array α).flatMap f = #[] := rfl
@[simp] theorem flatMap_toArray_cons {β} (f : α Array β) (a : α) (as : List α) :
(a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
simp [flatMap]
suffices cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
f a ++ List.foldl (fun bs a => bs ++ f a) cs as by
erw [empty_append] -- Why doesn't this work via `simp`?
simpa using this #[]
intro cs
induction as generalizing cs <;> simp_all
@[simp] theorem flatMap_toArray {β} (f : α Array β) (as : List α) :
as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
induction as with
| nil => simp
| cons a as ih =>
apply ext'
simp [ih]
end Array
/-! ### Deprecations -/

View File

@@ -1,159 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
prelude
import Init.Data.Array.Lemmas
import Init.Data.Array.Attach
import Init.Data.List.Monadic
/-!
# Lemmas about `Array.forIn'` and `Array.forIn`.
-/
namespace Array
open Nat
/-! ## Monadic operations -/
/-! ### mapM -/
theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α m β) (l : Array α) :
mapM f l = l.foldlM (fun acc a => return (acc.push ( f a))) #[] := by
rcases l with l
simp only [List.mapM_toArray, bind_pure_comp, size_toArray, List.foldlM_toArray']
rw [List.mapM_eq_reverse_foldlM_cons]
simp only [bind_pure_comp, Functor.map_map]
suffices (k), (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l by
exact this []
intro k
induction l generalizing k with
| nil => simp
| cons a as ih =>
simp [ih, List.foldlM_cons]
/-! ### foldlM and foldrM -/
theorem foldlM_map [Monad m] (f : β₁ β₂) (g : α β₂ m α) (l : Array β₁) (init : α) :
(l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
cases l
rw [List.map_toArray] -- Why doesn't this fire via `simp`?
simp [List.foldlM_map]
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ β₂) (g : β₂ α m α) (l : Array β₁)
(init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
cases l
rw [List.map_toArray] -- Why doesn't this fire via `simp`?
simp [List.foldrM_map]
theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α Option β) (g : γ β m γ) (l : Array α) (init : γ) :
(l.filterMap f).foldlM g init =
l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
cases l
rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
simp [List.foldlM_filterMap]
rfl
theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α Option β) (g : β γ m γ) (l : Array α) (init : γ) :
(l.filterMap f).foldrM g init =
l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
cases l
rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
simp [List.foldrM_filterMap]
rfl
theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α Bool) (g : β α m β) (l : Array α) (init : β) :
(l.filter p).foldlM g init =
l.foldlM (fun x y => if p y then g x y else pure x) init := by
cases l
rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
simp [List.foldlM_filter]
theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α Bool) (g : α β m β) (l : Array α) (init : β) :
(l.filter p).foldrM g init =
l.foldrM (fun x y => if p x then g x y else pure y) init := by
cases l
rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
simp [List.foldrM_filter]
/-! ### forIn' -/
/--
We can express a for loop over an array as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
(l : Array α) (f : (a : α) a l β m (ForInStep β)) (init : β) :
forIn' l init f = ForInStep.value <$>
l.attach.foldlM (fun b a, m => match b with
| .yield b => f a m b
| .done b => pure (.done b)) (ForInStep.yield init) := by
cases l
rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
simp only [List.forIn'_toArray, List.forIn'_eq_foldlM, List.attachWith_mem_toArray, size_toArray,
List.length_map, List.length_attach, List.foldlM_toArray', List.foldlM_map]
congr
/-- We can express a for loop over an array which always yields as a fold. -/
@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
(l : Array α) (f : (a : α) a l β m γ) (g : (a : α) a l β γ β) (init : β) :
forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
l.attach.foldlM (fun b a, m => g a m b <$> f a m b) init := by
cases l
rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
simp [List.foldlM_map]
theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
(l : Array α) (f : (a : α) a l β β) (init : β) :
forIn' l init (fun a m b => pure (.yield (f a m b))) =
pure (f := m) (l.attach.foldl (fun b a, h => f a h b) init) := by
cases l
simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
@[simp] theorem forIn'_yield_eq_foldl
(l : Array α) (f : (a : α) a l β β) (init : β) :
forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
l.attach.foldl (fun b a, h => f a h b) init := by
cases l
simp [List.foldl_map]
/--
We can express a for loop over an array as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
(f : α β m (ForInStep β)) (init : β) (l : Array α) :
forIn l init f = ForInStep.value <$>
l.foldlM (fun b a => match b with
| .yield b => f a b
| .done b => pure (.done b)) (ForInStep.yield init) := by
cases l
simp only [List.forIn_toArray, List.forIn_eq_foldlM, size_toArray, List.foldlM_toArray']
congr
/-- We can express a for loop over an array which always yields as a fold. -/
@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
(l : Array α) (f : α β m γ) (g : α β γ β) (init : β) :
forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
l.foldlM (fun b a => g a b <$> f a b) init := by
cases l
simp [List.foldlM_map]
theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
(l : Array α) (f : α β β) (init : β) :
forIn l init (fun a b => pure (.yield (f a b))) =
pure (f := m) (l.foldl (fun b a => f a b) init) := by
cases l
simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
@[simp] theorem forIn_yield_eq_foldl
(l : Array α) (f : α β β) (init : β) :
forIn (m := Id) l init (fun a b => .yield (f a b)) =
l.foldl (fun b a => f a b) init := by
cases l
simp [List.foldl_map]
end Array

View File

@@ -15,6 +15,15 @@ structure Subarray (α : Type u) where
start_le_stop : start stop
stop_le_array_size : stop array.size
@[deprecated Subarray.array (since := "2024-04-13")]
abbrev Subarray.as (s : Subarray α) : Array α := s.array
@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
theorem Subarray.h₁ (s : Subarray α) : s.start s.stop := s.start_le_stop
@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
theorem Subarray.h₂ (s : Subarray α) : s.stop s.array.size := s.stop_le_array_size
namespace Subarray
def size (s : Subarray α) : Nat :=

View File

@@ -29,6 +29,9 @@ section Nat
instance natCastInst : NatCast (BitVec w) := BitVec.ofNat w
@[deprecated isLt (since := "2024-03-12")]
theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
/-- Theorem for normalizing the bit vector literal representation. -/
-- TODO: This needs more usage data to assess which direction the simp should go.
@[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl

View File

@@ -403,7 +403,7 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} :
rw [carry_succ_one _ _ (by omega), Bool.xor_not, decide_not]
simp only [add_one_ne_zero, decide_false, getLsbD_not, and_eq_true, decide_eq_true_eq,
not_eq_eq_eq_not, Bool.not_true, false_bne, not_exists, _root_.not_and, not_eq_true,
bne_right_inj, decide_eq_decide]
bne_left_inj, decide_eq_decide]
constructor
· rintro h j hj; exact And.right <| h j (by omega)
· rintro h j hj; exact by omega, h j (by omega)
@@ -419,7 +419,7 @@ theorem getMsbD_neg {i : Nat} {x : BitVec w} :
simp [hi]; omega
case pos =>
have h₁ : w - 1 - i < w := by omega
simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_right_inj, decide_eq_decide]
simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide]
constructor
· rintro j, hj, h
refine w - 1 - j, by omega, by omega, by omega, _root_.cast ?_ h

View File

@@ -2611,7 +2611,7 @@ theorem getLsbD_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i
apply getLsbD_ge
omega
/-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsbD i`. -/
theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
(x.rotateLeft r).getLsbD i =
cond (i < r)
@@ -2638,56 +2638,6 @@ theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
if h' : i < r % w then x[(w - (r % w) + i)] else x[i - (r % w)] := by
simp [ BitVec.getLsbD_eq_getElem, h]
/-- If `w ≤ x < 2 * w`, then `x % w = x - w` -/
theorem mod_eq_sub_of_le_of_lt {x w : Nat} (x_le : w x) (x_lt : x < 2 * w) :
x % w = x - w := by
rw [Nat.mod_eq_sub_mod, Nat.mod_eq_of_lt (by omega)]
omega
theorem getMsbD_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
(x.rotateLeftAux r).getMsbD i = x.getMsbD (r + i) := by
rw [rotateLeftAux, getMsbD_or]
simp [show i < w - r by omega, Nat.add_comm]
theorem getMsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i w - r) :
(x.rotateLeftAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - (w - r))) := by
simp [rotateLeftAux, getMsbD_or, show i + r w by omega, show ¬i < w - r by omega]
/-- When `r < w`, we give a formula for `(x.rotateLeft r).getMsbD i`. -/
theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
(x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by
rcases w with rfl | w
· simp
· rw [BitVec.rotateLeft_eq_rotateLeftAux_of_lt (by omega)]
by_cases h : n < (w + 1) - r
· simp [getMsbD_rotateLeftAux_of_lt h, Nat.mod_eq_of_lt, show r + n < (w + 1) by omega, show n < w + 1 by omega]
· simp [getMsbD_rotateLeftAux_of_ge <| Nat.ge_of_not_lt h]
by_cases h₁ : n < w + 1
· simp only [h₁, decide_true, Bool.true_and]
have h₂ : (r + n) < 2 * (w + 1) := by omega
rw [mod_eq_sub_of_le_of_lt (by omega) (by omega)]
congr 1
omega
· simp [h₁]
theorem getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} :
(x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by
rcases w with rfl | w
· simp
· by_cases h : r < w
· rw [getMsbD_rotateLeft_of_lt (by omega)]
· rw [ rotateLeft_mod_eq_rotateLeft, getMsbD_rotateLeft_of_lt (by apply Nat.mod_lt; simp)]
simp
@[simp]
theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
(x.rotateLeft m).msb = x.getMsbD (m % w) := by
simp only [BitVec.msb, getMsbD_rotateLeft]
by_cases h : w = 0
· simp [h]
· simp
omega
/-! ## Rotate Right -/
/--
@@ -2749,7 +2699,7 @@ theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} :
simp only [rotateRight, Nat.mod_mod]
/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
theorem getLsbD_rotateRight_of_lt {x : BitVec w} {r i : Nat} (hr: r < w) :
theorem getLsbD_rotateRight_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
(x.rotateRight r).getLsbD i =
cond (i < w - r)
(x.getLsbD (r + i))
@@ -2767,7 +2717,7 @@ theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
(decide (i < w) && x.getLsbD (i - (w - (r % w)))) := by
rcases w with rfl, w
· simp
· rw [ rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_lt (Nat.mod_lt _ (by omega))]
· rw [ rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_le (Nat.mod_lt _ (by omega))]
@[simp]
theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
@@ -2775,56 +2725,6 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
simp only [ BitVec.getLsbD_eq_getElem]
simp [getLsbD_rotateRight, h]
theorem getMsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
(x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r)) := by
rw [rotateRightAux, getMsbD_or, getMsbD_ushiftRight]
simp [show i < r by omega]
theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i r) :
(x.rotateRightAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - r)) := by
simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) w by omega]
/-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`. -/
@[simp]
theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w):
(x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
rcases w with rfl | w
· simp
· rw [rotateRight_eq_rotateRightAux_of_lt (by omega)]
by_cases h : n < m
· simp only [getMsbD_rotateRightAux_of_lt h, show n < w + 1 by omega, decide_true,
show m % (w + 1) = m by rw [Nat.mod_eq_of_lt hr], h, reduceIte,
show (w + 1 + n - m) < (w + 1) by omega, Nat.mod_eq_of_lt, Bool.true_and]
congr 1
omega
· simp [h, getMsbD_rotateRightAux_of_ge <| Nat.ge_of_not_lt h]
by_cases h₁ : n < w + 1
· simp [h, h₁, decide_true, Bool.true_and, Nat.mod_eq_of_lt hr]
· simp [h₁]
@[simp]
theorem getMsbD_rotateRight {w n m : Nat} {x : BitVec w} :
(x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
rcases w with rfl | w
· simp
· by_cases h₀ : m < w
· rw [getMsbD_rotateRight_of_lt (by omega)]
· rw [ rotateRight_mod_eq_rotateRight, getMsbD_rotateRight_of_lt (by apply Nat.mod_lt; simp)]
simp
@[simp]
theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
(x.rotateRight r).msb = x.getMsbD ((w - r % w) % w) := by
simp only [BitVec.msb, getMsbD_rotateRight]
by_cases h₀ : 0 < w
· simp only [h₀, decide_true, Nat.add_zero, Nat.zero_le, Nat.sub_eq_zero_of_le, Bool.true_and,
ite_eq_left_iff, Nat.not_lt, Nat.le_zero_eq]
intro h₁
simp [h₁]
· simp [show w = 0 by omega]
/- ## twoPow -/
theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by

View File

@@ -238,8 +238,8 @@ theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by simp
@[simp] theorem bne_assoc : (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
instance : Std.Associative (· != ·) := bne_assoc
@[simp] theorem bne_right_inj : {x y z : Bool}, (x != y) = (x != z) y = z := by decide
@[simp] theorem bne_left_inj : {x y z : Bool}, (x != z) = (y != z) x = y := by decide
@[simp] theorem bne_left_inj : {x y z : Bool}, (x != y) = (x != z) y = z := by decide
@[simp] theorem bne_right_inj : {x y z : Bool}, (x != z) = (y != z) x = y := by decide
theorem eq_not_of_ne : {x y : Bool}, x y x = !y := by decide
@@ -295,9 +295,9 @@ theorem xor_right_comm : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = ((x ^^ z) ^^ y) :
theorem xor_assoc : (x y z : Bool), ((x ^^ y) ^^ z) = (x ^^ (y ^^ z)) := bne_assoc
theorem xor_right_inj : {x y z : Bool}, (x ^^ y) = (x ^^ z) y = z := bne_right_inj
theorem xor_left_inj : {x y z : Bool}, (x ^^ y) = (x ^^ z) y = z := bne_left_inj
theorem xor_left_inj : {x y z : Bool}, (x ^^ z) = (y ^^ z) x = y := bne_left_inj
theorem xor_right_inj : {x y z : Bool}, (x ^^ z) = (y ^^ z) x = y := bne_right_inj
/-! ### le/lt -/

View File

@@ -642,7 +642,7 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
ext
simp
@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 (i : Nat)) : (subNat 1 i h).succ = i := by
@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 i) : (subNat 1 i h).succ = i := by
ext
simp
omega

View File

@@ -31,7 +31,7 @@ opaque floatSpec : FloatSpec := {
structure Float where
val : floatSpec.float
instance : Nonempty Float := { val := floatSpec.val }
instance : Inhabited Float := { val := floatSpec.val }
@[extern "lean_float_add"] opaque Float.add : Float Float Float
@[extern "lean_float_sub"] opaque Float.sub : Float Float Float
@@ -47,25 +47,6 @@ def Float.lt : Float → Float → Prop := fun a b =>
def Float.le : Float Float Prop := fun a b =>
floatSpec.le a.val b.val
/--
Raw transmutation from `UInt64`.
Floats and UInts have the same endianness on all supported platforms.
IEEE 754 very precisely specifies the bit layout of floats.
-/
@[extern "lean_float_of_bits"] opaque Float.ofBits : UInt64 Float
/--
Raw transmutation to `UInt64`.
Floats and UInts have the same endianness on all supported platforms.
IEEE 754 very precisely specifies the bit layout of floats.
Note that this function is distinct from `Float.toUInt64`, which attempts
to preserve the numeric value, and not the bitwise value.
-/
@[extern "lean_float_to_bits"] opaque Float.toBits : Float UInt64
instance : Add Float := Float.add
instance : Sub Float := Float.sub
instance : Mul Float := Float.mul
@@ -136,9 +117,6 @@ instance : ToString Float where
@[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
instance : Inhabited Float where
default := UInt64.toFloat 0
instance : Repr Float where
reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n

View File

@@ -329,22 +329,22 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
/- ## add/sub injectivity -/
@[simp]
protected theorem add_left_inj {i j : Int} (k : Int) : (i + k = j + k) i = j := by
protected theorem add_right_inj {i j : Int} (k : Int) : (i + k = j + k) i = j := by
apply Iff.intro
· intro p
rw [Int.add_sub_cancel i k, Int.add_sub_cancel j k, p]
· exact congrArg (· + k)
@[simp]
protected theorem add_right_inj {i j : Int} (k : Int) : (k + i = k + j) i = j := by
protected theorem add_left_inj {i j : Int} (k : Int) : (k + i = k + j) i = j := by
simp [Int.add_comm k]
@[simp]
protected theorem sub_right_inj {i j : Int} (k : Int) : (k - i = k - j) i = j := by
protected theorem sub_left_inj {i j : Int} (k : Int) : (k - i = k - j) i = j := by
simp [Int.sub_eq_add_neg, Int.neg_inj]
@[simp]
protected theorem sub_left_inj {i j : Int} (k : Int) : (i - k = j - k) i = j := by
protected theorem sub_right_inj {i j : Int} (k : Int) : (i - k = j - k) i = j := by
simp [Int.sub_eq_add_neg]
/- ## Ring properties -/

View File

@@ -13,7 +13,7 @@ namespace List
`a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
but is defined only when all members of `l` satisfy `P`, using the proof
to apply `f`. -/
def pmap {P : α Prop} (f : a, P a β) : l : List α, (H : a l, P a) List β
@[simp] def pmap {P : α Prop} (f : a, P a β) : l : List α, (H : a l, P a) List β
| [], _ => []
| a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2
@@ -46,11 +46,6 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
| cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
exact go L h'
@[simp] theorem pmap_nil {P : α Prop} (f : a, P a β) : pmap f [] (by simp) = [] := rfl
@[simp] theorem pmap_cons {P : α Prop} (f : a, P a β) (a : α) (l : List α) (h : b a :: l, P b) :
pmap f (a :: l) h = f a (forall_mem_cons.1 h).1 :: pmap f l (forall_mem_cons.1 h).2 := rfl
@[simp] theorem attach_nil : ([] : List α).attach = [] := rfl
@[simp] theorem attachWith_nil : ([] : List α).attachWith P H = [] := rfl
@@ -153,7 +148,7 @@ theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h :
exact a, h, rfl
@[simp]
theorem length_pmap {p : α Prop} {f : a, p a β} {l H} : (pmap f l H).length = l.length := by
theorem length_pmap {p : α Prop} {f : a, p a β} {l H} : length (pmap f l H) = length l := by
induction l
· rfl
· simp only [*, pmap, length]
@@ -204,7 +199,7 @@ theorem attachWith_ne_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l,
@[simp]
theorem getElem?_pmap {p : α Prop} (f : a, p a β) {l : List α} (h : a l, p a) (n : Nat) :
(pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
(pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (getElem?_mem H) := by
induction l generalizing n with
| nil => simp
| cons hd tl hl =>
@@ -220,7 +215,7 @@ theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
· simp_all
theorem get?_pmap {p : α Prop} (f : a, p a β) {l : List α} (h : a l, p a) (n : Nat) :
get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H) := by
get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (get?_mem H) := by
simp only [get?_eq_getElem?]
simp [getElem?_pmap, h]
@@ -243,18 +238,18 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h :
(hn : n < (pmap f l h).length) :
get (pmap f l h) n, hn =
f (get l n, @length_pmap _ _ p f l h hn)
(h _ (getElem_mem (@length_pmap _ _ p f l h hn))) := by
(h _ (get_mem l n (@length_pmap _ _ p f l h hn))) := by
simp only [get_eq_getElem]
simp [getElem_pmap]
@[simp]
theorem getElem?_attachWith {xs : List α} {i : Nat} {P : α Prop} {H : a xs, P a} :
(xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
(xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (getElem?_mem a)) :=
getElem?_pmap ..
@[simp]
theorem getElem?_attach {xs : List α} {i : Nat} :
xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => mem_of_getElem? a) :=
xs.attach[i]? = xs[i]?.pmap Subtype.mk (fun _ a => getElem?_mem a) :=
getElem?_attachWith
@[simp]
@@ -338,7 +333,6 @@ This is useful when we need to use `attach` to show termination.
Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldl_subtype` below.
-/
theorem foldl_attach (l : List α) (f : β α β) (b : β) :
l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
@@ -354,7 +348,6 @@ This is useful when we need to use `attach` to show termination.
Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldr_subtype` below.
-/
theorem foldr_attach (l : List α) (f : α β β) (b : β) :
l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
@@ -459,16 +452,16 @@ theorem pmap_append' {p : α → Prop} (f : ∀ a : α, p a → β) (l₁ l₂ :
pmap_append f l₁ l₂ _
@[simp] theorem attach_append (xs ys : List α) :
(xs ++ ys).attach = xs.attach.map (fun x, h => x, mem_append_left ys h) ++
ys.attach.map fun x, h => x, mem_append_right xs h := by
(xs ++ ys).attach = xs.attach.map (fun x, h => x, mem_append_of_mem_left ys h) ++
ys.attach.map fun x, h => x, mem_append_of_mem_right xs h := by
simp only [attach, attachWith, pmap, map_pmap, pmap_append]
congr 1 <;>
exact pmap_congr_left _ fun _ _ _ _ => rfl
@[simp] theorem attachWith_append {P : α Prop} {xs ys : List α}
{H : (a : α), a xs ++ ys P a} :
(xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
(xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_of_mem_left ys h)) ++
ys.attachWith P (fun a h => H a (mem_append_of_mem_right xs h)) := by
simp only [attachWith, attach_append, map_pmap, pmap_append]
@[simp] theorem pmap_reverse {P : α Prop} (f : (a : α) P a β) (xs : List α)
@@ -605,15 +598,6 @@ def unattach {α : Type _} {p : α → Prop} (l : List { x // p x }) := l.map (
| nil => simp
| cons a l ih => simp [ih, Function.comp_def]
@[simp] theorem getElem?_unattach {p : α Prop} {l : List { x // p x }} (i : Nat) :
l.unattach[i]? = l[i]?.map Subtype.val := by
simp [unattach]
@[simp] theorem getElem_unattach
{p : α Prop} {l : List { x // p x }} (i : Nat) (h : i < l.unattach.length) :
l.unattach[i] = (l[i]'(by simpa using h)).1 := by
simp [unattach]
/-! ### Recognizing higher order functions on subtypes using a function that only depends on the value. -/
/--

View File

@@ -551,7 +551,7 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
/-! ### flatten -/
/--
`O(|flatten L|)`. `flatten L` concatenates all the lists in `L` into one list.
`O(|flatten L|)`. `join L` concatenates all the lists in `L` into one list.
* `flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
-/
def flatten : List (List α) List α
@@ -726,13 +726,13 @@ theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : List α} (h :
instance [BEq α] [LawfulBEq α] (a : α) (as : List α) : Decidable (a as) :=
decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
theorem mem_append_left {a : α} {as : List α} (bs : List α) : a as a as ++ bs := by
theorem mem_append_of_mem_left {a : α} {as : List α} (bs : List α) : a as a as ++ bs := by
intro h
induction h with
| head => apply Mem.head
| tail => apply Mem.tail; assumption
theorem mem_append_right {b : α} {bs : List α} (as : List α) : b bs b as ++ bs := by
theorem mem_append_of_mem_right {b : α} {bs : List α} (as : List α) : b bs b as ++ bs := by
intro h
induction as with
| nil => simp [h]

View File

@@ -256,7 +256,7 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
have : a as := by
have bs, h := h
subst h
exact mem_append_right _ (Mem.head ..)
exact mem_append_of_mem_right _ (Mem.head ..)
match ( f a this b) with
| ForInStep.done b => pure b
| ForInStep.yield b =>

View File

@@ -10,8 +10,7 @@ import Init.Data.List.Sublist
import Init.Data.List.Range
/-!
Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `List.indexOf`,
and `List.lookup`.
# Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, and `List.indexOf`.
-/
namespace List
@@ -96,22 +95,22 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
· simp only [Option.guard_eq_none] at h
simp [ih, h]
@[simp] theorem head?_filterMap (f : α Option β) (l : List α) : (l.filterMap f).head? = l.findSome? f := by
@[simp] theorem filterMap_head? (f : α Option β) (l : List α) : (l.filterMap f).head? = l.findSome? f := by
induction l with
| nil => simp
| cons x xs ih =>
simp only [filterMap_cons, findSome?_cons]
split <;> simp [*]
@[simp] theorem head_filterMap (f : α Option β) (l : List α) (h) :
(l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
@[simp] theorem filterMap_head (f : α Option β) (l : List α) (h) :
(l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
simp [head_eq_iff_head?_eq_some]
@[simp] theorem getLast?_filterMap (f : α Option β) (l : List α) : (l.filterMap f).getLast? = l.reverse.findSome? f := by
@[simp] theorem filterMap_getLast? (f : α Option β) (l : List α) : (l.filterMap f).getLast? = l.reverse.findSome? f := by
rw [getLast?_eq_head?_reverse]
simp [ filterMap_reverse]
@[simp] theorem getLast_filterMap (f : α Option β) (l : List α) (h) :
@[simp] theorem filterMap_getLast (f : α Option β) (l : List α) (h) :
(l.filterMap f).getLast h = (l.reverse.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
simp [getLast_eq_iff_getLast_eq_some]
@@ -292,18 +291,18 @@ theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h
· simp only [find?_cons]
split <;> simp_all
@[simp] theorem head?_filter (p : α Bool) (l : List α) : (l.filter p).head? = l.find? p := by
rw [ filterMap_eq_filter, head?_filterMap, findSome?_guard]
@[simp] theorem filter_head? (p : α Bool) (l : List α) : (l.filter p).head? = l.find? p := by
rw [ filterMap_eq_filter, filterMap_head?, findSome?_guard]
@[simp] theorem head_filter (p : α Bool) (l : List α) (h) :
@[simp] theorem filter_head (p : α Bool) (l : List α) (h) :
(l.filter p).head h = (l.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
simp [head_eq_iff_head?_eq_some]
@[simp] theorem getLast?_filter (p : α Bool) (l : List α) : (l.filter p).getLast? = l.reverse.find? p := by
@[simp] theorem filter_getLast? (p : α Bool) (l : List α) : (l.filter p).getLast? = l.reverse.find? p := by
rw [getLast?_eq_head?_reverse]
simp [ filter_reverse]
@[simp] theorem getLast_filter (p : α Bool) (l : List α) (h) :
@[simp] theorem filter_getLast (p : α Bool) (l : List α) (h) :
(l.filter p).getLast h = (l.reverse.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
simp [getLast_eq_iff_getLast_eq_some]

View File

@@ -91,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
@[specialize] def foldrTR (f : α β β) (init : β) (l : List α) : β := l.toArray.foldr f init
@[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
funext α β f init l; simp [foldrTR, Array.foldr_toList, -Array.size_toArray]
funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
/-! ### flatMap -/
@@ -331,7 +331,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
| a::as, n => by
rw [ show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
simp [enumFrom, f]
rw [ Array.foldr_toList]
rw [Array.foldr_eq_foldr_toList]
simp [go]
/-! ## Other list operations -/

View File

@@ -372,17 +372,6 @@ theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? =
@[deprecated getElem?_concat_length (since := "2024-06-12")]
theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
@[simp] theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome n < l.length := by
by_cases h : n < l.length
· simp_all
· simp [h]
simp_all
@[simp] theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone l.length n := by
by_cases h : n < l.length
· simp_all
· simp [h]
/-! ### mem -/
@[simp] theorem not_mem_nil (a : α) : ¬ a [] := nofun
@@ -394,9 +383,9 @@ theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = s
theorem mem_cons_self (a : α) (l : List α) : a a :: l := .head ..
theorem mem_concat_self (xs : List α) (a : α) : a xs ++ [a] :=
mem_append_right xs (mem_cons_self a _)
mem_append_of_mem_right xs (mem_cons_self a _)
theorem mem_append_cons_self : a xs ++ a :: ys := mem_append_right _ (mem_cons_self _ _)
theorem mem_append_cons_self : a xs ++ a :: ys := mem_append_of_mem_right _ (mem_cons_self _ _)
theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a xs) :
as bs, xs = as ++ a :: bs a as := by
@@ -503,20 +492,16 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
theorem get?_of_mem {a} {l : List α} (h : a l) : n, l.get? n = some a :=
let n, _, e := get_of_mem h; n, e get?_eq_get _
theorem get_mem : (l : List α) n, get l n l
| _ :: _, 0, _ => .head ..
| _ :: l, _+1, _ => .tail _ (get_mem l ..)
theorem get_mem : (l : List α) n h, get l n, h l
| _ :: _, 0, _ => .head ..
| _ :: l, _+1, _ => .tail _ (get_mem l ..)
theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a l :=
theorem getElem?_mem {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a l :=
let _, e := getElem?_eq_some_iff.1 e; e getElem_mem ..
@[deprecated mem_of_getElem? (since := "2024-09-06")] abbrev getElem?_mem := @mem_of_getElem?
theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a l :=
theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a l :=
let _, e := get?_eq_some.1 e; e get_mem ..
@[deprecated mem_of_get? (since := "2024-09-06")] abbrev get?_mem := @mem_of_get?
theorem mem_iff_getElem {a} {l : List α} : a l (n : Nat) (h : n < l.length), l[n]'h = a :=
getElem_of_mem, fun _, _, e => e getElem_mem ..
@@ -1040,10 +1025,6 @@ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
| _ :: _ :: _, _ => by
simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]
theorem getElem_length_sub_one_eq_getLast (l : List α) (h) :
l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by
rw [ getLast_eq_getElem]
@[deprecated getLast_eq_getElem (since := "2024-07-15")]
theorem getLast_eq_get (l : List α) (h : l []) :
getLast l h = l.get l.length - 1, by
@@ -1064,7 +1045,7 @@ theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a := by
@[simp] theorem getLast_singleton (a h) : @getLast α [a] h = a := rfl
theorem getLast!_cons_eq_getLastD [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
theorem getLast!_cons [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
simp [getLast!, getLast_eq_getLastD]
@[simp] theorem getLast_mem : {l : List α} (h : l []), getLast l h l
@@ -1128,12 +1109,7 @@ theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
/-! ### getLast! -/
theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
@[simp] theorem getLast!_eq_getLast?_getD [Inhabited α] {l : List α} : getLast! l = (getLast? l).getD default := by
cases l with
| nil => simp [getLast!_nil]
| cons _ _ => simp [getLast!, getLast?_eq_getLast]
@[simp] theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
theorem getLast!_of_getLast? [Inhabited α] : {l : List α}, getLast? l = some a getLast! l = a
| _ :: _, rfl => rfl
@@ -1168,11 +1144,6 @@ theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_p
| nil => simp at h
| cons _ _ => simp
theorem getElem_zero_eq_head (l : List α) (h) : l[0] = head l (by simpa [length_pos] using h) := by
cases l with
| nil => simp at h
| cons _ _ => simp
theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a xs.head? = some a := by
cases xs with
| nil => simp at h
@@ -2001,8 +1972,11 @@ theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t
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_append_left {a : α} {l₁ : List α} (l₂ : List α) (h : a l₁) : a l₁ ++ l₂ :=
mem_append.2 (Or.inl h)
theorem mem_append_right {a : α} (l₁ : List α) {l₂ : List α} (h : a l₂) : a l₁ ++ l₂ :=
mem_append.2 (Or.inr h)
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
@@ -2416,7 +2390,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
@[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) :
(replicate n a)[m] = a :=
eq_of_mem_replicate (getElem_mem _)
eq_of_mem_replicate (get_mem _ _ _)
@[deprecated getElem_replicate (since := "2024-06-12")]
theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by

View File

@@ -417,7 +417,7 @@ theorem Sublist.of_sublist_append_left (w : ∀ a, a ∈ l → a ∉ l₂) (h :
obtain l₁', l₂', rfl, h₁, h₂ := h
have : l₂' = [] := by
rw [eq_nil_iff_forall_not_mem]
exact fun x m => w x (mem_append_right l₁' m) (h₂.mem m)
exact fun x m => w x (mem_append_of_mem_right l₁' m) (h₂.mem m)
simp_all
theorem Sublist.of_sublist_append_right (w : a, a l a l₁) (h : l <+ l₁ ++ l₂) : l <+ l₂ := by
@@ -425,7 +425,7 @@ theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h :
obtain l₁', l₂', rfl, h₁, h₂ := h
have : l₁' = [] := by
rw [eq_nil_iff_forall_not_mem]
exact fun x m => w x (mem_append_left l₂' m) (h₁.mem m)
exact fun x m => w x (mem_append_of_mem_left l₂' m) (h₁.mem m)
simp_all
theorem Sublist.middle {l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l₁ ++ a :: l₂ := by

View File

@@ -1029,12 +1029,3 @@ instance decidableExistsLT [h : DecidablePred p] : DecidablePred fun n => ∃ m
instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => m : Nat, m n p m :=
fun n => decidable_of_iff ( m, m < n + 1 p m)
(exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
/-! ### Results about `List.sum` specialized to `Nat` -/
protected theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum x l, 0 < x := by
induction l with
| nil => simp
| cons x xs ih =>
simp [ ih]
omega

View File

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
prelude
import Init.ByCases
import Init.Data.Prod
import Init.Data.RArray
namespace Nat.Linear
@@ -16,7 +15,7 @@ namespace Nat.Linear
abbrev Var := Nat
abbrev Context := Lean.RArray Nat
abbrev Context := List Nat
/--
When encoding polynomials. We use `fixedVar` for encoding numerals.
@@ -24,7 +23,12 @@ abbrev Context := Lean.RArray Nat
def fixedVar := 100000000 -- Any big number should work here
def Var.denote (ctx : Context) (v : Var) : Nat :=
bif v == fixedVar then 1 else ctx.get v
bif v == fixedVar then 1 else go ctx v
where
go : List Nat Nat Nat
| [], _ => 0
| a::_, 0 => a
| _::as, i+1 => go as i
inductive Expr where
| num (v : Nat)
@@ -48,23 +52,25 @@ def Poly.denote (ctx : Context) (p : Poly) : Nat :=
| [] => 0
| (k, v) :: p => Nat.add (Nat.mul k (v.denote ctx)) (denote ctx p)
def Poly.insert (k : Nat) (v : Var) (p : Poly) : Poly :=
def Poly.insertSorted (k : Nat) (v : Var) (p : Poly) : Poly :=
match p with
| [] => [(k, v)]
| (k', v') :: p =>
bif Nat.blt v v' then
(k, v) :: (k', v') :: p
else bif Nat.beq v v' then
(k + k', v') :: p
else
(k', v') :: insert k v p
| (k', v') :: p => bif Nat.blt v v' then (k, v) :: (k', v') :: p else (k', v') :: insertSorted k v p
def Poly.norm (p : Poly) : Poly := go p []
where
go (p : Poly) (r : Poly) : Poly :=
def Poly.sort (p : Poly) : Poly :=
let rec go (p : Poly) (r : Poly) : Poly :=
match p with
| [] => r
| (k, v) :: p => go p (r.insert k v)
| (k, v) :: p => go p (r.insertSorted k v)
go p []
def Poly.fuse (p : Poly) : Poly :=
match p with
| [] => []
| (k, v) :: p =>
match fuse p with
| [] => [(k, v)]
| (k', v') :: p' => bif v == v' then (Nat.add k k', v)::p' else (k, v) :: (k', v') :: p'
def Poly.mul (k : Nat) (p : Poly) : Poly :=
bif k == 0 then
@@ -140,17 +146,15 @@ def Poly.combineAux (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
def Poly.combine (p₁ p₂ : Poly) : Poly :=
combineAux hugeFuel p₁ p₂
def Expr.toPoly (e : Expr) :=
go 1 e []
where
-- Implementation note: This assembles the result using difference lists
-- to avoid `++` on lists.
go (coeff : Nat) : Expr (Poly Poly)
| Expr.num k => bif k == 0 then id else ((coeff * k, fixedVar) :: ·)
| Expr.var i => ((coeff, i) :: ·)
| Expr.add a b => go coeff a go coeff b
| Expr.mulL k a
| Expr.mulR a k => bif k == 0 then id else go (coeff * k) a
def Expr.toPoly : Expr Poly
| Expr.num k => bif k == 0 then [] else [ (k, fixedVar) ]
| Expr.var i => [(1, i)]
| Expr.add a b => a.toPoly ++ b.toPoly
| Expr.mulL k a => a.toPoly.mul k
| Expr.mulR a k => a.toPoly.mul k
def Poly.norm (p : Poly) : Poly :=
p.sort.fuse
def Expr.toNormPoly (e : Expr) : Poly :=
e.toPoly.norm
@@ -197,7 +201,7 @@ def PolyCnstr.denote (ctx : Context) (c : PolyCnstr) : Prop :=
Poly.denote_le ctx (c.lhs, c.rhs)
def PolyCnstr.norm (c : PolyCnstr) : PolyCnstr :=
let (lhs, rhs) := Poly.cancel c.lhs.norm c.rhs.norm
let (lhs, rhs) := Poly.cancel c.lhs.sort.fuse c.rhs.sort.fuse
{ eq := c.eq, lhs, rhs }
def PolyCnstr.isUnsat (c : PolyCnstr) : Bool :=
@@ -264,32 +268,24 @@ def PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr :=
{ c with lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.right_distrib Nat.left_distrib Nat.mul_assoc Nat.mul_comm
attribute [local simp] Poly.denote Expr.denote Poly.insert Poly.norm Poly.norm.go Poly.cancelAux
attribute [local simp] Poly.denote Expr.denote Poly.insertSorted Poly.sort Poly.sort.go Poly.fuse Poly.cancelAux
attribute [local simp] Poly.mul Poly.mul.go
theorem Poly.denote_insert (ctx : Context) (k : Nat) (v : Var) (p : Poly) :
(p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (v : Var) (p : Poly) : (p.insertSorted k v).denote ctx = p.denote ctx + k * v.denote ctx := by
match p with
| [] => simp
| (k', v') :: p =>
by_cases h₁ : Nat.blt v v'
· simp [h₁]
· by_cases h₂ : Nat.beq v v'
· simp only [insert, h₁, h₂, cond_false, cond_true]
simp [Nat.eq_of_beq_eq_true h₂]
· simp only [insert, h₁, h₂, cond_false, cond_true]
simp [denote_insert]
| (k', v') :: p => by_cases h : Nat.blt v v' <;> simp [h, denote_insertSorted]
attribute [local simp] Poly.denote_insert
attribute [local simp] Poly.denote_insertSorted
theorem Poly.denote_norm_go (ctx : Context) (p : Poly) (r : Poly) : (norm.go p r).denote ctx = p.denote ctx + r.denote ctx := by
theorem Poly.denote_sort_go (ctx : Context) (p : Poly) (r : Poly) : (sort.go p r).denote ctx = p.denote ctx + r.denote ctx := by
match p with
| [] => simp
| (k, v):: p => simp [denote_norm_go]
| (k, v):: p => simp [denote_sort_go]
attribute [local simp] Poly.denote_norm_go
attribute [local simp] Poly.denote_sort_go
theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.norm.denote ctx = m.denote ctx := by
theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.sort.denote ctx = m.denote ctx := by
simp
attribute [local simp] Poly.denote_sort
@@ -320,6 +316,18 @@ theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.revers
attribute [local simp] Poly.denote_reverse
theorem Poly.denote_fuse (ctx : Context) (p : Poly) : p.fuse.denote ctx = p.denote ctx := by
match p with
| [] => rfl
| (k, v) :: p =>
have ih := denote_fuse ctx p
simp
split
case _ h => simp [ ih, h]
case _ k' v' p' h => by_cases he : v == v' <;> simp [he, ih, h]; rw [eq_of_beq he]
attribute [local simp] Poly.denote_fuse
theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx := by
simp
by_cases h : k == 0 <;> simp [h]; simp [eq_of_beq h]
@@ -508,25 +516,13 @@ theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p
attribute [local simp] Poly.denote_combine
theorem Expr.denote_toPoly_go (ctx : Context) (e : Expr) :
(toPoly.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
induction k, e using Expr.toPoly.go.induct generalizing p with
| case1 k k' =>
simp only [toPoly.go]
by_cases h : k' == 0
· simp [h, eq_of_beq h]
· simp [h, Var.denote]
| case2 k i => simp [toPoly.go]
| case3 k a b iha ihb => simp [toPoly.go, iha, ihb]
| case4 k k' a ih
| case5 k a k' ih =>
simp only [toPoly.go, denote, mul_eq]
by_cases h : k' == 0
· simp [h, eq_of_beq h]
· simp [h, cond_false, ih, Nat.mul_assoc]
theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
simp [toPoly, Expr.denote_toPoly_go]
induction e with
| num k => by_cases h : k == 0 <;> simp [toPoly, h, Var.denote]; simp [eq_of_beq h]
| var i => simp [toPoly]
| add a b iha ihb => simp [toPoly, iha, ihb]
| mulL k a ih => simp [toPoly, ih, -Poly.mul]
| mulR k a ih => simp [toPoly, ih, -Poly.mul]
attribute [local simp] Expr.denote_toPoly
@@ -558,8 +554,8 @@ theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denot
cases c; rename_i eq lhs rhs
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
by_cases h : eq = true <;> simp [h]
· simp [Poly.denote_eq]
· simp [Poly.denote_le]
· simp [Poly.denote_eq, Expr.toPoly]
· simp [Poly.denote_le, Expr.toPoly]
attribute [local simp] ExprCnstr.denote_toPoly

View File

@@ -16,22 +16,22 @@ def getM [Alternative m] : Option α → m α
| none => failure
| some a => pure a
@[deprecated getM (since := "2024-04-17")]
-- `[Monad m]` is not needed here.
def toMonad [Monad m] [Alternative m] : Option α m α := getM
/-- Returns `true` on `some x` and `false` on `none`. -/
@[inline] def isSome : Option α Bool
| some _ => true
| none => false
@[simp] theorem isSome_none : @isSome α none = false := rfl
@[simp] theorem isSome_some : isSome (some a) = true := rfl
@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α Bool := isSome
/-- Returns `true` on `none` and `false` on `some x`. -/
@[inline] def isNone : Option α Bool
| some _ => false
| none => true
@[simp] theorem isNone_none : @isNone α none = true := rfl
@[simp] theorem isNone_some : isNone (some a) = false := rfl
/--
`x?.isEqSome y` is equivalent to `x? == some y`, but avoids an allocation.
-/
@@ -134,10 +134,6 @@ def merge (fn : ααα) : Option α → Option α → Option α
@[inline] def get {α : Type u} : (o : Option α) isSome o α
| some x, _ => x
@[simp] theorem some_get : {x : Option α} (h : isSome x), some (x.get h) = x
| some _, _ => rfl
@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
/-- `guard p a` returns `some a` if `p a` holds, otherwise `none`. -/
@[inline] def guard (p : α Prop) [DecidablePred p] (a : α) : Option α :=
if p a then some a else none

View File

@@ -36,6 +36,11 @@ theorem get_of_mem : ∀ {o : Option α} (h : isSome o), a ∈ o → o.get h = a
theorem not_mem_none (a : α) : a (none : Option α) := nofun
@[simp] theorem some_get : {x : Option α} (h : isSome x), some (x.get h) = x
| some _, _ => rfl
@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl
theorem getD_of_ne_none {x : Option α} (hx : x none) (y : α) : some (x.getD y) = x := by
cases x; {contradiction}; rw [getD_some]
@@ -55,9 +60,7 @@ theorem get_eq_getD {fallback : α} : (o : Option α) → {h : o.isSome} → o.g
theorem some_get! [Inhabited α] : (o : Option α) o.isSome some (o.get!) = o
| some _, _ => rfl
theorem get!_eq_getD [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl
@[deprecated get!_eq_getD (since := "2024-11-18")] abbrev get!_eq_getD_default := @get!_eq_getD
theorem get!_eq_getD_default [Inhabited α] (o : Option α) : o.get! = o.getD default := rfl
theorem mem_unique {o : Option α} {a b : α} (ha : a o) (hb : b o) : a = b :=
some.inj <| ha hb
@@ -70,11 +73,19 @@ theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a
theorem eq_none_iff_forall_not_mem : o = none a, a o :=
fun e a h => by rw [e] at h; (cases h), fun h => ext <| by simp; exact h
@[simp] theorem isSome_none : @isSome α none = false := rfl
@[simp] theorem isSome_some : isSome (some a) = true := rfl
theorem isSome_iff_exists : isSome x a, x = some a := by cases x <;> simp [isSome]
theorem isSome_eq_isSome : (isSome x = isSome y) (x = none y = none) := by
cases x <;> cases y <;> simp
@[simp] theorem isNone_none : @isNone α none = true := rfl
@[simp] theorem isNone_some : isNone (some a) = false := rfl
@[simp] theorem not_isSome : isSome a = false a.isNone = true := by
cases a <;> simp

View File

@@ -1,69 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
prelude
import Init.PropLemmas
namespace Lean
/--
A `RArray` can model `Fin n → α` or `Array α`, but is optimized for a fast kernel-reducible `get`
operation.
The primary intended use case is the “denote” function of a typical proof by reflection proof, where
only the `get` operation is necessary. It is not suitable as a general-purpose data structure.
There is no well-formedness invariant attached to this data structure, to keep it concise; it's
semantics is given through `RArray.get`. In that way one can also view an `RArray` as a decision
tree implementing `Nat → α`.
See `RArray.ofFn` and `RArray.ofArray` in module `Lean.Data.RArray` for functions that construct an
`RArray`.
It is not universe-polymorphic. ; smaller proof objects and no complication with the `ToExpr` type
class.
-/
inductive RArray (α : Type) : Type where
| leaf : α RArray α
| branch : Nat RArray α RArray α RArray α
variable {α : Type}
/-- The crucial operation, written with very little abstractional overhead -/
noncomputable def RArray.get (a : RArray α) (n : Nat) : α :=
RArray.rec (fun x => x) (fun p _ _ l r => (Nat.ble p n).rec l r) a
private theorem RArray.get_eq_def (a : RArray α) (n : Nat) :
a.get n = match a with
| .leaf x => x
| .branch p l r => (Nat.ble p n).rec (l.get n) (r.get n) := by
conv => lhs; unfold RArray.get
split <;> rfl
/-- `RArray.get`, implemented conventionally -/
def RArray.getImpl (a : RArray α) (n : Nat) : α :=
match a with
| .leaf x => x
| .branch p l r => if n < p then l.getImpl n else r.getImpl n
@[csimp]
theorem RArray.get_eq_getImpl : @RArray.get = @RArray.getImpl := by
funext α a n
induction a with
| leaf _ => rfl
| branch p l r ihl ihr =>
rw [RArray.getImpl, RArray.get_eq_def]
simp only [ihl, ihr, Nat.not_le, Nat.ble_eq, ite_not]
cases hnp : Nat.ble p n <;> rfl
instance : GetElem (RArray α) Nat α (fun _ _ => True) where
getElem a n _ := a.get n
def RArray.size : RArray α Nat
| leaf _ => 1
| branch _ l r => l.size + r.size
end Lean

View File

@@ -113,10 +113,10 @@ initialize IO.stdGenRef : IO.Ref StdGen ←
let seed := UInt64.toNat (ByteArray.toUInt64LE! ( IO.getRandomBytes 8))
IO.mkRef (mkStdGen seed)
def IO.setRandSeed (n : Nat) : BaseIO Unit :=
def IO.setRandSeed (n : Nat) : IO Unit :=
IO.stdGenRef.set (mkStdGen n)
def IO.rand (lo hi : Nat) : BaseIO Nat := do
def IO.rand (lo hi : Nat) : IO Nat := do
let gen IO.stdGenRef.get
let (r, gen) := randNat gen lo hi
IO.stdGenRef.set gen

View File

@@ -148,9 +148,6 @@ instance : ShiftLeft Int8 := ⟨Int8.shiftLeft⟩
instance : ShiftRight Int8 := Int8.shiftRight
instance : DecidableEq Int8 := Int8.decEq
@[extern "lean_bool_to_int8"]
def Bool.toInt8 (b : Bool) : Int8 := if b then 1 else 0
@[extern "lean_int8_dec_lt"]
def Int8.decLt (a b : Int8) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -252,9 +249,6 @@ instance : ShiftLeft Int16 := ⟨Int16.shiftLeft⟩
instance : ShiftRight Int16 := Int16.shiftRight
instance : DecidableEq Int16 := Int16.decEq
@[extern "lean_bool_to_int16"]
def Bool.toInt16 (b : Bool) : Int16 := if b then 1 else 0
@[extern "lean_int16_dec_lt"]
def Int16.decLt (a b : Int16) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -360,9 +354,6 @@ instance : ShiftLeft Int32 := ⟨Int32.shiftLeft⟩
instance : ShiftRight Int32 := Int32.shiftRight
instance : DecidableEq Int32 := Int32.decEq
@[extern "lean_bool_to_int32"]
def Bool.toInt32 (b : Bool) : Int32 := if b then 1 else 0
@[extern "lean_int32_dec_lt"]
def Int32.decLt (a b : Int32) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -472,9 +463,6 @@ instance : ShiftLeft Int64 := ⟨Int64.shiftLeft⟩
instance : ShiftRight Int64 := Int64.shiftRight
instance : DecidableEq Int64 := Int64.decEq
@[extern "lean_bool_to_int64"]
def Bool.toInt64 (b : Bool) : Int64 := if b then 1 else 0
@[extern "lean_int64_dec_lt"]
def Int64.decLt (a b : Int64) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -586,9 +574,6 @@ instance : ShiftLeft ISize := ⟨ISize.shiftLeft⟩
instance : ShiftRight ISize := ISize.shiftRight
instance : DecidableEq ISize := ISize.decEq
@[extern "lean_bool_to_isize"]
def Bool.toISize (b : Bool) : ISize := if b then 1 else 0
@[extern "lean_isize_dec_lt"]
def ISize.decLt (a b : ISize) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))

View File

@@ -514,6 +514,9 @@ instance : Inhabited String := ⟨""⟩
instance : Append String := String.append
@[deprecated push (since := "2024-04-06")]
def str : String Char String := push
@[inline] def pushn (s : String) (c : Char) (n : Nat) : String :=
n.repeat (fun s => s.push c) s

View File

@@ -56,9 +56,6 @@ instance : Xor UInt8 := ⟨UInt8.xor⟩
instance : ShiftLeft UInt8 := UInt8.shiftLeft
instance : ShiftRight UInt8 := UInt8.shiftRight
@[extern "lean_bool_to_uint8"]
def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0
@[extern "lean_uint8_dec_lt"]
def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
@@ -119,9 +116,6 @@ instance : Xor UInt16 := ⟨UInt16.xor⟩
instance : ShiftLeft UInt16 := UInt16.shiftLeft
instance : ShiftRight UInt16 := UInt16.shiftRight
@[extern "lean_bool_to_uint16"]
def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0
set_option bootstrap.genMatcherCode false in
@[extern "lean_uint16_dec_lt"]
def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
@@ -180,9 +174,6 @@ instance : Xor UInt32 := ⟨UInt32.xor⟩
instance : ShiftLeft UInt32 := UInt32.shiftLeft
instance : ShiftRight UInt32 := UInt32.shiftRight
@[extern "lean_bool_to_uint32"]
def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
@[extern "lean_uint64_add"]
def UInt64.add (a b : UInt64) : UInt64 := a.toBitVec + b.toBitVec
@[extern "lean_uint64_sub"]
@@ -287,8 +278,5 @@ instance : Xor USize := ⟨USize.xor⟩
instance : ShiftLeft USize := USize.shiftLeft
instance : ShiftRight USize := USize.shiftRight
@[extern "lean_bool_to_usize"]
def Bool.toUSize (b : Bool) : USize := if b then 1 else 0
instance : Max USize := maxOfLe
instance : Min USize := minOfLe

View File

@@ -166,12 +166,6 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
have : Decidable (dom c i) := .isFalse h
simp [getElem!_def, getElem?_def, h]
@[simp] theorem get_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) [Decidable (dom c i)] (h) :
c[i]?.get h = c[i]'(by simp only [getElem?_def] at h; split at h <;> simp_all) := by
simp only [getElem?_def] at h
split <;> simp_all
namespace Fin
instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where

View File

@@ -374,9 +374,6 @@ partial def structEq : Syntax → Syntax → Bool
instance : BEq Lean.Syntax := structEq
instance : BEq (Lean.TSyntax k) := (·.raw == ·.raw)
/--
Finds the first `SourceInfo` from the back of `stx` or `none` if no `SourceInfo` can be found.
-/
partial def getTailInfo? : Syntax Option SourceInfo
| atom info _ => info
| ident info .. => info
@@ -385,39 +382,14 @@ partial def getTailInfo? : Syntax → Option SourceInfo
| node info _ _ => info
| _ => none
/--
Finds the first `SourceInfo` from the back of `stx` or `SourceInfo.none`
if no `SourceInfo` can be found.
-/
def getTailInfo (stx : Syntax) : SourceInfo :=
stx.getTailInfo?.getD SourceInfo.none
/--
Finds the trailing size of the first `SourceInfo` from the back of `stx`.
If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains no
trailing whitespace, the result is `0`.
-/
def getTrailingSize (stx : Syntax) : Nat :=
match stx.getTailInfo? with
| some (SourceInfo.original (trailing := trailing) ..) => trailing.bsize
| _ => 0
/--
Finds the trailing whitespace substring of the first `SourceInfo` from the back of `stx`.
If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
no trailing whitespace, the result is `none`.
-/
def getTrailing? (stx : Syntax) : Option Substring :=
stx.getTailInfo.getTrailing?
/--
Finds the tail position of the trailing whitespace of the first `SourceInfo` from the back of `stx`.
If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
no trailing whitespace and lacks a tail position, the result is `none`.
-/
def getTrailingTailPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos :=
stx.getTailInfo.getTrailingTailPos? canonicalOnly
/--
Return substring of original input covering `stx`.
Result is meaningful only if all involved `SourceInfo.original`s refer to the same string (as is the case after parsing). -/
@@ -431,20 +403,21 @@ def getSubstring? (stx : Syntax) (withLeading := true) (withTrailing := true) :
}
| _, _ => none
@[specialize] private partial def updateLast {α} (a : Array α) (f : α Option α) (i : Fin (a.size + 1)) : Option (Array α) :=
match i with
| 0 => none
| i + 1, h =>
let v := a[i]'(Nat.succ_lt_succ_iff.mp h)
@[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α Option α) (i : Nat) : Option (Array α) :=
if i == 0 then
none
else
let i := i - 1
let v := a[i]!
match f v with
| some v => some <| a.set i v (Nat.succ_lt_succ_iff.mp h)
| none => updateLast a f i, Nat.lt_of_succ_lt h
| some v => some <| a.set! i v
| none => updateLast a f i
partial def setTailInfoAux (info : SourceInfo) : Syntax Option Syntax
| atom _ val => some <| atom info val
| ident _ rawVal val pre => some <| ident info rawVal val pre
| node info' k args =>
match updateLast args (setTailInfoAux info) args.size, by simp with
match updateLast args (setTailInfoAux info) args.size with
| some args => some <| node info' k args
| none => none
| _ => none

View File

@@ -22,28 +22,28 @@ syntax explicitBinders := (ppSpace bracketedExplicitBinders)+ <|> unb
open TSyntax.Compat in
def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax :=
let rec loop (i : Nat) (h : i idents.size) (acc : Syntax) := do
let rec loop (i : Nat) (acc : Syntax) := do
match i with
| 0 => pure acc
| i + 1 =>
let ident := idents[i][0]
| i+1 =>
let ident := idents[i]![0]
let acc match ident.isIdent, type? with
| true, none => `($combinator fun $ident => $acc)
| true, some type => `($combinator fun $ident : $type => $acc)
| false, none => `($combinator fun _ => $acc)
| false, some type => `($combinator fun _ : $type => $acc)
loop i (Nat.le_of_succ_le h) acc
loop idents.size (by simp) body
loop i acc
loop idents.size body
def expandBrackedBindersAux (combinator : Syntax) (binders : Array Syntax) (body : Syntax) : MacroM Syntax :=
let rec loop (i : Nat) (h : i binders.size) (acc : Syntax) := do
let rec loop (i : Nat) (acc : Syntax) := do
match i with
| 0 => pure acc
| i+1 =>
let idents := binders[i][1].getArgs
let type := binders[i][3]
loop i (Nat.le_of_succ_le h) ( expandExplicitBindersAux combinator idents (some type) acc)
loop binders.size (by simp) body
let idents := binders[i]![1].getArgs
let type := binders[i]![3]
loop i ( expandExplicitBindersAux combinator idents (some type) acc)
loop binders.size body
def expandExplicitBinders (combinatorDeclName : Name) (explicitBinders : Syntax) (body : Syntax) : MacroM Syntax := do
let combinator := mkCIdentFrom ( getRef) combinatorDeclName

View File

@@ -2829,6 +2829,17 @@ instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabi
instance [Monad m] : [Nonempty α] Nonempty (m α)
| x => pure x
/-- A fusion of Haskell's `sequence` and `map`. Used in syntax quotations. -/
def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v Type w} [Monad m] (as : Array α) (f : α m β) : m (Array β) :=
let rec loop (i : Nat) (j : Nat) (bs : Array β) : m (Array β) :=
dite (LT.lt j as.size)
(fun hlt =>
match i with
| 0 => pure bs
| Nat.succ i' => Bind.bind (f (as.get j hlt)) fun b => loop i' (hAdd j 1) (bs.push b))
(fun _ => pure bs)
loop as.size 0 (Array.mkEmpty as.size)
/--
A function for lifting a computation from an inner `Monad` to an outer `Monad`.
Like Haskell's [`MonadTrans`], but `n` does not have to be a monad transformer.
@@ -3654,8 +3665,7 @@ namespace SourceInfo
/--
Gets the position information from a `SourceInfo`, if available.
If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
will also return `none`.
If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
-/
def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
match info, canonicalOnly with
@@ -3666,8 +3676,7 @@ def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
/--
Gets the end position information from a `SourceInfo`, if available.
If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
will also return `none`.
If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
-/
def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
match info, canonicalOnly with
@@ -3676,24 +3685,6 @@ def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos
| synthetic (endPos := endPos) .., false => some endPos
| _, _ => none
/--
Gets the substring representing the trailing whitespace of a `SourceInfo`, if available.
-/
def getTrailing? (info : SourceInfo) : Option Substring :=
match info with
| original (trailing := trailing) .. => some trailing
| _ => none
/--
Gets the end position information of the trailing whitespace of a `SourceInfo`, if available.
If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
will also return `none`.
-/
def getTrailingTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
match info.getTrailing? with
| some trailing => some trailing.stopPos
| none => info.getTailPos? canonicalOnly
end SourceInfo
/--
@@ -3992,6 +3983,7 @@ position information.
def getPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos :=
stx.getHeadInfo.getPos? canonicalOnly
/--
Get the ending position of the syntax, if possible.
If `canonicalOnly` is true, non-canonical `synthetic` nodes are treated as not carrying

View File

@@ -802,9 +802,6 @@ def run (args : SpawnArgs) : IO String := do
end Process
/-- Returns the thread ID of the calling thread. -/
@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt64
structure AccessRight where
read : Bool := false
write : Bool := false

View File

@@ -29,13 +29,13 @@ def decodeUri (uri : String) : String := Id.run do
let len := rawBytes.size
let mut i := 0
let percent := '%'.toNat.toUInt8
while h : i < len do
let c := rawBytes[i]
(decoded, i) := if h₁ : c == percent i + 1 < len then
let h1 := rawBytes[i + 1]
while i < len do
let c := rawBytes[i]!
(decoded, i) := if c == percent && i + 1 < len then
let h1 := rawBytes[i + 1]!
if let some hd1 := hexDigitToUInt8? h1 then
if h₂ : i + 2 < len then
let h2 := rawBytes[i + 2]
if i + 2 < len then
let h2 := rawBytes[i + 2]!
if let some hd2 := hexDigitToUInt8? h2 then
-- decode the hex digits into a byte.
(decoded.push (hd1 * 16 + hd2), i + 3)

View File

@@ -466,7 +466,7 @@ hypotheses or the goal. It can have one of the forms:
* `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
* `at *`: target all hypotheses and the goal
-/
syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)))
syntax location := withPosition(" at" (locationWildcard <|> locationHyp))
/--
* `change tgt'` will change the goal from `tgt` to `tgt'`,
@@ -1155,7 +1155,7 @@ Configuration for the `decide` tactic family.
structure DecideConfig where
/-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance.
This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel),
however kernel reduction ignores transparency settings. -/
however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/
kernel : Bool := false
/-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
admitting the result via the axiom `Lean.ofReduceBool`. This can be significantly more efficient,
@@ -1165,9 +1165,7 @@ structure DecideConfig where
native : Bool := false
/-- If true (default: true), then when preprocessing the goal, do zeta reduction to attempt to eliminate free variables. -/
zetaReduce : Bool := true
/-- If true (default: false), then when preprocessing, removes irrelevant variables and reverts the local context.
A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
or if it is a proposition that refers to a relevant variable. -/
/-- If true (default: false), then when preprocessing reverts free variables. -/
revert : Bool := false
/--
@@ -1242,6 +1240,17 @@ example : 1 + 1 = 2 := by rfl
-/
syntax (name := decide) "decide" optConfig : tactic
/--
`decide!` is a variant of the `decide` tactic that uses kernel reduction to prove the goal.
It has the following properties:
- Since it uses kernel reduction instead of elaborator reduction, it ignores transparency and can unfold everything.
- While `decide` needs to reduce the `Decidable` instance twice (once during elaboration to verify whether the tactic succeeds,
and once during kernel type checking), the `decide!` tactic reduces it exactly once.
The `decide!` syntax is short for `decide +kernel`.
-/
syntax (name := decideBang) "decide!" optConfig : tactic
/--
`native_decide` is a synonym for `decide +native`.
It will attempt to prove a goal of type `p` by synthesizing an instance

View File

@@ -133,8 +133,8 @@ def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option E
return mkConst ``Bool.false
def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b)
def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a b)
def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a b)
def natFoldFns : List (Name × BinFoldFn) :=
[(``Nat.add, foldNatAdd),

View File

@@ -271,9 +271,9 @@ def emitTag (x : VarId) (xType : IRType) : M Unit := do
emit x
def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) :=
if h : alts.size 2 then none
else match alts[0] with
| Alt.ctor c b => some (c.cidx, b, alts[1].body)
if alts.size != 2 then none
else match alts[0]! with
| Alt.ctor c b => some (c.cidx, b, alts[1]!.body)
| _ => none
def emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit := do

View File

@@ -1172,8 +1172,8 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
(needsPackedArgs? : Bool) (llvmfn : LLVM.Value llvmctx) (params : Array Param) : M llvmctx Unit := do
if needsPackedArgs? then do
let argsp LLVM.getParam llvmfn 0 -- lean_object **args
for h : i in [:params.size] do
let param := params[i]
for i in List.range params.size do
let param := params[i]!
-- argsi := (args + i)
let argsi LLVM.buildGEP2 builder ( LLVM.voidPtrType llvmctx) argsp #[ constIntUnsigned i] s!"packed_arg_{i}_slot"
let llvmty toLLVMType param.ty
@@ -1182,16 +1182,15 @@ def emitFnArgs (builder : LLVM.Builder llvmctx)
-- slot for arg[i] which is always void* ?
let alloca buildPrologueAlloca builder llvmty s!"arg_{i}"
LLVM.buildStore builder pv alloca
addVartoState param.x alloca llvmty
addVartoState params[i]!.x alloca llvmty
else
let n LLVM.countParams llvmfn
for i in [:n.toNat] do
let param := params[i]!
let llvmty toLLVMType param.ty
for i in (List.range n.toNat) do
let llvmty toLLVMType params[i]!.ty
let alloca buildPrologueAlloca builder llvmty s!"arg_{i}"
let arg LLVM.getParam llvmfn (UInt64.ofNat i)
let _ LLVM.buildStore builder arg alloca
addVartoState param.x alloca llvmty
addVartoState params[i]!.x alloca llvmty
def emitDeclAux (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) (d : Decl) : M llvmctx Unit := do
let env getEnv

View File

@@ -54,7 +54,7 @@ abbrev Mask := Array (Option VarId)
partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
let done (_ : Unit) := (bs ++ keep.reverse, mask)
let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
if h : bs.size < 2 then done ()
if bs.size < 2 then done ()
else
let b := bs.back!
match b with
@@ -62,7 +62,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
| .vdecl _ _ (.uproj _ _) _ => keepInstr b
| .inc z n c p _ =>
if n == 0 then done () else
let b' := bs[bs.size - 2]
let b' := bs[bs.size - 2]!
match b' with
| .vdecl w _ (.proj i x) _ =>
if w == z && y == x then

View File

@@ -366,10 +366,10 @@ to be updated.
@[implemented_by updateFunDeclCoreImp] opaque FunDeclCore.updateCore (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
def CasesCore.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
let found i := (cases.alts[i], { cases with alts := cases.alts.eraseIdx i })
if let some i := cases.alts.findFinIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
let found (i : Nat) := (cases.alts[i]!, { cases with alts := cases.alts.eraseIdx i })
if let some i := cases.alts.findIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
found i
else if let some i := cases.alts.findFinIdx? fun | .default _ => true | _ => false then
else if let some i := cases.alts.findIdx? fun | .default _ => true | _ => false then
found i
else
unreachable!

View File

@@ -134,9 +134,9 @@ def withEachOccurrence (targetName : Name) (f : Nat → PassInstaller) : PassIns
def installAfter (targetName : Name) (p : Pass Pass) (occurrence : Nat := 0) : PassInstaller where
install passes :=
if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
let passUnderTest := passes[idx]
return passes.insertIdx (idx + 1) (p passUnderTest)
if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
let passUnderTest := passes[idx]!
return passes.insertAt! (idx + 1) (p passUnderTest)
else
throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
@@ -145,9 +145,9 @@ def installAfterEach (targetName : Name) (p : Pass → Pass) : PassInstaller :=
def installBefore (targetName : Name) (p : Pass Pass) (occurrence : Nat := 0): PassInstaller where
install passes :=
if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
let passUnderTest := passes[idx]
return passes.insertIdx idx (p passUnderTest)
if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
let passUnderTest := passes[idx]!
return passes.insertAt! idx (p passUnderTest)
else
throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"

View File

@@ -152,8 +152,8 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
let specArgs? := getSpecializationArgs? ( getEnv) decl.name
let contains (i : Nat) : Bool := specArgs?.getD #[] |>.contains i
let mut paramsInfo : Array SpecParamInfo := #[]
for h :i in [:decl.params.size] do
let param := decl.params[i]
for i in [:decl.params.size] do
let param := decl.params[i]!
let info
if contains i then
pure .user
@@ -181,14 +181,14 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do
declsInfo := declsInfo.push paramsInfo
if declsInfo.any fun paramsInfo => paramsInfo.any (· matches .user | .fixedInst | .fixedHO) then
let m := mkFixedParamsMap decls
for hi : i in [:decls.size] do
let decl := decls[i]
for i in [:decls.size] do
let decl := decls[i]!
let mut paramsInfo := declsInfo[i]!
let some mask := m.find? decl.name | unreachable!
trace[Compiler.specialize.info] "{decl.name} {mask}"
paramsInfo := paramsInfo.zipWith mask fun info fixed => if fixed || info matches .user then info else .other
for j in [:paramsInfo.size] do
let mut info := paramsInfo[j]!
let mut info := paramsInfo[j]!
if info matches .fixedNeutral && !hasFwdDeps decl paramsInfo j then
paramsInfo := paramsInfo.set! j .other
if paramsInfo.any fun info => info matches .fixedInst | .fixedHO | .user then

View File

@@ -499,8 +499,8 @@ where
match app with
| .fvar f =>
let mut argsNew := #[]
for h :i in [arity : args.size] do
argsNew := argsNew.push ( visitAppArg args[i])
for i in [arity : args.size] do
argsNew := argsNew.push ( visitAppArg args[i]!)
letValueToArg <| .fvar f argsNew
| .erased | .type .. => return .erased

View File

@@ -26,14 +26,13 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
if let some idx := arg.isNatLit? then
if idx == 0 then throwErrorAt arg "invalid specialization argument index, index must be greater than 0"
let idx := idx - 1
if h : idx >= argNames.size then
if idx >= argNames.size then
throwErrorAt arg "invalid argument index, `{declName}` has #{argNames.size} arguments"
else
if result.contains idx then throwErrorAt arg "invalid specialization argument index, `{argNames[idx]}` has already been specified as a specialization candidate"
result := result.push idx
if result.contains idx then throwErrorAt arg "invalid specialization argument index, `{argNames[idx]!}` has already been specified as a specialization candidate"
result := result.push idx
else
let argName := arg.getId
if let some idx := argNames.indexOf? argName then
if let some idx := argNames.getIdx? argName then
if result.contains idx then throwErrorAt arg "invalid specialization argument name `{argName}`, it has already been specified as a specialization candidate"
result := result.push idx
else

View File

@@ -29,4 +29,4 @@ import Lean.Data.Xml
import Lean.Data.NameTrie
import Lean.Data.RBTree
import Lean.Data.RBMap
import Lean.Data.RArray
import Lean.Data.Rat

View File

@@ -365,7 +365,6 @@ structure TextDocumentRegistrationOptions where
inductive MarkupKind where
| plaintext | markdown
deriving DecidableEq, Hashable
instance : FromJson MarkupKind := fun
| str "plaintext" => Except.ok MarkupKind.plaintext
@@ -379,7 +378,7 @@ instance : ToJson MarkupKind := ⟨fun
structure MarkupContent where
kind : MarkupKind
value : String
deriving ToJson, FromJson, DecidableEq, Hashable
deriving ToJson, FromJson
/-- Reference to the progress of some in-flight piece of work.

View File

@@ -25,7 +25,7 @@ inductive CompletionItemKind where
| unit | value | enum | keyword | snippet
| color | file | reference | folder | enumMember
| constant | struct | event | operator | typeParameter
deriving Inhabited, DecidableEq, Repr, Hashable
deriving Inhabited, DecidableEq, Repr
instance : ToJson CompletionItemKind where
toJson a := toJson (a.toCtorIdx + 1)
@@ -39,11 +39,11 @@ structure InsertReplaceEdit where
newText : String
insert : Range
replace : Range
deriving FromJson, ToJson, BEq, Hashable
deriving FromJson, ToJson
inductive CompletionItemTag where
| deprecated
deriving Inhabited, DecidableEq, Repr, Hashable
deriving Inhabited, DecidableEq, Repr
instance : ToJson CompletionItemTag where
toJson t := toJson (t.toCtorIdx + 1)
@@ -73,7 +73,7 @@ structure CompletionItem where
commitCharacters? : string[]
command? : Command
-/
deriving FromJson, ToJson, Inhabited, BEq, Hashable
deriving FromJson, ToJson, Inhabited
structure CompletionList where
isIncomplete : Bool

View File

@@ -33,16 +33,6 @@ def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n
instance : ForIn m (NameMap α) (Name × α) :=
inferInstanceAs (ForIn _ (RBMap ..) ..)
/-- `filter f m` returns the `NameMap` consisting of all
"`key`/`val`"-pairs in `m` where `f key val` returns `true`. -/
def filter (f : Name α Bool) (m : NameMap α) : NameMap α := RBMap.filter f m
/-- `filterMap f m` filters an `NameMap` and simultaneously modifies the filtered values.
It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`.
The resulting entries with non-`none` value are collected to form the output `NameMap`. -/
def filterMap (f : Name α Option β) (m : NameMap α) : NameMap β := RBMap.filterMap f m
end NameMap
def NameSet := RBTree Name Name.quickCmp
@@ -63,9 +53,6 @@ def append (s t : NameSet) : NameSet :=
instance : Append NameSet where
append := NameSet.append
/-- `filter f s` returns the `NameSet` consisting of all `x` in `s` where `f x` returns `true`. -/
def filter (f : Name Bool) (s : NameSet) : NameSet := RBTree.filter f s
end NameSet
def NameSSet := SSet Name
@@ -86,9 +73,6 @@ instance : EmptyCollection NameHashSet := ⟨empty⟩
instance : Inhabited NameHashSet := {}
def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n
/-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`. -/
def filter (f : Name Bool) (s : NameHashSet) : NameHashSet := Std.HashSet.filter f s
end NameHashSet
def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=

View File

@@ -233,10 +233,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
| n@(Node.collision keys vals heq), _, k =>
match keys.indexOf? k with
| some idx =>
let keys' := keys.eraseIdx idx
have keq := keys.size_eraseIdx idx _
let vals' := vals.eraseIdx (Eq.ndrec idx heq)
have veq := vals.size_eraseIdx (Eq.ndrec idx heq) _
let keys' := keys.feraseIdx idx
have keq := keys.size_feraseIdx idx
let vals' := vals.feraseIdx (Eq.ndrec idx heq)
have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
have : keys.size - 1 = vals.size - 1 := by rw [heq]
Node.collision keys' vals' (keq.trans (this.trans veq.symm))
| none => n

View File

@@ -1,75 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joachim Breitner
-/
prelude
import Init.Data.RArray
import Lean.ToExpr
/-!
Auxillary definitions related to `Lean.RArray` that are typically only used in meta-code, in
particular the `ToExpr` instance.
-/
namespace Lean
-- This function could live in Init/Data/RArray.lean, but without omega it's tedious to implement
def RArray.ofFn {n : Nat} (f : Fin n α) (h : 0 < n) : RArray α :=
go 0 n h (Nat.le_refl _)
where
go (lb ub : Nat) (h1 : lb < ub) (h2 : ub n) : RArray α :=
if h : lb + 1 = ub then
.leaf (f lb, Nat.lt_of_lt_of_le h1 h2)
else
let mid := (lb + ub)/2
.branch mid (go lb mid (by omega) (by omega)) (go mid ub (by omega) h2)
def RArray.ofArray (xs : Array α) (h : 0 < xs.size) : RArray α :=
.ofFn (xs[·]) h
/-- The correctness theorem for `ofFn` -/
theorem RArray.get_ofFn {n : Nat} (f : Fin n α) (h : 0 < n) (i : Fin n) :
(ofFn f h).get i = f i :=
go 0 n h (Nat.le_refl _) (Nat.zero_le _) i.2
where
go lb ub h1 h2 (h3 : lb i.val) (h3 : i.val < ub) : (ofFn.go f lb ub h1 h2).get i = f i := by
induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
case case1 =>
simp [ofFn.go, RArray.get_eq_getImpl, RArray.getImpl]
congr
omega
case case2 ih1 ih2 hiu =>
rw [ofFn.go]; simp only [reduceDIte, *]
simp [RArray.get_eq_getImpl, RArray.getImpl] at *
split
· rw [ih1] <;> omega
· rw [ih2] <;> omega
@[simp]
theorem RArray.size_ofFn {n : Nat} (f : Fin n α) (h : 0 < n) :
(ofFn f h).size = n :=
go 0 n h (Nat.le_refl _)
where
go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by
induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
case case1 => simp [ofFn.go, size]; omega
case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega
section Meta
open Lean
def RArray.toExpr (ty : Expr) (f : α Expr) : RArray α Expr
| .leaf x =>
mkApp2 (mkConst ``RArray.leaf) ty (f x)
| .branch p l r =>
mkApp4 (mkConst ``RArray.branch) ty (mkRawNatLit p) (l.toExpr ty f) (r.toExpr ty f)
instance [ToExpr α] : ToExpr (RArray α) where
toTypeExpr := mkApp (mkConst ``RArray) (toTypeExpr α)
toExpr a := a.toExpr (toTypeExpr α) toExpr
end Meta
end Lean

View File

@@ -404,24 +404,6 @@ def intersectBy {γ : Type v₁} {δ : Type v₂} (mergeFn : α → β → γ
| some b₂ => acc.insert a <| mergeFn a b₁ b₂
| none => acc
/--
`filter f m` returns the `RBMap` consisting of all
"`key`/`val`"-pairs in `m` where `f key val` returns `true`.
-/
def filter (f : α β Bool) (m : RBMap α β cmp) : RBMap α β cmp :=
m.fold (fun r k v => if f k v then r.insert k v else r) {}
/--
`filterMap f m` filters an `RBMap` and simultaneously modifies the filtered values.
It takes a function `f : α → β → Option γ` and applies `f k v` to the value with key `k`.
The resulting entries with non-`none` value are collected to form the output `RBMap`.
-/
def filterMap (f : α β Option γ) (m : RBMap α β cmp) : RBMap α γ cmp :=
m.fold (fun r k v => match f k v with
| none => r
| some b => r.insert k b) {}
end RBMap
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α α Ordering) : RBMap α β cmp :=

View File

@@ -114,13 +114,6 @@ def union (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
def diff (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
t₂.fold .erase t₁
/--
`filter f m` returns the `RBTree` consisting of all
`x` in `m` where `f x` returns `true`.
-/
def filter (f : α Bool) (m : RBTree α cmp) : RBTree α cmp :=
RBMap.filter (fun a _ => f a) m
end RBTree
def rbtreeOf {α : Type u} (l : List α) (cmp : α α Ordering) : RBTree α cmp :=

View File

@@ -8,8 +8,7 @@ import Init.NotationExtra
import Init.Data.ToString.Macro
import Init.Data.Int.DivMod
import Init.Data.Nat.Gcd
namespace Std
namespace Internal
namespace Lean
/-!
Rational numbers for implementing decision procedures.
@@ -145,5 +144,4 @@ instance : Coe Int Rat where
coe num := { num }
end Rat
end Internal
end Std
end Lean

View File

@@ -1347,7 +1347,7 @@ where
let mut unusableNamedArgs := unusableNamedArgs
for x in xs, bInfo in bInfos do
let xDecl x.mvarId!.getDecl
if let some idx := remainingNamedArgs.findFinIdx? (·.name == xDecl.userName) then
if let some idx := remainingNamedArgs.findIdx? (·.name == xDecl.userName) then
/- If there is named argument with name `xDecl.userName`, then it is accounted for and we can't make use of it. -/
remainingNamedArgs := remainingNamedArgs.eraseIdx idx
else
@@ -1355,9 +1355,9 @@ where
/- We found a type of the form (baseName ...).
First, we check if the current argument is an explicit one,
and if the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
if h : argIdx args.size bInfo.isExplicit then
if argIdx args.size && bInfo.isExplicit then
/- We can insert `e` as an explicit argument -/
return (args.insertIdx argIdx (Arg.expr e), namedArgs)
return (args.insertAt! argIdx (Arg.expr e), namedArgs)
else
/- If we can't add `e` to `args`, we try to add it using a named argument, but this is only possible
if there isn't an argument with the same name occurring before it. -/
@@ -1399,8 +1399,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
let rec loop : Expr List LVal TermElabM Expr
| f, [] => elabAppArgs f namedArgs args expectedType? explicit ellipsis
| f, lval::lvals => do
if let LVal.fieldName (ref := ref) .. := lval then
addDotCompletionInfo ref f expectedType?
if let LVal.fieldName (fullRef := fullRef) .. := lval then
addDotCompletionInfo fullRef f expectedType?
let hasArgs := !namedArgs.isEmpty || !args.isEmpty
let (f, lvalRes) resolveLVal f lval hasArgs
match lvalRes with
@@ -1650,14 +1650,6 @@ private def getSuccesses (candidates : Array (TermElabResult Expr)) : TermElabM
-/
private def mergeFailures (failures : Array (TermElabResult Expr)) : TermElabM α := do
let exs := failures.map fun | .error ex _ => ex | _ => unreachable!
let trees := failures.map (fun | .error _ s => s.meta.core.infoState.trees | _ => unreachable!)
|>.filterMap (·[0]?)
-- Retain partial `InfoTree` subtrees in an `.ofChoiceInfo` node in case of multiple failures.
-- This ensures that the language server still has `Info` to work with when multiple overloaded
-- elaborators fail.
withInfoContext (mkInfo := pure <| .ofChoiceInfo { elaborator := .anonymous, stx := getRef }) do
for tree in trees do
pushInfoTree tree
throwErrorWithNestedErrors "overloaded" exs
private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (ellipsis : Bool) (expectedType? : Option Expr) : TermElabM Expr := do

View File

@@ -211,7 +211,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
else
`(bracketedBinderF| {$id $[: $ty?]?})
for id in ids.reverse do
if let some idx := binderIds.findFinIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
if let some idx := binderIds.findIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
binderIds := binderIds.eraseIdx idx
modifiedVarDecls := true
varDeclsNew := varDeclsNew.push ( mkBinder id explicit)

View File

@@ -42,15 +42,16 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
@[builtin_term_elab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
/- `ident.` is ambiguous in Lean, we may try to be completing a declaration name or access a "field". -/
if stx[0].isIdent then
-- Add both an `id` and a `dot` `CompletionInfo` and have the language server figure out which
-- one to use.
addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) ( getLCtx) expectedType?
/- If we can elaborate the identifier successfully, we assume it is a dot-completion. Otherwise, we treat it as
identifier completion with a dangling `.`.
Recall that the server falls back to identifier completion when dot-completion fails. -/
let s saveState
try
let e elabTerm stx[0] none
addDotCompletionInfo stx e expectedType?
catch _ =>
s.restore
addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) ( getLCtx) expectedType?
throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
else
elabPipeCompletion stx expectedType?
@@ -327,7 +328,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
@[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
match stx with
| `(with_annotate_term $stx $e) =>
withTermInfoContext' .anonymous stx (expectedType? := expectedType?) (elabTerm e expectedType?)
withInfoContext' stx (elabTerm e expectedType?) (mkTermInfo .anonymous (expectedType? := expectedType?) stx)
| _ => throwUnsupportedSyntax
private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=

View File

@@ -214,7 +214,7 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
let mut log := log
let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
for ((pos, endPos), traceMsg) in traces' do
let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
return log
@@ -555,11 +555,7 @@ private def getVarDecls (s : State) : Array Syntax :=
instance {α} : Inhabited (CommandElabM α) where
default := throw default
/--
The environment linter framework needs to be able to run linters with the same context
as `liftTermElabM`, so we expose that context as a public function here.
-/
def mkMetaContext : Meta.Context := {
private def mkMetaContext : Meta.Context := {
config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }
}

View File

@@ -49,9 +49,9 @@ invoking ``mkInstImplicitBinders `BarClass foo #[`α, `n, `β]`` gives `` `([Bar
def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array Syntax) :=
forallBoundedTelescope indVal.type indVal.numParams fun xs _ => do
let mut binders := #[]
for h : i in [:xs.size] do
for i in [:xs.size] do
try
let x := xs[i]
let x := xs[i]!
let c mkAppM className #[x]
if ( isTypeCorrect c) then
let argName := argNames[i]!
@@ -86,8 +86,8 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) : TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
let mut letDecls := #[]
for h : i in [:ctx.typeInfos.size] do
let indVal := ctx.typeInfos[i]
for i in [:ctx.typeInfos.size] do
let indVal := ctx.typeInfos[i]!
let auxFunName := ctx.auxFunNames[i]!
let currArgNames mkInductArgNames indVal
let numParams := indVal.numParams

View File

@@ -796,10 +796,10 @@ Note that we are not restricting the macro power since the
actions to be in the same universe.
-/
private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
if elems.size = 0 then
if elems.size == 0 then
mkUnit
else if h : elems.size = 1 then
return elems[0]
else if elems.size == 1 then
return elems[0]!
else
elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back!) fun elem tuple =>
``(MProd.mk $elem $tuple)
@@ -831,10 +831,10 @@ def isDoExpr? (doElem : Syntax) : Option Syntax :=
We use this method when expanding the `for-in` notation.
-/
private def destructTuple (uvars : Array Var) (x : Syntax) (body : Syntax) : MacroM Syntax := do
if uvars.size = 0 then
if uvars.size == 0 then
return body
else if h : uvars.size = 1 then
`(let $(uvars[0]):ident := $x; $body)
else if uvars.size == 1 then
`(let $(uvars[0]!):ident := $x; $body)
else
destruct uvars.toList x body
where
@@ -1314,9 +1314,9 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
else if liftMethodDelimiter k then
return stx
-- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
else if h : args.size >= 2 (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
else if args.size >= 2 && (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
let arg1 expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]
let arg1 expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]!
let args := args.set! 1 arg1
return Syntax.node i k args
else if k == ``Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
@@ -1518,7 +1518,7 @@ mutual
-/
partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
let doForDecls := doFor[1].getSepArgs
if h : doForDecls.size > 1 then
if doForDecls.size > 1 then
/-
Expand
```

View File

@@ -327,18 +327,15 @@ private def toExprCore (t : Tree) : TermElabM Expr := do
| .term _ trees e =>
modifyInfoState (fun s => { s with trees := s.trees ++ trees }); return e
| .binop ref kind f lhs rhs =>
withRef ref <|
withTermInfoContext' .anonymous ref do
mkBinOp (kind == .lazy) f ( toExprCore lhs) ( toExprCore rhs)
withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
mkBinOp (kind == .lazy) f ( toExprCore lhs) ( toExprCore rhs)
| .unop ref f arg =>
withRef ref <|
withTermInfoContext' .anonymous ref do
mkUnOp f ( toExprCore arg)
withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
mkUnOp f ( toExprCore arg)
| .macroExpansion macroName stx stx' nested =>
withRef stx <|
withTermInfoContext' macroName stx <|
withMacroExpansion stx stx' <|
toExprCore nested
withRef stx <| withInfoContext' stx (mkInfo := mkTermInfo macroName stx) do
withMacroExpansion stx stx' do
toExprCore nested
/--
Auxiliary function to decide whether we should coerce `f`'s argument to `maxType` or not.

View File

@@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
where
go initialSnap t commands :=
let snap := t.get
let commands := commands.push snap
let commands := commands.push snap.data
if let some next := snap.nextCmdSnap? then
go initialSnap next.task commands
else
@@ -115,9 +115,9 @@ where
-- snapshots as they subsume any info trees reported incrementally by their children.
let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'
return {
commandState := { snap.finishedSnap.get.cmdState with messages, infoState.trees := trees }
parserState := snap.parserState
cmdPos := snap.parserState.pos
commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees }
parserState := snap.data.parserState
cmdPos := snap.data.parserState.pos
commands := commands.map (·.stx)
inputCtx, initialSnap
}
@@ -164,8 +164,8 @@ def runFrontend
| return ( mkEmptyEnvironment, false)
if let some out := trace.profiler.output.get? opts then
let traceStates := snaps.getAll.map (·.traces)
let profile Firefox.Profile.export mainModuleName.toString startTime traceStates opts
let traceState := cmdState.traceState
let profile Firefox.Profile.export mainModuleName.toString startTime traceState opts
IO.FS.writeFile out <| Json.compress <| toJson profile
let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)

View File

@@ -173,15 +173,15 @@ private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
private def InductiveView.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
if h : views.size > 1 then
let levelNames := views[0].levelNames
if views.size > 1 then
let levelNames := views[0]!.levelNames
for view in views do
unless view.levelNames == levelNames do
throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
private def ElabHeaderResult.checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
if h : rs.size > 1 then
let levelNames := rs[0].levelNames
if rs.size > 1 then
let levelNames := rs[0]!.levelNames
for r in rs do
unless r.levelNames == levelNames do
throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
@@ -433,8 +433,8 @@ where
let mut args := e.getAppArgs
unless args.size params.size do
throwError "unexpected inductive type occurrence{indentExpr e}"
for h : i in [:params.size] do
let param := params[i]
for i in [:params.size] do
let param := params[i]!
let arg := args[i]!
unless ( isDefEq param arg) do
throwError "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
@@ -694,8 +694,8 @@ private def collectLevelParamsInInductive (indTypes : List InductiveType) : Arra
private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr := Id.run do
let levelParams := levelNames.map mkLevelParam;
let mut m : ExprMap Expr := {}
for h : i in [:views.size] do
let view := views[i]
for i in [:views.size] do
let view := views[i]!
let indFVar := indFVars[i]!
m := m.insert indFVar (mkConst view.declName levelParams)
return m
@@ -856,9 +856,9 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
withInductiveLocalDecls rs fun params indFVars => do
trace[Elab.inductive] "indFVars: {indFVars}"
let mut indTypesArray := #[]
for h : i in [:views.size] do
for i in [:views.size] do
let indFVar := indFVars[i]!
Term.addLocalVarInfo views[i].declId indFVar
Term.addLocalVarInfo views[i]!.declId indFVar
let r := rs[i]!
/- At this point, because of `withInductiveLocalDecls`, the only fvars that are in context are the ones related to the first inductive type.
Because of this, we need to replace the fvars present in each inductive type's header of the mutual block with those of the first inductive.

View File

@@ -139,16 +139,12 @@ def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO
def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
info.runMetaM ctx do
let ty : Format
try
Meta.ppExpr ( Meta.inferType info.expr)
catch _ =>
pure "<failed-to-infer-type>"
let ty : Format try
Meta.ppExpr ( Meta.inferType info.expr)
catch _ =>
pure "<failed-to-infer-type>"
return f!"{← Meta.ppExpr info.expr} {if info.isBinder then "(isBinder := true) " else ""}: {ty} @ {formatElabInfo ctx info.toElabInfo}"
def PartialTermInfo.format (ctx : ContextInfo) (info : PartialTermInfo) : Format :=
f!"Partial term @ {formatElabInfo ctx info.toElabInfo}"
def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
match info with
| .dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
@@ -195,13 +191,9 @@ def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format
def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
f!"Choice @ {formatElabInfo ctx info.toElabInfo}"
def Info.format (ctx : ContextInfo) : Info IO Format
| ofTacticInfo i => i.format ctx
| ofTermInfo i => i.format ctx
| ofPartialTermInfo i => pure <| i.format ctx
| ofCommandInfo i => i.format ctx
| ofMacroExpansionInfo i => i.format ctx
| ofOptionInfo i => i.format ctx
@@ -212,12 +204,10 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
| ofFVarAliasInfo i => pure <| i.format
| ofFieldRedeclInfo i => pure <| i.format ctx
| ofOmissionInfo i => i.format ctx
| ofChoiceInfo i => pure <| i.format ctx
def Info.toElabInfo? : Info Option ElabInfo
| ofTacticInfo i => some i.toElabInfo
| ofTermInfo i => some i.toElabInfo
| ofPartialTermInfo i => some i.toElabInfo
| ofCommandInfo i => some i.toElabInfo
| ofMacroExpansionInfo _ => none
| ofOptionInfo _ => none
@@ -228,7 +218,6 @@ def Info.toElabInfo? : Info → Option ElabInfo
| ofFVarAliasInfo _ => none
| ofFieldRedeclInfo _ => none
| ofOmissionInfo i => some i.toElabInfo
| ofChoiceInfo i => some i.toElabInfo
/--
Helper function for propagating the tactic metavariable context to its children nodes.
@@ -322,36 +311,24 @@ def realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name ×
addConstInfo ref n
return ns
/--
Adds a node containing the `InfoTree`s generated by `x` to the `InfoTree`s in `m`.
/-- Use this to descend a node on the infotree that is being built.
If `x` succeeds and `mkInfo` yields an `Info`, the `InfoTree`s of `x` become subtrees of a node
containing the `Info` produced by `mkInfo`, which is then added to the `InfoTree`s in `m`.
If `x` succeeds and `mkInfo` yields an `MVarId`, the `InfoTree`s of `x` are discarded and a `hole`
node is added to the `InfoTree`s in `m`.
If `x` fails, the `InfoTree`s of `x` become subtrees of a node containing the `Info` produced by
`mkInfoOnError`, which is then added to the `InfoTree`s in `m`.
The `InfoTree`s in `m` are reset before `x` is executed and restored with the addition of a new tree
after `x` is executed.
-/
def withInfoContext'
[MonadFinally m]
(x : m α)
(mkInfo : α m (Sum Info MVarId))
(mkInfoOnError : m Info) :
m α := do
It saves the current list of trees `t₀` and resets it and then runs `x >>= mkInfo`, producing either an `i : Info` or a hole id.
Running `x >>= mkInfo` will modify the trees state and produce a new list of trees `t₁`.
In the `i : Info` case, `t₁` become the children of a node `node i t₁` that is appended to `t₀`.
-/
def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α m (Sum Info MVarId)) : m α := do
if ( getInfoState).enabled then
let treesSaved getResetInfoTrees
Prod.fst <$> MonadFinally.tryFinally' x fun a? => do
let info do
match a? with
| none => pure <| .inl <| mkInfoOnError
| some a => mkInfo a
modifyInfoTrees fun trees =>
match info with
| Sum.inl info => treesSaved.push <| InfoTree.node info trees
| Sum.inr mvarId => treesSaved.push <| InfoTree.hole mvarId
match a? with
| none => modifyInfoTrees fun _ => treesSaved
| some a =>
let info mkInfo a
modifyInfoTrees fun trees =>
match info with
| Sum.inl info => treesSaved.push <| InfoTree.node info trees
| Sum.inr mvarId => treesSaved.push <| InfoTree.hole mvarId
else
x

View File

@@ -70,18 +70,6 @@ structure TermInfo extends ElabInfo where
isBinder : Bool := false
deriving Inhabited
/--
Used instead of `TermInfo` when a term couldn't successfully be elaborated,
and so there is no complete expression available.
The main purpose of `PartialTermInfo` is to ensure that the sub-`InfoTree`s of a failed elaborator
are retained so that they can still be used in the language server.
-/
structure PartialTermInfo extends ElabInfo where
lctx : LocalContext -- The local context when the term was elaborated.
expectedType? : Option Expr
deriving Inhabited
structure CommandInfo extends ElabInfo where
deriving Inhabited
@@ -91,7 +79,7 @@ inductive CompletionInfo where
| dot (termInfo : TermInfo) (expectedType? : Option Expr)
| id (stx : Syntax) (id : Name) (danglingDot : Bool) (lctx : LocalContext) (expectedType? : Option Expr)
| dotId (stx : Syntax) (id : Name) (lctx : LocalContext) (expectedType? : Option Expr)
| fieldId (stx : Syntax) (id : Option Name) (lctx : LocalContext) (structName : Name)
| fieldId (stx : Syntax) (id : Name) (lctx : LocalContext) (structName : Name)
| namespaceId (stx : Syntax)
| option (stx : Syntax)
| endSection (stx : Syntax) (scopeNames : List String)
@@ -177,18 +165,10 @@ regular delaboration settings.
structure OmissionInfo extends TermInfo where
reason : String
/--
Indicates that all overloaded elaborators failed. The subtrees of a `ChoiceInfo` node are the
partial `InfoTree`s of those failed elaborators. Retaining these partial `InfoTree`s helps
the language server provide interactivity even when all overloaded elaborators failed.
-/
structure ChoiceInfo extends ElabInfo where
/-- Header information for a node in `InfoTree`. -/
inductive Info where
| ofTacticInfo (i : TacticInfo)
| ofTermInfo (i : TermInfo)
| ofPartialTermInfo (i : PartialTermInfo)
| ofCommandInfo (i : CommandInfo)
| ofMacroExpansionInfo (i : MacroExpansionInfo)
| ofOptionInfo (i : OptionInfo)
@@ -199,7 +179,6 @@ inductive Info where
| ofFVarAliasInfo (i : FVarAliasInfo)
| ofFieldRedeclInfo (i : FieldRedeclInfo)
| ofOmissionInfo (i : OmissionInfo)
| ofChoiceInfo (i : ChoiceInfo)
deriving Inhabited
/-- The InfoTree is a structure that is generated during elaboration and used

View File

@@ -87,15 +87,12 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
view.decls.mapM fun view => do
forallBoundedTelescope view.type view.binderIds.size fun xs type => do
-- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
for h : i in [0:view.binderIds.size] do
addLocalVarInfo view.binderIds[i] xs[i]!
for i in [0:view.binderIds.size] do
addLocalVarInfo view.binderIds[i]! xs[i]!
withDeclName view.declName do
withInfoContext' view.valStx
(mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·))
(mkInfoOnError := (pure <| mkBodyInfo view.valStx none))
do
let value elabTermEnsuringType view.valStx type
mkLambdaFVars xs value
withInfoContext' view.valStx (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·)) do
let value elabTermEnsuringType view.valStx type
mkLambdaFVars xs value
private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
let letRecsToLiftCurr := ( get).letRecsToLift

View File

@@ -282,8 +282,8 @@ where
let dArg := dArgs[i]!
unless ( isDefEq tArg dArg) do
return i :: ( goType tArg dArg)
for h : i in [info.numParams : tArgs.size] do
let tArg := tArgs[i]
for i in [info.numParams : tArgs.size] do
let tArg := tArgs[i]!
let dArg := dArgs[i]!
unless ( isDefEq tArg dArg) do
return i :: ( goIndex tArg dArg)
@@ -644,7 +644,7 @@ where
if inaccessible? p |>.isSome then
return mkMData k ( withReader (fun _ => true) (go b))
else if let some (stx, p) := patternWithRef? p then
Elab.withInfoContext' (go p) (mkInfoOnError := mkPartialTermInfo .anonymous stx) fun p => do
Elab.withInfoContext' (go p) fun p => do
/- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/
mkTermInfo Name.anonymous stx p (isBinder := p.isFVar && !( read))
else

View File

@@ -283,7 +283,7 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
loop 0 #[]
private def expandWhereStructInst : Macro
| whereStx@`(Parser.Command.whereStructInst|where%$whereTk $[$decls:letDecl];* $[$whereDecls?:whereDecls]?) => do
| `(Parser.Command.whereStructInst|where $[$decls:letDecl];* $[$whereDecls?:whereDecls]?) => do
let letIdDecls decls.mapM fun stx => match stx with
| `(letDecl|$_decl:letPatDecl) => Macro.throwErrorAt stx "patterns are not allowed here"
| `(letDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl (useExplicit := false)
@@ -300,30 +300,7 @@ private def expandWhereStructInst : Macro
`(structInstField|$id:ident := $val)
| stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
| _ => Macro.throwUnsupported
let startOfStructureTkInfo : SourceInfo :=
match whereTk.getPos? with
| some pos => .synthetic pos pos.byteIdx + 1 true
| none => .none
-- Position the closing `}` at the end of the trailing whitespace of `where $[$_:letDecl];*`.
-- We need an accurate range of the generated structure instance in the generated `TermInfo`
-- so that we can determine the expected type in structure field completion.
let structureStxTailInfo :=
whereStx[1].getTailInfo?
<|> whereStx[0].getTailInfo?
let endOfStructureTkInfo : SourceInfo :=
match structureStxTailInfo with
| some (SourceInfo.original _ _ trailing _) =>
let tokenPos := trailing.str.prev trailing.stopPos
let tokenEndPos := trailing.stopPos
.synthetic tokenPos tokenEndPos true
| _ => .none
let body `(structInst| { $structInstFields,* })
let body := body.raw.setInfo <|
match startOfStructureTkInfo.getPos?, endOfStructureTkInfo.getTailPos? with
| some startPos, some endPos => .synthetic startPos endPos true
| _, _ => .none
match whereDecls? with
| some whereDecls => expandWhereDecls whereDecls body
| none => return body
@@ -440,15 +417,12 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
-- Store instantiated body in info tree for the benefit of the unused variables linter
-- and other metaprograms that may want to inspect it without paying for the instantiation
-- again
withInfoContext' valStx
(mkInfo := (pure <| .inl <| mkBodyInfo valStx ·))
(mkInfoOnError := (pure <| mkBodyInfo valStx none))
do
-- synthesize mvars here to force the top-level tactic block (if any) to run
let val elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-- leads to more section variables being included than necessary
instantiateMVarsProfiling val
withInfoContext' valStx (mkInfo := (pure <| .inl <| mkBodyInfo valStx ·)) do
-- synthesize mvars here to force the top-level tactic block (if any) to run
let val elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-- leads to more section variables being included than necessary
instantiateMVarsProfiling val
let val mkLambdaFVars xs val
if linter.unusedSectionVars.get ( getOptions) && !header.type.hasSorry && !val.hasSorry then
let unusedVars vars.filterMapM fun var => do

View File

@@ -49,12 +49,12 @@ private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) :
exs := exs.push ex
if exs.size == nss.length then
withRef idStx do
if h : exs.size = 1 then
throw exs[0]
if exs.size == 1 then
throw exs[0]!
else
throwErrorWithNestedErrors "failed to open" exs
if h : result.size = 1 then
return result[0]
if result.size == 1 then
return result[0]!
else
withRef idStx do throwError "ambiguous identifier '{idStx.getId}', possible interpretations: {result.map mkConst}"

View File

@@ -332,9 +332,9 @@ where
else
let accessible := isNextArgAccessible ctx
let (d, ctx) := getNextParam ctx
match ctx.namedArgs.findFinIdx? fun namedArg => namedArg.name == d.1 with
match ctx.namedArgs.findIdx? fun namedArg => namedArg.name == d.1 with
| some idx =>
let arg := ctx.namedArgs[idx]
let arg := ctx.namedArgs[idx]!
let ctx := { ctx with namedArgs := ctx.namedArgs.eraseIdx idx }
let ctx pushNewArg accessible ctx arg.val
processCtorAppContext ctx

View File

@@ -244,8 +244,8 @@ def checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit := do
lambdaTelescope preDef.value fun xs _ => return xs.size
forallBoundedTelescope preDefs[0]!.type arities[0]! fun _ type₀ => do
let u₀ getLevel type₀
for h : i in [1:preDefs.size] do
forallBoundedTelescope preDefs[i].type arities[i]! fun _ typeᵢ =>
for i in [1:preDefs.size] do
forallBoundedTelescope preDefs[i]!.type arities[i]! fun _ typeᵢ =>
unless isLevelDefEq u₀ ( getLevel typeᵢ) do
withOptions (fun o => pp.sanitizeNames.set o false) do
throwError m!"invalid mutual definition, result types must be in the same universe " ++

View File

@@ -50,9 +50,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
go mvarId
else if let some mvarId whnfReducibleLHS? mvarId then
go mvarId
else
let ctx Simp.mkContext (config := { dsimp := false })
match ( simpTargetStar mvarId ctx (simprocs := {})).1 with
else match ( simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
| TacticResultCNM.closed => return ()
| TacticResultCNM.modified mvarId => go mvarId
| TacticResultCNM.noChange =>

View File

@@ -292,9 +292,9 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
let packedFTypes inferArgumentTypesN positions.size brecOn
let packedFArgs positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
let brecOn := mkAppN brecOn packedFArgs
let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.indexOf? fnIdx
let some poss := positions.find? (·.contains fnIdx)
| throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
let brecOn PProdN.proj size idx brecOn
let brecOn PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn
mkLambdaFVars ys (mkAppN brecOn otherArgs)
end Lean.Elab.Structural

View File

@@ -45,9 +45,7 @@ where
go mvarId
else if let some mvarId simpIf? mvarId then
go mvarId
else
let ctx Simp.mkContext
match ( simpTargetStar mvarId ctx (simprocs := {})).1 with
else match ( simpTargetStar mvarId {} (simprocs := {})).1 with
| TacticResultCNM.closed => return ()
| TacticResultCNM.modified mvarId => go mvarId
| TacticResultCNM.noChange =>

View File

@@ -243,7 +243,7 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
recArgInfoss := recArgInfoss.push recArgInfos
-- Put non-indices first
recArgInfoss := recArgInfoss.map nonIndicesFirst
trace[Elab.definition.structural] "recArgInfos:{indentD (.joinSep (recArgInfoss.flatten.toList.map (repr ·)) Format.line)}"
trace[Elab.definition.structural] "recArgInfoss: {recArgInfoss.map (·.map (·.recArgPos))}"
-- Inductive groups to consider
let groups inductiveGroups recArgInfoss.flatten
trace[Elab.definition.structural] "inductive groups: {groups}"

View File

@@ -27,7 +27,7 @@ constituents.
structure IndGroupInfo where
all : Array Name
numNested : Nat
deriving BEq, Inhabited, Repr
deriving BEq, Inhabited
def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where
all := indInfo.all.toArray
@@ -56,7 +56,7 @@ mutual structural recursion on such incompatible types.
structure IndGroupInst extends IndGroupInfo where
levels : List Level
params : Array Expr
deriving Inhabited, Repr
deriving Inhabited
def IndGroupInst.toMessageData (igi : IndGroupInst) : MessageData :=
mkAppN (.const igi.all[0]! igi.levels) igi.params

View File

@@ -23,9 +23,9 @@ structure RecArgInfo where
fnName : Name
/-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/
numFixed : Nat
/-- position (counted including fixed prefix) of the argument we are recursing on -/
/-- position of the argument (counted including fixed prefix) we are recursing on -/
recArgPos : Nat
/-- position (counted including fixed prefix) of the indices of the inductive datatype we are recursing on -/
/-- position of the indices (counted including fixed prefix) of the inductive datatype indices we are recursing on -/
indicesPos : Array Nat
/-- The inductive group (with parameters) of the argument's type -/
indGroupInst : IndGroupInst
@@ -34,23 +34,20 @@ structure RecArgInfo where
If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
-/
indIdx : Nat
deriving Inhabited, Repr
deriving Inhabited
/--
If `xs` are the parameters of the functions (excluding fixed prefix), partitions them
into indices and major arguments, and other parameters.
-/
def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
-- First indices and major arg, using the order they appear in `info.indicesPos`
let mut indexMajorArgs := #[]
let indexMajorPos := info.indicesPos.push info.recArgPos
for j in indexMajorPos do
assert! info.numFixed j && j - info.numFixed < xs.size
indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]!
-- Then the other arguments, in the order they appear in `xs`
let mut otherArgs := #[]
for h : i in [:xs.size] do
unless indexMajorPos.contains (i + info.numFixed) do
let j := i + info.numFixed
if j = info.recArgPos || info.indicesPos.contains j then
indexMajorArgs := indexMajorArgs.push xs[i]
else
otherArgs := otherArgs.push xs[i]
return (indexMajorArgs, otherArgs)

View File

@@ -53,10 +53,10 @@ def TerminationArgument.elab (funName : Name) (type : Expr) (arity extraParams :
(hint : TerminationBy) : TermElabM TerminationArgument := withDeclName funName do
assert! extraParams arity
if h : hint.vars.size > extraParams then
if hint.vars.size > extraParams then
let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
m!"{funName} only binds {parameters extraParams}."
if let `($ident:ident) := hint.vars[0] then
if let `($ident:ident) := hint.vars[0]! then
if ident.getId.isSuffixOf funName then
msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
"expects the function name here.)"

View File

@@ -90,10 +90,10 @@ lambda of `value`, and throws appropriate errors.
-/
def TerminationBy.checkVars (funName : Name) (extraParams : Nat) (tb : TerminationBy) : MetaM Unit := do
unless tb.synthetic do
if h : tb.vars.size > extraParams then
if tb.vars.size > extraParams then
let mut msg := m!"{parameters tb.vars.size} bound in `termination_by`, but the body of " ++
m!"{funName} only binds {parameters extraParams}."
if let `($ident:ident) := tb.vars[0] then
if let `($ident:ident) := tb.vars[0]! then
if ident.getId.isSuffixOf funName then
msg := msg ++ m!" (Since Lean v4.6.0, the `termination_by` clause no longer " ++
"expects the function name here.)"

View File

@@ -57,9 +57,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
go mvarId
else if let some mvarId whnfReducibleLHS? mvarId then
go mvarId
else
let ctx Simp.mkContext (config := { dsimp := false })
match ( simpTargetStar mvarId ctx (simprocs := {})).1 with
else match ( simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
| TacticResultCNM.closed => return ()
| TacticResultCNM.modified mvarId => go mvarId
| TacticResultCNM.noChange =>

View File

@@ -227,7 +227,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsP
-- decreasing goals when the function has only one non fixed argument.
-- This renaming is irrelevant if the function has multiple non fixed arguments. See `process*` functions above.
let lctx := ( getLCtx).setUserName x.fvarId! varName
withLCtx' lctx do
withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
let F := xs[1]!
let val := preDef.value.beta (prefixArgs.push x)
let val processSumCasesOn x F val fun x F val => do

View File

@@ -166,7 +166,7 @@ def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool
def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
let mut lctx getLCtx
for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
withLCtx' lctx k
withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
/-- Create one measure for each (eligible) parameter of the given predefintion. -/
def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)

View File

@@ -21,8 +21,8 @@ open Meta
private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) : TermElabM Unit := do
let us := preDefNonRec.levelParams.map mkLevelParam
let all := preDefs.toList.map (·.declName)
for h : fidx in [:preDefs.size] do
let preDef := preDefs[fidx]
for fidx in [:preDefs.size] do
let preDef := preDefs[fidx]!
let value forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do
let value := mkAppN (mkConst preDefNonRec.declName us) xs
let value argsPacker.curryProj value fidx
@@ -87,7 +87,7 @@ def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Ar
xs.mapM (·.fvarId!.getUserName)
def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
let termArgs? := termArg?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
let termArgs? := termArg?s.sequenceMap id -- Either all or none, checked by `elabTerminationByHints`
let preDefs preDefs.mapM fun preDef =>
return { preDef with value := ( preprocess preDef.value) }
let (fixedPrefixSize, argsPacker, unaryPreDef) withoutModifyingEnv do

View File

@@ -40,7 +40,7 @@ private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames
return TransformStep.done e
let declName := f.constName!
let us := f.constLevels!
if let some fidx := funNames.indexOf? declName then
if let some fidx := funNames.getIdx? declName then
let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
let e' withAppN arity e fun args => do
let fixedArgs := args[:fixedPrefix]

View File

@@ -22,7 +22,7 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
m := m ++ ", " ++ toMessageData u
return m ++ "}"
private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
let m : MessageData :=
match ( getReducibilityStatus id) with
| ReducibilityStatus.irreducible => "@[irreducible] "
@@ -38,13 +38,11 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
let (m, id) := match privateToUserName? id with
| some id => (m ++ "private ", id)
| none => (m, id)
if sig then
return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}"
else
return m!"{m}{kind}"
let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type
pure m
private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData :=
mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig)
private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=
mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe)
private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
let m mkHeader kind id levelParams type safety
@@ -67,63 +65,32 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
logInfo m
/--
Computes the origin of a field. Returns its projection function at the origin.
Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin.
-/
private partial def getFieldOrigin (structName field : Name) : MetaM Name := do
let env getEnv
for parent in getStructureParentInfo env structName do
if (findField? env parent.structName field).isSome then
return getFieldOrigin parent.structName field
let some fi := getFieldInfo? env structName field
| throwError "no such field {field} in {structName}"
return fi.projFn
open Meta in
private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
(isUnsafe : Bool) : CommandElabM Unit := do
let env getEnv
let kind := if isClass env id then "class" else "structure"
let header mkHeader' kind id levelParams type isUnsafe (sig := false)
liftTermElabM <| forallTelescope ( getConstInfo id).type fun params _ =>
let s := Expr.const id (levelParams.map .param)
withLocalDeclD `self (mkAppN s params) fun self => do
let mut m : MessageData := header
-- Signature
m := m ++ " " ++ .ofFormatWithInfosM do
let (stx, infos) PrettyPrinter.delabCore s (delab := PrettyPrinter.Delaborator.delabConstWithSignature)
pure PrettyPrinter.ppTerm stx, infos
m := m ++ Format.line ++ m!"number of parameters: {numParams}"
-- Parents
let parents := getStructureParentInfo env id
unless parents.isEmpty do
m := m ++ Format.line ++ "parents:"
for parent in parents do
let ptype inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self)
m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}"
-- Fields
let fields := getStructureFieldsFlattened env id (includeSubobjectFields := false)
if fields.isEmpty then
m := m ++ Format.line ++ "fields: (none)"
else
m := m ++ Format.line ++ "fields:"
(ctor : Name) (fields : Array Name) (isUnsafe : Bool) (isClass : Bool) : CommandElabM Unit := do
let kind := if isClass then "class" else "structure"
let mut m mkHeader' kind id levelParams type isUnsafe
m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
m := m ++ Format.line ++ "constructor:"
let cinfo getConstInfo ctor
m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
m := m ++ Format.line ++ "fields:" ++ ( doFields)
logInfo m
where
doFields := liftTermElabM do
forallTelescope ( getConstInfo id).type fun params _ =>
withLocalDeclD `self (mkAppN (Expr.const id (levelParams.map .param)) params) fun self => do
let params := params.push self
let mut m : MessageData := ""
for field in fields do
let some source := findField? env id field | panic! "missing structure field info"
let proj getFieldOrigin source field
let modifier := if isPrivateName proj then "private " else ""
let ftype inferType ( mkProjection self field)
m := m ++ indentD (m!"{modifier}{.ofConstName proj (fullNames := true)} : {ftype}")
-- Constructor
let cinfo := getStructureCtor ( getEnv) id
let ctorModifier := if isPrivateName cinfo.name then "private " else ""
m := m ++ Format.line ++ "constructor:" ++ indentD (ctorModifier ++ .signature cinfo.name)
-- Resolution order
let resOrder getStructureResolutionOrder id
if resOrder.size > 1 then
m := m ++ Format.line ++ "resolution order:"
++ indentD (MessageData.joinSep (resOrder.map (.ofConstName · (fullNames := true))).toList ", ")
logInfo m
match getProjFnForField? ( getEnv) id field with
| some proj =>
let field : Format := if isPrivateName proj then "private " ++ toString field else toString field
let cinfo getConstInfo proj
let ftype instantiateForall cinfo.type params
m := m ++ Format.line ++ field ++ " : " ++ ftype
| none => panic! "missing structure field info"
addMessageContext m
private def printIdCore (id : Name) : CommandElabM Unit := do
let env getEnv
@@ -136,10 +103,11 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
| ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
| ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
| ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
if isStructure env id then
printStructure id us numParams t u
else
printInduct id us numParams t ctors u
match getStructureInfo? env id with
| some { fieldNames, .. } =>
let [ctor] := ctors | panic! "structures have only one constructor"
printStructure id us numParams t ctor fieldNames u (isClass env id)
| none => printInduct id us numParams t ctors u
| none => throwUnknownId id
private def printId (id : Syntax) : CommandElabM Unit := do

View File

@@ -58,7 +58,7 @@ partial def mkTuple : Array Syntax → TermElabM Syntax
| #[] => `(Unit.unit)
| #[e] => return e
| es => do
let stx mkTuple (es.eraseIdxIfInBounds 0)
let stx mkTuple (es.eraseIdx 0)
`(Prod.mk $(es[0]!) $stx)
def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name × List String) :=
@@ -434,7 +434,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
else mkNullNode contents
-- We use `no_error_if_unused%` in auxiliary `match`-syntax to avoid spurious error messages,
-- the outer `match` is checking for unused alternatives
`(match ($(discrs).mapM fun
`(match ($(discrs).sequenceMap fun
| `($contents) => no_error_if_unused% some $tuple
| _ => no_error_if_unused% none) with
| some $resId => $yes

View File

@@ -11,40 +11,21 @@ import Lean.Elab.App
import Lean.Elab.Binders
import Lean.PrettyPrinter
/-!
# Structure instance elaborator
A *structure instance* is notation to construct a term of a `structure`.
Examples: `{ x := 2, y.z := true }`, `{ s with cache := c' }`, and `{ s with values[2] := v }`.
Structure instances are the preferred way to invoke a `structure`'s constructor,
since they hide Lean implementation details such as whether parents are represented as subobjects,
and also they do correct processing of default values, which are complicated due to the fact that `structure`s can override default values of their parents.
This module elaborates structure instance notation.
Note that the `where` syntax to define structures (`Lean.Parser.Command.whereStructInst`)
macro expands into the structure instance notation elaborated by this module.
-/
namespace Lean.Elab.Term.StructInst
open Meta
open TSyntax.Compat
/-!
Recall that structure instances are of the form:
```
"{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
>> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
>> optEllipsis
>> optional (" : " >> termParser)
>> " }"
```
/-
Structure instances are of the form:
"{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
>> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
>> optEllipsis
>> optional (" : " >> termParser)
>> " }"
-/
/--
Transforms structure instances such as `{ x := 0 : Foo }` into `({ x := 0 } : Foo)`.
Structure instance notation makes use of the expected type.
-/
@[builtin_macro Lean.Parser.Term.structInst] def expandStructInstExpectedType : Macro := fun stx =>
let expectedArg := stx[4]
if expectedArg.isNone then
@@ -54,10 +35,7 @@ Structure instance notation makes use of the expected type.
let stxNew := stx.setArg 4 mkNullNode
`(($stxNew : $expected))
/--
Expands field abbreviation notation.
Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }`.
-/
/-- Expand field abbreviations. Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }` -/
@[builtin_macro Lean.Parser.Term.structInst] def expandStructInstFieldAbbrev : Macro
| `({ $[$srcs,* with]? $fields,* $[..%$ell]? $[: $ty]? }) =>
if fields.getElems.raw.any (·.getKind == ``Lean.Parser.Term.structInstFieldAbbrev) then do
@@ -71,12 +49,9 @@ Example: `{ x, y := 0 }` expands to `{ x := x, y := 0 }`.
| _ => Macro.throwUnsupported
/--
If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable,
expands into `let __src := sᵢ; { ..., __src, ... with ... }`.
The significance of `__src` is that the variable is treated as an implementation-detail local variable,
which can be unfolded by `simp` when `zetaDelta := false`.
If `stx` is of the form `{ s₁, ..., sₙ with ... }` and `sᵢ` is not a local variable, expand into `let src := sᵢ; { ..., src, ... with ... }`.
Note that this one is not a `Macro` because we need to access the local context.
Note that this one is not a `Macro` because we need to access the local context.
-/
private def expandNonAtomicExplicitSources (stx : Syntax) : TermElabM (Option Syntax) := do
let sourcesOpt := stx[1]
@@ -125,44 +100,27 @@ where
let r go sources (sourcesNew.push sourceNew)
`(let __src := $source; $r)
/--
An *explicit source* is one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`.
-/
structure ExplicitSourceView where
/-- The syntax of the explicit source. -/
structure ExplicitSourceInfo where
stx : Syntax
/-- The name of the structure for the type of the explicit source. -/
structName : Name
deriving Inhabited
/--
A view of the sources of fields for the structure instance notation.
-/
structure SourcesView where
/-- Explicit sources (i.e., one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`). -/
explicit : Array ExplicitSourceView
/-- The syntax for a trailing `..`. This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications. -/
implicit : Option Syntax
structure Source where
explicit : Array ExplicitSourceInfo -- `s₁ ... sₙ with`
implicit : Option Syntax -- `..`
deriving Inhabited
/-- Returns `true` if the structure instance has no sources (neither explicit sources nor a `..`). -/
def SourcesView.isNone : SourcesView Bool
def Source.isNone : Source Bool
| { explicit := #[], implicit := none } => true
| _ => false
/--
Given an array of explicit sources, returns syntax of the form
`optional (atomic (sepBy1 termParser ", " >> " with ")`
-/
/-- `optional (atomic (sepBy1 termParser ", " >> " with ")` -/
private def mkSourcesWithSyntax (sources : Array Syntax) : Syntax :=
let ref := sources[0]!
let stx := Syntax.mkSep sources (mkAtomFrom ref ", ")
mkNullNode #[stx, mkAtomFrom ref "with "]
/--
Creates a structure source view from structure instance notation.
-/
private def getStructSources (structStx : Syntax) : TermElabM SourcesView :=
private def getStructSource (structStx : Syntax) : TermElabM Source :=
withRef structStx do
let explicitSource := structStx[1]
let implicitSource := structStx[3]
@@ -180,13 +138,13 @@ private def getStructSources (structStx : Syntax) : TermElabM SourcesView :=
return { explicit, implicit }
/--
We say a structure instance notation is a "modifyOp" if it contains only a single array update.
```lean
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
```
We say a `{ ... }` notation is a `modifyOp` if it contains only one
```
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
```
-/
private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
let s? stx[2][0].getSepArgs.foldlM (init := none) fun s? arg => do
let s? stx[2].getSepArgs.foldlM (init := none) fun s? arg => do
/- arg is of the form `structInstFieldAbbrev <|> structInstField` -/
if arg.getKind == ``Lean.Parser.Term.structInstField then
/- Remark: the syntax for `structInstField` is
@@ -219,11 +177,7 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
| none => return none
| some s => if s[0][0].getKind == ``Lean.Parser.Term.structInstArrayRef then return s? else return none
/--
Given a `stx` that is a structure instance notation that's a modifyOp (according to `isModifyOp?`), elaborates it.
Only supports structure instances with a single source.
-/
private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSourceView) (expectedType? : Option Expr) : TermElabM Expr := do
private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSourceInfo) (expectedType? : Option Expr) : TermElabM Expr := do
if sources.size > 1 then
throwError "invalid \{...} notation, multiple sources and array update is not supported."
let cont (val : Syntax) : TermElabM Expr := do
@@ -245,18 +199,17 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
let valField := modifyOp.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[valFirst, valRest]
let valSource := mkSourcesWithSyntax #[s]
let val := stx.setArg 1 valSource
let val := val.setArg 2 <| mkNode ``Parser.Term.structInstFields #[mkNullNode #[valField]]
let val := val.setArg 2 <| mkNullNode #[valField]
trace[Elab.struct.modifyOp] "{stx}\nval: {val}"
cont val
/--
Gets the structure name for the structure instance from the expected type and the sources.
This method tries to postpone execution if the expected type is not available.
Get structure name.
This method triest to postpone execution if the expected type is not available.
If the expected type is available and it is a structure, then we use it.
Otherwise, we use the type of the first source.
-/
private def getStructName (expectedType? : Option Expr) (sourceView : SourcesView) : TermElabM Name := do
If the expected type is available and it is a structure, then we use it.
Otherwise, we use the type of the first source. -/
private def getStructName (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
tryPostponeIfNoneOrMVar expectedType?
let useSource : Unit TermElabM Name := fun _ => do
unless sourceView.explicit.isEmpty do
@@ -273,7 +226,7 @@ private def getStructName (expectedType? : Option Expr) (sourceView : SourcesVie
unless isStructure ( getEnv) constName do
throwError "invalid \{...} notation, structure type expected{indentExpr expectedType}"
return constName
| _ => useSource ()
| _ => useSource ()
where
throwUnknownExpectedType :=
throwError "invalid \{...} notation, expected type is not known"
@@ -284,92 +237,72 @@ where
else
throwError "invalid \{...} notation, {kind} type is not of the form (C ...){indentExpr type}"
/--
A component of a left-hand side for a field appearing in structure instance syntax.
-/
inductive FieldLHS where
/-- A name component for a field left-hand side. For example, `x` and `y` in `{ x.y := v }`. -/
| fieldName (ref : Syntax) (name : Name)
/-- A numeric index component for a field left-hand side. For example `3` in `{ x.3 := v }`. -/
| fieldIndex (ref : Syntax) (idx : Nat)
/-- An array indexing component for a field left-hand side. For example `[3]` in `{ arr[3] := v }`. -/
| modifyOp (ref : Syntax) (index : Syntax)
deriving Inhabited
instance : ToFormat FieldLHS where
format
| .fieldName _ n => format n
| .fieldIndex _ i => format i
| .modifyOp _ i => "[" ++ i.prettyPrint ++ "]"
instance : ToFormat FieldLHS := fun lhs =>
match lhs with
| .fieldName _ n => format n
| .fieldIndex _ i => format i
| .modifyOp _ i => "[" ++ i.prettyPrint ++ "]"
/--
`FieldVal StructInstView` is a representation of a field value in the structure instance.
-/
inductive FieldVal (σ : Type) where
/-- A `term` to use for the value of the field. -/
| term (stx : Syntax) : FieldVal σ
/-- A `StructInstView` to use for the value of a subobject field. -/
| term (stx : Syntax) : FieldVal σ
| nested (s : σ) : FieldVal σ
/-- A field that was not provided and should be synthesized using default values. -/
| default : FieldVal σ
| default : FieldVal σ -- mark that field must be synthesized using default value
deriving Inhabited
/--
`Field StructInstView` is a representation of a field in the structure instance.
-/
structure Field (σ : Type) where
/-- The whole field syntax. -/
ref : Syntax
/-- The LHS decomposed into components. -/
lhs : List FieldLHS
/-- The value of the field. -/
val : FieldVal σ
/-- The elaborated field value, filled in at `elabStruct`.
Missing fields use a metavariable for the elaborated value and are later solved for in `DefaultFields.propagate`. -/
expr? : Option Expr := none
deriving Inhabited
/--
Returns if the field has a single component in its LHS.
-/
def Field.isSimple {σ} : Field σ Bool
| { lhs := [_], .. } => true
| _ => false
/--
The view for structure instance notation.
-/
structure StructInstView where
/-- The syntax for the whole structure instance. -/
ref : Syntax
/-- The name of the structure for the type of the structure instance. -/
structName : Name
/-- Used for default values, to propagate structure type parameters. It is initially empty, and then set at `elabStruct`. -/
params : Array (Name × Expr)
/-- The fields of the structure instance. -/
fields : List (Field StructInstView)
/-- The additional sources for fields for the structure instance. -/
sources : SourcesView
inductive Struct where
/-- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/
| mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source)
deriving Inhabited
/-- Abbreviation for the type of `StructInstView.fields`, namely `List (Field StructInstView)`. -/
abbrev Fields := List (Field StructInstView)
abbrev Fields := List (Field Struct)
def Struct.ref : Struct Syntax
| ref, _, _, _, _ => ref
def Struct.structName : Struct Name
| _, structName, _, _, _ => structName
def Struct.params : Struct Array (Name × Expr)
| _, _, params, _, _ => params
def Struct.fields : Struct Fields
| _, _, _, fields, _ => fields
def Struct.source : Struct Source
| _, _, _, _, s => s
/-- `true` iff all fields of the given structure are marked as `default` -/
partial def StructInstView.allDefault (s : StructInstView) : Bool :=
partial def Struct.allDefault (s : Struct) : Bool :=
s.fields.all fun { val := val, .. } => match val with
| .term _ => false
| .default => true
| .nested s => allDefault s
def formatField (formatStruct : StructInstView Format) (field : Field StructInstView) : Format :=
def formatField (formatStruct : Struct Format) (field : Field Struct) : Format :=
Format.joinSep field.lhs " . " ++ " := " ++
match field.val with
| .term v => v.prettyPrint
| .nested s => formatStruct s
| .default => "<default>"
partial def formatStruct : StructInstView Format
partial def formatStruct : Struct Format
| _, _, _, fields, source =>
let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", "
let implicitFmt := if source.implicit.isSome then " .. " else ""
@@ -378,39 +311,31 @@ partial def formatStruct : StructInstView → Format
else
"{" ++ format (source.explicit.map (·.stx)) ++ " with " ++ fieldsFmt ++ implicitFmt ++ "}"
instance : ToFormat StructInstView := formatStruct
instance : ToString StructInstView := toString format
instance : ToFormat Struct := formatStruct
instance : ToString Struct := toString format
instance : ToFormat (Field StructInstView) := formatField formatStruct
instance : ToString (Field StructInstView) := toString format
/--
Converts a `FieldLHS` back into syntax. This assumes the `ref` fields have the correct structure.
instance : ToFormat (Field Struct) := formatField formatStruct
instance : ToString (Field Struct) := toString format
/-
Recall that `structInstField` elements have the form
```lean
def structInstField := leading_parser structInstLVal >> " := " >> termParser
def structInstLVal := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
```
def structInstField := leading_parser structInstLVal >> " := " >> termParser
def structInstLVal := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (("." >> (ident <|> numLit)) <|> structInstArrayRef)
def structInstArrayRef := leading_parser "[" >> termParser >>"]"
```
-/
-- Remark: this code relies on the fact that `expandStruct` only transforms `fieldLHS.fieldName`
private def FieldLHS.toSyntax (first : Bool) : FieldLHS Syntax
def FieldLHS.toSyntax (first : Bool) : FieldLHS Syntax
| .modifyOp stx _ => stx
| .fieldName stx name => if first then mkIdentFrom stx name else mkGroupNode #[mkAtomFrom stx ".", mkIdentFrom stx name]
| .fieldIndex stx _ => if first then stx else mkGroupNode #[mkAtomFrom stx ".", stx]
/--
Converts a `FieldVal StructInstView` back into syntax. Only supports `.term`, and it assumes the `stx` field has the correct structure.
-/
private def FieldVal.toSyntax : FieldVal Struct Syntax
def FieldVal.toSyntax : FieldVal Struct Syntax
| .term stx => stx
| _ => unreachable!
| _ => unreachable!
/--
Converts a `Field StructInstView` back into syntax. Used to construct synthetic structure instance notation for subobjects in `StructInst.expandStruct` processing.
-/
private def Field.toSyntax : Field Struct Syntax
def Field.toSyntax : Field Struct Syntax
| field =>
let stx := field.ref
let stx := stx.setArg 2 field.val.toSyntax
@@ -418,7 +343,6 @@ private def Field.toSyntax : Field Struct → Syntax
| first::rest => stx.setArg 0 <| mkNullNode #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
| _ => unreachable!
/-- Creates a view of a field left-hand side. -/
private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
if stx.getKind == ``Lean.Parser.Term.structInstArrayRef then
return FieldLHS.modifyOp stx stx[1]
@@ -431,16 +355,11 @@ private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
| some idx => return FieldLHS.fieldIndex stx idx
| none => Macro.throwError "unexpected structure syntax"
/--
Creates a structure instance view from structure instance notation
and the computed structure name (from `Lean.Elab.Term.StructInst.getStructName`)
and structure source view (from `Lean.Elab.Term.StructInst.getStructSources`).
-/
private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesView) : MacroM StructInstView := do
private def mkStructView (stx : Syntax) (structName : Name) (source : Source) : MacroM Struct := do
/- Recall that `stx` is of the form
```
leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
>> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ...)
>> sepByIndent (structInstFieldAbbrev <|> structInstField) ...
>> optional ".."
>> optional (" : " >> termParser)
>> " }"
@@ -448,22 +367,28 @@ private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesVi
This method assumes that `structInstFieldAbbrev` had already been expanded.
-/
let fields stx[2][0].getSepArgs.toList.mapM fun fieldStx => do
let fields stx[2].getSepArgs.toList.mapM fun fieldStx => do
let val := fieldStx[2]
let first toFieldLHS fieldStx[0][0]
let rest fieldStx[0][1].getArgs.toList.mapM toFieldLHS
return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field StructInstView }
return { ref := stx, structName, params := #[], fields, sources }
return { ref := fieldStx, lhs := first :: rest, val := FieldVal.term val : Field Struct }
return stx, structName, #[], fields, source
def StructInstView.modifyFieldsM {m : Type Type} [Monad m] (s : StructInstView) (f : Fields m Fields) : m StructInstView :=
def Struct.modifyFieldsM {m : Type Type} [Monad m] (s : Struct) (f : Fields m Fields) : m Struct :=
match s with
| { ref, structName, params, fields, sources } => return { ref, structName, params, fields := ( f fields), sources }
| ref, structName, params, fields, source => return ref, structName, params, ( f fields), source
def StructInstView.modifyFields (s : StructInstView) (f : Fields Fields) : StructInstView :=
def Struct.modifyFields (s : Struct) (f : Fields Fields) : Struct :=
Id.run <| s.modifyFieldsM f
/-- Expands name field LHSs with multi-component names into multi-component LHSs. -/
private def expandCompositeFields (s : StructInstView) : StructInstView :=
def Struct.setFields (s : Struct) (fields : Fields) : Struct :=
s.modifyFields fun _ => fields
def Struct.setParams (s : Struct) (ps : Array (Name × Expr)) : Struct :=
match s with
| ref, structName, _, fields, source => ref, structName, ps, fields, source
private def expandCompositeFields (s : Struct) : Struct :=
s.modifyFields fun fields => fields.map fun field => match field with
| { lhs := .fieldName _ (.str Name.anonymous ..) :: _, .. } => field
| { lhs := .fieldName ref n@(.str ..) :: rest, .. } =>
@@ -471,8 +396,7 @@ private def expandCompositeFields (s : StructInstView) : StructInstView :=
{ field with lhs := newEntries ++ rest }
| _ => field
/-- Replaces numeric index field LHSs with the corresponding named field, or throws an error if no such field exists. -/
private def expandNumLitFields (s : StructInstView) : TermElabM StructInstView :=
private def expandNumLitFields (s : Struct) : TermElabM Struct :=
s.modifyFieldsM fun fields => do
let env getEnv
let fieldNames := getStructureFields env s.structName
@@ -483,31 +407,28 @@ private def expandNumLitFields (s : StructInstView) : TermElabM StructInstView :
else return { field with lhs := .fieldName ref fieldNames[idx - 1]! :: rest }
| _ => return field
/--
Expands fields that are actually represented as fields of subobject fields.
/-- For example, consider the following structures:
```
structure A where
x : Nat
For example, consider the following structures:
```
structure A where
x : Nat
structure B extends A where
y : Nat
structure B extends A where
y : Nat
structure C extends B where
z : Bool
```
This method expands parent structure fields using the path to the parent structure.
For example,
```
{ x := 0, y := 0, z := true : C }
```
is expanded into
```
{ toB.toA.x := 0, toB.y := 0, z := true : C }
```
structure C extends B where
z : Bool
```
This method expands parent structure fields using the path to the parent structure.
For example,
```
{ x := 0, y := 0, z := true : C }
```
is expanded into
```
{ toB.toA.x := 0, toB.y := 0, z := true : C }
```
-/
private def expandParentFields (s : StructInstView) : TermElabM StructInstView := do
private def expandParentFields (s : Struct) : TermElabM Struct := do
let env getEnv
s.modifyFieldsM fun fields => fields.mapM fun field => do match field with
| { lhs := .fieldName ref fieldName :: _, .. } =>
@@ -527,11 +448,6 @@ private def expandParentFields (s : StructInstView) : TermElabM StructInstView :
private abbrev FieldMap := Std.HashMap Name Fields
/--
Creates a hash map collecting all fields with the same first name component.
Throws an error if there are multiple simple fields with the same name.
Used by `StructInst.expandStruct` processing.
-/
private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
fields.foldlM (init := {}) fun fieldMap field =>
match field.lhs with
@@ -545,16 +461,15 @@ private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
| _ => return fieldMap.insert fieldName [field]
| _ => unreachable!
/--
Given a value of the hash map created by `mkFieldMap`, returns true if the value corresponds to a simple field.
-/
private def isSimpleField? : Fields Option (Field StructInstView)
private def isSimpleField? : Fields Option (Field Struct)
| [field] => if field.isSimple then some field else none
| _ => none
/--
Creates projection notation for the given structure field. Used
-/
private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName : Name) : TermElabM Nat := do
match fieldNames.findIdx? fun n => n == fieldName with
| some idx => return idx
| none => throwError "field '{fieldName}' is not a valid field of '{structName}'"
def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
if (findField? ( getEnv) structName fieldName).isNone then
return none
@@ -563,10 +478,7 @@ def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (
#[mkAtomFrom s "@",
mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]]
/--
Finds a simple field of the given name.
-/
def findField? (fields : Fields) (fieldName : Name) : Option (Field StructInstView) :=
def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
fields.find? fun field =>
match field.lhs with
| [.fieldName _ n] => n == fieldName
@@ -574,10 +486,7 @@ def findField? (fields : Fields) (fieldName : Name) : Option (Field StructInstVi
mutual
/--
Groups compound fields according to which subobject they are from.
-/
private partial def groupFields (s : StructInstView) : TermElabM StructInstView := do
private partial def groupFields (s : Struct) : TermElabM Struct := do
let env getEnv
withRef s.ref do
s.modifyFieldsM fun fields => do
@@ -590,28 +499,26 @@ mutual
let field := fields.head!
match Lean.isSubobjectField? env s.structName fieldName with
| some substructName =>
let substruct := { ref := s.ref, structName := substructName, params := #[], fields := substructFields, sources := s.sources }
let substruct := Struct.mk s.ref substructName #[] substructFields s.source
let substruct expandStruct substruct
pure { field with lhs := [field.lhs.head!], val := FieldVal.nested substruct }
| none =>
let updateSource (structStx : Syntax) : TermElabM Syntax := do
let sourcesNew s.sources.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName
let sourcesNew s.source.explicit.filterMapM fun source => mkProjStx? source.stx source.structName fieldName
let explicitSourceStx := if sourcesNew.isEmpty then mkNullNode else mkSourcesWithSyntax sourcesNew
let implicitSourceStx := s.sources.implicit.getD mkNullNode
let implicitSourceStx := s.source.implicit.getD mkNullNode
return (structStx.setArg 1 explicitSourceStx).setArg 3 implicitSourceStx
let valStx := s.ref -- construct substructure syntax using s.ref as template
let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type
let args := substructFields.toArray.map (·.toSyntax)
let fieldsStx := mkNode ``Parser.Term.structInstFields
#[mkNullNode <| mkSepArray args (mkAtom ",")]
let valStx := valStx.setArg 2 fieldsStx
let valStx := valStx.setArg 2 (mkNullNode <| mkSepArray args (mkAtom ","))
let valStx updateSource valStx
return { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
/--
Adds in the missing fields using the explicit sources.
Invariant: a missing field always comes from the first source that can provide it.
-/
private partial def addMissingFields (s : StructInstView) : TermElabM StructInstView := do
private partial def addMissingFields (s : Struct) : TermElabM Struct := do
let env getEnv
let fieldNames := getStructureFields env s.structName
let ref := s.ref.mkSynthetic
@@ -620,7 +527,7 @@ mutual
match findField? s.fields fieldName with
| some field => return field::fields
| none =>
let addField (val : FieldVal StructInstView) : TermElabM Fields := do
let addField (val : FieldVal Struct) : TermElabM Fields := do
return { ref, lhs := [FieldLHS.fieldName ref fieldName], val := val } :: fields
match Lean.isSubobjectField? env s.structName fieldName with
| some substructName =>
@@ -628,8 +535,8 @@ mutual
let downFields := getStructureFieldsFlattened env substructName false
-- Filter out all explicit sources that do not share a leaf field keeping
-- structure with no fields
let filtered := s.sources.explicit.filter fun sources =>
let sourceFields := getStructureFieldsFlattened env sources.structName false
let filtered := s.source.explicit.filter fun source =>
let sourceFields := getStructureFieldsFlattened env source.structName false
sourceFields.any (fun name => downFields.contains name) || sourceFields.isEmpty
-- Take the first such one remaining
match filtered[0]? with
@@ -643,30 +550,27 @@ mutual
-- No sources could provide this subobject in the proper order.
-- Recurse to handle default values for fields.
else
let substruct := { ref, structName := substructName, params := #[], fields := [], sources := s.sources }
let substruct := Struct.mk ref substructName #[] [] s.source
let substruct expandStruct substruct
addField (FieldVal.nested substruct)
-- No sources could provide this subobject.
-- Recurse to handle default values for fields.
| none =>
let substruct := { ref, structName := substructName, params := #[], fields := [], sources := s.sources }
let substruct := Struct.mk ref substructName #[] [] s.source
let substruct expandStruct substruct
addField (FieldVal.nested substruct)
-- Since this is not a subobject field, we are free to use the first source that can
-- provide it.
| none =>
if let some val s.sources.explicit.findSomeM? fun source => mkProjStx? source.stx source.structName fieldName then
if let some val s.source.explicit.findSomeM? fun source => mkProjStx? source.stx source.structName fieldName then
addField (FieldVal.term val)
else if s.sources.implicit.isSome then
else if s.source.implicit.isSome then
addField (FieldVal.term (mkHole ref))
else
addField FieldVal.default
return { s with fields := fields.reverse }
return s.setFields fields.reverse
/--
Expands all fields of the structure instance, consolidates compound fields into subobject fields, and adds missing fields.
-/
private partial def expandStruct (s : StructInstView) : TermElabM StructInstView := do
private partial def expandStruct (s : Struct) : TermElabM Struct := do
let s := expandCompositeFields s
let s expandNumLitFields s
let s expandParentFields s
@@ -675,17 +579,10 @@ mutual
end
/--
The constructor to use for the structure instance notation.
-/
structure CtorHeaderResult where
/-- The constructor function with applied structure parameters. -/
ctorFn : Expr
/-- The type of `ctorFn` -/
ctorFnType : Expr
/-- Instance metavariables for structure parameters that are instance implicit. -/
instMVars : Array MVarId
/-- Type parameter names and metavariables for each parameter. Used to seed `StructInstView.params`. -/
params : Array (Name × Expr)
private def mkCtorHeaderAux : Nat Expr Expr Array MVarId Array (Name × Expr) TermElabM CtorHeaderResult
@@ -707,7 +604,6 @@ private partial def getForallBody : Nat → Expr → Option Expr
| _+1, _ => none
| 0, type => type
/-- Attempts to use the expected type to solve for structure parameters. -/
private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType? : Option Expr) : TermElabM Unit := do
match expectedType? with
| none => return ()
@@ -718,7 +614,6 @@ private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType?
unless typeBody.hasLooseBVars do
discard <| isDefEq expectedType typeBody
/-- Elaborates the structure constructor using the expected type, filling in all structure parameters. -/
private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
let us mkFreshLevelMVars ctorVal.levelParams.length
let val := Lean.mkConst ctorVal.name us
@@ -728,43 +623,32 @@ private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr
synthesizeAppInstMVars r.instMVars r.ctorFn
return r
/-- Annotates an expression that it is a value for a missing field. -/
def markDefaultMissing (e : Expr) : Expr :=
mkAnnotation `structInstDefault e
/-- If the expression has been annotated by `markDefaultMissing`, returns the unannotated expression. -/
def defaultMissing? (e : Expr) : Option Expr :=
annotation? `structInstDefault e
/-- Throws "failed to elaborate field" error. -/
def throwFailedToElabField {α} (fieldName : Name) (structName : Name) (msgData : MessageData) : TermElabM α :=
throwError "failed to elaborate field '{fieldName}' of '{structName}, {msgData}"
/-- If the struct has all-missing fields, tries to synthesize the structure using typeclass inference. -/
def trySynthStructInstance? (s : StructInstView) (expectedType : Expr) : TermElabM (Option Expr) := do
def trySynthStructInstance? (s : Struct) (expectedType : Expr) : TermElabM (Option Expr) := do
if !s.allDefault then
return none
else
try synthInstance? expectedType catch _ => return none
/-- The result of elaborating a `StructInstView` structure instance view. -/
structure ElabStructResult where
/-- The elaborated value. -/
val : Expr
/-- The modified `StructInstView` view after elaboration. -/
struct : StructInstView
/-- Metavariables for instance implicit fields. These will be registered after default value propagation. -/
struct : Struct
instMVars : Array MVarId
/--
Main elaborator for structure instances.
-/
private partial def elabStructInstView (s : StructInstView) (expectedType? : Option Expr) : TermElabM ElabStructResult := withRef s.ref do
private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : TermElabM ElabStructResult := withRef s.ref do
let env getEnv
let ctorVal := getStructureCtor env s.structName
if isPrivateNameFromImportedModule env ctorVal.name then
throwError "invalid \{...} notation, constructor for `{s.structName}` is marked as private"
-- We store the parameters at the resulting `StructInstView`. We use this information during default value propagation.
-- We store the parameters at the resulting `Struct`. We use this information during default value propagation.
let { ctorFn, ctorFnType, params, .. } mkCtorHeader ctorVal expectedType?
let (e, _, fields, instMVars) s.fields.foldlM (init := (ctorFn, ctorFnType, [], #[])) fun (e, type, fields, instMVars) field => do
match field.lhs with
@@ -773,7 +657,7 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt
trace[Elab.struct] "elabStruct {field}, {type}"
match type with
| .forallE _ d b bi =>
let cont (val : Expr) (field : Field StructInstView) (instMVars := instMVars) : TermElabM (Expr × Expr × Fields × Array MVarId) := do
let cont (val : Expr) (field : Field Struct) (instMVars := instMVars) : TermElabM (Expr × Expr × Fields × Array MVarId) := do
pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo {
projName := s.structName.append fieldName, fieldName, lctx := ( getLCtx), val, stx := ref }
let e := mkApp e val
@@ -787,7 +671,7 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt
match ( trySynthStructInstance? s d) with
| some val => cont val { field with val := FieldVal.term (mkHole field.ref) }
| none =>
let { val, struct := sNew, instMVars := instMVarsNew } elabStructInstView s (some d)
let { val, struct := sNew, instMVars := instMVarsNew } elabStruct s (some d)
let val ensureHasType d val
cont val { field with val := FieldVal.nested sNew } (instMVars ++ instMVarsNew)
| .default =>
@@ -816,21 +700,17 @@ private partial def elabStructInstView (s : StructInstView) (expectedType? : Opt
cont (markDefaultMissing val) field
| _ => withRef field.ref <| throwFailedToElabField fieldName s.structName m!"unexpected constructor type{indentExpr type}"
| _ => throwErrorAt field.ref "unexpected unexpanded structure field"
return { val := e, struct := { s with fields := fields.reverse, params }, instMVars }
return { val := e, struct := s.setFields fields.reverse |>.setParams params, instMVars }
namespace DefaultFields
/--
Context for default value propagation.
-/
structure Context where
/-- The current path through `.nested` subobject structures. We must search for default values overridden in derived structures. -/
structs : Array StructInstView := #[]
/-- The collection of structures that could provide a default value. -/
-- We must search for default values overridden in derived structures
structs : Array Struct := #[]
allStructNames : Array Name := #[]
/--
Consider the following example:
```lean
```
structure A where
x : Nat := 1
@@ -856,29 +736,22 @@ structure Context where
-/
maxDistance : Nat := 0
/--
State for default value propagation
-/
structure State where
/-- Whether progress has been made so far on this round of the propagation loop. -/
progress : Bool := false
/-- Collects all structures that may provide default values for fields. -/
partial def collectStructNames (struct : StructInstView) (names : Array Name) : Array Name :=
partial def collectStructNames (struct : Struct) (names : Array Name) : Array Name :=
let names := names.push struct.structName
struct.fields.foldl (init := names) fun names field =>
match field.val with
| .nested struct => collectStructNames struct names
| _ => names
/-- Gets the maximum nesting depth of subobjects. -/
partial def getHierarchyDepth (struct : StructInstView) : Nat :=
partial def getHierarchyDepth (struct : Struct) : Nat :=
struct.fields.foldl (init := 0) fun max field =>
match field.val with
| .nested struct => Nat.max max (getHierarchyDepth struct + 1)
| _ => max
/-- Returns whether the field is still missing. -/
def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field Struct) : m Bool := do
if let some expr := field.expr? then
if let some (.mvar mvarId) := defaultMissing? expr then
@@ -886,51 +759,40 @@ def isDefaultMissing? [Monad m] [MonadMCtx m] (field : Field Struct) : m Bool :=
return true
return false
/-- Returns a field that is still missing. -/
partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Option (Field StructInstView)) :=
partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : Struct) : m (Option (Field Struct)) :=
struct.fields.findSomeM? fun field => do
match field.val with
| .nested struct => findDefaultMissing? struct
| _ => return if ( isDefaultMissing? field) then field else none
/-- Returns all fields that are still missing. -/
partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : StructInstView) : m (Array (Field StructInstView)) :=
partial def allDefaultMissing [Monad m] [MonadMCtx m] (struct : Struct) : m (Array (Field Struct)) :=
go struct *> get |>.run' #[]
where
go (struct : StructInstView) : StateT (Array (Field StructInstView)) m Unit :=
go (struct : Struct) : StateT (Array (Field Struct)) m Unit :=
for field in struct.fields do
if let .nested struct := field.val then
go struct
else if ( isDefaultMissing? field) then
modify (·.push field)
/-- Returns the name of the field. Assumes all fields under consideration are simple and named. -/
def getFieldName (field : Field StructInstView) : Name :=
def getFieldName (field : Field Struct) : Name :=
match field.lhs with
| [.fieldName _ fieldName] => fieldName
| _ => unreachable!
abbrev M := ReaderT Context (StateRefT State TermElabM)
/-- Returns whether we should interrupt the round because we have made progress allowing nonzero depth. -/
def isRoundDone : M Bool := do
return ( get).progress && ( read).maxDistance > 0
/-- Returns the `expr?` for the given field. -/
def getFieldValue? (struct : StructInstView) (fieldName : Name) : Option Expr :=
def getFieldValue? (struct : Struct) (fieldName : Name) : Option Expr :=
struct.fields.findSome? fun field =>
if getFieldName field == fieldName then
field.expr?
else
none
/-- Instantiates a default value from the given default value declaration, if applicable. -/
partial def mkDefaultValue? (struct : StructInstView) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
withRef struct.ref do
let us mkFreshLevelMVarsFor cinfo
process ( instantiateValueLevelParams cinfo us)
where
process : Expr TermElabM (Option Expr)
partial def mkDefaultValueAux? (struct : Struct) : Expr TermElabM (Option Expr)
| .lam n d b c => withRef struct.ref do
if c.isExplicit then
let fieldName := n
@@ -939,26 +801,29 @@ where
| some val =>
let valType inferType val
if ( isDefEq valType d) then
process (b.instantiate1 val)
mkDefaultValueAux? struct (b.instantiate1 val)
else
return none
else
if let some (_, param) := struct.params.find? fun (paramName, _) => paramName == n then
-- Recall that we did not use to have support for parameter propagation here.
if ( isDefEq ( inferType param) d) then
process (b.instantiate1 param)
mkDefaultValueAux? struct (b.instantiate1 param)
else
return none
else
let arg mkFreshExprMVar d
process (b.instantiate1 arg)
mkDefaultValueAux? struct (b.instantiate1 arg)
| e =>
let_expr id _ a := e | return some e
return some a
/--
Reduces a default value. It performs beta reduction and projections of the given structures to reduce them to the provided values for fields.
-/
def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
withRef struct.ref do
let us mkFreshLevelMVarsFor cinfo
mkDefaultValueAux? struct ( instantiateValueLevelParams cinfo us)
/-- Reduce default value. It performs beta reduction and projections of the given structures. -/
partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
match e with
| .forallE .. =>
@@ -1015,10 +880,7 @@ where
else
k
/--
Attempts to synthesize a default value for a missing field `fieldName` using default values from each structure in `structs`.
-/
def tryToSynthesizeDefault (structs : Array StructInstView) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
let rec loop (i : Nat) (dist : Nat) := do
if dist > maxDistance then
return false
@@ -1038,25 +900,14 @@ def tryToSynthesizeDefault (structs : Array StructInstView) (allStructNames : Ar
| none =>
let mvarDecl getMVarDecl mvarId
let val ensureHasType mvarDecl.type val
/-
We must use `checkedAssign` here to ensure we do not create a cyclic
assignment. See #3150.
This can happen when there are holes in the the fields the default value
depends on.
Possible improvement: create a new `_` instead of returning `false` when
`checkedAssign` fails. Reason: the field will not be needed after the
other `_` are resolved by the user.
-/
mvarId.checkedAssign val
mvarId.assign val
return true
| _ => loop (i+1) dist
else
return false
loop 0 0
/--
Performs one step of default value synthesis.
-/
partial def step (struct : StructInstView) : M Unit :=
partial def step (struct : Struct) : M Unit :=
unless ( isRoundDone) do
withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) do
for field in struct.fields do
@@ -1073,10 +924,7 @@ partial def step (struct : StructInstView) : M Unit :=
modify fun _ => { progress := true }
| _ => pure ()
/--
Main entry point to default value synthesis in the `M` monad.
-/
partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : StructInstView) : M Unit := do
partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M Unit := do
match ( findDefaultMissing? struct) with
| none => return () -- Done
| some field =>
@@ -1099,22 +947,16 @@ partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : StructInstV
else
propagateLoop hierarchyDepth (d+1) struct
/--
Synthesizes default values for all missing fields, if possible.
-/
def propagate (struct : StructInstView) : TermElabM Unit :=
def propagate (struct : Struct) : TermElabM Unit :=
let hierarchyDepth := getHierarchyDepth struct
let structNames := collectStructNames struct #[]
propagateLoop hierarchyDepth 0 struct { allStructNames := structNames } |>.run' {}
end DefaultFields
/--
Main entry point to elaborator for structure instance notation, unless the structure instance is a modifyOp.
-/
private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sources : SourcesView) : TermElabM Expr := do
let structName getStructName expectedType? sources
let struct liftMacroM <| mkStructView stx structName sources
private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (source : Source) : TermElabM Expr := do
let structName getStructName expectedType? source
let struct liftMacroM <| mkStructView stx structName source
let struct expandStruct struct
trace[Elab.struct] "{struct}"
/- We try to synthesize pending problems with `withSynthesize` combinator before trying to use default values.
@@ -1132,7 +974,7 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
TODO: investigate whether this design decision may have unintended side effects or produce confusing behavior.
-/
let { val := r, struct, instMVars } withSynthesize (postpone := .yes) <| elabStructInstView struct expectedType?
let { val := r, struct, instMVars } withSynthesize (postpone := .yes) <| elabStruct struct expectedType?
trace[Elab.struct] "before propagate {r}"
DefaultFields.propagate struct
synthesizeAppInstMVars instMVars r
@@ -1142,13 +984,13 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
match ( expandNonAtomicExplicitSources stx) with
| some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
| none =>
let sourcesView getStructSources stx
let sourceView getStructSource stx
if let some modifyOp isModifyOp? stx then
if sourcesView.explicit.isEmpty then
if sourceView.explicit.isEmpty then
throwError "invalid \{...} notation, explicit source is required when using '[<index>] := <value>'"
elabModifyOp stx modifyOp sourcesView.explicit expectedType?
elabModifyOp stx modifyOp sourceView.explicit expectedType?
else
elabStructInstAux stx expectedType? sourcesView
elabStructInstAux stx expectedType? sourceView
builtin_initialize
registerTraceClass `Elab.struct

View File

@@ -19,12 +19,12 @@ def expandOptPrecedence (stx : Syntax) : MacroM (Option Nat) :=
return some ( evalPrec stx[0][1])
private def mkParserSeq (ds : Array (Term × Nat)) : TermElabM (Term × Nat) := do
if h₀ : ds.size = 0 then
if ds.size == 0 then
throwUnsupportedSyntax
else if h₁ : ds.size = 1 then
pure ds[0]
else if ds.size == 1 then
pure ds[0]!
else
let mut (r, stackSum) := ds[0]
let mut (r, stackSum) := ds[0]!
for (d, stackSz) in ds[1:ds.size] do
r `(ParserDescr.binary `andthen $r $d)
stackSum := stackSum + stackSz
@@ -142,7 +142,7 @@ where
let args := stx.getArgs
if ( checkLeftRec stx[0]) then
if args.size == 1 then throwErrorAt stx "invalid atomic left recursive syntax"
let args := args.eraseIdxIfInBounds 0
let args := args.eraseIdx 0
let args args.mapM fun arg => withNestedParser do process arg
mkParserSeq args
else
@@ -233,15 +233,11 @@ where
return ( `((with_annotate_term $(stx[0]) @ParserDescr.sepBy1) $p $sep $psep $(quote allowTrailingSep)), 1)
isValidAtom (s : String) : Bool :=
-- Pretty-printing instructions shouldn't affect validity
let s := s.trim
!s.isEmpty &&
(s.front != '\'' || "''".isPrefixOf s) &&
s.front != '\'' &&
s.front != '\"' &&
!(isIdBeginEscape s.front) &&
!(s.front == '`' && (s.endPos == ⟨1⟩ || isIdFirst (s.get ⟨1⟩) || isIdBeginEscape (s.get ⟨1⟩))) &&
!s.front.isDigit &&
!(s.any Char.isWhitespace)
!s.front.isDigit
processAtom (stx : Syntax) := do
match stx[0].isStrLit? with

View File

@@ -149,8 +149,8 @@ where
-- Succeeded. Collect new TC problems
trace[Elab.defaultInstance] "isDefEq worked {mkMVar mvarId} : {← inferType (mkMVar mvarId)} =?= {candidate} : {← inferType candidate}"
let mut pending := []
for h : i in [:bis.size] do
if bis[i] == BinderInfo.instImplicit then
for i in [:bis.size] do
if bis[i]! == BinderInfo.instImplicit then
pending := mvars[i]!.mvarId! :: pending
synthesizePending pending
else

View File

@@ -198,10 +198,11 @@ def rewriteRulesPass (maxSteps : Nat) : Pass where
let sevalThms getSEvalTheorems
let sevalSimprocs Simp.getSEvalSimprocs
let simpCtx Simp.mkContext
(config := { failIfUnchanged := false, zetaDelta := true, maxSteps })
(simpTheorems := #[bvThms, sevalThms])
(congrTheorems := ( getSimpCongrTheorems))
let simpCtx : Simp.Context := {
config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
simpTheorems := #[bvThms, sevalThms]
congrTheorems := ( getSimpCongrTheorems)
}
let hyps goal.getNondepPropHyps
let result?, _ simpGoal goal
@@ -216,23 +217,35 @@ Flatten out ands. That is look for hypotheses of the form `h : (x && y) = true`
with `h.left : x = true` and `h.right : y = true`. This can enable more fine grained substitutions
in embedded constraint substitution.
-/
partial def andFlatteningPass : Pass where
def andFlatteningPass : Pass where
name := `andFlattening
run goal := do
goal.withContext do
let hyps goal.getNondepPropHyps
let mut newHyps := #[]
let mut oldHyps := #[]
for fvar in hyps do
let hyp : Hypothesis := {
userName := ( fvar.getDecl).userName
type := fvar.getType
value := mkFVar fvar
for hyp in hyps do
let typ hyp.getType
let_expr Eq α eqLhs eqRhs := typ | continue
let_expr Bool.and lhs rhs := eqLhs | continue
let_expr Bool := α | continue
let_expr Bool.true := eqRhs | continue
let mkEqTrue (lhs : Expr) : Expr :=
mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) lhs (mkConst ``Bool.true)
let hypExpr := ( hyp.getDecl).toExpr
let leftHyp : Hypothesis := {
userName := ( hyp.getUserName) ++ `left,
type := mkEqTrue lhs,
value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_left) lhs rhs hypExpr
}
let sizeBefore := newHyps.size
newHyps splitAnds hyp newHyps
if newHyps.size > sizeBefore then
oldHyps := oldHyps.push fvar
let rightHyp : Hypothesis := {
userName := ( hyp.getUserName) ++ `right,
type := mkEqTrue rhs,
value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_right) lhs rhs hypExpr
}
newHyps := newHyps.push leftHyp
newHyps := newHyps.push rightHyp
oldHyps := oldHyps.push hyp
if newHyps.size == 0 then
return goal
else
@@ -240,38 +253,6 @@ partial def andFlatteningPass : Pass where
-- Given that we collected the hypotheses in the correct order above the invariant is given
let goal goal.tryClearMany oldHyps
return goal
where
splitAnds (hyp : Hypothesis) (hyps : Array Hypothesis) (first : Bool := true) :
MetaM (Array Hypothesis) := do
match trySplit hyp with
| some (left, right) =>
let hyps splitAnds left hyps false
splitAnds right hyps false
| none =>
if first then
return hyps
else
return hyps.push hyp
trySplit (hyp : Hypothesis) : MetaM (Option (Hypothesis × Hypothesis)) := do
let typ := hyp.type
let_expr Eq α eqLhs eqRhs := typ | return none
let_expr Bool.and lhs rhs := eqLhs | return none
let_expr Bool.true := eqRhs | return none
let_expr Bool := α | return none
let mkEqTrue (lhs : Expr) : Expr :=
mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) lhs (mkConst ``Bool.true)
let leftHyp : Hypothesis := {
userName := hyp.userName,
type := mkEqTrue lhs,
value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_left) lhs rhs hyp.value
}
let rightHyp : Hypothesis := {
userName := hyp.userName,
type := mkEqTrue rhs,
value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_right) lhs rhs hyp.value
}
return some (leftHyp, rightHyp)
/--
Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
@@ -302,10 +283,11 @@ def embeddedConstraintPass (maxSteps : Nat) : Pass where
let goal goal.tryClearMany duplicates
let simpCtx Simp.mkContext
(config := { failIfUnchanged := false, maxSteps })
(simpTheorems := relevantHyps)
(congrTheorems := ( getSimpCongrTheorems))
let simpCtx : Simp.Context := {
config := { failIfUnchanged := false, maxSteps }
simpTheorems := relevantHyps
congrTheorems := ( getSimpCongrTheorems)
}
let result?, _ simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := goal.getNondepPropHyps)
let some (_, newGoal) := result? | return none
@@ -328,18 +310,22 @@ def acNormalizePass : Pass where
return newGoal
/--
The normalization passes used by `bv_normalize` and thus `bv_decide`.
-/
def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
[
rewriteRulesPass cfg.maxSteps,
andFlatteningPass,
embeddedConstraintPass cfg.maxSteps
]
def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
let mut passPipeline := [rewriteRulesPass cfg.maxSteps]
let mut passPipeline := defaultPipeline cfg
if cfg.acNf then
passPipeline := passPipeline ++ [acNormalizePass]
if cfg.andFlattening then
passPipeline := passPipeline ++ [andFlatteningPass]
if cfg.embeddedConstraintSubst then
passPipeline := passPipeline ++ [embeddedConstraintPass cfg.maxSteps]
return passPipeline
end Pass

View File

@@ -218,7 +218,7 @@ where
let old snap.old?
-- If the kind is equal, we can assume the old version was a macro as well
guard <| old.stx.isOfKind stx.getKind
let state old.val.get.finished.get.state?
let state old.val.get.data.finished.get.state?
guard <| state.term.meta.core.nextMacroScope == nextMacroScope
-- check absence of traces; see Note [Incremental Macros]
guard <| state.term.meta.core.traceState.traces.size == 0
@@ -226,10 +226,9 @@ where
return old.val.get
Language.withAlwaysResolvedPromise fun promise => do
-- Store new unfolding in the snapshot tree
snap.new.resolve {
snap.new.resolve <| .mk {
stx := stx'
diagnostics := .empty
inner? := none
finished := .pure {
diagnostics := .empty
state? := ( Tactic.saveState)
@@ -241,7 +240,7 @@ where
new := promise
old? := do
let old old?
return old.stx, ( old.next.get? 0)
return old.data.stx, ( old.data.next.get? 0)
} }) do
evalTactic stx'
return

View File

@@ -60,7 +60,7 @@ where
if let some snap := ( readThe Term.Context).tacSnap? then
if let some old := snap.old? then
let oldParsed := old.val.get
oldInner? := oldParsed.inner? |>.map (oldParsed.stx, ·)
oldInner? := oldParsed.data.inner? |>.map (oldParsed.data.stx, ·)
-- compare `stx[0]` for `finished`/`next` reuse, focus on remainder of script
Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) fun stxs => do
let some snap := ( readThe Term.Context).tacSnap?
@@ -70,10 +70,10 @@ where
if let some old := snap.old? then
-- `tac` must be unchanged given the narrow above; let's reuse `finished`'s state!
let oldParsed := old.val.get
if let some state := oldParsed.finished.get.state? then
if let some state := oldParsed.data.finished.get.state? then
reusableResult? := some ((), state)
-- only allow `next` reuse in this case
oldNext? := oldParsed.next.get? 0 |>.map (old.stx, ·)
oldNext? := oldParsed.data.next.get? 0 |>.map (old.stx, ·)
-- For `tac`'s snapshot task range, disregard synthetic info as otherwise
-- `SnapshotTree.findInfoTreeAtPos` might choose the wrong snapshot: for example, when
@@ -89,7 +89,7 @@ where
withAlwaysResolvedPromise fun next => do
withAlwaysResolvedPromise fun finished => do
withAlwaysResolvedPromise fun inner => do
snap.new.resolve {
snap.new.resolve <| .mk {
desc := tac.getKind.toString
diagnostics := .empty
stx := tac

View File

@@ -13,31 +13,6 @@ open Meta
# Implementation of the `change` tactic
-/
/--
Elaborates the pattern `p` and ensures that it is defeq to `e`.
Emulates `(show p from ?m : e)`, returning the type of `?m`, but `e` and `p` do not need to be types.
Unlike `(show p from ?m : e)`, this can assign synthetic opaque metavariables appearing in `p`.
-/
def elabChange (e : Expr) (p : Term) : TacticM Expr := do
let p runTermElab do
let p Term.elabTermEnsuringType p ( inferType e)
unless isDefEq p e do
/-
Sometimes isDefEq can fail due to postponed elaboration problems.
We synthesize pending synthetic mvars while allowing typeclass instances to be postponed,
which might enable solving for them with an additional `isDefEq`.
-/
Term.synthesizeSyntheticMVars (postpone := .partial)
discard <| isDefEq p e
pure p
withAssignableSyntheticOpaque do
unless isDefEq p e do
let (p, tgt) addPPExplicitToExposeDiff p e
throwError "\
'change' tactic failed, pattern{indentExpr p}\n\
is not definitionally equal to target{indentExpr tgt}"
instantiateMVars p
/-- `change` can be used to replace the main goal or its hypotheses with
different, yet definitionally equal, goal or hypotheses.
@@ -63,13 +38,15 @@ the main goal. -/
| `(tactic| change $newType:term $[$loc:location]?) => do
withLocation (expandOptLocation (Lean.mkOptionalNode loc))
(atLocal := fun h => do
let (hTy', mvars) withCollectingNewGoalsFrom (elabChange ( h.getType) newType) ( getMainTag) `change
let hTy h.getType
-- This is a hack to get the new type to elaborate in the same sort of way that
-- it would for a `show` expression for the goal.
let mvar mkFreshExprMVar none
let (_, mvars) elabTermWithHoles
( `(term | show $newType from $( Term.exprToSyntax mvar))) hTy `change
liftMetaTactic fun mvarId => do
return ( mvarId.changeLocalDecl h hTy') :: mvars)
(atTarget := do
let (tgt', mvars) withCollectingNewGoalsFrom (elabChange ( getMainTarget) newType) ( getMainTag) `change
liftMetaTactic fun mvarId => do
return ( mvarId.replaceTargetDefEq tgt') :: mvars)
(failed := fun _ => throwError "'change' tactic failed")
return ( mvarId.changeLocalDecl h ( inferType mvar)) :: mvars)
(atTarget := evalTactic <| `(tactic| refine_lift show $newType from ?_))
(failed := fun _ => throwError "change tactic failed")
end Lean.Elab.Tactic

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