Compare commits

..

2 Commits

Author SHA1 Message Date
Kim Morrison
3578ec59e6 ordered rings 2025-05-21 16:38:18 +10:00
Kim Morrison
12b8498a4a initial commit 2025-05-21 14:42:53 +10:00
712 changed files with 2572 additions and 5803 deletions

View File

@@ -10,29 +10,11 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Check awaiting-mathlib label
id: check-awaiting-mathlib-label
if: github.event_name == 'pull_request'
uses: actions/github-script@v7
with:
script: |
const { labels, number: prNumber } = context.payload.pull_request;
const hasAwaiting = labels.some(label => label.name == "awaiting-mathlib");
const hasBreaks = labels.some(label => label.name == "breaks-mathlib");
const hasBuilds = labels.some(label => label.name == "builds-mathlib");
if (hasAwaiting && hasBreaks) {
core.setFailed('PR has both "awaiting-mathlib" and "breaks-mathlib" labels.');
} else if (hasAwaiting && !hasBreaks && !hasBuilds) {
core.info('PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.');
core.setOutput('awaiting', 'true');
const { labels } = context.payload.pull_request;
if (labels.some(label => label.name == "awaiting-mathlib") && !labels.some(label => label.name == "builds-mathlib")) {
core.setFailed('PR is marked "awaiting-mathlib" but "builds-mathlib" label has not been applied yet by the bot');
}
- name: Wait for mathlib compatibility
if: github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
run: |
echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."
# Keep the job running indefinitely to show "in progress" status
while true; do
sleep 3600 # Sleep for 1 hour at a time
done

View File

@@ -40,24 +40,34 @@ jobs:
run: |
git config --global user.name "Lean stage0 autoupdater"
git config --global user.email "<>"
# Would be nice, but does not work yet:
# https://github.com/DeterminateSystems/magic-nix-cache/issues/39
# This action does not run that often and building runs in a few minutes, so ok for now
#- if: env.should_update_stage0 == 'yes'
# uses: DeterminateSystems/magic-nix-cache-action@v2
- if: env.should_update_stage0 == 'yes'
name: Restore Build Cache
uses: actions/cache/restore@v4
with:
path: nix-store-cache
key: Nix Linux-nix-store-cache-${{ github.sha }}
# fall back to (latest) previous cache
restore-keys: |
Nix Linux-nix-store-cache
- if: env.should_update_stage0 == 'yes'
name: Further Set Up Nix Cache
shell: bash -euxo pipefail {0}
run: |
# Nix seems to mutate the cache, so make a copy
cp -r nix-store-cache nix-store-cache-copy || true
- if: env.should_update_stage0 == 'yes'
name: Install Nix
uses: DeterminateSystems/nix-installer-action@main
- name: Open Nix shell once
if: env.should_update_stage0 == 'yes'
run: true
shell: 'nix develop -c bash -euxo pipefail {0}'
- name: Set up NPROC
if: env.should_update_stage0 == 'yes'
run: |
echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
shell: 'nix develop -c bash -euxo pipefail {0}'
with:
extra-conf: |
substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org
- if: env.should_update_stage0 == 'yes'
run: cmake --preset release
shell: 'nix develop -c bash -euxo pipefail {0}'
- if: env.should_update_stage0 == 'yes'
run: make -j$NPROC -C build/release update-stage0-commit
shell: 'nix develop -c bash -euxo pipefail {0}'
run: nix run .#update-stage0-commit
- if: env.should_update_stage0 == 'yes'
run: git show --stat
- if: env.should_update_stage0 == 'yes' && github.event_name == 'push'

View File

@@ -6,7 +6,6 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
module
prelude
import Init.Ext
import Init.SimpLemmas
import Init.Meta
@@ -242,23 +241,13 @@ theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
namespace Id
@[ext] theorem ext {x y : Id α} (h : x.run = y.run) : x = y := h
@[simp] theorem map_eq (x : Id α) (f : α β) : f <$> x = f x := rfl
@[simp] theorem bind_eq (x : Id α) (f : α id β) : x >>= f = f x := rfl
@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
instance : LawfulMonad Id := by
refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
@[simp] theorem run_map (x : Id α) (f : α β) : (f <$> x).run = f x.run := rfl
@[simp] theorem run_bind (x : Id α) (f : α Id β) : (x >>= f).run = (f x.run).run := rfl
@[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
@[simp] theorem run_seq (f : Id (α β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
-- These lemmas are bad as they abuse the defeq of `Id α` and `α`
@[deprecated run_map (since := "2025-03-05")] theorem map_eq (x : Id α) (f : α β) : f <$> x = f x := rfl
@[deprecated run_bind (since := "2025-03-05")] theorem bind_eq (x : Id α) (f : α id β) : x >>= f = f x := rfl
@[deprecated run_pure (since := "2025-03-05")] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
end Id
/-! # Option -/

View File

@@ -69,11 +69,11 @@ well-founded recursion mechanism to prove that the function terminates.
simp [pmap]
@[simp] theorem toList_attachWith {xs : Array α} {P : α Prop} {H : x xs, P x} :
(xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList_iff] using H) := by
(xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList] using H) := by
simp [attachWith]
@[simp] theorem toList_attach {xs : Array α} :
xs.attach.toList = xs.toList.attachWith (· xs) (by simp [mem_toList_iff]) := by
xs.attach.toList = xs.toList.attachWith (· xs) (by simp [mem_toList]) := by
simp [attach]
@[simp] theorem toList_pmap {xs : Array α} {P : α Prop} {f : a, P a β} {H : a xs, P a} :
@@ -574,12 +574,9 @@ state, the right approach is usually the tactic `simp [Array.unattach, -Array.ma
-/
def unattach {α : Type _} {p : α Prop} (xs : Array { x // p x }) : Array α := xs.map (·.val)
@[simp] theorem unattach_empty {p : α Prop} : (#[] : Array { x // p x }).unattach = #[] := by
@[simp] theorem unattach_nil {p : α Prop} : (#[] : Array { x // p x }).unattach = #[] := by
simp [unattach]
@[deprecated unattach_empty (since := "2025-05-26")]
abbrev unattach_nil := @unattach_empty
@[simp] theorem unattach_push {p : α Prop} {a : { x // p x }} {xs : Array { x // p x }} :
(xs.push a).unattach = xs.unattach.push a.1 := by
simp only [unattach, Array.map_push]

View File

@@ -112,7 +112,7 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
rw [Array.mem_def, getElem_toList]
apply List.getElem_mem
@[simp, grind =] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
@[simp] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
@[simp] theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
@@ -544,7 +544,7 @@ Examples:
-/
@[inline]
def modify (xs : Array α) (i : Nat) (f : α α) : Array α :=
Id.run <| modifyM xs i (pure <| f ·)
Id.run <| modifyM xs i f
set_option linter.indexVariables false in -- Changing `idx` causes bootstrapping issues, haven't investigated.
/--
@@ -1059,7 +1059,7 @@ Examples:
-/
@[inline]
def foldl {α : Type u} {β : Type v} (f : β α β) (init : β) (as : Array α) (start := 0) (stop := as.size) : β :=
Id.run <| as.foldlM (pure <| f · ·) init start stop
Id.run <| as.foldlM f init start stop
/--
Folds a function over an array from the right, accumulating a value starting with `init`. The
@@ -1076,7 +1076,7 @@ Examples:
-/
@[inline]
def foldr {α : Type u} {β : Type v} (f : α β β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β :=
Id.run <| as.foldrM (pure <| f · ·) init start stop
Id.run <| as.foldrM f init start stop
/--
Computes the sum of the elements of an array.
@@ -1124,7 +1124,7 @@ Examples:
-/
@[inline]
def map {α : Type u} {β : Type v} (f : α β) (as : Array α) : Array β :=
Id.run <| as.mapM (pure <| f ·)
Id.run <| as.mapM f
instance : Functor Array where
map := map
@@ -1139,7 +1139,7 @@ valid.
-/
@[inline]
def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) α (h : i < as.size) β) : Array β :=
Id.run <| as.mapFinIdxM (pure <| f · · ·)
Id.run <| as.mapFinIdxM f
/--
Applies a function to each element of the array along with the index at which that element is found,
@@ -1150,7 +1150,7 @@ is valid.
-/
@[inline]
def mapIdx {α : Type u} {β : Type v} (f : Nat α β) (as : Array α) : Array β :=
Id.run <| as.mapIdxM (pure <| f · ·)
Id.run <| as.mapIdxM f
/--
Pairs each element of an array with its index, optionally starting from an index other than `0`.
@@ -1198,7 +1198,7 @@ some 10
-/
@[inline]
def findSome? {α : Type u} {β : Type v} (f : α Option β) (as : Array α) : Option β :=
Id.run <| as.findSomeM? (pure <| f ·)
Id.run <| as.findSomeM? f
/--
Returns the first non-`none` result of applying the function `f` to each element of the
@@ -1232,7 +1232,7 @@ Examples:
-/
@[inline]
def findSomeRev? {α : Type u} {β : Type v} (f : α Option β) (as : Array α) : Option β :=
Id.run <| as.findSomeRevM? (pure <| f ·)
Id.run <| as.findSomeRevM? f
/--
Returns the last element of the array for which the predicate `p` returns `true`, or `none` if no
@@ -1244,7 +1244,7 @@ Examples:
-/
@[inline]
def findRev? {α : Type} (p : α Bool) (as : Array α) : Option α :=
Id.run <| as.findRevM? (pure <| p ·)
Id.run <| as.findRevM? p
/--
Returns the index of the first element for which `p` returns `true`, or `none` if there is no such
@@ -1383,7 +1383,7 @@ Examples:
-/
@[inline]
def any (as : Array α) (p : α Bool) (start := 0) (stop := as.size) : Bool :=
Id.run <| as.anyM (pure <| p ·) start stop
Id.run <| as.anyM p start stop
/--
Returns `true` if `p` returns `true` for every element of `as`.
@@ -1401,7 +1401,7 @@ Examples:
-/
@[inline]
def all (as : Array α) (p : α Bool) (start := 0) (stop := as.size) : Bool :=
Id.run <| as.allM (pure <| p ·) start stop
Id.run <| as.allM p start stop
/--
Checks whether `a` is an element of `as`, using `==` to compare elements.
@@ -1670,7 +1670,7 @@ Example:
-/
@[inline]
def filterMap (f : α Option β) (as : Array α) (start := 0) (stop := as.size) : Array β :=
Id.run <| as.filterMapM (pure <| f ·) (start := start) (stop := stop)
Id.run <| as.filterMapM f (start := start) (stop := stop)
/--
Returns the largest element of the array, as determined by the comparison `lt`, or `none` if

View File

@@ -88,4 +88,4 @@ pointer equality, and does not allocate a new array if the result of each functi
pointer-equal to its argument.
-/
@[inline] def Array.mapMono (as : Array α) (f : α α) : Array α :=
Id.run <| as.mapMonoM (pure <| f ·)
Id.run <| as.mapMonoM f

View File

@@ -129,6 +129,6 @@ Examples:
* `#[].binInsert (· < ·) 1 = #[1]`
-/
@[inline] def binInsert {α : Type u} (lt : α α Bool) (as : Array α) (k : α) : Array α :=
Id.run <| binInsertM lt (fun _ => pure k) (fun _ => pure k) as k
Id.run <| binInsertM lt (fun _ => k) (fun _ => k) as k
end Array

View File

@@ -89,13 +89,9 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init
xs.toList.foldr f init = xs.foldr f init :=
List.foldr_eq_foldrM .. foldrM_toList ..
@[simp, grind =] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by
rcases xs with xs
@[simp, grind =] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
simp [push, List.concat_eq_append]
@[deprecated toList_push (since := "2025-05-26")]
abbrev push_toList := @toList_push
@[simp, grind =] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
simp [toListAppend, foldr_toList]

View File

@@ -52,8 +52,8 @@ theorem countP_push {a : α} {xs : Array α} : countP p (xs.push a) = countP p x
rcases xs with xs
simp_all
theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
simp
@[simp] theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by
simp [countP_push]
theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + countP (fun a => ¬p a) xs := by
rcases xs with xs

View File

@@ -24,7 +24,7 @@ open Nat
/-! ### eraseP -/
theorem eraseP_empty : #[].eraseP p = #[] := by simp
@[simp] theorem eraseP_empty : #[].eraseP p = #[] := by simp
theorem eraseP_of_forall_mem_not {xs : Array α} (h : a, a xs ¬p a) : xs.eraseP p = xs := by
rcases xs with xs

View File

@@ -238,9 +238,11 @@ theorem extract_append_left {as bs : Array α} :
(as ++ bs).extract 0 as.size = as.extract 0 as.size := by
simp
theorem extract_append_right {as bs : Array α} :
@[simp] theorem extract_append_right {as bs : Array α} :
(as ++ bs).extract as.size (as.size + i) = bs.extract 0 i := by
simp
simp only [extract_append, extract_size_left, Nat.sub_self, empty_append]
congr 1
omega
@[simp] theorem map_extract {as : Array α} {i j : Nat} :
(as.extract i j).map f = (as.map f).extract i j := by

View File

@@ -142,9 +142,9 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
@[simp] theorem find?_empty : find? p #[] = none := rfl
theorem find?_singleton {a : α} {p : α Bool} :
@[simp] theorem find?_singleton {a : α} {p : α Bool} :
#[a].find? p = if p a then some a else none := by
simp
simp [singleton_eq_toArray_singleton]
@[simp] theorem findRev?_push_of_pos {xs : Array α} (h : p a) :
findRev? p (xs.push a) = some a := by
@@ -347,8 +347,7 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
/-! ### findIdx -/
theorem findIdx_empty : findIdx p #[] = 0 := rfl
@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl
theorem findIdx_singleton {a : α} {p : α Bool} :
#[a].findIdx p = if p a then 0 else 1 := by
simp
@@ -601,8 +600,7 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
/-! ### findFinIdx? -/
theorem findFinIdx?_empty {p : α Bool} : findFinIdx? p #[] = none := by simp
@[simp] theorem findFinIdx?_empty {p : α Bool} : findFinIdx? p #[] = none := by simp
theorem findFinIdx?_singleton {a : α} {p : α Bool} :
#[a].findFinIdx? p = if p a then some 0, by simp else none := by
simp
@@ -701,7 +699,7 @@ The verification API for `idxOf?` is still incomplete.
The lemmas below should be made consistent with those for `findIdx?` (and proved using them).
-/
theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp
@[simp] theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp
@[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
xs.idxOf? a = none a xs := by
@@ -714,10 +712,14 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
rcases xs with xs
simp
@[simp]
theorem isNone_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
(xs.idxOf? a).isNone = ¬ a xs := by
rcases xs with xs
simp
/-! ### finIdxOf?
The verification API for `finIdxOf?` is still incomplete.
@@ -728,7 +730,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
@[simp] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
@[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
xs.finIdxOf? a = none a xs := by
@@ -746,8 +748,10 @@ theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
rcases xs with xs
simp
@[simp]
theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
(xs.finIdxOf? a).isNone = ¬ a xs := by
rcases xs with xs
simp
end Array

View File

@@ -63,7 +63,7 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
/-! ### size -/
theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
@[grind ] theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
cases xs
simp_all
@@ -75,6 +75,7 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
cases xs
simpa using List.ne_nil_of_length_pos h
@[grind]
theorem size_eq_zero_iff : xs.size = 0 xs = #[] :=
eq_empty_of_size_eq_zero, fun h => h rfl
@@ -116,11 +117,14 @@ abbrev size_eq_one := @size_eq_one_iff
/-! ## L[i] and L[i]? -/
theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none xs.size i := by
simp
@[simp] theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none xs.size i := by
by_cases h : i < xs.size
· simp [getElem?_pos, h]
· rw [getElem?_neg xs i h]
simp_all
theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? xs.size i := by
simp
@[simp] theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? xs.size i := by
simp [eq_comm (a := none)]
theorem getElem?_eq_none {xs : Array α} (h : xs.size i) : xs[i]? = none := by
simp [getElem?_eq_none_iff, h]
@@ -130,8 +134,8 @@ grind_pattern Array.getElem?_eq_none => xs.size ≤ i, xs[i]?
@[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] :=
getElem?_pos ..
theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b h : i < xs.size, xs[i] = b :=
_root_.getElem?_eq_some_iff
theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b h : i < xs.size, xs[i] = b := by
simp [getElem?_def]
@[grind ]
theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a h : i < xs.size, xs[i] = a :=
@@ -140,13 +144,13 @@ theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs
theorem some_eq_getElem?_iff {xs : Array α} : some b = xs[i]? h : i < xs.size, xs[i] = b := by
rw [eq_comm, getElem?_eq_some_iff]
theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
@[simp] theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
(some xs[i] = xs[i]?) True := by
simp
simp [h]
theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
@[simp] theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) :
(xs[i]? = some xs[i]) True := by
simp
simp [h]
theorem getElem_eq_iff {xs : Array α} {i : Nat} {h : i < xs.size} : xs[i] = x xs[i]? = some x := by
simp only [getElem?_eq_some_iff]
@@ -182,15 +186,16 @@ theorem getElem_push {xs : Array α} {x : α} {i : Nat} (h : i < (xs.push x).siz
· simp at h
simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
@[grind =] theorem getElem?_push {xs : Array α} {x} : (xs.push x)[i]? = if i = xs.size then some x else xs[i]? := by
theorem getElem?_push {xs : Array α} {x} : (xs.push x)[i]? = if i = xs.size then some x else xs[i]? := by
simp [getElem?_def, getElem_push]
(repeat' split) <;> first | rfl | omega
theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
simp
@[simp] theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by
simp [getElem?_push]
theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a := by
simp
@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a :=
match i, h with
| 0, _ => rfl
@[grind]
theorem getElem?_singleton {a : α} {i : Nat} : #[a][i]? = if i = 0 then some a else none := by
@@ -239,6 +244,10 @@ theorem back?_pop {xs : Array α} :
@[simp] theorem push_empty : #[].push x = #[x] := rfl
@[simp] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by
rcases xs with xs
simp
@[simp] theorem push_ne_empty {a : α} {xs : Array α} : xs.push a #[] := by
cases xs
simp
@@ -418,7 +427,8 @@ theorem eq_empty_iff_forall_not_mem {xs : Array α} : xs = #[] ↔ ∀ a, a ∉
theorem eq_of_mem_singleton (h : a #[b]) : a = b := by
simpa using h
theorem mem_singleton {a b : α} : a #[b] a = b := by simp
@[simp] theorem mem_singleton {a b : α} : a #[b] a = b :=
eq_of_mem_singleton, (by simp [·])
theorem forall_mem_push {p : α Prop} {xs : Array α} {a : α} :
( x, x xs.push a p x) p a x, x xs p x := by
@@ -603,13 +613,13 @@ theorem anyM_loop_cons [Monad m] {p : α → m Bool} {a : α} {as : List α} {st
-- Auxiliary for `any_iff_exists`.
theorem anyM_loop_iff_exists {p : α Bool} {as : Array α} {start stop} (h : stop as.size) :
(anyM.loop (m := Id) (pure <| p ·) as stop h start).run = true
anyM.loop (m := Id) p as stop h start = true
(i : Nat) (_ : i < as.size), start i i < stop p as[i] = true := by
unfold anyM.loop
split <;> rename_i h₁
· dsimp
split <;> rename_i h₂
· simp only [true_iff, Id.run_pure]
· simp only [true_iff]
refine start, by omega, by omega, by omega, h₂
· rw [anyM_loop_iff_exists]
constructor
@@ -626,9 +636,9 @@ termination_by stop - start
-- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
theorem any_iff_exists {p : α Bool} {as : Array α} {start stop} :
as.any p start stop (i : Nat) (_ : i < as.size), start i i < stop p as[i] := by
dsimp [any, anyM]
dsimp [any, anyM, Id.run]
split
· rw [anyM_loop_iff_exists (p := p)]
· rw [anyM_loop_iff_exists]
· rw [anyM_loop_iff_exists]
constructor
· rintro i, hi, ge, _, h
@@ -862,8 +872,8 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
@[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
xs.contains a = decide (a xs) := by rw [ elem_eq_contains, elem_eq_mem]
@[grind] theorem any_empty [BEq α] {p : α Bool} : (#[] : Array α).any p = false := by simp
@[grind] theorem all_empty [BEq α] {p : α Bool} : (#[] : Array α).all p = true := by simp
@[simp, grind] theorem any_empty [BEq α] {p : α Bool} : (#[] : Array α).any p = false := by simp
@[simp, grind] theorem all_empty [BEq α] {p : α Bool} : (#[] : Array α).all p = true := by simp
/-- Variant of `any_push` with a side condition on `stop`. -/
@[simp, grind] theorem any_push' [BEq α] {xs : Array α} {a : α} {p : α Bool} (h : stop = xs.size + 1) :
@@ -1222,7 +1232,7 @@ where
@[simp] theorem mapM_empty [Monad m] (f : α m β) : mapM f #[] = pure #[] := by
rw [mapM, mapM.map]; rfl
@[grind] theorem map_empty {f : α β} : map f #[] = #[] := by simp
@[simp, grind] theorem map_empty {f : α β} : map f #[] = #[] := mapM_empty f
@[simp, grind] theorem map_push {f : α β} {as : Array α} {x : α} :
(as.push x).map f = (as.map f).push (f x) := by
@@ -1360,17 +1370,17 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] {f : α → m β} {xs : Ar
@[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
theorem mapM_map_eq_foldl {as : Array α} {f : α β} {i : Nat} :
mapM.map (m := Id) (pure <| f ·) as i b = pure (as.foldl (start := i) (fun acc a => acc.push (f a)) b) := by
mapM.map (m := Id) f as i b = as.foldl (start := i) (fun acc a => acc.push (f a)) b := by
unfold mapM.map
split <;> rename_i h
· ext : 1
dsimp [foldl, foldlM]
· simp only [Id.bind_eq]
dsimp [foldl, Id.run, foldlM]
rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
-- Calling `split` here gives a bad goal.
have : size as - i = Nat.succ (size as - i - 1) := by omega
rw [this]
simp [foldl, foldlM, Nat.sub_add_eq]
· dsimp [foldl, foldlM]
simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
· dsimp [foldl, Id.run, foldlM]
rw [dif_pos (by omega), foldlM.loop, dif_neg h]
rfl
termination_by as.size - i
@@ -1592,8 +1602,8 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
as.toList ++ List.filterMap f xs := ?_
exact this #[]
induction xs
· simp_all
· simp_all [List.filterMap_cons]
· simp_all [Id.run]
· simp_all [Id.run, List.filterMap_cons]
split <;> simp_all
@[grind] theorem toList_filterMap {f : α Option β} {xs : Array α} :
@@ -1807,8 +1817,7 @@ theorem toArray_append {xs : List α} {ys : Array α} :
theorem singleton_eq_toArray_singleton {a : α} : #[a] = [a].toArray := rfl
@[deprecated empty_append (since := "2025-05-26")]
theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
@[simp] theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by
funext l
simp
@@ -1959,8 +1968,8 @@ theorem append_left_inj {xs₁ xs₂ : Array α} (ys) : xs₁ ++ ys = xs₂ ++ y
theorem eq_empty_of_append_eq_empty {xs ys : Array α} (h : xs ++ ys = #[]) : xs = #[] ys = #[] :=
append_eq_empty_iff.mp h
theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys xs = #[] ys = #[] := by
simp
@[simp] theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys xs = #[] ys = #[] := by
rw [eq_comm, append_eq_empty_iff]
theorem append_ne_empty_of_left_ne_empty {xs ys : Array α} (h : xs #[]) : xs ++ ys #[] := by
simp_all
@@ -2028,7 +2037,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
simp only [List.append_toArray, List.set_toArray, List.set_append]
split <;> simp
@[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) :
@[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) :
(xs ++ ys).set i x (by simp; omega) = xs.set i x ++ ys := by
simp [set_append, h]
@@ -2103,13 +2112,14 @@ theorem append_eq_map_iff {f : α → β} :
| nil => simp
| cons as => induction as.toList <;> simp [*]
@[simp] theorem flatten_toArray_map {L : List (List α)} :
(L.map List.toArray).toArray.flatten = L.flatten.toArray := by
@[simp] theorem flatten_map_toArray {L : List (List α)} :
(L.toArray.map List.toArray).flatten = L.flatten.toArray := by
apply ext'
simp [Function.comp_def]
theorem flatten_map_toArray {L : List (List α)} :
(L.toArray.map List.toArray).flatten = L.flatten.toArray := by
@[simp] theorem flatten_toArray_map {L : List (List α)} :
(L.map List.toArray).toArray.flatten = L.flatten.toArray := by
rw [ flatten_map_toArray]
simp
-- We set this to lower priority so that `flatten_toArray_map` is applied first when relevant.
@@ -2137,8 +2147,8 @@ theorem mem_flatten : ∀ {xss : Array (Array α)}, a ∈ xss.flatten ↔ ∃ xs
induction xss using array₂_induction
simp
theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten xs xss, xs = #[] := by
simp
@[simp] theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten xs xss, xs = #[] := by
rw [eq_comm, flatten_eq_empty_iff]
theorem flatten_ne_empty_iff {xss : Array (Array α)} : xss.flatten #[] xs, xs xss xs #[] := by
simp
@@ -2278,9 +2288,15 @@ theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} :
rw [List.map_inj_right]
simp +contextual
theorem flatten_toArray_map_toArray {xss : List (List α)} :
@[simp] theorem flatten_toArray_map_toArray {xss : List (List α)} :
(xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
simp
simp [flatten]
suffices as, List.foldl (fun acc bs => acc ++ bs) 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]
/-! ### flatMap -/
@@ -2310,9 +2326,13 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α}
intro cs
induction as generalizing cs <;> simp_all
theorem flatMap_toArray {β} {f : α Array β} {as : List α} :
@[simp, grind =] theorem flatMap_toArray {β} {f : α Array β} {as : List α} :
as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
simp
induction as with
| nil => simp
| cons a as ih =>
apply ext'
simp [ih, flatMap_toArray_cons]
@[simp] theorem flatMap_id {xss : Array (Array α)} : xss.flatMap id = xss.flatten := by simp [flatMap_def]
@@ -2778,7 +2798,7 @@ theorem reverse_eq_iff {xs ys : Array α} : xs.reverse = ys ↔ xs = ys.reverse
cases xs
simp
@[grind _=_] theorem filterMap_reverse {f : α Option β} {xs : Array α} : (xs.reverse.filterMap f) = (xs.filterMap f).reverse := by
@[grind _=_]theorem filterMap_reverse {f : α Option β} {xs : Array α} : (xs.reverse.filterMap f) = (xs.filterMap f).reverse := by
cases xs
simp
@@ -3014,21 +3034,19 @@ theorem take_size {xs : Array α} : xs.take xs.size = xs := by
| succ n ih =>
simp [shrink.loop, ih]
-- This doesn't need to be a simp lemma, as shortly we will simplify `shrink` to `take`.
theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by
@[simp] theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by
simp [shrink]
omega
-- This doesn't need to be a simp lemma, as shortly we will simplify `shrink` to `take`.
theorem getElem_shrink {xs : Array α} {i j : Nat} (h : j < (xs.shrink i).size) :
(xs.shrink i)[j] = xs[j]'(by simp [size_shrink] at h; omega) := by
@[simp] theorem getElem_shrink {xs : Array α} {i j : Nat} (h : j < (xs.shrink i).size) :
(xs.shrink i)[j] = xs[j]'(by simp at h; omega) := by
simp [shrink]
@[simp] theorem shrink_eq_take {xs : Array α} {i : Nat} : xs.shrink i = xs.take i := by
ext <;> simp [size_shrink, getElem_shrink]
@[simp] theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by
apply List.ext_getElem <;> simp
theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by
simp
@[simp] theorem shrink_eq_take {xs : Array α} {i : Nat} : xs.shrink i = xs.take i := by
ext <;> simp
/-! ### foldlM and foldrM -/
@@ -3197,16 +3215,18 @@ theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Array α} {a : α} {f : β
rw [foldr, foldrM_start_stop, foldrM_toList, List.foldrM_pure, foldr_toList, foldr, foldrM_start_stop]
theorem foldl_eq_foldlM {f : β α β} {b} {xs : Array α} {start stop : Nat} :
xs.foldl f b start stop = (xs.foldlM (m := Id) (pure <| f · ·) b start stop).run := rfl
xs.foldl f b start stop = xs.foldlM (m := Id) f b start stop := by
simp [foldl, Id.run]
theorem foldr_eq_foldrM {f : α β β} {b} {xs : Array α} {start stop : Nat} :
xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
xs.foldr f b start stop = xs.foldrM (m := Id) f b start stop := by
simp [foldr, Id.run]
@[simp] theorem id_run_foldlM {f : β α Id β} {b} {xs : Array α} {start stop : Nat} :
Id.run (xs.foldlM f b start stop) = xs.foldl (f · · |>.run) b start stop := rfl
Id.run (xs.foldlM f b start stop) = xs.foldl f b start stop := foldl_eq_foldlM.symm
@[simp] theorem id_run_foldrM {f : α β Id β} {b} {xs : Array α} {start stop : Nat} :
Id.run (xs.foldrM f b start stop) = xs.foldr (f · · |>.run) b start stop := rfl
Id.run (xs.foldrM f b start stop) = xs.foldr f b start stop := foldr_eq_foldrM.symm
/-- Variant of `foldlM_reverse` with a side condition for the `stop` argument. -/
@[simp] theorem foldlM_reverse' [Monad m] {xs : Array α} {f : β α m β} {b} {stop : Nat}
@@ -3235,7 +3255,7 @@ theorem foldrM_reverse [Monad m] {xs : Array α} {f : α → β → m β} {b} :
theorem foldrM_push [Monad m] {f : α β m β} {init : β} {xs : Array α} {a : α} :
(xs.push a).foldrM f init = f a init >>= xs.foldrM f := by
simp only [foldrM_eq_reverse_foldlM_toList, toList_push, List.reverse_append, List.reverse_cons,
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]
/--
@@ -3506,16 +3526,17 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
@[simp] theorem foldr_append' {f : α β β} {b} {xs ys : Array α} {start : Nat}
(w : start = xs.size + ys.size) :
(xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) :=
foldrM_append' w
(xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) := by
subst w
simp [foldr_eq_foldrM]
@[grind _=_] theorem foldl_append {β : Type _} {f : β α β} {b} {xs ys : Array α} :
(xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) :=
foldlM_append
@[grind _=_]theorem foldl_append {β : Type _} {f : β α β} {b} {xs ys : Array α} :
(xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by
simp [foldl_eq_foldlM]
@[grind _=_] theorem foldr_append {f : α β β} {b} {xs ys : Array α} :
(xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) :=
foldrM_append
(xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by
simp [foldr_eq_foldrM]
@[simp] theorem foldl_flatten' {f : β α β} {b} {xss : Array (Array α)} {stop : Nat}
(w : stop = xss.flatten.size) :
@@ -3544,22 +3565,21 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
/-- Variant of `foldl_reverse` with a side condition for the `stop` argument. -/
@[simp] theorem foldl_reverse' {xs : Array α} {f : β α β} {b} {stop : Nat}
(w : stop = xs.size) :
xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b :=
foldlM_reverse' w
xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b := by
simp [w, foldl_eq_foldlM, foldr_eq_foldrM]
/-- Variant of `foldr_reverse` with a side condition for the `start` argument. -/
@[simp] theorem foldr_reverse' {xs : Array α} {f : α β β} {b} {start : Nat}
(w : start = xs.size) :
xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b :=
foldrM_reverse' w
xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b := by
simp [w, foldl_eq_foldlM, foldr_eq_foldrM]
@[grind] theorem foldl_reverse {xs : Array α} {f : β α β} {b} :
xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b :=
foldlM_reverse
xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
@[grind] theorem foldr_reverse {xs : Array α} {f : α β β} {b} :
xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b :=
foldrM_reverse
(foldl_reverse ..).symm.trans <| by simp
theorem foldl_eq_foldr_reverse {xs : Array α} {f : β α β} {b} :
xs.foldl f b = xs.reverse.foldr (fun x y => f y x) b := by simp
@@ -3640,7 +3660,7 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} {r : β
theorem back?_eq_some_iff {xs : Array α} {a : α} :
xs.back? = some a ys : Array α, xs = ys.push a := by
rcases xs with xs
simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, toList_push]
simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, push_toList]
constructor
· rintro ys, rfl
exact ys.toArray, by simp
@@ -3765,7 +3785,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
rcases xs with xs
simp [List.contains_iff_exists_mem_beq]
@[grind _=_]
@[grind]
theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
xs.contains a a xs := by
simp
@@ -4074,16 +4094,15 @@ abbrev all_mkArray := @all_replicate
/-! ### modify -/
@[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α α} : (xs.modify i f).size = xs.size := by
unfold modify modifyM
unfold modify modifyM Id.run
split <;> simp
theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
(xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by
simp only [modify, modifyM]
simp only [modify, modifyM, Id.run, Id.pure_eq]
split
· simp only [getElem_set, Id.run_pure, Id.run_bind]; split <;> simp [*]
· simp only [Id.run_pure]
rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
· simp only [Id.bind_eq, getElem_set]; split <;> simp [*]
· rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
@[simp] theorem toList_modify {xs : Array α} {f : α α} {i : Nat} :
(xs.modify i f).toList = xs.toList.modify i f := by
@@ -4411,8 +4430,7 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i
/-! # mem -/
@[deprecated mem_toList_iff (since := "2025-05-26")]
theorem mem_toList {a : α} {xs : Array α} : a xs.toList a xs := mem_def.symm
@[simp, grind =] theorem mem_toList {a : α} {xs : Array α} : a xs.toList a xs := mem_def.symm
@[deprecated not_mem_empty (since := "2025-03-25")]
theorem not_mem_nil (a : α) : ¬ a #[] := nofun
@@ -4461,7 +4479,7 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
simp
@[simp, grind =] theorem forIn'_toList [Monad m] {xs : Array α} {b : β} {f : (a : α) a xs.toList β m (ForInStep β)} :
forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList_iff.mpr m) b) := by
forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList.mpr m) b) := by
cases xs
simp
@@ -4558,8 +4576,8 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by simp
@[grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
simp
@[simp, grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
apply Array.ext <;> simp
@[simp, grind =] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α m β} {l : List α} :
l.toArray.mapM f = List.toArray <$> l.mapM f := by
@@ -4625,12 +4643,12 @@ namespace Array
@[simp] theorem findSomeRev?_eq_findSome?_reverse {f : α Option β} {xs : Array α} :
xs.findSomeRev? f = xs.reverse.findSome? f := by
cases xs
simp [findSomeRev?]
simp [findSomeRev?, Id.run]
@[simp] theorem findRev?_eq_find?_reverse {f : α Bool} {xs : Array α} :
xs.findRev? f = xs.reverse.find? f := by
cases xs
simp [findRev?]
simp [findRev?, Id.run]
/-! ### unzip -/

View File

@@ -29,12 +29,16 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys
Decidable.not_not
@[simp] theorem lex_empty [BEq α] {lt : α α Bool} {xs : Array α} : xs.lex #[] lt = false := by
simp [lex]
simp [lex, Id.run]
@[simp] theorem singleton_lex_singleton [BEq α] {lt : α α Bool} : #[a].lex #[b] lt = lt a b := by
simp only [lex, List.getElem_toArray, List.getElem_singleton]
cases lt a b <;> cases a != b <;> simp [Id.run]
private theorem cons_lex_cons [BEq α] {lt : α α Bool} {a b : α} {xs ys : Array α} :
(#[a] ++ xs).lex (#[b] ++ ys) lt =
(lt a b || a == b && xs.lex ys lt) := by
simp only [lex]
simp only [lex, Id.run]
simp only [Std.Range.forIn'_eq_forIn'_range', size_append, List.size_toArray, List.length_singleton,
Nat.add_comm 1]
simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left,
@@ -47,16 +51,13 @@ private theorem cons_lex_cons [BEq α] {lt : αα → Bool} {a b : α} {xs
@[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α α Bool} {l₁ l₂ : List α} :
l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
induction l₁ generalizing l₂ with
| nil => cases l₂ <;> simp [lex]
| nil => cases l₂ <;> simp [lex, Id.run]
| cons x l₁ ih =>
cases l₂ with
| nil => simp [lex]
| nil => simp [lex, Id.run]
| cons y l₂ =>
rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
theorem singleton_lex_singleton [BEq α] {lt : α α Bool} : #[a].lex #[b] lt = lt a b := by
simp
@[simp, grind =] theorem lex_toList [BEq α] {lt : α α Bool} {xs ys : Array α} :
xs.toList.lex ys.toList lt = xs.lex ys lt := by
cases xs <;> cases ys <;> simp

View File

@@ -27,7 +27,7 @@ theorem mapFinIdx_induction (xs : Array α) (f : (i : Nat) → α → (h : i < x
motive xs.size eq : (Array.mapFinIdx xs f).size = xs.size,
i h, p i ((Array.mapFinIdx xs f)[i]) h := by
let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : i h h', p i bs[i] h) (hm : motive j) :
let as : Array β := Id.run <| Array.mapFinIdxM.map xs (pure <| f · · ·) i j h bs
let as : Array β := Array.mapFinIdxM.map (m := Id) xs f i j h bs
motive xs.size eq : as.size = xs.size, i h, p i as[i] h := by
induction i generalizing j bs with simp [mapFinIdxM.map]
| zero =>

View File

@@ -25,10 +25,10 @@ open Nat
/-! ## Monadic operations -/
theorem map_toList_inj [Monad m] [LawfulMonad m]
@[simp] theorem map_toList_inj [Monad m] [LawfulMonad m]
{xs : m (Array α)} {ys : m (Array α)} :
toList <$> xs = toList <$> ys xs = ys := by
simp
toList <$> xs = toList <$> ys xs = ys :=
_root_.map_inj_right (by simp)
/-! ### mapM -/
@@ -36,11 +36,7 @@ theorem map_toList_inj [Monad m] [LawfulMonad m]
xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by
induction xs; simp_all
@[simp] theorem idRun_mapM {xs : Array α} {f : α Id β} : (xs.mapM f).run = xs.map (f · |>.run) :=
mapM_pure
@[deprecated idRun_mapM (since := "2025-05-21")]
theorem mapM_id {xs : Array α} {f : α Id β} : xs.mapM f = xs.map f :=
@[simp] theorem mapM_id {xs : Array α} {f : α Id β} : xs.mapM f = xs.map f :=
mapM_pure
@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α β} {g : β m γ} {xs : Array α} :
@@ -195,18 +191,12 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
rcases xs with xs
simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
theorem idRun_forIn'_yield_eq_foldl
{xs : Array α} (f : (a : α) a xs β Id β) (init : β) :
(forIn' xs init (fun a m b => .yield <$> f a m b)).run =
xs.attach.foldl (fun b a, h => f a h b |>.run) init := by
simp
@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
theorem forIn'_yield_eq_foldl
@[simp] theorem forIn'_yield_eq_foldl
{xs : Array α} (f : (a : α) a xs β β) (init : β) :
forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) =
xs.attach.foldl (fun b a, h => f a h b) init :=
forIn'_pure_yield_eq_foldl _ _
xs.attach.foldl (fun b a, h => f a h b) init := by
rcases xs with xs
simp [List.foldl_map]
@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
{xs : Array α} (g : α β) (f : (b : β) b xs.map g γ m (ForInStep γ)) :
@@ -243,18 +233,12 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
rcases xs with xs
simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
theorem idRun_forIn_yield_eq_foldl
{xs : Array α} (f : α β Id β) (init : β) :
(forIn xs init (fun a b => .yield <$> f a b)).run =
xs.foldl (fun b a => f a b |>.run) init := by
simp
@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
theorem forIn_yield_eq_foldl
@[simp] theorem forIn_yield_eq_foldl
{xs : Array α} (f : α β β) (init : β) :
forIn (m := Id) xs init (fun a b => .yield (f a b)) =
xs.foldl (fun b a => f a b) init :=
forIn_pure_yield_eq_foldl _ _
xs.foldl (fun b a => f a b) init := by
rcases xs with xs
simp [List.foldl_map]
@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
{xs : Array α} {g : α β} {f : β γ m (ForInStep γ)} :

View File

@@ -129,6 +129,7 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
@[simp, grind =] theorem idRun_ofFnM {f : Fin n Id α} :
Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
unfold Id.run
induction n with
| zero => simp
| succ n ih => simp [ofFnM_succ', ofFn_succ', ih]

View File

@@ -27,27 +27,23 @@ Internal implementation of `Array.qsort`.
It does so by first swapping the elements at indices `lo`, `mid := (lo + hi) / 2`, and `hi`
if necessary so that the middle (pivot) element is at index `hi`.
We then iterate from `k = lo` to `k = hi`, with a pointer `i` starting at `lo`, and
We then iterate from `j = lo` to `j = hi`, with a pointer `i` starting at `lo`, and
swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
-/
def qpartition {n} (as : Vector α n) (lt : α α Bool) (lo hi : Nat) (w : lo hi := by omega)
(hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo m m hi} × Vector α n :=
def qpartition {n} (as : Vector α n) (lt : α α Bool) (lo hi : Nat)
(hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo m m < n} × Vector α n :=
let mid := (lo + hi) / 2
let as := if lt as[mid] as[lo] then as.swap lo mid else as
let as := if lt as[hi] as[lo] then as.swap lo hi else as
let as := if lt as[mid] as[hi] then as.swap mid hi else as
let pivot := as[hi]
-- During this loop, elements below in `[lo, i)` are less than `pivot`,
-- elements in `[i, k)` are greater than or equal to `pivot`,
-- elements in `[k, hi)` are unexamined,
-- while `as[hi]` is (by definition) the pivot.
let rec loop (as : Vector α n) (i k : Nat)
(ilo : lo i := by omega) (ik : i k := by omega) (w : k hi := by omega) :=
if h : k < hi then
if lt as[k] pivot then
loop (as.swap i k) (i+1) (k+1)
let rec loop (as : Vector α n) (i j : Nat)
(ilo : lo i := by omega) (jh : j < n := by omega) (w : i j := by omega) :=
if h : j < hi then
if lt as[j] pivot then
loop (as.swap i j) (i+1) (j+1)
else
loop as i (k+1)
loop as i (j+1)
else
(i, ilo, by omega, as.swap i hi)
loop as lo lo
@@ -55,28 +51,25 @@ def qpartition {n} (as : Vector α n) (lt : αα → Bool) (lo hi : Nat) (w
/--
In-place quicksort.
`qsort as lt lo hi` sorts the subarray `as[lo:hi+1]` in-place using `lt` to compare elements.
`qsort as lt low high` sorts the subarray `as[low:high+1]` in-place using `lt` to compare elements.
-/
@[inline] def qsort (as : Array α) (lt : α α Bool := by exact (· < ·))
(lo := 0) (hi := as.size - 1) : Array α :=
let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat) (w : lo hi := by omega)
(low := 0) (high := as.size - 1) : Array α :=
let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
(hlo : lo < n := by omega) (hhi : hi < n := by omega) :=
if h₁ : lo < hi then
let mid, hmid, as := qpartition as lt lo hi
if h₂ : mid hi then
-- This only occurs when `hi ≤ lo`,
-- and thus `as[lo:hi+1]` is trivially already sorted.
as
else
-- Otherwise, we recursively sort the two subarrays.
sort (sort as lo mid) (mid+1) hi
else as
if h : as.size = 0 then
as
else
let lo := min lo (as.size - 1)
let hi := max lo (min hi (as.size - 1))
sort as.toVector lo hi |>.toArray
let low := min low (as.size - 1)
let high := min high (as.size - 1)
sort as.toVector low high |>.toArray
set_option linter.unusedVariables.funArgs false in
/--

View File

@@ -290,7 +290,7 @@ Examples:
-/
@[inline]
def foldl {α : Type u} {β : Type v} (f : β α β) (init : β) (as : Subarray α) : β :=
Id.run <| as.foldlM (pure <| f · ·) (init := init)
Id.run <| as.foldlM f (init := init)
/--
Folds an operation from right to left over the elements in a subarray.
@@ -304,7 +304,7 @@ Examples:
-/
@[inline]
def foldr {α : Type u} {β : Type v} (f : α β β) (init : β) (as : Subarray α) : β :=
Id.run <| as.foldrM (pure <| f · ·) (init := init)
Id.run <| as.foldrM f (init := init)
/--
Checks whether any of the elements in a subarray satisfy a Boolean predicate.
@@ -314,7 +314,7 @@ an element that satisfies the predicate is found.
-/
@[inline]
def any {α : Type u} (p : α Bool) (as : Subarray α) : Bool :=
Id.run <| as.anyM (pure <| p ·)
Id.run <| as.anyM p
/--
Checks whether all of the elements in a subarray satisfy a Boolean predicate.
@@ -324,7 +324,7 @@ an element that does not satisfy the predicate is found.
-/
@[inline]
def all {α : Type u} (p : α Bool) (as : Subarray α) : Bool :=
Id.run <| as.allM (pure <| p ·)
Id.run <| as.allM p
/--
Applies a monadic function to each element in a subarray in reverse order, stopping at the first
@@ -394,7 +394,7 @@ Examples:
-/
@[inline]
def findRev? {α : Type} (as : Subarray α) (p : α Bool) : Option α :=
Id.run <| as.findRevM? (pure <| p ·)
Id.run <| as.findRevM? p
end Subarray

View File

@@ -334,13 +334,11 @@ abbrev zipWithAll_mkArray := @zipWithAll_replicate
/-! ### unzip -/
@[deprecated fst_unzip (since := "2025-05-26")]
theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
simp
@[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by
induction l <;> simp_all
@[deprecated snd_unzip (since := "2025-05-26")]
theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
simp
@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by
induction l <;> simp_all
theorem unzip_eq_map {xs : Array (α × β)} : unzip xs = (xs.map Prod.fst, xs.map Prod.snd) := by
cases xs
@@ -373,7 +371,7 @@ theorem unzip_zip {as : Array α} {bs : Array β} (h : as.size = bs.size) :
theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl : xs.map Prod.fst = as)
(hr : xs.map Prod.snd = bs) : xs = as.zip bs := by
rw [ hl, hr, zip_unzip xs, fst_unzip, snd_unzip, zip_unzip, zip_unzip]
rw [ hl, hr, zip_unzip xs, unzip_fst, unzip_snd, zip_unzip, zip_unzip]
@[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by

View File

@@ -68,11 +68,11 @@ theorem lt_of_getMsbD {x : BitVec w} {i : Nat} : getMsbD x i = true → i < w :=
@[simp] theorem getElem?_eq_getElem {l : BitVec w} {n} (h : n < w) : l[n]? = some l[n] := by
simp only [getElem?_def, h, reduceDIte]
theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a h : n < w, l[n] = a :=
_root_.getElem?_eq_some_iff
theorem some_eq_getElem?_iff {l : BitVec w} : some a = l[n]? h : n < w, l[n] = a :=
_root_.some_eq_getElem?_iff
theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a h : n < w, l[n] = a := by
simp only [getElem?_def]
split
· simp_all
· simp; omega
theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a h : n < w, l[n] = a :=
getElem?_eq_some_iff.mp
@@ -81,11 +81,11 @@ set_option linter.missingDocs false in
@[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
abbrev getElem?_eq_some := @getElem?_eq_some_iff
theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none w n := by
simp
theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? w n := by
simp
@[simp] theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none w n := by
simp only [getElem?_def]
split
· simp_all
· simp; omega
theorem getElem?_eq_none {l : BitVec w} (h : w n) : l[n]? = none := getElem?_eq_none_iff.mpr h
@@ -93,13 +93,13 @@ theorem getElem?_eq (l : BitVec w) (i : Nat) :
l[i]? = if h : i < w then some l[i] else none := by
split <;> simp_all
theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
@[simp] theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
(some l[i] = l[i]?) True := by
simp
simp [h]
theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
@[simp] theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
(l[i]? = some l[i]) True := by
simp
simp [h]
theorem getElem_eq_iff {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x l[n]? = some x := by
simp only [getElem?_eq_some_iff]
@@ -505,7 +505,7 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) &&
· simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
by_cases hi : i = 0 <;> simp [hi] <;> omega
theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
@[simp] theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
@[simp]
theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
@@ -3179,11 +3179,11 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
· simp [Nat.mod_eq_of_lt b.toNat_lt]
· simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
@[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
@[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
simp [getElem_concat]
theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
simp
@[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by
simp [getElem_concat]
@[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by
simp [getLsbD_concat]

View File

@@ -205,7 +205,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
@[inline]
def foldl {β : Type v} (f : β UInt8 β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
Id.run <| as.foldlM (pure <| f · ·) init start stop
Id.run <| as.foldlM f init start stop
/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.

View File

@@ -266,7 +266,7 @@ theorem foldl_add (f : α → Fin (n + m) → α) (x) :
| succ m ih => simp [foldl_succ_last, ih, Nat.add_assoc]
theorem foldl_eq_foldlM (f : α Fin n α) (x) :
foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by
foldl n f x = foldlM (m:=Id) n f x := by
induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
-- This is not marked `@[simp]` as it would match on every occurrence of `foldlM`.
@@ -319,7 +319,7 @@ theorem foldr_add (f : Fin (n + m) → αα) (x) :
| succ m ih => simp [foldr_succ_last, ih, Nat.add_assoc]
theorem foldr_eq_foldrM (f : Fin n α α) (x) :
foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by
foldr n f x = foldrM (m:=Id) n f x := by
induction n <;> simp [foldr_succ, foldrM_succ, *]
theorem foldl_rev (f : Fin n α α) (x) :

View File

@@ -165,7 +165,7 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float →
@[inline]
def foldl {β : Type v} (f : β Float β) (init : β) (as : FloatArray) (start := 0) (stop := as.size) : β :=
Id.run <| as.foldlM (pure <| f · ·) init start stop
Id.run <| as.foldlM f init start stop
end FloatArray

View File

@@ -264,8 +264,8 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
match k, h with
| _, t, rfl => rw [Int.mul_assoc, add_mul_emod_self_left]
theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
simp
@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
conv => rhs; rw [ emod_add_ediv a b, add_mul_emod_self_left]
theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
apply (emod_add_cancel_right b).mp

View File

@@ -1410,7 +1410,8 @@ theorem mul_tmod (a b n : Int) : (a * b).tmod n = (a.tmod n * b.tmod n).tmod n :
norm_cast at h
rw [Nat.mod_mod_of_dvd _ h]
theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b := by simp
@[simp] theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b :=
tmod_tmod_of_dvd a (Int.dvd_refl b)
theorem tmod_eq_zero_of_dvd : {a b : Int}, a b tmod b a = 0
| _, _, _, rfl => mul_tmod_right ..
@@ -1468,8 +1469,9 @@ protected theorem tdiv_mul_cancel {a b : Int} (H : b a) : a.tdiv b * b = a :
protected theorem mul_tdiv_cancel' {a b : Int} (H : a b) : a * b.tdiv a = b := by
rw [Int.mul_comm, Int.tdiv_mul_cancel H]
theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by
simp
@[simp] theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by
rw [ dvd_iff_tmod_eq_zero, Int.dvd_neg]
exact Int.dvd_refl a
theorem lt_tdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.tdiv b + 1) * b := by
rw [Int.add_mul, Int.one_mul, Int.mul_comm]
@@ -1566,11 +1568,13 @@ theorem dvd_tmod_sub_self {x m : Int} : m x.tmod m - x := by
theorem dvd_self_sub_tmod {x m : Int} : m x - x.tmod m :=
Int.dvd_neg.1 (by simpa only [Int.neg_sub] using dvd_tmod_sub_self)
theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by
simp
@[simp] theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by
rw [ dvd_iff_tmod_eq_zero, Int.dvd_neg]
exact Int.dvd_mul_right a b
theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by
simp
@[simp] theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by
rw [ dvd_iff_tmod_eq_zero, Int.dvd_neg]
exact Int.dvd_mul_left a b
@[simp] protected theorem tdiv_one : a : Int, a.tdiv 1 = a
| (n:Nat) => congrArg ofNat (Nat.div_one _)
@@ -2189,8 +2193,8 @@ theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n :
match k, h with
| _, t, rfl => rw [Int.mul_assoc, add_mul_fmod_self_left]
theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b := by
simp
@[simp] theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b :=
fmod_fmod_of_dvd _ (Int.dvd_refl b)
theorem sub_fmod (a b n : Int) : (a - b).fmod n = (a.fmod n - b.fmod n).fmod n := by
apply (fmod_add_cancel_right b).mp

View File

@@ -254,7 +254,7 @@ pointer-equal to its argument.
For verification purposes, `List.mapMono = List.map`.
-/
def mapMono (as : List α) (f : α α) : List α :=
Id.run <| as.mapMonoM (pure <| f ·)
Id.run <| as.mapMonoM f
/-! ## Additional lemmas required for bootstrapping `Array`. -/

View File

@@ -348,16 +348,9 @@ theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List
| false => simp [ih]
@[simp]
theorem idRun_findM? (p : α Id Bool) (as : List α) :
(findM? p as).run = as.find? (p · |>.run) :=
theorem findM?_id (p : α Bool) (as : List α) : findM? (m := Id) p as = as.find? p :=
findM?_pure _ _
@[deprecated idRun_findM? (since := "2025-05-21")]
theorem findM?_id (p : α Id Bool) (as : List α) :
findM? (m := Id) p as = as.find? p :=
findM?_pure _ _
/--
Returns the first non-`none` result of applying the monadic function `f` to each element of the
list, in order. Returns `none` if `f` returns `none` for all elements.
@@ -401,13 +394,7 @@ theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α → Option β} {as : L
| none => simp [ih]
@[simp]
theorem idRun_findSomeM? (f : α Id (Option β)) (as : List α) :
(findSomeM? f as).run = as.findSome? (f · |>.run) :=
findSomeM?_pure
@[deprecated idRun_findSomeM? (since := "2025-05-21")]
theorem findSomeM?_id (f : α Id (Option β)) (as : List α) :
findSomeM? (m := Id) f as = as.findSome? f :=
theorem findSomeM?_id {f : α Option β} {as : List α} : findSomeM? (m := Id) f as = as.findSome? f :=
findSomeM?_pure
theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α m Bool} {as : List α} :

View File

@@ -1108,9 +1108,14 @@ theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
simp only [finIdxOf?_cons]
split <;> simp_all [@eq_comm _ x a]
@[simp]
theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
(l.finIdxOf? a).isNone = ¬ a l := by
simp
induction l with
| nil => simp
| cons x xs ih =>
simp only [finIdxOf?_cons]
split <;> simp_all [@eq_comm _ x a]
/-! ### idxOf?
@@ -1149,9 +1154,15 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
simp only [idxOf?_cons]
split <;> simp_all [@eq_comm _ x a]
@[simp]
theorem isNone_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
(l.idxOf? a).isNone = ¬ a l := by
simp
induction l with
| nil => simp
| cons x xs ih =>
simp only [idxOf?_cons]
split <;> simp_all [@eq_comm _ x a]
/-! ### lookup -/

View File

@@ -109,7 +109,7 @@ Example:
let rec go : as acc, filterMapTR.go f as acc = acc.toList ++ as.filterMap f
| [], acc => by simp [filterMapTR.go, filterMap]
| a::as, acc => by
simp only [filterMapTR.go, go as, Array.toList_push, append_assoc, singleton_append,
simp only [filterMapTR.go, go as, Array.push_toList, append_assoc, singleton_append,
filterMap]
split <;> simp [*]
exact (go l #[]).symm

View File

@@ -272,13 +272,13 @@ theorem getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.len
theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? h : i < l.length, l[i] = a := by
rw [eq_comm, getElem?_eq_some_iff]
theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) :
@[simp] theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) :
(some xs[i] = xs[i]?) True := by
simp
simp [h]
theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) :
@[simp] theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) :
(xs[i]? = some xs[i]) True := by
simp
simp [h]
theorem getElem_eq_iff {l : List α} {i : Nat} (h : i < l.length) : l[i] = x l[i]? = some x := by
simp only [getElem?_eq_some_iff]
@@ -296,7 +296,7 @@ theorem getD_getElem? {l : List α} {i : Nat} {d : α} :
have p : i l.length := Nat.le_of_not_gt h
simp [getElem?_eq_none p, h]
@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a := by
@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a :=
match i, h with
| 0, _ => rfl
@@ -434,8 +434,8 @@ theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := b
theorem eq_of_mem_singleton : a [b] a = b
| .head .. => rfl
theorem mem_singleton {a b : α} : a [b] a = b := by
simp
@[simp] theorem mem_singleton {a b : α} : a [b] a = b :=
eq_of_mem_singleton, (by simp [·])
theorem forall_mem_cons {p : α Prop} {a : α} {l : List α} :
( x, x a :: l p x) p a x, x l p x :=
@@ -1685,8 +1685,8 @@ theorem getLast_concat {a : α} : ∀ {l : List α}, getLast (l ++ [a]) (by simp
@[deprecated append_eq_nil_iff (since := "2025-01-13")] abbrev append_eq_nil := @append_eq_nil_iff
theorem nil_eq_append_iff : [] = a ++ b a = [] b = [] := by
simp
@[simp] theorem nil_eq_append_iff : [] = a ++ b a = [] b = [] := by
rw [eq_comm, append_eq_nil_iff]
@[grind ]
theorem eq_nil_of_append_eq_nil {l₁ l₂ : List α} (h : l₁ ++ l₂ = []) : l₁ = [] l₂ = [] :=
@@ -1897,8 +1897,8 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∃ l' b, l = concat l' b
@[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] l L, l = [] := by
induction L <;> simp_all
theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten l L, l = [] := by
simp
@[simp] theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten l L, l = [] := by
rw [eq_comm, flatten_eq_nil_iff]
theorem flatten_ne_nil_iff {xss : List (List α)} : xss.flatten [] xs, xs xss xs [] := by
simp
@@ -2541,25 +2541,17 @@ theorem flatten_reverse {L : List (List α)} :
induction l generalizing b <;> simp [*]
theorem foldl_eq_foldlM {f : β α β} {b : β} {l : List α} :
l.foldl f b = (l.foldlM (m := Id) (pure <| f · ·) b).run := by
simp
l.foldl f b = l.foldlM (m := Id) f b := by
induction l generalizing b <;> simp [*, foldl]
theorem foldr_eq_foldrM {f : α β β} {b : β} {l : List α} :
l.foldr f b = (l.foldrM (m := Id) (pure <| f · ·) b).run := by
simp
l.foldr f b = l.foldrM (m := Id) f b := by
induction l <;> simp [*, foldr]
theorem idRun_foldlM {f : β α Id β} {b : β} {l : List α} :
Id.run (l.foldlM f b) = l.foldl (f · · |>.run) b := foldl_eq_foldlM.symm
@[deprecated idRun_foldlM (since := "2025-05-21")]
theorem id_run_foldlM {f : β α Id β} {b : β} {l : List α} :
@[simp] theorem id_run_foldlM {f : β α Id β} {b : β} {l : List α} :
Id.run (l.foldlM f b) = l.foldl f b := foldl_eq_foldlM.symm
theorem idRun_foldrM {f : α β Id β} {b : β} {l : List α} :
Id.run (l.foldrM f b) = l.foldr (f · · |>.run) b := foldr_eq_foldrM.symm
@[deprecated idRun_foldrM (since := "2025-05-21")]
theorem id_run_foldrM {f : α β Id β} {b : β} {l : List α} :
@[simp] theorem id_run_foldrM {f : α β Id β} {b : β} {l : List α} :
Id.run (l.foldrM f b) = l.foldr f b := foldr_eq_foldrM.symm
@[simp] theorem foldlM_reverse [Monad m] {l : List α} {f : β α m β} {b : β} :
@@ -2585,9 +2577,9 @@ theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
induction l generalizing l' <;> simp [*]
/-- Variant of `foldl_flip_cons_eq_append` specalized to `f = id`. -/
@[grind] theorem foldl_flip_cons_eq_append' {l l' : List α} :
@[simp, grind] theorem foldl_flip_cons_eq_append' {l l' : List α} :
l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := by
simp
induction l generalizing l' <;> simp [*]
@[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α List β} {l' : List β} :
l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
@@ -2654,10 +2646,10 @@ theorem foldr_map_hom {g : α → β} {f : ααα} {f' : β → β →
induction l <;> simp [*]
@[simp, grind _=_] theorem foldl_append {β : Type _} {f : β α β} {b : β} {l l' : List α} :
(l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM, -foldlM_pure]
(l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
@[simp, grind _=_] theorem foldr_append {f : α β β} {b : β} {l l' : List α} :
(l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM, -foldrM_pure]
(l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
@[grind] theorem foldl_flatten {f : β α β} {b : β} {L : List (List α)} :
(flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
@@ -2668,8 +2660,7 @@ theorem foldr_map_hom {g : α → β} {f : ααα} {f' : β → β →
induction L <;> simp_all
@[simp, grind] theorem foldl_reverse {l : List α} {f : β α β} {b : β} :
l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by
simp [foldl_eq_foldlM, foldr_eq_foldrM, -foldrM_pure]
l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
@[simp, grind] theorem foldr_reverse {l : List α} {f : α β β} {b : β} :
l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
@@ -2952,7 +2943,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
l.contains a a' l, a == a' := by
induction l <;> simp_all
@[grind _=_]
@[grind]
theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
l.contains a a l := by
simp
@@ -3427,8 +3418,8 @@ variable [LawfulBEq α]
| Or.inr h' => exact h'
else rw [insert_of_not_mem h, mem_cons]
theorem mem_insert_self {a : α} {l : List α} : a l.insert a := by
simp
@[simp] theorem mem_insert_self {a : α} {l : List α} : a l.insert a :=
mem_insert_iff.2 (Or.inl rfl)
theorem mem_insert_of_mem {l : List α} (h : a l) : a l.insert b :=
mem_insert_iff.2 (Or.inr h)

View File

@@ -348,7 +348,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
split <;> split
· simp only [Option.some.injEq]
rw [ Array.getElem_toList]
simp only [Array.toList_push]
simp only [Array.push_toList]
rw [getElem_append_left, Array.getElem_toList]
· have : i = acc.size := by omega
simp_all

View File

@@ -68,11 +68,7 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] {f : α → m β} {l : List α}
l.mapM (m := m) (pure <| f ·) = pure (l.map f) := by
induction l <;> simp_all
@[simp] theorem idRun_mapM {l : List α} {f : α Id β} : (l.mapM f).run = l.map (f · |>.run) :=
mapM_pure
@[deprecated idRun_mapM (since := "2025-05-21")]
theorem mapM_id {l : List α} {f : α Id β} : (l.mapM f).run = l.map (f · |>.run) :=
@[simp] theorem mapM_id {l : List α} {f : α Id β} : l.mapM f = l.map f :=
mapM_pure
@[simp] theorem mapM_map [Monad m] [LawfulMonad m] {f : α β} {g : β m γ} {l : List α} :
@@ -349,18 +345,12 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
simp only [forIn'_eq_foldlM]
induction l.attach generalizing init <;> simp_all
@[simp] theorem idRun_forIn'_yield_eq_foldl
(l : List α) (f : (a : α) a l β Id β) (init : β) :
(forIn' l init (fun a m b => .yield <$> f a m b)).run =
l.attach.foldl (fun b a, h => f a h b |>.run) init :=
forIn'_pure_yield_eq_foldl _ _
@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
theorem forIn'_yield_eq_foldl
@[simp] theorem forIn'_yield_eq_foldl
{l : List α} (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 :=
forIn'_pure_yield_eq_foldl _ _
l.attach.foldl (fun b a, h => f a h b) init := by
simp only [forIn'_eq_foldlM]
induction l.attach generalizing init <;> simp_all
@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
{l : List α} (g : α β) (f : (b : β) b l.map g γ m (ForInStep γ)) :
@@ -408,18 +398,12 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
simp only [forIn_eq_foldlM]
induction l generalizing init <;> simp_all
@[simp] theorem idRun_forIn_yield_eq_foldl
(l : List α) (f : α β Id β) (init : β) :
(forIn l init (fun a b => .yield <$> f a b)).run =
l.foldl (fun b a => f a b |>.run) init :=
forIn_pure_yield_eq_foldl _ _
@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
theorem forIn_yield_eq_foldl
@[simp] theorem forIn_yield_eq_foldl
{l : List α} (f : α β β) (init : β) :
forIn (m := Id) l init (fun a b => .yield (f a b)) =
l.foldl (fun b a => f a b) init :=
forIn_pure_yield_eq_foldl _ _
l.foldl (fun b a => f a b) init := by
simp only [forIn_eq_foldlM]
induction l generalizing init <;> simp_all
@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
{l : List α} {g : α β} {f : β γ m (ForInStep γ)} :

View File

@@ -56,7 +56,7 @@ theorem getElem?_take_eq_none {l : List α} {i j : Nat} (h : i ≤ j) :
(l.take i)[j]? = none :=
getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
@[grind =] theorem getElem?_take {l : List α} {i j : Nat} :
@[grind =]theorem getElem?_take {l : List α} {i j : Nat} :
(l.take i)[j]? = if j < i then l[j]? else none := by
split
· next h => exact getElem?_take_of_lt h

View File

@@ -71,7 +71,6 @@ protected theorem getElem?_ofFn {f : Fin n → α} :
theorem ofFn_zero {f : Fin 0 α} : ofFn f = [] := by
rw [ofFn, Fin.foldr_zero]
@[simp]
theorem ofFn_succ {n} {f : Fin (n + 1) α} : ofFn f = f 0 :: ofFn fun i => f i.succ :=
ext_get (by simp) (fun i hi₁ hi₂ => by
cases i
@@ -92,7 +91,7 @@ theorem ofFn_add {n m} {f : Fin (n + m) → α} :
ofFn f = (ofFn fun i => f (i.castLE (Nat.le_add_right n m))) ++ (ofFn fun i => f (i.natAdd n)) := by
induction m with
| zero => simp
| succ m ih => simp [-ofFn_succ, ofFn_succ_last, ih]
| succ m ih => simp [ofFn_succ_last, ih]
@[simp]
theorem ofFn_eq_nil_iff {f : Fin n α} : ofFn f = [] n = 0 := by
@@ -173,8 +172,9 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
@[simp, grind =] theorem idRun_ofFnM {f : Fin n Id α} :
Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
unfold Id.run
induction n with
| zero => simp
| succ n ih => simp [-ofFn_succ, ofFnM_succ_last, ofFn_succ_last, ih]
| succ n ih => simp [ofFnM_succ_last, ofFn_succ_last, ih]
end List

View File

@@ -24,7 +24,7 @@ open Nat
/-! ### Pairwise -/
@[grind ] theorem Pairwise.sublist : l₁ <+ l₂ l₂.Pairwise R l₁.Pairwise R
theorem Pairwise.sublist : l₁ <+ l₂ l₂.Pairwise R l₁.Pairwise R
| .slnil, h => h
| .cons _ s, .cons _ h₂ => h₂.sublist s
| .cons₂ _ s, .cons h₁ h₂ => (h₂.sublist s).cons fun _ h => h₁ _ (s.subset h)
@@ -37,11 +37,11 @@ theorem Pairwise.imp {α R S} (H : ∀ {a b}, R a b → S a b) :
theorem rel_of_pairwise_cons (p : (a :: l).Pairwise R) : {a'}, a' l R a a' :=
(pairwise_cons.1 p).1 _
@[grind ] theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
theorem Pairwise.of_cons (p : (a :: l).Pairwise R) : Pairwise R l :=
(pairwise_cons.1 p).2
set_option linter.unusedVariables false in
@[grind] theorem Pairwise.tail : {l : List α} (h : Pairwise R l), Pairwise R l.tail
theorem Pairwise.tail : {l : List α} (h : Pairwise R l), Pairwise R l.tail
| [], h => h
| _ :: _, h => h.of_cons
@@ -101,11 +101,11 @@ theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pa
· exact h₃.1 _ hx
· exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy
@[grind] theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
@[grind =] theorem pairwise_pair {a b : α} : Pairwise R [a, b] R a b := by simp
theorem pairwise_pair {a b : α} : Pairwise R [a, b] R a b := by simp
@[grind =] theorem pairwise_map {l : List α} :
theorem pairwise_map {l : List α} :
(l.map f).Pairwise R l.Pairwise fun a b => R (f a) (f b) := by
induction l
· simp
@@ -115,11 +115,11 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
(p : Pairwise S (map f l)) : Pairwise R l :=
(pairwise_map.1 p).imp (H _ _)
@[grind] theorem Pairwise.map {S : β β Prop} (f : α β) (H : a b : α, R a b S (f a) (f b))
theorem Pairwise.map {S : β β Prop} (f : α β) (H : a b : α, R a b S (f a) (f b))
(p : Pairwise R l) : Pairwise S (map f l) :=
pairwise_map.2 <| p.imp (H _ _)
@[grind =] theorem pairwise_filterMap {f : β Option α} {l : List β} :
theorem pairwise_filterMap {f : β Option α} {l : List β} :
Pairwise R (filterMap f l) Pairwise (fun a a' : β => b, f a = some b b', f a' = some b' R b b') l := by
let _S (a a' : β) := b, f a = some b b', f a' = some b' R b b'
induction l with
@@ -134,20 +134,20 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
simpa [IH, e] using fun _ =>
fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab
@[grind] theorem Pairwise.filterMap {S : β β Prop} (f : α Option β)
theorem Pairwise.filterMap {S : β β Prop} (f : α Option β)
(H : a a' : α, R a a' b, f a = some b b', f a' = some b' S b b') {l : List α} (p : Pairwise R l) :
Pairwise S (filterMap f l) :=
pairwise_filterMap.2 <| p.imp (H _ _)
@[grind =] theorem pairwise_filter {p : α Bool} {l : List α} :
theorem pairwise_filter {p : α Prop} [DecidablePred p] {l : List α} :
Pairwise R (filter p l) Pairwise (fun x y => p x p y R x y) l := by
rw [ filterMap_eq_filter, pairwise_filterMap]
simp
@[grind] theorem Pairwise.filter (p : α Bool) : Pairwise R l Pairwise R (filter p l) :=
theorem Pairwise.filter (p : α Bool) : Pairwise R l Pairwise R (filter p l) :=
Pairwise.sublist filter_sublist
@[grind =] theorem pairwise_append {l₁ l₂ : List α} :
theorem pairwise_append {l₁ l₂ : List α} :
(l₁ ++ l₂).Pairwise R l₁.Pairwise R l₂.Pairwise R a l₁, b l₂, R a b := by
induction l₁ <;> simp [*, or_imp, forall_and, and_assoc, and_left_comm]
@@ -157,13 +157,13 @@ theorem pairwise_append_comm {R : αα → Prop} (s : ∀ {x y}, R x y →
(x : α) (xm : x l₂) (y : α) (ym : y l₁) : R x y := s (H y ym x xm)
simp only [pairwise_append, and_left_comm]; rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
@[grind =] theorem pairwise_middle {R : α α Prop} (s : {x y}, R x y R y x) {a : α} {l₁ l₂ : List α} :
theorem pairwise_middle {R : α α Prop} (s : {x y}, R x y R y x) {a : α} {l₁ l₂ : List α} :
Pairwise R (l₁ ++ a :: l₂) Pairwise R (a :: (l₁ ++ l₂)) := by
show Pairwise R (l₁ ++ ([a] ++ l₂)) Pairwise R ([a] ++ l₁ ++ l₂)
rw [ append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]
simp only [mem_append, or_comm]
@[grind =] theorem pairwise_flatten {L : List (List α)} :
theorem pairwise_flatten {L : List (List α)} :
Pairwise R (flatten L)
( l L, Pairwise R l) Pairwise (fun l₁ l₂ => x l₁, y l₂, R x y) L := by
induction L with
@@ -174,16 +174,16 @@ theorem pairwise_append_comm {R : αα → Prop} (s : ∀ {x y}, R x y →
rw [and_comm, and_congr_left_iff]
intros; exact fun h l' b c d e => h c d e l' b, fun h c d e l' b => h l' b c d e
@[grind =] theorem pairwise_flatMap {R : β β Prop} {l : List α} {f : α List β} :
theorem pairwise_flatMap {R : β β Prop} {l : List α} {f : α List β} :
List.Pairwise R (l.flatMap f)
( a l, Pairwise R (f a)) Pairwise (fun a₁ a₂ => x f a₁, y f a₂, R x y) l := by
simp [List.flatMap, pairwise_flatten, pairwise_map]
@[grind =] theorem pairwise_reverse {l : List α} :
theorem pairwise_reverse {l : List α} :
l.reverse.Pairwise R l.Pairwise (fun a b => R b a) := by
induction l <;> simp [*, pairwise_append, and_comm]
@[simp, grind =] theorem pairwise_replicate {n : Nat} {a : α} :
@[simp] theorem pairwise_replicate {n : Nat} {a : α} :
(replicate n a).Pairwise R n 1 R a a := by
induction n with
| zero => simp
@@ -205,10 +205,10 @@ theorem pairwise_append_comm {R : αα → Prop} (s : ∀ {x y}, R x y →
simp
· exact fun _ => h, Or.inr h
@[grind] theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
h.sublist (drop_sublist _ _)
@[grind] theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
h.sublist (take_sublist _ _)
theorem pairwise_iff_forall_sublist : l.Pairwise R ( {a b}, [a,b] <+ l R a b) := by
@@ -247,7 +247,7 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : αα → Prop} (h :
intro a b hab
apply h <;> (apply hab.subset; simp)
@[grind =] theorem pairwise_pmap {p : β Prop} {f : b, p b α} {l : List β} (h : x l, p x) :
theorem pairwise_pmap {p : β Prop} {f : b, p b α} {l : List β} (h : x l, p x) :
Pairwise R (l.pmap f h)
Pairwise (fun b₁ b₂ => (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l := by
induction l with
@@ -259,7 +259,7 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : αα → Prop} (h :
rintro H _ b hb rfl
exact H b hb _ _
@[grind] theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α Prop} {f : a, p a β}
theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α Prop} {f : a, p a β}
(h : x l, p x) {S : β β Prop}
(hS : x (hx : p x) y (hy : p y), R x y S (f x hx) (f y hy)) :
Pairwise S (l.pmap f h) := by
@@ -268,15 +268,15 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : αα → Prop} (h :
/-! ### Nodup -/
@[simp, grind]
@[simp]
theorem nodup_nil : @Nodup α [] :=
Pairwise.nil
@[simp, grind =]
@[simp]
theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) a l Nodup l := by
simp only [Nodup, pairwise_cons, forall_mem_ne]
@[grind ] theorem Nodup.sublist : l₁ <+ l₂ Nodup l₂ Nodup l₁ :=
theorem Nodup.sublist : l₁ <+ l₂ Nodup l₂ Nodup l₁ :=
Pairwise.sublist
theorem Sublist.nodup : l₁ <+ l₂ Nodup l₂ Nodup l₁ :=
@@ -303,7 +303,7 @@ theorem getElem?_inj {xs : List α}
rw [mem_iff_getElem?]
exact _, h₂; exact _ , h₂.symm
@[simp, grind =] theorem nodup_replicate {n : Nat} {a : α} :
@[simp] theorem nodup_replicate {n : Nat} {a : α} :
(replicate n a).Nodup n 1 := by simp [Nodup]
end List

View File

@@ -31,11 +31,6 @@ theorem take_cons {l : List α} (h : 0 < i) : (a :: l).take i = a :: l.take (i -
| zero => exact absurd h (Nat.lt_irrefl _)
| succ i => rfl
theorem drop_cons {l : List α} (h : 0 < i) : (a :: l).drop i = l.drop (i - 1) := by
cases i with
| zero => exact absurd h (Nat.lt_irrefl _)
| succ i => rfl
@[simp]
theorem drop_one : {l : List α}, l.drop 1 = l.tail
| [] | _ :: _ => rfl

View File

@@ -256,16 +256,16 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
@[simp, grind =] theorem findSome?_toArray (f : α Option β) (l : List α) :
l.toArray.findSome? f = l.findSome? f := by
rw [Array.findSome?, findSomeM?_toArray, findSomeM?_pure, Id.run_pure]
rw [Array.findSome?, findSomeM?_id, findSomeM?_toArray, Id.run]
@[simp, grind =] theorem find?_toArray (f : α Bool) (l : List α) :
l.toArray.find? f = l.find? f := by
rw [Array.find?]
simp only [forIn_toArray]
simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
induction l with
| nil => simp
| cons a l ih =>
simp only [forIn_cons, find?]
simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
by_cases f a <;> simp_all
private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) :

View File

@@ -150,7 +150,7 @@ theorem add_one (n : Nat) : n + 1 = succ n :=
@[simp] theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
rfl
theorem add_one_ne_zero (n : Nat) : n + 1 0 := nofun
@[simp] theorem add_one_ne_zero (n : Nat) : n + 1 0 := nofun
theorem zero_ne_add_one (n : Nat) : 0 n + 1 := by simp
protected theorem add_comm : (n m : Nat), n + m = m + n
@@ -731,12 +731,13 @@ theorem exists_eq_add_one_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n =
theorem ctor_eq_zero : Nat.zero = 0 :=
rfl
protected theorem one_ne_zero : 1 (0 : Nat) := by simp
@[simp] protected theorem one_ne_zero : 1 (0 : Nat) :=
fun h => Nat.noConfusion h
@[simp] protected theorem zero_ne_one : 0 (1 : Nat) :=
fun h => Nat.noConfusion h
theorem succ_ne_zero (n : Nat) : succ n 0 := by simp
@[simp] theorem succ_ne_zero (n : Nat) : succ n 0 := by simp
instance instNeZeroSucc {n : Nat} : NeZero (n + 1) := succ_ne_zero n

View File

@@ -415,7 +415,7 @@ theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
| inl h => rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
| inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]
protected theorem min_self (a : Nat) : min a a = a := by simp
@[simp] protected theorem min_self (a : Nat) : min a a = a := Nat.min_eq_left (Nat.le_refl _)
instance : Std.IdempotentOp (α := Nat) min := Nat.min_self
@[simp] protected theorem min_assoc : (a b c : Nat), min (min a b) c = min a (min b c)
@@ -431,14 +431,16 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
@[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
rw [Nat.min_comm m n, Nat.min_assoc, Nat.min_self]
theorem min_add_left_self {a b : Nat} : min a (b + a) = a := by
@[simp] theorem min_add_left_self {a b : Nat} : min a (b + a) = a := by
rw [Nat.min_def]
simp
theorem min_add_right_self {a b : Nat} : min a (a + b) = a := by
simp
theorem add_left_min_self {a b : Nat} : min (b + a) a = a := by
simp
theorem add_right_min_self {a b : Nat} : min (a + b) a = a := by
@[simp] theorem min_add_right_self {a b : Nat} : min a (a + b) = a := by
rw [Nat.min_def]
simp
@[simp] theorem add_left_min_self {a b : Nat} : min (b + a) a = a := by
rw [Nat.min_comm, min_add_left_self]
@[simp] theorem add_right_min_self {a b : Nat} : min (a + b) a = a := by
rw [Nat.min_comm, min_add_right_self]
protected theorem sub_sub_eq_min : (a b : Nat), a - (a - b) = min a b
| 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
@@ -460,7 +462,7 @@ protected theorem succ_max_succ (x y) : max (succ x) (succ y) = succ (max x y) :
| inl h => rw [Nat.max_eq_right h, Nat.max_eq_right (Nat.succ_le_succ h)]
| inr h => rw [Nat.max_eq_left h, Nat.max_eq_left (Nat.succ_le_succ h)]
protected theorem max_self (a : Nat) : max a a = a := by simp
@[simp] protected theorem max_self (a : Nat) : max a a = a := Nat.max_eq_right (Nat.le_refl _)
instance : Std.IdempotentOp (α := Nat) max := Nat.max_self
instance : Std.LawfulIdentity (α := Nat) max 0 where
@@ -474,14 +476,16 @@ instance : Std.LawfulIdentity (α := Nat) max 0 where
| _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
instance : Std.Associative (α := Nat) max := Nat.max_assoc
theorem max_add_left_self {a b : Nat} : max a (b + a) = b + a := by
@[simp] theorem max_add_left_self {a b : Nat} : max a (b + a) = b + a := by
rw [Nat.max_def]
simp
theorem max_add_right_self {a b : Nat} : max a (a + b) = a + b := by
simp
theorem add_left_max_self {a b : Nat} : max (b + a) a = b + a := by
simp
theorem add_right_max_self {a b : Nat} : max (a + b) a = a + b := by
@[simp] theorem max_add_right_self {a b : Nat} : max a (a + b) = a + b := by
rw [Nat.max_def]
simp
@[simp] theorem add_left_max_self {a b : Nat} : max (b + a) a = b + a := by
rw [Nat.max_comm, max_add_left_self]
@[simp] theorem add_right_max_self {a b : Nat} : max (a + b) a = a + b := by
rw [Nat.max_comm, max_add_right_self]
protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
match Nat.le_total a b with
@@ -810,8 +814,10 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
simp [mul_succ, Nat.add_comm] at h₁; simp [h₁]
rw [mul_succ, Nat.sub_sub, mod_eq_sub_mod h₄, sub_mul_mod h₂]
theorem mod_mod (a n : Nat) : (a % n) % n = a % n := by
simp
@[simp] theorem mod_mod (a n : Nat) : (a % n) % n = a % n :=
match eq_zero_or_pos n with
| .inl n0 => by simp [n0, mod_zero]
| .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)
theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
rw (occs := [1]) [ mod_add_div a n]

View File

@@ -39,11 +39,11 @@ namespace Option
o.toArray.foldr f a = o.elim a (fun b => f b a) := by
cases o <;> simp
@[simp, grind =]
@[simp]
theorem toList_toArray {o : Option α} : o.toArray.toList = o.toList := by
cases o <;> simp
@[simp, grind =]
@[simp]
theorem toArray_toList {o : Option α} : o.toList.toArray = o.toArray := by
cases o <;> simp
@@ -69,8 +69,7 @@ theorem toArray_min [Min α] {o o' : Option α} :
theorem size_toArray_le {o : Option α} : o.toArray.size 1 := by
cases o <;> simp
@[grind =]
theorem size_toArray {o : Option α} :
theorem size_toArray_eq_ite {o : Option α} :
o.toArray.size = if o.isSome then 1 else 0 := by
cases o <;> simp
@@ -82,9 +81,10 @@ theorem toArray_eq_empty_iff {o : Option α} : o.toArray = #[] ↔ o = none := b
theorem toArray_eq_singleton_iff {o : Option α} : o.toArray = #[a] o = some a := by
cases o <;> simp
@[simp]
theorem size_toArray_eq_zero_iff {o : Option α} :
o.toArray.size = 0 o = none := by
simp
cases o <;> simp
@[simp]
theorem size_toArray_eq_one_iff {o : Option α} :

View File

@@ -51,12 +51,12 @@ terminates.
-/
@[inline] def attach (xs : Option α) : Option {x // xs = some x} := xs.attachWith _ fun _ => id
@[simp, grind =] theorem attach_none : (none : Option α).attach = none := rfl
@[simp, grind =] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
@[simp] theorem attach_none : (none : Option α).attach = none := rfl
@[simp] theorem attachWith_none : (none : Option α).attachWith P H = none := rfl
@[simp, grind =] theorem attach_some {x : α} :
@[simp] theorem attach_some {x : α} :
(some x).attach = some x, rfl := rfl
@[simp, grind =] theorem attachWith_some {x : α} {P : α Prop} (h : (b : α), some x = some b P b) :
@[simp] theorem attachWith_some {x : α} {P : α Prop} (h : (b : α), some x = some b P b) :
(some x).attachWith P h = some x, by simpa using h := rfl
theorem attach_congr {o₁ o₂ : Option α} (h : o₁ = o₂) :
@@ -76,7 +76,7 @@ theorem attach_map_val (o : Option α) (f : α → β) :
@[deprecated attach_map_val (since := "2025-02-17")]
abbrev attach_map_coe := @attach_map_val
@[simp, grind =]theorem attach_map_subtype_val (o : Option α) :
theorem attach_map_subtype_val (o : Option α) :
o.attach.map Subtype.val = o :=
(attach_map_val _ _).trans (congrFun Option.map_id _)
@@ -87,7 +87,7 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H
@[deprecated attachWith_map_val (since := "2025-02-17")]
abbrev attachWith_map_coe := @attachWith_map_val
@[simp, grind =] theorem attachWith_map_subtype_val {p : α Prop} (o : Option α) (H : a, o = some a p a) :
theorem attachWith_map_subtype_val {p : α Prop} (o : Option α) (H : a, o = some a p a) :
(o.attachWith p H).map Subtype.val = o :=
(attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
@@ -98,17 +98,17 @@ theorem attach_eq_some : ∀ (o : Option α) (x : {x // o = some x}), o.attach =
theorem mem_attach : (o : Option α) (x : {x // o = some x}), x o.attach :=
attach_eq_some
@[simp, grind =] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
@[simp] theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone := by
cases o <;> simp
@[simp, grind =] theorem isNone_attachWith {p : α Prop} (o : Option α) (H : a, o = some a p a) :
@[simp] theorem isNone_attachWith {p : α Prop} (o : Option α) (H : a, o = some a p a) :
(o.attachWith p H).isNone = o.isNone := by
cases o <;> simp
@[simp, grind =] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
@[simp] theorem isSome_attach (o : Option α) : o.attach.isSome = o.isSome := by
cases o <;> simp
@[simp, grind =] theorem isSome_attachWith {p : α Prop} (o : Option α) (H : a, o = some a p a) :
@[simp] theorem isSome_attachWith {p : α Prop} (o : Option α) (H : a, o = some a p a) :
(o.attachWith p H).isSome = o.isSome := by
cases o <;> simp
@@ -127,28 +127,25 @@ theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach
o.attachWith p H = some x o = some x.val := by
cases o <;> cases x <;> simp
@[simp, grind =] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
@[simp] theorem get_attach {o : Option α} (h : o.attach.isSome = true) :
o.attach.get h = o.get (by simpa using h), by simp :=
Subsingleton.elim _ _
@[simp, grind =] theorem getD_attach {o : Option α} {fallback} :
@[simp] theorem getD_attach {o : Option α} {fallback} :
o.attach.getD fallback = fallback :=
Subsingleton.elim _ _
@[simp, grind =] theorem get!_attach {o : Option α} [Inhabited { x // o = some x }] :
@[simp] theorem get!_attach {o : Option α} [Inhabited { x // o = some x }] :
o.attach.get! = default :=
Subsingleton.elim _ _
@[simp, grind =] theorem get_attachWith {p : α Prop} {o : Option α} (H : a, o = some a p a) (h : (o.attachWith p H).isSome) :
@[simp] theorem get_attachWith {p : α Prop} {o : Option α} (H : a, o = some a p a) (h : (o.attachWith p H).isSome) :
(o.attachWith p H).get h = o.get (by simpa using h), H _ (by simp) := by
cases o <;> simp
@[simp, grind =] theorem getD_attachWith {p : α Prop} {o : Option α} {h} {fallback} :
@[simp] theorem getD_attachWith {p : α Prop} {o : Option α} {h} {fallback} :
(o.attachWith p h).getD fallback =
o.getD fallback.val, by
cases o
· exact fallback.property
· exact h _ (by simp) := by
o.getD fallback.1, by cases o <;> (try exact fallback.2) <;> exact h _ (by simp) := by
cases o <;> simp
theorem toList_attach (o : Option α) :
@@ -171,23 +168,23 @@ theorem toArray_attachWith {p : α → Prop} {o : Option α} {h} :
o.toList.attach = (o.attach.map fun a, h => a, by simpa using h).toList := by
cases o <;> simp [toList]
@[grind =] theorem attach_map {o : Option α} (f : α β) :
theorem attach_map {o : Option α} (f : α β) :
(o.map f).attach = o.attach.map (fun x, h => f x, map_eq_some_iff.2 _, h, rfl) := by
cases o <;> simp
@[grind =] theorem attachWith_map {o : Option α} (f : α β) {P : β Prop} {H : (b : β), o.map f = some b P b} :
theorem attachWith_map {o : Option α} (f : α β) {P : β Prop} {H : (b : β), o.map f = some b P b} :
(o.map f).attachWith P H = (o.attachWith (P f) (fun _ h => H _ (map_eq_some_iff.2 _, h, rfl))).map
fun x, h => f x, h := by
cases o <;> simp
@[grind =] theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } β) :
theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } β) :
o.attach.map f = o.pmap (fun a (h : o = some a) => f a, h) (fun _ h => h) := by
cases o <;> simp
@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
abbrev map_attach := @map_attach_eq_pmap
@[simp, grind =] theorem map_attachWith {l : Option α} {P : α Prop} {H : (a : α), l = some a P a}
@[simp] theorem map_attachWith {l : Option α} {P : α Prop} {H : (a : α), l = some a P a}
(f : { x // P x } β) :
(l.attachWith P H).map f = l.attach.map fun x, h => f x, H _ h := by
cases l <;> simp_all
@@ -203,12 +200,12 @@ theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, o
o.attach.map (fun x => x.1, f x.1 x.2) = o.attachWith p f := by
cases o <;> simp_all [Function.comp_def]
@[grind =] theorem attach_bind {o : Option α} {f : α Option β} :
theorem attach_bind {o : Option α} {f : α Option β} :
(o.bind f).attach =
o.attach.bind fun x, h => (f x).attach.map fun y, h' => y, bind_eq_some_iff.2 _, h, h' := by
cases o <;> simp
@[grind =] theorem bind_attach {o : Option α} {f : {x // o = some x} Option β} :
theorem bind_attach {o : Option α} {f : {x // o = some x} Option β} :
o.attach.bind f = o.pbind fun a h => f a, h := by
cases o <;> simp
@@ -216,7 +213,7 @@ theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → o = some a → Op
o.pbind f = o.attach.bind fun x, h => f x h := by
cases o <;> simp
@[grind =] theorem attach_filter {o : Option α} {p : α Bool} :
theorem attach_filter {o : Option α} {p : α Bool} :
(o.filter p).attach =
o.attach.bind fun x, h => if h' : p x then some x, by simp_all else none := by
cases o with
@@ -232,12 +229,12 @@ theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → o = some a → Op
· rintro h, rfl
simp [h]
@[grind =] theorem filter_attachWith {P : α Prop} {o : Option α} {h : x, o = some x P x} {q : α Bool} :
theorem filter_attachWith {P : α Prop} {o : Option α} {h : x, o = some x P x} {q : α Bool} :
(o.attachWith P h).filter q =
(o.filter q).attachWith P (fun _ h' => h _ (eq_some_of_filter_eq_some h')) := by
cases o <;> simp [filter_some] <;> split <;> simp
@[grind =] theorem filter_attach {o : Option α} {p : {x // o = some x} Bool} :
theorem filter_attach {o : Option α} {p : {x // o = some x} Bool} :
o.attach.filter p = o.pbind fun a h => if p a, h then some a, h else none := by
cases o <;> simp [filter_some]
@@ -281,7 +278,7 @@ theorem toArray_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a →
(o.pmap f h).toArray = o.attach.toArray.map (fun x => f x.1 (h _ x.2)) := by
cases o <;> simp
@[grind =] theorem attach_pfilter {o : Option α} {p : (a : α) o = some a Bool} :
theorem attach_pfilter {o : Option α} {p : (a : α) o = some a Bool} :
(o.pfilter p).attach =
o.attach.pbind fun x h => if h' : p x (by simp_all) then
some x.1, by simpa [pfilter_eq_some_iff] using _, h' else none := by

View File

@@ -14,7 +14,7 @@ import Init.Ext
namespace Option
@[grind =] theorem default_eq_none : (default : Option α) = none := rfl
theorem default_eq_none : (default : Option α) = none := rfl
@[deprecated mem_def (since := "2025-04-07")]
theorem mem_iff {a : α} {b : Option α} : a b b = some a := .rfl
@@ -254,11 +254,11 @@ theorem isSome_apply_of_isSome_bind {α β : Type _} {x : Option α} {f : α
(isSome_apply_of_isSome_bind h) := by
cases x <;> trivial
@[grind =] theorem any_bind {p : β Bool} {f : α Option β} {o : Option α} :
theorem any_bind {p : β Bool} {f : α Option β} {o : Option α} :
(o.bind f).any p = o.any (Option.any p f) := by
cases o <;> simp
@[grind =] theorem all_bind {p : β Bool} {f : α Option β} {o : Option α} :
theorem all_bind {p : β Bool} {f : α Option β} {o : Option α} :
(o.bind f).all p = o.all (Option.all p f) := by
cases o <;> simp
@@ -431,7 +431,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
x.filter p = x.bind (Option.guard p) :=
(bind_guard x p).symm
@[simp, grind =] theorem any_filter : (o : Option α)
@[simp] theorem any_filter : (o : Option α)
(Option.filter p o).any q = Option.any (fun a => p a && q a) o
| none => rfl
| some a =>
@@ -439,7 +439,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
| false => by simp [filter_some_neg h, h]
| true => by simp [filter_some_pos h, h]
@[simp, grind =] theorem all_filter : (o : Option α)
@[simp] theorem all_filter : (o : Option α)
(Option.filter p o).all q = Option.all (fun a => !p a || q a) o
| none => rfl
| some a =>
@@ -447,7 +447,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
| false => by simp [filter_some_neg h, h]
| true => by simp [filter_some_pos h, h]
@[simp, grind =] theorem isNone_filter :
@[simp] theorem isNone_filter :
Option.isNone (Option.filter p o) = Option.all (fun a => !p a) o :=
match o with
| none => rfl
@@ -468,7 +468,7 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
Option.filter q (Option.filter p o) = Option.filter (fun x => p x && q x) o := by
cases o <;> repeat (simp_all [filter_some]; try split)
@[grind =] theorem filter_bind {f : α Option β} :
theorem filter_bind {f : α Option β} :
(Option.bind x f).filter p = (x.filter (fun a => (f a).any p)).bind f := by
cases x with
| none => simp
@@ -483,16 +483,16 @@ theorem filter_eq_bind (x : Option α) (p : α → Bool) :
theorem eq_some_of_filter_eq_some {o : Option α} {a : α} (h : o.filter p = some a) : o = some a :=
filter_eq_some_iff.1 h |>.1
@[grind =] theorem filter_map {f : α β} {p : β Bool} :
theorem filter_map {f : α β} {p : β Bool} :
(Option.map f x).filter p = (x.filter (p f)).map f := by
cases x <;> simp [filter_some]
@[simp] theorem all_guard (a : α) :
@[simp, grind] theorem all_guard (a : α) :
Option.all q (guard p a) = (!p a || q a) := by
simp only [guard]
split <;> simp_all
@[simp] theorem any_guard (a : α) : Option.any q (guard p a) = (p a && q a) := by
@[simp, grind] theorem any_guard (a : α) : Option.any q (guard p a) = (p a && q a) := by
simp only [guard]
split <;> simp_all
@@ -563,21 +563,21 @@ theorem bind_map_comm {α β} {x : Option (Option α)} {f : α → β} :
theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a x.join) : some a x :=
h.symm join_eq_some_iff.1 h
@[grind _=_] theorem any_join {p : α Bool} {x : Option (Option α)} :
theorem any_join {p : α Bool} {x : Option (Option α)} :
x.join.any p = x.any (Option.any p) := by
cases x <;> simp
@[grind _=_] theorem all_join {p : α Bool} {x : Option (Option α)} :
theorem all_join {p : α Bool} {x : Option (Option α)} :
x.join.all p = x.all (Option.all p) := by
cases x <;> simp
@[grind =] theorem isNone_join {x : Option (Option α)} : x.join.isNone = x.all Option.isNone := by
theorem isNone_join {x : Option (Option α)} : x.join.isNone = x.all Option.isNone := by
cases x <;> simp
@[grind =]theorem isSome_join {x : Option (Option α)} : x.join.isSome = x.any Option.isSome := by
theorem isSome_join {x : Option (Option α)} : x.join.isSome = x.any Option.isSome := by
cases x <;> simp
@[grind =] theorem get_join {x : Option (Option α)} {h} : x.join.get h =
theorem get_join {x : Option (Option α)} {h} : x.join.get h =
(x.get (Option.isSome_of_any (Option.isSome_join h))).get (get_of_any_eq_true _ _ (Option.isSome_join h)) := by
cases x with
| none => simp at h
@@ -588,11 +588,11 @@ theorem join_eq_get {x : Option (Option α)} {h} : x.join = x.get h := by
| none => simp at h
| some _ => simp
@[grind =] theorem getD_join {x : Option (Option α)} {default : α} :
theorem getD_join {x : Option (Option α)} {default : α} :
x.join.getD default = (x.getD (some default)).getD default := by
cases x <;> simp
@[grind =] theorem get!_join [Inhabited α] {x : Option (Option α)} :
theorem get!_join [Inhabited α] {x : Option (Option α)} :
x.join.get! = x.get!.get! := by
cases x <;> simp [default_eq_none]
@@ -602,13 +602,13 @@ theorem join_eq_get {x : Option (Option α)} {h} : x.join = x.get h := by
@[deprecated guard_eq_some_iff (since := "2025-04-10")]
abbrev guard_eq_some := @guard_eq_some_iff
@[simp, grind =] theorem isSome_guard : (Option.guard p a).isSome = p a :=
@[simp] theorem isSome_guard : (Option.guard p a).isSome = p a :=
if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]
@[deprecated isSome_guard (since := "2025-03-18")]
abbrev guard_isSome := @isSome_guard
@[simp, grind =] theorem isNone_guard : (Option.guard p a).isNone = !p a := by
@[simp] theorem isNone_guard : (Option.guard p a).isNone = !p a := by
rw [ not_isSome, isSome_guard]
@[simp] theorem guard_eq_none_iff : Option.guard p a = none p a = false :=
@@ -643,7 +643,7 @@ theorem get_none (a : α) {h} : none.get h = a := by
theorem get_none_eq_iff_true {h} : (none : Option α).get h = a True := by
simp at h
@[simp, grind =] theorem get_guard : (guard p a).get h = a := by
theorem get_guard : (guard p a).get h = a := by
simp only [guard]
split <;> simp
@@ -672,7 +672,7 @@ theorem map_guard {p : α → Bool} {f : α → β} {x : α} :
(Option.guard p x).map f = if p x then some (f x) else none := by
simp [guard_eq_ite]
@[grind =] theorem join_filter {p : Option α Bool} : {o : Option (Option α)}
theorem join_filter {p : Option α Bool} : {o : Option (Option α)}
(o.filter p).join = o.join.filter (fun a => p (some a))
| none => by simp
| some none => by
@@ -682,7 +682,7 @@ theorem map_guard {p : α → Bool} {f : α → β} {x : α} :
simp only [join_some, filter_some]
split <;> simp
@[grind =] theorem filter_join {p : α Bool} : {o : Option (Option α)}
theorem filter_join {p : α Bool} : {o : Option (Option α)}
o.join.filter p = (o.filter (Option.any p)).join
| none => by simp
| some none => by
@@ -754,22 +754,22 @@ theorem merge_eq_some_iff {o o' : Option α} {f : ααα} {a : α} :
theorem merge_eq_none_iff {o o' : Option α} : o.merge f o' = none o = none o' = none := by
cases o <;> cases o' <;> simp
@[simp, grind =]
@[simp]
theorem any_merge {p : α Bool} {f : α α α} (hpf : a b, p (f a b) = (p a || p b))
{o o' : Option α} : (o.merge f o').any p = (o.any p || o'.any p) := by
cases o <;> cases o' <;> simp [*]
@[simp, grind =]
@[simp]
theorem all_merge {p : α Bool} {f : α α α} (hpf : a b, p (f a b) = (p a && p b))
{o o' : Option α} : (o.merge f o').all p = (o.all p && o'.all p) := by
cases o <;> cases o' <;> simp [*]
@[simp, grind =]
@[simp]
theorem isSome_merge {o o' : Option α} {f : α α α} :
(o.merge f o').isSome = (o.isSome || o'.isSome) := by
simp [ any_true]
@[simp, grind =]
@[simp]
theorem isNone_merge {o o' : Option α} {f : α α α} :
(o.merge f o').isNone = (o.isNone && o'.isNone) := by
simp [ all_false]
@@ -783,7 +783,7 @@ theorem get_merge {o o' : Option α} {f : ααα} {i : α} [Std.Lawful
@[simp, grind] theorem elim_some (x : β) (f : α β) (a : α) : (some a).elim x f = f a := rfl
@[grind =] theorem elim_filter {o : Option α} {b : β} :
theorem elim_filter {o : Option α} {b : β} :
Option.elim (Option.filter p o) b f = Option.elim o b (fun a => if p a then f a else b) :=
match o with
| none => rfl
@@ -792,7 +792,7 @@ theorem get_merge {o o' : Option α} {f : ααα} {i : α} [Std.Lawful
| false => by simp [filter_some_neg h, h]
| true => by simp [filter_some_pos, h]
@[grind =] theorem elim_join {o : Option (Option α)} {b : β} {f : α β} :
theorem elim_join {o : Option (Option α)} {b : β} {f : α β} :
o.join.elim b f = o.elim b (·.elim b f) := by
cases o <;> simp
@@ -830,16 +830,9 @@ theorem choice_eq_default [Subsingleton α] [Inhabited α] : choice α = some de
theorem choice_eq_none_iff_not_nonempty : choice α = none ¬Nonempty α := by
simp [choice]
theorem isNone_choice_iff_not_nonempty : (choice α).isNone ¬Nonempty α := by
rw [isNone_iff_eq_none, choice_eq_none_iff_not_nonempty]
grind_pattern isNone_choice_iff_not_nonempty => (choice α).isNone
theorem isSome_choice_iff_nonempty : (choice α).isSome Nonempty α :=
fun h => (choice α).get h, fun h => by simp only [choice, dif_pos h, isSome_some]
grind_pattern isSome_choice_iff_nonempty => (choice α).isSome
@[simp]
theorem isSome_choice [Nonempty α] : (choice α).isSome :=
isSome_choice_iff_nonempty.2 inferInstance
@@ -847,16 +840,19 @@ theorem isSome_choice [Nonempty α] : (choice α).isSome :=
@[deprecated isSome_choice_iff_nonempty (since := "2025-03-18")]
abbrev choice_isSome_iff_nonempty := @isSome_choice_iff_nonempty
theorem isNone_choice_iff_not_nonempty : (choice α).isNone ¬Nonempty α := by
rw [isNone_iff_eq_none, choice_eq_none_iff_not_nonempty]
@[simp]
theorem isNone_choice_eq_false [Nonempty α] : (choice α).isNone = false := by
simp [ not_isSome]
@[simp, grind =]
@[simp]
theorem getD_choice {a} :
(choice α).getD a = (choice α).get (isSome_choice_iff_nonempty.2 a) := by
rw [get_eq_getD]
@[simp, grind =]
@[simp]
theorem get!_choice [Inhabited α] : (choice α).get! = (choice α).get isSome_choice := by
rw [get_eq_get!]
@@ -937,16 +933,16 @@ theorem or_of_isNone {o o' : Option α} (h : o.isNone) : o.or o' = o' := by
match o, h with
| none, _ => simp
@[simp, grind =]
@[simp, grind]
theorem getD_or {o o' : Option α} {fallback : α} :
(o.or o').getD fallback = o.getD (o'.getD fallback) := by
cases o <;> simp
@[simp, grind =]
@[simp]
theorem get!_or {o o' : Option α} [Inhabited α] : (o.or o').get! = o.getD o'.get! := by
cases o <;> simp
@[simp, grind =] theorem filter_or_filter {o o' : Option α} {f : α Bool} :
@[simp] theorem filter_or_filter {o o' : Option α} {f : α Bool} :
(o.or (o'.filter f)).filter f = (o.or o').filter f := by
cases o <;> cases o' <;> simp
@@ -1030,16 +1026,16 @@ variable [BEq α]
@[simp] theorem beq_none {o : Option α} : (o == none) = o.isNone := by cases o <;> simp
@[simp, grind =]
theorem filter_beq_self [ReflBEq α] {p : α Bool} {o : Option α} : (o.filter p == o) = o.all p := by
@[simp]
theorem filter_beq_self [ReflBEq α] {p : α Bool} {o : Option α} : (o.filter p == o) = (o.all p) := by
cases o with
| none => simp
| some _ =>
simp only [filter_some]
split <;> simp [*]
@[simp, grind =]
theorem self_beq_filter [ReflBEq α] {p : α Bool} {o : Option α} : (o == o.filter p) = o.all p := by
@[simp]
theorem self_beq_filter [ReflBEq α] {p : α Bool} {o : Option α} : (o == o.filter p) = (o.all p) := by
cases o with
| none => simp
| some _ =>
@@ -1208,7 +1204,7 @@ theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → o = some a → Optio
o.pbind f = some b a h, f a h = some b := by
cases o <;> simp
@[grind =] theorem pbind_join {o : Option (Option α)} {f : (a : α) o.join = some a Option β} :
theorem pbind_join {o : Option (Option α)} {f : (a : α) o.join = some a Option β} :
o.join.pbind f = o.pbind (fun o' ho' => o'.pbind (fun a ha => f a (by simp_all))) := by
cases o <;> simp <;> congr
@@ -1222,7 +1218,7 @@ theorem isSome_get_of_isSome_pbind {o : Option α} {f : (a : α) → o = some a
| none => simp at h
| some a => simp [ h]
@[simp, grind =]
@[simp]
theorem get_pbind {o : Option α} {f : (a : α) o = some a Option β} {h} :
(o.pbind f).get h = (f (o.get (isSome_of_isSome_pbind h)) (by simp)).get (isSome_get_of_isSome_pbind h) := by
cases o <;> simp
@@ -1260,7 +1256,7 @@ theorem get_pbind {o : Option α} {f : (a : α) → o = some a → Option β} {h
· rintro h, rfl
rfl
@[simp]
@[simp, grind]
theorem pmap_eq_map (p : α Prop) (f : α β) (o : Option α) (H) :
@pmap _ _ p (fun a _ => f a) o H = Option.map f o := by
cases o <;> simp
@@ -1309,7 +1305,7 @@ theorem pmap_guard {q : α → Bool} {p : α → Prop} (f : (x : α) → p x →
simp only [guard_eq_ite]
split <;> simp_all
@[simp, grind =]
@[simp]
theorem get_pmap {p : α Bool} {f : (x : α) p x β} {o : Option α}
{h : a, o = some a p a} {h'} :
(o.pmap f h).get h' = f (o.get (by simpa using h')) (h _ (by simp)) := by
@@ -1320,7 +1316,7 @@ theorem get_pmap {p : α → Bool} {f : (x : α) → p x → β} {o : Option α}
@[simp, grind] theorem pelim_none : pelim none b f = b := rfl
@[simp, grind] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
@[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
@[simp, grind] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
cases o <;> simp
@[simp, grind] theorem elim_pmap {p : α Prop} (f : (a : α) p a β) (o : Option α)
@@ -1333,7 +1329,7 @@ theorem pelim_congr_left {o o' : Option α } {b : β} {f : (a : α) → (a ∈ o
pelim o b f = pelim o' b (fun a ha => f a (h ha)) := by
cases h; rfl
@[grind =] theorem pelim_filter {o : Option α} {b : β} {f : (a : α) a o.filter p β} :
theorem pelim_filter {o : Option α} {b : β} {f : (a : α) a o.filter p β} :
Option.pelim (Option.filter p o) b f =
Option.pelim o b (fun a h => if hp : p a then f a (Option.mem_filter_iff.2 h, hp) else b) :=
match o with
@@ -1343,7 +1339,7 @@ theorem pelim_congr_left {o o' : Option α } {b : β} {f : (a : α) → (a ∈ o
| false => by simp [pelim_congr_left (filter_some_neg h), h]
| true => by simp [pelim_congr_left (filter_some_pos h), h]
@[grind =] theorem pelim_join {o : Option (Option α)} {b : β} {f : (a : α) a o.join β} :
theorem pelim_join {o : Option (Option α)} {b : β} {f : (a : α) a o.join β} :
o.join.pelim b f = o.pelim b (fun o' ho' => o'.pelim b (fun a ha => f a (by simp_all))) := by
cases o <;> simp <;> congr
@@ -1421,7 +1417,7 @@ theorem eq_some_of_pfilter_eq_some {o : Option α} {p : (a : α) → o = some a
{a : α} (h : o.pfilter p = some a) : o = some a :=
pfilter_eq_some_iff.1 h |>.1
@[grind =] theorem filter_pbind {f : (a : α) o = some a Option β} :
theorem filter_pbind {f : (a : α) o = some a Option β} :
(Option.pbind o f).filter p =
(o.pfilter (fun a h => (f a h).any p)).pbind (fun a h => f a (eq_some_of_pfilter_eq_some h)) := by
cases o with
@@ -1433,7 +1429,7 @@ theorem eq_some_of_pfilter_eq_some {o : Option α} {p : (a : α) → o = some a
· simp only [h, filter_some, any_some]
split <;> simp [h]
@[simp] theorem pfilter_eq_filter {α : Type _} {o : Option α} {p : α Bool} :
@[simp, grind] theorem pfilter_eq_filter {α : Type _} {o : Option α} {p : α Bool} :
o.pfilter (fun a _ => p a) = o.filter p := by
cases o with
| none => rfl
@@ -1472,7 +1468,7 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
· rfl
· simp only [Option.pfilter, Bool.cond_eq_ite, Option.pbind_some]
@[grind =] theorem filter_pmap {p : α Prop} {f : (a : α) p a β} {h : (a : α), o = some a p a}
theorem filter_pmap {p : α Prop} {f : (a : α) p a β} {h : (a : α), o = some a p a}
{q : β Bool} : (o.pmap f h).filter q = (o.pfilter (fun a h' => q (f a (h _ h')))).pmap f
(fun _ h' => h _ (eq_some_of_pfilter_eq_some h')) := by
cases o with
@@ -1481,7 +1477,7 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
simp only [pmap_some, filter_some, pfilter_some]
split <;> simp
@[grind =] theorem pfilter_join {o : Option (Option α)} {p : (a : α) o.join = some a Bool} :
theorem pfilter_join {o : Option (Option α)} {p : (a : α) o.join = some a Bool} :
o.join.pfilter p = (o.pfilter (fun o' h => o'.pelim false (fun a ha => p a (by simp_all)))).join := by
cases o with
| none => simp
@@ -1492,11 +1488,11 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
simp only [join_some, pfilter_some, pelim_some]
split <;> simp
@[grind =] theorem join_pfilter {o : Option (Option α)} {p : (o' : Option α) o = some o' Bool} :
theorem join_pfilter {o : Option (Option α)} {p : (o' : Option α) o = some o' Bool} :
(o.pfilter p).join = o.pbind (fun o' ho' => if p o' ho' then o' else none) := by
cases o <;> simp <;> split <;> simp
@[grind =] theorem elim_pfilter {o : Option α} {b : β} {f : α β} {p : (a : α) o = some a Bool} :
theorem elim_pfilter {o : Option α} {b : β} {f : α β} {p : (a : α) o = some a Bool} :
(o.pfilter p).elim b f = o.pelim b (fun a ha => if p a ha then f a else b) := by
cases o with
| none => simp
@@ -1504,7 +1500,7 @@ theorem pfilter_eq_pbind_ite {α : Type _} {o : Option α}
simp only [pfilter_some, pelim_some]
split <;> simp
@[grind =] theorem pelim_pfilter {o : Option α} {b : β} {p : (a : α) o = some a Bool}
theorem pelim_pfilter {o : Option α} {b : β} {p : (a : α) o = some a Bool}
{f : (a : α) o.pfilter p = some a β} :
(o.pfilter p).pelim b f = o.pelim b
(fun a ha => if hp : p a ha then f a (pfilter_eq_some_iff.2 _, hp) else b) := by
@@ -1522,13 +1518,13 @@ theorem pfilter_guard {a : α} {p : α → Bool} {q : (a' : α) → guard p a =
/-! ### LT and LE -/
@[simp, grind] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]
@[grind] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]
@[simp] theorem none_lt [LT α] {a : Option α} : none < a a.isSome := by cases a <;> simp [none_lt_some]
@[simp, grind] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]
@[simp] theorem none_lt [LT α] {a : Option α} : none < a a.isSome := by cases a <;> simp
@[simp, grind] theorem some_lt_some [LT α] {a b : α} : some a < some b a < b := by simp [LT.lt, Option.lt]
@[simp, grind] theorem none_le [LE α] {a : Option α} : none a := by cases a <;> simp [LE.le, Option.le]
@[grind] theorem not_some_le_none [LE α] {a : α} : ¬ some a none := by simp [LE.le, Option.le]
@[simp] theorem le_none [LE α] {a : Option α} : a none a = none := by cases a <;> simp [not_some_le_none]
@[simp, grind] theorem not_some_le_none [LE α] {a : α} : ¬ some a none := by simp [LE.le, Option.le]
@[simp] theorem le_none [LE α] {a : Option α} : a none a = none := by cases a <;> simp
@[simp, grind] theorem some_le_some [LE α] {a b : α} : some a some b a b := by simp [LE.le, Option.le]
@[simp]
@@ -1793,19 +1789,19 @@ theorem min_pfilter_right [Min α] [Std.IdempotentOp (α := α) min] {o : Option
simp only [pfilter_some]
split <;> simp [Std.IdempotentOp.idempotent]
@[simp, grind =]
@[simp]
theorem isSome_max [Max α] {o o' : Option α} : (max o o').isSome = (o.isSome || o'.isSome) := by
cases o <;> cases o' <;> simp
@[simp, grind =]
@[simp]
theorem isNone_max [Max α] {o o' : Option α} : (max o o').isNone = (o.isNone && o'.isNone) := by
cases o <;> cases o' <;> simp
@[simp, grind =]
@[simp]
theorem isSome_min [Min α] {o o' : Option α} : (min o o').isSome = (o.isSome && o'.isSome) := by
cases o <;> cases o' <;> simp
@[simp, grind =]
@[simp]
theorem isNone_min [Min α] {o o' : Option α} : (min o o').isNone = (o.isNone || o'.isNone) := by
cases o <;> cases o' <;> simp
@@ -1817,7 +1813,7 @@ theorem max_join_right [Max α] {o : Option α} {o' : Option (Option α)} :
max o o'.join = (max (some o) o').get (by simp) := by
cases o' <;> simp
@[grind _=_] theorem join_max [Max α] {o o' : Option (Option α)} :
theorem join_max [Max α] {o o' : Option (Option α)} :
(max o o').join = max o.join o'.join := by
cases o <;> cases o' <;> simp
@@ -1829,7 +1825,7 @@ theorem min_join_right [Min α] {o : Option α} {o' : Option (Option α)} :
min o o'.join = (min (some o) o').join := by
cases o' <;> simp
@[grind _=_] theorem join_min [Min α] {o o' : Option (Option α)} :
theorem join_min [Min α] {o o' : Option (Option α)} :
(min o o').join = min o.join o'.join := by
cases o <;> cases o' <;> simp
@@ -1877,12 +1873,12 @@ theorem min_eq_none_iff [Min α] {o o' : Option α} :
min o o' = none o = none o' = none := by
cases o <;> cases o' <;> simp
@[simp, grind =]
@[simp]
theorem any_max [Max α] {o o' : Option α} {p : α Bool} (hp : a b, p (max a b) = (p a || p b)) :
(max o o').any p = (o.any p || o'.any p) := by
cases o <;> cases o' <;> simp [hp]
@[simp, grind =]
@[simp]
theorem all_min [Min α] {o o' : Option α} {p : α Bool} (hp : a b, p (min a b) = (p a || p b)) :
(min o o').all p = (o.all p || o'.all p) := by
cases o <;> cases o' <;> simp [hp]
@@ -1893,7 +1889,7 @@ theorem isSome_left_of_isSome_min [Min α] {o o' : Option α} : (min o o').isSom
theorem isSome_right_of_isSome_min [Min α] {o o' : Option α} : (min o o').isSome o'.isSome := by
cases o' <;> simp
@[simp, grind =]
@[simp]
theorem get_min [Min α] {o o' : Option α} {h} :
(min o o').get h = min (o.get (isSome_left_of_isSome_min h)) (o'.get (isSome_right_of_isSome_min h)) := by
cases o <;> cases o' <;> simp

View File

@@ -73,8 +73,7 @@ theorem toList_min [Min α] {o o' : Option α} :
theorem length_toList_le {o : Option α} : o.toList.length 1 := by
cases o <;> simp
@[grind =]
theorem length_toList {o : Option α} :
theorem length_toList_eq_ite {o : Option α} :
o.toList.length = if o.isSome then 1 else 0 := by
cases o <;> simp
@@ -86,9 +85,10 @@ theorem toList_eq_nil_iff {o : Option α} : o.toList = [] ↔ o = none := by
theorem toList_eq_singleton_iff {o : Option α} : o.toList = [a] o = some a := by
cases o <;> simp
@[simp]
theorem length_toList_eq_zero_iff {o : Option α} :
o.toList.length = 0 o = none := by
simp
cases o <;> simp
@[simp]
theorem length_toList_eq_one_iff {o : Option α} :

View File

@@ -90,18 +90,11 @@ theorem forIn'_eq_pelim [Monad m] [LawfulMonad m]
pure (f := m) (o.pelim b (fun a h => f a h b)) := by
cases o <;> simp
@[simp] theorem idRun_forIn'_yield_eq_pelim
(o : Option α) (f : (a : α) a o β Id β) (b : β) :
(forIn' o b (fun a m b => .yield <$> f a m b)).run =
o.pelim b (fun a h => f a h b |>.run) :=
forIn'_pure_yield_eq_pelim _ _ _
@[deprecated idRun_forIn'_yield_eq_pelim (since := "2025-05-21")]
theorem forIn'_id_yield_eq_pelim
@[simp] theorem forIn'_id_yield_eq_pelim
(o : Option α) (f : (a : α) a o β β) (b : β) :
forIn' (m := Id) o b (fun a m b => .yield (f a m b)) =
o.pelim b (fun a h => f a h b) :=
forIn'_pure_yield_eq_pelim _ _ _
o.pelim b (fun a h => f a h b) := by
cases o <;> simp
@[simp, grind] theorem forIn'_map [Monad m] [LawfulMonad m]
(o : Option α) (g : α β) (f : (b : β) b o.map g γ m (ForInStep γ)) :
@@ -133,18 +126,11 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
pure (f := m) (o.elim b (fun a => f a b)) := by
cases o <;> simp
@[simp] theorem idRun_forIn_yield_eq_elim
(o : Option α) (f : (a : α) β Id β) (b : β) :
(forIn o b (fun a b => .yield <$> f a b)).run =
o.elim b (fun a => f a b |>.run) :=
forIn_pure_yield_eq_elim _ _ _
@[deprecated idRun_forIn_yield_eq_elim (since := "2025-05-21")]
theorem forIn_id_yield_eq_elim
@[simp] theorem forIn_id_yield_eq_elim
(o : Option α) (f : (a : α) β β) (b : β) :
forIn (m := Id) o b (fun a b => .yield (f a b)) =
o.elim b (fun a => f a b) :=
forIn_pure_yield_eq_elim _ _ _
o.elim b (fun a => f a b) := by
cases o <;> simp
@[simp, grind] theorem forIn_map [Monad m] [LawfulMonad m]
(o : Option α) (g : α β) (f : β γ m (ForInStep γ)) :
@@ -156,26 +142,26 @@ theorem forIn_join [Monad m] [LawfulMonad m]
forIn o.join init f = forIn o init (fun o' b => ForInStep.yield <$> forIn o' b f) := by
cases o <;> simp
@[simp, grind =] theorem elimM_pure [Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α m β) :
@[simp] theorem elimM_pure [Monad m] [LawfulMonad m] (x : Option α) (y : m β) (z : α m β) :
Option.elimM (pure x : m (Option α)) y z = x.elim y z := by
simp [Option.elimM]
@[simp, grind =] theorem elimM_bind [Monad m] [LawfulMonad m] (x : m α) (f : α m (Option β))
@[simp] theorem elimM_bind [Monad m] [LawfulMonad m] (x : m α) (f : α m (Option β))
(y : m γ) (z : β m γ) : Option.elimM (x >>= f) y z = (do Option.elimM (f ( x)) y z) := by
simp [Option.elimM]
@[simp, grind =] theorem elimM_map [Monad m] [LawfulMonad m] (x : m α) (f : α Option β)
@[simp] theorem elimM_map [Monad m] [LawfulMonad m] (x : m α) (f : α Option β)
(y : m γ) (z : β m γ) : Option.elimM (f <$> x) y z = (do Option.elim (f ( x)) y z) := by
simp [Option.elimM]
@[simp, grind =] theorem tryCatch_eq_or (o : Option α) (alternative : Unit Option α) :
@[simp] theorem tryCatch_eq_or (o : Option α) (alternative : Unit Option α) :
tryCatch o alternative = o.or (alternative ()) := by cases o <;> rfl
@[simp, grind =] theorem throw_eq_none : throw () = (none : Option α) := rfl
@[simp] theorem throw_eq_none : throw () = (none : Option α) := rfl
@[simp, grind =] theorem filterM_none [Applicative m] (p : α m Bool) :
@[simp, grind] theorem filterM_none [Applicative m] (p : α m Bool) :
none.filterM p = pure none := rfl
@[grind =] theorem filterM_some [Applicative m] (p : α m Bool) (a : α) :
theorem filterM_some [Applicative m] (p : α m Bool) (a : α) :
(some a).filterM p = (fun b => if b then some a else none) <$> p a := rfl
theorem sequence_join [Applicative m] [LawfulApplicative m] {o : Option (Option (m α))} :

View File

@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dany Fabian, Sebastian Ullrich
-/
module
prelude
@@ -20,13 +21,13 @@ The relationship between the compared items may be:
* `Ordering.gt`: greater than
-/
inductive Ordering where
/-- Less than. -/
| lt
/-- Equal. -/
| eq
/-- Greater than. -/
| gt
deriving Inhabited, DecidableEq, Repr
| /-- Less than. -/
lt
| /-- Equal. -/
eq
| /-- Greater than. -/
gt
deriving Inhabited, DecidableEq
namespace Ordering
@@ -38,7 +39,6 @@ Examples:
* `Ordering.eq.swap = Ordering.eq`
* `Ordering.gt.swap = Ordering.lt`
-/
@[inline]
def swap : Ordering Ordering
| .lt => .gt
| .eq => .eq
@@ -96,7 +96,6 @@ Ordering.lt
/--
Checks whether the ordering is `eq`.
-/
@[inline]
def isEq : Ordering Bool
| eq => true
| _ => false
@@ -104,7 +103,6 @@ def isEq : Ordering → Bool
/--
Checks whether the ordering is not `eq`.
-/
@[inline]
def isNe : Ordering Bool
| eq => false
| _ => true
@@ -112,7 +110,6 @@ def isNe : Ordering → Bool
/--
Checks whether the ordering is `lt` or `eq`.
-/
@[inline]
def isLE : Ordering Bool
| gt => false
| _ => true
@@ -120,7 +117,6 @@ def isLE : Ordering → Bool
/--
Checks whether the ordering is `lt`.
-/
@[inline]
def isLT : Ordering Bool
| lt => true
| _ => false
@@ -128,7 +124,6 @@ def isLT : Ordering → Bool
/--
Checks whether the ordering is `gt`.
-/
@[inline]
def isGT : Ordering Bool
| gt => true
| _ => false
@@ -136,158 +131,203 @@ def isGT : Ordering → Bool
/--
Checks whether the ordering is `gt` or `eq`.
-/
@[inline]
def isGE : Ordering Bool
| lt => false
| _ => true
section Lemmas
protected theorem «forall» {p : Ordering Prop} : ( o, p o) p .lt p .eq p .gt := by
constructor
· intro h
exact h _, h _, h _
· rintro h₁, h₂, h₃ (_ | _ | _) <;> assumption
@[simp]
theorem isLT_lt : lt.isLT := rfl
protected theorem «exists» {p : Ordering Prop} : ( o, p o) p .lt p .eq p .gt := by
constructor
· rintro (_ | _ | _), h
· exact .inl h
· exact .inr (.inl h)
· exact .inr (.inr h)
· rintro (h | h | h) <;> exact _, h
@[simp]
theorem isLE_lt : lt.isLE := rfl
instance [DecidablePred p] : Decidable ( o : Ordering, p o) :=
decidable_of_decidable_of_iff Ordering.«forall».symm
@[simp]
theorem isEq_lt : lt.isEq = false := rfl
instance [DecidablePred p] : Decidable ( o : Ordering, p o) :=
decidable_of_decidable_of_iff Ordering.«exists».symm
@[simp]
theorem isNe_lt : lt.isNe = true := rfl
@[simp] theorem isLT_lt : lt.isLT := rfl
@[simp] theorem isLE_lt : lt.isLE := rfl
@[simp] theorem isEq_lt : lt.isEq = false := rfl
@[simp] theorem isNe_lt : lt.isNe = true := rfl
@[simp] theorem isGE_lt : lt.isGE = false := rfl
@[simp] theorem isGT_lt : lt.isGT = false := rfl
@[simp]
theorem isGE_lt : lt.isGE = false := rfl
@[simp] theorem isLT_eq : eq.isLT = false := rfl
@[simp] theorem isLE_eq : eq.isLE := rfl
@[simp] theorem isEq_eq : eq.isEq := rfl
@[simp] theorem isNe_eq : eq.isNe = false := rfl
@[simp] theorem isGE_eq : eq.isGE := rfl
@[simp] theorem isGT_eq : eq.isGT = false := rfl
@[simp]
theorem isGT_lt : lt.isGT = false := rfl
@[simp] theorem isLT_gt : gt.isLT = false := rfl
@[simp] theorem isLE_gt : gt.isLE = false := rfl
@[simp] theorem isEq_gt : gt.isEq = false := rfl
@[simp] theorem isNe_gt : gt.isNe = true := rfl
@[simp] theorem isGE_gt : gt.isGE := rfl
@[simp] theorem isGT_gt : gt.isGT := rfl
@[simp]
theorem isLT_eq : eq.isLT = false := rfl
@[simp] theorem lt_beq_eq : (lt == eq) = false := rfl
@[simp] theorem lt_beq_gt : (lt == gt) = false := rfl
@[simp] theorem eq_beq_lt : (eq == lt) = false := rfl
@[simp] theorem eq_beq_gt : (eq == gt) = false := rfl
@[simp] theorem gt_beq_lt : (gt == lt) = false := rfl
@[simp] theorem gt_beq_eq : (gt == eq) = false := rfl
@[simp]
theorem isLE_eq : eq.isLE := rfl
@[simp] theorem swap_lt : lt.swap = .gt := rfl
@[simp] theorem swap_eq : eq.swap = .eq := rfl
@[simp] theorem swap_gt : gt.swap = .lt := rfl
@[simp]
theorem isEq_eq : eq.isEq := rfl
theorem eq_eq_of_isLE_of_isLE_swap : {o : Ordering}, o.isLE o.swap.isLE o = .eq := by decide
theorem eq_eq_of_isGE_of_isGE_swap : {o : Ordering}, o.isGE o.swap.isGE o = .eq := by decide
theorem eq_eq_of_isLE_of_isGE : {o : Ordering}, o.isLE o.isGE o = .eq := by decide
theorem eq_swap_iff_eq_eq : {o : Ordering}, o = o.swap o = .eq := by decide
theorem eq_eq_of_eq_swap : {o : Ordering}, o = o.swap o = .eq := eq_swap_iff_eq_eq.mp
@[simp]
theorem isNe_eq : eq.isNe = false := rfl
@[simp] theorem isLE_eq_false : {o : Ordering}, o.isLE = false o = .gt := by decide
@[simp] theorem isGE_eq_false : {o : Ordering}, o.isGE = false o = .lt := by decide
@[simp] theorem isNe_eq_false : {o : Ordering}, o.isNe = false o = .eq := by decide
@[simp] theorem isEq_eq_false : {o : Ordering}, o.isEq = false ¬o = .eq := by decide
@[simp]
theorem isGE_eq : eq.isGE := rfl
@[simp] theorem swap_eq_gt : {o : Ordering}, o.swap = .gt o = .lt := by decide
@[simp] theorem swap_eq_lt : {o : Ordering}, o.swap = .lt o = .gt := by decide
@[simp] theorem swap_eq_eq : {o : Ordering}, o.swap = .eq o = .eq := by decide
@[simp]
theorem isGT_eq : eq.isGT = false := rfl
@[simp] theorem isLT_swap : {o : Ordering}, o.swap.isLT = o.isGT := by decide
@[simp] theorem isLE_swap : {o : Ordering}, o.swap.isLE = o.isGE := by decide
@[simp] theorem isEq_swap : {o : Ordering}, o.swap.isEq = o.isEq := by decide
@[simp] theorem isNe_swap : {o : Ordering}, o.swap.isNe = o.isNe := by decide
@[simp] theorem isGE_swap : {o : Ordering}, o.swap.isGE = o.isLE := by decide
@[simp] theorem isGT_swap : {o : Ordering}, o.swap.isGT = o.isLT := by decide
@[simp]
theorem isLT_gt : gt.isLT = false := rfl
theorem isLE_of_eq_lt : {o : Ordering}, o = .lt o.isLE := by decide
theorem isLE_of_eq_eq : {o : Ordering}, o = .eq o.isLE := by decide
theorem isGE_of_eq_gt : {o : Ordering}, o = .gt o.isGE := by decide
theorem isGE_of_eq_eq : {o : Ordering}, o = .eq o.isGE := by decide
@[simp]
theorem isLE_gt : gt.isLE = false := rfl
theorem ne_eq_of_eq_lt : {o : Ordering}, o = .lt o .eq := by decide
theorem ne_eq_of_eq_gt : {o : Ordering}, o = .gt o .eq := by decide
@[simp]
theorem isEq_gt : gt.isEq = false := rfl
@[simp] theorem isLT_iff_eq_lt : {o : Ordering}, o.isLT o = .lt := by decide
@[simp] theorem isGT_iff_eq_gt : {o : Ordering}, o.isGT o = .gt := by decide
@[simp] theorem isEq_iff_eq_eq : {o : Ordering}, o.isEq o = .eq := by decide
@[simp] theorem isNe_iff_ne_eq : {o : Ordering}, o.isNe ¬o = .eq := by decide
@[simp]
theorem isNe_gt : gt.isNe = true := rfl
theorem isLE_iff_ne_gt : {o : Ordering}, o.isLE ¬o = .gt := by decide
theorem isGE_iff_ne_lt : {o : Ordering}, o.isGE ¬o = .lt := by decide
theorem isLE_iff_eq_lt_or_eq_eq : {o : Ordering}, o.isLE o = .lt o = .eq := by decide
theorem isGE_iff_eq_gt_or_eq_eq : {o : Ordering}, o.isGE o = .gt o = .eq := by decide
@[simp]
theorem isGE_gt : gt.isGE := rfl
theorem isLT_eq_beq_lt : {o : Ordering}, o.isLT = (o == .lt) := by decide
theorem isLE_eq_not_beq_gt : {o : Ordering}, o.isLE = (!o == .gt) := by decide
theorem isLE_eq_isLT_or_isEq : {o : Ordering}, o.isLE = (o.isLT || o.isEq) := by decide
theorem isGT_eq_beq_gt : {o : Ordering}, o.isGT = (o == .gt) := by decide
theorem isGE_eq_not_beq_lt : {o : Ordering}, o.isGE = (!o == .lt) := by decide
theorem isGE_eq_isGT_or_isEq : {o : Ordering}, o.isGE = (o.isGT || o.isEq) := by decide
theorem isEq_eq_beq_eq : {o : Ordering}, o.isEq = (o == .eq) := by decide
theorem isNe_eq_not_beq_eq : {o : Ordering}, o.isNe = (!o == .eq) := by decide
theorem isNe_eq_isLT_or_isGT : {o : Ordering}, o.isNe = (o.isLT || o.isGT) := by decide
@[simp]
theorem isGT_gt : gt.isGT := rfl
@[simp] theorem not_isLT_eq_isGE : {o : Ordering}, !o.isLT = o.isGE := by decide
@[simp] theorem not_isLE_eq_isGT : {o : Ordering}, !o.isLE = o.isGT := by decide
@[simp] theorem not_isGT_eq_isLE : {o : Ordering}, !o.isGT = o.isLE := by decide
@[simp] theorem not_isGE_eq_isLT : {o : Ordering}, !o.isGE = o.isLT := by decide
@[simp] theorem not_isNe_eq_isEq : {o : Ordering}, !o.isNe = o.isEq := by decide
theorem not_isEq_eq_isNe : {o : Ordering}, !o.isEq = o.isNe := by decide
@[simp]
theorem swap_lt : lt.swap = .gt := rfl
theorem ne_lt_iff_isGE : {o : Ordering}, ¬o = .lt o.isGE := by decide
theorem ne_gt_iff_isLE : {o : Ordering}, ¬o = .gt o.isLE := by decide
@[simp]
theorem swap_eq : eq.swap = .eq := rfl
@[simp] theorem swap_swap : {o : Ordering}, o.swap.swap = o := by decide
@[simp] theorem swap_inj : {o₁ o₂ : Ordering}, o₁.swap = o₂.swap o₁ = o₂ := by decide
@[simp]
theorem swap_gt : gt.swap = .lt := rfl
theorem swap_then : (o₁ o₂ : Ordering), (o₁.then o).swap = o.swap.then o₂.swap := by decide
theorem eq_eq_of_isLE_of_isLE_swap {o : Ordering} : o.isLE o.swap.isLE o = .eq := by
cases o <;> simp
theorem then_eq_lt : {o o₂ : Ordering}, o.then o₂ = lt o₁ = lt o = eq o₂ = lt := by decide
theorem then_eq_gt : {o₁ o₂ : Ordering}, o₁.then o₂ = gt o₁ = gt o₁ = eq o₂ = gt := by decide
@[simp] theorem then_eq_eq : {o₁ o₂ : Ordering}, o₁.then o₂ = eq o₁ = eq o₂ = eq := by decide
theorem eq_eq_of_isGE_of_isGE_swap {o : Ordering} : o.isGE o.swap.isGE o = .eq := by
cases o <;> simp
theorem isLT_then : {o o₂ : Ordering}, (o₁.then o).isLT = (o.isLT || o.isEq && o₂.isLT) := by decide
theorem isEq_then : {o₁ o₂ : Ordering}, (o₁.then o₂).isEq = (o₁.isEq && o₂.isEq) := by decide
theorem isNe_then : {o₁ o₂ : Ordering}, (o₁.then o₂).isNe = (o₁.isNe || o₂.isNe) := by decide
theorem isGT_then : {o₁ o₂ : Ordering}, (o₁.then o₂).isGT = (o₁.isGT || o₁.isEq && o₂.isGT) := by decide
theorem eq_eq_of_isLE_of_isGE {o : Ordering} : o.isLE o.isGE o = .eq := by
cases o <;> simp
@[simp] theorem lt_then {o : Ordering} : lt.then o = lt := rfl
@[simp] theorem gt_then {o : Ordering} : gt.then o = gt := rfl
@[simp] theorem eq_then {o : Ordering} : eq.then o = o := rfl
theorem eq_swap_iff_eq_eq {o : Ordering} : o = o.swap o = .eq := by
cases o <;> simp
@[simp] theorem then_eq : {o : Ordering}, o.then eq = o := by decide
@[simp] theorem then_self : {o : Ordering}, o.then o = o := by decide
theorem then_assoc : (o₁ o₂ o₃ : Ordering), (o₁.then o₂).then o₃ = o₁.then (o₂.then o₃) := by decide
theorem eq_eq_of_eq_swap {o : Ordering} : o = o.swap o = .eq :=
eq_swap_iff_eq_eq.mp
theorem isLE_then_iff_or : {o₁ o₂ : Ordering}, (o₁.then o₂).isLE o₁ = lt (o₁ = eq o₂.isLE) := by decide
theorem isLE_then_iff_and : {o o₂ : Ordering}, (o₁.then o).isLE o₁.isLE (o = lt o₂.isLE) := by decide
theorem isLE_left_of_isLE_then : {o o₂ : Ordering}, (o₁.then o₂).isLE o₁.isLE := by decide
theorem isGE_left_of_isGE_then : {o₁ o₂ : Ordering}, (o₁.then o₂).isGE o₁.isGE := by decide
@[simp]
theorem isLE_eq_false {o : Ordering} : o.isLE = false o = .gt := by
cases o <;> simp
instance : Std.Associative Ordering.then := then_assoc
instance : Std.IdempotentOp Ordering.then := fun _ => then_self
@[simp]
theorem isGE_eq_false {o : Ordering} : o.isGE = false o = .lt := by
cases o <;> simp
instance : Std.LawfulIdentity Ordering.then eq where
left_id _ := eq_then
right_id _ := then_eq
@[simp]
theorem swap_eq_gt {o : Ordering} : o.swap = .gt o = .lt := by
cases o <;> simp
@[simp]
theorem swap_eq_lt {o : Ordering} : o.swap = .lt o = .gt := by
cases o <;> simp
@[simp]
theorem swap_eq_eq {o : Ordering} : o.swap = .eq o = .eq := by
cases o <;> simp
@[simp]
theorem isLT_swap {o : Ordering} : o.swap.isLT = o.isGT := by
cases o <;> simp
@[simp]
theorem isLE_swap {o : Ordering} : o.swap.isLE = o.isGE := by
cases o <;> simp
@[simp]
theorem isEq_swap {o : Ordering} : o.swap.isEq = o.isEq := by
cases o <;> simp
@[simp]
theorem isNe_swap {o : Ordering} : o.swap.isNe = o.isNe := by
cases o <;> simp
@[simp]
theorem isGE_swap {o : Ordering} : o.swap.isGE = o.isLE := by
cases o <;> simp
@[simp]
theorem isGT_swap {o : Ordering} : o.swap.isGT = o.isLT := by
cases o <;> simp
theorem isLT_iff_eq_lt {o : Ordering} : o.isLT o = .lt := by
cases o <;> simp
theorem isLE_iff_eq_lt_or_eq_eq {o : Ordering} : o.isLE o = .lt o = .eq := by
cases o <;> simp
theorem isLE_of_eq_lt {o : Ordering} : o = .lt o.isLE := by
rintro rfl; rfl
theorem isLE_of_eq_eq {o : Ordering} : o = .eq o.isLE := by
rintro rfl; rfl
theorem isEq_iff_eq_eq {o : Ordering} : o.isEq o = .eq := by
cases o <;> simp
theorem isNe_iff_ne_eq {o : Ordering} : o.isNe o .eq := by
cases o <;> simp
theorem isGE_iff_eq_gt_or_eq_eq {o : Ordering} : o.isGE o = .gt o = .eq := by
cases o <;> simp
theorem isGE_of_eq_gt {o : Ordering} : o = .gt o.isGE := by
rintro rfl; rfl
theorem isGE_of_eq_eq {o : Ordering} : o = .eq o.isGE := by
rintro rfl; rfl
theorem isGT_iff_eq_gt {o : Ordering} : o.isGT o = .gt := by
cases o <;> simp
@[simp]
theorem swap_swap {o : Ordering} : o.swap.swap = o := by
cases o <;> simp
@[simp] theorem swap_inj {o₁ o₂ : Ordering} : o₁.swap = o₂.swap o₁ = o₂ :=
fun h => by simpa using congrArg swap h, congrArg _
theorem swap_then (o₁ o₂ : Ordering) : (o₁.then o₂).swap = o₁.swap.then o₂.swap := by
cases o₁ <;> rfl
theorem then_eq_lt {o₁ o₂ : Ordering} : o₁.then o₂ = lt o₁ = lt o₁ = eq o₂ = lt := by
cases o₁ <;> cases o₂ <;> decide
theorem then_eq_eq {o₁ o₂ : Ordering} : o₁.then o₂ = eq o₁ = eq o₂ = eq := by
cases o₁ <;> simp [«then»]
theorem then_eq_gt {o₁ o₂ : Ordering} : o₁.then o₂ = gt o₁ = gt o₁ = eq o₂ = gt := by
cases o₁ <;> cases o₂ <;> decide
@[simp]
theorem lt_then {o : Ordering} : lt.then o = lt := rfl
@[simp]
theorem gt_then {o : Ordering} : gt.then o = gt := rfl
@[simp]
theorem eq_then {o : Ordering} : eq.then o = o := rfl
theorem isLE_then_iff_or {o₁ o₂ : Ordering} : (o₁.then o₂).isLE o₁ = lt (o₁ = eq o₂.isLE) := by
cases o₁ <;> simp
theorem isLE_then_iff_and {o₁ o₂ : Ordering} : (o₁.then o₂).isLE o₁.isLE (o₁ = lt o₂.isLE) := by
cases o₁ <;> simp
theorem isLE_left_of_isLE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isLE) : o₁.isLE := by
cases o₁ <;> simp_all
theorem isGE_left_of_isGE_then {o₁ o₂ : Ordering} (h : (o₁.then o₂).isGE) : o₁.isGE := by
cases o₁ <;> simp_all
end Lemmas
@@ -335,7 +375,7 @@ section Lemmas
@[simp]
theorem compareLex_eq_eq {α} {cmp₁ cmp₂} {a b : α} :
compareLex cmp₁ cmp₂ a b = .eq cmp₁ a b = .eq cmp₂ a b = .eq := by
simp [compareLex]
simp [compareLex, Ordering.then_eq_eq]
theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α] [DecidableLT α] [DecidableEq α]
(h : x y : α, x < y ¬ y < x x y) {x y : α} :
@@ -344,14 +384,14 @@ theorem compareOfLessAndEq_eq_swap_of_lt_iff_not_gt_and_ne {α : Type u} [LT α]
split
· rename_i h'
rw [h] at h'
simp only [h'.1, h'.2.symm, reduceIte, Ordering.swap_gt]
simp only [h'.1, h'.2.symm, reduceIte, Ordering.swap_gt]
· split
· rename_i h'
have : ¬ y < y := Not.imp (·.2 rfl) <| (h y y).mp
simp only [h', this, reduceIte, Ordering.swap_eq]
simp only [h', this, reduceIte, Ordering.swap_eq]
· rename_i h' h''
replace h' := (h y x).mpr h', Ne.symm h''
simp only [h', Ne.symm h'', reduceIte, Ordering.swap_lt]
simp only [h', Ne.symm h'', reduceIte, Ordering.swap_lt]
theorem lt_iff_not_gt_and_ne_of_antisymm_of_total_of_not_le
{α : Type u} [LT α] [LE α] [DecidableLT α] [DecidableEq α]
@@ -438,13 +478,13 @@ but this is not enforced by the typeclass.
There is a derive handler, so appending `deriving Ord` to an inductive type or structure
will attempt to create an `Ord` instance.
-/
@[ext]
class Ord (α : Type u) where
/-- Compare two elements in `α` using the comparator contained in an `[Ord α]` instance. -/
compare : α α Ordering
export Ord (compare)
set_option linter.unusedVariables false in -- allow specifying `ord` explicitly
/--
Compares two values by comparing the results of applying a function.
@@ -724,13 +764,6 @@ end Vector
def lexOrd [Ord α] [Ord β] : Ord (α × β) where
compare := compareLex (compareOn (·.1)) (compareOn (·.2))
/--
Constructs an `BEq` instance from an `Ord` instance that asserts that the result of `compare` is
`Ordering.eq`.
-/
@[expose] def beqOfOrd [Ord α] : BEq α where
beq a b := (compare a b).isEq
/--
Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
`Ordering.lt`.
@@ -738,9 +771,8 @@ Constructs an `LT` instance from an `Ord` instance that asserts that the result
@[expose] def ltOfOrd [Ord α] : LT α where
lt a b := compare a b = Ordering.lt
@[inline]
instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) := fun a b =>
decidable_of_bool (compare a b).isLT Ordering.isLT_iff_eq_lt
instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
/--
Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
@@ -749,29 +781,35 @@ satisfies `Ordering.isLE`.
@[expose] def leOfOrd [Ord α] : LE α where
le a b := (compare a b).isLE
@[inline]
instance [Ord α] : DecidableRel (@LE.le α leOfOrd) := fun _ _ => instDecidableEqBool ..
instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
namespace Ord
/--
Constructs a `BEq` instance from an `Ord` instance.
-/
@[expose] protected abbrev toBEq (ord : Ord α) : BEq α :=
beqOfOrd
protected def toBEq (ord : Ord α) : BEq α where
beq x y := ord.compare x y == .eq
/--
Constructs an `LT` instance from an `Ord` instance.
-/
@[expose] protected abbrev toLT (ord : Ord α) : LT α :=
@[expose] protected def toLT (ord : Ord α) : LT α :=
ltOfOrd
instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
/--
Constructs an `LE` instance from an `Ord` instance.
-/
@[expose] protected abbrev toLE (ord : Ord α) : LE α :=
@[expose] protected def toLE (ord : Ord α) : LE α :=
leOfOrd
instance [i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i)) :=
inferInstanceAs (DecidableRel (fun a b => (compare a b).isLE))
/--
Inverts the order of an `Ord` instance.
@@ -795,7 +833,7 @@ protected def on (_ : Ord β) (f : α → β) : Ord α where
/--
Constructs the lexicographic order on products `α × β` from orders for `α` and `β`.
-/
protected abbrev lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
protected def lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
lexOrd
/--

View File

@@ -474,10 +474,7 @@ If not, usually the right approach is `simp [Vector.unattach, -Vector.map_subtyp
-/
def unattach {α : Type _} {p : α Prop} (xs : Vector { x // p x } n) : Vector α n := xs.map (·.val)
theorem unattach_empty {p : α Prop} : (#v[] : Vector { x // p x } 0).unattach = #v[] := by simp
@[deprecated unattach_empty (since := "2025-05-26")]
abbrev unattach_nil := @unattach_empty
@[simp] theorem unattach_nil {p : α Prop} : (#v[] : Vector { x // p x } 0).unattach = #v[] := by simp
@[simp] theorem unattach_push {p : α Prop} {a : { x // p x }} {xs : Vector { x // p x } n} :
(xs.push a).unattach = xs.unattach.push a.1 := by

View File

@@ -198,8 +198,6 @@ result is empty. If `stop` is greater than the size of the vector, the size is u
/--
Extract the first `i` elements of a vector. If `i` is greater than or equal to the size of the
vector then the vector is returned unchanged.
We immediately simplify this to the `extract` operation, so there is no verification API for this function.
-/
@[inline] def take (xs : Vector α n) (i : Nat) : Vector α (min i n) :=
xs.toArray.take i, by simp
@@ -209,22 +207,16 @@ We immediately simplify this to the `extract` operation, so there is no verifica
/--
Deletes the first `i` elements of a vector. If `i` is greater than or equal to the size of the
vector then the empty vector is returned.
We immediately simplify this to the `extract` operation, so there is no verification API for this function.
-/
@[inline] def drop (xs : Vector α n) (i : Nat) : Vector α (n - i) :=
xs.toArray.drop i, by simp
set_option linter.indexVariables false in
@[simp] theorem drop_eq_cast_extract (xs : Vector α n) (i : Nat) :
xs.drop i = (xs.extract i).cast (by simp) := by
xs.drop i = (xs.extract i n).cast (by simp) := by
simp [drop, extract, Vector.cast]
/--
Shrinks a vector to the first `m` elements, by repeatedly popping the last element.
We immediately simplify this to the `extract` operation, so there is no verification API for this function.
-/
/-- Shrinks a vector to the first `m` elements, by repeatedly popping the last element. -/
@[inline] def shrink (xs : Vector α n) (i : Nat) : Vector α (min i n) :=
xs.toArray.shrink i, by simp
@@ -402,17 +394,12 @@ instance [BEq α] : BEq (Vector α n) where
have : Inhabited (Vector α (n+1)) := xs.push x
panic! "index out of bounds"
/--
Delete the first element of a vector. Returns the empty vector if the input vector is empty.
We immediately simplify this to the `extract` operation, so there is no verification API for this function.
-/
@[inline]
def tail (xs : Vector α n) : Vector α (n-1) :=
(xs.extract 1).cast (by omega)
@[simp] theorem tail_eq_cast_extract (xs : Vector α n) :
xs.tail = (xs.extract 1).cast (by omega) := rfl
/-- Delete the first element of a vector. Returns the empty vector if the input vector is empty. -/
@[inline] def tail (xs : Vector α n) : Vector α (n-1) :=
if _ : 0 < n then
xs.eraseIdx 0
else
xs.cast (by omega)
/--
Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the

View File

@@ -40,8 +40,8 @@ theorem countP_push {a : α} {xs : Vector α n} : countP p (xs.push a) = countP
rcases xs with xs, rfl
simp [Array.countP_push]
theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by
simp
@[simp] theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by
simp [countP_push]
theorem size_eq_countP_add_countP {xs : Vector α n} : n = countP p xs + countP (fun a => ¬p a) xs := by
rcases xs with xs, rfl

View File

@@ -48,18 +48,15 @@ theorem beq_eq_decide [BEq α] (xs ys : Vector α n) :
(xs == ys) = decide ( (i : Nat) (h' : i < n), xs[i] == ys[i]) := by
simp [BEq.beq, isEqv_eq_decide]
@[deprecated mk_beq_mk (since := "2025-05-26")]
theorem beq_mk [BEq α] (xs ys : Array α) (ha : xs.size = n) (hb : ys.size = n) :
@[simp] theorem beq_mk [BEq α] (xs ys : Array α) (ha : xs.size = n) (hb : ys.size = n) :
(mk xs ha == mk ys hb) = (xs == ys) := by
simp
simp [BEq.beq]
@[deprecated toArray_beq_toArray (since := "2025-05-26")]
theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by
simp
@[simp, grind =] theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by
simp [beq_eq_decide, Array.beq_eq_decide]
@[deprecated toList_beq_toList (since := "2025-05-26")]
theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by
simp
@[simp] theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by
simp [beq_eq_decide, List.beq_eq_decide]
instance [BEq α] [ReflBEq α] : ReflBEq (Vector α n) where
rfl := by simp [BEq.beq, isEqv_self_beq]

View File

@@ -144,7 +144,7 @@ abbrev findSome?_mkVector_of_isNone := @findSome?_replicate_of_isNone
@[simp] theorem find?_empty : find? p #v[] = none := rfl
theorem find?_singleton {a : α} {p : α Bool} :
@[simp] theorem find?_singleton {a : α} {p : α Bool} :
#v[a].find? p = if p a then some a else none := by
simp
@@ -291,8 +291,7 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
/-! ### findFinIdx? -/
theorem findFinIdx?_empty {p : α Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
@[simp] theorem findFinIdx?_empty {p : α Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
theorem findFinIdx?_singleton {a : α} {p : α Bool} :
#[a].findFinIdx? p = if p a then some 0, by simp else none := by
simp

View File

@@ -486,7 +486,7 @@ abbrev toArray_mkVector := @toArray_replicate
`Vector.ext` is an extensionality theorem.
Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
-/
@[ext, grind ext]
@[ext]
protected theorem ext {xs ys : Vector α n} (h : (i : Nat) (_ : i < n) xs[i] = ys[i]) : xs = ys := by
apply Vector.toArray_inj.1
apply Array.ext
@@ -684,7 +684,8 @@ abbrev toList_eq_empty_iff {α n} (xs) := @toList_eq_nil_iff α n xs
/-! ### empty -/
theorem empty_eq {xs : Vector α 0} : #v[] = xs xs = #v[] := by
@[simp] theorem empty_eq {xs : Vector α 0} : #v[] = xs xs = #v[] := by
cases xs
simp
/-- A vector of length `0` is the empty vector. -/
@@ -815,11 +816,14 @@ abbrev mkVector_eq_mk_mkArray := @replicate_eq_mk_replicate
/-! ## L[i] and L[i]? -/
theorem getElem?_eq_none_iff {xs : Vector α n} : xs[i]? = none n i := by
simp
@[simp] theorem getElem?_eq_none_iff {xs : Vector α n} : xs[i]? = none n i := by
by_cases h : i < n
· simp [getElem?_pos, h]
· rw [getElem?_neg xs i h]
simp_all
theorem none_eq_getElem?_iff {xs : Vector α n} {i : Nat} : none = xs[i]? n i := by
simp
@[simp] theorem none_eq_getElem?_iff {xs : Vector α n} {i : Nat} : none = xs[i]? n i := by
simp [eq_comm (a := none)]
theorem getElem?_eq_none {xs : Vector α n} (h : n i) : xs[i]? = none := by
simp [getElem?_eq_none_iff, h]
@@ -831,23 +835,23 @@ grind_pattern Vector.getElem?_eq_none => n ≤ i, xs[i]?
@[simp] theorem getElem?_eq_getElem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i]? = some xs[i] :=
getElem?_pos ..
theorem getElem?_eq_some_iff {xs : Vector α n} : xs[i]? = some b h : i < n, xs[i] = b :=
_root_.getElem?_eq_some_iff
theorem getElem?_eq_some_iff {xs : Vector α n} : xs[i]? = some b h : i < n, xs[i] = b := by
simp [getElem?_def]
@[grind ]
theorem getElem_of_getElem? {xs : Vector α n} : xs[i]? = some a h : i < n, xs[i] = a :=
getElem?_eq_some_iff.mp
theorem some_eq_getElem?_iff {xs : Vector α n} : some b = xs[i]? h : i < n, xs[i] = b :=
_root_.some_eq_getElem?_iff
theorem some_eq_getElem?_iff {xs : Vector α n} : some b = xs[i]? h : i < n, xs[i] = b := by
rw [eq_comm, getElem?_eq_some_iff]
theorem some_getElem_eq_getElem?_iff {xs : Vector α n} {i : Nat} (h : i < n) :
@[simp] theorem some_getElem_eq_getElem?_iff {xs : Vector α n} {i : Nat} (h : i < n) :
(some xs[i] = xs[i]?) True := by
simp
simp [h]
theorem getElem?_eq_some_getElem_iff {xs : Vector α n} {i : Nat} (h : i < n) :
@[simp] theorem getElem?_eq_some_getElem_iff {xs : Vector α n} {i : Nat} (h : i < n) :
(xs[i]? = some xs[i]) True := by
simp
simp [h]
theorem getElem_eq_iff {xs : Vector α n} {i : Nat} {h : i < n} : xs[i] = x xs[i]? = some x := by
simp only [getElem?_eq_some_iff]
@@ -887,11 +891,12 @@ theorem getElem?_push {xs : Vector α n} {x : α} {i : Nat} : (xs.push x)[i]? =
(repeat' split) <;> first | rfl | omega
set_option linter.indexVariables false in
theorem getElem?_push_size {xs : Vector α n} {x : α} : (xs.push x)[n]? = some x := by
simp
@[simp] theorem getElem?_push_size {xs : Vector α n} {x : α} : (xs.push x)[n]? = some x := by
simp [getElem?_push]
theorem getElem_singleton {a : α} (h : i < 1) : #v[a][i] = a := by
simp
@[simp] theorem getElem_singleton {a : α} (h : i < 1) : #v[a][i] = a :=
match i, h with
| 0, _ => rfl
@[grind]
theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a else none := by
@@ -903,7 +908,7 @@ theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a
rcases xs with xs, rfl
simp
theorem not_mem_empty (a : α) : ¬ a #v[] := nofun
@[simp] theorem not_mem_empty (a : α) : ¬ a #v[] := nofun
@[simp] theorem mem_push {xs : Vector α n} {x y : α} : x xs.push y x xs x = y := by
rcases xs with xs, rfl
@@ -952,7 +957,8 @@ theorem size_zero_iff_forall_not_mem {xs : Vector α n} : n = 0 ↔ ∀ a, a ∉
theorem eq_of_mem_singleton (h : a #v[b]) : a = b := by
simpa using h
theorem mem_singleton {a b : α} : a #v[b] a = b := by simp
@[simp] theorem mem_singleton {a b : α} : a #v[b] a = b :=
eq_of_mem_singleton, (by simp [·])
theorem forall_mem_push {p : α Prop} {xs : Vector α n} {a : α} :
( x, x xs.push a p x) p a x, x xs p x := by
@@ -1438,9 +1444,10 @@ theorem back_eq_getElem [NeZero n] {xs : Vector α n} : xs.back = xs[n - 1]'(by
simp
/-- The empty vector maps to the empty vector. -/
@[grind]
@[simp, grind]
theorem map_empty {f : α β} : map f #v[] = #v[] := by
simp
rw [map, mk.injEq]
exact Array.map_empty
@[simp, grind] theorem map_push {f : α β} {as : Vector α n} {x : α} :
(as.push x).map f = (as.map f).push (f x) := by
@@ -1517,8 +1524,9 @@ theorem map_eq_push_iff {f : α → β} {xs : Vector α (n + 1)} {ys : Vector β
· rintro xs', a, h₁, h₂, rfl
refine xs'.toArray, a, by simp_all
theorem map_eq_singleton_iff {f : α β} {xs : Vector α 1} {b : β} :
@[simp] theorem map_eq_singleton_iff {f : α β} {xs : Vector α 1} {b : β} :
map f xs = #v[b] a, xs = #v[a] f a = b := by
cases xs
simp
theorem map_eq_map_iff {f g : α β} {xs : Vector α n} :
@@ -2097,7 +2105,7 @@ abbrev forall_mem_mkVector := @forall_mem_replicate
@[deprecated getElem_replicate (since := "2025-03-18")]
abbrev getElem_mkVector := @getElem_replicate
@[grind] theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
@[grind]theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
simp [getElem?_def]
@[deprecated getElem?_replicate (since := "2025-03-18")]
@@ -2353,13 +2361,13 @@ set_option linter.indexVariables false in
rcases ys with ys, rfl
simp
theorem foldlM_empty [Monad m] {f : β α m β} {init : β} :
@[simp] theorem foldlM_empty [Monad m] {f : β α m β} {init : β} :
foldlM f init #v[] = return init := by
simp
simp [foldlM]
@[grind] theorem foldrM_empty [Monad m] {f : α β m β} {init : β} :
@[simp, grind] theorem foldrM_empty [Monad m] {f : α β m β} {init : β} :
foldrM f init #v[] = return init := by
simp
simp [foldrM]
@[simp, grind] theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Vector α n} {a : α} {f : β α m β} {b} :
(xs.push a).foldlM f b = xs.foldlM f b >>= fun b => f b a := by
@@ -2377,23 +2385,19 @@ theorem foldrM_pure [Monad m] [LawfulMonad m] {f : α → β → β} {b} {xs : V
Array.foldrM_pure
theorem foldl_eq_foldlM {f : β α β} {b} {xs : Vector α n} :
xs.foldl f b = (xs.foldlM (m := Id) (pure <| f · ·) b).run := rfl
xs.foldl f b = xs.foldlM (m := Id) f b := by
rcases xs with xs, rfl
simp [Array.foldl_eq_foldlM]
theorem foldr_eq_foldrM {f : α β β} {b} {xs : Vector α n} :
xs.foldr f b = (xs.foldrM (m := Id) (pure <| f · ·) b).run := rfl
xs.foldr f b = xs.foldrM (m := Id) f b := by
rcases xs with xs, rfl
simp [Array.foldr_eq_foldrM]
@[simp] theorem idRun_foldlM {f : β α Id β} {b} {xs : Vector α n} :
Id.run (xs.foldlM f b) = xs.foldl (f · · |>.run) b := foldl_eq_foldlM.symm
@[deprecated idRun_foldlM (since := "2025-05-21")]
theorem id_run_foldlM {f : β α Id β} {b} {xs : Vector α n} :
@[simp] theorem id_run_foldlM {f : β α Id β} {b} {xs : Vector α n} :
Id.run (xs.foldlM f b) = xs.foldl f b := foldl_eq_foldlM.symm
@[simp] theorem idRun_foldrM {f : α β Id β} {b} {xs : Vector α n} :
Id.run (xs.foldrM f b) = xs.foldr (f · · |>.run) b := foldr_eq_foldrM.symm
@[deprecated idRun_foldrM (since := "2025-05-21")]
theorem id_run_foldrM {f : α β Id β} {b} {xs : Vector α n} :
@[simp] theorem id_run_foldrM {f : α β Id β} {b} {xs : Vector α n} :
Id.run (xs.foldrM f b) = xs.foldr f b := foldr_eq_foldrM.symm
@[simp] theorem foldlM_reverse [Monad m] {xs : Vector α n} {f : β α m β} {b} :
@@ -2481,10 +2485,10 @@ theorem foldr_map_hom {g : α → β} {f : ααα} {f' : β → β →
simp
@[simp, grind _=_] theorem foldl_append {β : Type _} {f : β α β} {b} {xs : Vector α n} {ys : Vector α k} :
(xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := foldlM_append
(xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by simp [foldl_eq_foldlM]
@[simp, grind _=_] theorem foldr_append {f : α β β} {b} {xs : Vector α n} {ys : Vector α k} :
(xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := foldrM_append
(xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by simp [foldr_eq_foldrM]
@[simp, grind] theorem foldl_flatten {f : β α β} {b} {xss : Vector (Vector α m) n} :
(flatten xss).foldl f b = xss.foldl (fun b xs => xs.foldl f b) b := by
@@ -2497,8 +2501,7 @@ theorem foldr_map_hom {g : α → β} {f : ααα} {f' : β → β →
simp [Array.foldr_flatten', Array.foldr_map']
@[simp, grind] theorem foldl_reverse {xs : Vector α n} {f : β α β} {b} :
xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b :=
foldlM_reverse
xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
@[simp, grind] theorem foldr_reverse {xs : Vector α n} {f : α β β} {b} :
xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b :=
@@ -2677,7 +2680,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Vector α n} {a : α} :
rcases xs with xs, rfl
simp [Array.contains_iff_exists_mem_beq]
@[grind _=_]
@[grind]
theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
xs.contains a a xs := by
simp
@@ -3050,7 +3053,8 @@ end replace
/-! Content below this point has not yet been aligned with `List` and `Array`. -/
set_option linter.indexVariables false in
theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by
@[simp] theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by
rcases xs with xs, rfl
simp
@[simp] theorem push_pop_back (xs : Vector α (n + 1)) : xs.pop.push xs.back = xs := by
@@ -3082,7 +3086,8 @@ theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by
/-! ### take -/
set_option linter.indexVariables false in
theorem take_size {as : Vector α n} : as.take n = as.cast (by simp) := by
@[simp] theorem take_size {as : Vector α n} : as.take n = as.cast (by simp) := by
rcases as with as, rfl
simp
/-! ### swap -/
@@ -3131,8 +3136,9 @@ theorem swap_comm {xs : Vector α n} {i j : Nat} (hi hj) :
/-! ### drop -/
@[grind =] theorem getElem_drop {xs : Vector α n} {j : Nat} (hi : i < n - j) :
@[simp, grind =] theorem getElem_drop {xs : Vector α n} {j : Nat} (hi : i < n - j) :
(xs.drop j)[i] = xs[j + i] := by
cases xs
simp
/-! ### Decidable quantifiers. -/

View File

@@ -58,8 +58,9 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys
cases xs
simp_all
theorem singleton_lex_singleton [BEq α] {lt : α α Bool} : #v[a].lex #v[b] lt = lt a b := by
simp
@[simp] theorem singleton_lex_singleton [BEq α] {lt : α α Bool} : #v[a].lex #v[b] lt = lt a b := by
simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton]
cases lt a b <;> cases a != b <;> simp [Id.run]
protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α α Prop)] (xs : Vector α n) : ¬ xs < xs :=
Array.lt_irrefl xs.toArray

View File

@@ -295,8 +295,9 @@ theorem mapIdx_eq_push_iff {xs : Vector α (n + 1)} {b : β} :
· rintro a, zs, rfl, rfl, rfl
exact zs, a, rfl, by simp
theorem mapIdx_eq_singleton_iff {xs : Vector α 1} {f : Nat α β} {b : β} :
@[simp] theorem mapIdx_eq_singleton_iff {xs : Vector α 1} {f : Nat α β} {b : β} :
mapIdx f xs = #v[b] (a : α), xs = #v[a] f 0 a = b := by
rcases xs with xs
simp
theorem mapIdx_eq_append_iff {xs : Vector α (n + m)} {f : Nat α β} {ys : Vector β n} {zs : Vector β m} :

View File

@@ -25,10 +25,10 @@ open Nat
/-! ## Monadic operations -/
theorem map_toArray_inj [Monad m] [LawfulMonad m]
@[simp] theorem map_toArray_inj [Monad m] [LawfulMonad m]
{xs : m (Vector α n)} {ys : m (Vector α n)} :
toArray <$> xs = toArray <$> ys xs = ys := by
simp
toArray <$> xs = toArray <$> ys xs = ys :=
_root_.map_inj_right (by simp)
/-! ### mapM -/
@@ -148,18 +148,12 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
rcases xs with xs, rfl
simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map]
theorem idRun_forIn'_yield_eq_foldl
{xs : Vector α n} (f : (a : α) a xs β Id β) (init : β) :
(forIn' xs init (fun a m b => .yield <$> f a m b)).run =
xs.attach.foldl (fun b a, h => f a h b |>.run) init := by
simp
@[deprecated forIn'_yield_eq_foldl (since := "2025-05-21")]
theorem forIn'_yield_eq_foldl
@[simp] theorem forIn'_yield_eq_foldl
{xs : Vector α n} (f : (a : α) a xs β β) (init : β) :
forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) =
xs.attach.foldl (fun b a, h => f a h b) init :=
forIn'_pure_yield_eq_foldl _ _
xs.attach.foldl (fun b a, h => f a h b) init := by
rcases xs with xs, rfl
simp [List.foldl_map]
@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
{xs : Vector α n} (g : α β) (f : (b : β) b xs.map g γ m (ForInStep γ)) :
@@ -196,18 +190,12 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
rcases xs with xs, rfl
simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map]
theorem idRun_forIn_yield_eq_foldl
{xs : Vector α n} (f : α β Id β) (init : β) :
(forIn xs init (fun a b => .yield <$> f a b)).run =
xs.foldl (fun b a => f a b |>.run) init := by
simp
@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
theorem forIn_yield_eq_foldl
@[simp] theorem forIn_yield_eq_foldl
{xs : Vector α n} (f : α β β) (init : β) :
forIn (m := Id) xs init (fun a b => .yield (f a b)) =
xs.foldl (fun b a => f a b) init :=
forIn_pure_yield_eq_foldl _ _
xs.foldl (fun b a => f a b) init := by
rcases xs with xs, rfl
simp
@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
{xs : Vector α n} (g : α β) (f : β γ m (ForInStep γ)) :

View File

@@ -154,6 +154,7 @@ theorem ofFnM_pure [Monad m] [LawfulMonad m] {n} {f : Fin n → α} :
@[simp, grind =] theorem idRun_ofFnM {f : Fin n Id α} :
Id.run (ofFnM f) = ofFn (fun i => Id.run (f i)) := by
unfold Id.run
induction n with
| zero => simp
| succ n ih => simp [ofFnM_succ', ofFn_succ', ih]

View File

@@ -82,8 +82,6 @@ end Lean
attribute [ext] Prod PProd Sigma PSigma
attribute [ext] funext propext Subtype.eq Array.ext
attribute [grind ext] Array.ext
@[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
protected theorem Unit.ext (x y : Unit) : x = y := rfl

View File

@@ -198,58 +198,6 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
simp only [getElem?_def]
split <;> simp_all
@[simp] theorem none_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) [Decidable (dom c i)] : none = c[i]? ¬dom c i := by
simp only [getElem?_def]
split <;> simp_all
theorem of_getElem?_eq_some [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
{c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : dom c i := by
simp only [getElem?_def] at h
split at h <;> rename_i h'
case isTrue =>
exact h'
case isFalse =>
simp at h
theorem getElem?_eq_some_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
{c : cont} {i : idx} [Decidable (dom c i)] : c[i]? = some e Exists fun h : dom c i => c[i] = e := by
simp only [getElem?_def]
split <;> rename_i h
case isTrue =>
constructor
case mp =>
intro w
refine h, ?_
simpa using w
case mpr =>
intro h, w
simpa using w
case isFalse =>
simp only [reduceCtorEq, false_iff]
intro w, w'
exact h w
theorem some_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
{c : cont} {i : idx} [Decidable (dom c i)] : some e = c[i]? Exists fun h : dom c i => c[i] = e := by
rw [eq_comm, getElem?_eq_some_iff]
theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
{c : cont} {i : idx} [Decidable (dom c i)] (h : c[i]? = some e) : Exists fun h : dom c i => c[i] = e :=
getElem?_eq_some_iff.mp h
grind_pattern getElem_of_getElem? => c[i]?, some e
@[simp] theorem some_getElem_eq_getElem?_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
{c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
(some c[i] = c[i]?) True := by
simpa [some_eq_getElem?_iff, h] using h, trivial
@[simp] theorem getElem?_eq_some_getElem_iff [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
{c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i):
(c[i]? = some c[i]) True := by
simpa [getElem?_eq_some_iff, h] using h, trivial
@[deprecated getElem?_eq_none_iff (since := "2025-02-17")]
abbrev getElem?_eq_none := @getElem?_eq_none_iff
@@ -348,8 +296,7 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where
| zero => rfl
| succ i => exact ih ..
-- This is only needed locally; after the `LawfulGetElem` instance the general `getElem?_eq_none_iff` lemma applies.
@[local simp] theorem getElem?_eq_none_iff : l[i]? = none length l i :=
@[simp] theorem getElem?_eq_none_iff : l[i]? = none length l i :=
match l with
| [] => by simp; rfl
| _ :: l => by
@@ -359,7 +306,7 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where
simp only [length_cons, Nat.add_le_add_iff_right]
exact getElem?_eq_none_iff (l := l) (i := i)
theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? length l i := by
@[simp] theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? length l i := by
simp [eq_comm (a := none)]
theorem getElem?_eq_none (h : length l i) : l[i]? = none := getElem?_eq_none_iff.mpr h

View File

@@ -12,8 +12,8 @@ namespace Lean.Grind
class Field (α : Type u) extends CommRing α, Inv α, Div α where
div_eq_mul_inv : a b : α, a / b = a * b⁻¹
zero_ne_one : (0 : α) 1
inv_zero : (0 : α)⁻¹ = 0
inv_one : (1 : α)⁻¹ = 1
mul_inv_cancel : {a : α}, a 0 a * a⁻¹ = 1
attribute [instance 100] Field.toInv Field.toDiv
@@ -25,52 +25,6 @@ variable [Field α] {a : α}
theorem inv_mul_cancel (h : a 0) : a⁻¹ * a = 1 := by
rw [CommSemiring.mul_comm, mul_inv_cancel h]
theorem eq_inv_of_mul_eq_one (h : a * b = 1) : a = b⁻¹ := by
by_cases h' : b = 0
· subst h'
rw [Semiring.mul_zero] at h
exfalso
exact zero_ne_one h
· replace h := congrArg (fun x => x * b⁻¹) h
simpa [Semiring.mul_assoc, mul_inv_cancel h', Semiring.mul_one, Semiring.one_mul] using h
theorem inv_one : (1 : α)⁻¹ = 1 :=
(eq_inv_of_mul_eq_one (Semiring.mul_one 1)).symm
theorem inv_inv (a : α) : a⁻¹⁻¹ = a := by
by_cases h : a = 0
· subst h
simp [Field.inv_zero]
· symm
apply eq_inv_of_mul_eq_one
exact mul_inv_cancel h
theorem inv_neg (a : α) : (-a)⁻¹ = -a⁻¹ := by
by_cases h : a = 0
· subst h
simp [Field.inv_zero, Ring.neg_zero]
· symm
apply eq_inv_of_mul_eq_one
simp [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg, Field.inv_mul_cancel h]
theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 a = 0 := by
constructor
· intro w
by_cases h : a = 0
· subst h
rfl
· have := congrArg (fun x => x * a) w
dsimp at this
rw [Semiring.zero_mul, inv_mul_cancel h] at this
exfalso
exact zero_ne_one this.symm
· intro w
subst w
simp [Field.inv_zero]
theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ 0 = a := by
rw [eq_comm, inv_eq_zero_iff, eq_comm]
instance [IsCharP α 0] : NoNatZeroDivisors α where
no_nat_zero_divisors := by
intro a b h w

View File

@@ -6,8 +6,7 @@ Authors: Kim Morrison
module
prelude
import Init.Grind.Ordered.Order
import Init.Grind.Ordered.PartialOrder
import Init.Grind.Ordered.Module
import Init.Grind.Ordered.Ring
import Init.Grind.Ordered.Field
import Init.Grind.Ordered.Int

View File

@@ -1,188 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
module
prelude
import Init.Grind.CommRing.Field
import Init.Grind.Ordered.Ring
namespace Lean.Grind
namespace Field.IsOrdered
variable {R : Type u} [Field R] [LinearOrder R] [Ring.IsOrdered R]
open Ring.IsOrdered
theorem pos_of_inv_pos {a : R} (h : 0 < a⁻¹) : 0 < a := by
rcases LinearOrder.trichotomy 0 a with (h' | rfl | h')
· exact h'
· simpa [Field.inv_zero] using h
· exfalso
have := Ring.IsOrdered.mul_neg_of_pos_of_neg h h'
rw [inv_mul_cancel (Preorder.ne_of_lt h')] at this
exact Ring.IsOrdered.not_one_lt_zero this
theorem inv_pos_iff {a : R} : 0 < a⁻¹ 0 < a := by
constructor
· exact pos_of_inv_pos
· intro h
rw [ Field.inv_inv a] at h
exact pos_of_inv_pos h
theorem inv_neg_iff {a : R} : a⁻¹ < 0 a < 0 := by
have := inv_pos_iff (a := -a)
rw [Field.inv_neg] at this
simpa [IntModule.IsOrdered.neg_pos_iff]
theorem inv_nonneg_iff {a : R} : 0 a⁻¹ 0 a := by
simp [PartialOrder.le_iff_lt_or_eq, inv_pos_iff, Field.zero_eq_inv_iff]
theorem inv_nonpos_iff {a : R} : a⁻¹ 0 a 0 := by
have := inv_nonneg_iff (a := -a)
rw [Field.inv_neg] at this
simpa [IntModule.IsOrdered.neg_nonneg_iff] using this
private theorem mul_le_of_le_mul_inv {a b c : R} (h : 0 < c) (h' : a b * c⁻¹) : a * c b := by
simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
Ring.IsOrdered.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt h)
private theorem le_mul_inv_of_mul_le {a b c : R} (h : 0 < b) (h' : a * b c) : a c * b⁻¹ := by
simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
Ring.IsOrdered.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
theorem le_mul_inv_iff_mul_le (a b : R) {c : R} (h : 0 < c) : a b * c⁻¹ a * c b :=
mul_le_of_le_mul_inv h, le_mul_inv_of_mul_le h
private theorem mul_inv_le_iff_le_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ c a c * b := by
have := (le_mul_inv_iff_mul_le a c (inv_pos_iff.mpr h)).symm
simpa [Field.inv_inv] using this
private theorem mul_lt_of_lt_mul_inv {a b c : R} (h : 0 < c) (h' : a < b * c⁻¹) : a * c < b := by
simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
Ring.IsOrdered.mul_lt_mul_of_pos_right h' h
private theorem lt_mul_inv_of_mul_lt {a b c : R} (h : 0 < b) (h' : a * b < c) : a < c * b⁻¹ := by
simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
Ring.IsOrdered.mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
theorem lt_mul_inv_iff_mul_lt (a b : R) {c : R} (h : 0 < c) : a < b * c⁻¹ a * c < b :=
mul_lt_of_lt_mul_inv h, lt_mul_inv_of_mul_lt h
theorem mul_inv_lt_iff_lt_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ < c a < c * b := by
simpa [Field.inv_inv] using (lt_mul_inv_iff_mul_lt a c (inv_pos_iff.mpr h)).symm
private theorem le_mul_of_le_mul_inv {a b c : R} (h : c < 0) (h' : a b * c⁻¹) : b a * c := by
simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
private theorem mul_le_of_mul_inv_le {a b c : R} (h : b < 0) (h' : a * b⁻¹ c) : c * b a := by
simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
private theorem mul_inv_le_of_mul_le {a b c : R} (h : b < 0) (h' : a * b c) : c * b⁻¹ a := by
simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
private theorem le_mul_inv_of_le_mul {a b c : R} (h : c < 0) (h' : a b * c) : b a * c⁻¹ := by
simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
theorem le_mul_inv_iff_le_mul_of_neg (a b : R) {c : R} (h : c < 0) : a b * c⁻¹ b a * c :=
le_mul_of_le_mul_inv h, le_mul_inv_of_le_mul h
theorem mul_inv_le_iff_mul_le_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹ c c * b a :=
mul_le_of_mul_inv_le h, mul_inv_le_of_mul_le h
private theorem lt_mul_of_lt_mul_inv {a b c : R} (h : c < 0) (h' : a < b * c⁻¹) : b < a * c := by
simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
Ring.IsOrdered.mul_lt_mul_of_neg_right h' h
private theorem mul_lt_of_mul_inv_lt {a b c : R} (h : b < 0) (h' : a * b⁻¹ < c) : c * b < a := by
simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
Ring.IsOrdered.mul_lt_mul_of_neg_right h' h
private theorem mul_inv_lt_of_mul_lt {a b c : R} (h : b < 0) (h' : a * b < c) : c * b⁻¹ < a := by
simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
Ring.IsOrdered.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
private theorem lt_mul_inv_of_lt_mul {a b c : R} (h : c < 0) (h' : a < b * c) : b < a * c⁻¹ := by
simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
Ring.IsOrdered.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
theorem lt_mul_inv_iff_lt_mul_of_neg (a b : R) {c : R} (h : c < 0) : a < b * c⁻¹ b < a * c :=
lt_mul_of_lt_mul_inv h, lt_mul_inv_of_lt_mul h
theorem mul_inv_lt_iff_mul_lt_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹ < c c * b < a :=
mul_lt_of_mul_inv_lt h, mul_inv_lt_of_mul_lt h
theorem mul_lt_mul_iff_of_pos_right {a b c : R} (h : 0 < c) : a * c < b * c a < b := by
constructor
· intro h'
have := mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_gt h),
Semiring.mul_one, Semiring.mul_one] at this
· exact (mul_lt_mul_of_pos_right · h)
theorem mul_lt_mul_iff_of_pos_left {a b c : R} (h : 0 < c) : c * a < c * b a < b := by
constructor
· intro h'
have := mul_lt_mul_of_pos_left h' (inv_pos_iff.mpr h)
rwa [ Semiring.mul_assoc, Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_gt h),
Semiring.one_mul, Semiring.one_mul] at this
· exact (mul_lt_mul_of_pos_left · h)
theorem mul_lt_mul_iff_of_neg_right {a b c : R} (h : c < 0) : a * c < b * c b < a := by
constructor
· intro h'
have := mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_lt h),
Semiring.mul_one, Semiring.mul_one] at this
· exact (mul_lt_mul_of_neg_right · h)
theorem mul_lt_mul_iff_of_neg_left {a b c : R} (h : c < 0) : c * a < c * b b < a := by
constructor
· intro h'
have := mul_lt_mul_of_neg_left h' (inv_neg_iff.mpr h)
rwa [ Semiring.mul_assoc, Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_lt h),
Semiring.one_mul, Semiring.one_mul] at this
· exact (mul_lt_mul_of_neg_left · h)
theorem mul_le_mul_iff_of_pos_right {a b c : R} (h : 0 < c) : a * c b * c a b := by
constructor
· intro h'
have := mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_gt h),
Semiring.mul_one, Semiring.mul_one] at this
· exact (mul_le_mul_of_nonneg_right · (Preorder.le_of_lt h))
theorem mul_le_mul_iff_of_pos_left {a b c : R} (h : 0 < c) : c * a c * b a b := by
constructor
· intro h'
have := mul_le_mul_of_nonneg_left h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
rwa [ Semiring.mul_assoc, Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_gt h),
Semiring.one_mul, Semiring.one_mul] at this
· exact (mul_le_mul_of_nonneg_left · (Preorder.le_of_lt h))
theorem mul_le_mul_iff_of_neg_right {a b c : R} (h : c < 0) : a * c b * c b a := by
constructor
· intro h'
have := mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_lt h),
Semiring.mul_one, Semiring.mul_one] at this
· exact (mul_le_mul_of_nonpos_right · (Preorder.le_of_lt h))
theorem mul_le_mul_iff_of_neg_left {a b c : R} (h : c < 0) : c * a c * b b a := by
constructor
· intro h'
have := mul_le_mul_of_nonpos_left h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
rwa [ Semiring.mul_assoc, Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_lt h),
Semiring.one_mul, Semiring.one_mul] at this
· exact (mul_le_mul_of_nonpos_left · (Preorder.le_of_lt h))
end Field.IsOrdered
end Lean.Grind

View File

@@ -8,7 +8,7 @@ module
prelude
import Init.Data.Int.Order
import Init.Grind.Module.Basic
import Init.Grind.Ordered.Order
import Init.Grind.Ordered.PartialOrder
namespace Lean.Grind

View File

@@ -34,22 +34,9 @@ theorem lt_of_le_of_lt {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c := b
theorem lt_trans {a b c : α} (h₁ : a < b) (h₂ : b < c) : a < c :=
lt_of_lt_of_le h₁ (le_of_lt h₂)
theorem lt_irrefl (a : α) : ¬ (a < a) := by
intro h
theorem lt_irrefl {a : α} (h : a < a) : False := by
simp [lt_iff_le_not_le] at h
theorem ne_of_lt {a b : α} (h : a < b) : a b :=
fun w => lt_irrefl a (w.symm h)
theorem ne_of_gt {a b : α} (h : a > b) : a b :=
fun w => lt_irrefl b (w.symm h)
theorem not_ge_of_lt {a b : α} (h : a < b) : ¬b a :=
fun w => lt_irrefl a (lt_of_lt_of_le h w)
theorem not_gt_of_lt {a b : α} (h : a < b) : ¬a > b :=
fun w => lt_irrefl a (lt_trans h w)
end Preorder
class PartialOrder (α : Type u) extends Preorder α where
@@ -71,26 +58,4 @@ theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b a = b := by
end PartialOrder
class LinearOrder (α : Type u) extends PartialOrder α where
le_total : a b : α, a b b a
namespace LinearOrder
variable {α : Type u} [LinearOrder α]
theorem trichotomy (a b : α) : a < b a = b b < a := by
cases LinearOrder.le_total a b with
| inl h =>
rw [PartialOrder.le_iff_lt_or_eq] at h
cases h with
| inl h => left; exact h
| inr h => right; left; exact h
| inr h =>
rw [PartialOrder.le_iff_lt_or_eq] at h
cases h with
| inl h => right; right; exact h
| inr h => right; left; exact h.symm
end LinearOrder
end Lean.Grind

View File

@@ -13,7 +13,7 @@ namespace Lean.Grind
class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends IntModule.IsOrdered R where
/-- In a strict ordered semiring, we have `0 < 1`. -/
zero_lt_one : (0 : R) < 1
zero_lt_one : 0 < 1
/-- In a strict ordered semiring, we can multiply an inequality `a < b` on the left
by a positive element `0 < c` to obtain `c * a < c * b`. -/
mul_lt_mul_of_pos_left : {a b c : R}, a < b 0 < c c * a < c * b
@@ -23,15 +23,7 @@ class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends IntModule.IsOrde
namespace Ring.IsOrdered
variable {R : Type u} [Ring R]
section PartialOrder
variable [PartialOrder R] [Ring.IsOrdered R]
theorem zero_le_one : (0 : R) 1 := Preorder.le_of_lt zero_lt_one
theorem not_one_lt_zero : ¬ ((1 : R) < 0) :=
fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h)
variable {R : Type u} [Ring R] [PartialOrder R] [Ring.IsOrdered R]
theorem mul_le_mul_of_nonneg_left {a b c : R} (h : a b) (h' : 0 c) : c * a c * b := by
rw [PartialOrder.le_iff_lt_or_eq] at h'
@@ -55,104 +47,19 @@ theorem mul_le_mul_of_nonneg_right {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : a
| inr h => subst h; exact Preorder.le_refl (a * c)
| inr h' => subst h'; simp [Semiring.mul_zero, Preorder.le_refl]
theorem mul_le_mul_of_nonpos_left {a b c : R} (h : a b) (h' : c 0) : c * b c * a := by
have := mul_le_mul_of_nonneg_left h (IntModule.IsOrdered.neg_nonneg_iff.mpr h')
rwa [Ring.neg_mul, Ring.neg_mul, IntModule.IsOrdered.neg_le_iff, IntModule.neg_neg] at this
theorem mul_le_mul_of_nonpos_right {a b c : R} (h : a b) (h' : c 0) : b * c a * c := by
have := mul_le_mul_of_nonneg_right h (IntModule.IsOrdered.neg_nonneg_iff.mpr h')
rwa [Ring.mul_neg, Ring.mul_neg, IntModule.IsOrdered.neg_le_iff, IntModule.neg_neg] at this
theorem mul_lt_mul_of_neg_left {a b c : R} (h : a < b) (h' : c < 0) : c * b < c * a := by
have := mul_lt_mul_of_pos_left h (IntModule.IsOrdered.neg_pos_iff.mpr h')
rwa [Ring.neg_mul, Ring.neg_mul, IntModule.IsOrdered.neg_lt_iff, IntModule.neg_neg] at this
theorem mul_lt_mul_of_neg_right {a b c : R} (h : a < b) (h' : c < 0) : b * c < a * c := by
have := mul_lt_mul_of_pos_right h (IntModule.IsOrdered.neg_pos_iff.mpr h')
rwa [Ring.mul_neg, Ring.mul_neg, IntModule.IsOrdered.neg_lt_iff, IntModule.neg_neg] at this
theorem mul_nonneg {a b : R} (h₁ : 0 a) (h₂ : 0 b) : 0 a * b := by
simpa [Semiring.zero_mul] using mul_le_mul_of_nonneg_right h₁ h₂
theorem mul_nonneg_of_nonpos_of_nonpos {a b : R} (h₁ : a 0) (h₂ : b 0) : 0 a * b := by
have := mul_nonneg (IntModule.IsOrdered.neg_nonneg_iff.mpr h₁) (IntModule.IsOrdered.neg_nonneg_iff.mpr h₂)
simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
theorem mul_nonpos_of_nonneg_of_nonpos {a b : R} (h₁ : 0 a) (h₂ : b 0) : a * b 0 := by
rw [ IntModule.IsOrdered.neg_nonneg_iff, Ring.mul_neg]
apply mul_nonneg h₁ (IntModule.IsOrdered.neg_nonneg_iff.mpr h₂)
theorem mul_nonpos_of_nonpos_of_nonneg {a b : R} (h₁ : a 0) (h₂ : 0 b) : a * b 0 := by
rw [ IntModule.IsOrdered.neg_nonneg_iff, Ring.neg_mul]
apply mul_nonneg (IntModule.IsOrdered.neg_nonneg_iff.mpr h₁) h₂
theorem mul_pos {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂
theorem mul_pos_of_neg_of_neg {a b : R} (h : a < 0) (h₂ : b < 0) : 0 < a * b := by
have := mul_pos (IntModule.IsOrdered.neg_pos_iff.mpr h₁) (IntModule.IsOrdered.neg_pos_iff.mpr h₂)
simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
theorem sq_nonneg {a : R} (h : 0 a) : 0 a^2 := by
rw [Semiring.pow_two]
apply mul_nonneg h h
theorem mul_neg_of_pos_of_neg {a b : R} (h : 0 < a) (h₂ : b < 0) : a * b < 0 := by
rw [ IntModule.IsOrdered.neg_pos_iff, Ring.mul_neg]
apply mul_pos h (IntModule.IsOrdered.neg_pos_iff.mpr h)
theorem mul_neg_of_neg_of_pos {a b : R} (h₁ : a < 0) (h₂ : 0 < b) : a * b < 0 := by
rw [ IntModule.IsOrdered.neg_pos_iff, Ring.neg_mul]
apply mul_pos (IntModule.IsOrdered.neg_pos_iff.mpr h₁) h₂
end PartialOrder
section LinearOrder
variable [LinearOrder R] [Ring.IsOrdered R]
theorem mul_nonneg_iff {a b : R} : 0 a * b 0 a 0 b a 0 b 0 := by
rcases LinearOrder.trichotomy 0 a with (ha | rfl | ha)
· rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
· simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, mul_nonneg]
· simp [Semiring.mul_zero, Preorder.le_refl, LinearOrder.le_total]
· have m : a * b < 0 := mul_neg_of_pos_of_neg ha hb
simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, Preorder.not_ge_of_lt m,
Preorder.not_ge_of_lt ha, Preorder.not_ge_of_lt hb]
· simp [Semiring.zero_mul, Preorder.le_refl, LinearOrder.le_total]
· rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
· have m : a * b < 0 := mul_neg_of_neg_of_pos ha hb
simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, Preorder.not_ge_of_lt m,
Preorder.not_ge_of_lt ha, Preorder.not_ge_of_lt hb]
· simp [Semiring.mul_zero, Preorder.le_refl, LinearOrder.le_total]
· simp [Preorder.le_of_lt ha, Preorder.le_of_lt hb, mul_nonneg_of_nonpos_of_nonpos]
theorem mul_pos_iff {a b : R} : 0 < a * b 0 < a 0 < b a < 0 b < 0 := by
rcases LinearOrder.trichotomy 0 a with (ha | rfl | ha)
· rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
· simp [ha, hb, mul_pos]
· simp [Preorder.lt_irrefl, Semiring.mul_zero]
· have m : a * b < 0 := mul_neg_of_pos_of_neg ha hb
simp [ha, hb, Preorder.not_gt_of_lt m,
Preorder.not_gt_of_lt ha, Preorder.not_gt_of_lt hb]
· simp [Preorder.lt_irrefl, Semiring.zero_mul]
· rcases LinearOrder.trichotomy 0 b with (hb | rfl | hb)
· have m : a * b < 0 := mul_neg_of_neg_of_pos ha hb
simp [ha, hb, Preorder.not_gt_of_lt m,
Preorder.not_gt_of_lt ha, Preorder.not_gt_of_lt hb]
· simp [Preorder.lt_irrefl, Semiring.mul_zero]
· simp [ha, hb, mul_pos_of_neg_of_neg]
theorem sq_nonneg {a : R} : 0 a^2 := by
rw [Semiring.pow_two, mul_nonneg_iff]
rcases LinearOrder.le_total 0 a with (h | h)
· exact .inl h, h
· exact .inr h, h
theorem sq_pos {a : R} (h : a 0) : 0 < a^2 := by
rw [Semiring.pow_two, mul_pos_iff]
rcases LinearOrder.trichotomy 0 a with (h' | rfl | h')
· exact .inl h', h'
· simp at h
· exact .inr h', h'
end LinearOrder
theorem sq_pos {a : R} (h : 0 < a) : 0 < a^2 := by
rw [Semiring.pow_two]
apply mul_pos h h
end Ring.IsOrdered

View File

@@ -97,7 +97,7 @@ structure Config where
This approach is cheaper but incomplete. -/
qlia : Bool := false
/--
If `mbtc` is `true`, `grind` will use model-based theory combination for creating new case splits.
If `mbtc` is `true`, `grind` will use model-based theory commbination for creating new case splits.
See paper "Model-based Theory Combination" for details.
-/
mbtc : Bool := true

View File

@@ -1317,7 +1317,7 @@ test with the predicate `p`. The resulting array contains the tested elements fo
`true`, separated by the corresponding separator elements.
-/
def filterSepElems (a : Array Syntax) (p : Syntax → Bool) : Array Syntax :=
Id.run <| a.filterSepElemsM (pure <| p ·)
Id.run <| a.filterSepElemsM p
private partial def mapSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax → m Syntax) (i : Nat) (acc : Array Syntax) : m (Array Syntax) := do
if h : i < a.size then
@@ -1334,7 +1334,7 @@ def mapSepElemsM {m : Type → Type} [Monad m] (a : Array Syntax) (f : Syntax
mapSepElemsMAux a f 0 #[]
def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax :=
Id.run <| a.mapSepElemsM (pure <| f ·)
Id.run <| a.mapSepElemsM f
end Array

View File

@@ -244,11 +244,6 @@ structure Config where
`let x := v; e` simplifies to `e` when `x` does not occur in `e`.
-/
zetaUnused : Bool := true
/--
When `true` (default : `true`), then simps will catch runtime exceptions and
convert them into `simp` exceptions.
-/
catchRuntime : Bool := true
deriving Inhabited, BEq
-- Configuration object for `simp_all`

View File

@@ -140,36 +140,9 @@ references to a hypothesis.
syntax (name := clear) "clear" (ppSpace colGt term:max)+ : tactic
/--
Syntax for trying to clear the values of all local definitions.
-/
syntax clearValueStar := "*"
/--
* `clear_value x...` clears the values of the given local definitions.
A local definition `x : α := v` becomes a hypothesis `x : α`.
* `clear_value x with h` adds a hypothesis `h : x = v` before clearing the value of `x`.
This is short for `have h : x = v := rfl; clear_value x`, with the benefit of not needing to mention `v`.
* `clear_value *` clears values of all hypotheses that can be cleared.
Fails if none can be cleared.
These syntaxes can be combined. For example, `clear_value x y *` ensures that `x` and `y` are cleared
while trying to clear all other local definitions, and `clear_value x y * with hx` does the same,
but adds the `hx : x = v` hypothesis first. Having a `with` binding associated to `*` is not allowed.
-/
syntax (name := clearValue) "clear_value" (ppSpace colGt (clearValueStar <|> term:max))+ (" with" (ppSpace colGt binderIdent)+)? : tactic
/--
`subst x...` substitutes each hypothesis `x` with a definition found in the local context,
then eliminates the hypothesis.
- If `x` is a local definition, then its definition is used.
- Otherwise, if there is a hypothesis of the form `x = e` or `e = x`,
then `e` is used for the definition of `x`.
If `h : a = b`, then `subst h` may be used if either `a` or `b` unfolds to a local hypothesis.
This is similar to the `cases h` tactic.
See also: `subst_vars` for substituting all local hypotheses that have a defining equation.
`subst x...` substitutes each `x` with `e` in the goal if there is a hypothesis
of type `x = e` or `e = x`.
If `x` is itself a hypothesis of type `y = e` or `e = y`, `y` is substituted instead.
-/
syntax (name := subst) "subst" (ppSpace colGt term:max)+ : tactic

View File

@@ -497,13 +497,8 @@ def emitNumLit (t : IRType) (v : Nat) : M Unit := do
else
if v < UInt32.size then
emit v
else if t == .usize then
emit "((size_t)"
emit v
emit "ULL)"
else
emit v
emit "ULL"
emit v; emit "ULL"
def emitLit (z : VarId) (t : IRType) (v : LitVal) : M Unit := do
emitLhs z;

View File

@@ -70,7 +70,7 @@ def lowerLitValue (v : LCNF.LitValue) : LitVal :=
| .uint8 v => .num (UInt8.toNat v)
| .uint16 v => .num (UInt16.toNat v)
| .uint32 v => .num (UInt32.toNat v)
| .uint64 v | .usize v => .num (UInt64.toNat v)
| .uint64 v => .num (UInt64.toNat v)
-- TODO: This should be cached.
def lowerEnumToScalarType (name : Name) : M (Option IRType) := do

View File

@@ -40,9 +40,7 @@ inductive LitValue where
| uint16 (val : UInt16)
| uint32 (val : UInt32)
| uint64 (val : UInt64)
-- USize has a maximum size of 64 bits
| usize (val : UInt64)
-- TODO: add constructors for `Int`, `Float`, ...
-- TODO: add constructors for `Int`, `Float`, `USize` ...
deriving Inhabited, BEq, Hashable
def LitValue.toExpr : LitValue Expr
@@ -52,7 +50,6 @@ def LitValue.toExpr : LitValue → Expr
| .uint16 v => .app (.const ``UInt16.ofNat []) (.lit (.natVal (UInt16.toNat v)))
| .uint32 v => .app (.const ``UInt32.ofNat []) (.lit (.natVal (UInt32.toNat v)))
| .uint64 v => .app (.const ``UInt64.ofNat []) (.lit (.natVal (UInt64.toNat v)))
| .usize v => .app (.const ``USize.ofNat []) (.lit (.natVal (UInt64.toNat v)))
inductive Arg where
| erased

View File

@@ -177,7 +177,7 @@ def ofLCNFLit : LCNF.LitValue → Value
| .uint8 v => ofNat (UInt8.toNat v)
| .uint16 v => ofNat (UInt16.toNat v)
| .uint32 v => ofNat (UInt32.toNat v)
| .uint64 v | .usize v => ofNat (UInt64.toNat v)
| .uint64 v => ofNat (UInt64.toNat v)
partial def proj : Value Nat Value
| .ctor _ vs , i => vs.getD i bot

View File

@@ -1,156 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Cameron Zwarich
-/
prelude
import Lean.Compiler.ClosedTermCache
import Lean.Compiler.NeverExtractAttr
import Lean.Compiler.LCNF.Basic
import Lean.Compiler.LCNF.InferType
import Lean.Compiler.LCNF.Internalize
import Lean.Compiler.LCNF.MonoTypes
import Lean.Compiler.LCNF.PassManager
import Lean.Compiler.LCNF.ToExpr
namespace Lean.Compiler.LCNF
namespace ExtractClosed
abbrev ExtractM := StateRefT (Array CodeDecl) CompilerM
mutual
partial def extractLetValue (v : LetValue) : ExtractM Unit := do
match v with
| .const _ _ args => args.forM extractArg
| .fvar fnVar args =>
extractFVar fnVar
args.forM extractArg
| .proj _ _ baseVar => extractFVar baseVar
| .lit _ | .erased => return ()
partial def extractArg (arg : Arg) : ExtractM Unit := do
match arg with
| .fvar fvarId => extractFVar fvarId
| .type _ | .erased => return ()
partial def extractFVar (fvarId : FVarId) : ExtractM Unit := do
if let some letDecl findLetDecl? fvarId then
modify fun decls => decls.push (.let letDecl)
extractLetValue letDecl.value
end
def isIrrelevantArg (arg : Arg) : Bool :=
match arg with
| .erased | .type _ => true
| .fvar _ => false
structure Context where
baseName : Name
sccDecls : Array Decl
structure State where
decls : Array Decl := {}
abbrev M := ReaderT Context $ StateRefT State CompilerM
mutual
partial def shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool := do
match v with
| .lit (.str _) => return true
| .lit (.nat v) =>
-- The old compiler's implementation used the runtime's `is_scalar` function, which
-- introduces a dependency on the architecture used by the compiler.
return v >= Nat.pow 2 63
| .lit _ | .erased => return !isRoot
| .const name _ args =>
if ( read).sccDecls.any (·.name == name) then
return false
if hasNeverExtractAttribute ( getEnv) name then
return false
if isRoot then
if let some constInfo := ( getEnv).find? name then
let shouldExtract := match constInfo with
| .defnInfo val => val.type.isForall
| .ctorInfo _ => !(args.all isIrrelevantArg)
| _ => true
if !shouldExtract then
return false
args.allM shouldExtractArg
| .fvar fnVar args => return ( shouldExtractFVar fnVar) && ( args.allM shouldExtractArg)
| .proj _ _ baseVar => shouldExtractFVar baseVar
partial def shouldExtractArg (arg : Arg) : M Bool := do
match arg with
| .fvar fvarId => shouldExtractFVar fvarId
| .type _ | .erased => return true
partial def shouldExtractFVar (fvarId : FVarId) : M Bool := do
if let some letDecl findLetDecl? fvarId then
shouldExtractLetValue false letDecl.value
else
return false
end
mutual
partial def visitCode (code : Code) : M Code := do
match code with
| .let decl k =>
if ( shouldExtractLetValue true decl.value) then
let _, decls extractLetValue decl.value |>.run {}
let decls := decls.reverse.push (.let decl)
let decls decls.mapM Internalize.internalizeCodeDecl |>.run' {}
let closedCode := attachCodeDecls decls (.return decls.back!.fvarId)
let closedExpr := closedCode.toExpr
let env getEnv
let name if let some closedTermName := getClosedTermName? env closedExpr then
eraseCode closedCode
pure closedTermName
else
let name := ( read).baseName ++ (`_closedTerm).appendIndexAfter ( get).decls.size
cacheClosedTermName env closedExpr name |> setEnv
let decl := { name, levelParams := [], type := decl.type, params := #[],
value := .code closedCode, inlineAttr? := some .noinline }
decl.saveMono
modify fun s => { s with decls := s.decls.push decl }
pure name
let decl decl.updateValue (.const name [] #[])
return code.updateLet! decl ( visitCode k)
else
return code.updateLet! decl ( visitCode k)
| .fun decl k =>
let decl decl.updateValue ( visitCode decl.value)
return code.updateFun! decl ( visitCode k)
| .jp decl k =>
let decl decl.updateValue ( visitCode decl.value)
return code.updateFun! decl ( visitCode k)
| .cases cases =>
let alts cases.alts.mapM (fun alt => do return alt.updateCode ( visitCode alt.getCode))
return code.updateAlts! alts
| .jmp .. | .return _ | .unreach .. => return code
end
def visitDecl (decl : Decl) : M Decl := do
let value decl.value.mapCodeM visitCode
return { decl with value }
end ExtractClosed
partial def Decl.extractClosed (decl : Decl) (sccDecls : Array Decl) : CompilerM (Array Decl) := do
let decl, s ExtractClosed.visitDecl decl |>.run { baseName := decl.name, sccDecls } |>.run {}
return s.decls.push decl
def extractClosed : Pass where
phase := .mono
name := `extractClosed
run := fun decls =>
decls.foldlM (init := #[]) fun newDecls decl => return newDecls ++ ( decl.extractClosed decls)
builtin_initialize registerTraceClass `Compiler.extractClosed (inherited := true)
end Lean.Compiler.LCNF

View File

@@ -205,9 +205,9 @@ where
if !( f fvar) then failure
def anyFVar [TraverseFVar α] (f : FVarId Bool) (x : α) : Bool :=
Id.run <| anyFVarM (pure <| f ·) x
Id.run <| anyFVarM f x
def allFVar [TraverseFVar α] (f : FVarId Bool) (x : α) : Bool :=
Id.run <| allFVarM (pure <| f ·) x
Id.run <| allFVarM f x
end Lean.Compiler.LCNF

View File

@@ -109,7 +109,6 @@ def inferLitValueType (value : LitValue) : Expr :=
| .uint16 .. => mkConst ``UInt16
| .uint32 .. => mkConst ``UInt32
| .uint64 .. => mkConst ``UInt64
| .usize .. => mkConst ``USize
mutual
partial def inferArgType (arg : Arg) : InferTypeM Expr :=

View File

@@ -19,7 +19,6 @@ import Lean.Compiler.LCNF.FloatLetIn
import Lean.Compiler.LCNF.ReduceArity
import Lean.Compiler.LCNF.ElimDeadBranches
import Lean.Compiler.LCNF.StructProjCases
import Lean.Compiler.LCNF.ExtractClosed
namespace Lean.Compiler.LCNF
@@ -80,8 +79,7 @@ def builtinPassManager : PassManager := {
simp (occurrence := 5) (phase := .mono),
structProjCases,
cse (occurrence := 2) (phase := .mono),
saveMono, -- End of mono phase
extractClosed
saveMono -- End of mono phase
]
}

View File

@@ -13,8 +13,7 @@ abbrev DeclExtState := PHashMap Name Decl
private abbrev declLt (a b : Decl) :=
Name.quickLt a.name b.name
private def sortedDecls (s : DeclExtState) : Array Decl :=
let decls := s.foldl (init := #[]) fun ps _ v => ps.push v
private abbrev sortDecls (decls : Array Decl) : Array Decl :=
decls.qsort declLt
private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Decl :=
@@ -22,28 +21,17 @@ private abbrev findAtSorted? (decls : Array Decl) (declName : Name) : Option Dec
let tmpDecl := { tmpDecl with name := declName }
decls.binSearch tmpDecl declLt
def DeclExt := PersistentEnvExtension Decl Decl DeclExtState
abbrev DeclExt := SimplePersistentEnvExtension Decl DeclExtState
instance : Inhabited DeclExt :=
inferInstanceAs (Inhabited (PersistentEnvExtension Decl Decl DeclExtState))
def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt :=
registerPersistentEnvExtension {
name,
mkInitial := pure {},
addImportedFn := fun _ => pure {},
addEntryFn := fun s decl => s.insert decl.name decl
exportEntriesFn := sortedDecls
statsFn := fun s =>
let numEntries := s.foldl (init := 0) (fun count _ _ => count + 1)
format "number of local entries: " ++ format numEntries
asyncMode := .sync,
replay? := some <| fun oldState newState _ otherState =>
newState.foldl (init := otherState) fun otherState k v =>
if oldState.contains k then
otherState
else
otherState.insert k v
def mkDeclExt (name : Name := by exact decl_name%) : IO DeclExt := do
registerSimplePersistentEnvExtension {
name := name
addImportedFn := fun _ => {}
addEntryFn := fun decls decl => decls.insert decl.name decl
toArrayFn := (sortDecls ·.toArray)
asyncMode := .sync -- compilation is non-parallel anyway
replay? := some <| SimplePersistentEnvExtension.replayOfFilter
(fun s d => !s.contains d.name) (fun decls decl => decls.insert decl.name decl)
}
builtin_initialize baseExt : DeclExt mkDeclExt

View File

@@ -58,7 +58,7 @@ def ppArgs (args : Array Arg) : M Format := do
def ppLitValue (lit : LitValue) : M Format := do
match lit with
| .nat v | .uint8 v | .uint16 v | .uint32 v | .uint64 v | .usize v => return format v
| .nat v | .uint8 v | .uint16 v | .uint32 v | .uint64 v => return format v
| .str v => return format (repr v)
def ppLetValue (e : LetValue) : M Format := do

View File

@@ -368,7 +368,6 @@ def conversionFolders : List (Name × Folder) := [
(``UInt16.ofNat, Folder.ofNat (fun v => .uint16 (UInt16.ofNat v))),
(``UInt32.ofNat, Folder.ofNat (fun v => .uint32 (UInt32.ofNat v))),
(``UInt64.ofNat, Folder.ofNat (fun v => .uint64 (UInt64.ofNat v))),
(``USize.ofNat, Folder.ofNat (fun v => .usize (UInt64.ofNat v))),
]
/--

View File

@@ -31,11 +31,11 @@ def mkFieldParamsForCtorType (e : Expr) (numParams : Nat): CompilerM (Array Para
| _ => return params
loop #[] e numParams
structure State where
structure StructProjState where
projMap : Std.HashMap FVarId (Array FVarId) := {}
fvarMap : Std.HashMap FVarId FVarId := {}
abbrev M := StateRefT State CompilerM
abbrev M := StateRefT StructProjState CompilerM
def M.run (x : M α) : CompilerM α := do
x.run' {}
@@ -128,6 +128,4 @@ end StructProjCases
def structProjCases : Pass :=
.mkPerDeclaration `structProjCases (StructProjCases.visitDecl · |>.run) .mono
builtin_initialize registerTraceClass `Compiler.structProjCases (inherited := true)
end Lean.Compiler.LCNF

View File

@@ -38,7 +38,7 @@ def isEmpty : AssocList α β → Bool
foldlM f d es
@[inline] def foldl (f : δ α β δ) (init : δ) (as : AssocList α β) : δ :=
Id.run (foldlM (pure <| f · · ·) init as)
Id.run (foldlM f init as)
def toList (as : AssocList α β) : List (α × β) :=
as.foldl (init := []) (fun r a b => (a, b)::r) |>.reverse

View File

@@ -75,9 +75,9 @@ def NameTrie.forM [Monad m] (t : NameTrie β) (f : β → m Unit) : m Unit :=
t.forMatchingM Name.anonymous f
def NameTrie.matchingToArray (t : NameTrie β) (k : Name) : Array β :=
Id.run <| t.foldMatchingM k #[] fun v acc => return acc.push v
Id.run <| t.foldMatchingM k #[] fun v acc => acc.push v
def NameTrie.toArray (t : NameTrie β) : Array β :=
Id.run <| t.foldM #[] fun v acc => return acc.push v
Id.run <| t.foldM #[] fun v acc => acc.push v
end Lean

View File

@@ -281,10 +281,10 @@ instance : ForIn m (PersistentArray α) α where
end
@[inline] def foldl (t : PersistentArray α) (f : β α β) (init : β) (start : Nat := 0) : β :=
Id.run <| t.foldlM (pure <| f · ·) init start
Id.run <| t.foldlM f init start
@[inline] def foldr (t : PersistentArray α) (f : α β β) (init : β) : β :=
Id.run <| t.foldrM (pure <| f · ·) init
Id.run <| t.foldrM f init
@[inline] def filter (as : PersistentArray α) (p : α Bool) : PersistentArray α :=
as.foldl (init := {}) fun asNew a => if p a then asNew.push a else asNew
@@ -301,10 +301,10 @@ def append (t₁ t₂ : PersistentArray α) : PersistentArray α :=
instance : Append (PersistentArray α) := append
@[inline] def findSome? {β} (t : PersistentArray α) (f : α (Option β)) : Option β :=
Id.run $ t.findSomeM? (pure <| f ·)
Id.run $ t.findSomeM? f
@[inline] def findSomeRev? {β} (t : PersistentArray α) (f : α (Option β)) : Option β :=
Id.run $ t.findSomeRevM? (pure <| f ·)
Id.run $ t.findSomeRevM? f
def toList (t : PersistentArray α) : List α :=
(t.foldl (init := []) fun xs x => x :: xs).reverse
@@ -325,7 +325,7 @@ variable {m : Type → Type w} [Monad m]
end
@[inline] def any (a : PersistentArray α) (p : α Bool) : Bool :=
Id.run $ anyM a (pure <| p ·)
Id.run $ anyM a p
@[inline] def all (a : PersistentArray α) (p : α Bool) : Bool :=
!any a fun v => !p v
@@ -346,7 +346,7 @@ variable {β : Type u}
end
@[inline] def map {β} (f : α β) (t : PersistentArray α) : PersistentArray β :=
Id.run $ t.mapM (pure <| f ·)
Id.run $ t.mapM f
structure Stats where
numNodes : Nat

View File

@@ -288,7 +288,7 @@ def forM {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : α
map.foldlM (fun _ => f)
def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ α β σ) (init : σ) : σ :=
Id.run <| map.foldlM (pure <| f · · ·) init
Id.run <| map.foldlM f init
protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
(map : PersistentHashMap α β) (init : σ) (f : α × β σ m (ForInStep σ)) : m σ := do
@@ -322,7 +322,7 @@ def mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Mona
return { root }
def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β σ) : PersistentHashMap α σ :=
Id.run <| pm.mapM (pure <| f ·)
Id.run <| pm.mapM f
def toList {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) : List (α × β) :=
m.foldl (init := []) fun ps k v => (k, v) :: ps

View File

@@ -48,7 +48,7 @@ variable {_ : BEq α} {_ : Hashable α}
s.set.foldlM (init := init) fun d a _ => f d a
@[inline] def fold {β : Type v} (f : β α β) (init : β) (s : PersistentHashSet α) : β :=
Id.run $ s.foldM (pure <| f · ·) init
Id.run $ s.foldM f init
def toList (s : PersistentHashSet α) : List α :=
s.set.toList.map (·.1)

View File

@@ -1146,11 +1146,8 @@ inductive LValResolution where
The `fullName` is the name of the recursive function, and `baseName` is the base name of the type to search for in the parameter list. -/
| localRec (baseName : Name) (fullName : Name) (fvar : Expr)
private def throwLValErrorAt (ref : Syntax) (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
throwErrorAt ref "{msg}{indentExpr e}\nhas type{indentExpr eType}"
private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α := do
throwLValErrorAt ( getRef) e eType msg
private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
throwError "{msg}{indentExpr e}\nhas type{indentExpr eType}"
/--
`findMethod? S fName` tries the for each namespace `S'` in the resolution order for `S` to resolve the name `S'.fname`.
@@ -1209,7 +1206,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
return LValResolution.projIdx structName (idx - 1)
else
throwLValError e eType m!"invalid projection, structure has only {numFields} field(s)"
| some structName, LVal.fieldName _ fieldName _ fullRef =>
| some structName, LVal.fieldName _ fieldName _ _ =>
let env getEnv
if isStructure env structName then
if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
@@ -1226,10 +1223,10 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
if let some (baseStructName, fullName) findMethod? structName (.mkSimple fieldName) then
return LValResolution.const baseStructName structName fullName
let msg := mkUnknownIdentifierMessage m!"invalid field '{fieldName}', the environment does not contain '{Name.mkStr structName fieldName}'"
throwLValErrorAt fullRef e eType msg
| none, LVal.fieldName _ _ (some suffix) fullRef =>
throwLValError e eType msg
| none, LVal.fieldName _ _ (some suffix) _ =>
if e.isConst then
throwUnknownConstantAt fullRef (e.constName! ++ suffix)
throwUnknownConstant (e.constName! ++ suffix)
else
throwInvalidFieldNotation e eType
| _, _ => throwInvalidFieldNotation e eType
@@ -1514,7 +1511,7 @@ where
else if let some (fvar, []) resolveLocalName idNew then
return fvar
else
throwUnknownIdentifierAt id m!"invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
throwUnknownIdentifier m!"invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
catch
| ex@(.error ..) =>
match ( unfoldDefinition? resultType) with

View File

@@ -311,7 +311,7 @@ def elabMutual : CommandElab := fun stx => do
if ( Simp.isBuiltinSimproc name) then
pure [name]
else
throwUnknownConstantAt ident name
throwUnknownConstant name
let declName ensureNonAmbiguous ident declNames
Term.applyAttributes declName attrs
for attrName in toErase do

View File

@@ -209,14 +209,14 @@ where
| none => processLeaf s
processBinOp (ref : Syntax) (kind : BinOpKind) (f lhs rhs : Syntax) := do
let some f resolveId? f | throwUnknownConstantAt f f.getId
let some f resolveId? f | throwUnknownConstant f.getId
-- treat corresponding argument as leaf for `leftact/rightact`
let lhs if kind == .leftact then processLeaf lhs else go lhs
let rhs if kind == .rightact then processLeaf rhs else go rhs
return .binop ref kind f lhs rhs
processUnOp (ref : Syntax) (f arg : Syntax) := do
let some f resolveId? f | throwUnknownConstantAt f f.getId
let some f resolveId? f | throwUnknownConstant f.getId
return .unop ref f ( go arg)
processLeaf (s : Syntax) := do
@@ -547,7 +547,7 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
let result toExprCore ( applyCoe tree maxType (isPred := true))
trace[Elab.binrel] "result: {result}"
return result
| none => throwUnknownConstantAt stx[1] stx[1].getId
| none => throwUnknownConstant stx[1].getId
where
/-- If `noProp == true` and `e` has type `Prop`, then coerce it to `Bool`. -/
toBoolIfNecessary (e : Expr) : TermElabM Expr := do

View File

@@ -344,56 +344,6 @@ where
replaceMainGoal [mvarId]
| _ => throwUnsupportedSyntax
@[builtin_tactic Lean.Parser.Tactic.clearValue] def evalClearValue : Tactic := fun stx =>
match stx with
| `(tactic| clear_value $xs* $[with $hs*]?) => withMainContext do
let hs := hs.getD #[]
if xs.size < hs.size then throwErrorAt hs[xs.size]! "Too many binders provided."
let mut fvarIds : Array FVarId := #[]
let mut hasStar := false
let mut newHyps : Array (FVarId × Name) := #[]
for i in [0:xs.size], x in xs do
if x.raw.isOfKind ``Parser.Tactic.clearValueStar then
if i < hs.size then
throwErrorAt hs[i]! "When using `*`, no binder may be provided for it."
hasStar := true
else
let fvarId getFVarId x
unless ( fvarId.isLetVar) do
throwErrorAt x "Hypothesis `{mkFVar fvarId}` is not a local definition."
if fvarIds.contains fvarId then
throwErrorAt x "Hypothesis `{mkFVar fvarId}` appears multiple times."
fvarIds := fvarIds.push fvarId
if let some h := hs[i]? then
let hName
match h with
| `(binderIdent| $n:ident) => pure n.raw.getId
| _ => mkFreshBinderNameForTactic `h
newHyps := newHyps.push (fvarId, hName)
let mut g popMainGoal
unless newHyps.isEmpty do
let mut hyps : Array Hypothesis := #[]
for (fvarId, hName) in newHyps do
let type mkEq (mkFVar fvarId) ( fvarId.getValue?).get!
let value mkEqRefl (mkFVar fvarId)
hyps := hyps.push { userName := hName, type, value }
g Prod.snd <$> g.assertHypotheses hyps
let toClear g.withContext do
if hasStar then pure <| ( getLocalHyps).map Expr.fvarId!
else sortFVarIds fvarIds
let mut succeeded := false
for fvarId in toClear.reverse do
try
g g.clearValue fvarId
succeeded := true
catch _ =>
if fvarIds.contains fvarId then
g.withContext do throwError "Tactic `clear_value` failed, the value of `{Expr.fvar fvarId}` cannot be cleared.\n{g}"
unless succeeded do
g.withContext do throwError "Tactic `clear_value` failed to clear any values.\n{g}"
pushGoal g
| _ => throwUnsupportedSyntax
def forEachVar (hs : Array Syntax) (tac : MVarId FVarId MetaM MVarId) : TacticM Unit := do
for h in hs do
withMainContext do
@@ -403,20 +353,7 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
@[builtin_tactic Lean.Parser.Tactic.subst] def evalSubst : Tactic := fun stx =>
match stx with
| `(tactic| subst $hs*) => forEachVar hs fun mvarId fvarId => do
let decl fvarId.getDecl
if decl.isLet then
-- Zeta delta reduce the let and eliminate it.
let (_, mvarId) mvarId.withReverted #[fvarId] fun mvarId' fvars => mvarId'.withContext do
let tgt mvarId'.getType
assert! tgt.isLet
let mvarId'' mvarId'.replaceTargetDefEq (tgt.letBody!.instantiate1 tgt.letValue!)
-- Dropped the let fvar
let aliasing := (fvars.extract 1).map some
return ((), aliasing, mvarId'')
return mvarId
else
Meta.subst mvarId fvarId
| `(tactic| subst $hs*) => forEachVar hs Meta.subst
| _ => throwUnsupportedSyntax
@[builtin_tactic Lean.Parser.Tactic.substVars] def evalSubstVars : Tactic := fun _ =>

View File

@@ -202,7 +202,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
if ( Simp.isBuiltinSimproc name) then
simprocs := simprocs.erase name
else
throwUnknownConstantAt id name
withRef id <| throwUnknownConstant name
else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
let post :=
if arg[0].isNone then

View File

@@ -47,10 +47,10 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
`(tactic| simp_all!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
else
`(tactic| simp_all%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
let { ctx, simprocs, .. } mkSimpContext stx (eraseLocal := true)
let { ctx, .. } mkSimpContext stx (eraseLocal := true)
(kind := .simpAll) (ignoreStarArg := true)
let ctx := if bang.isSome then ctx.setAutoUnfold else ctx
let (result?, stats) simpAll ( getMainGoal) ctx (simprocs := simprocs)
let (result?, stats) simpAll ( getMainGoal) ctx
match result? with
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]

View File

@@ -1979,7 +1979,7 @@ where
isValidAutoBoundImplicitName n (relaxedAutoImplicit.get ( getOptions)) then
throwAutoBoundImplicitLocal n
else
throwUnknownIdentifierAt stx m!"unknown identifier '{Lean.mkConst n}'"
throwUnknownIdentifier m!"unknown identifier '{Lean.mkConst n}'"
mkConsts candidates explicitLevels
/--

View File

@@ -454,9 +454,6 @@ private partial def AsyncConsts.findRec? (aconsts : AsyncConsts) (declName : Nam
let c aconsts.findPrefix? declName
if c.constInfo.name == declName then
return c
-- If privacy is the only difference between `declName` and `findPrefix?` result, we can assume
-- `declName` does not exist according to the `add` invariant
guard <| privateToUserName c.constInfo.name != privateToUserName declName
let aconsts c.consts.get.get? AsyncConsts
AsyncConsts.findRec? aconsts declName

View File

@@ -76,43 +76,28 @@ prompt the code action.
-/
def unknownIdentifierMessageTag : Name := `unknownIdentifier
/-- Throw an error exception using the given message data and reference syntax. -/
protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α := do
withRef ref <| Lean.throwError msg
/--
Creates a `MessageData` that is tagged with `unknownIdentifierMessageTag`.
This tag is used by the 'import unknown identifier' code action to detect messages that should
prompt the code action.
The end position of the range of an unknown identifier message should always point at the end of the
unknown identifier.
-/
def mkUnknownIdentifierMessage (msg : MessageData) : MessageData :=
MessageData.tagged unknownIdentifierMessageTag msg
/--
Throw an unknown identifier error message that is tagged with `unknownIdentifierMessageTag`.
The end position of the range of `ref` should always point at the unknown identifier.
See also `mkUnknownIdentifierMessage`.
-/
def throwUnknownIdentifierAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α :=
Lean.throwErrorAt ref <| mkUnknownIdentifierMessage msg
def throwUnknownIdentifier [Monad m] [MonadError m] (msg : MessageData) : m α :=
Lean.throwError <| mkUnknownIdentifierMessage msg
/--
Throw an unknown constant error message.
The end position of the range of `ref` should point at the unknown identifier.
See also `mkUnknownIdentifierMessage`.
-/
def throwUnknownConstantAt [Monad m] [MonadError m] (ref : Syntax) (constName : Name) : m α := do
throwUnknownIdentifierAt ref m!"unknown constant '{.ofConstName constName}'"
/-- Throw an unknown constant error message. -/
def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α :=
throwUnknownIdentifier m!"unknown constant '{.ofConstName constName}'"
/--
Throw an unknown constant error message.
The end position of the range of the current reference should point at the unknown identifier.
See also `mkUnknownIdentifierMessage`.
-/
def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α := do
throwUnknownConstantAt ( getRef) constName
/-- Throw an error exception using the given message data and reference syntax. -/
protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α := do
withRef ref <| Lean.throwError msg
/--
Convert an `Except` into a `m` monadic action, where `m` is any monad that

View File

@@ -750,7 +750,7 @@ def mkStrLit (s : String) : Expr :=
def mkAppN (f : Expr) (args : Array Expr) : Expr :=
args.foldl mkApp f
private def mkAppRangeAux (n : Nat) (args : Array Expr) (i : Nat) (e : Expr) : Expr :=
private partial def mkAppRangeAux (n : Nat) (args : Array Expr) (i : Nat) (e : Expr) : Expr :=
if i < n then mkAppRangeAux n args (i+1) (mkApp e args[i]!) else e
/-- `mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ]` ==> the expression `f a_i ... a_{j-1}` -/
@@ -1502,8 +1502,8 @@ abbrev PersistentExprStructMap (α : Type) := PHashMap ExprStructEq α
namespace Expr
private def mkAppRevRangeAux (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : Expr :=
if i start then b
private partial def mkAppRevRangeAux (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : Expr :=
if i == start then b
else
let i := i - 1
mkAppRevRangeAux revArgs start (mkApp b revArgs[i]!) i
@@ -1880,7 +1880,7 @@ def updateFn : Expr → Expr → Expr
/--
Eta reduction. If `e` is of the form `(fun x => f x)`, then return `f`.
-/
def eta (e : Expr) : Expr :=
partial def eta (e : Expr) : Expr :=
match e with
| Expr.lam _ d b _ =>
let b' := b.eta

View File

@@ -82,12 +82,6 @@ structure SnapshotTask (α : Type) where
`Syntax` processed by this `SnapshotTask`.
The `Syntax` is used by the language server to determine whether to force this `SnapshotTask`
when a request is made.
In general, the elaborator retains the following invariant:
If `stx?` is `none`, then this snapshot task (and all of its children) do not contain `InfoTree`
information that can be used in the language server, and so the language server will ignore it
when it is looking for an `InfoTree`.
Nonetheless, if `stx?` is `none`, then this snapshot task (and any of its children) may still
contain message log information.
-/
stx? : Option Syntax
/--
@@ -315,7 +309,7 @@ def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options)
/-- Waits on and returns all snapshots in the tree. -/
def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
Id.run <| s.foldM (pure <| ·.push ·) #[]
Id.run <| s.foldM (·.push ·) #[]
/-- Returns a task that waits on all snapshots in the tree. -/
def SnapshotTree.waitAll : SnapshotTree BaseIO (Task Unit)

View File

@@ -687,8 +687,7 @@ where
-- create a temporary snapshot tree containing all tasks but it
let snaps := #[
{ stx? := stx', task := elabPromise.result!.map (sync := true) toSnapshotTree, cancelTk? := none },
{ stx? := stx', task := resultPromise.result!.map (sync := true) toSnapshotTree, cancelTk? := none },
{ stx? := stx', task := finishedPromise.result!.map (sync := true) toSnapshotTree, cancelTk? := none }] ++
{ stx? := stx', task := resultPromise.result!.map (sync := true) toSnapshotTree, cancelTk? := none }] ++
cmdState.snapshotTasks
let tree := SnapshotTree.mk { diagnostics := .empty } snaps
BaseIO.bindTask ( tree.waitAll) fun _ => do

View File

@@ -295,10 +295,9 @@ private def isAlreadyNormalizedCheap : Level → Bool
/- Auxiliary function used at `normalize` -/
private def mkIMaxAux : Level Level Level
| _, zero => zero
| zero, u => u
| succ zero, u => u
| u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
| _, zero => zero
| zero, u => u
| u₁, u₂ => if u == u₂ then u₁ else mkLevelIMax u₁ u₂
/- Auxiliary function used at `normalize` -/
@[specialize] private partial def getMaxArgsAux (normalize : Level Level) : Level Bool Array Level Array Level

View File

@@ -397,19 +397,19 @@ instance : ForIn m LocalContext LocalDecl where
| some d => f d b
@[inline] def foldl (lctx : LocalContext) (f : β LocalDecl β) (init : β) (start : Nat := 0) : β :=
Id.run <| lctx.foldlM (pure <| f · ·) init start
Id.run <| lctx.foldlM f init start
@[inline] def foldr (lctx : LocalContext) (f : LocalDecl β β) (init : β) : β :=
Id.run <| lctx.foldrM (pure <| f · ·) init
Id.run <| lctx.foldrM f init
def size (lctx : LocalContext) : Nat :=
lctx.foldl (fun n _ => n+1) 0
@[inline] def findDecl? (lctx : LocalContext) (f : LocalDecl Option β) : Option β :=
Id.run <| lctx.findDeclM? (pure <| f ·)
Id.run <| lctx.findDeclM? f
@[inline] def findDeclRev? (lctx : LocalContext) (f : LocalDecl Option β) : Option β :=
Id.run <| lctx.findDeclRevM? (pure <| f ·)
Id.run <| lctx.findDeclRevM? f
partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVars : Array Expr) (i j : Nat) : Bool :=
if h : i < a₁.size then
@@ -473,11 +473,11 @@ def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
/-- Return `true` if `lctx` contains a local declaration satisfying `p`. -/
@[inline] def any (lctx : LocalContext) (p : LocalDecl Bool) : Bool :=
Id.run <| lctx.anyM (pure <| p ·)
Id.run <| lctx.anyM p
/-- Return `true` if all declarations in `lctx` satisfy `p`. -/
@[inline] def all (lctx : LocalContext) (p : LocalDecl Bool) : Bool :=
Id.run <| lctx.allM (pure <| p ·)
Id.run <| lctx.allM p
/-- If option `pp.sanitizeNames` is set to `true`, add tombstone to shadowed local declaration names and ones contains macroscopes. -/
def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext := do

View File

@@ -1221,7 +1221,7 @@ private def getConstTemp? (constName : Name) : MetaM (Option ConstantInfo) := do
| some (info@(ConstantInfo.thmInfo _)) => getTheoremInfo info
| some (info@(ConstantInfo.defnInfo _)) => getDefInfoTemp info
| some info => pure (some info)
| none => throwUnknownConstantAt ( getRef) constName
| none => throwUnknownConstant constName
private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do
if isClass ( getEnv) constName then

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