Skip to content

Commit

Permalink
Merge branch 'master' into shift-msb-lsb
Browse files Browse the repository at this point in the history
  • Loading branch information
luisacicolini committed Oct 5, 2024
2 parents b509af4 + 0178f2b commit dcedcad
Showing 603 changed files with 179,973 additions and 166,123 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/pr-release.yml
Original file line number Diff line number Diff line change
@@ -340,7 +340,7 @@ jobs:
# (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
lake update batteries
get add lake-manifest.json
git add lake-manifest.json
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi
2 changes: 1 addition & 1 deletion RELEASES.md
Original file line number Diff line number Diff line change
@@ -181,7 +181,7 @@ v4.12.0
* [#4953](https://github.com/leanprover/lean4/pull/4953) defines "and-inverter graphs" (AIGs) as described in section 3 of [Davis-Swords 2013](https://arxiv.org/pdf/1304.7861.pdf).
* **Parsec**
* [#4774](https://github.com/leanprover/lean4/pull/4774) generalizes the `Parsec` library, allowing parsing of iterable data beyong `String` such as `ByteArray`. (See breaking changes.)
* [#4774](https://github.com/leanprover/lean4/pull/4774) generalizes the `Parsec` library, allowing parsing of iterable data beyond `String` such as `ByteArray`. (See breaking changes.)
* [#5115](https://github.com/leanprover/lean4/pull/5115) moves `Lean.Data.Parsec` to `Std.Internal.Parsec` for bootstrappng reasons.
* `Thunk`
6 changes: 3 additions & 3 deletions src/Init/Control/Lawful/Basic.lean
Original file line number Diff line number Diff line change
@@ -183,9 +183,9 @@ end Id

instance : LawfulMonad Option := LawfulMonad.mk'
(id_map := fun x => by cases x <;> rfl)
(pure_bind := fun x f => rfl)
(bind_assoc := fun x f g => by cases x <;> rfl)
(bind_pure_comp := fun f x => by cases x <;> rfl)
(pure_bind := fun _ _ => rfl)
(bind_assoc := fun x _ _ => by cases x <;> rfl)
(bind_pure_comp := fun _ x => by cases x <;> rfl)

instance : LawfulApplicative Option := inferInstance
instance : LawfulFunctor Option := inferInstance
4 changes: 2 additions & 2 deletions src/Init/Control/Lawful/Instances.lean
Original file line number Diff line number Diff line change
@@ -95,8 +95,8 @@ end ExceptT

instance : LawfulMonad (Except ε) := LawfulMonad.mk'
(id_map := fun x => by cases x <;> rfl)
(pure_bind := fun a f => rfl)
(bind_assoc := fun a f g => by cases a <;> rfl)
(pure_bind := fun _ _ => rfl)
(bind_assoc := fun a _ _ => by cases a <;> rfl)

instance : LawfulApplicative (Except ε) := inferInstance
instance : LawfulFunctor (Except ε) := inferInstance
149 changes: 149 additions & 0 deletions src/Init/Data/Array/Attach.lean
Original file line number Diff line number Diff line change
@@ -5,6 +5,7 @@ Authors: Joachim Breitner, Mario Carneiro
-/
prelude
import Init.Data.Array.Mem
import Init.Data.Array.Lemmas
import Init.Data.List.Attach

namespace Array
@@ -26,4 +27,152 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
with the same elements but in the type `{x // x ∈ xs}`. -/
@[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id

@[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
l.toArray.attachWith P H = (l.attachWith P (by simpa using H)).toArray := by
simp [attachWith]

@[simp] theorem _root_.List.attach_toArray {l : List α} :
l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
simp [attach]

@[simp] theorem toList_attachWith {l : Array α} {P : α → Prop} {H : ∀ x ∈ l, P x} :
(l.attachWith P H).toList = l.toList.attachWith P (by simpa [mem_toList] using H) := by
simp [attachWith]

@[simp] theorem toList_attach {α : Type _} {l : Array α} :
l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
simp [attach]

/-! ## unattach
`Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
We use it by providing a simp lemma `l.attach.unattach = l`, and simp lemmas which recognize higher order
functions applied to `l : Array { x // p x }` which only depend on the value, not the predicate, and rewrite these
in terms of a simpler function applied to `l.unattach`.
Further, we provide simp lemmas that push `unattach` inwards.
-/

/--
A synonym for `l.map (·.val)`. Mostly this should not be needed by users.
It is introduced as in intermediate step by lemmas such as `map_subtype`,
and is ideally subsequently simplified away by `unattach_attach`.
If not, usually the right approach is `simp [Array.unattach, -Array.map_subtype]` to unfold.
-/
def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (·.val)

@[simp] theorem unattach_nil {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := rfl
@[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {l : Array { x // p x }} :
(l.push a).unattach = l.unattach.push a.1 := by
simp only [unattach, Array.map_push]

@[simp] theorem size_unattach {p : α → Prop} {l : Array { x // p x }} :
l.unattach.size = l.size := by
unfold unattach
simp

@[simp] theorem _root_.List.unattach_toArray {p : α → Prop} {l : List { x // p x }} :
l.toArray.unattach = l.unattach.toArray := by
simp only [unattach, List.map_toArray, List.unattach]

@[simp] theorem toList_unattach {p : α → Prop} {l : Array { x // p x }} :
l.unattach.toList = l.toList.unattach := by
simp only [unattach, toList_map, List.unattach]

@[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
cases l
simp

@[simp] theorem unattach_attachWith {p : α → Prop} {l : Array α}
{H : ∀ a ∈ l, p a} :
(l.attachWith p H).unattach = l := by
cases l
simp

/-! ### Recognizing higher order functions using a function that only depends on the value. -/

/--
This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
theorem foldl_subtype {p : α → Prop} {l : Array { x // p x }}
{f : β → { x // p x } → β} {g : β → α → β} {x : β}
{hf : ∀ b x h, f b ⟨x, h⟩ = g b x} :
l.foldl f x = l.unattach.foldl g x := by
cases l
simp only [List.foldl_toArray', List.unattach_toArray]
rw [List.foldl_subtype] -- Why can't simp do this?
simp [hf]

/-- Variant of `foldl_subtype` with side condition to check `stop = l.size`. -/
@[simp] theorem foldl_subtype' {p : α → Prop} {l : Array { x // p x }}
{f : β → { x // p x } → β} {g : β → α → β} {x : β}
{hf : ∀ b x h, f b ⟨x, h⟩ = g b x} (h : stop = l.size) :
l.foldl f x 0 stop = l.unattach.foldl g x := by
subst h
rwa [foldl_subtype]

/--
This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
theorem foldr_subtype {p : α → Prop} {l : Array { x // p x }}
{f : { x // p x } → β → β} {g : α → β → β} {x : β}
{hf : ∀ x h b, f ⟨x, h⟩ b = g x b} :
l.foldr f x = l.unattach.foldr g x := by
cases l
simp only [List.foldr_toArray', List.unattach_toArray]
rw [List.foldr_subtype]
simp [hf]

/-- Variant of `foldr_subtype` with side condition to check `stop = l.size`. -/
@[simp] theorem foldr_subtype' {p : α → Prop} {l : Array { x // p x }}
{f : { x // p x } → β → β} {g : α → β → β} {x : β}
{hf : ∀ x h b, f ⟨x, h⟩ b = g x b} (h : start = l.size) :
l.foldr f x start 0 = l.unattach.foldr g x := by
subst h
rwa [foldr_subtype]

/--
This lemma identifies maps over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem map_subtype {p : α → Prop} {l : Array { x // p x }}
{f : { x // p x } → β} {g : α → β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
l.map f = l.unattach.map g := by
cases l
simp only [List.map_toArray, List.unattach_toArray]
rw [List.map_subtype]
simp [hf]

@[simp] theorem filterMap_subtype {p : α → Prop} {l : Array { x // p x }}
{f : { x // p x } → Option β} {g : α → Option β} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
l.filterMap f = l.unattach.filterMap g := by
cases l
simp only [size_toArray, List.filterMap_toArray', List.unattach_toArray, List.length_unattach,
mk.injEq]
rw [List.filterMap_subtype]
simp [hf]

@[simp] theorem unattach_filter {p : α → Prop} {l : Array { x // p x }}
{f : { x // p x } → Bool} {g : α → Bool} {hf : ∀ x h, f ⟨x, h⟩ = g x} :
(l.filter f).unattach = l.unattach.filter g := by
cases l
simp [hf]

/-! ### Simp lemmas pushing `unattach` inwards. -/

@[simp] theorem unattach_reverse {p : α → Prop} {l : Array { x // p x }} :
l.reverse.unattach = l.unattach.reverse := by
cases l
simp

@[simp] theorem unattach_append {p : α → Prop} {l₁ l₂ : Array { x // p x }} :
(l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach := by
cases l₁
cases l₂
simp

end Array
5 changes: 3 additions & 2 deletions src/Init/Data/Array/Basic.lean
Original file line number Diff line number Diff line change
@@ -11,6 +11,7 @@ import Init.Data.UInt.Basic
import Init.Data.Repr
import Init.Data.ToString.Basic
import Init.GetElem
import Init.Data.List.ToArray
universe u v w

/-! ### Array literal syntax -/
@@ -617,7 +618,7 @@ def concatMap (f : α → Array β) (as : Array α) : Array β :=
`flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`
-/
def flatten (as : Array (Array α)) : Array α :=
@[inline] def flatten (as : Array (Array α)) : Array α :=
as.foldl (init := empty) fun r a => r ++ a

@[inline]
@@ -720,7 +721,7 @@ termination_by a.size - i.val
decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt

-- This is required in `Lean.Data.PersistentHashMap`.
theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
@[simp] theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
induction a, i using Array.feraseIdx.induct with
| @case1 a i h a' _ ih =>
unfold feraseIdx
Loading

0 comments on commit dcedcad

Please sign in to comment.