Compare commits

...

21 Commits

Author SHA1 Message Date
Leonardo de Moura
aa4ebd0fed fix: new code generator must generate code for opaque declarations that are not @[extern] 2024-12-14 11:59:22 -08:00
Leonardo de Moura
b5542b4c4f chore: align code with conventions 2024-12-14 11:40:22 -08:00
Leonardo de Moura
6571bc01d7 fix: withTrackingZetaDelta must reset cache (#6381)
This PR fixes a bug in `withTrackingZetaDelta` and
`withTrackingZetaDeltaSet`. The `MetaM` caches need to be reset. See new
test.
2024-12-14 18:23:32 +00:00
Kim Morrison
37122c3262 chore: move implementation details of mergeSort into namespace (#6380) 2024-12-14 11:24:15 +00:00
Mac Malone
280fcc9883 feat: lean --error=kind (#6362)
This PR adds the `--error=kind` option (shorthand: `-Ekind`) to the
`lean` CLI. When set, messages of `kind` (e.g.,
`linter.unusedVariables`) will be reported as errors. This setting does
nothing in interactive contexts (e.g., the server).

Closes #5194.

The spelling `--error` was chosen instead of the common `-Werror` both
for practical and behavioral reasons. Behaviorally, this option effects
not just warnings, but informational messages as well. Practically,
`-Werror` conflicts with the existing `-W` option for the worker and
`lean` also does not currently use long single-hyphen option names.
2024-12-14 01:31:14 +00:00
Leonardo de Moura
19eac5f341 fix: propagate Simp.Config when reducing terms and checking definitional equality in simp (#6123)
This PR ensures that the configuration in `Simp.Config` is used when
reducing terms and checking definitional equality in `simp`.

closes #5455

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
2024-12-14 00:59:40 +00:00
Cameron Zwarich
aa00725624 chore: stop running compiler twice during tests (#6321)
The reason given for this in the comment seemingly no longer holds.

Co-authored-by: Cameron Zwarich <cameron@lean-fro.org>
2024-12-13 23:59:20 +00:00
Cameron Zwarich
7530fd6955 chore: remove Lean.Compiler.LCNF.ForEachExpr (#6313)
Co-authored-by: Cameron Zwarich <cameron@lean-fro.org>
2024-12-13 23:58:42 +00:00
Alissa Tung
58ffd15a8f doc: fix typo reference in doc of lazy discrimination tree (#6377)
This PR fix a bad reference in doc of lazy discrimination tree.
2024-12-13 07:41:04 +00:00
Kim Morrison
bac34c7767 feat: theorems about == on Vector (#6376)
This PR adds theorems about `==` on `Vector`, reproducing those already
on `List` and `Array`.
2024-12-13 02:07:12 +00:00
Kim Morrison
db354d2cde chore: run Batteries linter on Lean (#6364)
This PR makes fixes suggested by the Batteries environment linters,
particularly `simpNF`, and `unusedHavesSuffices`.
2024-12-13 01:28:53 +00:00
Leonardo de Moura
945abe0065 fix: unused let_fun elimination in simp (#6375)
This PR fixes a bug in the simplifier. It was producing terms with loose
bound variables when eliminating unused `let_fun` expressions.

This issue was affecting the example at #6374. The example is now timing
out.
2024-12-13 01:18:46 +00:00
Kim Morrison
48be424eaa feat: lemmas about Vector.any/all/set (#6369)
This PR adds lemmas about `Vector.set`, `anyM`, `any`, `allM`, and
`all`.

With these additions, `Vector` is now as in-sync with the `List` API as
`Array` is, and in future I'll be updating both simultaneously.
2024-12-12 04:48:34 +00:00
Kyle Miller
58f8e21502 feat: labeled and unique sorries (#5757)
This PR makes it harder to create "fake" theorems about definitions that
are stubbed-out with `sorry` by ensuring that each `sorry` is not
definitionally equal to any other. For example, this now fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```
However, this still succeeds, since the `sorry` is a single
indeterminate `Nat`:
```lean
def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds
```
One can be more careful by putting parameters to the right of the colon:
```lean
def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails
```
Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on `sorry` in the Infoview, which brings you to its origin.
The option `set_option pp.sorrySource true` causes the pretty printer to
show source position information on sorries.

**Details:**

* Adds `Lean.Meta.mkLabeledSorry`, which creates a sorry that is labeled
with its source position. For example, `(sorry : Nat)` might elaborate
to
  ```
sorryAx (Lean.Name → Nat) false
`lean.foo.12.8.12.13.8.13._sorry._@.lean.foo._hyg.153
  ```
It can either be made unique (like the above) or merely labeled. Labeled
sorries use an encoding that does not impact defeq:
  ```
sorryAx (Unit → Nat) false (Function.const Lean.Name ()
`lean.foo.14.7.13.7.13.69._sorry._@.lean.foo._hyg.174)
  ```

* Makes the `sorry` term, the `sorry` tactic, and every elaboration
failure create labeled sorries. Most are unique sorries, but some
elaboration errors are labeled sorries.

* Renames `OmissionInfo` to `DelabTermInfo` and adds configuration
options to control LSP interactions. One field is a source position to
use for "go to definition". This is used to implement "go to definition"
on labeled sorries.

* Makes hovering over a labeled `sorry` show something friendlier than
that full `sorryAx` expression. Instead, the first hover shows the
simplified ``sorry `«lean.foo:48:11»``. Hovering over that hover shows
the full `sorryAx`. Setting `set_option pp.sorrySource true` makes
`sorry` always start with printing with this source position
information.

* Removes `Lean.Meta.mkSyntheticSorry` in favor of `Lean.Meta.mkSorry`
and `Lean.Meta.mkLabeledSorry`.

* Changes `sorryAx` so that the `synthetic` argument is no longer
optional.

* Gives `addPPExplicitToExposeDiff` awareness of labeled sorries. It can
set `pp.sorrySource` when source positions differ.

* Modifies the delaborator framework so that delaborators can set Info
themselves without it being overwritten.

Incidentally closes #4972.

Inspired by [this Zulip
thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Is.20a.20.60definition_wanted.60.20keyword.20possible.3F/near/477260277).
2024-12-11 23:53:02 +00:00
Mac Malone
a64a17e914 feat: Nat.shiftRight_bitwise_distrib (#6334)
This PR adds `Nat` theorems for distributing `>>>` over bitwise
operations, paralleling those of `BitVec`.

This enables closing goals like the following using `simp`:

```lean
example (n : Nat) : (n <<< 2 ||| 3) >>> 2 = n := by simp [Nat.shiftRight_or_distrib]
```

It might be nice for these theorems to be `simp` lemmas, but they are
not currently in order to be consistent with the existing `BitVec` and
`div_two` theorems.
2024-12-11 23:30:54 +00:00
Sebastian Ullrich
b862e2d251 chore: preserve reported messages in MessageLog (#6307)
Fixes #4460 (and similar future changes) making prior messages
inaccessible to metaprograms such as linters
2024-12-11 12:24:00 +00:00
Kim Morrison
8709ca35e9 chore: DecidableRel allows a heterogeneous relation (#6341)
This PR generalizes `DecidableRel` to allow a heterogeneous relation.
2024-12-11 05:02:58 +00:00
Mac Malone
19fb1fb388 feat: do not propagate pretty printer errors through messages (#3696)
This PR makes all message constructors handle pretty printer errors.

Prior to this change, pretty printer errors in messages were not
uniformly handled. In core, some printers capture their errors (e.g.,
`ppExprWithInfos` and `ppTerm` ) and some do not (e.g., `ppGoal` and
`ppSignature`) propagate them to whatever serializes the message (e.g.,
the frontend).

To resolve this inconsistency and uniformly handle errors, the signature
for `ofLazy` now uses `BaseIO`. As such, all printers been adapted to
capture any errors within them and print similar messages to
`ppExprWithInfos` and `ppTerm` on such errors.
2024-12-11 04:10:09 +00:00
Kim Morrison
cb31ddc6ad feat: lemmas about indexing and membership for Vector (#6367)
This PR brings Vector lemmas about membership and indexing to parity
with List and Array.
2024-12-11 03:52:04 +00:00
Leonardo de Moura
633c825ff3 feat: add Float32 support (#6366)
This PR adds support for `Float32` and fixes a bug in the runtime.
2024-12-11 02:55:58 +00:00
Kim Morrison
c83ce020bf feat: alignment of Array.set lemmas with List lemmas (#6365)
This PR expands the `Array.set` and `Array.setIfInBounds` lemmas to
match existing lemmas for `List.set`.
2024-12-11 01:45:06 +00:00
126 changed files with 3688 additions and 1041 deletions

View File

@@ -106,7 +106,7 @@ theorem seq_eq_bind_map {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α
theorem bind_congr [Bind m] {x : m α} {f g : α m β} (h : a, f a = g a) : x >>= f = x >>= g := by
simp [funext h]
@[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ) = x := by
theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ) = x := by
rw [bind_pure]
theorem map_congr [Functor m] {x : m α} {f g : α β} (h : a, f a = g a) : (f <$> x : m β) = g <$> x := by
@@ -133,7 +133,7 @@ theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y
rw [ bind_pure_comp]
simp only [bind_assoc, pure_bind]
@[simp] theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
simp [map]
/--

View File

@@ -150,7 +150,6 @@ theorem attach_map_coe (l : Array α) (f : α → β) :
theorem attach_map_val (l : Array α) (f : α β) : (l.attach.map fun i => f i.val) = l.map f :=
attach_map_coe _ _
@[simp]
theorem attach_map_subtype_val (l : Array α) : l.attach.map Subtype.val = l := by
cases l; simp
@@ -162,7 +161,6 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : Array α) (H :
((l.attachWith p H).map fun i => f i.val) = l.map f :=
attachWith_map_coe _ _ _
@[simp]
theorem attachWith_map_subtype_val {p : α Prop} (l : Array α) (H : a l, p a) :
(l.attachWith p H).map Subtype.val = l := by
cases l; simp
@@ -204,8 +202,8 @@ theorem pmap_ne_empty_iff {P : α → Prop} (f : (a : α) → P a → β) {xs :
(H : (a : α), a xs P a) : xs.pmap f H #[] xs #[] := by
cases xs; simp
theorem pmap_eq_self {l : Array α} {p : α Prop} (hp : (a : α), a l p a)
(f : (a : α) p a α) : l.pmap f hp = l a (h : a l), f a (hp a h) = a := by
theorem pmap_eq_self {l : Array α} {p : α Prop} {hp : (a : α), a l p a}
{f : (a : α) p a α} : l.pmap f hp = l a (h : a l), f a (hp a h) = a := by
cases l; simp [List.pmap_eq_self]
@[simp]

View File

@@ -79,7 +79,8 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl
-- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
theorem toList_toArray (as : List α) : as.toArray.toList = as := rfl
@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
@@ -208,7 +209,7 @@ instance : EmptyCollection (Array α) := ⟨Array.empty⟩
instance : Inhabited (Array α) where
default := Array.empty
@[simp] def isEmpty (a : Array α) : Bool :=
def isEmpty (a : Array α) : Bool :=
a.size = 0
@[specialize]
@@ -662,9 +663,15 @@ def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
def all (as : Array α) (p : α Bool) (start := 0) (stop := as.size) : Bool :=
Id.run <| as.allM p start stop
/-- `as.contains a` is true if there is some element `b` in `as` such that `a == b`. -/
def contains [BEq α] (as : Array α) (a : α) : Bool :=
as.any (a == ·)
/--
Variant of `Array.contains` with arguments reversed.
For verification purposes, we simplify this to `contains`.
-/
def elem [BEq α] (a : α) (as : Array α) : Bool :=
as.contains a
@@ -814,7 +821,7 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
induction a, i, h using Array.eraseIdx.induct with
| @case1 a i h h' a' ih =>
unfold eraseIdx
simp [h', a', ih]
simp +zetaDelta [h', a', ih]
| case2 a i h h' =>
unfold eraseIdx
simp [h']

View File

@@ -32,10 +32,8 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra
have := Array.of_push_eq_push ih₂
simp [this]
@[simp] theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
apply propext; apply Iff.intro
· intro h; simpa [toArray] using h
· intro h; rw [h]
theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
simp
def Array.mapM' [Monad m] (f : α m β) (as : Array α) : m { bs : Array β // bs.size = as.size } :=
go 0 mkEmpty as.size, rfl (by simp)

View File

@@ -93,11 +93,14 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
@[simp] theorem appendList_eq_append
(arr : Array α) (l : List α) : arr.appendList l = arr ++ l := rfl
@[simp] theorem appendList_toList (arr : Array α) (l : List α) :
@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
(arr ++ l).toList = arr.toList ++ l := by
rw [ appendList_eq_append]; unfold Array.appendList
induction l generalizing arr <;> simp [*]
@[deprecated toList_appendList (since := "2024-12-11")]
abbrev appendList_toList := @toList_appendList
@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
theorem foldrM_eq_foldrM_toList [Monad m]
(f : α β m β) (init : β) (arr : Array α) :
@@ -149,7 +152,7 @@ abbrev pop_data := @pop_toList
@[deprecated toList_append (since := "2024-09-09")]
abbrev append_data := @toList_append
@[deprecated appendList_toList (since := "2024-09-09")]
abbrev appendList_data := @appendList_toList
@[deprecated toList_appendList (since := "2024-09-09")]
abbrev appendList_data := @toList_appendList
end Array

View File

@@ -42,7 +42,7 @@ theorem rel_of_isEqv {r : αα → Bool} {a b : Array α} :
· exact fun h' => h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'
· intro; contradiction
theorem isEqv_iff_rel (a b : Array α) (r) :
theorem isEqv_iff_rel {a b : Array α} {r} :
Array.isEqv a b r h : a.size = b.size, (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h h')) :=
rel_of_isEqv, fun h, w => by
simp only [isEqv, h, reduceDIte]

View File

@@ -99,7 +99,7 @@ theorem back?_flatten {L : Array (Array α)} :
simp [List.getLast?_flatten, List.map_reverse, List.findSome?_map, Function.comp_def]
theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
simp [mkArray_eq_toArray_replicate, List.findSome?_replicate]
simp [ List.toArray_replicate, List.findSome?_replicate]
@[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by
simp [findSome?_mkArray, Nat.ne_of_gt h]
@@ -246,7 +246,7 @@ theorem find?_flatMap_eq_none {xs : Array α} {f : α → Array β} {p : β →
theorem find?_mkArray :
find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
simp [mkArray_eq_toArray_replicate, List.find?_replicate]
simp [ List.toArray_replicate, List.find?_replicate]
@[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) :
find? p (mkArray n a) = if p a then some a else none := by
@@ -262,15 +262,15 @@ theorem find?_mkArray :
-- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α Bool} :
(mkArray n a).find? p = none n = 0 !p a := by
simp [mkArray_eq_toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
simp [ List.toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
@[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α Bool} :
(mkArray n a).find? p = some b n 0 p a a = b := by
simp [mkArray_eq_toArray_replicate]
simp [ List.toArray_replicate]
@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α Bool) (h) :
((mkArray n a).find? p).get h = a := by
simp [mkArray_eq_toArray_replicate]
simp [ List.toArray_replicate]
theorem find?_pmap {P : α Prop} (f : (a : α) P a β) (xs : Array α)
(H : (a : α), a xs P a) (p : β Bool) :

View File

@@ -19,16 +19,14 @@ import Init.Data.List.ToArray
## Theorems about `Array`.
-/
namespace Array
/-! ## Preliminaries -/
/-! ### toList -/
theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by
cases a; cases b; simpa using h
theorem toList_inj {a b : Array α} : a.toList = b.toList a = b := by
cases a; cases b; simp
@[simp] theorem toList_eq_nil_iff (l : Array α) : l.toList = [] l = #[] := by
cases l <;> simp
@@ -55,7 +53,7 @@ theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[] := by
cases l
simpa using List.ne_nil_of_length_pos h
@[simp] theorem size_eq_zero : l.size = 0 l = #[] :=
theorem size_eq_zero : l.size = 0 l = #[] :=
eq_empty_of_size_eq_zero, fun h => h rfl
theorem size_pos_of_mem {a : α} {l : Array α} (h : a l) : 0 < l.size := by
@@ -145,6 +143,34 @@ theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
(ys : Array α) (a : α), xs = ys.push a :=
exists_push_of_size_pos (by simp [h])
theorem singleton_inj : #[a] = #[b] a = b := by
simp
/-! ### mkArray -/
@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
List.length_replicate ..
@[simp] theorem toList_mkArray : (mkArray n a).toList = List.replicate n a := by
simp only [mkArray]
@[simp] theorem mkArray_zero : mkArray 0 a = #[] := rfl
theorem mkArray_succ : mkArray (n + 1) a = (mkArray n a).push a := by
apply toList_inj.1
simp [List.replicate_succ']
theorem mkArray_inj : mkArray n a = mkArray m b n = m (n = 0 a = b) := by
rw [ List.replicate_inj, toList_inj]
simp
@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
(mkArray n v)[i] = v := by simp [ getElem_toList]
theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
(mkArray n v)[i]? = if i < n then some v else none := by
simp [getElem?_def]
/-! ## L[i] and L[i]? -/
@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none a.size i := by
@@ -176,7 +202,7 @@ theorem some_eq_getElem?_iff {a : Array α} : some b = a[i]? ↔ ∃ h : i < a.s
(a[i]? = some a[i]) True := by
simp [h]
theorem getElem_eq_iff {a : Array α} {n : Nat} {h : n < a.size} : a[n] = x a[n]? = some x := by
theorem getElem_eq_iff {a : Array α} {i : Nat} {h : i < a.size} : a[i] = x a[i]? = some x := by
simp only [getElem?_eq_some_iff]
exact fun w => h, w, fun h => h.2
@@ -184,7 +210,15 @@ theorem getElem_eq_getElem?_get (a : Array α) (i : Nat) (h : i < a.size) :
a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h]) := by
simp [getElem_eq_iff]
@[simp] theorem getElem?_empty {n : Nat} : (#[] : Array α)[n]? = none := rfl
theorem getD_getElem? (a : Array α) (i : Nat) (d : α) :
a[i]?.getD d = if p : i < a.size then a[i]'p else d := by
if h : i < a.size then
simp [h, getElem?_def]
else
have p : i a.size := Nat.le_of_not_gt h
simp [getElem?_eq_none p, h]
@[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl
theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
@@ -218,7 +252,7 @@ theorem getElem?_singleton (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a
/-! ### mem -/
@[simp] theorem not_mem_empty (a : α) : ¬ a #[] := nofun
theorem not_mem_empty (a : α) : ¬ a #[] := by simp
@[simp] theorem mem_push {a : Array α} {x y : α} : x a.push y x a x = y := by
simp only [mem_def]
@@ -245,19 +279,19 @@ theorem eq_empty_iff_forall_not_mem {l : Array α} : l = #[] ↔ ∀ a, a ∉ l
cases l
simp [List.eq_nil_iff_forall_not_mem]
@[simp] theorem mem_dite_nil_left {x : α} [Decidable p] {l : ¬ p Array α} :
@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p Array α} :
(x if h : p then #[] else l h) h : ¬ p, x l h := by
split <;> simp_all
@[simp] theorem mem_dite_nil_right {x : α} [Decidable p] {l : p Array α} :
@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p Array α} :
(x if h : p then l h else #[]) h : p, x l h := by
split <;> simp_all
@[simp] theorem mem_ite_nil_left {x : α} [Decidable p] {l : Array α} :
@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
(x if p then #[] else l) ¬ p x l := by
split <;> simp_all
@[simp] theorem mem_ite_nil_right {x : α} [Decidable p] {l : Array α} :
@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
(x if p then l else #[]) p x l := by
split <;> simp_all
@@ -284,7 +318,7 @@ theorem forall_mem_empty (p : α → Prop) : ∀ (x) (_ : x ∈ #[]), p x := nof
theorem exists_mem_push {p : α Prop} {a : α} {xs : Array α} :
( x, _ : x xs.push a, p x) p a x, _ : x xs, p x := by
simp
simp only [mem_push, exists_prop]
constructor
· rintro x, (h | rfl), h'
· exact .inr x, h, h'
@@ -313,7 +347,7 @@ theorem eq_or_ne_mem_of_mem {a b : α} {l : Array α} (h' : a ∈ l.push b) :
if h : a = b then
exact .inl h
else
simp [h] at h'
simp only [mem_push, h, or_false] at h'
exact .inr h, h'
theorem ne_empty_of_mem {a : α} {l : Array α} (h : a l) : l #[] := by
@@ -337,27 +371,27 @@ theorem not_mem_push_of_ne_of_not_mem {a y : α} {l : Array α} : a ≠ y → a
theorem ne_and_not_mem_of_not_mem_push {a y : α} {l : Array α} : a l.push y a y a l := by
simp +contextual
theorem getElem_of_mem {a} {l : Array α} (h : a l) : (n : Nat) (h : n < l.size), l[n]'h = a := by
theorem getElem_of_mem {a} {l : Array α} (h : a l) : (i : Nat) (h : i < l.size), l[i]'h = a := by
cases l
simp [List.getElem_of_mem (by simpa using h)]
theorem getElem?_of_mem {a} {l : Array α} (h : a l) : n : Nat, l[n]? = some a :=
theorem getElem?_of_mem {a} {l : Array α} (h : a l) : i : Nat, l[i]? = some a :=
let n, _, e := getElem_of_mem h; n, e getElem?_eq_getElem _
theorem mem_of_getElem? {l : Array α} {n : Nat} {a : α} (e : l[n]? = some a) : a l :=
theorem mem_of_getElem? {l : Array α} {i : Nat} {a : α} (e : l[i]? = some a) : a l :=
let _, e := getElem?_eq_some_iff.1 e; e getElem_mem ..
theorem mem_iff_getElem {a} {l : Array α} : a l (n : Nat) (h : n < l.size), l[n]'h = a :=
theorem mem_iff_getElem {a} {l : Array α} : a l (i : Nat) (h : i < l.size), l[i]'h = a :=
getElem_of_mem, fun _, _, e => e getElem_mem ..
theorem mem_iff_getElem? {a} {l : Array α} : a l n : Nat, l[n]? = some a := by
theorem mem_iff_getElem? {a} {l : Array α} : a l i : Nat, l[i]? = some a := by
simp [getElem?_eq_some_iff, mem_iff_getElem]
theorem forall_getElem {l : Array α} {p : α Prop} :
( (n : Nat) h, p (l[n]'h)) a, a l p a := by
( (i : Nat) h, p (l[i]'h)) a, a l p a := by
cases l; simp [List.forall_getElem]
/-! ### isEmpty-/
/-! ### isEmpty -/
@[simp] theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty := by
rcases l with _ | _ <;> simp
@@ -477,7 +511,7 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
rw [Bool.eq_false_iff, Ne, any_eq_true]
simp
theorem any_toList {p : α Bool} (as : Array α) : as.toList.any p = as.any p := by
@[simp] theorem any_toList {p : α Bool} (as : Array α) : as.toList.any p = as.any p := by
rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]
simp only [List.mem_iff_getElem, getElem_toList]
exact fun _, i, w, rfl, h => i, w, h, fun i, w, h => _, i, w, rfl, h
@@ -516,7 +550,7 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
rw [Bool.eq_false_iff, Ne, all_eq_true]
simp
theorem all_toList {p : α Bool} (as : Array α) : as.toList.all p = as.all p := by
@[simp] theorem all_toList {p : α Bool} (as : Array α) : as.toList.all p = as.all p := by
rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]
simp only [List.mem_iff_getElem, getElem_toList]
constructor
@@ -528,20 +562,6 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p x, x l p x := by
simp only [ all_toList, List.all_eq_true, mem_def]
theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α m Bool) (l : List α) :
l.toArray.anyM p = l.anyM p := by
rw [ anyM_toList]
theorem _root_.List.any_toArray (p : α Bool) (l : List α) : l.toArray.any p = l.any p := by
rw [any_toList]
theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α m Bool) (l : List α) :
l.toArray.allM p = l.allM p := by
rw [ allM_toList]
theorem _root_.List.all_toArray (p : α Bool) (l : List α) : l.toArray.all p = l.all p := by
rw [all_toList]
/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
@[simp] theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] (p : α m Bool) (l : List α)
(h : stop = l.toArray.size) :
@@ -568,6 +588,20 @@ theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all
subst h
rw [all_toList]
theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α m Bool) (l : List α) :
l.toArray.anyM p = l.anyM p := by
rw [ anyM_toList]
theorem _root_.List.any_toArray (p : α Bool) (l : List α) : l.toArray.any p = l.any p := by
rw [any_toList]
theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α m Bool) (l : List α) :
l.toArray.allM p = l.allM p := by
rw [ allM_toList]
theorem _root_.List.all_toArray (p : α Bool) (l : List α) : l.toArray.all p = l.all p := by
rw [all_toList]
/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
theorem any_eq_true' {p : α Bool} {as : Array α} :
as.any p = true ( x, x as p x) := by
@@ -635,7 +669,7 @@ theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
l.toArray.contains a = l.contains a := by
simp [Array.contains, List.any_beq]
@[simp] theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
Array.elem a l.toArray = List.elem a l := by
simp [Array.elem]
@@ -657,26 +691,32 @@ theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
(xs.all fun x => x != a) = !xs.contains a := by
simp only [bne_comm, all_bne]
theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : elem a as = true a as := by
theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : as.contains a = true a as := by
cases as
simp
theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a as) : elem a as = true := by
@[deprecated mem_of_contains_eq_true (since := "2024-12-12")]
abbrev mem_of_elem_eq_true := @mem_of_contains_eq_true
theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a as) : as.contains a = true := by
cases as
simpa using h
@[deprecated contains_eq_true_of_mem (since := "2024-12-12")]
abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a as) :=
decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
decidable_of_decidable_of_iff (Iff.intro mem_of_contains_eq_true contains_eq_true_of_mem)
@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : Array α} :
elem a l = l.contains a := by
simp [elem]
theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
elem a as = true a as := mem_of_elem_eq_true, elem_eq_true_of_mem
elem a as = true a as := mem_of_contains_eq_true, contains_eq_true_of_mem
theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
as.contains a = true a as := mem_of_elem_eq_true, elem_eq_true_of_mem
as.contains a = true a as := mem_of_contains_eq_true, contains_eq_true_of_mem
theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
elem a as = decide (a as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
@@ -710,8 +750,231 @@ theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
(l.push a).contains b = (l.contains b || b == a) := by
simp [contains]
theorem singleton_inj : #[a] = #[b] a = b := by
/-! ### set -/
@[simp] theorem getElem_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
(eq : i = j) (p : j < (a.set i v).size) :
(a.set i v)[j]'p = v := by
cases a
simp
simp [set, getElem_toList, eq]
@[deprecated getElem_set_self (since := "2024-12-11")]
abbrev getElem_set_eq := @getElem_set_self
@[simp] theorem getElem?_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
(a.set i v)[i]? = v := by simp [getElem?_eq_getElem, h]
@[deprecated getElem?_set_self (since := "2024-12-11")]
abbrev getElem?_set_eq := @getElem?_set_self
@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
(pj : j < (a.set i v).size) (h : i j) :
(a.set i v)[j]'pj = a[j]'(size_set a i v _ pj) := by
simp only [set, getElem_toList, List.getElem_set_ne h]
@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
(ne : i j) : (a.set i v)[j]? = a[j]? := by
by_cases h : j < a.size <;> simp [getElem?_eq_getElem, getElem?_eq_none, Nat.ge_of_not_lt, ne, h]
theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
(h : j < (a.set i v).size) :
(a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ h) := by
by_cases p : i = j <;> simp [p]
theorem getElem?_set (a : Array α) (i : Nat) (h : i < a.size) (v : α) (j : Nat) :
(a.set i v)[j]? = if i = j then some v else a[j]? := by
split <;> simp_all
@[simp] theorem set_getElem_self {as : Array α} {i : Nat} (h : i < as.size) :
as.set i as[i] = as := by
cases as
simp
@[simp] theorem set_eq_empty_iff {as : Array α} (n : Nat) (a : α) (h) :
as.set n a = #[] as = #[] := by
cases as <;> cases n <;> simp [set]
theorem set_comm (a b : α)
{i j : Nat} (as : Array α) {hi : i < as.size} {hj : j < (as.set i a).size} (h : i j) :
(as.set i a).set j b = (as.set j b (by simpa using hj)).set i a (by simpa using hi) := by
cases as
simp [List.set_comm _ _ _ h]
@[simp]
theorem set_set (a b : α) (as : Array α) (i : Nat) (h : i < as.size) :
(as.set i a).set i b (by simpa using h) = as.set i b := by
cases as
simp
theorem mem_set (as : Array α) (i : Nat) (h : i < as.size) (a : α) :
a as.set i a := by
simp [mem_iff_getElem]
exact i, (by simpa using h), by simp
theorem mem_or_eq_of_mem_set
{as : Array α} {i : Nat} {a b : α} {w : i < as.size} (h : a as.set i b) : a as a = b := by
cases as
simpa using List.mem_or_eq_of_mem_set (by simpa using h)
@[simp] theorem toList_set (a : Array α) (i x h) :
(a.set i x).toList = a.toList.set i x := rfl
/-! ### setIfInBounds -/
@[simp] theorem set!_eq_setIfInBounds : @set! = @setIfInBounds := rfl
@[deprecated set!_eq_setIfInBounds (since := "2024-12-12")]
abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds
@[simp] theorem size_setIfInBounds (as : Array α) (index : Nat) (val : α) :
(as.setIfInBounds index val).size = as.size := by
if h : index < as.size then
simp [setIfInBounds, h]
else
simp [setIfInBounds, h]
theorem getElem_setIfInBounds (as : Array α) (i : Nat) (v : α) (j : Nat)
(hj : j < (as.setIfInBounds i v).size) :
(as.setIfInBounds i v)[j]'hj = if i = j then v else as[j]'(by simpa using hj) := by
simp only [setIfInBounds]
split
· simp [getElem_set]
· simp only [size_setIfInBounds] at hj
rw [if_neg]
omega
@[simp] theorem getElem_setIfInBounds_self (as : Array α) {i : Nat} (v : α) (h : _) :
(as.setIfInBounds i v)[i]'h = v := by
simp at h
simp only [setIfInBounds, h, reduceDIte, getElem_set_self]
@[deprecated getElem_setIfInBounds_self (since := "2024-12-11")]
abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
@[simp] theorem getElem_setIfInBounds_ne (as : Array α) {i : Nat} (v : α) {j : Nat}
(hj : j < (as.setIfInBounds i v).size) (h : i j) :
(as.setIfInBounds i v)[j]'hj = as[j]'(by simpa using hj) := by
simp [getElem_setIfInBounds, h]
theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α} :
(as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
cases as
simp [List.getElem?_set]
theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (v : α) :
(as.setIfInBounds i v)[i]? = if i < as.size then some v else none := by
simp [getElem?_setIfInBounds]
@[simp]
theorem getElem?_setIfInBounds_self_of_lt (as : Array α) {i : Nat} (v : α) (h : i < as.size) :
(as.setIfInBounds i v)[i]? = some v := by
simp [getElem?_setIfInBounds, h]
@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
@[simp] theorem getElem?_setIfInBounds_ne {as : Array α} {i j : Nat} (h : i j) {a : α} :
(as.setIfInBounds i a)[j]? = as[j]? := by
simp [getElem?_setIfInBounds, h]
theorem setIfInBounds_eq_of_size_le {l : Array α} {n : Nat} (h : l.size n) {a : α} :
l.setIfInBounds n a = l := by
cases l
simp [List.set_eq_of_length_le (by simpa using h)]
@[simp] theorem setIfInBounds_eq_empty_iff {as : Array α} (n : Nat) (a : α) :
as.setIfInBounds n a = #[] as = #[] := by
cases as <;> cases n <;> simp
theorem setIfInBounds_comm (a b : α)
{i j : Nat} (as : Array α) (h : i j) :
(as.setIfInBounds i a).setIfInBounds j b = (as.setIfInBounds j b).setIfInBounds i a := by
cases as
simp [List.set_comm _ _ _ h]
@[simp]
theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (i : Nat) :
(as.setIfInBounds i a).setIfInBounds i b = as.setIfInBounds i b := by
cases as
simp
theorem mem_setIfInBounds (as : Array α) (i : Nat) (h : i < as.size) (a : α) :
a as.setIfInBounds i a := by
simp [mem_iff_getElem]
exact i, (by simpa using h), by simp
theorem mem_or_eq_of_mem_setIfInBounds
{as : Array α} {i : Nat} {a b : α} (h : a as.setIfInBounds i b) : a as a = b := by
cases as
simpa using List.mem_or_eq_of_mem_set (by simpa using h)
/-- Simplifies a normal form from `get!` -/
@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
(setIfInBounds a i v)[i]?.getD d = if i < a.size then v else d := by
by_cases h : i < a.size <;>
simp [setIfInBounds, Nat.not_lt_of_le, h, getD_getElem?]
@[simp] theorem toList_setIfInBounds (a : Array α) (i x) :
(a.setIfInBounds i x).toList = a.toList.set i x := by
simp only [setIfInBounds]
split <;> rename_i h
· simp
· simp [List.set_eq_of_length_le (by simpa using h)]
/-! ### BEq -/
@[simp] theorem push_beq_push [BEq α] {a b : α} {v : Array α} {w : Array α} :
(v.push a == w.push b) = (v == w && a == b) := by
cases v
cases w
simp
@[simp] theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} :
(mkArray n a == mkArray n b) = (n == 0 || a == b) := by
cases n with
| zero => simp
| succ n =>
rw [mkArray_succ, mkArray_succ, push_beq_push, mkArray_beq_mkArray]
rw [Bool.eq_iff_iff]
simp +contextual
@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ReflBEq α := by
constructor
· intro h
constructor
intro a
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
apply Array.isEqv_self_beq
@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) LawfulBEq α := by
constructor
· intro h
constructor
· intro a b h
apply singleton_inj.1
apply eq_of_beq
simp only [instBEq, isEqv, isEqvAux]
simpa
· intro a
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
· intro a b h
obtain hs, hi := rel_of_isEqv h
ext i h₁ h₂
· exact hs
· simpa using hi _ h₁
· intro a
apply Array.isEqv_self_beq
/-! Content below this point has not yet been aligned with `List`. -/
theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
@@ -726,8 +989,8 @@ theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
@[simp] theorem mkEmpty_eq (α n) : @mkEmpty α n = #[] := rfl
@[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
@[deprecated size_toArray (since := "2024-12-11")]
theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
theorem foldrM_push [Monad m] (f : α β m β) (init : β) (arr : Array α) (a : α) :
(arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
@@ -796,11 +1059,6 @@ where
@[simp] theorem appendList_cons (arr : Array α) (a : α) (l : List α) :
arr ++ (a :: l) = arr.push a ++ l := Array.ext' (by simp)
@[simp] theorem toList_appendList (arr : Array α) (l : List α) :
(arr ++ l).toList = arr.toList ++ l := by
cases arr
simp
theorem foldl_toList_eq_flatMap (l : List α) (acc : Array β)
(F : Array β α Array β) (G : α List β)
(H : acc a, (F acc a).toList = acc.toList ++ G a) :
@@ -820,102 +1078,31 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
/-! # get -/
@[deprecated getElem?_eq_getElem (since := "2024-12-11")]
theorem getElem?_lt
(a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
@[deprecated getElem?_eq_none (since := "2024-12-11")]
theorem getElem?_ge
(a : Array α) {i : Nat} (h : i a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
@[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
@[deprecated getElem?_eq_none (since := "2024-12-11")]
theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size i) : a[i]? = none := by
simp [getElem?_ge, h]
simp [getElem?_eq_none, h]
theorem getD_get? (a : Array α) (i : Nat) (d : α) :
Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
if h : i < a.size then
simp [setIfInBounds, h, getElem?_def]
else
have p : i a.size := Nat.le_of_not_gt h
simp [setIfInBounds, getElem?_len_le _ p, h]
@[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
@[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
@[simp] theorem getD_eq_get? (a : Array α) (i d) : a.getD i d = (a[i]?).getD d := by
simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_getElem?, *]
theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
a.get! i = (a.get? i).getD default := by
by_cases p : i < a.size <;>
simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
/-! # set -/
@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
(eq : i = j) (p : j < (a.set i v).size) :
(a.set i v)[j]'p = v := by
cases a
simp
simp [set, getElem_toList, eq]
@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
(pj : j < (a.set i v).size) (h : i j) :
(a.set i v)[j]'pj = a[j]'(size_set a i v _ pj) := by
simp only [set, getElem_toList, List.getElem_set_ne h]
theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
(h : j < (a.set i v).size) :
(a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ h) := by
by_cases p : i = j <;> simp [p]
@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
(a.set i v)[i]? = v := by simp [getElem?_lt, h]
@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
(ne : i j) : (a.set i v)[j]? = a[j]? := by
by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
/-! # setIfInBounds -/
@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
@[simp] theorem size_setIfInBounds (a : Array α) (index : Nat) (val : α) :
(Array.setIfInBounds a index val).size = a.size := by
if h : index < a.size then
simp [setIfInBounds, h]
else
simp [setIfInBounds, h]
theorem getElem_setIfInBounds (a : Array α) (i : Nat) (v : α) (j : Nat)
(hj : j < (setIfInBounds a i v).size) :
(setIfInBounds a i v)[j]'hj = if i = j then v else a[j]'(by simpa using hj) := by
simp only [setIfInBounds]
split
· simp [getElem_set]
· simp only [size_setIfInBounds] at hj
rw [if_neg]
omega
@[simp] theorem getElem_setIfInBounds_eq (a : Array α) {i : Nat} (v : α) (h : _) :
(setIfInBounds a i v)[i]'h = v := by
simp at h
simp only [setIfInBounds, h, reduceDIte, getElem_set_eq]
@[simp] theorem getElem_setIfInBounds_ne (a : Array α) {i : Nat} (v : α) {j : Nat}
(hj : j < (setIfInBounds a i v).size) (h : i j) :
(setIfInBounds a i v)[j]'hj = a[j]'(by simpa using hj) := by
simp [getElem_setIfInBounds, h]
@[simp]
theorem getElem?_setIfInBounds_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) :
(a.setIfInBounds i v)[i]? = some v := by
simp [getElem?_lt, p]
/-- Simplifies a normal form from `get!` -/
@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
Option.getD (setIfInBounds a i v)[i]? d = if i < a.size then v else d := by
by_cases h : i < a.size <;>
simp [setIfInBounds, Nat.not_lt_of_le, h, getD_get?]
simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?]
/-! # ofFn -/
@@ -973,44 +1160,12 @@ theorem ofFn_succ (f : Fin (n+1) → α) :
simp at h₁ h₂
omega
/-! # mkArray -/
@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
List.length_replicate ..
@[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
theorem mkArray_eq_toArray_replicate (n : Nat) (v : α) : mkArray n v = (List.replicate n v).toArray := rfl
@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
(mkArray n v)[i] = v := by simp [ getElem_toList]
theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
(mkArray n v)[i]? = if i < n then some v else none := by
simp [getElem?_def]
/-! # mem -/
@[simp] theorem mem_toList {a : α} {l : Array α} : a l.toList a l := mem_def.symm
theorem not_mem_nil (a : α) : ¬ a #[] := nofun
@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p Array α} :
(x if h : p then #[] else l h) h : ¬ p, x l h := by
split <;> simp_all
@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p Array α} :
(x if h : p then l h else #[]) h : p, x l h := by
split <;> simp_all
@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Array α} :
(x if p then #[] else l) ¬ p x l := by
split <;> simp_all
@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Array α} :
(x if p then l else #[]) p x l := by
split <;> simp_all
/-! # get lemmas -/
theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} (_ : a[idx] = x) :
@@ -1067,8 +1222,6 @@ theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x
@[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
@[simp] theorem toList_set (a : Array α) (i v h) : (a.set i v).toList = a.toList.set i v := rfl
theorem get_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
(a.set i v h)[i]'(by simp [h]) = v := by
simp only [set, getElem_toList, List.getElem_set_self]
@@ -1092,9 +1245,6 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
(h : i j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
simp only [set, getElem_toList, List.getElem_set_ne h]
theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
(a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
private theorem fin_cast_val (e : n = n') (i : Fin n) : e i = i.1, e i.2 := by cases e; rfl
theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
@@ -1111,8 +1261,8 @@ theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j
@[simp] theorem swapAt_def (a : Array α) (i : Nat) (v : α) (hi) :
a.swapAt i v hi = (a[i], a.set i v) := rfl
@[simp] theorem size_swapAt (a : Array α) (i : Nat) (v : α) (hi) :
(a.swapAt i v hi).2.size = a.size := by simp [swapAt_def]
theorem size_swapAt (a : Array α) (i : Nat) (v : α) (hi) :
(a.swapAt i v hi).2.size = a.size := by simp
@[simp]
theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
@@ -1221,43 +1371,6 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
true_and, Nat.not_lt] at h
rw [List.getElem?_eq_none_iff.2 _, List.getElem?_eq_none_iff.2 (a.toList.length_reverse _)]
/-! ### BEq -/
@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ReflBEq α := by
constructor
· intro h
constructor
intro a
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
apply Array.isEqv_self_beq
@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) LawfulBEq α := by
constructor
· intro h
constructor
· intro a b h
apply singleton_inj.1
apply eq_of_beq
simp only [instBEq, isEqv, isEqvAux]
simpa
· intro a
suffices (#[a] == #[a]) = true by
simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
simp
· intro h
constructor
· intro a b h
obtain hs, hi := rel_of_isEqv h
ext i h₁ h₂
· exact hs
· simpa using hi _ h₁
· intro a
apply Array.isEqv_self_beq
/-! ### take -/
@[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by
@@ -1606,13 +1719,9 @@ theorem mem_append_right {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈
@[simp] theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := by
simp only [size, toList_append, List.length_append]
@[simp] theorem empty_append (as : Array α) : #[] ++ as = as := by
cases as
simp
theorem empty_append (as : Array α) : #[] ++ as = as := by simp
@[simp] theorem append_empty (as : Array α) : as ++ #[] = as := by
cases as
simp
theorem append_empty (as : Array α) : as ++ #[] = as := by simp
theorem getElem_append {as bs : Array α} (h : i < (as ++ bs).size) :
(as ++ bs)[i] = if h' : i < as.size then as[i] else bs[i - as.size]'(by simp at h; omega) := by
@@ -1634,21 +1743,21 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
conv => rhs; rw [ List.getElem_append_right (h₁ := hle) (h₂ := h')]
apply List.get_of_eq; rw [toList_append]
theorem getElem?_append_left {as bs : Array α} {n : Nat} (hn : n < as.size) :
(as ++ bs)[n]? = as[n]? := by
have hn' : n < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
(as ++ bs)[i]? = as[i]? := by
have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
size_append .. Nat.le_add_right ..
simp_all [getElem?_eq_getElem, getElem_append]
theorem getElem?_append_right {as bs : Array α} {n : Nat} (h : as.size n) :
(as ++ bs)[n]? = bs[n - as.size]? := by
theorem getElem?_append_right {as bs : Array α} {i : Nat} (h : as.size i) :
(as ++ bs)[i]? = bs[i - as.size]? := by
cases as
cases bs
simp at h
simp [List.getElem?_append_right, h]
theorem getElem?_append {as bs : Array α} {n : Nat} :
(as ++ bs)[n]? = if n < as.size then as[n]? else bs[n - as.size]? := by
theorem getElem?_append {as bs : Array α} {i : Nat} :
(as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]? := by
split <;> rename_i h
· exact getElem?_append_left h
· exact getElem?_append_right (by simpa using h)
@@ -1968,8 +2077,7 @@ namespace List
Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
-/
@[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
simp
theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by simp
@[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by
apply ext'
@@ -1993,18 +2101,8 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
apply ext'
simp
@[simp] theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) :
l.toArray.uset i a h = (l.set i.toNat a).toArray := by
apply ext'
simp
@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
l.toArray.setIfInBounds i a = (l.set i a).toArray := by
apply ext'
simp only [setIfInBounds]
split
· simp
· simp_all [List.set_eq_of_length_le]
theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) :
l.toArray.uset i a h = (l.set i.toNat a).toArray := by simp
@[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
@@ -2040,7 +2138,8 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
l.toArray.filterMap f = (l.filterMap f).toArray := by
simp
@[simp] theorem flatten_toArray (l : List (List α)) : (l.toArray.map List.toArray).flatten = l.flatten.toArray := by
@[simp] theorem flatten_toArray (l : List (List α)) :
(l.toArray.map List.toArray).flatten = l.flatten.toArray := by
apply ext'
simp [Function.comp_def]
@@ -2248,19 +2347,15 @@ end List
namespace Array
@[simp] theorem toList_fst_unzip (as : Array (α × β)) :
as.unzip.1.toList = as.toList.unzip.1 := by
cases as
simp
theorem toList_fst_unzip (as : Array (α × β)) :
as.unzip.1.toList = as.toList.unzip.1 := by simp
@[simp] theorem toList_snd_unzip (as : Array (α × β)) :
as.unzip.2.toList = as.toList.unzip.2 := by
cases as
simp
theorem toList_snd_unzip (as : Array (α × β)) :
as.unzip.2.toList = as.toList.unzip.2 := by simp
@[simp] theorem flatMap_empty {β} (f : α Array β) : (#[] : Array α).flatMap f = #[] := rfl
@[simp] theorem flatMap_toArray_cons {β} (f : α Array β) (a : α) (as : List α) :
theorem flatMap_toArray_cons {β} (f : α Array β) (a : α) (as : List α) :
(a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
simp [flatMap]
suffices cs, List.foldl (fun bs a => bs ++ f a) (f a ++ cs) as =
@@ -2276,7 +2371,7 @@ namespace Array
| nil => simp
| cons a as ih =>
apply ext'
simp [ih]
simp [ih, flatMap_toArray_cons]
end Array
@@ -2322,10 +2417,10 @@ abbrev get?_eq_toList_get? := @get?_eq_get?_toList
@[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
@[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
@[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_eq_setIfInBounds
@[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_eq
@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_eq
@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_self
@[deprecated getD_get?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_get?_setIfInBounds
@[deprecated getElem_setIfInBounds (since := "2024-11-24")] abbrev getElem_setD := @getElem_setIfInBounds

View File

@@ -332,11 +332,11 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m n) : x < 2 ^ n :=
Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
@[simp] theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by
simp [getElem_eq_testBit_toNat]
theorem getElem_zero_ofNat_zero (i : Nat) (h : i < w) : (BitVec.ofNat w 0)[i] = false := by
simp
@[simp] theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by
simp [getElem_eq_testBit_toNat, h]
theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by
simp
theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by
simp
@@ -362,12 +362,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
@[simp]
theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
rcases b with rfl | rfl
· simp [ofBool]
· simp only [ofBool]
by_cases hi : i = 0 <;> simp [hi] <;> omega
theorem getElem_ofBool {b : Bool} : (ofBool b)[0] = b := by simp
@[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by
cases b <;> simp [getMsbD]
@@ -538,7 +533,7 @@ theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
A bitvector, when interpreted as an integer, is less than zero iff
its most significant bit is true.
-/
theorem slt_zero_iff_msb_cond (x : BitVec w) : x.slt 0#w x.msb = true := by
theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w x.msb = true := by
have := toInt_eq_msb_cond x
constructor
· intros h
@@ -1120,12 +1115,8 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
rw [h]
simp
@[simp] theorem getMsb_not {x : BitVec w} :
(~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by
simp only [getMsbD]
by_cases h : i < w
· simp [h]; omega
· simp [h];
theorem getMsb_not {x : BitVec w} :
(~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by simp
@[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by
simp [BitVec.msb]
@@ -1243,7 +1234,6 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
@[simp] theorem getMsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
getMsbD (shiftLeftZeroExtend x n) i = getMsbD x i := by
have : n i + n := by omega
simp_all [shiftLeftZeroExtend_eq]
@[simp] theorem msb_shiftLeftZeroExtend (x : BitVec w) (i : Nat) :
@@ -1291,10 +1281,9 @@ theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
(x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
simp [shiftLeft_eq', getLsbD_shiftLeft]
@[simp]
theorem getElem_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) :
(x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
simp [shiftLeft_eq', getLsbD_shiftLeft]
simp
/-! ### ushiftRight -/
@@ -1597,39 +1586,25 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
@[simp]
theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat := rfl
@[simp]
theorem getLsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
-- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form.
theorem getLsbD_sshiftRight' {x y : BitVec w} {i : Nat} :
getLsbD (x.sshiftRight' y) i =
(!decide (w i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
@[simp]
-- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form.
theorem getElem_sshiftRight' {x y : BitVec w} {i : Nat} (h : i < w) :
(x.sshiftRight' y)[i] =
(!decide (w i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
simp only [ getLsbD_eq_getElem, BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
@[simp]
theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
(x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by
simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight]
by_cases h : i < w
· simp only [h, decide_true, Bool.true_and]
by_cases h₁ : w w - 1 - i
· simp [h₁]
omega
· simp only [h₁, decide_false, Bool.not_false, Bool.true_and]
by_cases h₂ : i < y.toNat
· simp only [h₂, reduceIte, ite_eq_right_iff]
omega
· simp only [show i - y.toNat < w by omega, h₂, reduceIte, decide_true, Bool.true_and]
by_cases h₄ : y.toNat + (w - 1 - i) < w <;> (simp only [h₄, reduceIte]; congr; omega)
· simp [h]
(x.sshiftRight y.toNat).getMsbD i =
(decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by
simp
@[simp]
theorem msb_sshiftRight' {x y: BitVec w} :
(x.sshiftRight' y).msb = x.msb := by
simp [BitVec.sshiftRight', BitVec.msb_sshiftRight]
(x.sshiftRight' y).msb = x.msb := by simp
/-! ### signExtend -/
@@ -1883,7 +1858,6 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} :
· simp_all
· simp_all only [Bool.iff_and_self, decide_eq_true_eq]
intro h
have := BitVec.lt_of_getLsbD h
omega
@[simp] theorem setWidth_cons {x : BitVec w} : (cons a x).setWidth w = x := by
@@ -2091,8 +2065,9 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
@[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by
simp [getLsbD_concat]
@[simp] theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i < w) :
@[simp] theorem getElem_concat_succ {x : BitVec w} {i : Nat} (h : i + 1 < w + 1) :
(concat x b)[i + 1] = x[i] := by
simp only [Nat.add_lt_add_iff_right] at h
simp [getElem_concat, h, getLsbD_eq_getElem]
@[simp]
@@ -2195,7 +2170,6 @@ theorem toNat_shiftConcat_lt_of_lt {x : BitVec w} {b : Bool} {k : Nat}
(hk : k < w) (hx : x.toNat < 2 ^ k) :
(x.shiftConcat b).toNat < 2 ^ (k + 1) := by
rw [toNat_shiftConcat_eq_of_lt hk hx]
have : 2 ^ (k + 1) 2 ^ w := Nat.pow_le_pow_of_le_right (by decide) (by assumption)
have := Bool.toNat_lt b
omega
@@ -2704,7 +2678,7 @@ theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
@[simp]
theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n) := by
rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond x, hx, negOne_eq_allOnes]
rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond, hx, negOne_eq_allOnes]
/-! ### srem -/
@@ -3024,10 +2998,10 @@ theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i
simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) w by omega]
/-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`. -/
@[simp]
theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w):
-- This should not be a simp lemma as `getMsbD_rotateRight` will apply first.
theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w) :
(x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))) := by
rcases w with rfl | w
· simp
· rw [rotateRight_eq_rotateRightAux_of_lt (by omega)]
@@ -3590,9 +3564,7 @@ Note, however, that for large numerals the decision procedure may be very slow.
instance instDecidableExistsBitVec :
(n : Nat) (P : BitVec n Prop) [DecidablePred P], Decidable ( v, P v)
| 0, _, _ => inferInstance
| n + 1, _, _ =>
have := instDecidableExistsBitVec n
inferInstance
| _ + 1, _, _ => inferInstance
/-! ### Deprecations -/

View File

@@ -225,7 +225,7 @@ theorem bne_not_self : ∀ (x : Bool), (x != !x) = true := by decide
Added for equivalence with `Bool.not_beq_self` and needed for confluence
due to `beq_iff_eq`.
-/
@[simp] theorem not_eq_self : (b : Bool), ((!b) = b) False := by decide
theorem not_eq_self : (b : Bool), ((!b) = b) False := by simp
@[simp] theorem eq_not_self : (b : Bool), (b = (!b)) False := by decide
@[simp] theorem beq_self_left : (a b : Bool), (a == (a == b)) = b := by decide
@@ -420,7 +420,7 @@ def toInt (b : Bool) : Int := cond b 1 0
@[simp] theorem ite_eq_true_else_eq_false {q : Prop} :
(if b = true then q else b = false) (b = true q) := by
cases b <;> simp
cases b <;> simp [not_eq_self]
/-
`not_ite_eq_true_eq_true` and related theorems below are added for

View File

@@ -545,10 +545,8 @@ theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
natAdd m (natAdd n i) = (natAdd (m + n) i).cast (Nat.add_assoc ..) :=
Fin.ext <| (Nat.add_assoc ..).symm
@[simp]
theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
(natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) :=
Fin.ext <| Nat.zero_add _
(natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) := by simp
@[simp]
theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :

View File

@@ -9,9 +9,6 @@ import Init.Data.Int.Basic
import Init.Data.ToString.Basic
import Init.Data.Float
/-
#exit -- TODO: Remove after update stage0
-- Just show FloatSpec is inhabited.
opaque float32Spec : FloatSpec := {
float := Unit,
@@ -130,7 +127,7 @@ Returns an undefined value if `x` is not finite.
instance : ToString Float32 where
toString := Float32.toString
@[extern "lean_uint64_to_float"] opaque UInt64.toFloat32 (n : UInt64) : Float32
@[extern "lean_uint64_to_float32"] opaque UInt64.toFloat32 (n : UInt64) : Float32
instance : Inhabited Float32 where
default := UInt64.toFloat32 0
@@ -177,4 +174,6 @@ Efficiently computes `x * 2^i`.
-/
@[extern "lean_float32_scaleb"]
opaque Float32.scaleB (x : Float32) (i : @& Int) : Float32
-/
@[extern "lean_float32_to_float"] opaque Float32.toFloat : Float32 Float
@[extern "lean_float_to_float32"] opaque Float.toFloat32 : Float Float32

View File

@@ -118,7 +118,6 @@ theorem attach_map_coe (l : List α) (f : α → β) :
theorem attach_map_val (l : List α) (f : α β) : (l.attach.map fun i => f i.val) = l.map f :=
attach_map_coe _ _
@[simp]
theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
(attach_map_coe _ _).trans (List.map_id _)
@@ -130,7 +129,6 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (l : List α) (H :
((l.attachWith p H).map fun i => f i.val) = l.map f :=
attachWith_map_coe _ _ _
@[simp]
theorem attachWith_map_subtype_val {p : α Prop} (l : List α) (H : a l, p a) :
(l.attachWith p H).map Subtype.val = l :=
(attachWith_map_coe _ _ _).trans (List.map_id _)
@@ -174,8 +172,8 @@ theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : Li
(H : (a : α), a xs P a) : xs.pmap f H [] xs [] := by
simp
theorem pmap_eq_self {l : List α} {p : α Prop} (hp : (a : α), a l p a)
(f : (a : α) p a α) : l.pmap f hp = l a (h : a l), f a (hp a h) = a := by
theorem pmap_eq_self {l : List α} {p : α Prop} {hp : (a : α), a l p a}
{f : (a : α) p a α} : l.pmap f hp = l a (h : a l), f a (hp a h) = a := by
rw [pmap_eq_map_attach]
conv => lhs; rhs; rw [ attach_map_subtype_val l]
rw [map_inj_left]

View File

@@ -566,7 +566,6 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
| inl e => simpa [e, Fin.zero_eta, get_cons_zero]
| inr e =>
have ipm := Nat.succ_pred_eq_of_pos e
have ilt := Nat.le_trans ho (findIdx_le_length p)
simp +singlePass only [ ipm, getElem_cons_succ]
rw [ ipm, Nat.succ_lt_succ_iff] at h
simpa using ih h

View File

@@ -332,7 +332,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
rw [ show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
simp [enumFrom, f]
rw [ Array.foldr_toList]
simp [go]
simp +zetaDelta [go]
/-! ## Other list operations -/

View File

@@ -154,6 +154,9 @@ theorem ne_nil_iff_exists_cons {l : List α} : l ≠ [] ↔ ∃ b L, l = b :: L
theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] a = b := by
simp
@[simp] theorem concat_ne_nil (a : α) (l : List α) : l ++ [a] [] := by
cases l <;> simp
/-! ## L[i] and L[i]? -/
/-! ### `get` and `get?`.
@@ -191,50 +194,52 @@ We simplify away `getD`, replacing `getD l n a` with `(l[n]?).getD a`.
Because of this, there is only minimal API for `getD`.
-/
@[simp] theorem getD_eq_getElem?_getD (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by
@[simp] theorem getD_eq_getElem?_getD (l) (i) (a : α) : getD l i a = (l[i]?).getD a := by
simp [getD]
/-! ### get!
We simplify `l.get! n` to `l[n]!`.
We simplify `l.get! i` to `l[i]!`.
-/
theorem get!_eq_getD [Inhabited α] : (l : List α) n, l.get! n = l.getD n default
theorem get!_eq_getD [Inhabited α] : (l : List α) i, l.get! i = l.getD i default
| [], _ => rfl
| _a::_, 0 => rfl
| _a::l, n+1 => get!_eq_getD l n
@[simp] theorem get!_eq_getElem! [Inhabited α] (l : List α) (n) : l.get! n = l[n]! := by
@[simp] theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]! := by
simp [get!_eq_getD]
rfl
/-! ### getElem!
We simplify `l[n]!` to `(l[n]?).getD default`.
We simplify `l[i]!` to `(l[i]?).getD default`.
-/
@[simp] theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (n : Nat) :
l[n]! = (l[n]?).getD (default : α) := by
@[simp] theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (i : Nat) :
l[i]! = (l[i]?).getD (default : α) := by
simp only [getElem!_def]
split <;> simp_all
match l[i]? with
| some _ => simp
| none => simp
/-! ### getElem? and getElem -/
@[simp] theorem getElem?_eq_none_iff : l[n]? = none length l n := by
@[simp] theorem getElem?_eq_none_iff : l[i]? = none length l i := by
simp only [ get?_eq_getElem?, get?_eq_none_iff]
@[simp] theorem none_eq_getElem?_iff {l : List α} {n : Nat} : none = l[n]? length l n := 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 n) : l[n]? = none := getElem?_eq_none_iff.mpr h
theorem getElem?_eq_none (h : length l i) : l[i]? = none := getElem?_eq_none_iff.mpr h
@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] :=
@[simp] theorem getElem?_eq_getElem {l : List α} {i} (h : i < l.length) : l[i]? = some l[i] :=
getElem?_pos ..
theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a h : n < l.length, l[n] = a := by
theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a h : i < l.length, l[i] = a := by
simp only [ get?_eq_getElem?, get?_eq_some_iff, get_eq_getElem]
theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? h : n < l.length, l[n] = a := by
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]
@[simp] theorem some_getElem_eq_getElem?_iff (xs : List α) (i : Nat) (h : i < xs.length) :
@@ -245,7 +250,7 @@ theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.le
(xs[i]? = some xs[i]) True := by
simp [h]
theorem getElem_eq_iff {l : List α} {n : Nat} {h : n < l.length} : l[n] = x l[n]? = some x := by
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]
exact fun w => h, w, fun h => h.2
@@ -253,7 +258,15 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
simp [getElem_eq_iff]
@[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
theorem getD_getElem? (l : List α) (i : Nat) (d : α) :
l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
if h : i < l.length then
simp [h, getElem?_def]
else
have p : i l.length := Nat.le_of_not_gt h
simp [getElem?_eq_none p, h]
@[simp] theorem getElem?_nil {i : Nat} : ([] : List α)[i]? = none := rfl
theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
(a :: l)[i] =
@@ -262,7 +275,7 @@ theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by
@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[i+1]? = l[i]? := by
simp only [ get?_eq_getElem?]
rfl
@@ -289,11 +302,11 @@ theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_po
match l, h with
| _ :: _, _ => rfl
@[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : n : Nat, l₁[n]? = l₂[n]?) : l₁ = l₂ :=
@[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂ :=
ext_get? fun n => by simp_all
theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
(h : (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁[n]'h₁ = l₂[n]'h₂) : l₁ = l₂ :=
(h : (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i]'h₁ = l₂[i]'h₂) : l₁ = l₂ :=
ext_getElem? fun n =>
if h₁ : n < length l₁ then by
simp_all [getElem?_eq_getElem]
@@ -414,25 +427,25 @@ theorem not_mem_cons_of_ne_of_not_mem {a y : α} {l : List α} : a ≠ y → a
theorem ne_and_not_mem_of_not_mem_cons {a y : α} {l : List α} : a y :: l a y a l :=
fun p => ne_of_not_mem_cons p, not_mem_of_not_mem_cons p
theorem getElem_of_mem : {a} {l : List α}, a l (n : Nat) (h : n < l.length), l[n]'h = a
theorem getElem_of_mem : {a} {l : List α}, a l (i : Nat) (h : i < l.length), l[i]'h = a
| _, _ :: _, .head .. => 0, Nat.succ_pos _, rfl
| _, _ :: _, .tail _ m => let n, h, e := getElem_of_mem m; n+1, Nat.succ_lt_succ h, e
| _, _ :: _, .tail _ m => let i, h, e := getElem_of_mem m; i+1, Nat.succ_lt_succ h, e
theorem getElem?_of_mem {a} {l : List α} (h : a l) : n : Nat, l[n]? = some a := by
theorem getElem?_of_mem {a} {l : List α} (h : a l) : i : Nat, l[i]? = some a := by
let n, _, e := getElem_of_mem h
exact n, e getElem?_eq_getElem _
theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a l :=
theorem mem_of_getElem? {l : List α} {i : Nat} {a : α} (e : l[i]? = some a) : a l :=
let _, e := getElem?_eq_some_iff.1 e; e getElem_mem ..
theorem mem_iff_getElem {a} {l : List α} : a l (n : Nat) (h : n < l.length), l[n]'h = a :=
theorem mem_iff_getElem {a} {l : List α} : a l (i : Nat) (h : i < l.length), l[i]'h = a :=
getElem_of_mem, fun _, _, e => e getElem_mem ..
theorem mem_iff_getElem? {a} {l : List α} : a l n : Nat, l[n]? = some a := by
theorem mem_iff_getElem? {a} {l : List α} : a l i : Nat, l[i]? = some a := by
simp [getElem?_eq_some_iff, mem_iff_getElem]
theorem forall_getElem {l : List α} {p : α Prop} :
( (n : Nat) h, p (l[n]'h)) a, a l p a := by
( (i : Nat) h, p (l[i]'h)) a, a l p a := by
induction l with
| nil => simp
| cons a l ih =>
@@ -585,10 +598,10 @@ theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} :
simp_all
· rw [getElem?_eq_none (by simp_all), getElem?_eq_none (by simp_all)]
theorem getElem_set {l : List α} {m n} {a} (h) :
(set l m a)[n]'h = if m = n then a else l[n]'(length_set .. h) := by
if h : m = n then
subst m; simp only [getElem_set_self, reduceIte]
theorem getElem_set {l : List α} {i j} {a} (h) :
(set l i a)[j]'h = if i = j then a else l[j]'(length_set .. h) := by
if h : i = j then
subst h; simp only [getElem_set_self, reduceIte]
else
simp [h]
@@ -707,6 +720,15 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s
@[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
(a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
@[simp] theorem concat_beq_concat [BEq α] {a b : α} {l₁ l₂ : List α} :
(l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b) := by
induction l₁ generalizing l₂ with
| nil => cases l₂ <;> simp
| cons x l₁ ih =>
cases l₂ with
| nil => simp
| cons y l₂ => simp [ih, Bool.and_assoc]
theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length :=
match l₁, l₂ with
| [], [] => rfl
@@ -1011,8 +1033,8 @@ theorem getLastD_mem_cons : ∀ (l : List α) (a : α), getLastD l a ∈ a::l
| [], _ => .head ..
| _::_, _ => .tail _ <| getLast_mem _
theorem getElem_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
(x :: xs)[n]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by
theorem getElem_cons_length (x : α) (xs : List α) (i : Nat) (h : i = xs.length) :
(x :: xs)[i]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by
rw [getLast_eq_getElem]; cases h; rfl
@[deprecated getElem_cons_length (since := "2024-06-12")]
@@ -1244,24 +1266,24 @@ theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
| nil => simp [List.map]
| cons _ as ih => simp [List.map, ih]
@[simp] theorem getElem?_map (f : α β) : (l : List α) (n : Nat), (map f l)[n]? = Option.map f l[n]?
@[simp] theorem getElem?_map (f : α β) : (l : List α) (i : Nat), (map f l)[i]? = Option.map f l[i]?
| [], _ => rfl
| _ :: _, 0 => by simp
| _ :: l, n+1 => by simp [getElem?_map f l n]
| _ :: l, i+1 => by simp [getElem?_map f l i]
@[deprecated getElem?_map (since := "2024-06-12")]
theorem get?_map (f : α β) : l n, (map f l).get? n = (l.get? n).map f
theorem get?_map (f : α β) : l i, (map f l).get? i = (l.get? i).map f
| [], _ => rfl
| _ :: _, 0 => rfl
| _ :: l, n+1 => get?_map f l n
| _ :: l, i+1 => get?_map f l i
@[simp] theorem getElem_map (f : α β) {l} {n : Nat} {h : n < (map f l).length} :
(map f l)[n] = f (l[n]'(length_map l f h)) :=
@[simp] theorem getElem_map (f : α β) {l} {i : Nat} {h : i < (map f l).length} :
(map f l)[i] = f (l[i]'(length_map l f h)) :=
Option.some.inj <| by rw [ getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl
@[deprecated getElem_map (since := "2024-06-12")]
theorem get_map (f : α β) {l n} :
get (map f l) n = f (get l n, length_map l f n.2) := by
theorem get_map (f : α β) {l i} :
get (map f l) i = f (get l i, length_map l f i.2) := by
simp
@[simp] theorem mem_map {f : α β} : {l : List α}, b l.map f a, a l f a = b
@@ -1692,71 +1714,71 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
@[simp] theorem cons_append_fun (a : α) (as : List α) :
(fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h : n < (l₁ ++ l₂).length) :
(l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
theorem getElem_append {l₁ l₂ : List α} (i : Nat) (h : i < (l₁ ++ l₂).length) :
(l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
split <;> rename_i h'
· rw [getElem_append_left h']
· rw [getElem_append_right (by simpa using h')]
theorem getElem?_append_left {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
(l₁ ++ l₂)[n]? = l₁[n]? := by
have hn' : n < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <|
theorem getElem?_append_left {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :
(l₁ ++ l₂)[i]? = l₁[i]? := by
have hn' : i < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <|
length_append .. Nat.le_add_right ..
simp_all [getElem?_eq_getElem, getElem_append]
theorem getElem?_append_right : {l₁ l₂ : List α} {n : Nat}, l₁.length n
(l₁ ++ l₂)[n]? = l₂[n - l₁.length]?
theorem getElem?_append_right : {l₁ l₂ : List α} {i : Nat}, l₁.length i
(l₁ ++ l₂)[i]? = l₂[i - l₁.length]?
| [], _, _, _ => rfl
| a :: l, _, n+1, h₁ => by
| a :: l, _, i+1, h₁ => by
rw [cons_append]
simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)]
theorem getElem?_append {l₁ l₂ : List α} {n : Nat} :
(l₁ ++ l₂)[n]? = if n < l₁.length then l₁[n]? else l₂[n - l₁.length]? := by
theorem getElem?_append {l₁ l₂ : List α} {i : Nat} :
(l₁ ++ l₂)[i]? = if i < l₁.length then l₁[i]? else l₂[i - l₁.length]? := by
split <;> rename_i h
· exact getElem?_append_left h
· exact getElem?_append_right (by simpa using h)
@[deprecated getElem?_append_right (since := "2024-06-12")]
theorem get?_append_right {l₁ l₂ : List α} {n : Nat} (h : l₁.length n) :
(l₁ ++ l₂).get? n = l₂.get? (n - l₁.length) := by
theorem get?_append_right {l₁ l₂ : List α} {i : Nat} (h : l₁.length i) :
(l₁ ++ l₂).get? i = l₂.get? (i - l₁.length) := by
simp [getElem?_append_right, h]
/-- Variant of `getElem_append_left` useful for rewriting from the small list to the big list. -/
theorem getElem_append_left' (l₂ : List α) {l₁ : List α} {n : Nat} (hn : n < l₁.length) :
l₁[n] = (l₁ ++ l₂)[n]'(by simpa using Nat.lt_add_right l₂.length hn) := by
theorem getElem_append_left' (l₂ : List α) {l₁ : List α} {i : Nat} (hi : i < l₁.length) :
l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.length hi) := by
rw [getElem_append_left] <;> simp
/-- Variant of `getElem_append_right` useful for rewriting from the small list to the big list. -/
theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {n : Nat} (hn : n < l₂.length) :
l₂[n] = (l₁ ++ l₂)[n + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hn _) := by
theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi : i < l₂.length) :
l₂[i] = (l₁ ++ l₂)[i + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _) := by
rw [getElem_append_right] <;> simp [*, le_add_left]
@[deprecated "Deprecated without replacement." (since := "2024-06-12")]
theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat}
(h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length := by
theorem get_append_right_aux {l₁ l₂ : List α} {i : Nat}
(h₁ : l₁.length i) (h₂ : i < (l₁ ++ l₂).length) : i - l₁.length < l₂.length := by
rw [length_append] at h₂
exact Nat.sub_lt_left_of_lt_add h₁ h₂
set_option linter.deprecated false in
@[deprecated getElem_append_right (since := "2024-06-12")]
theorem get_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length n) (h₂) :
(l₁ ++ l₂).get n, h₂ = l₂.get n - l₁.length, get_append_right_aux h₁ h₂ :=
theorem get_append_right' {l₁ l₂ : List α} {i : Nat} (h₁ : l₁.length i) (h₂) :
(l₁ ++ l₂).get i, h₂ = l₂.get i - l₁.length, get_append_right_aux h₁ h₂ :=
Option.some.inj <| by rw [ get?_eq_get, get?_eq_get, get?_append_right h₁]
theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :
l[n]'(eq h by simp_arith) = a := Option.some.inj <| by
theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
l[i]'(eq h by simp_arith) = a := Option.some.inj <| by
rw [ getElem?_eq_getElem, eq, getElem?_append_right (h Nat.le_refl _), h]
simp
@[deprecated "Deprecated without replacement." (since := "2024-06-12")]
theorem get_of_append_proof {l : List α}
(eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : n < length l := eq h by simp_arith
(eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) : i < length l := eq h by simp_arith
set_option linter.deprecated false in
@[deprecated getElem_of_append (since := "2024-06-12")]
theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :
l.get n, get_of_append_proof eq h = a := Option.some.inj <| by
theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
l.get i, get_of_append_proof eq h = a := Option.some.inj <| by
rw [ get?_eq_get, eq, get?_append_right (h Nat.le_refl _), h, Nat.sub_self]; rfl
/--
@@ -2064,8 +2086,6 @@ theorem concat_inj_right {l : List α} {a a' : α} : concat l a = concat l a'
@[deprecated concat_inj (since := "2024-09-05")] abbrev concat_eq_concat := @concat_inj
theorem concat_ne_nil (a : α) (l : List α) : concat l a [] := by cases l <;> simp
theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by simp
theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
@@ -2318,6 +2338,10 @@ theorem flatMap_eq_foldl (f : α → List β) (l : List α) :
@[simp] theorem replicate_one : replicate 1 a = [a] := rfl
/-- Variant of `replicate_succ` that concatenates `a` to the end of the list. -/
theorem replicate_succ' : replicate (n + 1) a = replicate n a ++ [a] := by
induction n <;> simp_all [replicate_succ, cons_append]
@[simp] theorem mem_replicate {a b : α} : {n}, b replicate n a n 0 b = a
| 0 => by simp
| n+1 => by simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]
@@ -3396,12 +3420,12 @@ theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default :=
theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
rw [getElem!_pos] <;> simp
theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[n+1]! = l[n]! := by
by_cases h : n < l.length
theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[i+1]! = l[i]! := by
by_cases h : i < l.length
· rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff]
· rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff]
theorem getElem!_of_getElem? [Inhabited α] : {l : List α} {n : Nat}, l[n]? = some a l[n]! = a
theorem getElem!_of_getElem? [Inhabited α] : {l : List α} {i : Nat}, l[i]? = some a l[i]! = a
| _a::_, 0, _ => by
rw [getElem!_pos] <;> simp_all
| _::l, _+1, e => by
@@ -3550,7 +3574,7 @@ theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length
simp
@[deprecated _root_.isNone_getElem? (since := "2024-12-09")]
theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone l.length n := by
theorem isNone_getElem? {l : List α} {i : Nat} : l[i]?.isNone l.length i := by
simp
end List

View File

@@ -68,8 +68,8 @@ theorem getElem?_modifyHead {l : List α} {f : αα} {n} :
(l.modifyHead f).drop n = l.drop n := by
cases l <;> cases n <;> simp_all
@[simp] theorem eraseIdx_modifyHead_zero {f : α α} {l : List α} :
(l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by cases l <;> simp
theorem eraseIdx_modifyHead_zero {f : α α} {l : List α} :
(l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by simp
@[simp] theorem eraseIdx_modifyHead_of_pos {f : α α} {l : List α} {n} (h : 0 < n) :
(l.modifyHead f).eraseIdx n = (l.eraseIdx n).modifyHead f := by cases l <;> cases n <;> simp_all
@@ -142,7 +142,7 @@ theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (n : Nat) (
theorem modifyHead_eq_modify_zero (f : α α) (l : List α) :
l.modifyHead f = l.modify f 0 := by cases l <;> simp
@[simp] theorem modify_eq_nil_iff (f : α α) (n) (l : List α) :
@[simp] theorem modify_eq_nil_iff {f : α α} {n} {l : List α} :
l.modify f n = [] l = [] := by cases l <;> cases n <;> simp
theorem getElem?_modify (f : α α) :

View File

@@ -40,12 +40,15 @@ def merge (xs ys : List α) (le : αα → Bool := by exact fun a b => a
/--
Split a list in two equal parts. If the length is odd, the first part will be one element longer.
This is an implementation detail of `mergeSort`.
-/
def splitInTwo (l : { l : List α // l.length = n }) :
def MergeSort.Internal.splitInTwo (l : { l : List α // l.length = n }) :
{ l : List α // l.length = (n+1)/2 } × { l : List α // l.length = n/2 } :=
let r := splitAt ((n+1)/2) l.1
(r.1, by simp [r, splitAt_eq, l.2]; omega, r.2, by simp [r, splitAt_eq, l.2]; omega)
open MergeSort.Internal in
set_option linter.unusedVariables false in
/--
Simplified implementation of stable merge sort.

View File

@@ -147,23 +147,21 @@ where
mergeTR (run' r) (run l) le
theorem splitRevInTwo'_fst (l : { l : List α // l.length = n }) :
(splitRevInTwo' l).1 = (splitInTwo l.1.reverse, by simpa using l.2).2.1, by have := l.2; simp; omega := by
(splitRevInTwo' l).1 = (splitInTwo l.1.reverse, by simpa using l.2).2.1, by simp; omega := by
simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_snd]
congr
have := l.2
omega
theorem splitRevInTwo'_snd (l : { l : List α // l.length = n }) :
(splitRevInTwo' l).2 = (splitInTwo l.1.reverse, by simpa using l.2).1.1.reverse, by have := l.2; simp; omega := by
(splitRevInTwo' l).2 = (splitInTwo l.1.reverse, by simpa using l.2).1.1.reverse, by simp; omega := by
simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_fst, reverse_reverse]
congr 2
have := l.2
simp
omega
theorem splitRevInTwo_fst (l : { l : List α // l.length = n }) :
(splitRevInTwo l).1 = (splitInTwo l).1.1.reverse, by have := l.2; simp; omega := by
(splitRevInTwo l).1 = (splitInTwo l).1.1.reverse, by simp; omega := by
simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_fst]
theorem splitRevInTwo_snd (l : { l : List α // l.length = n }) :
(splitRevInTwo l).2 = (splitInTwo l).2.1, by have := l.2; simp; omega := by
(splitRevInTwo l).2 = (splitInTwo l).2.1, by simp; omega := by
simp only [splitRevInTwo, splitRevAt_eq, reverse_take, splitInTwo_snd]
theorem mergeSortTR_run_eq_mergeSort : {n : Nat} (l : { l : List α // l.length = n }) mergeSortTR.run le l = mergeSort l.1 le

View File

@@ -25,6 +25,8 @@ namespace List
/-! ### splitInTwo -/
namespace MergeSort.Internal
@[simp] theorem splitInTwo_fst (l : { l : List α // l.length = n }) :
(splitInTwo l).1 = l.1.take ((n+1)/2), by simp [splitInTwo, splitAt_eq, l.2]; omega := by
simp [splitInTwo, splitAt_eq]
@@ -82,6 +84,10 @@ theorem splitInTwo_fst_le_splitInTwo_snd {l : { l : List α // l.length = n }} (
intro a b ma mb
exact h.rel_of_mem_take_of_mem_drop ma mb
end MergeSort.Internal
open MergeSort.Internal
/-! ### enumLE -/
variable {le : α α Bool}
@@ -285,8 +291,6 @@ theorem sorted_mergeSort
| [] => by simp [mergeSort]
| [a] => by simp [mergeSort]
| a :: b :: xs => by
have : (splitInTwo a :: b :: xs, rfl).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega
have : (splitInTwo a :: b :: xs, rfl).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega
rw [mergeSort]
apply sorted_merge @trans @total
apply sorted_mergeSort trans total

View File

@@ -38,7 +38,7 @@ theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
simp
@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
cases l <;> simp
cases l <;> simp [Array.isEmpty]
@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
@@ -363,4 +363,17 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
l.toArray.takeWhile p = (l.takeWhile p).toArray := by
simp [Array.takeWhile, takeWhile_go_toArray]
@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
l.toArray.setIfInBounds i a = (l.set i a).toArray := by
apply ext'
simp only [setIfInBounds]
split
· simp
· simp_all [List.set_eq_of_length_le]
@[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = mkArray n v := rfl
@[deprecated toArray_replicate (since := "2024-12-13")]
abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
end List

View File

@@ -106,9 +106,21 @@ theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i := by
unfold testBit
simp [shiftRight_succ_inside]
theorem testBit_add (x i n : Nat) : testBit x (i + n) = testBit (x / 2 ^ n) i := by
revert x
induction n with
| zero => simp
| succ n ih =>
intro x
rw [ Nat.add_assoc, testBit_add_one, ih (x / 2),
Nat.pow_succ, Nat.div_div_eq_div_mul, Nat.mul_comm]
theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := by
simp
theorem testBit_div_two_pow (x i : Nat) : testBit (x / 2 ^ n) i = testBit x (i + n) :=
testBit_add .. |>.symm
theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
induction i generalizing x with
| zero =>
@@ -365,7 +377,7 @@ theorem testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : testBit (2 ^ n) m = f
/-! ### bitwise -/
theorem testBit_bitwise (false_false_axiom : f false false = false) (x y i : Nat) :
theorem testBit_bitwise (of_false_false : f false false = false) (x y i : Nat) :
(bitwise f x y).testBit i = f (x.testBit i) (y.testBit i) := by
induction i using Nat.strongRecOn generalizing x y with
| ind i hyp =>
@@ -373,12 +385,12 @@ theorem testBit_bitwise (false_false_axiom : f false false = false) (x y i : Nat
if x_zero : x = 0 then
cases p : f false true <;>
cases yi : testBit y i <;>
simp [x_zero, p, yi, false_false_axiom]
simp [x_zero, p, yi, of_false_false]
else if y_zero : y = 0 then
simp [x_zero, y_zero]
cases p : f true false <;>
cases xi : testBit x i <;>
simp [p, xi, false_false_axiom]
simp [p, xi, of_false_false]
else
simp only [x_zero, y_zero, Nat.two_mul]
cases i with
@@ -440,6 +452,11 @@ theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x
case neg =>
apply Nat.add_lt_add <;> exact hyp1
theorem bitwise_div_two_pow (of_false_false : f false false = false := by rfl) :
(bitwise f x y) / 2 ^ n = bitwise f (x / 2 ^ n) (y / 2 ^ n) := by
apply Nat.eq_of_testBit_eq
simp [testBit_bitwise of_false_false, testBit_div_two_pow]
/-! ### and -/
@[simp] theorem testBit_and (x y i : Nat) : (x &&& y).testBit i = (x.testBit i && y.testBit i) := by
@@ -495,9 +512,11 @@ theorem and_pow_two_sub_one_of_lt_two_pow {x : Nat} (lt : x < 2^n) : x &&& 2^n -
rw [testBit_and]
simp
theorem and_div_two : (a &&& b) / 2 = a / 2 &&& b / 2 := by
apply Nat.eq_of_testBit_eq
simp [testBit_and, testBit_add_one]
theorem and_div_two_pow : (a &&& b) / 2 ^ n = a / 2 ^ n &&& b / 2 ^ n :=
bitwise_div_two_pow
theorem and_div_two : (a &&& b) / 2 = a / 2 &&& b / 2 :=
and_div_two_pow (n := 1)
/-! ### lor -/
@@ -563,9 +582,11 @@ theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y
rw [testBit_or]
simp
theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 := by
apply Nat.eq_of_testBit_eq
simp [testBit_or, testBit_add_one]
theorem or_div_two_pow : (a ||| b) / 2 ^ n = a / 2 ^ n ||| b / 2 ^ n :=
bitwise_div_two_pow
theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 :=
or_div_two_pow (n := 1)
/-! ### xor -/
@@ -619,9 +640,11 @@ theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a
rw [testBit_xor]
simp
theorem xor_div_two : (a ^^^ b) / 2 = a / 2 ^^^ b / 2 := by
apply Nat.eq_of_testBit_eq
simp [testBit_xor, testBit_add_one]
theorem xor_div_two_pow : (a ^^^ b) / 2 ^ n = a / 2 ^ n ^^^ b / 2 ^ n :=
bitwise_div_two_pow
theorem xor_div_two : (a ^^^ b) / 2 = a / 2 ^^^ b / 2 :=
xor_div_two_pow (n := 1)
/-! ### Arithmetic -/
@@ -693,6 +716,19 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]
exact (Bool.beq_eq_decide_eq _ _).symm
theorem shiftRight_bitwise_distrib {a b : Nat} (of_false_false : f false false = false := by rfl) :
(bitwise f a b) >>> i = bitwise f (a >>> i) (b >>> i) := by
simp [shiftRight_eq_div_pow, bitwise_div_two_pow of_false_false]
theorem shiftRight_and_distrib {a b : Nat} : (a &&& b) >>> i = a >>> i &&& b >>> i :=
shiftRight_bitwise_distrib
theorem shiftRight_or_distrib {a b : Nat} : (a ||| b) >>> i = a >>> i ||| b >>> i :=
shiftRight_bitwise_distrib
theorem shiftRight_xor_distrib {a b : Nat} : (a ^^^ b) >>> i = a >>> i ^^^ b >>> i :=
shiftRight_bitwise_distrib
/-! ### le -/
theorem le_of_testBit {n m : Nat} (h : i, n.testBit i = true m.testBit i = true) : n m := by

View File

@@ -77,7 +77,7 @@ theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m n := by
theorem dvd_iff_mod_eq_zero {m n : Nat} : m n n % m = 0 :=
mod_eq_zero_of_dvd, dvd_of_mod_eq_zero
instance decidable_dvd : @DecidableRel Nat (··) :=
instance decidable_dvd : @DecidableRel Nat Nat (··) :=
fun _ _ => decidable_of_decidable_of_iff dvd_iff_mod_eq_zero.symm
theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a b) : 0 < b % a := by

View File

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
prelude
import Init.Meta
import Init.Data.Float
import Init.Data.Float32
import Init.Data.Nat.Log2
/-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
@@ -56,3 +57,34 @@ instance : OfNat Float n := ⟨Float.ofNat n⟩
abbrev Nat.toFloat (n : Nat) : Float :=
Float.ofNat n
/-- Computes `m * 2^e`. -/
def Float32.ofBinaryScientific (m : Nat) (e : Int) : Float32 :=
let s := m.log2 - 63
let m := (m >>> s).toUInt64
let e := e + s
m.toFloat32.scaleB e
protected opaque Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float32 :=
if s then
let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
let m := (m <<< (3 * e + s)) / 5^e
Float32.ofBinaryScientific m (-4 * e - s)
else
Float32.ofBinaryScientific (m * 5^e) e
instance : OfScientific Float32 where
ofScientific := Float32.ofScientific
@[export lean_float32_of_nat]
def Float32.ofNat (n : Nat) : Float32 :=
OfScientific.ofScientific n false 0
def Float32.ofInt : Int Float
| Int.ofNat n => Float.ofNat n
| Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))
instance : OfNat Float32 n := Float32.ofNat n
abbrev Nat.toFloat32 (n : Nat) : Float32 :=
Float32.ofNat n

View File

@@ -56,7 +56,6 @@ theorem attach_map_val (o : Option α) (f : α → β) :
(o.attach.map fun i => f i.val) = o.map f :=
attach_map_coe _ _
@[simp]
theorem attach_map_subtype_val (o : Option α) :
o.attach.map Subtype.val = o :=
(attach_map_coe _ _).trans (congrFun Option.map_id _)
@@ -69,12 +68,11 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H
((o.attachWith p H).map fun i => f i.val) = o.map f :=
attachWith_map_coe _ _ _
@[simp]
theorem attachWith_map_subtype_val {p : α Prop} (o : Option α) (H : a o, p a) :
(o.attachWith p H).map Subtype.val = o :=
(attachWith_map_coe _ _ _).trans (congrFun Option.map_id _)
@[simp] theorem mem_attach : (o : Option α) (x : {x // x o}), x o.attach
theorem mem_attach : (o : Option α) (x : {x // x o}), x o.attach
| none, x, h => by simp at h
| some a, x, h => by simpa using h
@@ -92,14 +90,14 @@ theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a
(o.attachWith p H).isSome = o.isSome := by
cases o <;> simp
@[simp] theorem attach_eq_none_iff (o : Option α) : o.attach = none o = none := by
@[simp] theorem attach_eq_none_iff {o : Option α} : o.attach = none o = none := by
cases o <;> simp
@[simp] theorem attach_eq_some_iff {o : Option α} {x : {x // x o}} :
o.attach = some x o = some x.val := by
cases o <;> cases x <;> simp
@[simp] theorem attachWith_eq_none_iff {p : α Prop} (o : Option α) (H : a o, p a) :
@[simp] theorem attachWith_eq_none_iff {p : α Prop} {o : Option α} (H : a o, p a) :
o.attachWith p H = none o = none := by
cases o <;> simp

View File

@@ -96,12 +96,12 @@ This is similar to `<|>`/`orElse`, but it is strict in the second argument. -/
| some a, _ => some a
| none, b => b
@[inline] protected def lt (r : α α Prop) : Option α Option α Prop
@[inline] protected def lt (r : α β Prop) : Option α Option β Prop
| none, some _ => True
| some x, some y => r x y
| _, _ => False
instance (r : α α Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)
instance (r : α β Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)
| none, some _ => isTrue trivial
| some x, some y => s x y
| some _, none => isFalse not_false

View File

@@ -30,7 +30,7 @@ protected theorem «exists» {p : α ⊕ β → Prop} :
| Or.inl a, h => inl a, h
| Or.inr b, h => inr b, h
theorem forall_sum {γ : α β Sort _} (p : ( ab, γ ab) Prop) :
theorem forall_sum {γ : α β Sort _} {p : ( ab, γ ab) Prop} :
( fab, p fab) ( fa fb, p (Sum.rec fa fb)) := by
refine fun h fa fb => h _, fun h fab => ?_
have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by

View File

@@ -70,6 +70,16 @@ instance [Inhabited α] : Inhabited (Vector α n) where
instance : GetElem (Vector α n) Nat α fun _ i => i < n where
getElem x i h := get x i, h
/-- Check if there is an element which satisfies `a == ·`. -/
def contains [BEq α] (v : Vector α n) (a : α) : Bool := v.toArray.contains a
/-- `a ∈ v` is a predicate which asserts that `a` is in the vector `v`. -/
structure Mem (as : Vector α n) (a : α) : Prop where
val : a as.toArray
instance : Membership α (Vector α n) where
mem := Mem
/--
Get an element of a vector using a `Nat` index. Returns the given default value if the index is out
of bounds.
@@ -254,3 +264,19 @@ no element of the index matches the given value.
/-- Returns `true` when `v` is a prefix of the vector `w`. -/
@[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool :=
v.toArray.isPrefixOf w.toArray
/-- Returns `true` with the monad if `p` returns `true` for any element of the vector. -/
@[inline] def anyM [Monad m] (p : α m Bool) (v : Vector α n) : m Bool :=
v.toArray.anyM p
/-- Returns `true` with the monad if `p` returns `true` for all elements of the vector. -/
@[inline] def allM [Monad m] (p : α m Bool) (v : Vector α n) : m Bool :=
v.toArray.allM p
/-- Returns `true` if `p` returns `true` for any element of the vector. -/
@[inline] def any (v : Vector α n) (p : α Bool) : Bool :=
v.toArray.any p
/-- Returns `true` if `p` returns `true` for all elements of the vector. -/
@[inline] def all (v : Vector α n) (p : α Bool) : Bool :=
v.toArray.all p

View File

@@ -22,44 +22,26 @@ end Array
namespace Vector
/-! ### mk lemmas -/
theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
@[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
(Vector.mk data size)[i] = data[i] := rfl
@[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
xs.toArray[i] = xs[i]'(by simpa using h) := by
cases xs
simp
@[simp] theorem getElem?_mk {data : Array α} {size : data.size = n} {i : Nat} :
(Vector.mk data size)[i]? = data[i]? := by
subst size
simp [getElem?_def]
@[simp] theorem getElem_ofFn {α n} (f : Fin n α) (i : Nat) (h : i < n) :
(Vector.ofFn f)[i] = f i, by simpa using h := by
simp [ofFn]
@[simp] theorem mem_mk {data : Array α} {size : data.size = n} {a : α} :
a Vector.mk data size a data :=
fun h => h, fun h => h
/-- The empty vector maps to the empty vector. -/
@[simp]
theorem map_empty (f : α β) : map f #v[] = #v[] := by
rw [map, mk.injEq]
exact Array.map_empty f
theorem toArray_inj : {v w : Vector α n}, v.toArray = w.toArray v = w
| {..}, {..}, rfl => rfl
/-- A vector of length `0` is the empty vector. -/
protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
apply Vector.toArray_inj
apply Array.eq_empty_of_size_eq_zero v.2
/--
`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]
protected theorem ext {a b : Vector α n} (h : (i : Nat) (_ : i < n) a[i] = b[i]) : a = b := by
apply Vector.toArray_inj
apply Array.ext
· rw [a.size_toArray, b.size_toArray]
· intro i hi _
rw [a.size_toArray] at hi
exact h i hi
@[simp] theorem contains_mk [BEq α] {data : Array α} {size : data.size = n} {a : α} :
(Vector.mk data size).contains a = data.contains a := by
simp [contains]
@[simp] theorem push_mk {data : Array α} {size : data.size = n} {x : α} :
(Vector.mk data size).push x =
@@ -68,39 +50,9 @@ protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i
@[simp] theorem pop_mk {data : Array α} {size : data.size = n} :
(Vector.mk data size).pop = Vector.mk data.pop (by simp [size]) := rfl
@[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
rcases v with data, rfl
simp
@[simp] theorem getElem_push_lt {v : Vector α n} {x : α} {i : Nat} (h : i < n) :
(v.push x)[i] = v[i] := by
rcases v with data, rfl
simp [Array.getElem_push_lt, h]
@[simp] theorem getElem_pop {v : Vector α n} {i : Nat} (h : i < n - 1) : (v.pop)[i] = v[i] := by
rcases v with data, rfl
simp
/--
Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
defeq issues in the implicit size argument.
-/
@[simp] theorem getElem_pop' (v : Vector α (n + 1)) (i : Nat) (h : i < n + 1 - 1) :
@getElem (Vector α n) Nat α (fun _ i => i < n) instGetElemNatLt v.pop i h = v[i] :=
getElem_pop h
@[simp] theorem push_pop_back (v : Vector α (n + 1)) : v.pop.push v.back = v := by
ext i
by_cases h : i < n
· simp [h]
· replace h : i = v.size - 1 := by rw [size_toArray]; omega
subst h
simp [pop, back, back!, Array.eq_push_pop_back!_of_size_ne_zero]
/-! ### mk lemmas -/
theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
@[simp] theorem mk_beq_mk [BEq α] {a b : Array α} {h : a.size = n} {h' : b.size = n} :
(Vector.mk a h == Vector.mk b h') = (a == b) := by
simp [instBEq, isEqv, Array.instBEq, Array.isEqv, h, h']
@[simp] theorem allDiff_mk [BEq α] (a : Array α) (h : a.size = n) :
(Vector.mk a h).allDiff = a.allDiff := rfl
@@ -177,8 +129,30 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
(ha : a.size = n) (hb : b.size = n) : zipWith (Vector.mk a ha) (Vector.mk b hb) f =
Vector.mk (Array.zipWith a b f) (by simp [ha, hb]) := rfl
@[simp] theorem anyM_mk [Monad m] (p : α m Bool) (a : Array α) (h : a.size = n) :
(Vector.mk a h).anyM p = a.anyM p := rfl
@[simp] theorem allM_mk [Monad m] (p : α m Bool) (a : Array α) (h : a.size = n) :
(Vector.mk a h).allM p = a.allM p := rfl
@[simp] theorem any_mk (p : α Bool) (a : Array α) (h : a.size = n) :
(Vector.mk a h).any p = a.any p := rfl
@[simp] theorem all_mk (p : α Bool) (a : Array α) (h : a.size = n) :
(Vector.mk a h).all p = a.all p := rfl
/-! ### toArray lemmas -/
@[simp] theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
xs.toArray[i] = xs[i]'(by simpa using h) := by
cases xs
simp
@[simp] theorem getElem?_toArray {α n} (xs : Vector α n) (i : Nat) :
xs.toArray[i]? = xs[i]? := by
cases xs
simp
@[simp] theorem toArray_append (a : Vector α m) (b : Vector α n) :
(a ++ b).toArray = a.toArray ++ b.toArray := rfl
@@ -212,6 +186,10 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
@[simp] theorem toArray_push (a : Vector α n) (x) : (a.push x).toArray = a.toArray.push x := rfl
@[simp] theorem toArray_beq_toArray [BEq α] (a : Vector α n) (b : Vector α n) :
(a.toArray == b.toArray) = (a == b) := by
simp [instBEq, isEqv, Array.instBEq, Array.isEqv, a.2, b.2]
@[simp] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl
@[simp] theorem toArray_reverse (a : Vector α n) : a.reverse.toArray = a.toArray.reverse := rfl
@@ -247,30 +225,684 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
@[simp] theorem toArray_zipWith (f : α β γ) (a : Vector α n) (b : Vector β n) :
(Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
/-! ### toList lemmas -/
@[simp] theorem anyM_toArray [Monad m] (p : α m Bool) (v : Vector α n) :
v.toArray.anyM p = v.anyM p := by
cases v
simp
@[simp] theorem allM_toArray [Monad m] (p : α m Bool) (v : Vector α n) :
v.toArray.allM p = v.allM p := by
cases v
simp
@[simp] theorem any_toArray (p : α Bool) (v : Vector α n) :
v.toArray.any p = v.any p := by
cases v
simp
@[simp] theorem all_toArray (p : α Bool) (v : Vector α n) :
v.toArray.all p = v.all p := by
cases v
simp
@[simp] theorem toArray_mkVector : (mkVector n a).toArray = mkArray n a := rfl
theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray v = w := by
cases v
cases w
simp
/--
`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]
protected theorem ext {a b : Vector α n} (h : (i : Nat) (_ : i < n) a[i] = b[i]) : a = b := by
apply Vector.toArray_inj.1
apply Array.ext
· rw [a.size_toArray, b.size_toArray]
· intro i hi _
rw [a.size_toArray] at hi
exact h i hi
@[simp] theorem toArray_eq_empty_iff (v : Vector α n) : v.toArray = #[] n = 0 := by
rcases v with v, h
exact by rintro rfl; simp_all, by rintro rfl; simpa using h
@[simp] theorem mem_toArray_iff (a : α) (v : Vector α n) : a v.toArray a v :=
fun h => h, fun h => h
/-! ### toList -/
@[simp] theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
xs.toList[i] = xs[i]'(by simpa using h) := by
cases xs
simp
@[simp] theorem getElem?_toList {α n} (xs : Vector α n) (i : Nat) :
xs.toList[i]? = xs[i]? := by
cases xs
simp
theorem toList_append (a : Vector α m) (b : Vector α n) :
(a ++ b).toList = a.toList ++ b.toList := by simp
@[simp] theorem toList_drop (a : Vector α n) (m) :
(a.drop m).toList = a.toList.drop m := by
simp [List.take_of_length_le]
theorem toList_empty : (#v[] : Vector α 0).toArray = #[] := by simp
theorem toList_mkEmpty (cap) :
(Vector.mkEmpty (α := α) cap).toList = [] := rfl
theorem toList_eraseIdx (a : Vector α n) (i) (h) :
(a.eraseIdx i h).toList = a.toList.eraseIdx i := by simp
@[simp] theorem toList_eraseIdx! (a : Vector α n) (i) (hi : i < n) :
(a.eraseIdx! i).toList = a.toList.eraseIdx i := by
cases a; simp_all [Array.eraseIdx!]
theorem toList_cast (a : Vector α n) (h : n = m) :
(a.cast h).toList = a.toList := rfl
theorem toList_extract (a : Vector α n) (start stop) :
(a.extract start stop).toList = (a.toList.drop start).take (stop - start) := by
simp
theorem toList_map (f : α β) (a : Vector α n) :
(a.map f).toList = a.toList.map f := by simp
theorem toList_ofFn (f : Fin n α) : (Vector.ofFn f).toList = List.ofFn f := by simp
theorem toList_pop (a : Vector α n) : a.pop.toList = a.toList.dropLast := rfl
theorem toList_push (a : Vector α n) (x) : (a.push x).toList = a.toList ++ [x] := by simp
@[simp] theorem toList_beq_toList [BEq α] (a : Vector α n) (b : Vector α n) :
(a.toList == b.toList) = (a == b) := by
simp [instBEq, isEqv, Array.instBEq, Array.isEqv, a.2, b.2]
theorem toList_range : (Vector.range n).toList = List.range n := by simp
theorem toList_reverse (a : Vector α n) : a.reverse.toList = a.toList.reverse := by simp
theorem toList_set (a : Vector α n) (i x h) :
(a.set i x).toList = a.toList.set i x := rfl
@[simp] theorem toList_setIfInBounds (a : Vector α n) (i x) :
(a.setIfInBounds i x).toList = a.toList.set i x := by
simp [Vector.setIfInBounds]
theorem toList_singleton (x : α) : (Vector.singleton x).toList = [x] := rfl
theorem toList_swap (a : Vector α n) (i j) (hi hj) :
(a.swap i j).toList = (a.toList.set i a[j]).set j a[i] := rfl
@[simp] theorem toList_take (a : Vector α n) (m) : (a.take m).toList = a.toList.take m := by
simp [List.take_of_length_le]
@[simp] theorem toList_zipWith (f : α β γ) (a : Vector α n) (b : Vector β n) :
(Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl
@[simp] theorem anyM_toList [Monad m] (p : α m Bool) (v : Vector α n) :
v.toList.anyM p = v.anyM p := by
cases v
simp
@[simp] theorem allM_toList [Monad m] [LawfulMonad m] (p : α m Bool) (v : Vector α n) :
v.toList.allM p = v.allM p := by
cases v
simp
@[simp] theorem any_toList (p : α Bool) (v : Vector α n) :
v.toList.any p = v.any p := by
cases v
simp
@[simp] theorem all_toList (p : α Bool) (v : Vector α n) :
v.toList.all p = v.all p := by
cases v
simp
@[simp] theorem toList_mkVector : (mkVector n a).toList = List.replicate n a := rfl
theorem toList_inj {v w : Vector α n} : v.toList = w.toList v = w := by
cases v
cases w
simp [Array.toList_inj]
@[simp] theorem toList_eq_empty_iff (v : Vector α n) : v.toList = [] n = 0 := by
rcases v with v, h
simp only [Array.toList_eq_nil_iff]
exact by rintro rfl; simp_all, by rintro rfl; simpa using h
@[simp] theorem mem_toList_iff (a : α) (v : Vector α n) : a v.toList a v := by
simp
theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by simp
theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
xs.toList[i] = xs[i]'(by simpa using h) := by simp
/-! ### empty -/
theorem toList_inj {a b : Vector α n} (h : a.toList = b.toList) : a = b := by
rcases a with a, ha
rcases b with b, hb
@[simp] theorem empty_eq {xs : Vector α 0} : #v[] = xs xs = #v[] := by
cases xs
simp
/-- A vector of length `0` is the empty vector. -/
protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
apply Vector.toArray_inj.1
apply Array.eq_empty_of_size_eq_zero v.2
/-! ### size -/
theorem eq_empty_of_size_eq_zero (xs : Vector α n) (h : n = 0) : xs = #v[].cast h.symm := by
rcases xs with xs, rfl
apply toArray_inj.1
simp only [List.length_eq_zero, Array.toList_eq_nil_iff] at h
simp [h]
theorem size_eq_one {xs : Vector α 1} : a, xs = #v[a] := by
rcases xs with xs, h
simpa using Array.size_eq_one.mp h
/-! ### push -/
theorem back_eq_of_push_eq {a b : α} {xs ys : Vector α n} (h : xs.push a = ys.push b) : a = b := by
cases xs
cases ys
replace h := congrArg Vector.toArray h
simp only [push_mk] at h
apply Array.back_eq_of_push_eq h
theorem pop_eq_of_push_eq {a b : α} {xs ys : Vector α n} (h : xs.push a = ys.push b) : xs = ys := by
cases xs
cases ys
replace h := congrArg Vector.toArray h
simp only [push_mk] at h
simpa using Array.pop_eq_of_push_eq h
theorem push_inj_left {a : α} {xs ys : Vector α n} : xs.push a = ys.push a xs = ys :=
pop_eq_of_push_eq, fun h => by simp [h]
theorem push_inj_right {a b : α} {xs : Vector α n} : xs.push a = xs.push b a = b :=
back_eq_of_push_eq, fun h => by simp [h]
theorem push_eq_push {a b : α} {xs ys : Vector α n} : xs.push a = ys.push b a = b xs = ys := by
constructor
· intro h
exact back_eq_of_push_eq h, pop_eq_of_push_eq h
· rintro rfl, rfl
rfl
theorem exists_push {xs : Vector α (n + 1)} :
(ys : Vector α n) (a : α), xs = ys.push a := by
rcases xs with xs, w
obtain ys, a, h := Array.exists_push_of_size_eq_add_one w
exact ys, by simp_all, a, toArray_inj.1 h
theorem singleton_inj : #v[a] = #v[b] a = b := by
simp
/-! ### mkVector -/
@[simp] theorem mkVector_zero : mkVector 0 a = #v[] := rfl
theorem mkVector_succ : mkVector (n + 1) a = (mkVector n a).push a := by
simp [mkVector, Array.mkArray_succ]
theorem mkVector_inj : mkVector n a = mkVector n b n = 0 a = b := by
simp [ toArray_inj, toArray_mkVector, Array.mkArray_inj]
/-! ## L[i] and L[i]? -/
@[simp] theorem getElem?_eq_none_iff {a : Vector α n} : a[i]? = none n i := by
by_cases h : i < n
· simp [getElem?_pos, h]
· rw [getElem?_neg a i h]
simp_all
@[simp] theorem none_eq_getElem?_iff {a : Vector α n} {i : Nat} : none = a[i]? n i := by
simp [eq_comm (a := none)]
theorem getElem?_eq_none {a : Vector α n} (h : n i) : a[i]? = none := by
simp [getElem?_eq_none_iff, h]
@[simp] theorem getElem?_eq_getElem {a : Vector α n} {i : Nat} (h : i < n) : a[i]? = some a[i] :=
getElem?_pos ..
theorem getElem?_eq_some_iff {a : Vector α n} : a[i]? = some b h : i < n, a[i] = b := by
simp [getElem?_def]
theorem some_eq_getElem?_iff {a : Vector α n} : some b = a[i]? h : i < n, a[i] = b := by
rw [eq_comm, getElem?_eq_some_iff]
@[simp] theorem some_getElem_eq_getElem?_iff (a : Vector α n) (i : Nat) (h : i < n) :
(some a[i] = a[i]?) True := by
simp [h]
@[simp] theorem getElem?_eq_some_getElem_iff (a : Vector α n) (i : Nat) (h : i < n) :
(a[i]? = some a[i]) True := by
simp [h]
theorem getElem_eq_iff {a : Vector α n} {i : Nat} {h : i < n} : a[i] = x a[i]? = some x := by
simp only [getElem?_eq_some_iff]
exact fun w => h, w, fun h => h.2
theorem getElem_eq_getElem?_get (a : Vector α n) (i : Nat) (h : i < n) :
a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h]) := by
simp [getElem_eq_iff]
theorem getD_getElem? (a : Vector α n) (i : Nat) (d : α) :
a[i]?.getD d = if p : i < n then a[i]'p else d := by
if h : i < n then
simp [h, getElem?_def]
else
have p : i n := Nat.le_of_not_gt h
simp [getElem?_eq_none p, h]
@[simp] theorem getElem?_empty {n : Nat} : (#v[] : Vector α 0)[n]? = none := rfl
@[simp] theorem getElem_push_lt {v : Vector α n} {x : α} {i : Nat} (h : i < n) :
(v.push x)[i] = v[i] := by
rcases v with data, rfl
simp [Array.getElem_push_lt, h]
@[simp] theorem getElem_push_eq (a : Vector α n) (x : α) : (a.push x)[n] = x := by
rcases a with a, rfl
simp
theorem getElem_push (a : Vector α n) (x : α) (i : Nat) (h : i < n + 1) :
(a.push x)[i] = if h : i < n then a[i] else x := by
rcases a with a, rfl
simp [Array.getElem_push]
theorem getElem?_push {a : Vector α n} {x} : (a.push x)[i]? = if i = n then some x else a[i]? := by
simp [getElem?_def, getElem_push]
(repeat' split) <;> first | rfl | omega
@[simp] theorem getElem?_push_size {a : Vector α n} {x} : (a.push x)[n]? = some x := by
simp [getElem?_push]
@[simp] theorem getElem_singleton (a : α) (h : i < 1) : #v[a][i] = a :=
match i, h with
| 0, _ => rfl
theorem getElem?_singleton (a : α) (i : Nat) : #v[a][i]? = if i = 0 then some a else none := by
simp [List.getElem?_singleton]
/-! ### mem -/
@[simp] theorem getElem_mem {l : Vector α n} {i : Nat} (h : i < n) : l[i] l := by
rcases l with l, rfl
simp
@[simp] theorem not_mem_empty (a : α) : ¬ a #v[] := nofun
@[simp] theorem mem_push {a : Vector α n} {x y : α} : x a.push y x a x = y := by
cases a
simp
theorem mem_push_self {a : Vector α n} {x : α} : x a.push x :=
mem_push.2 (Or.inr rfl)
theorem eq_push_append_of_mem {xs : Vector α n} {x : α} (h : x xs) :
(n₁ n₂ : Nat) (as : Vector α n₁) (bs : Vector α n₂) (h : n₁ + 1 + n₂ = n),
xs = (as.push x ++ bs).cast h x as:= by
rcases xs with xs, rfl
obtain as, bs, h, w := Array.eq_push_append_of_mem (by simpa using h)
simp only at h
obtain rfl := h
exact _, _, as.toVector, bs.toVector, by simp, by simp, by simpa using w
theorem mem_push_of_mem {a : Vector α n} {x : α} (y : α) (h : x a) : x a.push y :=
mem_push.2 (Or.inl h)
theorem exists_mem_of_size_pos (l : Vector α n) (h : 0 < n) : x, x l := by
simpa using List.exists_mem_of_ne_nil l.toList (by simpa using (Nat.ne_of_gt h))
theorem size_zero_iff_forall_not_mem {l : Vector α n} : n = 0 a, a l := by
simpa using List.eq_nil_iff_forall_not_mem (l := l.toList)
@[simp] theorem mem_dite_empty_left {x : α} [Decidable p] {l : ¬ p Vector α 0} :
(x if h : p then #v[] else l h) h : ¬ p, x l h := by
split <;> simp_all
@[simp] theorem mem_dite_empty_right {x : α} [Decidable p] {l : p Vector α 0} :
(x if h : p then l h else #v[]) h : p, x l h := by
split <;> simp_all
@[simp] theorem mem_ite_empty_left {x : α} [Decidable p] {l : Vector α 0} :
(x if p then #v[] else l) ¬ p x l := by
split <;> simp_all
@[simp] theorem mem_ite_empty_right {x : α} [Decidable p] {l : Vector α 0} :
(x if p then l else #v[]) p x l := by
split <;> simp_all
theorem eq_of_mem_singleton (h : a #v[b]) : a = b := by
simpa using h
@[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
cases xs
simp [or_comm, forall_eq_or_imp]
theorem forall_mem_ne {a : α} {l : Vector α n} : ( a' : α, a' l ¬a = a') a l :=
fun h m => h _ m rfl, fun h _ m e => h (e.symm m)
theorem forall_mem_ne' {a : α} {l : Vector α n} : ( a' : α, a' l ¬a' = a) a l :=
fun h m => h _ m rfl, fun h _ m e => h (e.symm m)
theorem exists_mem_empty (p : α Prop) : ¬ ( x, _ : x #v[], p x) := nofun
theorem forall_mem_empty (p : α Prop) : (x) (_ : x #v[]), p x := nofun
theorem exists_mem_push {p : α Prop} {a : α} {xs : Vector α n} :
( x, _ : x xs.push a, p x) p a x, _ : x xs, p x := by
simp only [mem_push, exists_prop]
constructor
· rintro x, (h | rfl), h'
· exact .inr x, h, h'
· exact .inl h'
· rintro (h | x, h, h')
· exact a, by simp, h
· exact x, .inl h, h'
theorem forall_mem_singleton {p : α Prop} {a : α} : ( (x) (_ : x #v[a]), p x) p a := by
simp only [mem_singleton, forall_eq]
theorem mem_empty_iff (a : α) : a (#v[] : Vector α 0) False := by simp
theorem mem_singleton_self (a : α) : a #v[a] := by simp
theorem mem_of_mem_push_of_mem {a b : α} {l : Vector α n} : a l.push b b l a l := by
rcases l with l, rfl
simpa using Array.mem_of_mem_push_of_mem
theorem eq_or_ne_mem_of_mem {a b : α} {l : Vector α n} (h' : a l.push b) :
a = b (a b a l) := by
if h : a = b then
exact .inl h
else
simp only [mem_push, h, or_false] at h'
exact .inr h, h'
theorem size_ne_zero_of_mem {a : α} {l : Vector α n} (h : a l) : n 0 := by
rcases l with l, rfl
simpa using Array.ne_empty_of_mem (by simpa using h)
theorem mem_of_ne_of_mem {a y : α} {l : Vector α n} (h₁ : a y) (h₂ : a l.push y) : a l := by
simpa [h₁] using h₂
theorem ne_of_not_mem_push {a b : α} {l : Vector α n} (h : a l.push b) : a b := by
simp only [mem_push, not_or] at h
exact h.2
theorem not_mem_of_not_mem_push {a b : α} {l : Vector α n} (h : a l.push b) : a l := by
simp only [mem_push, not_or] at h
exact h.1
theorem not_mem_push_of_ne_of_not_mem {a y : α} {l : Vector α n} : a y a l a l.push y :=
mt mem_of_ne_of_mem
theorem ne_and_not_mem_of_not_mem_push {a y : α} {l : Vector α n} : a l.push y a y a l := by
simp +contextual
theorem getElem_of_mem {a} {l : Vector α n} (h : a l) : (i : Nat) (h : i < n), l[i]'h = a := by
rcases l with l, rfl
simpa using Array.getElem_of_mem (by simpa using h)
theorem getElem?_of_mem {a} {l : Vector α n} (h : a l) : i : Nat, l[i]? = some a :=
let n, _, e := getElem_of_mem h; n, e getElem?_eq_getElem _
theorem mem_of_getElem? {l : Vector α n} {i : Nat} {a : α} (e : l[i]? = some a) : a l :=
let _, e := getElem?_eq_some_iff.1 e; e getElem_mem ..
theorem mem_iff_getElem {a} {l : Vector α n} : a l (i : Nat) (h : i < n), l[i]'h = a :=
getElem_of_mem, fun _, _, e => e getElem_mem ..
theorem mem_iff_getElem? {a} {l : Vector α n} : a l i : Nat, l[i]? = some a := by
simp [getElem?_eq_some_iff, mem_iff_getElem]
theorem forall_getElem {l : Vector α n} {p : α Prop} :
( (i : Nat) h, p (l[i]'h)) a, a l p a := by
rcases l with l, rfl
simp [Array.forall_getElem]
/-! ### Decidability of bounded quantifiers -/
instance {xs : Vector α n} {p : α Prop} [DecidablePred p] :
Decidable ( x, x xs p x) :=
decidable_of_iff ( (i : Nat) h, p (xs[i]'h)) (by
simp only [mem_iff_getElem, forall_exists_index]
exact
by rintro w _ i h rfl; exact w i h, fun w i h => w _ i h rfl)
instance {xs : Vector α n} {p : α Prop} [DecidablePred p] :
Decidable ( x, x xs p x) :=
decidable_of_iff ( (i : Nat), (h : i < n), p (xs[i]'h)) (by
simp [mem_iff_getElem]
exact
by rintro i, h, w; exact _, i, h, rfl, w, fun _, i, h, rfl, w => i, h, w)
/-! ### any / all -/
theorem any_iff_exists {p : α Bool} {xs : Vector α n} :
xs.any p (i : Nat) (_ : i < n), p xs[i] := by
rcases xs with xs, rfl
simp [Array.any_iff_exists]
theorem all_iff_forall {p : α Bool} {xs : Vector α n} :
xs.all p (i : Nat) (_ : i < n), p xs[i] := by
rcases xs with xs, rfl
simp [Array.all_iff_forall]
theorem any_eq_true {p : α Bool} {xs : Vector α n} :
xs.any p = true (i : Nat) (_ : i < n), p xs[i] := by
simp [any_iff_exists]
theorem any_eq_false {p : α Bool} {xs : Vector α n} :
xs.any p = false (i : Nat) (_ : i < n), ¬p xs[i] := by
rw [Bool.eq_false_iff, Ne, any_eq_true]
simp
theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α m Bool} {xs : Vector α n} :
xs.allM p = (! ·) <$> xs.anyM ((! ·) <$> p ·) := by
rcases xs with xs, rfl
simp [Array.allM_eq_not_anyM_not]
theorem all_eq_not_any_not {p : α Bool} {xs : Vector α n} :
xs.all p = !(xs.any (!p ·)) := by
rcases xs with xs, rfl
simp [Array.all_eq_not_any_not]
@[simp] theorem all_eq_true {p : α Bool} {xs : Vector α n} :
xs.all p = true (i : Nat) (_ : i < n), p xs[i] := by
simp [all_iff_forall]
@[simp] theorem all_eq_false {p : α Bool} {xs : Vector α n} :
xs.all p = false (i : Nat) (_ : i < n), ¬p xs[i] := by
rw [Bool.eq_false_iff, Ne, all_eq_true]
simp
theorem all_eq_true_iff_forall_mem {xs : Vector α n} : xs.all p x, x xs p x := by
rcases xs with xs, rfl
simp only [all_mk, Array.all_eq_true_iff_forall_mem]
simp
/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
theorem any_eq_true' {p : α Bool} {xs : Vector α n} :
xs.any p = true ( x, x xs p x) := by
rcases xs with xs, rfl
simp only [any_mk, Array.any_eq_true']
simp
/-- Variant of `any_eq_false` in terms of membership rather than an array index. -/
theorem any_eq_false' {p : α Bool} {xs : Vector α n} :
xs.any p = false x, x xs ¬p x := by
rcases xs with xs, rfl
simp only [any_mk, Array.any_eq_false']
simp
/-- Variant of `all_eq_true` in terms of membership rather than an array index. -/
theorem all_eq_true' {p : α Bool} {xs : Vector α n} :
xs.all p = true x, x xs p x := by
rcases xs with xs, rfl
simp only [all_mk, Array.all_eq_true']
simp
/-- Variant of `all_eq_false` in terms of membership rather than an array index. -/
theorem all_eq_false' {p : α Bool} {xs : Vector α n} :
xs.all p = false x, x xs ¬p x := by
rcases xs with xs, rfl
simp only [all_mk, Array.all_eq_false']
simp
theorem any_eq {xs : Vector α n} {p : α Bool} : xs.any p = decide ( i : Nat, h, p (xs[i]'h)) := by
by_cases h : xs.any p
· simp_all [any_eq_true]
· simp_all [any_eq_false]
/-- Variant of `any_eq` in terms of membership rather than an array index. -/
theorem any_eq' {xs : Vector α n} {p : α Bool} : xs.any p = decide ( x, x xs p x) := by
by_cases h : xs.any p
· simp_all [any_eq_true']
· simp only [Bool.not_eq_true] at h
simp only [h]
simp only [any_eq_false'] at h
simpa using h
theorem all_eq {xs : Vector α n} {p : α Bool} : xs.all p = decide ( i, (_ : i < n) p xs[i]) := by
by_cases h : xs.all p
· simp_all [all_eq_true]
· simp only [Bool.not_eq_true] at h
simp only [h]
simp only [all_eq_false] at h
simpa using h
/-- Variant of `all_eq` in terms of membership rather than an array index. -/
theorem all_eq' {xs : Vector α n} {p : α Bool} : xs.all p = decide ( x, x xs p x) := by
rcases xs with xs, rfl
simp only [all_mk, Array.all_eq']
simp
theorem decide_exists_mem {xs : Vector α n} {p : α Prop} [DecidablePred p] :
decide ( x, x xs p x) = xs.any p := by
simp [any_eq']
theorem decide_forall_mem {xs : Vector α n} {p : α Prop} [DecidablePred p] :
decide ( x, x xs p x) = xs.all p := by
simp [all_eq']
theorem any_beq [BEq α] {xs : Vector α n} {a : α} : (xs.any fun x => a == x) = xs.contains a := by
rcases xs with xs, rfl
simp [Array.any_beq]
/-- Variant of `any_beq` with `==` reversed. -/
theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Vector α n} :
(xs.any fun x => x == a) = xs.contains a := by
simp only [BEq.comm, any_beq]
theorem all_bne [BEq α] {xs : Vector α n} : (xs.all fun x => a != x) = !xs.contains a := by
rcases xs with xs, rfl
simp [Array.all_bne]
/-- Variant of `all_bne` with `!=` reversed. -/
theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Vector α n} :
(xs.all fun x => x != a) = !xs.contains a := by
simp only [bne_comm, all_bne]
theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
as.contains a = true a as := by
rcases as with as, rfl
simp [Array.mem_of_contains_eq_true]
theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} (h : a as) :
as.contains a = true := by
rcases as with as, rfl
simp only [mem_mk] at h
simp [Array.contains_eq_true_of_mem, h]
instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a as) :=
decidable_of_decidable_of_iff (Iff.intro mem_of_contains_eq_true contains_eq_true_of_mem)
theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
as.contains a = true a as := mem_of_contains_eq_true, contains_eq_true_of_mem
@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
as.contains a = decide (a as) := by
rw [Bool.eq_iff_iff, contains_iff, decide_eq_true_iff]
@[simp] theorem any_push [BEq α] {as : Vector α n} {a : α} {p : α Bool} :
(as.push a).any p = (as.any p || p a) := by
rcases as with as, rfl
simp [Array.any_push]
@[simp] theorem all_push [BEq α] {as : Vector α n} {a : α} {p : α Bool} :
(as.push a).all p = (as.all p && p a) := by
rcases as with as, rfl
simp [Array.all_push]
@[simp] theorem contains_push [BEq α] {l : Vector α n} {a : α} {b : α} :
(l.push a).contains b = (l.contains b || b == a) := by
rcases l with l, rfl
simp [Array.contains_push]
/-! ### set -/
theorem getElem_set (a : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat) (hj : j < n) :
(a.set i x hi)[j] = if i = j then x else a[j] := by
cases a
theorem getElem_set (v : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat) (hj : j < n) :
(v.set i x hi)[j] = if i = j then x else v[j] := by
cases v
split <;> simp_all [Array.getElem_set]
@[simp] theorem getElem_set_eq (a : Vector α n) (i : Nat) (x : α) (hi : i < n) :
(a.set i x hi)[i] = x := by simp [getElem_set]
@[simp] theorem getElem_set_self (v : Vector α n) (i : Nat) (x : α) (hi : i < n) :
(v.set i x hi)[i] = x := by simp [getElem_set]
@[simp] theorem getElem_set_ne (a : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat)
(hj : j < n) (h : i j) : (a.set i x hi)[j] = a[j] := by simp [getElem_set, h]
@[deprecated getElem_set_self (since := "2024-12-12")]
abbrev getElem_set_eq := @getElem_set_self
@[simp] theorem getElem_set_ne (v : Vector α n) (i : Nat) (x : α) (hi : i < n) (j : Nat)
(hj : j < n) (h : i j) : (v.set i x hi)[j] = v[j] := by simp [getElem_set, h]
theorem getElem?_set (v : Vector α n) (i : Nat) (hi : i < n) (x : α) (j : Nat) :
(v.set i x hi)[j]? = if i = j then some x else v[j]? := by
cases v
split <;> simp_all [getElem?_eq_getElem, getElem_set]
@[simp] theorem getElem?_set_self (v : Vector α n) (i : Nat) (hi : i < n) (x : α) :
(v.set i x hi)[i]? = some x := by simp [getElem?_eq_getElem, hi]
@[simp] theorem getElem?_set_ne (v : Vector α n) (i : Nat) (hi : i < n) (x : α) (j : Nat)
(h : i j) : (v.set i x hi)[j]? = v[j]? := by
simp [getElem?_set, h]
@[simp] theorem set_getElem_self {v : Vector α n} {i : Nat} (hi : i < n) :
v.set i v[i] hi = v := by
cases v
simp
theorem set_comm (a b : α) {i j : Nat} (v : Vector α n) {hi : i < n} {hj : j < n} (h : i j) :
(v.set i a hi).set j b hj = (v.set j b hj).set i a hi := by
cases v
simp [Array.set_comm, h]
@[simp] theorem set_set (a b : α) (v : Vector α n) (i : Nat) (hi : i < n) :
(v.set i a hi).set i b hi = v.set i b hi := by
cases v
simp
theorem mem_set (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
a v.set i a hi := by
simp [mem_iff_getElem]
exact i, (by simpa using hi), by simp
theorem mem_or_eq_of_mem_set {v : Vector α n} {i : Nat} {a b : α} {w : i < n} (h : a v.set i b) : a v a = b := by
cases v
simpa using Array.mem_or_eq_of_mem_set (by simpa using h)
/-! ### setIfInBounds -/
@@ -279,11 +911,146 @@ theorem getElem_setIfInBounds (a : Vector α n) (i : Nat) (x : α) (j : Nat)
cases a
split <;> simp_all [Array.getElem_setIfInBounds]
@[simp] theorem getElem_setIfInBounds_eq (a : Vector α n) (i : Nat) (x : α) (hj : i < n) :
(a.setIfInBounds i x)[i] = x := by simp [getElem_setIfInBounds]
@[simp] theorem getElem_setIfInBounds_self (v : Vector α n) (i : Nat) (x : α) (hi : i < n) :
(v.setIfInBounds i x)[i] = x := by simp [getElem_setIfInBounds, hi]
@[simp] theorem getElem_setIfInBounds_ne (a : Vector α n) (i : Nat) (x : α) (j : Nat)
(hj : j < n) (h : i j) : (a.setIfInBounds i x)[j] = a[j] := by simp [getElem_setIfInBounds, h]
@[deprecated getElem_setIfInBounds_self (since := "2024-12-12")]
abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
@[simp] theorem getElem_setIfInBounds_ne (v : Vector α n) (i : Nat) (x : α) (j : Nat)
(hj : j < n) (h : i j) : (v.setIfInBounds i x)[j] = v[j] := by simp [getElem_setIfInBounds, h]
theorem getElem?_setIfInBounds (v : Vector α n) (i : Nat) (x : α) (j : Nat) :
(v.setIfInBounds i x)[j]? = if i = j then if i < n then some x else none else v[j]? := by
rcases v with v, rfl
simp [Array.getElem?_setIfInBounds]
theorem getElem?_setIfInBounds_self (v : Vector α n) (i : Nat) (x : α) :
(v.setIfInBounds i x)[i]? = if i < n then some x else none := by simp [getElem?_setIfInBounds]
@[simp] theorem getElem?_setIfInBounds_self_of_lt (v : Vector α n) (i : Nat) (x : α) (h : i < n) :
(v.setIfInBounds i x)[i]? = some x := by simp [getElem?_setIfInBounds, h]
@[simp] theorem getElem?_setIfInBounds_ne (a : Vector α n) (i : Nat) (x : α) (j : Nat)
(h : i j) : (a.setIfInBounds i x)[j]? = a[j]? := by simp [getElem?_setIfInBounds, h]
theorem setIfInBounds_eq_of_size_le {l : Vector α n} {m : Nat} (h : l.size m) {a : α} :
l.setIfInBounds m a = l := by
rcases l with l, rfl
simp [Array.setIfInBounds_eq_of_size_le (by simpa using h)]
theorem setIfInBound_comm (a b : α) {i j : Nat} (v : Vector α n) (h : i j) :
(v.setIfInBounds i a).setIfInBounds j b = (v.setIfInBounds j b).setIfInBounds i a := by
rcases v with v, rfl
simp only [setIfInBounds_mk, mk.injEq]
rw [Array.setIfInBounds_comm _ _ _ h]
@[simp] theorem setIfInBounds_setIfInBounds (a b : α) (v : Vector α n) (i : Nat) :
(v.setIfInBounds i a).setIfInBounds i b = v.setIfInBounds i b := by
rcases v with v, rfl
simp
theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
a v.setIfInBounds i a := by
simp [mem_iff_getElem]
exact i, (by simpa using hi), by simp
/-! ### BEq -/
@[simp] theorem push_beq_push [BEq α] {a b : α} {n : Nat} {v : Vector α n} {w : Vector α n} :
(v.push a == w.push b) = (v == w && a == b) := by
cases v
cases w
simp
@[simp] theorem mkVector_beq_mkVector [BEq α] {a b : α} {n : Nat} :
(mkVector n a == mkVector n b) = (n == 0 || a == b) := by
cases n with
| zero => simp
| succ n =>
rw [mkVector_succ, mkVector_succ, push_beq_push, mkVector_beq_mkVector]
rw [Bool.eq_iff_iff]
simp +contextual
@[simp] theorem reflBEq_iff [BEq α] [NeZero n] : ReflBEq (Vector α n) ReflBEq α := by
match n, NeZero.ne n with
| n + 1, _ =>
constructor
· intro h
constructor
intro a
suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this
exact this.2
simp
· intro h
constructor
rintro v, h
simpa using Array.isEqv_self_beq ..
@[simp] theorem lawfulBEq_iff [BEq α] [NeZero n] : LawfulBEq (Vector α n) LawfulBEq α := by
match n, NeZero.ne n with
| n + 1, _ =>
constructor
· intro h
constructor
· intro a b h
have := mkVector_inj (n := n+1) (a := a) (b := b)
simp only [Nat.add_one_ne_zero, false_or] at this
rw [ this]
apply eq_of_beq
rw [mkVector_beq_mkVector]
simpa
· intro a
suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
rw [mkVector_beq_mkVector] at this
simpa
simp
· intro h
constructor
· rintro a, ha b, hb h
simp at h
obtain hs, hi := Array.rel_of_isEqv h
ext i h
· simpa using hi _ (by omega)
· rintro a, ha
simpa using Array.isEqv_self_beq ..
/-! Content below this point has not yet been aligned with `List` and `Array`. -/
@[simp] theorem getElem_ofFn {α n} (f : Fin n α) (i : Nat) (h : i < n) :
(Vector.ofFn f)[i] = f i, by simpa using h := by
simp [ofFn]
/-- The empty vector maps to the empty vector. -/
@[simp]
theorem map_empty (f : α β) : map f #v[] = #v[] := by
rw [map, mk.injEq]
exact Array.map_empty f
@[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
rcases v with data, rfl
simp
@[simp] theorem getElem_pop {v : Vector α n} {i : Nat} (h : i < n - 1) : (v.pop)[i] = v[i] := by
rcases v with data, rfl
simp
/--
Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
defeq issues in the implicit size argument.
-/
@[simp] theorem getElem_pop' (v : Vector α (n + 1)) (i : Nat) (h : i < n + 1 - 1) :
@getElem (Vector α n) Nat α (fun _ i => i < n) instGetElemNatLt v.pop i h = v[i] :=
getElem_pop h
@[simp] theorem push_pop_back (v : Vector α (n + 1)) : v.pop.push v.back = v := by
ext i
by_cases h : i < n
· simp [h]
· replace h : i = v.size - 1 := by rw [size_toArray]; omega
subst h
simp [pop, back, back!, Array.eq_push_pop_back!_of_size_ne_zero]
/-! ### append -/

View File

@@ -176,11 +176,14 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
simp only [getElem?_def] at h
split <;> simp_all
@[simp] theorem isNone_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isNone = ¬dom c i := by
@[simp] theorem getElem?_eq_none [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = none ¬dom c i := by
simp only [getElem?_def]
split <;> simp_all
@[deprecated getElem?_eq_none (since := "2024-12-11")]
abbrev isNone_getElem? := @getElem?_eq_none
@[simp] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by
simp only [getElem?_def]

View File

@@ -168,11 +168,6 @@ end Lean
| `($(_) $c $t $e) => `(if $c then $t else $e)
| _ => throw ()
@[app_unexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
| `($(_) $_) => `(sorry)
| `($(_) $_ $_) => `(sorry)
| _ => throw ()
@[app_unexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
| `($(_) $m $h) => `($h $m)
| _ => throw ()

View File

@@ -645,23 +645,22 @@ set_option linter.unusedVariables.funArgs false in
@[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a
/--
Auxiliary axiom used to implement `sorry`.
Auxiliary axiom used to implement the `sorry` term and tactic.
The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`. This is a
proof of anything, which is intended for stubbing out incomplete parts of a
proof while still having a syntactically correct proof skeleton. Lean will give
a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but
you can double check if a theorem depends on `sorry` by using
`#print axioms my_thm` and looking for `sorryAx` in the axiom list.
The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`.
It is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
but you can check if a declaration depends on `sorry` either directly or indirectly by looking for `sorryAx` in the output
of the `#print axioms my_thm` command.
The `synthetic` flag is false when written explicitly by the user, but it is
The `synthetic` flag is false when a `sorry` is written explicitly by the user, but it is
set to `true` when a tactic fails to prove a goal, or if there is a type error
in the expression. A synthetic `sorry` acts like a regular one, except that it
suppresses follow-up errors in order to prevent one error from causing a cascade
suppresses follow-up errors in order to prevent an error from causing a cascade
of other errors because the desired term was not constructed.
-/
@[extern "lean_sorry", never_extract]
axiom sorryAx (α : Sort u) (synthetic := false) : α
axiom sorryAx (α : Sort u) (synthetic : Bool) : α
theorem eq_false_of_ne_true : {b : Bool} Not (Eq b true) Eq b false
| true, h => False.elim (h rfl)
@@ -860,8 +859,8 @@ abbrev DecidablePred {α : Sort u} (r : α → Prop) :=
(a : α) Decidable (r a)
/-- A decidable relation. See `Decidable`. -/
abbrev DecidableRel {α : Sort u} (r : α α Prop) :=
(a b : α) Decidable (r a b)
abbrev DecidableRel {α : Sort u} {β : Sort v} (r : α β Prop) :=
(a : α) (b : β) Decidable (r a b)
/--
Asserts that `α` has decidable equality, that is, `a = b` is decidable
@@ -3932,6 +3931,13 @@ def getId : Syntax → Name
| ident _ _ val _ => val
| _ => Name.anonymous
/-- Retrieve the immediate info from the Syntax node. -/
def getInfo? : Syntax Option SourceInfo
| atom info .. => some info
| ident info .. => some info
| node info .. => some info
| missing => none
/-- Retrieve the left-most node or leaf's info in the Syntax tree. -/
partial def getHeadInfo? : Syntax Option SourceInfo
| atom info _ => some info

View File

@@ -153,6 +153,7 @@ instance : Std.LawfulIdentity Or False where
@[simp] theorem false_implies (p : Prop) : (False p) = True := eq_true False.elim
@[simp] theorem forall_false (p : False Prop) : ( h : False, p h) = True := eq_true (False.elim ·)
@[simp] theorem implies_true (α : Sort u) : (α True) = True := eq_true fun _ => trivial
-- This is later proved by the simp lemma `forall_const`, but this is useful during bootstrapping.
@[simp] theorem true_implies (p : Prop) : (True p) = p := propext (· trivial), (fun _ => ·)
@[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim
@[simp] theorem not_true_eq_false : (¬ True) = False := by decide

View File

@@ -408,16 +408,18 @@ example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
syntax (name := acRfl) "ac_rfl" : tactic
/--
The `sorry` tactic closes the goal using `sorryAx`. This is intended for stubbing out incomplete
parts of a proof while still having a syntactically correct proof skeleton. Lean will give
a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but
you can double check if a theorem depends on `sorry` by using
`#print axioms my_thm` and looking for `sorryAx` in the axiom list.
-/
macro "sorry" : tactic => `(tactic| exact @sorryAx _ false)
The `sorry` tactic is a temporary placeholder for an incomplete tactic proof,
closing the main goal using `exact sorry`.
/-- `admit` is a shorthand for `exact sorry`. -/
macro "admit" : tactic => `(tactic| exact @sorryAx _ false)
This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton.
Lean will give a warning whenever a proof uses `sorry`, so you aren't likely to miss it,
but you can double check if a theorem depends on `sorry` by looking for `sorryAx` in the output
of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.
-/
macro "sorry" : tactic => `(tactic| exact sorry)
/-- `admit` is a synonym for `sorry`. -/
macro "admit" : tactic => `(tactic| sorry)
/--
`infer_instance` is an abbreviation for `exact inferInstance`.

View File

@@ -35,7 +35,6 @@ import Lean.Compiler.LCNF.ToLCNF
import Lean.Compiler.LCNF.Types
import Lean.Compiler.LCNF.Util
import Lean.Compiler.LCNF.ConfigOptions
import Lean.Compiler.LCNF.ForEachExpr
import Lean.Compiler.LCNF.MonoTypes
import Lean.Compiler.LCNF.ToMono
import Lean.Compiler.LCNF.MonadScope

View File

@@ -1,14 +0,0 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Util.ForEachExpr
import Lean.Compiler.LCNF.Basic
namespace Lean.Compiler.LCNF
-- TODO: delete
end Lean.Compiler.LCNF

View File

@@ -29,7 +29,7 @@ and `[specialize]` since they can be partially applied.
def shouldGenerateCode (declName : Name) : CoreM Bool := do
if ( isCompIrrelevant |>.run') then return false
let some info getDeclInfo? declName | return false
unless info.hasValue do return false
unless info.hasValue (allowOpaque := true) do return false
let env getEnv
if isExtern env declName then return false
if hasMacroInlineAttribute env declName then return false

View File

@@ -7,7 +7,6 @@ prelude
import Lean.Compiler.LCNF.CompilerM
import Lean.Compiler.LCNF.PassManager
import Lean.Compiler.LCNF.PhaseExt
import Lean.Compiler.LCNF.ForEachExpr
namespace Lean.Compiler.LCNF

View File

@@ -96,7 +96,7 @@ The steps for this are roughly:
def toDecl (declName : Name) : CompilerM Decl := do
let declName := if let some name := isUnsafeRecName? declName then name else declName
let some info getDeclInfo? declName | throwError "declaration `{declName}` not found"
let some value := info.value? | throwError "declaration `{declName}` does not have a value"
let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value"
let (type, value) Meta.MetaM.run' do
let type toLCNFType info.type
let value Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs ( Meta.etaExpand body)
@@ -107,7 +107,7 @@ def toDecl (declName : Name) : CompilerM Decl := do
/- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macro_inline]`. -/
let value macroInline value
/-
Remark: we have disabled the following transformation, we will perform it at phase 2, after code specialization.
Remark: we have disabled the following transformatbion, we will perform it at phase 2, after code specialization.
It prevents many optimizations (e.g., "cases-of-ctor").
-/
-- let value ← applyCasesOnImplementedBy value

View File

@@ -612,14 +612,14 @@ instance : MonadRuntimeException CoreM where
/--
Returns `true` if the given message kind has not been reported in the message log,
and then mark it as reported. Otherwise, returns `false`.
We use this API to ensure we don't report the same kind of warning multiple times.
and then mark it as logged. Otherwise, returns `false`.
We use this API to ensure we don't log the same kind of warning multiple times.
-/
def reportMessageKind (kind : Name) : CoreM Bool := do
if ( get).messages.reportedKinds.contains kind then
def logMessageKind (kind : Name) : CoreM Bool := do
if ( get).messages.loggedKinds.contains kind then
return false
else
modify fun s => { s with messages.reportedKinds := s.messages.reportedKinds.insert kind }
modify fun s => { s with messages.loggedKinds := s.messages.loggedKinds.insert kind }
return true
end Lean

View File

@@ -0,0 +1,49 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Data.Position
/-!
# Data types for declaration ranges
The environment extension for declaration ranges is in `Lean.DeclarationRange`.
-/
namespace Lean
/-- Store position information for declarations. -/
structure DeclarationRange where
pos : Position
/-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
file, which is IO-heavy. -/
charUtf16 : Nat
endPos : Position
/-- See `charUtf16`. -/
endCharUtf16 : Nat
deriving Inhabited, DecidableEq, Repr
instance : ToExpr DeclarationRange where
toExpr r := mkAppN (mkConst ``DeclarationRange.mk) #[toExpr r.pos, toExpr r.charUtf16, toExpr r.endPos, toExpr r.endCharUtf16]
toTypeExpr := mkConst ``DeclarationRange
structure DeclarationRanges where
range : DeclarationRange
selectionRange : DeclarationRange
deriving Inhabited, Repr
instance : ToExpr DeclarationRanges where
toExpr r := mkAppN (mkConst ``DeclarationRanges.mk) #[toExpr r.range, toExpr r.selectionRange]
toTypeExpr := mkConst ``DeclarationRanges
/--
A declaration location is a declaration range along with the name of the module the declaration resides in.
-/
structure DeclarationLocation where
module : Name
range : DeclarationRange
deriving Inhabited, DecidableEq, Repr

View File

@@ -55,7 +55,7 @@ where
go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by
induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n)
case case1 => simp [ofFn.go, size]; omega
case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega
case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega
section Meta
open Lean

View File

@@ -44,7 +44,7 @@ def mkReducibilityHintsRegularEx (h : UInt32) : ReducibilityHints :=
@[export lean_reducibility_hints_get_height]
def ReducibilityHints.getHeightEx (h : ReducibilityHints) : UInt32 :=
match h with
| ReducibilityHints.regular h => h
| .regular h => h
| _ => 0
namespace ReducibilityHints
@@ -74,8 +74,8 @@ def isAbbrev : ReducibilityHints → Bool
| _ => false
def isRegular : ReducibilityHints Bool
| regular .. => true
| _ => false
| .regular .. => true
| _ => false
end ReducibilityHints
@@ -186,7 +186,7 @@ def mkInductiveDeclEs (lparams : List Name) (nparams : Nat) (types : List Induct
@[export lean_is_unsafe_inductive_decl]
def Declaration.isUnsafeInductiveDeclEx : Declaration Bool
| Declaration.inductDecl _ _ _ isUnsafe => isUnsafe
| .inductDecl _ _ _ isUnsafe => isUnsafe
| _ => false
def Declaration.definitionVal! : Declaration DefinitionVal
@@ -195,18 +195,16 @@ def Declaration.definitionVal! : Declaration → DefinitionVal
@[specialize] def Declaration.foldExprM {α} {m : Type Type} [Monad m] (d : Declaration) (f : α Expr m α) (a : α) : m α :=
match d with
| Declaration.quotDecl => pure a
| Declaration.axiomDecl { type := type, .. } => f a type
| Declaration.defnDecl { type := type, value := value, .. } => do let a f a type; f a value
| Declaration.opaqueDecl { type := type, value := value, .. } => do let a f a type; f a value
| Declaration.thmDecl { type := type, value := value, .. } => do let a f a type; f a value
| Declaration.mutualDefnDecl vals => vals.foldlM (fun a v => do let a f a v.type; f a v.value) a
| Declaration.inductDecl _ _ inductTypes _ =>
inductTypes.foldlM
(fun a inductType => do
let a f a inductType.type
inductType.ctors.foldlM (fun a ctor => f a ctor.type) a)
a
| .quotDecl => pure a
| .axiomDecl { type := type, .. } => f a type
| .defnDecl { type := type, value := value, .. } => do let a f a type; f a value
| .opaqueDecl { type := type, value := value, .. } => do let a f a type; f a value
| .thmDecl { type := type, value := value, .. } => do let a f a type; f a value
| .mutualDefnDecl vals => vals.foldlM (fun a v => do let a f a v.type; f a v.value) a
| .inductDecl _ _ inductTypes _ =>
inductTypes.foldlM (init := a) fun a inductType => do
let a f a inductType.type
inductType.ctors.foldlM (fun a ctor => f a ctor.type) a
@[inline] def Declaration.forExprM {m : Type Type} [Monad m] (d : Declaration) (f : Expr m Unit) : m Unit :=
d.foldExprM (fun _ a => f a) ()
@@ -302,14 +300,7 @@ structure ConstructorVal extends ConstantVal where
@[export lean_mk_constructor_val]
def mkConstructorValEx (name : Name) (levelParams : List Name) (type : Expr) (induct : Name) (cidx numParams numFields : Nat) (isUnsafe : Bool) : ConstructorVal := {
name := name,
levelParams := levelParams,
type := type,
induct := induct,
cidx := cidx,
numParams := numParams,
numFields := numFields,
isUnsafe := isUnsafe
name, levelParams, type, induct, cidx, numParams, numFields, isUnsafe
}
@[export lean_constructor_val_is_unsafe] def ConstructorVal.isUnsafeEx (v : ConstructorVal) : Bool := v.isUnsafe
@@ -353,8 +344,8 @@ structure RecursorVal extends ConstantVal where
@[export lean_mk_recursor_val]
def mkRecursorValEx (name : Name) (levelParams : List Name) (type : Expr) (all : List Name) (numParams numIndices numMotives numMinors : Nat)
(rules : List RecursorRule) (k isUnsafe : Bool) : RecursorVal := {
name := name, levelParams := levelParams, type := type, all := all, numParams := numParams, numIndices := numIndices,
numMotives := numMotives, numMinors := numMinors, rules := rules, k := k, isUnsafe := isUnsafe
name, levelParams, type, all, numParams, numIndices,
numMotives, numMinors, rules, k, isUnsafe
}
@[export lean_recursor_k] def RecursorVal.kEx (v : RecursorVal) : Bool := v.k
@@ -410,27 +401,27 @@ inductive ConstantInfo where
namespace ConstantInfo
def toConstantVal : ConstantInfo ConstantVal
| defnInfo {toConstantVal := d, ..} => d
| axiomInfo {toConstantVal := d, ..} => d
| thmInfo {toConstantVal := d, ..} => d
| opaqueInfo {toConstantVal := d, ..} => d
| quotInfo {toConstantVal := d, ..} => d
| inductInfo {toConstantVal := d, ..} => d
| ctorInfo {toConstantVal := d, ..} => d
| recInfo {toConstantVal := d, ..} => d
| .defnInfo {toConstantVal := d, ..} => d
| .axiomInfo {toConstantVal := d, ..} => d
| .thmInfo {toConstantVal := d, ..} => d
| .opaqueInfo {toConstantVal := d, ..} => d
| .quotInfo {toConstantVal := d, ..} => d
| .inductInfo {toConstantVal := d, ..} => d
| .ctorInfo {toConstantVal := d, ..} => d
| .recInfo {toConstantVal := d, ..} => d
def isUnsafe : ConstantInfo Bool
| defnInfo v => v.safety == .unsafe
| axiomInfo v => v.isUnsafe
| thmInfo _ => false
| opaqueInfo v => v.isUnsafe
| quotInfo _ => false
| inductInfo v => v.isUnsafe
| ctorInfo v => v.isUnsafe
| recInfo v => v.isUnsafe
| .defnInfo v => v.safety == .unsafe
| .axiomInfo v => v.isUnsafe
| .thmInfo _ => false
| .opaqueInfo v => v.isUnsafe
| .quotInfo _ => false
| .inductInfo v => v.isUnsafe
| .ctorInfo v => v.isUnsafe
| .recInfo v => v.isUnsafe
def isPartial : ConstantInfo Bool
| defnInfo v => v.safety == .partial
| .defnInfo v => v.safety == .partial
| _ => false
def name (d : ConstantInfo) : Name :=
@@ -445,36 +436,42 @@ def numLevelParams (d : ConstantInfo) : Nat :=
def type (d : ConstantInfo) : Expr :=
d.toConstantVal.type
def value? : ConstantInfo Option Expr
| defnInfo {value := r, ..} => some r
| thmInfo {value := r, ..} => some r
| _ => none
def value? (info : ConstantInfo) (allowOpaque := false) : Option Expr :=
match info with
| .defnInfo {value, ..} => some value
| .thmInfo {value, ..} => some value
| .opaqueInfo {value, ..} => if allowOpaque then some value else none
| _ => none
def hasValue : ConstantInfo Bool
| defnInfo _ => true
| thmInfo _ => true
| _ => false
def hasValue (info : ConstantInfo) (allowOpaque := false) : Bool :=
match info with
| .defnInfo _ => true
| .thmInfo _ => true
| .opaqueInfo _ => allowOpaque
| _ => false
def value! : ConstantInfo Expr
| defnInfo {value := r, ..} => r
| thmInfo {value := r, ..} => r
| _ => panic! "declaration with value expected"
def value! (info : ConstantInfo) (allowOpaque := false) : Expr :=
match info with
| .defnInfo {value, ..} => value
| .thmInfo {value, ..} => value
| .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected"
| _ => panic! "declaration with value expected"
def hints : ConstantInfo ReducibilityHints
| defnInfo {hints := r, ..} => r
| _ => ReducibilityHints.opaque
| .defnInfo {hints, ..} => hints
| _ => .opaque
def isCtor : ConstantInfo Bool
| ctorInfo _ => true
| _ => false
| .ctorInfo _ => true
| _ => false
def isInductive : ConstantInfo Bool
| inductInfo _ => true
| _ => false
| .inductInfo _ => true
| _ => false
def isTheorem : ConstantInfo Bool
| thmInfo _ => true
| _ => false
| .thmInfo _ => true
| _ => false
def inductiveVal! : ConstantInfo InductiveVal
| .inductInfo val => val
@@ -484,11 +481,11 @@ def inductiveVal! : ConstantInfo → InductiveVal
List of all (including this one) declarations in the same mutual block.
-/
def all : ConstantInfo List Name
| inductInfo val => val.all
| defnInfo val => val.all
| thmInfo val => val.all
| opaqueInfo val => val.all
| info => [info.name]
| .inductInfo val => val.all
| .defnInfo val => val.all
| .thmInfo val => val.all
| .opaqueInfo val => val.all
| info => [info.name]
end ConstantInfo

View File

@@ -4,38 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Data.DeclarationRange
import Lean.MonadEnv
import Lean.AuxRecursor
import Lean.ToExpr
/-!
# Environment extension for declaration ranges
-/
namespace Lean
/-- Store position information for declarations. -/
structure DeclarationRange where
pos : Position
/-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
file, which is IO-heavy. -/
charUtf16 : Nat
endPos : Position
/-- See `charUtf16`. -/
endCharUtf16 : Nat
deriving Inhabited, DecidableEq, Repr
instance : ToExpr DeclarationRange where
toExpr r := mkAppN (mkConst ``DeclarationRange.mk) #[toExpr r.pos, toExpr r.charUtf16, toExpr r.endPos, toExpr r.endCharUtf16]
toTypeExpr := mkConst ``DeclarationRange
structure DeclarationRanges where
range : DeclarationRange
selectionRange : DeclarationRange
deriving Inhabited, Repr
instance : ToExpr DeclarationRanges where
toExpr r := mkAppN (mkConst ``DeclarationRanges.mk) #[toExpr r.range, toExpr r.selectionRange]
toTypeExpr := mkConst ``DeclarationRanges
builtin_initialize builtinDeclRanges : IO.Ref (NameMap DeclarationRanges) IO.mkRef {}
builtin_initialize declRangeExt : MapDeclarationExtension DeclarationRanges mkMapDeclarationExtension

View File

@@ -212,9 +212,9 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
| `(dbg_trace $arg:term; $body) => `(dbgTrace (toString $arg) fun _ => $body)
| _ => Macro.throwUnsupported
@[builtin_term_elab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
let stxNew `(@sorryAx _ false) -- Remark: we use `@` to ensure `sorryAx` will not consume auto params
withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
@[builtin_term_elab «sorry»] def elabSorry : TermElab := fun _ expectedType? => do
let type expectedType?.getDM mkFreshTypeMVar
mkLabeledSorry type (synthetic := false) (unique := true)
/-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/
partial def mkPairs (elems : Array Term) : MacroM Term :=

View File

@@ -581,7 +581,7 @@ def elabDefaultOrNonempty : TermElab := fun stx expectedType? => do
else
-- It is in the context of an `unsafe` constant. We can use sorry instead.
-- Another option is to make a recursive application since it is unsafe.
mkSorry expectedType false
mkLabeledSorry expectedType false (unique := true)
builtin_initialize
registerTraceClass `Elab.binop

View File

@@ -142,6 +142,7 @@ def runFrontend
(trustLevel : UInt32 := 0)
(ileanFileName? : Option String := none)
(jsonOutput : Bool := false)
(errorOnKinds : Array Name := #[])
: IO (Environment × Bool) := do
let startTime := ( IO.monoNanosNow).toFloat / 1000000000
let inputCtx := Parser.mkInputContext input fileName
@@ -150,7 +151,8 @@ def runFrontend
let processor := Language.Lean.process
let snap processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx
let snaps := Language.toSnapshotTree snap
snaps.runAndReport opts jsonOutput
let severityOverrides := errorOnKinds.foldl (·.insert · .error) {}
let hasErrors snaps.runAndReport opts jsonOutput severityOverrides
if let some ileanFileName := ileanFileName? then
let trees := snaps.getAll.flatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
@@ -168,7 +170,6 @@ def runFrontend
let profile Firefox.Profile.export mainModuleName.toString startTime traceStates opts
IO.FS.writeFile out <| Json.compress <| toJson profile
let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
-- no point in freeing the snapshot graph and all referenced data this close to process exit
Runtime.forget snaps
pure (cmdState.env, !hasErrors)

View File

@@ -26,7 +26,7 @@ namespace Lean.Elab.Tactic.GuardMsgs
/-- Gives a string representation of a message without source position information.
Ensures the message ends with a '\n'. -/
private def messageToStringWithoutPos (msg : Message) : IO String := do
private def messageToStringWithoutPos (msg : Message) : BaseIO String := do
let mut str msg.data.toString
unless msg.caption == "" do
str := msg.caption ++ ":\n" ++ str

View File

@@ -192,8 +192,12 @@ def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
f!"FieldRedecl @ {formatStxRange ctx info.stx}"
def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do
let loc := if let some loc := info.location? then f!"{loc.module} {loc.range.pos}-{loc.range.endPos}" else "none"
return f!"DelabTermInfo @ {← TermInfo.format ctx info.toTermInfo}\n\
Location: {loc}\n\
Docstring: {repr info.docString?}\n\
Explicit: {info.explicit}"
def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
f!"Choice @ {formatElabInfo ctx info.toElabInfo}"
@@ -211,7 +215,7 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
| ofCustomInfo i => pure <| Std.ToFormat.format i
| ofFVarAliasInfo i => pure <| i.format
| ofFieldRedeclInfo i => pure <| i.format ctx
| ofOmissionInfo i => i.format ctx
| ofDelabTermInfo i => i.format ctx
| ofChoiceInfo i => pure <| i.format ctx
def Info.toElabInfo? : Info Option ElabInfo
@@ -227,7 +231,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
| ofCustomInfo _ => none
| ofFVarAliasInfo _ => none
| ofFieldRedeclInfo _ => none
| ofOmissionInfo i => some i.toElabInfo
| ofDelabTermInfo i => some i.toElabInfo
| ofChoiceInfo i => some i.toElabInfo
/--

View File

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.Data.Position
import Lean.Data.DeclarationRange
import Lean.Data.OpenDecl
import Lean.MetavarContext
import Lean.Environment
@@ -168,14 +168,22 @@ structure FieldRedeclInfo where
stx : Syntax
/--
Denotes information for the term `⋯` that is emitted by the delaborator when omitting a term
due to `pp.deepTerms false` or `pp.proofs false`. Omission needs to be treated differently from regular terms because
Denotes TermInfo with additional configurations to control interactions with delaborated terms.
For example, the omission term `⋯` that is emitted by the delaborator when omitting a term
due to `pp.deepTerms false` or `pp.proofs false` uses this.
Omission needs to be treated differently from regular terms because
it has to be delaborated differently in `Lean.Widget.InteractiveDiagnostics.infoToInteractive`:
Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with
regular delaboration settings.
regular delaboration settings. Additionally, omissions come with a reason for omission.
-/
structure OmissionInfo extends TermInfo where
reason : String
structure DelabTermInfo extends TermInfo where
/-- A source position to use for "go to definition", to override the default. -/
location? : Option DeclarationLocation := none
/-- Text to use to override the docstring. -/
docString? : Option String := none
/-- Whether to use explicit mode when pretty printing the term on hover. -/
explicit : Bool := true
/--
Indicates that all overloaded elaborators failed. The subtrees of a `ChoiceInfo` node are the
@@ -198,7 +206,7 @@ inductive Info where
| ofCustomInfo (i : CustomInfo)
| ofFVarAliasInfo (i : FVarAliasInfo)
| ofFieldRedeclInfo (i : FieldRedeclInfo)
| ofOmissionInfo (i : OmissionInfo)
| ofDelabTermInfo (i : DelabTermInfo)
| ofChoiceInfo (i : ChoiceInfo)
deriving Inhabited

View File

@@ -1007,7 +1007,7 @@ where
values.mapM (instantiateMVarsProfiling ·)
catch ex =>
logException ex
headers.mapM fun header => mkSorry header.type (synthetic := true)
headers.mapM fun header => withRef header.declId <| mkLabeledSorry header.type (synthetic := true) (unique := true)
let headers headers.mapM instantiateMVarsAtHeader
let letRecsToLift getLetRecsToLift
let letRecsToLift letRecsToLift.mapM instantiateMVarsAtLetRecToLift

View File

@@ -159,7 +159,7 @@ private def processVar (idStx : Syntax) : M Syntax := do
private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do
if h₁ : s₁.vars.size = s₂.vars.size then
for h₂ : i in [startingAt:s₁.vars.size] do
if s₁.vars[i] != s₂.vars[i]'(by obtain _, y := h₂; simp_all) then return false
if s₁.vars[i] != s₂.vars[i]'(by obtain _, y := h₂; simp_all +zetaDelta) then return false
true
else
false

View File

@@ -9,7 +9,6 @@ import Lean.Compiler.NoncomputableAttr
import Lean.Util.CollectLevelParams
import Lean.Util.NumObjs
import Lean.Util.NumApps
import Lean.PrettyPrinter
import Lean.Meta.AbstractNestedProofs
import Lean.Meta.ForEachExpr
import Lean.Meta.Eqns

View File

@@ -20,7 +20,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
let all := preDefs.toList.map (·.declName)
forallTelescope preDef.type fun xs type => do
let value if useSorry then
mkLambdaFVars xs ( mkSorry type (synthetic := true))
mkLambdaFVars xs ( withRef preDef.ref <| mkLabeledSorry type (synthetic := true) (unique := true))
else
let msg := m!"failed to compile 'partial' definition '{preDef.declName}'"
liftM <| mkInhabitantFor msg xs type
@@ -115,7 +115,7 @@ private partial def ensureNoUnassignedLevelMVarsAtPreDef (preDef : PreDefinition
private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM PreDefinition := do
let pendingMVarIds getMVarsAtPreDef preDef
if ( logUnassignedUsingErrorInfos pendingMVarIds) then
let preDef := { preDef with value := ( mkSorry preDef.type (synthetic := true)) }
let preDef := { preDef with value := ( withRef preDef.ref <| mkLabeledSorry preDef.type (synthetic := true) (unique := true)) }
if ( getMVarsAtPreDef preDef).isEmpty then
return preDef
else

View File

@@ -14,7 +14,7 @@ open Meta
def admitGoal (mvarId : MVarId) : MetaM Unit :=
mvarId.withContext do
let mvarType inferType (mkMVar mvarId)
mvarId.assign ( mkSorry mvarType (synthetic := true))
mvarId.assign ( mkLabeledSorry mvarType (synthetic := true) (unique := true))
def goalsToMessageData (goals : List MVarId) : MessageData :=
MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n"

View File

@@ -70,7 +70,7 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
if let some suggestions librarySearch introdGoal then
if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
mkSorry expectedType (synthetic := true)
mkLabeledSorry expectedType (synthetic := true) (unique := true)
else
addTermSuggestion stx ( instantiateMVars goal).headBeta
instantiateMVars goal

View File

@@ -173,68 +173,71 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
syntax simpErase := "-" ident
-/
let go := withMainContext do
let mut thmsArray := ctx.simpTheorems
let mut thms := thmsArray[0]!
let mut simprocs := simprocs
let mut starArg := false
for arg in stx[1].getSepArgs do
try -- like withLogging, but compatible with do-notation
if arg.getKind == ``Lean.Parser.Tactic.simpErase then
let fvar? if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none
if let some fvar := fvar? then
-- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
thms := thms.eraseCore (.fvar fvar.fvarId!)
let zetaDeltaSet toZetaDeltaSet stx ctx
withTrackingZetaDeltaSet zetaDeltaSet do
let mut thmsArray := ctx.simpTheorems
let mut thms := thmsArray[0]!
let mut simprocs := simprocs
let mut starArg := false
for arg in stx[1].getSepArgs do
try -- like withLogging, but compatible with do-notation
if arg.getKind == ``Lean.Parser.Tactic.simpErase then
let fvar? if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none
if let some fvar := fvar? then
-- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
thms := thms.eraseCore (.fvar fvar.fvarId!)
else
let id := arg[1]
if let .ok declName observing (realizeGlobalConstNoOverloadWithInfo id) then
if ( Simp.isSimproc declName) then
simprocs := simprocs.erase declName
else if ctx.config.autoUnfold then
thms := thms.eraseCore (.decl declName)
else
thms withRef id <| thms.erase (.decl declName)
else
-- If `id` could not be resolved, we should check whether it is a builtin simproc.
-- before returning error.
let name := id.getId.eraseMacroScopes
if ( Simp.isBuiltinSimproc name) then
simprocs := simprocs.erase name
else
withRef id <| throwUnknownConstant name
else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
let post :=
if arg[0].isNone then
true
else
arg[0][0].getKind == ``Parser.Tactic.simpPost
let inv := !arg[1].isNone
let term := arg[2]
match ( resolveSimpIdTheorem? term) with
| .expr e =>
let name mkFreshId
thms addDeclToUnfoldOrTheorem ctx.indexConfig thms (.stx name arg) e post inv kind
| .simproc declName =>
simprocs simprocs.add declName post
| .ext (some ext₁) (some ext₂) _ =>
thmsArray := thmsArray.push ( ext₁.getTheorems)
simprocs := simprocs.push ( ext₂.getSimprocs)
| .ext (some ext₁) none _ =>
thmsArray := thmsArray.push ( ext₁.getTheorems)
| .ext none (some ext₂) _ =>
simprocs := simprocs.push ( ext₂.getSimprocs)
| .none =>
let name mkFreshId
thms addSimpTheorem ctx.indexConfig thms (.stx name arg) term post inv
else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
starArg := true
else
let id := arg[1]
if let .ok declName observing (realizeGlobalConstNoOverloadWithInfo id) then
if ( Simp.isSimproc declName) then
simprocs := simprocs.erase declName
else if ctx.config.autoUnfold then
thms := thms.eraseCore (.decl declName)
else
thms withRef id <| thms.erase (.decl declName)
else
-- If `id` could not be resolved, we should check whether it is a builtin simproc.
-- before returning error.
let name := id.getId.eraseMacroScopes
if ( Simp.isBuiltinSimproc name) then
simprocs := simprocs.erase name
else
withRef id <| throwUnknownConstant name
else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
let post :=
if arg[0].isNone then
true
else
arg[0][0].getKind == ``Parser.Tactic.simpPost
let inv := !arg[1].isNone
let term := arg[2]
match ( resolveSimpIdTheorem? term) with
| .expr e =>
let name mkFreshId
thms addDeclToUnfoldOrTheorem ctx.indexConfig thms (.stx name arg) e post inv kind
| .simproc declName =>
simprocs simprocs.add declName post
| .ext (some ext₁) (some ext₂) _ =>
thmsArray := thmsArray.push ( ext₁.getTheorems)
simprocs := simprocs.push ( ext₂.getSimprocs)
| .ext (some ext₁) none _ =>
thmsArray := thmsArray.push ( ext₁.getTheorems)
| .ext none (some ext₂) _ =>
simprocs := simprocs.push ( ext₂.getSimprocs)
| .none =>
let name mkFreshId
thms addSimpTheorem ctx.indexConfig thms (.stx name arg) term post inv
else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
starArg := true
else
throwUnsupportedSyntax
catch ex =>
if ( read).recover then
logException ex
else
throw ex
return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg }
throwUnsupportedSyntax
catch ex =>
if ( read).recover then
logException ex
else
throw ex
let ctx := ctx.setZetaDeltaSet zetaDeltaSet ( getZetaDeltaFVarIds)
return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg }
-- If recovery is disabled, then we want simp argument elaboration failures to be exceptions.
-- This affects `addSimpTheorem`.
if ( read).recover then
@@ -277,6 +280,20 @@ where
else
return .none
/-- If `zetaDelta := false`, create a `FVarId` set with all local let declarations in the `simp` argument list. -/
toZetaDeltaSet (stx : Syntax) (ctx : Simp.Context) : TacticM FVarIdSet := do
if ctx.config.zetaDelta then return {}
Term.withoutCheckDeprecated do -- We do not want to report deprecated constants in the first pass
let mut s : FVarIdSet := {}
for arg in stx[1].getSepArgs do
if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
if arg[0].isNone && arg[1].isNone then
let term := arg[2]
let .expr (.fvar fvarId) resolveSimpIdTheorem? term | pure ()
if ( fvarId.getDecl).isLet then
s := s.insert fvarId
return s
@[inline] def simpOnlyBuiltins : List Name := [``eq_self, ``iff_self]
structure MkSimpContextResult where
@@ -323,7 +340,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
let simprocs := r.simprocs
let mut simpTheorems := ctx.simpTheorems
/-
When using `zeta := false`, we do not expand let-declarations when using `[*]`.
When using `zetaDelta := false`, we do not expand let-declarations when using `[*]`.
Users must explicitly include it in the list.
-/
let hs getPropHyps

View File

@@ -326,6 +326,10 @@ structure Context where
`refine' (fun x => _)
-/
holesAsSyntheticOpaque : Bool := false
/--
If `checkDeprecated := true`, then `Linter.checkDeprecated` when creating constants.
-/
checkDeprecated : Bool := true
abbrev TermElabM := ReaderT Context $ StateRefT State MetaM
abbrev TermElab := Syntax Option Expr TermElabM Expr
@@ -1154,7 +1158,7 @@ private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr :
let expectedType match expectedType? with
| none => mkFreshTypeMVar
| some expectedType => pure expectedType
mkSyntheticSorry expectedType
mkLabeledSorry expectedType (synthetic := true) (unique := false)
/--
Log the given exception, and create a synthetic sorry for representing the failed
@@ -1260,7 +1264,7 @@ The `tacticCode` syntax is the full `by ..` syntax.
-/
def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Expr := do
if pure (debug.byAsSorry.get ( getOptions)) <&&> isProp type then
mkSorry type false
withRef tacticCode <| mkLabeledSorry type false (unique := true)
else
let mvar mkFreshExprMVar type MetavarKind.syntheticOpaque
let mvarId := mvar.mvarId!
@@ -1851,7 +1855,7 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPo
withRef stx <| ensureHasType expectedType? e errorMsgHeader?
catch ex =>
if ( read).errToSorry && ex matches .error .. then
exceptionToSorry ex expectedType?
withRef stx <| exceptionToSorry ex expectedType?
else
throw ex
@@ -2026,6 +2030,10 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
trace[Elab.letrec] "mvarId root: {mkMVar mvarId}"
return ( get).letRecsToLift.any (·.mvarId == mvarId)
private def checkDeprecatedCore (constName : Name) : TermElabM Unit := do
if ( read).checkDeprecated then
Linter.checkDeprecated constName
/--
Create an `Expr.const` using the given name and explicit levels.
Remark: fresh universe metavariables are created if the constant has more universe
@@ -2033,9 +2041,8 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
If `checkDeprecated := true`, then `Linter.checkDeprecated` is invoked.
-/
def mkConst (constName : Name) (explicitLevels : List Level := []) (checkDeprecated := true) : TermElabM Expr := do
if checkDeprecated then
Linter.checkDeprecated constName
def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do
checkDeprecatedCore constName
let cinfo getConstInfo constName
if explicitLevels.length > cinfo.levelParams.length then
throwError "too many explicit universe levels for '{constName}'"
@@ -2046,7 +2053,10 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) (checkDepreca
def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do
if let .const declName _ := e.getAppFn then
withRef ref do Linter.checkDeprecated declName
withRef ref do checkDeprecatedCore declName
@[inline] def withoutCheckDeprecated [MonadWithReaderOf Context m] : m α m α :=
withTheReader Context (fun ctx => { ctx with checkDeprecated := false })
private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
candidates.foldlM (init := []) fun result (declName, projs) => do
@@ -2058,7 +2068,7 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of
`TermElabResult`s.
-/
let const mkConst declName explicitLevels (checkDeprecated := false)
let const withoutCheckDeprecated <| mkConst declName explicitLevels
return (const, projs) :: result
def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do

View File

@@ -262,6 +262,16 @@ instance : Inhabited DynamicSnapshot where
f element
children.forM (·.get.forM f)
/--
Runs a tree of snapshots to conclusion,
folding the function `f` over each snapshot in tree preorder. -/
@[specialize] partial def SnapshotTree.foldM [Monad m] (s : SnapshotTree)
(f : α Snapshot m α) (init : α) : m α := do
match s with
| mk element children =>
let a f init element
children.foldlM (fun a snap => snap.get.foldM f a) a
/--
Option for printing end position of each message in addition to start position. Used for testing
message ranges in the test suite. -/
@@ -269,24 +279,43 @@ register_builtin_option printMessageEndPos : Bool := {
defValue := false, descr := "print end position of each message in addition to start position"
}
/-- Reports messages on stdout. If `json` is true, prints messages as JSON (one per line). -/
def reportMessages (msgLog : MessageLog) (opts : Options) (json := false) : IO Unit := do
if json then
msgLog.forM (·.toJson <&> (·.compress) >>= IO.println)
else
msgLog.forM (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print)
/--
Reports messages on stdout and returns whether an error was reported.
If `json` is true, prints messages as JSON (one per line).
If a message's kind is in `severityOverrides`, it will be reported with
the specified severity.
-/
def reportMessages (msgLog : MessageLog) (opts : Options)
(json := false) (severityOverrides : NameMap MessageSeverity := {}) : IO Bool := do
let includeEndPos := printMessageEndPos.get opts
msgLog.unreported.foldlM (init := false) fun hasErrors msg => do
let msg : Message :=
if let some severity := severityOverrides.find? msg.kind then
{msg with severity}
else
msg
if json then
let j msg.toJson
IO.println j.compress
else
let s msg.toString includeEndPos
IO.print s
return hasErrors || msg.severity matches .error
/--
Runs a tree of snapshots to conclusion and incrementally report messages on stdout. Messages are
reported in tree preorder.
reported in tree preorder. Returns whether any errors were reported.
This function is used by the cmdline driver; see `Lean.Server.FileWorker.reportSnapshots` for how
the language server reports snapshots asynchronously. -/
def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false) : IO Unit := do
s.forM (reportMessages ·.diagnostics.msgLog opts json)
def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options)
(json := false) (severityOverrides : NameMap MessageSeverity := {}) : IO Bool := do
s.foldM (init := false) fun e snap => do
let e' reportMessages snap.diagnostics.msgLog opts json severityOverrides
return strictOr e e'
/-- Waits on and returns all snapshots in the tree. -/
def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
s.forM (m := StateM _) (fun s => modify (·.push s)) |>.run #[] |>.2
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

@@ -91,7 +91,7 @@ inductive MessageData where
If the thunked message is produced for a term that contains a synthetic sorry,
`hasSyntheticSorry` should return `true`.
This is used to filter out certain messages. -/
| ofLazy (f : Option PPContext IO Dynamic) (hasSyntheticSorry : MetavarContext Bool)
| ofLazy (f : Option PPContext BaseIO Dynamic) (hasSyntheticSorry : MetavarContext Bool)
deriving Inhabited, TypeName
namespace MessageData
@@ -103,7 +103,7 @@ def ofFormat (fmt : Format) : MessageData := .ofFormatWithInfos ⟨fmt, .empty
Lazy message data production, with access to the context as given by
a surrounding `MessageData.withContext` (which is expected to exist).
-/
def lazy (f : PPContext IO MessageData)
def lazy (f : PPContext BaseIO MessageData)
(hasSyntheticSorry : MetavarContext Bool := fun _ => false) : MessageData :=
.ofLazy (hasSyntheticSorry := hasSyntheticSorry) fun ctx? => do
let msg match ctx? with
@@ -220,9 +220,9 @@ where
| trace _ msg msgs => visit mctx? msg || msgs.any (visit mctx?)
| _ => false
partial def formatAux : NamingContext Option MessageDataContext MessageData IO Format
| _, _, ofFormatWithInfos fmt => return fmt.1
| _, none, ofGoal mvarId => return "goal " ++ format (mkMVar mvarId)
partial def formatAux : NamingContext Option MessageDataContext MessageData BaseIO Format
| _, _, ofFormatWithInfos fmt => return fmt.1
| _, none, ofGoal mvarId => return formatRawGoal mvarId
| nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId
| nCtx, ctx, ofWidget _ d => formatAux nCtx ctx d
| nCtx, _, withContext ctx d => formatAux nCtx ctx d
@@ -244,10 +244,10 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
| panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}"
formatAux nCtx ctx? msg
protected def format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : IO Format :=
protected def format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : BaseIO Format :=
formatAux { currNamespace := Name.anonymous, openDecls := [] } ctx? msgData
protected def toString (msgData : MessageData) : IO String := do
protected def toString (msgData : MessageData) : BaseIO String := do
return toString ( msgData.format)
instance : Append MessageData := compose
@@ -374,14 +374,14 @@ namespace Message
msg.data.kind
/-- Serializes the message, converting its data into a string and saving its kind. -/
@[inline] def serialize (msg : Message) : IO SerialMessage := do
@[inline] def serialize (msg : Message) : BaseIO SerialMessage := do
return {msg with kind := msg.kind, data := msg.data.toString}
protected def toString (msg : Message) (includeEndPos := false) : IO String := do
protected def toString (msg : Message) (includeEndPos := false) : BaseIO String := do
-- Remark: The inline here avoids a new message allocation when `msg` is shared
return inline <| ( msg.serialize).toString includeEndPos
protected def toJson (msg : Message) : IO Json := do
protected def toJson (msg : Message) : BaseIO Json := do
-- Remark: The inline here avoids a new message allocation when `msg` is shared
return inline <| toJson ( msg.serialize)
@@ -391,23 +391,14 @@ end Message
A persistent array of messages.
In the Lean elaborator, we use a fresh message log per command but may also report diagnostics at
various points inside a command, which will empty `unreported` and updated `hadErrors` accordingly
(see `CoreM.getAndEmptyMessageLog`).
various points inside a command, which will empty `unreported` and move its messages to `reported`.
Reported messages are preserved for some specific "lookback" operations such as `hasError` that
should consider the entire message history of the current command; most other functions such as
`add` and `toList` will only operate on unreported messages.
-/
structure MessageLog where
/--
If true, there was an error in the log previously that has already been reported to the user and
removed from the log. Thus we say that in the current context (usually the current command), we
"have errors" if either this flag is set or there is an error in `msgs`; see
`MessageLog.hasErrors`. If we have errors, we suppress some error messages that are often the
result of a previous error.
-/
/-
Design note: We considered introducing a `hasErrors` field instead that already includes the
presence of errors in `msgs` but this would not be compatible with e.g.
`MessageLog.errorsToWarnings`.
-/
hadErrors : Bool := false
/-- The list of messages already reported (i.e. saved in a `Snapshot`), in insertion order. -/
reported : PersistentArray Message := {}
/-- The list of messages not already reported, in insertion order. -/
unreported : PersistentArray Message := {}
/--
@@ -416,7 +407,7 @@ structure MessageLog where
the configuration option `exponentiation.threshold`.
We don't produce a warning if the kind is already in the following set.
-/
reportedKinds : NameSet := {}
loggedKinds : NameSet := {}
deriving Inhabited
namespace MessageLog
@@ -426,24 +417,33 @@ def empty : MessageLog := {}
using `MessageLog.toList/toArray`" (since := "2024-05-22")]
def msgs : MessageLog PersistentArray Message := unreported
def reportedPlusUnreported : MessageLog PersistentArray Message
| { reported := r, unreported := u, .. } => r ++ u
def hasUnreported (log : MessageLog) : Bool :=
!log.unreported.isEmpty
def add (msg : Message) (log : MessageLog) : MessageLog :=
{ log with unreported := log.unreported.push msg }
protected def append (l₁ l₂ : MessageLog) : MessageLog :=
{ hadErrors := l₁.hadErrors || l₂.hadErrors, unreported := l₁.unreported ++ l₂.unreported }
protected def append (l₁ l₂ : MessageLog) : MessageLog where
reported := l₁.reported ++ l₂.reported
unreported := l₁.unreported ++ l₂.unreported
loggedKinds := l₁.loggedKinds.union l₂.loggedKinds
instance : Append MessageLog :=
MessageLog.append
/--
Checks if either of `reported` or `unreported` contains an error, i.e. whether the current command
has errored yet.
-/
def hasErrors (log : MessageLog) : Bool :=
log.hadErrors || log.unreported.any (·.severity matches .error)
log.reported.any (·.severity matches .error) || log.unreported.any (·.severity matches .error)
/-- Clears unreported messages while preserving `hasErrors`. -/
/-- Moves `unreported` messages to `reported`. -/
def markAllReported (log : MessageLog) : MessageLog :=
{ log with unreported := {}, hadErrors := log.hasErrors }
{ log with unreported := {}, reported := log.reported ++ log.unreported }
def errorsToWarnings (log : MessageLog) : MessageLog :=
{ unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }

View File

@@ -17,6 +17,7 @@ import Lean.Meta.Instances
import Lean.Meta.AbstractMVars
import Lean.Meta.SynthInstance
import Lean.Meta.AppBuilder
import Lean.Meta.Sorry
import Lean.Meta.Tactic
import Lean.Meta.KAbstract
import Lean.Meta.RecursorInfo

View File

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
-/
prelude
import Lean.Structure
import Lean.Util.Recognizers
import Lean.Meta.SynthInstance
import Lean.Meta.Check
import Lean.Meta.DecLevel
@@ -513,10 +512,6 @@ def mkSome (type value : Expr) : MetaM Expr := do
let u getDecLevel type
return mkApp2 (mkConst ``Option.some [u]) type value
def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
let u getLevel type
return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)
/-- Return `Decidable.decide p` -/
def mkDecide (p : Expr) : MetaM Expr :=
mkAppOptM ``Decidable.decide #[p, none]
@@ -545,10 +540,6 @@ def mkDefault (α : Expr) : MetaM Expr :=
def mkOfNonempty (α : Expr) : MetaM Expr := do
mkAppOptM ``Classical.ofNonempty #[α, none]
/-- Return `sorryAx type` -/
def mkSyntheticSorry (type : Expr) : MetaM Expr :=
return mkApp2 (mkConst ``sorryAx [ getLevel type]) type (mkConst ``Bool.true)
/-- Return `funext h` -/
def mkFunExt (h : Expr) : MetaM Expr :=
mkAppM ``funext #[h]

View File

@@ -141,18 +141,6 @@ structure Config where
Controls which definitions and theorems can be unfolded by `isDefEq` and `whnf`.
-/
transparency : TransparencyMode := TransparencyMode.default
/--
When `trackZetaDelta = true`, we track all free variables that have been zetaDelta-expanded.
That is, suppose the local context contains
the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaDeltaFVarIds`.
We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`.
When we find these declarations we set their `nonDep` flag with `true`.
To find these let-declarations in a given term `s`, we
1- Reset `State.zetaDeltaFVarIds`
2- Set `trackZetaDelta := true`
3- Type-check `s`.
-/
trackZetaDelta : Bool := false
/-- Eta for structures configuration mode. -/
etaStruct : EtaStructMode := .all
/--
@@ -187,7 +175,7 @@ structure Config where
Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
-/
zetaDelta : Bool := true
deriving Inhabited
deriving Inhabited, Repr
/-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/
private def Config.toKey (c : Config) : UInt64 :=
@@ -419,7 +407,7 @@ structure Diagnostics where
structure State where
mctx : MetavarContext := {}
cache : Cache := {}
/-- When `trackZetaDelta == true`, then any let-decl free variable that is zetaDelta-expanded by `MetaM` is stored in `zetaDeltaFVarIds`. -/
/-- When `Context.trackZetaDelta == true`, then any let-decl free variable that is zetaDelta-expanded by `MetaM` is stored in `zetaDeltaFVarIds`. -/
zetaDeltaFVarIds : FVarIdSet := {}
/-- Array of postponed universe level constraints -/
postponed : PersistentArray PostponedEntry := {}
@@ -445,6 +433,28 @@ register_builtin_option maxSynthPendingDepth : Nat := {
structure Context where
private config : Config := {}
private configKey : UInt64 := config.toKey
/--
When `trackZetaDelta = true`, we track all free variables that have been zetaDelta-expanded.
That is, suppose the local context contains
the declaration `x : t := v`, and we reduce `x` to `v`, then we insert `x` into `State.zetaDeltaFVarIds`.
We use `trackZetaDelta` to discover which let-declarations `let x := v; e` can be represented as `(fun x => e) v`.
When we find these declarations we set their `nonDep` flag with `true`.
To find these let-declarations in a given term `s`, we
1- Reset `State.zetaDeltaFVarIds`
2- Set `trackZetaDelta := true`
3- Type-check `s`.
Note that, we do not include this field in the `Config` structure because this field is not
taken into account while caching results. See also field `zetaDeltaSet`.
-/
trackZetaDelta : Bool := false
/--
If `config.zetaDelta := false`, we may select specific local declarations to be unfolded using
the field `zetaDeltaSet`. Note that, we do not include this field in the `Config` structure
because this field is not taken into account while caching results.
Moreover, we reset all caches whenever setting it.
-/
zetaDeltaSet : FVarIdSet := {}
/-- Local context -/
lctx : LocalContext := {}
/-- Local instances in `lctx`. -/
@@ -1086,11 +1096,42 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
@[inline] def withInTypeClassResolution : n α n α :=
mapMetaM <| withReader (fun ctx => { ctx with inTypeClassResolution := true })
@[inline] def withFreshCache : n α n α :=
mapMetaM fun x => do
let cacheSaved := ( get).cache
modify fun s => { s with cache := {} }
try
x
finally
modify fun s => { s with cache := cacheSaved }
/--
Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
-/
@[inline] def withTrackingZetaDelta (x : n α) : n α :=
withConfig (fun cfg => { cfg with trackZetaDelta := true }) x
@[inline] def withTrackingZetaDelta : n α n α :=
mapMetaM fun x =>
withFreshCache <| withReader (fun ctx => { ctx with trackZetaDelta := true }) x
/--
`withZetaDeltaSet s x` executes `x` with `zetaDeltaSet := s`.
The cache is reset while executing `x` if `s` is not empty.
-/
def withZetaDeltaSet (s : FVarIdSet) : n α n α :=
mapMetaM fun x =>
if s.isEmpty then
x
else
withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s }) x
/--
Similar to `withZetaDeltaSet`, but also enables `withTrackingZetaDelta` if `s` is not empty.
-/
def withTrackingZetaDeltaSet (s : FVarIdSet) : n α n α :=
mapMetaM fun x =>
if s.isEmpty then
x
else
withFreshCache <| withReader (fun ctx => { ctx with zetaDeltaSet := s, trackZetaDelta := true }) x
@[inline] def withoutProofIrrelevance (x : n α) : n α :=
withConfig (fun cfg => { cfg with proofIrrelevance := false }) x

View File

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Lean.Meta.InferType
import Lean.Meta.Sorry
/-!
This is not the Kernel type checker, but an auxiliary method for checking
@@ -133,6 +134,12 @@ where
if fn? == ``OfNat.ofNat && as.size 3 && firstImplicitDiff? == some 0 then
-- Even if there is an explicit diff, it is better to see that the type is different.
return (a.setPPNumericTypes true, b.setPPNumericTypes true)
if fn? == ``sorryAx then
-- If these are `sorry`s with differing source positions, make sure the delaborator shows the positions.
if let some { module? := moda? } := isLabeledSorry? a then
if let some { module? := modb? } := isLabeledSorry? b then
if moda? != modb? then
return (a.setOption `pp.sorrySource true, b.setOption `pp.sorrySource true)
-- General case
if let some i := firstExplicitDiff? <|> firstImplicitDiff? then
let (ai, bi) visit as[i]! bs[i]!

View File

@@ -304,14 +304,14 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
if info.isInstImplicit then
discard <| trySynthPending a₁
discard <| trySynthPending a₂
unless ( withAtLeastTransparency TransparencyMode.default <| Meta.isExprDefEqAux a₁ a₂) do
unless ( withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do
return false
for i in postponedHO do
let a₁ := args₁[i]!
let a₂ := args₂[i]!
let info := finfo.paramInfo[i]!
if info.isInstImplicit then
unless ( withAtLeastTransparency TransparencyMode.default <| Meta.isExprDefEqAux a₁ a₂) do
unless ( withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do
return false
else
unless ( Meta.isExprDefEqAux a₁ a₂) do
@@ -380,12 +380,13 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
else
-- must check whether types are definitionally equal or not, before assigning and returning true
let mvarType inferType mvar
let vType inferType v
if ( withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then
mvar.mvarId!.assign v
pure true
else
pure false
withInferTypeConfig do
let vType inferType v
if ( Meta.isExprDefEqAux mvarType vType) then
mvar.mvarId!.assign v
pure true
else
pure false
/--
Auxiliary method for solving constraints of the form `?m xs := v`.
@@ -1582,7 +1583,7 @@ private def etaEq (t s : Expr) : Bool :=
Then, we can enable the flag only when applying `simp` and `rw` theorems.
-/
private def withProofIrrelTransparency (k : MetaM α) : MetaM α :=
withAtLeastTransparency .default k
withInferTypeConfig k
private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do
if ( getConfig).proofIrrelevance then

View File

@@ -177,15 +177,20 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
modifyInferTypeCache fun c => c.insert key type
return type
private def defaultConfig : ConfigWithKey :=
{ : Config }.toConfigWithKey
/--
Ensure `MetaM` configuration is strong enough for inferring/checking types.
For example, `beta := true` is essential when type checking.
private def allConfig : ConfigWithKey :=
{ transparency := .all : Config }.toConfigWithKey
@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := do
let cfg := if ( getTransparency) == .all then allConfig else defaultConfig
withConfigWithKey cfg x
Remark: we previously use the default configuration here, but this is problematic
because it overrides unrelated configurations.
-/
@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α :=
withAtLeastTransparency .default do
let cfg getConfig
if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj == .yesWithDelta then
x
else
withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaDelta := true, proj := .yesWithDelta }) x
@[export lean_infer_type]
def inferTypeImp (e : Expr) : MetaM Expr :=

View File

@@ -15,7 +15,7 @@ population of imported modules for use in tactics. It uses a lazy
initialization strategy.
The discrimination tree can be created through
`createImportedEnvironment`. This creates a discrimination tree from all
`createImportedDiscrTree`. This creates a discrimination tree from all
imported modules in an environment using a callback that provides the
entries as `InitEntry` values.

115
src/Lean/Meta/Sorry.lean Normal file
View File

@@ -0,0 +1,115 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
-/
prelude
import Lean.Data.Lsp.Utf16
import Lean.Meta.InferType
import Lean.Util.Recognizers
/-!
# Utilities for creating and recognizing `sorry`
This module develops material for creating and recognizing `sorryAx` terms that encode originating source positions.
There are three orthogonal configurations for sorries:
- The sorry could be *synthetic*. When elaboration fails on some subterm, then we can use a sorry to fill in the missing subterm.
In this case elaboration marks the sorry as being "synthetic" while logging an error.
The presence of synthetic sorries tends to suppress further errors. For example, the "this declaration contains sorry" error
is not triggered for synthetic sorries as we assume there is already an error message logged.
- The sorry could be *unique*. A unique sorry is not definitionally equal to any other sorry, even if they have the same type.
Normally `sorryAx α s = sorryAx α s` is a definitional equality. Unique sorries insert a unique tag `t` using the encoding `sorryAx (τ → α) s t`.
- The sorry could be *labeled*. A labeled sorry contains source position information, supporting the LSP "go to definition" feature in the Infoview,
and also supporting pretty printing the sorry with an indication of source position when the option `pp.sorrySource` is true.
-/
namespace Lean.Meta
/--
Returns `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error.
See also `Lean.Meta.mkLabeledSorry`, for creating a `sorry` that is labeled or unique.
-/
def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
let u getLevel type
return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)
structure SorryLabelView where
/--
Records the origin module name, logical source position, and LSP range for the `sorry`.
The logical source position is used when displaying the sorry when the `pp.sorrySource` option is true,
and the LSP range is used for "go to definition" in the Infoview.
-/
module? : Option DeclarationLocation := none
def SorryLabelView.encode (view : SorryLabelView) : CoreM Name :=
let name :=
if let some { module, range := { pos, endPos, charUtf16, endCharUtf16 } } := view.module? then
module
|>.num pos.line |>.num pos.column
|>.num endPos.line |>.num endPos.column
|>.num charUtf16 |>.num endCharUtf16
else
.anonymous
mkFreshUserName (name.str "_sorry")
def SorryLabelView.decode? (name : Name) : Option SorryLabelView := do
guard <| name.hasMacroScopes
let .str name "_sorry" := name.eraseMacroScopes | failure
if let .num (.num (.num (.num (.num (.num module posLine) posCol) endLine) endCol) charUtf16) endCharUtf16 := name then
return { module? := some { module, range := { pos := posLine, posCol, endPos := endLine, endCol, charUtf16, endCharUtf16 } } }
else
failure
/--
Constructs a `sorryAx`.
* If the current ref has a source position, then creates a labeled sorry.
This supports "go to definition" in the InfoView and pretty printing a source position when the `pp.sorrySource` option is true.
* If `synthetic` is true, then the `sorry` is regarded as being generated by the elaborator.
The caller should ensure that there is an associated error logged.
* If `unique` is true, the `sorry` is unique, in the sense that it is not defeq to any other `sorry` created by `mkLabeledSorry`.
-/
def mkLabeledSorry (type : Expr) (synthetic : Bool) (unique : Bool) : MetaM Expr := do
let tag
if let (some startSPos, some endSPos) := (( getRef).getPos?, ( getRef).getTailPos?) then
let fileMap getFileMap
SorryLabelView.encode {
module? := some {
module := ( getMainModule)
range := {
pos := fileMap.toPosition startSPos
endPos := fileMap.toPosition endSPos
charUtf16 := (fileMap.utf8PosToLspPos startSPos).character
endCharUtf16 := (fileMap.utf8PosToLspPos endSPos).character
}
}
}
else
SorryLabelView.encode {}
if unique then
let e mkSorry (mkForall `tag .default (mkConst ``Lean.Name) type) synthetic
return .app e (toExpr tag)
else
let e mkSorry (mkForall `tag .default (mkConst ``Unit) type) synthetic
let tag' := mkApp4 (mkConst ``Function.const [levelOne, levelOne]) (mkConst ``Unit) (mkConst ``Lean.Name) (mkConst ``Unit.unit) (toExpr tag)
return .app e tag'
/--
Returns a `SorryLabelView` if `e` is an application of an expression returned by `mkLabeledSorry`.
If it is, then the `sorry` takes the first three arguments, and the tag is at argument 3.
-/
def isLabeledSorry? (e : Expr) : Option SorryLabelView := do
guard <| e.isAppOf ``sorryAx
let numArgs := e.getAppNumArgs
guard <| numArgs 3
let arg := e.getArg! 2
if let some tag := arg.name? then
SorryLabelView.decode? tag
else
guard <| arg.isAppOfArity ``Function.const 4
guard <| arg.appFn!.appArg!.isAppOfArity ``Unit.unit 0
let tag arg.appArg!.name?
SorryLabelView.decode? tag

View File

@@ -57,7 +57,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
match e? with
| none => pure none
| some e =>
match ( reduceProj? e.getAppFn) with
match ( withSimpMetaConfig <| reduceProj? e.getAppFn) with
| some f => return some (mkAppN f e.getAppArgs)
| none => return none
if projInfo.fromClass then
@@ -152,7 +152,7 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
withDefault <| unfoldDefinition? e
else if ( isMatchDef fName) then
let some value withDefault <| unfoldDefinition? e | return none
let .reduced value reduceMatcher? value | return none
let .reduced value withSimpMetaConfig <| reduceMatcher? value | return none
return some value
else
return none
@@ -166,6 +166,7 @@ private def reduceStep (e : Expr) : SimpM Expr := do
let f := e.getAppFn
if f.isMVar then
return ( instantiateMVars e)
withSimpMetaConfig do
if cfg.beta then
if f.isHeadBetaTargetFn false then
return f.betaRev e.getAppRevArgs
@@ -256,7 +257,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
withFreshCache do f
def simpProj (e : Expr) : SimpM Result := do
match ( reduceProj? e) with
match ( withSimpMetaConfig <| reduceProj? e) with
| some e => return { expr := e }
| none =>
let s := e.projExpr!
@@ -484,7 +485,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
let rhs := hType.appArg!
rhs.withApp fun m zs => do
let val mkLambdaFVars zs r.expr
unless ( isDefEq m val) do
unless ( withSimpMetaConfig <| isDefEq m val) do
throwCongrHypothesisFailed
let mut proof r.getProof
if hType.isAppOf ``Iff then
@@ -528,7 +529,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
let args := e.getAppArgs
e := mkAppN e.getAppFn args[:numArgs]
extraArgs := args[numArgs:].toArray
if ( isDefEq lhs e) then
if ( withSimpMetaConfig <| isDefEq lhs e) then
let mut modified := false
for i in c.hypothesesPos do
let x := xs[i]!
@@ -647,6 +648,8 @@ partial def simpNonDepLetFun (e : Expr) : SimpM Result := do
let x := mkConst `__no_used_dummy__ -- dummy value
let { expr, proof, .. } go (xs.push x) body.bindingBody!
let proof := mkApp6 (mkConst ``letFun_unused us) alpha betaFun.bindingBody! val body.bindingBody! expr proof
let expr := expr.lowerLooseBVars 1 1
let proof := proof.lowerLooseBVars 1 1
return { expr, proof, modified := true }
else
let beta := betaFun.bindingBody!
@@ -764,16 +767,28 @@ where
trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
simpLoop e
-- TODO: delete
@[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α :=
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
@[inline] private def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α := do
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <|
withTrackingZetaDeltaSet ctx.zetaDeltaSet <|
withReducible x
private def updateUsedSimpsWithZetaDeltaCore (s : UsedSimps) (usedZetaDelta : FVarIdSet) : UsedSimps :=
usedZetaDelta.fold (init := s) fun s fvarId =>
s.insert <| .fvar fvarId
private def updateUsedSimpsWithZetaDelta (ctx : Context) (stats : Stats) : MetaM Stats := do
let used := stats.usedTheorems
let used := updateUsedSimpsWithZetaDeltaCore used ctx.initUsedZetaDelta
let used := updateUsedSimpsWithZetaDeltaCore used ( getZetaDeltaFVarIds)
return { stats with usedTheorems := used }
def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
let ctx ctx.setLctxInitIndices
withSimpContext ctx do
let (r, s) go e methods.toMethodsRef ctx |>.run { stats with }
trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
return (r, { s with })
let s updateUsedSimpsWithZetaDelta ctx { s with }
return (r, s)
where
go (e : Expr) : SimpM Result :=
tryCatchRuntimeEx
@@ -788,7 +803,8 @@ where
def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
withSimpContext ctx do
let (r, s) go e methods.toMethodsRef ctx |>.run { stats with }
pure (r, { s with })
let s updateUsedSimpsWithZetaDelta ctx { s with }
pure (r, s)
where
go (e : Expr) : SimpM Expr :=
tryCatchRuntimeEx

View File

@@ -117,7 +117,7 @@ private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
recordTriedSimpTheorem thm.origin
let rec go (e : Expr) : SimpM (Option Result) := do
if ( isDefEq lhs e) then
if ( withSimpMetaConfig <| isDefEq lhs e) then
unless ( synthesizeArgs thm.origin bis xs) do
return none
let proof? if ( useImplicitDefEqProof thm) then
@@ -342,7 +342,7 @@ def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do
def simpMatch : Simproc := fun e => do
unless ( getConfig).iota do
return .continue
if let some e reduceRecMatcher? e then
if let some e withSimpMetaConfig <| reduceRecMatcher? e then
return .visit { expr := e }
let .const declName _ := e.getAppFn
| return .continue
@@ -549,7 +549,7 @@ private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
-- well-behaved discharger. See comment at `Methods.wellBehavedDischarge`
else if !contextual && localDecl.index >= lctxInitIndices then
return none
else if ( isDefEq e localDecl.type) then
else if ( withSimpMetaConfig <| isDefEq e localDecl.type) then
return some localDecl.toExpr
else
return none
@@ -591,7 +591,7 @@ def dischargeRfl (e : Expr) : SimpM (Option Expr) := do
forallTelescope e fun xs e => do
let some (t, a, b) := e.eq? | return .none
unless a.getAppFn.isMVar || b.getAppFn.isMVar do return .none
if ( withReducible <| isDefEq a b) then
if ( withSimpMetaConfig <| isDefEq a b) then
trace[Meta.Tactic.simp.discharge] "Discharging with rfl: {e}"
let u getLevel t
let proof := mkApp2 (.const ``rfl [u]) t a

View File

@@ -54,6 +54,12 @@ abbrev CongrCache := ExprMap (Option CongrTheorem)
structure Context where
private mk ::
config : Config := {}
/-- Local declarations to propagate to `Meta.Context` -/
zetaDeltaSet : FVarIdSet := {}
/--
When processing `Simp` arguments, `zetaDelta` may be performed if `zetaDeltaSet` is not empty.
We save the local free variable ids in `initUsedZetaDelta`. `initUsedZetaDelta` is a subset of `zetaDeltaSet`. -/
initUsedZetaDelta : FVarIdSet := {}
metaConfig : ConfigWithKey := default
indexConfig : ConfigWithKey := default
/-- `maxDischargeDepth` from `config` as an `UInt32`. -/
@@ -122,8 +128,18 @@ private def updateArith (c : Config) : CoreM Config := do
/--
Converts `Simp.Config` into `Meta.ConfigWithKey` used for indexing.
-/
private def mkIndexConfig (c : Config) : ConfigWithKey :=
{ c with
private def mkIndexConfig (c : Config) : MetaM ConfigWithKey := do
let curr Meta.getConfig
return { curr with
beta := c.beta
iota := c.iota
zeta := c.zeta
zetaDelta := c.zetaDelta
etaStruct := c.etaStruct
/-
When indexing terms we disable projection to ensure a term such as `f ((a, b).1)`
is an instance of the pattern `f (?x.1)`
-/
proj := .no
transparency := .reducible
: Meta.Config }.toConfigWithKey
@@ -131,9 +147,14 @@ private def mkIndexConfig (c : Config) : ConfigWithKey :=
/--
Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`.
-/
-- TODO: use `metaConfig` at `isDefEq`. It is not being used yet because it will break Mathlib.
private def mkMetaConfig (c : Config) : ConfigWithKey :=
{ c with
private def mkMetaConfig (c : Config) : MetaM ConfigWithKey := do
let curr Meta.getConfig
return { curr with
beta := c.beta
zeta := c.zeta
iota := c.iota
zetaDelta := c.zetaDelta
etaStruct := c.etaStruct
proj := if c.proj then .yesWithDelta else .no
transparency := .reducible
: Meta.Config }.toConfigWithKey
@@ -142,12 +163,16 @@ def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (
let config updateArith config
return {
config, simpTheorems, congrTheorems
metaConfig := mkMetaConfig config
indexConfig := mkIndexConfig config
metaConfig := ( mkMetaConfig config)
indexConfig := ( mkIndexConfig config)
}
def Context.setConfig (context : Context) (config : Config) : Context :=
{ context with config }
def Context.setConfig (context : Context) (config : Config) : MetaM Context := do
return { context with
config
metaConfig := ( mkMetaConfig config)
indexConfig := ( mkIndexConfig config)
}
def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
{ c with simpTheorems }
@@ -164,6 +189,9 @@ def Context.setFailIfUnchanged (c : Context) (flag : Bool) : Context :=
def Context.setMemoize (c : Context) (flag : Bool) : Context :=
{ c with config.memoize := flag }
def Context.setZetaDeltaSet (c : Context) (zetaDeltaSet : FVarIdSet) (initUsedZetaDelta : FVarIdSet) : Context :=
{ c with zetaDeltaSet, initUsedZetaDelta }
def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
ctx.simpTheorems.isDeclToUnfold declName
@@ -237,6 +265,12 @@ For example, if the user has set `simp (config := { zeta := false })`,
@[inline] def withSimpIndexConfig (x : SimpM α) : SimpM α := do
withConfigWithKey ( readThe Simp.Context).indexConfig x
/--
Executes `x` using a `MetaM` configuration for inferred from `Simp.Config`.
-/
@[inline] def withSimpMetaConfig (x : SimpM α) : SimpM α := do
withConfigWithKey ( readThe Simp.Context).metaConfig x
@[extern "lean_simp"]
opaque simp (e : Expr) : SimpM Result

View File

@@ -60,7 +60,7 @@ def _root_.Lean.MVarId.admit (mvarId : MVarId) (synthetic := true) : MetaM Unit
mvarId.withContext do
mvarId.checkNotAssigned `admit
let mvarType mvarId.getType
let val mkSorry mvarType synthetic
let val mkLabeledSorry mvarType synthetic (unique := true)
mvarId.assign val
/-- Beta reduce the metavariable type head -/

View File

@@ -349,8 +349,10 @@ end
-- Let-declarations marked as implementation detail should always be unfolded
-- We initially added this feature for `simp`, and added it here for consistency.
let cfg getConfig
unless cfg.zetaDelta || decl.isImplementationDetail do return e
if cfg.trackZetaDelta then
if !decl.isImplementationDetail && !cfg.zetaDelta then
if !( read).zetaDeltaSet.contains fvarId then
return e
if ( read).trackZetaDelta then
modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId }
whnfEasyCases v k
| .mvar mvarId =>
@@ -572,7 +574,17 @@ where
return ( go <| mkAppN (b.instantiate1 v) args)
let f := f.getAppFn
let f' go f
if cfg.beta && f'.isLambda then
/-
If `f'` is a lambda, then we perform beta-reduction here IF
1- `cfg.beta` is enabled, OR
2- `f` was not a lambda expression. That is, `f` was reduced, and the beta-reduction step is part
of this step. This is similar to allowing beta-reduction while unfolding expressions even if `cfg.beta := false`.
We added case 2 because a failure at `norm_cast`. See test `6123_mod_cast.lean`.
Another possible fix to this test is to set `beta := true` at the `Simp.Config` value at
`NormCast.lean`.
-/
if f'.isLambda && (cfg.beta || !f.isLambda) then
let revArgs := e.getAppRevArgs
go <| f'.betaRev revArgs
else if let some eNew whnfDelayedAssigned? f' e then

View File

@@ -215,7 +215,23 @@ However, in case it is copied and pasted from the Infoview, `⋯` logs a warning
@[builtin_term_parser] def omission := leading_parser
""
def binderIdent : Parser := ident <|> hole
/-- A temporary placeholder for a missing proof or value. -/
/--
The `sorry` term is a temporary placeholder for a missing proof or value.
The syntax is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output
of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.
"Go to definition" on `sorry` in the Infoview will go to the source position where it was introduced, if such information is available.
Each `sorry` is guaranteed to be unique, so for example the following fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```
See also the `sorry` tactic, which is short for `exact sorry`.
-/
@[builtin_term_parser] def «sorry» := leading_parser
"sorry"
/--

View File

@@ -142,8 +142,10 @@ open Lean PrettyPrinter Delaborator
Turns a `MetaM FormatWithInfos` into a `MessageData.lazy` which will run the monadic value.
-/
def ofFormatWithInfosM (fmt : MetaM FormatWithInfos) : MessageData :=
.lazy fun ctx => ctx.runMetaM <|
.ofFormatWithInfos <$> fmt
.lazy fun ctx => do
match ( ctx.runMetaM fmt |>.toBaseIO) with
| .ok fmt => return .ofFormatWithInfos fmt
| .error ex => return m!"[Error pretty printing: {ex}]"
/--
Turns a `MetaM MessageData` into a `MessageData.lazy` which will run the monadic value.
@@ -152,7 +154,11 @@ comprise the expressions that are included in the message data.
-/
def ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData :=
.lazy
(f := fun ppctxt => ppctxt.runMetaM f)
(f := fun ppctxt => do
match ( ppctxt.runMetaM f |>.toBaseIO) with
| .ok fmt => return fmt
| .error ex => return m!"[Error pretty printing: {ex}]"
)
(hasSyntheticSorry := fun mvarctxt => es.any (fun a =>
instantiateMVarsCore mvarctxt a |>.1.hasSyntheticSorry
))
@@ -168,11 +174,16 @@ def ofConst (e : Expr) : MessageData :=
let delab : Delab := withOptionAtCurrPos `pp.tagAppFns true delabConst
.ofFormatWithInfosM (PrettyPrinter.ppExprWithInfos (delab := delab) e)
else
have : Inhabited MessageData :=
m!"[Error pretty printing: expression not a constant]{Format.line}{e}"
panic! "not a constant"
/-- Generates `MessageData` for a declaration `c` as `c.{<levels>} <params> : <type>`, with terminfo. -/
def signature (c : Name) : MessageData :=
.ofFormatWithInfosM (PrettyPrinter.ppSignature c)
.lazy fun ctx => do
match ( ctx.runMetaM (PrettyPrinter.ppSignature c) |>.toBaseIO) with
| .ok fmt => return .ofFormatWithInfos fmt
| .error ex => return m!"[Error pretty printing signature: {ex}]{Format.line}{c}"
end MessageData

View File

@@ -211,6 +211,16 @@ where
stx := stx
}
def addDelabTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false)
(location? : Option DeclarationLocation := none) (docString? : Option String := none) (explicit : Bool := true) : DelabM Unit := do
let info := Info.ofDelabTermInfo {
toTermInfo := addTermInfo.mkTermInfo stx e (isBinder := isBinder)
location? := location?
docString? := docString?
explicit := explicit
}
modify fun s => { s with infos := s.infos.insert pos info }
/--
Annotates the term with the current expression position and registers `TermInfo`
to associate the term to the current expression.
@@ -221,13 +231,30 @@ def annotateTermInfo (stx : Term) : Delab := do
pure stx
/--
Modifies the delaborator so that it annotates the resulting term with the current expression
position and registers `TermInfo` to associate the term to the current expression.
Annotates the term with the current expression position and registers `TermInfo`
to associate the term to the current expression, unless the syntax has a synthetic position
and associated `Info` already.
-/
def annotateTermInfoUnlessAnnotated (stx : Term) : Delab := do
if let some (.synthetic pos pos') := stx.raw.getInfo? then
if pos == pos' && ( get).infos.contains pos then
return stx
annotateTermInfo stx
/--
Modifies the delaborator so that it annotates the resulting term using `annotateTermInfo`.
-/
def withAnnotateTermInfo (d : Delab) : Delab := do
let stx d
annotateTermInfo stx
/--
Modifies the delaborator so that it ensures resulting term is annotated using `annotateTermInfoUnlessAnnotated`.
-/
def withAnnotateTermInfoUnlessAnnotated (d : Delab) : Delab := do
let stx d
annotateTermInfoUnlessAnnotated stx
/--
Gets an name based on `suggestion` that is unused in the local context.
Erases macro scopes.
@@ -294,13 +321,7 @@ def OmissionReason.toString : OmissionReason → String
| maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
let info := Info.ofOmissionInfo <| mkOmissionInfo stx e
modify fun s => { s with infos := s.infos.insert pos info }
where
mkOmissionInfo stx e := return {
toTermInfo := addTermInfo.mkTermInfo stx e (isBinder := false)
reason := reason.toString
}
addDelabTermInfo pos stx e (docString? := reason.toString) (explicit := false)
/--
Runs the delaborator `act` with increased depth.
@@ -381,7 +402,7 @@ def omission (reason : OmissionReason) : Delab := do
partial def delabFor : Name Delab
| Name.anonymous => failure
| k =>
(do annotateTermInfo ( (delabAttribute.getValues ( getEnv) k).firstM id))
(do annotateTermInfoUnlessAnnotated ( (delabAttribute.getValues ( getEnv) k).firstM id))
-- have `app.Option.some` fall back to `app` etc.
<|> if k.isAtomic then failure else delabFor k.getRoot
@@ -433,7 +454,7 @@ open SubExpr (Pos PosMap)
open Delaborator (OptionsPerPos topDownAnalyze DelabM)
def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM α) :
MetaM (α × PosMap Elab.Info) := do
MetaM (α × PosMap Elab.Info) := do
/- Using `erasePatternAnnotations` here is a bit hackish, but we do it
`Expr.mdata` affects the delaborator. TODO: should we fix that? -/
let e Meta.erasePatternRefAnnotations e
@@ -453,7 +474,8 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM
topDownAnalyze e
else pure optionsPerPos
let (stx, {infos := infos, ..}) catchInternalId Delaborator.delabFailureId
(delab
-- Clear the ref to ensure that quotations in delaborators start with blank source info.
(MonadRef.withRef .missing delab
{ optionsPerPos := optionsPerPos
currNamespace := ( getCurrNamespace)
openDecls := ( getOpenDecls)

View File

@@ -587,7 +587,7 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
else
let delabHead (insertExplicit : Bool) : Delab := do
guard <| !insertExplicit
withAnnotateTermInfo x
withAnnotateTermInfoUnlessAnnotated x
delabAppCore (n - arity) delabHead (unexpand := false)
@[builtin_delab app]
@@ -1287,6 +1287,35 @@ def delabNameMkStr : Delab := whenPPOption getPPNotation do
@[builtin_delab app.Lean.Name.num]
def delabNameMkNum : Delab := delabNameMkStr
@[builtin_delab app.sorryAx]
def delabSorry : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExplicit do
let numArgs := ( getExpr).getAppNumArgs
guard <| numArgs 2
-- Cache the current position's value, since it might be applied to the entire application.
let sorrySource getPPOption getPPSorrySource
-- If this is constructed by `Lean.Meta.mkLabeledSorry`, then normally we don't print the unique tag.
-- But, if `pp.explicit` is false and `pp.sorrySource` is true, then print a simplified version of the tag.
if let some view := isLabeledSorry? ( getExpr) then
withOverApp 3 do
if let some loc := view.module? then
let (stx, explicit)
if pure sorrySource <||> getPPOption getPPSorrySource then
let posAsName := Name.mkSimple s!"{loc.module}:{loc.range.pos.line}:{loc.range.pos.column}"
let pos := mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{posAsName}"]
let src withAppArg <| annotateTermInfo pos
pure ( `(sorry $src), true)
else
-- Set `explicit` to false so that the first hover sets `pp.sorrySource` to true in `Lean.Widget.ppExprTagged`
pure ( `(sorry), false)
let stx annotateCurPos stx
addDelabTermInfo ( getPos) stx ( getExpr) (explicit := explicit) (location? := loc)
(docString? := "This is a `sorry` term associated to a source position. Use 'Go to definition' to go there.")
return stx
else
`(sorry)
else
withOverApp 2 `(sorry)
open Parser Command Term in
@[run_builtin_parser_attribute_hooks]
-- use `termParser` instead of `declId` so we can reuse `delabConst`

View File

@@ -39,6 +39,11 @@ register_builtin_option pp.match : Bool := {
group := "pp"
descr := "(pretty printer) disable/enable 'match' notation"
}
register_builtin_option pp.sorrySource : Bool := {
defValue := false
group := "pp"
descr := "(pretty printer) if true, pretty print 'sorry' with its originating source position, if available"
}
register_builtin_option pp.coercions : Bool := {
defValue := true
group := "pp"
@@ -262,6 +267,7 @@ def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
def getPPParens (o : Options) : Bool := o.get pp.parens.name pp.parens.defValue
def getPPUnicodeFun (o : Options) : Bool := o.get pp.unicode.fun.name false
def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o)
def getPPSorrySource (o : Options) : Bool := o.get pp.sorrySource.name pp.sorrySource.defValue
def getPPFieldNotation (o : Options) : Bool := o.get pp.fieldNotation.name (!getPPAll o)
def getPPFieldNotationGeneralized (o : Options) : Bool := o.get pp.fieldNotation.generalized.name pp.fieldNotation.generalized.defValue
def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o)

View File

@@ -152,13 +152,22 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
let i := ictx.info
let ci := ictx.ctx
let children := ictx.children
match i with
| .ofTermInfo ti =>
let locationLinksDefault : RequestM (Array LocationLink) := do
-- If other go-tos fail, we try to show the elaborator or parser
if let some ei := i.toElabInfo? then
if kind == declaration && ci.env.contains ei.stx.getKind then
return ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
if kind == definition && ci.env.contains ei.elaborator then
return ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
return #[]
let locationLinksFromTermInfo (ti : TermInfo) : RequestM (Array LocationLink) := do
let mut expr := ti.expr
if kind == type then
expr ci.runMetaM i.lctx do
return Expr.getAppFn ( instantiateMVars ( Meta.inferType expr))
match expr with
match expr.consumeMData with
| Expr.const n .. => return ci.runMetaM i.lctx <| locationLinksFromDecl i n
| Expr.fvar id .. => return ci.runMetaM i.lctx <| locationLinksFromBinder i id
| _ => pure ()
@@ -176,7 +185,7 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
-- go-to-definition on a projection application of a typeclass
-- should return all instances generated by TC
expr ci.runMetaM i.lctx do instantiateMVars expr
if let .const n _ := expr.getAppFn then
if let .const n _ := expr.getAppFn.consumeMData then
-- also include constant along with instance results
let mut results ci.runMetaM i.lctx <| locationLinksFromDecl i n
if let some info := ci.env.getProjectionFnInfo? n then
@@ -193,12 +202,29 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
| .const declName _ => do
if ci.runMetaM i.lctx do Lean.Meta.isInstance declName then pure #[declName] else pure #[]
| .app fn arg => do pure $ ( extractInstances fn).append ( extractInstances arg)
| .mdata _ e => extractInstances e
| _ => pure #[]
if let some instArg := appArgs.get? instIdx then
for inst in ( extractInstances instArg) do
results := results.append ( ci.runMetaM i.lctx <| locationLinksFromDecl i inst)
results := results.append elaborators -- put elaborators at the end of the results
return results
locationLinksDefault
match i with
| .ofTermInfo ti =>
return locationLinksFromTermInfo ti
| .ofDelabTermInfo { toTermInfo := ti, location?, .. } =>
if let some location := location? then
if let some targetUri documentUriFromModule rc.srcSearchPath location.module then
let range := location.range.toLspRange
let result : LocationLink := {
targetUri, targetRange := range, targetSelectionRange := range,
originSelectionRange? := (·.toLspRange text) <$> i.range?
}
return #[result]
-- If we fail to find a DocumentUri, fall through and use the default method to at least try to have something to jump to.
return locationLinksFromTermInfo ti
| .ofFieldInfo fi =>
if kind == type then
let expr ci.runMetaM i.lctx do
@@ -213,13 +239,7 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
if kind == definition || kind == declaration then
return ci.runMetaM i.lctx <| locationLinksFromImport i
| _ => pure ()
-- If other go-tos fail, we try to show the elaborator or parser
if let some ei := i.toElabInfo? then
if kind == declaration && ci.env.contains ei.stx.getKind then
return ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
if kind == definition && ci.env.contains ei.elaborator then
return ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
return #[]
locationLinksDefault
open Elab GoToKind in
def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)

View File

@@ -53,13 +53,12 @@ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
| some type => some <$> ppExprTagged type
| none => pure none
let exprExplicit? match i.info with
| Elab.Info.ofTermInfo ti =>
pure <| some <| ppExprTaggedWithoutTopLevelHighlight ti.expr (explicit := true)
| Elab.Info.ofOmissionInfo { toTermInfo := ti, .. } =>
-- Omitted terms are simply to be expanded, not printed explicitly.
-- Keep the top-level tag so that users can also see the explicit version
-- of the omitted term.
pure <| some <| ppExprTagged ti.expr (explicit := false)
| Elab.Info.ofTermInfo ti
| Elab.Info.ofDelabTermInfo { toTermInfo := ti, explicit := true, ..} =>
some <$> ppExprTaggedWithoutTopLevelHighlight ti.expr (explicit := true)
| Elab.Info.ofDelabTermInfo { toTermInfo := ti, explicit := false, ..} =>
-- Keep the top-level tag so that users can also see the explicit version of the term on an additional hover.
some <$> ppExprTagged ti.expr (explicit := false)
| Elab.Info.ofFieldInfo fi => pure <| some <| TaggedText.text fi.fieldName.toString
| _ => pure none
return {

View File

@@ -146,13 +146,13 @@ def Info.stx : Info → Syntax
| ofUserWidgetInfo i => i.stx
| ofFVarAliasInfo _ => .missing
| ofFieldRedeclInfo i => i.stx
| ofOmissionInfo i => i.stx
| ofDelabTermInfo i => i.stx
| ofChoiceInfo i => i.stx
def Info.lctx : Info LocalContext
| .ofTermInfo i => i.lctx
| .ofFieldInfo i => i.lctx
| .ofOmissionInfo i => i.lctx
| .ofDelabTermInfo i => i.lctx
| .ofMacroExpansionInfo i => i.lctx
| .ofCompletionInfo i => i.lctx
| _ => LocalContext.empty
@@ -251,15 +251,17 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
def Info.type? (i : Info) : MetaM (Option Expr) :=
match i with
| Info.ofTermInfo ti => Meta.inferType ti.expr
| Info.ofFieldInfo fi => Meta.inferType fi.val
| Info.ofOmissionInfo oi => Meta.inferType oi.expr
| Info.ofTermInfo ti => Meta.inferType ti.expr
| Info.ofFieldInfo fi => Meta.inferType fi.val
| Info.ofDelabTermInfo ti => Meta.inferType ti.expr
| _ => return none
def Info.docString? (i : Info) : MetaM (Option String) := do
let env getEnv
match i with
| .ofTermInfo ti =>
| .ofDelabTermInfo { docString? := some s, .. } => return s
| .ofTermInfo ti
| .ofDelabTermInfo ti =>
if let some n := ti.expr.constName? then
return ( findDocString? env n)
| .ofFieldInfo fi => return findDocString? env fi.projName
@@ -269,7 +271,6 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
if let some decl := ( getOptionDecls).find? oi.optionName then
return decl.descr
return none
| .ofOmissionInfo { reason := s, .. } => return s -- Show the omission reason for the docstring.
| _ => pure ()
if let some ei := i.toElabInfo? then
return findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
@@ -418,7 +419,7 @@ where go ci?
| .node i cs =>
match ci?, i with
| some ci, .ofTermInfo ti
| some ci, .ofOmissionInfo { toTermInfo := ti, .. } => do
| some ci, .ofDelabTermInfo ti => do
-- NOTE: `instantiateMVars` can potentially be expensive but we rely on the elaborator
-- creating a fully instantiated `MutualDef.body` term info node which has the implicit effect
-- of making the `instantiateMVars` here a no-op and avoids further recursing into the body

View File

@@ -54,55 +54,73 @@ structure PPFns where
ppExprWithInfos : PPContext Expr IO FormatWithInfos
ppConstNameWithInfos : PPContext Name IO FormatWithInfos
ppTerm : PPContext Term IO Format
ppLevel : PPContext Level IO Format
ppLevel : PPContext Level BaseIO Format
ppGoal : PPContext MVarId IO Format
deriving Inhabited
def formatRawTerm (ctx : PPContext) (stx : Term) : Format :=
stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts)
def formatRawGoal (mvarId : MVarId) : Format :=
"goal " ++ format (mkMVar mvarId)
builtin_initialize ppFnsRef : IO.Ref PPFns
IO.mkRef {
ppExprWithInfos := fun _ e => return format (toString e)
ppConstNameWithInfos := fun _ n => return format n
ppTerm := fun ctx stx => return stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts)
ppTerm := fun ctx stx => return formatRawTerm ctx stx
ppLevel := fun _ l => return format l
ppGoal := fun _ _ => return "goal"
ppGoal := fun _ mvarId => return formatRawGoal mvarId
}
builtin_initialize ppExt : EnvExtension PPFns
registerEnvExtension ppFnsRef.get
def ppExprWithInfos (ctx : PPContext) (e : Expr) : IO FormatWithInfos := do
def ppExprWithInfos (ctx : PPContext) (e : Expr) : BaseIO FormatWithInfos := do
if pp.raw.get ctx.opts then
let e := instantiateMVarsCore ctx.mctx e |>.1
return format (toString e)
else
try
ppExt.getState ctx.env |>.ppExprWithInfos ctx e
catch ex =>
match ( ppExt.getState ctx.env |>.ppExprWithInfos ctx e |>.toBaseIO) with
| .ok fmt => return fmt
| .error ex =>
if pp.rawOnError.get ctx.opts then
pure f!"[Error pretty printing expression: {ex}. Falling back to raw printer.]{Format.line}{e}"
else
pure f!"failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)"
def ppConstNameWithInfos (ctx : PPContext) (n : Name) : IO FormatWithInfos :=
ppExt.getState ctx.env |>.ppConstNameWithInfos ctx n
def ppConstNameWithInfos (ctx : PPContext) (n : Name) : BaseIO FormatWithInfos := do
match ( ppExt.getState ctx.env |>.ppConstNameWithInfos ctx n |>.toBaseIO) with
| .ok fmt => return fmt
| .error ex =>
if pp.rawOnError.get ctx.opts then
pure f!"[Error pretty printing constant: {ex}. Falling back to raw printer.]{Format.line}{format n}"
else
pure f!"failed to pretty print constant (use 'set_option pp.rawOnError true' for raw representation)"
def ppTerm (ctx : PPContext) (stx : Term) : IO Format :=
let fmtRaw := fun () => stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts)
def ppTerm (ctx : PPContext) (stx : Term) : BaseIO Format := do
if pp.raw.get ctx.opts then
return fmtRaw ()
return formatRawTerm ctx stx
else
try
ppExt.getState ctx.env |>.ppTerm ctx stx
catch ex =>
match ( ppExt.getState ctx.env |>.ppTerm ctx stx |>.toBaseIO) with
| .ok fmt => return fmt
| .error ex =>
if pp.rawOnError.get ctx.opts then
pure f!"[Error pretty printing syntax: {ex}. Falling back to raw printer.]{Format.line}{fmtRaw ()}"
pure f!"[Error pretty printing syntax: {ex}. Falling back to raw printer.]{Format.line}{formatRawTerm ctx stx}"
else
pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)"
def ppLevel (ctx : PPContext) (l : Level) : IO Format :=
def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format :=
ppExt.getState ctx.env |>.ppLevel ctx l
def ppGoal (ctx : PPContext) (mvarId : MVarId) : IO Format :=
ppExt.getState ctx.env |>.ppGoal ctx mvarId
def ppGoal (ctx : PPContext) (mvarId : MVarId) : BaseIO Format := do
match ( ppExt.getState ctx.env |>.ppGoal ctx mvarId |>.toBaseIO) with
| .ok fmt => return fmt
| .error ex =>
if pp.rawOnError.get ctx.opts then
pure f!"[Error pretty printing goal: {ex}. Falling back to raw printer.]{Format.line}{formatRawGoal mvarId}"
else
pure f!"failed to pretty print goal (use 'set_option pp.rawOnError true' for raw representation)"
end Lean

View File

@@ -25,7 +25,7 @@ This method ensures there is at most one warning message of this kind in the mes
def checkExponent (n : Nat) : CoreM Bool := do
let threshold := exponentiation.threshold.get ( getOptions)
if n > threshold then
if ( reportMessageKind `unsafe.exponentiation) then
if ( logMessageKind `unsafe.exponentiation) then
logWarning s!"exponent {n} exceeds the threshold {threshold}, exponentiation operation was not evaluated, use `set_option {exponentiation.threshold.name} <num>` to set a new threshold"
return false
else

View File

@@ -9,17 +9,17 @@ import Lean.Declaration
namespace Lean
def Expr.isSorry : Expr Bool
| app (app (.const ``sorryAx ..) ..) .. => true
| _ => false
/-- Returns `true` if the expression is an application of `sorryAx`. -/
def Expr.isSorry (e : Expr) : Bool :=
e.isAppOf ``sorryAx
def Expr.isSyntheticSorry : Expr Bool
| app (app (const ``sorryAx ..) ..) (const ``Bool.true ..) => true
| _ => false
/-- Returns `true` if the expression is of the form `sorryAx _ true ..`. -/
def Expr.isSyntheticSorry (e : Expr) : Bool :=
e.isAppOf ``sorryAx && e.getAppNumArgs 2 && (e.getArg! 1).isConstOf ``Bool.true
def Expr.isNonSyntheticSorry : Expr Bool
| app (app (const ``sorryAx ..) ..) (const ``Bool.false ..) => true
| _ => false
/-- Returns `true` if the expression is of the form `sorryAx _ false ..`. -/
def Expr.isNonSyntheticSorry (e : Expr) : Bool :=
e.isAppOf ``sorryAx && e.getAppNumArgs 2 && (e.getArg! 1).isConstOf ``Bool.false
def Expr.hasSorry (e : Expr) : Bool :=
Option.isSome <| e.find? (·.isConstOf ``sorryAx)

View File

@@ -86,7 +86,7 @@ variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions
def printTraces : m Unit := do
for {msg, ..} in ( getTraceState).traces do
IO.println ( msg.format)
IO.println ( msg.format.toIO)
def resetTraceState : m Unit :=
modifyTraceState (fun _ => {})

View File

@@ -84,6 +84,7 @@ def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos :=
delabApp
else
withOptionAtCurrPos pp.proofs.name true do
withOptionAtCurrPos pp.sorrySource.name true do
delab
let mut e := e
-- When hovering over a metavariable, we want to see its value, even if `pp.instantiateMVars` is false.

View File

@@ -830,9 +830,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
simp_to_model using List.containsKey_eq_keys_contains.symm
@[simp]
theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
theorem mem_keys [LawfulBEq α] (h : m.1.WF) {k : α} :
k m.1.keys m.contains k := by
simp_to_model
simp_to_model
rw [List.containsKey_eq_keys_contains]
theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :

View File

@@ -111,15 +111,11 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k
a m.insert k v (k == a) = false a m := by
simpa [mem_iff_contains, -contains_insert] using contains_of_contains_insert
@[simp]
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).contains k :=
Raw₀.contains_insert_self m.1, _ m.2
(m.insert k v).contains k := by simp
@[simp]
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
k m.insert k v := by
simp [mem_iff_contains, contains_insert_self]
k m.insert k v := by simp
@[simp]
theorem size_empty {c} : (empty c : DHashMap α β).size = 0 :=
@@ -959,13 +955,13 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
Raw₀.contains_keys m.1, _ m.2
@[simp]
theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
k m.keys k m := by
theorem mem_keys [LawfulBEq α] {k : α} :
k m.keys k m := by
rw [mem_iff_contains]
exact Raw₀.mem_keys m.1, _ m.2
theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
m.keys.Pairwise (fun a b => (a == b) = false) :=
m.keys.Pairwise (fun a b => (a == b) = false) :=
Raw₀.distinct_keys m.1, m.2.size_buckets_pos m.2
end Std.DHashMap

View File

@@ -119,14 +119,11 @@ theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β}
a m.insert k v (k == a) = false a m :=
DHashMap.mem_of_mem_insert
@[simp]
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).contains k :=
DHashMap.contains_insert_self
(m.insert k v).contains k := by simp
@[simp]
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k m.insert k v :=
DHashMap.mem_insert_self
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k m.insert k v := by
simp
@[simp]
theorem size_empty {c} : (empty c : HashMap α β).size = 0 :=

View File

@@ -122,13 +122,10 @@ theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.insert k ¬((k == a) ¬k m) a m :=
DHashMap.mem_of_mem_insertIfNew'
@[simp]
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k :=
HashMap.contains_insertIfNew_self
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).contains k := by
simp
@[simp]
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k m.insert k :=
HashMap.mem_insertIfNew_self
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k m.insert k := by simp
@[simp]
theorem size_empty {c} : (empty c : HashSet α).size = 0 :=

View File

@@ -471,7 +471,7 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
have := input.lhs.ref.hgate
have := input.rhs.ref.hgate
omega
{ aig with decls, invariant, cache }, g, by simp [decls]
{ aig with decls, invariant, cache }, g, by simp [g, decls]
/--
Add a new input node to the AIG in `aig`. Note that this version is only meant for proving,
@@ -487,7 +487,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
split at h2
· apply aig.invariant <;> assumption
· contradiction
{ decls, invariant, cache }, g, by simp [decls]
{ decls, invariant, cache }, g, by simp [g, decls]
/--
Add a new constant node to `aig`. Note that this version is only meant for proving,
@@ -503,7 +503,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
split at h2
· apply aig.invariant <;> assumption
· contradiction
{ decls, invariant, cache }, g, by simp [decls]
{ decls, invariant, cache }, g, by simp [g, decls]
end AIG

View File

@@ -505,7 +505,7 @@ def State.addConst (state : State aig) (idx : Nat) (h : idx < aig.decls.size)
let newCnf := Decl.constToCNF (.inr idx, h) b
have hinv := toCNF.State.Inv_constToCNF htip
let cache, hcache := cache.addConst idx h htip
newCnf ++ cnf, cache, State.Inv_append hinv inv, by simp [hcache]
newCnf ++ cnf, cache, State.Inv_append hinv inv, by simp [newCnf, hcache]
/--
Add the CNF for a `Decl.atom` to the state.
@@ -517,7 +517,7 @@ def State.addAtom (state : State aig) (idx : Nat) (h : idx < aig.decls.size)
let newCnf := Decl.atomToCNF (.inr idx, h) (.inl a)
have hinv := toCNF.State.Inv_atomToCNF htip
let cache, hcache := cache.addAtom idx h htip
newCnf ++ cnf, cache, State.Inv_append hinv inv, by simp [hcache]
newCnf ++ cnf, cache, State.Inv_append hinv inv, by simp [newCnf, hcache]
/--
Add the CNF for a `Decl.gate` to the state.
@@ -537,7 +537,7 @@ def State.addGate (state : State aig) {hlb} {hrb} (idx : Nat) (h : idx < aig.dec
rinv
have hinv := toCNF.State.Inv_gateToCNF htip
let cache, hcache := cache.addGate idx h htip hl hr
newCnf ++ cnf, cache, State.Inv_append hinv inv, by simp [hcache]
newCnf ++ cnf, cache, State.Inv_append hinv inv, by simp [newCnf, hcache]
/--
Evaluate the CNF contained within the state.

View File

@@ -65,7 +65,7 @@ def relabel (r : α → β) (aig : AIG α) : AIG β :=
cache,
invariant := by
intro idx lhs rhs linv rinv hbound hgate
simp [decls] at hgate
simp +zetaDelta [decls] at hgate
have := Decl.relabel_gate hgate
apply aig.invariant
assumption

View File

@@ -494,7 +494,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
conv => rhs; rw [Array.size_mk]
conv => rhs; rw [Array.size_toArray]
exact hbound
simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_toList, decidableGetElem?] at heq
@@ -527,7 +527,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
conv => rhs; rw [Array.size_mk]
conv => rhs; rw [Array.size_toArray]
exact hbound
simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_toList, decidableGetElem?] at heq
@@ -587,7 +587,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
· next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx < f.clauses.size := by
conv => rhs; rw [Array.size_mk]
conv => rhs; rw [Array.size_toArray]
exact hbound
simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, reduceDIte,
Fin.eta, Array.get_eq_getElem, Array.getElem_toList, decidableGetElem?] at heq

View File

@@ -224,7 +224,7 @@ theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p
have insertRupUnits_rw : (insertRupUnits f (negate c)).1 =
(insertRupUnits f (negate c)).1.clauses, (insertRupUnits f (negate c)).1.rupUnits,
(insertRupUnits f (negate c)).1.ratUnits, (insertRupUnits f (negate c)).1.assignments := rfl
simp only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints,
simp +zetaDelta only [performRatCheck_fold_formula_eq performRupCheck_res h_performRupCheck_res (Literal.negate p) ratHints,
clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
restoreAssignments_performRupCheck fc fc_assignments_size, insertRupUnits_rw,
clear_insertRup f f_readyForRatAdd.2 (negate c), fc, performRupCheck_res]

View File

@@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
units.size, units_size_lt_updatedUnits_size
have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
refine mostRecentUnitIdx, l.2, i_gt_zero, ?_
simp only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
simp +zetaDelta only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
constructor
· rfl
· constructor
@@ -131,7 +131,6 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
exact k_property
· intro h
simp only [ h, not_true, mostRecentUnitIdx] at hk
exact hk rfl
rw [Array.getElem_push_lt _ _ _ k_in_bounds]
rw [i_eq_l] at h2
exact h2 k.1, k_in_bounds
@@ -193,7 +192,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
constructor
· rw [Array.getElem_push_lt units l j.1 j.2, h1]
· constructor
· simp [i_eq_l, hl]
· simp +zetaDelta [i_eq_l, hl]
rfl
· constructor
· simp only [i_eq_l]
@@ -228,7 +227,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
refine mostRecentUnitIdx, j.1, j_lt_updatedUnits_size, i_gt_zero, ?_
simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq]
constructor
· simp [i_eq_l, hl]
· simp +zetaDelta [i_eq_l, hl]
rfl
· constructor
· rw [Array.getElem_push_lt units l j.1 j.2, h1]
@@ -1115,11 +1114,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
simp [li, Array.getElem_mem]
have i_in_bounds : i.1 < derivedLits.length := by
have i_property := i.2
simp only [derivedLits_arr_def, Array.size_mk] at i_property
simp only [derivedLits_arr_def, Array.size_toArray] at i_property
exact i_property
have j_in_bounds : j.1 < derivedLits.length := by
have j_property := j.2
simp only [derivedLits_arr_def, Array.size_mk] at j_property
simp only [derivedLits_arr_def, Array.size_toArray] at j_property
exact j_property
rcases derivedLits_satisfies_invariant li.1.1, li.1.2.2 with _, h2 | k, _, _, _, h3 |
k1, k2, _, _, k1_eq_true, k2_eq_false, _, _, h3
@@ -1216,7 +1215,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
exact h2 derivedLits_arr[j] idx_in_list
· apply Or.inr Or.inl
have j_lt_derivedLits_arr_size : j.1 < derivedLits_arr.size := by
simp only [derivedLits_arr_def, Array.size_mk]
simp only [derivedLits_arr_def, Array.size_toArray]
exact j.2
have i_gt_zero : i.1 > 0 := by rw [ j_eq_i]; exact (List.get derivedLits j).1.2.1
refine j.1, j_lt_derivedLits_arr_size, List.get derivedLits j |>.2, i_gt_zero, ?_
@@ -1229,7 +1228,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
intro k _ k_ne_j
have k_in_bounds : k < derivedLits.length := by
have k_property := k.2
simp only [derivedLits_arr_def, Array.size_mk] at k_property
simp only [derivedLits_arr_def, Array.size_toArray] at k_property
exact k_property
have k_ne_j : k.1, k_in_bounds j := by
apply Fin.ne_of_val_ne
@@ -1239,10 +1238,10 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
exact h3 k.1, k_in_bounds k_ne_j
· apply Or.inr Or.inr
have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
simp only [derivedLits_arr_def, Array.size_mk]
simp only [derivedLits_arr_def, Array.size_toArray]
exact j1.2
have j2_lt_derivedLits_arr_size : j2.1 < derivedLits_arr.size := by
simp only [derivedLits_arr_def, Array.size_mk]
simp only [derivedLits_arr_def, Array.size_toArray]
exact j2.2
have i_gt_zero : i.1 > 0 := by rw [ j1_eq_i]; exact (List.get derivedLits j1).1.2.1
refine j1.1, j1_lt_derivedLits_arr_size,
@@ -1260,7 +1259,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
intro k _ k_ne_j1 k_ne_j2
have k_in_bounds : k < derivedLits.length := by
have k_property := k.2
simp only [derivedLits_arr_def, Array.size_mk] at k_property
simp only [derivedLits_arr_def, Array.size_toArray] at k_property
exact k_property
have k_ne_j1 : k.1, k_in_bounds j1 := by
apply Fin.ne_of_val_ne
@@ -1328,7 +1327,7 @@ theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (ru
have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
rw [size_assignments_insertRupUnits f (negate c)]
exact f_readyForRupAdd.2.1
simp only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
simp +zetaDelta only [clauses_performRupCheck, rupUnits_performRupCheck, ratUnits_performRupCheck,
restoreAssignments_performRupCheck fc fc_assignments_size, Prod.mk.injEq, and_true] at rupAddSuccess
have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
rw [rupAddSuccess]

View File

@@ -48,7 +48,7 @@ def ofOrdinal (ordinal : Day.Ordinal.OfYear leap) : ValidDate leap :=
let bounded := Bounded.LE.mk ordinal.val (And.intro h h₁) |>.sub acc
let bounded : Bounded.LE 1 monthDays.val := bounded.cast (by omega) (by omega)
let days₁ : Day.Ordinal := bounded.val, And.intro bounded.property.left (Int.le_trans bounded.property.right monthDays.property.right)
idx, days₁, Int.le_trans bounded.property.right (by simp)
idx, days₁, Int.le_trans bounded.property.right (by simp +zetaDelta)
else by
let h₂ := Int.not_le.mp h₁

View File

@@ -9,7 +9,6 @@ import Lake.Config.Package
import Lake.CLI.Translate.Toml
import Lake.CLI.Translate.Lean
import Lake.Load.Lean.Elab
import Lean.PrettyPrinter
namespace Lake
open Toml Lean System PrettyPrinter

View File

@@ -268,10 +268,10 @@ instance : OfNat Log.Pos (nat_lit 0) := ⟨⟨0⟩⟩
instance : Ord Log.Pos := (compare ·.val ·.val)
instance : LT Log.Pos := (·.val < ·.val)
instance : DecidableRel (LT.lt (α := Log.Pos)) :=
inferInstanceAs (DecidableRel (α := Log.Pos) (·.val < ·.val))
inferInstanceAs (DecidableRel (α := Log.Pos) (β := Log.Pos) (·.val < ·.val))
instance : LE Log.Pos := (·.val ·.val)
instance : DecidableRel (LE.le (α := Log.Pos)) :=
inferInstanceAs (DecidableRel (α := Log.Pos) (·.val ·.val))
inferInstanceAs (DecidableRel (α := Log.Pos) (β := Log.Pos) (·.val ·.val))
instance : Min Log.Pos := minOfLe
instance : Max Log.Pos := maxOfLe

View File

@@ -55,11 +55,8 @@ def mkMessageStringCore
def mkMessageString (msg : Message) (includeEndPos := false) (infoWithPos := false) : BaseIO String := do
let endPos? := if includeEndPos then msg.endPos else none
match ( msg.data.toString.toBaseIO) with
| .ok s =>
return mkMessageStringCore msg.severity msg.fileName msg.caption s msg.pos endPos? infoWithPos
| .error e =>
return mkMessageStringCore .error msg.fileName msg.caption (toString e) msg.pos endPos? infoWithPos
let s msg.data.toString
return mkMessageStringCore msg.severity msg.fileName msg.caption s msg.pos endPos? infoWithPos
def mkMessageLogString (log : MessageLog) : BaseIO String :=
log.toList.foldlM (init := "") fun s m => do

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