Compare commits

..

1 Commits

Author SHA1 Message Date
Leonardo de Moura
f88263cdc9 fix: handle propositional and decidable instances in sym canonicalizer
This PR refactors instance canonicalization in the sym canonicalizer to
properly handle `Grind.nestedProof` and `Grind.nestedDecidable` markers.
Previously, the canonicalizer would report an issue when it failed to
resynthesize propositional instances that were provided by `grind`
itself or by the user via `haveI`. Now, resynthesis failure gracefully
falls back to the original instance in value positions, while remaining
strict inside types. This also removes the separate `cacheInsts` cache
in favor of the existing type/value caches via `withCaching`.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2026-04-04 00:21:28 +00:00
537 changed files with 561 additions and 5667 deletions

9
.vscode/tasks.json vendored
View File

@@ -11,15 +11,6 @@
"isDefault": true
}
},
{
"label": "build stage2",
"type": "shell",
"command": "make -C build/release stage2 -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
"problemMatcher": [],
"group": {
"kind": "build"
}
},
{
"label": "build-old",
"type": "shell",

View File

@@ -127,8 +127,7 @@ if(USE_MIMALLOC)
# Unnecessarily deep directory structure, but it saves us from a complicated
# stage0 update for now. If we ever update the other dependencies like
# cadical, it might be worth reorganizing the directory structure.
SOURCE_DIR
"${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
SOURCE_DIR "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
)
FetchContent_MakeAvailable(mimalloc)
endif()

View File

@@ -243,10 +243,6 @@ public theorem lt_iff_le_and_ne [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrd
a < b a b a b := by
simpa [le_iff_lt_or_eq, or_and_right] using Std.ne_of_lt
public theorem lt_trichotomy [LT α] [Std.Trichotomous (α := α) (· < ·)] (a b : α) :
a < b a = b b < a :=
Trichotomous.rel_or_eq_or_rel_swap
end LT
end Std

View File

@@ -1386,11 +1386,6 @@ theorem Slice.copy_eq_copy_sliceTo {s : Slice} {pos : s.Pos} :
rw [Nat.max_eq_right]
exact pos.offset_str_le_offset_endExclusive
@[simp]
theorem Slice.sliceTo_append_sliceFrom {s : Slice} {pos : s.Pos} :
(s.sliceTo pos).copy ++ (s.sliceFrom pos).copy = s.copy :=
copy_eq_copy_sliceTo.symm
/-- Given a slice `s` and a position on `s.copy`, obtain the corresponding position on `s`. -/
@[inline]
def Pos.ofCopy {s : Slice} (pos : s.copy.Pos) : s.Pos where
@@ -1750,31 +1745,6 @@ theorem Slice.Pos.offset_cast {s t : Slice} {pos : s.Pos} {h : s.copy = t.copy}
theorem Slice.Pos.cast_rfl {s : Slice} {pos : s.Pos} : pos.cast rfl = pos :=
Slice.Pos.ext (by simp)
@[simp]
theorem Slice.Pos.cast_cast {s t u : Slice} {hst : s.copy = t.copy} {htu : t.copy = u.copy}
{pos : s.Pos} : (pos.cast hst).cast htu = pos.cast (hst.trans htu) :=
Slice.Pos.ext (by simp)
@[simp]
theorem Slice.Pos.cast_inj {s t : Slice} {hst : s.copy = t.copy} {p q : s.Pos} : p.cast hst = q.cast hst p = q := by
simp [Slice.Pos.ext_iff]
@[simp]
theorem Slice.Pos.cast_startPos {s t : Slice} {hst : s.copy = t.copy} : s.startPos.cast hst = t.startPos :=
Slice.Pos.ext (by simp)
@[simp]
theorem Slice.Pos.cast_eq_startPos {s t : Slice} {p : s.Pos} {hst : s.copy = t.copy} : p.cast hst = t.startPos p = s.startPos := by
rw [ cast_startPos (hst := hst), Pos.cast_inj]
@[simp]
theorem Slice.Pos.cast_endPos {s t : Slice} {hst : s.copy = t.copy} : s.endPos.cast hst = t.endPos :=
Slice.Pos.ext (by simp [ rawEndPos_copy, hst])
@[simp]
theorem Slice.Pos.cast_eq_endPos {s t : Slice} {p : s.Pos} {hst : s.copy = t.copy} : p.cast hst = t.endPos p = s.endPos := by
rw [ cast_endPos (hst := hst), Pos.cast_inj]
@[simp]
theorem Slice.Pos.cast_le_cast_iff {s t : Slice} {pos pos' : s.Pos} {h : s.copy = t.copy} :
pos.cast h pos'.cast h pos pos' := by
@@ -1785,22 +1755,6 @@ theorem Slice.Pos.cast_lt_cast_iff {s t : Slice} {pos pos' : s.Pos} {h : s.copy
pos.cast h < pos'.cast h pos < pos' := by
simp [Slice.Pos.lt_iff]
theorem Slice.Pos.cast_le_iff {s t : Slice} {pos : s.Pos} {pos' : t.Pos} {h : s.copy = t.copy} :
pos.cast h pos' pos pos'.cast h.symm := by
simp [Slice.Pos.le_iff]
theorem Slice.Pos.le_cast_iff {s t : Slice} {pos : t.Pos} {pos' : s.Pos} {h : s.copy = t.copy} :
pos pos'.cast h pos.cast h.symm pos' := by
simp [Slice.Pos.le_iff]
theorem Slice.Pos.cast_lt_iff {s t : Slice} {pos : s.Pos} {pos' : t.Pos} {h : s.copy = t.copy} :
pos.cast h < pos' pos < pos'.cast h.symm := by
simp [Slice.Pos.lt_iff]
theorem Slice.Pos.lt_cast_iff {s t : Slice} {pos : t.Pos} {pos' : s.Pos} {h : s.copy = t.copy} :
pos < pos'.cast h pos.cast h.symm < pos' := by
simp [Slice.Pos.lt_iff]
/-- Constructs a valid position on `t` from a valid position on `s` and a proof that `s = t`. -/
@[inline]
def Pos.cast {s t : String} (pos : s.Pos) (h : s = t) : t.Pos where
@@ -1815,31 +1769,6 @@ theorem Pos.offset_cast {s t : String} {pos : s.Pos} {h : s = t} :
theorem Pos.cast_rfl {s : String} {pos : s.Pos} : pos.cast rfl = pos :=
Pos.ext (by simp)
@[simp]
theorem Pos.cast_cast {s t u : String} {hst : s = t} {htu : t = u}
{pos : s.Pos} : (pos.cast hst).cast htu = pos.cast (hst.trans htu) :=
Pos.ext (by simp)
@[simp]
theorem Pos.cast_inj {s t : String} {hst : s = t} {p q : s.Pos} : p.cast hst = q.cast hst p = q := by
simp [Pos.ext_iff]
@[simp]
theorem Pos.cast_startPos {s t : String} {hst : s = t} : s.startPos.cast hst = t.startPos := by
subst hst; simp
@[simp]
theorem Pos.cast_eq_startPos {s t : String} {hst : s = t} {p : s.Pos} : p.cast hst = t.startPos p = s.startPos := by
rw [ Pos.cast_startPos (hst := hst), Pos.cast_inj]
@[simp]
theorem Pos.cast_endPos {s t : String} {hst : s = t} : s.endPos.cast hst = t.endPos := by
subst hst; simp
@[simp]
theorem Pos.cast_eq_endPos {s t : String} {hst : s = t} {p : s.Pos} : p.cast hst = t.endPos p = s.endPos := by
rw [ Pos.cast_endPos (hst := hst), Pos.cast_inj]
@[simp]
theorem Pos.cast_le_cast_iff {s t : String} {pos pos' : s.Pos} {h : s = t} :
pos.cast h pos'.cast h pos pos' := by
@@ -1850,22 +1779,6 @@ theorem Pos.cast_lt_cast_iff {s t : String} {pos pos' : s.Pos} {h : s = t} :
pos.cast h < pos'.cast h pos < pos' := by
cases h; simp
theorem Pos.cast_le_iff {s t : String} {pos : s.Pos} {pos' : t.Pos} {h : s = t} :
pos.cast h pos' pos pos'.cast h.symm := by
simp [Pos.le_iff]
theorem Pos.le_cast_iff {s t : String} {pos : t.Pos} {pos' : s.Pos} {h : s = t} :
pos pos'.cast h pos.cast h.symm pos' := by
simp [Pos.le_iff]
theorem Pos.cast_lt_iff {s t : String} {pos : s.Pos} {pos' : t.Pos} {h : s = t} :
pos.cast h < pos' pos < pos'.cast h.symm := by
simp [Pos.lt_iff]
theorem Pos.lt_cast_iff {s t : String} {pos : t.Pos} {pos' : s.Pos} {h : s = t} :
pos < pos'.cast h pos.cast h.symm < pos' := by
simp [Pos.lt_iff]
theorem Pos.copy_toSlice_eq_cast {s : String} (p : s.Pos) :
p.toSlice.copy = p.cast copy_toSlice.symm :=
Pos.ext (by simp)
@@ -2141,10 +2054,6 @@ theorem Pos.le_ofToSlice_iff {s : String} {p : s.Pos} {q : s.toSlice.Pos} :
theorem Pos.toSlice_lt_toSlice_iff {s : String} {p q : s.Pos} :
p.toSlice < q.toSlice p < q := Iff.rfl
@[simp]
theorem Pos.toSlice_le_toSlice_iff {s : String} {p q : s.Pos} :
p.toSlice q.toSlice p q := Iff.rfl
theorem Pos.next_le_of_lt {s : String} {p q : s.Pos} {h} : p < q p.next h q := by
rw [next, Pos.ofToSlice_le_iff, Pos.toSlice_lt_toSlice_iff]
exact Slice.Pos.next_le_of_lt

View File

@@ -22,10 +22,6 @@ public section
namespace String
@[simp]
theorem singleton_inj {c d : Char} : singleton c = singleton d c = d := by
simp [ toList_inj]
@[simp]
theorem singleton_append_inj : singleton c ++ s = singleton d ++ t c = d s = t := by
simp [ toList_inj]
@@ -195,74 +191,18 @@ theorem sliceTo_slice {s : String} {p₁ p₂ h p} :
theorem Slice.sliceFrom_startPos {s : Slice} : s.sliceFrom s.startPos = s := by
ext <;> simp
@[simp]
theorem Slice.sliceFrom_eq_self_iff {s : Slice} {p : s.Pos} : s.sliceFrom p = s p = s.startPos := by
refine ?_, by rintro rfl; simp
rcases s with str, startInclusive, endExclusive, h
simp [sliceFrom, Slice.startPos, String.Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.ext_iff]
@[simp]
theorem Slice.sliceTo_endPos {s : Slice} : s.sliceTo s.endPos = s := by
ext <;> simp
@[simp]
theorem Slice.sliceTo_eq_self_iff {s : Slice} {p : s.Pos} : s.sliceTo p = s p = s.endPos := by
refine ?_, by rintro rfl; simp
rcases s with str, startInclusive, endExclusive, h
simp [sliceTo, Slice.endPos, String.Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.ext_iff,
utf8ByteSize_eq]
omega
@[simp]
theorem Slice.slice_startPos {s : Slice} {p : s.Pos} :
s.slice s.startPos p (Pos.startPos_le _) = s.sliceTo p := by
ext <;> simp
@[simp]
theorem Slice.slice_eq_self_iff {s : Slice} {p₁ p₂ : s.Pos} {h} :
s.slice p₁ p₂ h = s p₁ = s.startPos p₂ = s.endPos := by
refine ?_, by rintro rfl, rfl; simp
rcases s with str, startInclusive, endExclusive, h
simp [slice, Slice.endPos, String.Pos.ext_iff, Pos.Raw.ext_iff, Slice.Pos.ext_iff,
utf8ByteSize_eq]
omega
@[simp]
theorem Slice.slice_endPos {s : Slice} {p : s.Pos} :
s.slice p s.endPos (Pos.le_endPos _) = s.sliceFrom p := by
ext <;> simp
@[simp]
theorem sliceFrom_startPos {s : String} : s.sliceFrom s.startPos = s := by
ext <;> simp
@[simp]
theorem sliceFrom_eq_toSlice_iff {s : String} {p : s.Pos} : s.sliceFrom p = s.toSlice p = s.startPos := by
simp [ sliceFrom_toSlice]
@[simp]
theorem sliceTo_endPos {s : String} : s.sliceTo s.endPos = s := by
ext <;> simp
@[simp]
theorem sliceTo_eq_toSlice_iff {s : String} {p : s.Pos} : s.sliceTo p = s.toSlice p = s.endPos := by
simp [ sliceTo_toSlice]
@[simp]
theorem slice_startPos {s : String} {p : s.Pos} :
s.slice s.startPos p (Pos.startPos_le _) = s.sliceTo p := by
ext <;> simp
@[simp]
theorem slice_endPos {s : String} {p : s.Pos} :
s.slice p s.endPos (Pos.le_endPos _) = s.sliceFrom p := by
ext <;> simp
@[simp]
theorem slice_eq_toSlice_iff {s : String} {p₁ p₂ : s.Pos} {h} :
s.slice p₁ p₂ h = s.toSlice p₁ = s.startPos p₂ = s.endPos := by
simp [ slice_toSlice]
end Iterate
theorem Slice.copy_eq_copy_slice {s : Slice} {pos₁ pos₂ : s.Pos} {h} :
@@ -352,39 +292,4 @@ theorem nextn_endPos {s : String} : s.endPos.nextn n = s.endPos := by
end Pos
@[simp]
theorem Slice.Pos.cast_toSlice_copy {s : Slice} {pos : s.Pos} :
pos.copy.toSlice.cast (by simp) = pos := by
ext; simp
@[simp]
theorem Slice.Pos.sliceFrom_eq_startPos {s : Slice} {p : s.Pos} :
(Pos.sliceFrom p p (Pos.le_refl _)) = Slice.startPos _ := by
simp [ Pos.ofSliceFrom_inj]
@[simp]
theorem Slice.Pos.sliceFrom_endPos {s : Slice} {p : s.Pos} :
(Pos.sliceFrom p s.endPos (Pos.le_endPos _)) = Slice.endPos _ := by
simp [ Pos.ofSliceFrom_inj]
@[simp]
theorem Slice.Pos.sliceTo_startPos {s : Slice} {p : s.Pos} :
(Pos.sliceTo p s.startPos (Pos.startPos_le _)) = Slice.startPos _ := by
simp [ Pos.ofSliceTo_inj]
@[simp]
theorem Slice.Pos.sliceTo_eq_endPos {s : Slice} {p : s.Pos} :
(Pos.sliceTo p p (Pos.le_refl _)) = Slice.endPos _ := by
simp [ Pos.ofSliceTo_inj]
@[simp]
theorem Slice.Pos.slice_eq_startPos {s : Slice} {p₀ p₁ : s.Pos} {h} :
(Pos.slice p₀ p₀ p₁ (Pos.le_refl _) h) = Slice.startPos _ := by
simp [ Pos.ofSlice_inj]
@[simp]
theorem Slice.Pos.slice_eq_endPos {s : Slice} {p₀ p₁ : s.Pos} {h} :
(Pos.slice p₁ p₀ p₁ h (Pos.le_refl _)) = Slice.endPos _ := by
simp [ Pos.ofSlice_inj]
end String

View File

@@ -77,15 +77,6 @@ theorem join_cons : join (s :: l) = s ++ join l := by
theorem toList_join {l : List String} : (String.join l).toList = l.flatMap String.toList := by
induction l <;> simp_all
@[simp]
theorem join_append {l m : List String} : String.join (l ++ m) = String.join l ++ String.join m := by
simp [ toList_inj]
@[simp]
theorem length_join {l : List String} : (String.join l).length = (l.map String.length).sum := by
simp only [ length_toList, toList_join, List.length_flatMap]
simp
namespace Slice
@[simp]

View File

@@ -368,41 +368,21 @@ theorem Slice.Pos.ofSliceTo_ne_endPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo
refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₀))
simpa [ lt_endPos_iff, ofSliceTo_lt_ofSliceTo_iff] using h
theorem Slice.Pos.ne_endPos_of_sliceTo_ne_endPos {s : Slice} {p p₀ : s.Pos} {h₀}
(h : Pos.sliceTo p₀ p h₀ Slice.endPos _) : p s.endPos := by
rw [ Pos.ofSliceTo_sliceTo (h := h₀)]
apply Pos.ofSliceTo_ne_endPos h
theorem Slice.Pos.ofSliceFrom_ne_startPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos}
(h : p (s.sliceFrom p₀).startPos) : Pos.ofSliceFrom p s.startPos := by
refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
simpa [ startPos_lt_iff, ofSliceFrom_lt_ofSliceFrom_iff] using h
theorem Slice.Pos.ne_startPos_of_sliceFrom_ne_startPos {s : Slice} {p p₀ : s.Pos} {h₀}
(h : Pos.sliceFrom p₀ p h₀ Slice.startPos _) : p s.startPos := by
rw [ Pos.ofSliceFrom_sliceFrom (h := h₀)]
apply Pos.ofSliceFrom_ne_startPos h
theorem Pos.ofSliceTo_ne_endPos {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos}
(h : p (s.sliceTo p₀).endPos) : Pos.ofSliceTo p s.endPos := by
refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₀))
simpa [ Slice.Pos.lt_endPos_iff, ofSliceTo_lt_ofSliceTo_iff] using h
theorem Pos.ne_endPos_of_sliceTo_ne_endPos {s : String} {p p₀ : s.Pos} {h₀}
(h : Pos.sliceTo p₀ p h₀ Slice.endPos _) : p s.endPos := by
rw [ Pos.ofSliceTo_sliceTo (h := h₀)]
apply Pos.ofSliceTo_ne_endPos h
theorem Pos.ofSliceFrom_ne_startPos {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos}
(h : p (s.sliceFrom p₀).startPos) : Pos.ofSliceFrom p s.startPos := by
refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
simpa [ Slice.Pos.startPos_lt_iff, ofSliceFrom_lt_ofSliceFrom_iff] using h
theorem Pos.ne_startPos_of_sliceFrom_ne_startPos {s : String} {p p₀ : s.Pos} {h₀}
(h : Pos.sliceFrom p₀ p h₀ Slice.startPos _) : p s.startPos := by
rw [ Pos.ofSliceFrom_sliceFrom (h := h₀)]
apply Pos.ofSliceFrom_ne_startPos h
theorem Slice.Pos.ofSliceTo_next {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h} :
Pos.ofSliceTo (p.next h) = (Pos.ofSliceTo p).next (ofSliceTo_ne_endPos h) := by
rw [eq_comm, Pos.next_eq_iff]
@@ -534,41 +514,21 @@ theorem Slice.Pos.ofSlice_ne_endPos {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.
refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₁))
simpa [ lt_endPos_iff, ofSlice_lt_ofSlice_iff] using h
theorem Slice.Pos.ne_endPos_of_slice_ne_endPos {s : Slice} {p p₀ p₁ : s.Pos} {h₁ h₂}
(h : Pos.slice p p₀ p₁ h₁ h₂ Slice.endPos _) : p s.endPos := by
rw [ Pos.ofSlice_slice (h₁ := h₁) (h₂ := h₂)]
apply Pos.ofSlice_ne_endPos h
theorem Slice.Pos.ofSlice_ne_startPos {s : Slice} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
(h : p (s.slice p₀ p₁ h).startPos) : Pos.ofSlice p s.startPos := by
refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
simpa [ startPos_lt_iff, ofSlice_lt_ofSlice_iff] using h
theorem Slice.Pos.ne_startPos_of_slice_ne_startPos {s : Slice} {p p₀ p₁ : s.Pos} {h₁ h₂}
(h : Pos.slice p p₀ p₁ h₁ h₂ Slice.startPos _) : p s.startPos := by
rw [ Pos.ofSlice_slice (h₁ := h₁) (h₂ := h₂)]
apply Pos.ofSlice_ne_startPos h
theorem Pos.ofSlice_ne_endPos {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
(h : p (s.slice p₀ p₁ h).endPos) : Pos.ofSlice p s.endPos := by
refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₁))
simpa [ Slice.Pos.lt_endPos_iff, ofSlice_lt_ofSlice_iff] using h
theorem Pos.ne_endPos_of_slice_ne_endPos {s : String} {p p₀ p₁ : s.Pos} {h₁ h₂}
(h : Pos.slice p p₀ p₁ h₁ h₂ Slice.endPos _) : p s.endPos := by
rw [ Pos.ofSlice_slice (h₁ := h₁) (h₂ := h₂)]
apply Pos.ofSlice_ne_endPos h
theorem Pos.ofSlice_ne_startPos {s : String} {p₀ p₁ : s.Pos} {h} {p : (s.slice p₀ p₁ h).Pos}
(h : p (s.slice p₀ p₁ h).startPos) : Pos.ofSlice p s.startPos := by
refine (startPos_lt_iff _).1 (Std.lt_of_le_of_lt (startPos_le p₀) ?_)
simpa [ Slice.Pos.startPos_lt_iff, ofSlice_lt_ofSlice_iff] using h
theorem Pos.ne_startPos_of_slice_ne_startPos {s : String} {p p₀ p₁ : s.Pos} {h₁ h₂}
(h : Pos.slice p p₀ p₁ h₁ h₂ Slice.startPos _) : p s.startPos := by
rw [ Pos.ofSlice_slice (h₁ := h₁) (h₂ := h₂)]
apply Pos.ofSlice_ne_startPos h
@[simp]
theorem Slice.Pos.offset_le_rawEndPos {s : Slice} {p : s.Pos} :
p.offset s.rawEndPos :=
@@ -621,37 +581,21 @@ theorem Slice.Pos.get_eq_get_ofSliceTo {s : Slice} {p₀ : s.Pos} {pos : (s.slic
pos.get h = (ofSliceTo pos).get (ofSliceTo_ne_endPos h) := by
simp [Slice.Pos.get]
theorem Slice.Pos.get_sliceTo {s : Slice} {p₀ p : s.Pos} {h h'} :
(Pos.sliceTo p₀ p h).get h' = p.get (ne_endPos_of_sliceTo_ne_endPos h') := by
simp [get_eq_get_ofSliceTo]
theorem Pos.get_eq_get_ofSliceTo {s : String} {p₀ : s.Pos}
{pos : (s.sliceTo p₀).Pos} {h} :
pos.get h = (ofSliceTo pos).get (ofSliceTo_ne_endPos h) := by
simp [Pos.get, Slice.Pos.get]
theorem Pos.get_sliceTo {s : String} {p₀ p : s.Pos} {h h'} :
(Pos.sliceTo p₀ p h).get h' = p.get (ne_endPos_of_sliceTo_ne_endPos h') := by
simp [get_eq_get_ofSliceTo]
theorem Slice.Pos.get_eq_get_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h}
{pos : (s.slice p₀ p₁ h).Pos} {h'} :
pos.get h' = (ofSlice pos).get (ofSlice_ne_endPos h') := by
simp [Slice.Pos.get, Nat.add_assoc]
theorem Slice.Pos.get_slice {s : Slice} {p p₀ p₁ : s.Pos} {h₁ h₂ h} :
(Pos.slice p p₀ p₁ h₁ h₂).get h = p.get (ne_endPos_of_slice_ne_endPos h) := by
simp [get_eq_get_ofSlice]
theorem Pos.get_eq_get_ofSlice {s : String} {p₀ p₁ : s.Pos} {h}
{pos : (s.slice p₀ p₁ h).Pos} {h'} :
pos.get h' = (ofSlice pos).get (ofSlice_ne_endPos h') := by
simp [Pos.get, Slice.Pos.get]
theorem Pos.get_slice {s : String} {p p₀ p₁ : s.Pos} {h₁ h₂ h} :
(Pos.slice p p₀ p₁ h₁ h₂).get h = p.get (ne_endPos_of_slice_ne_endPos h) := by
simp [get_eq_get_ofSlice]
theorem Slice.Pos.ofSlice_next {s : Slice} {p₀ p₁ : s.Pos} {h}
{p : (s.slice p₀ p₁ h).Pos} {h'} :
Pos.ofSlice (p.next h') = (Pos.ofSlice p).next (ofSlice_ne_endPos h') := by

View File

@@ -12,7 +12,7 @@ public import Init.Data.Iterators.Consumers.Collect
import all Init.Data.String.Pattern.Basic
import Init.Data.String.OrderInstances
import Init.Data.String.Lemmas.IsEmpty
public import Init.Data.String.Lemmas.Basic
import Init.Data.String.Lemmas.Basic
import Init.Data.String.Lemmas.Order
import Init.Data.String.Termination
import Init.Data.Order.Lemmas
@@ -52,23 +52,19 @@ The corresponding compatibility typeclasses are
{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.Model.LawfulForwardPatternModel`
and
{name (scope := "Init.Data.String.Lemmas.Pattern.Basic")}`String.Slice.Pattern.Model.LawfulToForwardSearcherModel`.
We include the condition that the empty string is not a match. This is necessary for the theory to
work out as there is just no reasonable notion of searching that works for the empty string that is
still specific enough to yield reasonably strong correctness results for operations based on
searching.
This means that pattern types that allow searching for the empty string will have to special-case
the empty string in their correctness statements.
-/
class PatternModel {ρ : Type} (pat : ρ) : Type where
/-- The predicate that says which strings match the pattern. -/
Matches : String Prop
/--
Type class for the condition that the empty string is not a match. This is necessary for the theory to
work out as there is just no reasonable notion of searching that works for the empty string that is
still specific enough to yield reasonably strong correctness results for operations based on
searching.
-/
class StrictPatternModel {ρ : Type} (pat : ρ) [PatternModel pat] : Prop where
not_matches_empty : ¬ PatternModel.Matches pat ""
theorem not_matches_empty {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] :
¬ PatternModel.Matches pat "" :=
StrictPatternModel.not_matches_empty
not_matches_empty : ¬ Matches ""
/--
Predicate stating that the region between the start of the slice {name}`s` and the position
@@ -78,10 +74,10 @@ Predicate stating that the region between the start of the slice {name}`s` and t
structure IsMatch (pat : ρ) [PatternModel pat] {s : Slice} (endPos : s.Pos) : Prop where
matches_copy : PatternModel.Matches pat (s.sliceTo endPos).copy
theorem IsMatch.ne_startPos {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {pos : s.Pos}
theorem IsMatch.ne_startPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
(h : IsMatch pat pos) : pos s.startPos := by
intro hc
apply not_matches_empty (pat := pat)
apply PatternModel.not_matches_empty (pat := pat)
simpa [hc] using h.matches_copy
theorem isMatch_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
@@ -94,21 +90,6 @@ theorem isMatch_iff_exists_splits {pat : ρ} [PatternModel pat] {s : Slice} {pos
refine fun h => _, _, pos.splits, h, fun t₁, t₂, h₁, h₂ => ?_
rwa [h₁.eq_left pos.splits] at h₂
@[simp]
theorem isMatch_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice} (h : s.copy = t.copy) {pos : s.Pos} :
IsMatch pat (pos.cast h) IsMatch pat pos := by
simp [isMatch_iff]
@[simp]
theorem isMatch_sliceTo_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos p : s.Pos} {h} :
IsMatch pat (Pos.sliceTo p pos h) IsMatch pat pos := by
simp [isMatch_iff]
@[simp]
theorem isMatch_ofSliceTo_iff {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {pos : (s.sliceTo p).Pos} :
IsMatch pat (Pos.ofSliceTo pos) IsMatch pat pos := by
rw [ isMatch_sliceTo_iff (p := p) (h := Pos.ofSliceTo_le), Pos.sliceTo_ofSliceTo]
/--
Predicate stating that the region between the position {name}`startPos` and the end of the slice
{name}`s` matches the pattern {name}`pat`. Note that there might be a longer match.
@@ -116,10 +97,10 @@ Predicate stating that the region between the position {name}`startPos` and the
structure IsRevMatch (pat : ρ) [PatternModel pat] {s : Slice} (startPos : s.Pos) : Prop where
matches_copy : PatternModel.Matches pat (s.sliceFrom startPos).copy
theorem IsRevMatch.ne_endPos {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {pos : s.Pos}
theorem IsRevMatch.ne_endPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
(h : IsRevMatch pat pos) : pos s.endPos := by
intro hc
apply not_matches_empty (pat := pat)
apply PatternModel.not_matches_empty (pat := pat)
simpa [hc] using h.matches_copy
theorem isRevMatch_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
@@ -132,21 +113,6 @@ theorem isRevMatch_iff_exists_splits {pat : ρ} [PatternModel pat] {s : Slice} {
refine fun h => _, _, pos.splits, h, fun t₁, t₂, h₁, h₂ => ?_
rwa [h₁.eq_right pos.splits] at h₂
@[simp]
theorem isRevMatch_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice} (h : s.copy = t.copy) {pos : s.Pos} :
IsRevMatch pat (pos.cast h) IsRevMatch pat pos := by
simp [isRevMatch_iff]
@[simp]
theorem isRevMatch_sliceFrom_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos p : s.Pos} {h} :
IsRevMatch pat (Pos.sliceFrom p pos h) IsRevMatch pat pos := by
simp [isRevMatch_iff]
@[simp]
theorem isRevMatch_ofSliceFrom_iff {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {pos : (s.sliceFrom p).Pos} :
IsRevMatch pat (Pos.ofSliceFrom pos) IsRevMatch pat pos := by
rw [ isRevMatch_sliceFrom_iff (p := p) (h := Pos.le_ofSliceFrom), Pos.sliceFrom_ofSliceFrom]
/--
Predicate stating that the region between the start of the slice {name}`s` and the position
{name}`pos` matches the pattern {name}`pat`, and that there is no longer match starting at the
@@ -159,19 +125,10 @@ structure IsLongestMatch (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.Pos)
isMatch : IsMatch pat pos
not_isMatch : pos', pos < pos' ¬ IsMatch pat pos'
theorem isLongestMatch_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
IsLongestMatch pat pos IsMatch pat pos pos', pos < pos' ¬ IsMatch pat pos' :=
fun h, h' => h, h', fun h, h' => h, h'
theorem IsLongestMatch.ne_startPos {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {pos : s.Pos}
theorem IsLongestMatch.ne_startPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
(h : IsLongestMatch pat pos) : pos s.startPos :=
h.isMatch.ne_startPos
@[simp]
theorem not_isLongestMatch_startPos {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} :
¬IsLongestMatch pat s.startPos :=
fun h => h.ne_startPos rfl
theorem IsLongestMatch.eq {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos}
(h : IsLongestMatch pat pos) (h' : IsLongestMatch pat pos') : pos = pos' := by
apply Std.le_antisymm
@@ -192,34 +149,6 @@ theorem IsLongestMatch.le_of_isMatch {pat : ρ} [PatternModel pat] {s : Slice} {
(h : IsLongestMatch pat pos) (h' : IsMatch pat pos') : pos' pos :=
Std.not_lt.1 (fun hlt => h.not_isMatch _ hlt h')
@[simp]
theorem isLongestMatch_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice}
(hst : s.copy = t.copy) {pos : s.Pos} :
IsLongestMatch pat (pos.cast hst) IsLongestMatch pat pos := by
simp only [isLongestMatch_iff, isMatch_cast_iff, and_congr_right_iff]
refine fun _ => fun h p hp => ?_, fun h p hp => ?_
· rw [ isMatch_cast_iff hst]
exact h _ (by simpa)
· have : p = (p.cast hst.symm).cast hst := by simp
rw [this, isMatch_cast_iff hst]
exact h _ (by rwa [this, Pos.cast_lt_cast_iff] at hp)
theorem IsLongestMatch.of_eq {pat : ρ} [PatternModel pat] {s t : Slice} {pos : s.Pos} {pos' : t.Pos}
(h : IsLongestMatch pat pos) (h₁ : s.copy = t.copy) (h₂ : pos.cast h₁ = pos') :
IsLongestMatch pat pos' := by
subst h₂; simpa
theorem IsLongestMatch.sliceTo {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
(h : IsLongestMatch pat pos) (p : s.Pos) (hp : pos p) : IsLongestMatch pat (Pos.sliceTo p pos hp) := by
simp [isLongestMatch_iff] at h
refine h.1, fun p hp => ?_
rw [ isMatch_ofSliceTo_iff]
exact h.2 _ (by simpa [Pos.sliceTo_lt_iff] using hp)
theorem isLongestMatch_of_ofSliceTo {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {pos : (s.sliceTo p).Pos}
(h : IsLongestMatch pat (Pos.ofSliceTo pos)) : IsLongestMatch pat pos := by
simpa using h.sliceTo p
/--
Predicate stating that the region between the start of the slice {name}`s` and the position
{name}`pos` matches the pattern {name}`pat`, and that there is no longer match starting at the
@@ -232,19 +161,10 @@ structure IsLongestRevMatch (pat : ρ) [PatternModel pat] {s : Slice} (pos : s.P
isRevMatch : IsRevMatch pat pos
not_isRevMatch : pos', pos' < pos ¬ IsRevMatch pat pos'
theorem isLongestRevMatch_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos} :
IsLongestRevMatch pat pos IsRevMatch pat pos pos', pos' < pos ¬ IsRevMatch pat pos' :=
fun h, h' => h, h', fun h, h' => h, h'
theorem IsLongestRevMatch.ne_endPos {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {pos : s.Pos}
theorem IsLongestRevMatch.ne_endPos {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
(h : IsLongestRevMatch pat pos) : pos s.endPos :=
h.isRevMatch.ne_endPos
@[simp]
theorem not_isLongestRevMatch_endPos {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} :
¬IsLongestRevMatch pat s.endPos :=
fun h => h.ne_endPos rfl
theorem IsLongestRevMatch.eq {pat : ρ} [PatternModel pat] {s : Slice} {pos pos' : s.Pos}
(h : IsLongestRevMatch pat pos) (h' : IsLongestRevMatch pat pos') : pos = pos' := by
apply Std.le_antisymm
@@ -265,34 +185,6 @@ theorem IsLongestRevMatch.le_of_isRevMatch {pat : ρ} [PatternModel pat] {s : Sl
(h : IsLongestRevMatch pat pos) (h' : IsRevMatch pat pos') : pos pos' :=
Std.not_lt.1 (fun hlt => h.not_isRevMatch _ hlt h')
@[simp]
theorem isLongestRevMatch_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice}
(hst : s.copy = t.copy) {pos : s.Pos} :
IsLongestRevMatch pat (pos.cast hst) IsLongestRevMatch pat pos := by
simp only [isLongestRevMatch_iff, isRevMatch_cast_iff, and_congr_right_iff]
refine fun _ => fun h p hp => ?_, fun h p hp => ?_
· rw [ isRevMatch_cast_iff hst]
exact h _ (by simpa)
· have : p = (p.cast hst.symm).cast hst := by simp
rw [this, isRevMatch_cast_iff hst]
exact h _ (by rwa [this, Pos.cast_lt_cast_iff] at hp)
theorem IsLongestRevMatch.of_eq {pat : ρ} [PatternModel pat] {s t : Slice} {pos : s.Pos} {pos' : t.Pos}
(h : IsLongestRevMatch pat pos) (h₁ : s.copy = t.copy) (h₂ : pos.cast h₁ = pos') :
IsLongestRevMatch pat pos' := by
subst h₂; simpa
theorem IsLongestRevMatch.sliceFrom {pat : ρ} [PatternModel pat] {s : Slice} {pos : s.Pos}
(h : IsLongestRevMatch pat pos) (p : s.Pos) (hp : p pos) : IsLongestRevMatch pat (Pos.sliceFrom p pos hp) := by
simp [isLongestRevMatch_iff] at h
refine h.1, fun p' hp' => ?_
rw [ isRevMatch_ofSliceFrom_iff]
exact h.2 _ (by simpa [Pos.lt_sliceFrom_iff] using hp')
theorem isLongestRevMatch_of_ofSliceFrom {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {pos : (s.sliceFrom p).Pos}
(h : IsLongestRevMatch pat (Pos.ofSliceFrom pos)) : IsLongestRevMatch pat pos := by
simpa using h.sliceFrom p
/--
Predicate stating that a match for a given pattern is never a proper prefix of another match.
@@ -348,21 +240,12 @@ theorem isLongestMatchAt_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos₁ p
(h : pos₁ pos₂), IsLongestMatch pat (Slice.Pos.sliceFrom _ _ h) :=
fun h, h' => h, h', fun h, h' => h, h'
theorem IsLongestMatchAt.lt {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {startPos endPos : s.Pos}
theorem IsLongestMatchAt.lt {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestMatchAt pat startPos endPos) : startPos < endPos := by
have := h.isLongestMatch_sliceFrom.ne_startPos
rw [ Pos.startPos_lt_iff, Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff] at this
simpa
theorem IsLongestMatchAt.ne {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestMatchAt pat startPos endPos) : startPos endPos :=
Std.ne_of_lt h.lt
@[simp]
theorem not_isLongestMatchAt_self {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {startPos : s.Pos} :
¬IsLongestMatchAt pat startPos startPos :=
fun h => h.ne rfl
theorem IsLongestMatchAt.eq {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos endPos' : s.Pos}
(h : IsLongestMatchAt pat startPos endPos) (h' : IsLongestMatchAt pat startPos endPos') :
endPos = endPos' := by
@@ -399,77 +282,6 @@ theorem isLongestMatchAt_startPos_iff {pat : ρ} [PatternModel pat] {s : Slice}
fun h => isLongestMatch_of_eq (by simp) (by simp) h,
fun h => isLongestMatch_of_eq (by simp) (by simp) h
theorem isLongestMatch_iff_isLongestMatchAt_ofSliceFrom {pat : ρ} [PatternModel pat]
{s : Slice} {base : s.Pos} (endPos : (s.sliceFrom base).Pos) :
IsLongestMatch pat endPos IsLongestMatchAt pat base (Pos.ofSliceFrom endPos) := by
simp [ isLongestMatchAt_startPos_iff, isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom]
theorem IsLongestMatchAt.matches_slice {pat : ρ} [PatternModel pat] {s : Slice}
{startPos endPos : s.Pos} (h : IsLongestMatchAt pat startPos endPos) :
PatternModel.Matches pat (s.slice startPos endPos h.le).copy := by
simpa using h.isLongestMatch_sliceFrom.isMatch.matches_copy
@[simp]
theorem isLongestMatchAt_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy)
{startPos endPos : s.Pos} :
IsLongestMatchAt pat (startPos.cast hst) (endPos.cast hst) IsLongestMatchAt pat startPos endPos := by
simp [isLongestMatchAt_iff, Pos.sliceFrom_cast]
theorem IsLongestMatchAt.of_eq {pat : ρ} [PatternModel pat] {s t : Slice} {s₁ e₁ : s.Pos} {s₂ e₂ : t.Pos}
(h : IsLongestMatchAt pat s₁ e₁) (h₁ : s.copy = t.copy) (h₂ : s₁.cast h₁ = s₂) (h₃ : e₁.cast h₁ = e₂) :
IsLongestMatchAt pat s₂ e₂ := by
subst h₂ h₃; simpa
theorem IsLongestMatchAt.sliceTo {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestMatchAt pat startPos endPos) (p : s.Pos) (hp : endPos p) :
IsLongestMatchAt pat (Pos.sliceTo p startPos (by exact Std.le_trans h.le hp)) (Pos.sliceTo p endPos hp) := by
simp only [isLongestMatchAt_iff, Pos.sliceTo_le_sliceTo_iff] at h
obtain h, hp' := h
exact h, (hp'.sliceTo (Pos.sliceFrom startPos p (Std.le_trans h hp)) (by simpa)).of_eq (by simp) (by ext; simp)
theorem isLongestMatchAt_of_ofSliceTo {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {startPos endPos : (s.sliceTo p).Pos}
(h : IsLongestMatchAt pat (Pos.ofSliceTo startPos) (Pos.ofSliceTo endPos)) :
IsLongestMatchAt pat startPos endPos := by
simpa using h.sliceTo p Pos.ofSliceTo_le
/--
Predicate stating that the range between two positions of {name}`s` can be covered by longest
matches of the pattern within {name}`s`.
-/
inductive IsLongestMatchAtChain (pat : ρ) [PatternModel pat] {s : Slice} : s.Pos s.Pos Prop where
| nil (p : s.Pos) : IsLongestMatchAtChain pat p p
| cons (startPos middlePos endPos : s.Pos) : IsLongestMatchAt pat startPos middlePos
IsLongestMatchAtChain pat middlePos endPos IsLongestMatchAtChain pat startPos endPos
attribute [simp] IsLongestMatchAtChain.nil
theorem IsLongestMatchAtChain.eq_of_isLongestMatchAt_self {pat : ρ} [PatternModel pat] {s : Slice}
{startPos endPos : s.Pos} (h : IsLongestMatchAtChain pat startPos endPos) (h' : IsLongestMatchAt pat startPos startPos) :
startPos = endPos := by
induction h with
| nil => rfl
| cons p₁ p₂ p₃ h₁ h₂ ih =>
obtain rfl : p₁ = p₂ := h'.eq h₁
exact ih h₁
theorem IsLongestMatchAtChain.le {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestMatchAtChain pat startPos endPos) : startPos endPos := by
induction h with
| nil => exact Std.le_refl _
| cons p₁ p₂ p₃ h₁ h₂ ih => exact Std.le_trans h₁.le ih
theorem IsLongestMatchAtChain.sliceTo {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestMatchAtChain pat startPos endPos) (p : s.Pos) (hp : endPos p) :
IsLongestMatchAtChain pat (Pos.sliceTo p startPos (by exact Std.le_trans h.le hp)) (Pos.sliceTo p endPos hp) := by
induction h with
| nil => simp
| cons p₁ p₂ p₃ h₁ h₂ ih => exact .cons _ _ _ (h₁.sliceTo p (Std.le_trans h₂.le hp)) (ih hp)
theorem isLongestMatchAtChain_of_ofSliceTo {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos}
{startPos endPos : (s.sliceTo p).Pos} (h : IsLongestMatchAtChain pat (Pos.ofSliceTo startPos) (Pos.ofSliceTo endPos)) :
IsLongestMatchAtChain pat startPos endPos := by
simpa using h.sliceTo p Pos.ofSliceTo_le
/--
Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains is a match
of {name}`pat` in {name}`s` and it is longest among matches ending at {name}`endPos`.
@@ -483,21 +295,12 @@ theorem isLongestRevMatchAt_iff {pat : ρ} [PatternModel pat] {s : Slice} {pos
(h : pos₁ pos₂), IsLongestRevMatch pat (Slice.Pos.sliceTo _ _ h) :=
fun h, h' => h, h', fun h, h' => h, h'
theorem IsLongestRevMatchAt.lt {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {startPos endPos : s.Pos}
theorem IsLongestRevMatchAt.lt {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestRevMatchAt pat startPos endPos) : startPos < endPos := by
have := h.isLongestRevMatch_sliceTo.ne_endPos
rw [ Pos.lt_endPos_iff, Slice.Pos.ofSliceTo_lt_ofSliceTo_iff] at this
simpa
theorem IsLongestRevMatchAt.ne {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestRevMatchAt pat startPos endPos) : startPos endPos :=
Std.ne_of_lt h.lt
@[simp]
theorem not_isLongestRevMatchAt_self {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} {endPos : s.Pos} :
¬IsLongestRevMatchAt pat endPos endPos :=
fun h => h.ne rfl
theorem IsLongestRevMatchAt.eq {pat : ρ} [PatternModel pat] {s : Slice} {startPos startPos' endPos : s.Pos}
(h : IsLongestRevMatchAt pat startPos endPos) (h' : IsLongestRevMatchAt pat startPos' endPos) :
startPos = startPos' := by
@@ -532,77 +335,6 @@ theorem isLongestRevMatchAt_endPos_iff {pat : ρ} [PatternModel pat] {s : Slice}
fun h => isLongestRevMatch_of_eq (by simp) (by simp) h,
fun h => isLongestRevMatch_of_eq (by simp) (by simp) h
theorem isLongestRevMatch_iff_isLongestRevMatchAt_ofSliceTo {pat : ρ} [PatternModel pat]
{s : Slice} {base : s.Pos} (startPos : (s.sliceTo base).Pos) :
IsLongestRevMatch pat startPos IsLongestRevMatchAt pat (Pos.ofSliceTo startPos) base := by
simp [ isLongestRevMatchAt_endPos_iff, isLongestRevMatchAt_iff_isLongestRevMatchAt_ofSliceTo]
theorem IsLongestRevMatchAt.matches_slice {pat : ρ} [PatternModel pat] {s : Slice}
{startPos endPos : s.Pos} (h : IsLongestRevMatchAt pat startPos endPos) :
PatternModel.Matches pat (s.slice startPos endPos h.le).copy := by
simpa using h.isLongestRevMatch_sliceTo.isRevMatch.matches_copy
@[simp]
theorem isLongestRevMatchAt_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy)
{startPos endPos : s.Pos} :
IsLongestRevMatchAt pat (startPos.cast hst) (endPos.cast hst) IsLongestRevMatchAt pat startPos endPos := by
simp [isLongestRevMatchAt_iff, Pos.sliceTo_cast]
theorem IsLongestRevMatchAt.of_eq {pat : ρ} [PatternModel pat] {s t : Slice} {s₁ e₁ : s.Pos} {s₂ e₂ : t.Pos}
(h : IsLongestRevMatchAt pat s₁ e₁) (h₁ : s.copy = t.copy) (h₂ : s₁.cast h₁ = s₂) (h₃ : e₁.cast h₁ = e₂) :
IsLongestRevMatchAt pat s₂ e₂ := by
subst h₂ h₃; simpa
theorem IsLongestRevMatchAt.sliceFrom {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestRevMatchAt pat startPos endPos) (p : s.Pos) (hp : p startPos) :
IsLongestRevMatchAt pat (Pos.sliceFrom p startPos hp) (Pos.sliceFrom p endPos (by exact Std.le_trans hp h.le)) := by
simp only [isLongestRevMatchAt_iff, Pos.sliceFrom_le_sliceFrom_iff] at h
obtain h, hp' := h
exact h, (hp'.sliceFrom (Pos.sliceTo endPos p (Std.le_trans hp h)) (by simpa)).of_eq (by simp) (by ext; simp)
theorem isLongestRevMatchAt_of_ofSliceFrom {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos} {startPos endPos : (s.sliceFrom p).Pos}
(h : IsLongestRevMatchAt pat (Pos.ofSliceFrom startPos) (Pos.ofSliceFrom endPos)) :
IsLongestRevMatchAt pat startPos endPos := by
simpa using h.sliceFrom p Pos.le_ofSliceFrom
/--
Predicate stating that the range between two positions of {name}`s` can be covered by longest
reverse matches of the pattern within {name}`s`.
-/
inductive IsLongestRevMatchAtChain (pat : ρ) [PatternModel pat] {s : Slice} : s.Pos s.Pos Prop where
| nil (p : s.Pos) : IsLongestRevMatchAtChain pat p p
| cons (startPos middlePos endPos : s.Pos) : IsLongestRevMatchAtChain pat startPos middlePos
IsLongestRevMatchAt pat middlePos endPos IsLongestRevMatchAtChain pat startPos endPos
attribute [simp] IsLongestRevMatchAtChain.nil
theorem IsLongestRevMatchAtChain.eq_of_isLongestRevMatchAt_self {pat : ρ} [PatternModel pat] {s : Slice}
{startPos endPos : s.Pos} (h : IsLongestRevMatchAtChain pat startPos endPos) (h' : IsLongestRevMatchAt pat endPos endPos) :
startPos = endPos := by
induction h with
| nil => rfl
| cons mid endP hchain hmatch ih =>
obtain rfl := hmatch.eq h'
exact ih hmatch
theorem IsLongestRevMatchAtChain.le {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestRevMatchAtChain pat startPos endPos) : startPos endPos := by
induction h with
| nil => exact Std.le_refl _
| cons mid endP hchain hmatch ih => exact Std.le_trans ih hmatch.le
theorem IsLongestRevMatchAtChain.sliceFrom {pat : ρ} [PatternModel pat] {s : Slice} {startPos endPos : s.Pos}
(h : IsLongestRevMatchAtChain pat startPos endPos) (p : s.Pos) (hp : p startPos) :
IsLongestRevMatchAtChain pat (Pos.sliceFrom p startPos hp) (Pos.sliceFrom p endPos (by exact Std.le_trans hp h.le)) := by
induction h with
| nil => simp
| cons mid endP hchain hmatch ih => exact .cons _ _ _ ih (hmatch.sliceFrom p (Std.le_trans hp hchain.le))
theorem isLongestRevMatchAtChain_of_ofSliceFrom {pat : ρ} [PatternModel pat] {s : Slice} {p : s.Pos}
{startPos endPos : (s.sliceFrom p).Pos} (h : IsLongestRevMatchAtChain pat (Pos.ofSliceFrom startPos) (Pos.ofSliceFrom endPos)) :
IsLongestRevMatchAtChain pat startPos endPos := by
simpa using h.sliceFrom p Pos.le_ofSliceFrom
/--
Predicate stating that there is a (longest) match starting at the given position.
-/
@@ -628,7 +360,7 @@ theorem matchesAt_iff_exists_isMatch {pat : ρ} [PatternModel pat] {s : Slice}
by simpa using hq
@[simp]
theorem not_matchesAt_endPos {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} :
theorem not_matchesAt_endPos {pat : ρ} [PatternModel pat] {s : Slice} :
¬ MatchesAt pat s.endPos := by
simp only [matchesAt_iff_exists_isMatch, Pos.endPos_le, exists_prop_eq]
intro h
@@ -648,14 +380,6 @@ theorem IsLongestMatchAt.matchesAt {pat : ρ} [PatternModel pat] {s : Slice} {st
(h : IsLongestMatchAt pat startPos endPos) : MatchesAt pat startPos where
exists_isLongestMatchAt := _, h
@[simp]
theorem matchesAt_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy)
{pos : s.Pos} : MatchesAt pat (pos.cast hst) MatchesAt pat pos := by
simp only [matchesAt_iff_exists_isLongestMatchAt]
refine fun endPos, h => ?_, fun endPos, h => ?_
· exact endPos.cast hst.symm, by simpa [ isLongestMatchAt_cast_iff hst]
· exact endPos.cast hst, by simpa
/--
Predicate stating that there is a (longest) match ending at the given position.
-/
@@ -681,7 +405,7 @@ theorem revMatchesAt_iff_exists_isRevMatch {pat : ρ} [PatternModel pat] {s : Sl
by simpa using hq
@[simp]
theorem not_revMatchesAt_startPos {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice} :
theorem not_revMatchesAt_startPos {pat : ρ} [PatternModel pat] {s : Slice} :
¬ RevMatchesAt pat s.startPos := by
simp only [revMatchesAt_iff_exists_isRevMatch, Pos.le_startPos, exists_prop_eq]
intro h
@@ -701,14 +425,6 @@ theorem IsLongestRevMatchAt.revMatchesAt {pat : ρ} [PatternModel pat] {s : Slic
(h : IsLongestRevMatchAt pat startPos endPos) : RevMatchesAt pat endPos where
exists_isLongestRevMatchAt := _, h
@[simp]
theorem revMatchesAt_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy)
{pos : s.Pos} : RevMatchesAt pat (pos.cast hst) RevMatchesAt pat pos := by
simp only [revMatchesAt_iff_exists_isLongestRevMatchAt]
refine fun endPos, h => ?_, fun endPos, h => ?_
· exact endPos.cast hst.symm, by simpa [ isLongestRevMatchAt_cast_iff hst]
· exact endPos.cast hst, by simpa
open Classical in
/--
Noncomputable model function returning the end point of the longest match starting at the given
@@ -734,21 +450,6 @@ theorem matchAt?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat]
| case1 h => simpa using h
| case2 h => simpa using fun h' => h h'
theorem lt_of_matchAt?_eq_some {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat]
{s : Slice} {startPos endPos : s.Pos} (h : matchAt? pat startPos = some endPos) :
startPos < endPos :=
(matchAt?_eq_some_iff.1 h).lt
@[simp]
theorem matchAt?_cast {ρ : Type} (pat : ρ) [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy)
{startPos : s.Pos} :
matchAt? pat (startPos.cast hst) = (matchAt? pat startPos).map (Slice.Pos.cast · hst) := by
refine Option.ext (fun endPos => ?_)
have : endPos = (endPos.cast hst.symm).cast hst := by simp
conv => lhs; rw [this, matchAt?_eq_some_iff, isLongestMatchAt_cast_iff]
simp only [Option.map_eq_some_iff, matchAt?_eq_some_iff]
exact fun h => _, h, by simp, by rintro pos, h, rfl; simpa
open Classical in
/--
Noncomputable model function returning the start point of the longest match ending at the given
@@ -774,21 +475,6 @@ theorem revMatchAt?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat]
| case1 h => simpa using h
| case2 h => simpa using fun h' => h h'
theorem lt_of_revMatchAt?_eq_some {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat]
{s : Slice} {startPos endPos : s.Pos} (h : revMatchAt? pat endPos = some startPos) :
startPos < endPos :=
(revMatchAt?_eq_some_iff.1 h).lt
@[simp]
theorem revMatchAt?_cast {ρ : Type} (pat : ρ) [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy)
{startPos : s.Pos} :
revMatchAt? pat (startPos.cast hst) = (revMatchAt? pat startPos).map (Slice.Pos.cast · hst) := by
refine Option.ext (fun endPos => ?_)
have : endPos = (endPos.cast hst.symm).cast hst := by simp
conv => lhs; rw [this, revMatchAt?_eq_some_iff, isLongestRevMatchAt_cast_iff]
simp only [Option.map_eq_some_iff, revMatchAt?_eq_some_iff]
exact fun h => _, h, by simp, by rintro pos, h, rfl; simpa
/--
Predicate stating compatibility between {name}`PatternModel` and {name}`ForwardPattern`.
@@ -884,24 +570,6 @@ theorem IsValidSearchFrom.endPos_of_eq {pat : ρ} [PatternModel pat] {s : Slice}
cases hl
exact IsValidSearchFrom.endPos
theorem isValidSearchFrom_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy)
{pos : s.Pos} {l : List (SearchStep t)} :
IsValidSearchFrom pat (pos.cast hst) l IsValidSearchFrom pat pos (l.map (·.cast hst.symm)) := by
suffices (s t : Slice) (hst : s.copy = t.copy) (pos : s.Pos) (l : List (SearchStep s)),
IsValidSearchFrom pat pos l IsValidSearchFrom pat (pos.cast hst) (l.map (·.cast hst)) from
fun h => by simpa using this _ _ hst.symm _ _ h, fun h => by
have hcomp : (SearchStep.cast hst) (SearchStep.cast hst.symm) = id := by ext; simp
simpa [hcomp] using this _ _ hst _ _ h
intro s t hst pos l hl
induction hl with
| endPos => simpa using IsValidSearchFrom.endPos
| matched h₁ h₂ ih =>
simpa only [List.map_cons, SearchStep.cast_matched] using IsValidSearchFrom.matched (by simpa) ih
| mismatched h₁ h₂ h₃ ih =>
simp only [List.map_cons, SearchStep.cast_rejected]
refine IsValidSearchFrom.mismatched (by simpa) (fun p hp₁ hp₂ hp₃ => ?_) ih
exact h₂ (p.cast hst.symm) (by simpa [Pos.le_cast_iff]) (by simpa [Pos.cast_lt_iff]) (by simpa)
/--
Predicate stating compatibility between {name}`PatternModel` and {name}`ToForwardSearcher`.
@@ -995,24 +663,6 @@ theorem IsValidRevSearchFrom.startPos_of_eq {pat : ρ} [PatternModel pat] {s : S
cases hl
exact IsValidRevSearchFrom.startPos
theorem isValidRevSearchFrom_cast_iff {pat : ρ} [PatternModel pat] {s t : Slice} (hst : s.copy = t.copy)
{pos : s.Pos} {l : List (SearchStep t)} :
IsValidRevSearchFrom pat (pos.cast hst) l IsValidRevSearchFrom pat pos (l.map (·.cast hst.symm)) := by
suffices (s t : Slice) (hst : s.copy = t.copy) (pos : s.Pos) (l : List (SearchStep s)),
IsValidRevSearchFrom pat pos l IsValidRevSearchFrom pat (pos.cast hst) (l.map (·.cast hst)) from
fun h => by simpa using this _ _ hst.symm _ _ h, fun h => by
have hcomp : (SearchStep.cast hst) (SearchStep.cast hst.symm) = id := by ext; simp
simpa [hcomp] using this _ _ hst _ _ h
intro s t hst pos l hl
induction hl with
| startPos => simpa using IsValidRevSearchFrom.startPos
| matched h₁ h₂ ih =>
simpa only [List.map_cons, SearchStep.cast_matched] using IsValidRevSearchFrom.matched (by simpa) ih
| mismatched h₁ h₂ h₃ ih =>
simp only [List.map_cons, SearchStep.cast_rejected]
refine IsValidRevSearchFrom.mismatched (by simpa) (fun p hp₁ hp₂ hp₃ => ?_) ih
exact h₂ (p.cast hst.symm) (by simpa [Pos.lt_cast_iff]) (by simpa [Pos.cast_le_iff]) (by simpa)
/--
Predicate stating compatibility between {name}`PatternModel` and {name}`ToBackwardSearcher`.

View File

@@ -28,9 +28,7 @@ namespace String.Slice.Pattern.Model.Char
instance {c : Char} : PatternModel c where
Matches s := s = String.singleton c
instance {c : Char} : StrictPatternModel c where
not_matches_empty := by simp [PatternModel.Matches]
not_matches_empty := by simp
instance {c : Char} : NoPrefixPatternModel c :=
.of_length_eq (by simp +contextual [PatternModel.Matches])
@@ -170,61 +168,11 @@ theorem isLongestMatchAt_iff_isLongestMatchAt_beq {c : Char} {s : Slice}
IsLongestMatchAt c pos pos' IsLongestMatchAt (· == c) pos pos' := by
simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_beq]
theorem isLongestMatchAtChain_iff_isLongestMatchAtChain_beq {c : Char} {s : Slice} {pos pos' : s.Pos} :
IsLongestMatchAtChain c pos pos' IsLongestMatchAtChain (· == c) pos pos' := by
refine fun h => ?_, fun h => ?_
· induction h with
| nil => simp
| cons p₁ p₂ p₃ h₁ h₂ ih => exact .cons _ _ _ (isLongestMatchAt_iff_isLongestMatchAt_beq.1 h₁) ih
· induction h with
| nil => simp
| cons p₁ p₂ p₃ h₁ h₂ ih => exact .cons _ _ _ (isLongestMatchAt_iff_isLongestMatchAt_beq.2 h₁) ih
theorem isLongestMatchAtChain_iff {c : Char} {s : Slice} {pos pos' : s.Pos} :
IsLongestMatchAtChain c pos pos' pos pos' pos'', pos pos'' (h : pos'' < pos') pos''.get (Pos.ne_endPos_of_lt h) = c := by
simp [isLongestMatchAtChain_iff_isLongestMatchAtChain_beq, CharPred.isLongestMatchAtChain_iff]
theorem isLongestMatchAtChain_iff_toList {c : Char} {s : Slice} {pos pos' : s.Pos} :
IsLongestMatchAtChain c pos pos'
(h : pos pos'), (s.slice pos pos' h).copy.toList = List.replicate (s.slice pos pos' h).copy.length c := by
simp [isLongestMatchAtChain_iff_isLongestMatchAtChain_beq, CharPred.isLongestMatchAtChain_iff_toList,
List.eq_replicate_iff]
theorem isLongestMatchAtChain_startPos_endPos_iff_toList {c : Char} {s : Slice} :
IsLongestMatchAtChain c s.startPos s.endPos s.copy.toList = List.replicate s.copy.length c := by
simp [isLongestMatchAtChain_iff_isLongestMatchAtChain_beq,
CharPred.isLongestMatchAtChain_startPos_endPos_iff_toList, List.eq_replicate_iff]
theorem isLongestRevMatchAt_iff_isLongestRevMatchAt_beq {c : Char} {s : Slice}
{pos pos' : s.Pos} :
IsLongestRevMatchAt c pos pos' IsLongestRevMatchAt (· == c) pos pos' := by
simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff_isLongestRevMatch_beq]
theorem isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_beq {c : Char} {s : Slice} {pos pos' : s.Pos} :
IsLongestRevMatchAtChain c pos pos' IsLongestRevMatchAtChain (· == c) pos pos' := by
refine fun h => ?_, fun h => ?_
· induction h with
| nil => simp
| cons p₂ p₃ _ hmatch ih => exact .cons _ _ _ ih (isLongestRevMatchAt_iff_isLongestRevMatchAt_beq.1 hmatch)
· induction h with
| nil => simp
| cons p₂ p₃ _ hmatch ih => exact .cons _ _ _ ih (isLongestRevMatchAt_iff_isLongestRevMatchAt_beq.2 hmatch)
theorem isLongestRevMatchAtChain_iff {c : Char} {s : Slice} {pos pos' : s.Pos} :
IsLongestRevMatchAtChain c pos pos' pos pos' pos'', pos pos'' (h : pos'' < pos') pos''.get (Pos.ne_endPos_of_lt h) = c := by
simp [isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_beq, CharPred.isLongestRevMatchAtChain_iff]
theorem isLongestRevMatchAtChain_iff_toList {c : Char} {s : Slice} {pos pos' : s.Pos} :
IsLongestRevMatchAtChain c pos pos'
(h : pos pos'), (s.slice pos pos' h).copy.toList = List.replicate (s.slice pos pos' h).copy.length c := by
simp [isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_beq, CharPred.isLongestRevMatchAtChain_iff_toList,
List.eq_replicate_iff]
theorem isLongestRevMatchAtChain_startPos_endPos_iff_toList {c : Char} {s : Slice} :
IsLongestRevMatchAtChain c s.startPos s.endPos s.copy.toList = List.replicate s.copy.length c := by
simp [isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_beq,
CharPred.isLongestRevMatchAtChain_startPos_endPos_iff_toList, List.eq_replicate_iff]
theorem matchesAt_iff_matchesAt_beq {c : Char} {s : Slice} {pos : s.Pos} :
MatchesAt c pos MatchesAt (· == c) pos := by
simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_beq]
@@ -294,21 +242,18 @@ theorem skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} :
theorem Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} :
skipPrefix? c s = skipPrefix? (· == c) s := (rfl)
theorem Pos.skip?_char_eq_skip?_beq {c : Char} {s : Slice} {pos : s.Pos} :
pos.skip? c = pos.skip? (· == c) := (rfl)
theorem Pos.skipWhile_char_eq_skipWhile_beq {c : Char} {s : Slice} (curr : s.Pos) :
Pos.skipWhile curr c = Pos.skipWhile curr (· == c) := by
fun_induction Pos.skipWhile curr c with
| case1 pos nextCurr h₁ h₂ ih =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_char_eq_skip?_beq, h₁, h₂, ih]
simp [ Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h₁, h₂, ih]
| case2 pos nextCurr h ih =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_char_eq_skip?_beq, h, ih]
simp [ Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h, ih]
| case3 pos h =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_char_eq_skip?_beq, h]
simp [ Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq]
theorem skipPrefixWhile_char_eq_skipPrefixWhile_beq {c : Char} {s : Slice} :
s.skipPrefixWhile c = s.skipPrefixWhile (· == c) :=
@@ -324,7 +269,7 @@ theorem takeWhile_char_eq_takeWhile_beq {c : Char} {s : Slice} :
theorem all_char_eq_all_beq {c : Char} {s : Slice} :
s.all c = s.all (· == c) := by
simp only [all, skipPrefixWhile_char_eq_skipPrefixWhile_beq]
simp only [all, dropWhile_char_eq_dropWhile_beq]
theorem find?_char_eq_find?_beq {c : Char} {s : Slice} :
s.find? c = s.find? (· == c) :=
@@ -353,21 +298,18 @@ theorem dropSuffix_char_eq_dropSuffix_beq {c : Char} {s : Slice} :
theorem Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq {c : Char} {s : Slice} :
skipSuffix? c s = skipSuffix? (· == c) s := (rfl)
theorem Pos.revSkip?_char_eq_revSkip?_beq {c : Char} {s : Slice} {pos : s.Pos} :
pos.revSkip? c = pos.revSkip? (· == c) := (rfl)
theorem Pos.revSkipWhile_char_eq_revSkipWhile_beq {c : Char} {s : Slice} (curr : s.Pos) :
Pos.revSkipWhile curr c = Pos.revSkipWhile curr (· == c) := by
fun_induction Pos.revSkipWhile curr c with
| case1 pos nextCurr h₁ h₂ ih =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_char_eq_revSkip?_beq, h₁, h₂, ih]
simp [ Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq, h₁, h₂, ih]
| case2 pos nextCurr h ih =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_char_eq_revSkip?_beq, h, ih]
simp [ Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq, h, ih]
| case3 pos h =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_char_eq_revSkip?_beq, h]
simp [ Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq]
theorem skipSuffixWhile_char_eq_skipSuffixWhile_beq {c : Char} {s : Slice} :
s.skipSuffixWhile c = s.skipSuffixWhile (· == c) :=
@@ -381,16 +323,4 @@ theorem takeEndWhile_char_eq_takeEndWhile_beq {c : Char} {s : Slice} :
s.takeEndWhile c = s.takeEndWhile (· == c) := by
simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_char_eq_skipSuffixWhile_beq
theorem revFind?_char_eq_revFind?_beq {c : Char} {s : Slice} :
s.revFind? c = s.revFind? (· == c) :=
(rfl)
theorem Pos.revFind?_char_eq_revFind?_beq {c : Char} {s : Slice} {p : s.Pos} :
p.revFind? c = p.revFind? (· == c) :=
(rfl)
theorem revAll_char_eq_revAll_beq {c : Char} {s : Slice} :
s.revAll c = s.revAll (· == c) := by
simp [revAll, skipSuffixWhile_char_eq_skipSuffixWhile_beq]
end String.Slice

View File

@@ -23,8 +23,8 @@ open Std String.Slice Pattern Pattern.Model
namespace String.Slice
theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat]
{σ : Slice Type} [ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice Type}
[ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
[ s, IteratorLoop (σ s) Id Id] [ s, LawfulIteratorLoop (σ s) Id Id]
[ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} :
s.find? pat = some pos MatchesAt pat pos ( pos', pos' < pos ¬ MatchesAt pat pos') := by
@@ -40,8 +40,8 @@ theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [PatternModel pat
| matched h₁ _ _ => have := h₁.matchesAt; grind
| mismatched => grind
theorem Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat]
{σ : Slice Type} [ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
theorem Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice Type}
[ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
[ s, IteratorLoop (σ s) Id Id] [ s, LawfulIteratorLoop (σ s) Id Id]
[ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
s.find? pat = none (pos : s.Pos), ¬ MatchesAt pat pos := by
@@ -65,15 +65,15 @@ theorem find?_eq_none_iff {ρ : Type} (pat : ρ) {σ : Slice → Type}
[ToForwardSearcher pat σ] {s : Slice} : s.find? pat = none s.contains pat = false := by
rw [ Option.isNone_iff_eq_none, Option.isSome_eq_false_iff, isSome_find?]
theorem Pattern.Model.contains_eq_false_iff {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat]
{σ : Slice Type} [ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
theorem Pattern.Model.contains_eq_false_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice Type}
[ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
[ s, IteratorLoop (σ s) Id Id] [ s, LawfulIteratorLoop (σ s) Id Id]
[ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
s.contains pat = false (pos : s.Pos), ¬ MatchesAt pat pos := by
rw [ find?_eq_none_iff, Slice.find?_eq_none_iff]
theorem Pattern.Model.contains_eq_true_iff {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat]
{σ : Slice Type} [ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
theorem Pattern.Model.contains_eq_true_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice Type}
[ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
[ s, IteratorLoop (σ s) Id Id] [ s, LawfulIteratorLoop (σ s) Id Id]
[ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
s.contains pat (pos : s.Pos), MatchesAt pat pos := by
@@ -85,7 +85,7 @@ theorem Pos.find?_eq_find?_sliceFrom {ρ : Type} {pat : ρ} {σ : Slice → Type
p.find? pat = ((s.sliceFrom p).find? pat).map Pos.ofSliceFrom :=
(rfl)
theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {σ : Slice Type}
theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] {σ : Slice Type}
[ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
[ s, IteratorLoop (σ s) Id Id] [ s, LawfulIteratorLoop (σ s) Id Id]
[ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos pos' : s.Pos} :
@@ -100,8 +100,8 @@ theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel
refine Pos.sliceFrom _ _ h₁, by simpa using h₂, fun p hp₁ hp₂ => ?_, by simp
exact h₃ (Pos.ofSliceFrom p) Slice.Pos.le_ofSliceFrom (Pos.lt_sliceFrom_iff.1 hp₁) hp₂
theorem Pattern.Model.posFind?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat]
{σ : Slice Type} [ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
theorem Pattern.Model.posFind?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] {σ : Slice Type}
[ s, Iterator (σ s) Id (SearchStep s)] [ s, Iterators.Finite (σ s) Id]
[ s, IteratorLoop (σ s) Id Id] [ s, LawfulIteratorLoop (σ s) Id Id]
[ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} :
pos.find? pat = none pos', pos pos' ¬ MatchesAt pat pos' := by

View File

@@ -49,10 +49,9 @@ theorem contains_slice_iff {t s : Slice} :
by_cases ht : t.isEmpty
· simp [contains_eq_true_of_isEmpty ht s, copy_eq_empty_iff.mpr ht, String.toList_empty]
· simp only [Bool.not_eq_true] at ht
have := Pattern.Model.ForwardSliceSearcher.strictPatternModel ht
have := Pattern.Model.ForwardSliceSearcher.lawfulToForwardSearcherModel ht
simp only [Pattern.Model.contains_eq_true_iff,
Pattern.Model.ForwardSliceSearcher.exists_matchesAt_iff_eq_append, isInfix_toList_iff]
Pattern.Model.ForwardSliceSearcher.exists_matchesAt_iff_eq_append ht, isInfix_toList_iff]
@[simp]
theorem contains_string_iff {t : String} {s : Slice} :

View File

@@ -18,7 +18,6 @@ import Init.Data.String.Lemmas.Basic
import Init.Data.String.Lemmas.Order
import Init.Data.Order.Lemmas
import Init.Data.String.OrderInstances
import Init.Data.String.Lemmas.Iterate
import Init.Omega
import Init.Data.String.Lemmas.FindPos
@@ -28,9 +27,8 @@ namespace String.Slice.Pattern.Model.CharPred
instance {p : Char Bool} : PatternModel p where
Matches s := c, s = singleton c p c
instance {p : Char Bool} : StrictPatternModel p where
not_matches_empty := by simp [PatternModel.Matches]
not_matches_empty := by
simp
instance {p : Char Bool} : NoPrefixPatternModel p :=
.of_length_eq (by simp +contextual [PatternModel.Matches])
@@ -73,39 +71,6 @@ theorem isLongestMatchAt_iff {p : Char → Bool} {s : Slice} {pos pos' : s.Pos}
simp +contextual [Model.isLongestMatchAt_iff, isLongestMatch_iff, Pos.ofSliceFrom_inj,
Pos.get_eq_get_ofSliceFrom, Pos.ofSliceFrom_next]
theorem isLongestMatchAtChain_iff {p : Char Bool} {s : Slice} {pos pos' : s.Pos} :
IsLongestMatchAtChain p pos pos' pos pos' pos'', pos pos'' (h : pos'' < pos') p (pos''.get (Pos.ne_endPos_of_lt h)) := by
induction pos using WellFounded.induction Pos.wellFounded_gt with | h pos ih
obtain (h|rfl|h) := Std.lt_trichotomy pos pos'
· refine fun h => ?_, fun h₁, h₂ => ?_
· cases h with
| nil => exact (Std.lt_irrefl h).elim
| cons _ mid _ h₁ h₂ =>
obtain h₀, rfl, h₁' := isLongestMatchAt_iff.1 h₁
refine Std.le_of_lt h, fun pos'' hp₁ hp₂ => ?_
obtain (hh|rfl) := Std.le_iff_lt_or_eq.1 hp₁
· exact ((ih (pos.next (Pos.ne_endPos_of_lt h)) Pos.lt_next).1 h₂).2 _ (by simpa) hp₂
· exact h₁'
· refine .cons _ (pos.next (Pos.ne_endPos_of_lt h)) _ ?_ ((ih _ Pos.lt_next).2 ?_)
· exact isLongestMatchAt_iff.2 Pos.ne_endPos_of_lt h, rfl, h₂ _ (by simp) h
· exact by simpa, fun pos'' hp₁ hp₂ => h₂ _ (Std.le_trans Pos.le_next hp₁) hp₂
· simpa using fun _ h₁ h₂ => (Std.lt_irrefl (Std.lt_of_le_of_lt h₁ h₂)).elim
· simpa [Std.not_le.2 h] using fun h' => (Std.not_le.2 h h'.le).elim
theorem isLongestMatchAtChain_iff_toList {p : Char Bool} {s : Slice} {pos pos' : s.Pos} :
IsLongestMatchAtChain p pos pos' (h : pos pos'), c, c (s.slice pos pos' h).copy.toList p c := by
simp only [isLongestMatchAtChain_iff, mem_toList_copy_iff_exists_get, Pos.get_eq_get_ofSlice,
forall_exists_index]
refine fun h₁, h₂ => h₁, fun c p' hp => ?_, fun h₁, h₂ => h₁, fun p' hp₁ hp₂ => ?_
· rintro rfl
exact h₂ _ Pos.le_ofSlice (by simp [Pos.ofSlice_lt_iff, h₁, hp])
· refine h₂ _ (Pos.slice p' _ _ hp₁ (Std.le_of_lt hp₂)) ?_ (by simp)
rwa [ Pos.lt_endPos_iff, Pos.slice_eq_endPos (h := h₁), Pos.slice_lt_slice_iff]
theorem isLongestMatchAtChain_startPos_endPos_iff_toList {p : Char Bool} {s : Slice} :
IsLongestMatchAtChain p s.startPos s.endPos c, c s.copy.toList p c := by
simp [isLongestMatchAtChain_iff_toList]
theorem isLongestRevMatchAt_iff {p : Char Bool} {s : Slice} {pos pos' : s.Pos} :
IsLongestRevMatchAt p pos pos' h, pos = pos'.prev h p ((pos'.prev h).get (by simp)) := by
simp +contextual [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff, Pos.ofSliceTo_inj,
@@ -119,35 +84,6 @@ theorem isLongestRevMatchAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos}
(hc : p ((pos.prev h).get (by simp))) : IsLongestRevMatchAt p (pos.prev h) pos :=
isLongestRevMatchAt_iff.2 h, by simp [hc]
theorem isLongestRevMatchAtChain_iff {p : Char Bool} {s : Slice} {pos pos' : s.Pos} :
IsLongestRevMatchAtChain p pos pos' pos pos' pos'', pos pos'' (h : pos'' < pos') p (pos''.get (Pos.ne_endPos_of_lt h)) := by
induction pos' using WellFounded.induction Pos.wellFounded_lt with | h pos' ih
obtain (h|rfl|h) := Std.lt_trichotomy pos pos'
· refine fun h => ?_, fun h₁, h₂ => ?_
· cases h with
| nil => exact (Std.lt_irrefl h).elim
| cons _ _ hchain hmatch =>
obtain hne, hmid, hp := isLongestRevMatchAt_iff.1 hmatch
refine Std.le_of_lt h, fun pos'' hp₁ hp₂ => ?_
rcases Std.le_iff_lt_or_eq.1 (Pos.le_prev_iff_lt.2 hp₂) with hh | heq
· exact ((ih _ Pos.prev_lt).1 (hmid hchain)).2 _ hp₁ hh
· exact heq hp
· have hne : pos' s.startPos := Slice.Pos.ne_startPos_of_lt h
refine .cons _ (pos'.prev hne) _ ((ih _ Pos.prev_lt).2 ?_)
(isLongestRevMatchAt_of_get (h₂ _ (Pos.le_prev_iff_lt.2 h) Pos.prev_lt))
exact Pos.le_prev_iff_lt.2 h, fun pos'' hp₁ hp₂ =>
h₂ _ hp₁ (Std.lt_trans hp₂ Pos.prev_lt)
· simpa using fun _ h₁ h₂ => (Std.lt_irrefl (Std.lt_of_le_of_lt h₁ h₂)).elim
· simpa [Std.not_le.2 h] using fun h' => (Std.not_le.2 h h'.le).elim
theorem isLongestRevMatchAtChain_iff_toList {p : Char Bool} {s : Slice} {pos pos' : s.Pos} :
IsLongestRevMatchAtChain p pos pos' (h : pos pos'), c, c (s.slice pos pos' h).copy.toList p c :=
isLongestRevMatchAtChain_iff.trans (isLongestMatchAtChain_iff.symm.trans isLongestMatchAtChain_iff_toList)
theorem isLongestRevMatchAtChain_startPos_endPos_iff_toList {p : Char Bool} {s : Slice} :
IsLongestRevMatchAtChain p s.startPos s.endPos c, c s.copy.toList p c := by
simp [isLongestRevMatchAtChain_iff_toList]
instance {p : Char Bool} : LawfulForwardPatternModel p where
skipPrefix?_eq_some_iff {s} pos := by
simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, and_comm, eq_comm (b := pos)]
@@ -192,9 +128,7 @@ namespace Decidable
instance {p : Char Prop} [DecidablePred p] : PatternModel p where
Matches := PatternModel.Matches (decide <| p ·)
instance {p : Char Prop} [DecidablePred p] : StrictPatternModel p where
not_matches_empty := StrictPatternModel.not_matches_empty (pat := (decide <| p ·))
not_matches_empty := PatternModel.not_matches_empty (pat := (decide <| p ·))
instance {p : Char Prop} [DecidablePred p] : NoPrefixPatternModel p where
eq_empty := NoPrefixPatternModel.eq_empty (pat := (decide <| p ·))
@@ -248,32 +182,6 @@ theorem isLongestRevMatchAt_iff_isLongestRevMatchAt_decide {p : Char → Prop} [
IsLongestRevMatchAt p pos pos' IsLongestRevMatchAt (decide <| p ·) pos pos' := by
simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff_isLongestRevMatch_decide]
theorem isLongestMatchAtChain_iff_isLongestMatchAtChain_decide {p : Char Prop} [DecidablePred p]
{s : Slice} {pos pos' : s.Pos} :
IsLongestMatchAtChain p pos pos' IsLongestMatchAtChain (decide <| p ·) pos pos' := by
constructor
· intro h; induction h with
| nil => exact .nil _
| cons _ mid _ hmatch hchain ih =>
exact .cons _ mid _ (isLongestMatchAt_iff_isLongestMatchAt_decide.1 hmatch) ih
· intro h; induction h with
| nil => exact .nil _
| cons _ mid _ hmatch hchain ih =>
exact .cons _ mid _ (isLongestMatchAt_iff_isLongestMatchAt_decide.2 hmatch) ih
theorem isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_decide {p : Char Prop} [DecidablePred p]
{s : Slice} {pos pos' : s.Pos} :
IsLongestRevMatchAtChain p pos pos' IsLongestRevMatchAtChain (decide <| p ·) pos pos' := by
constructor
· intro h; induction h with
| nil => exact .nil _
| cons _ _ hchain hmatch ih =>
exact .cons _ _ _ ih (isLongestRevMatchAt_iff_isLongestRevMatchAt_decide.1 hmatch)
· intro h; induction h with
| nil => exact .nil _
| cons _ _ hchain hmatch ih =>
exact .cons _ _ _ ih (isLongestRevMatchAt_iff_isLongestRevMatchAt_decide.2 hmatch)
theorem isLongestMatchAt_iff {p : Char Prop} [DecidablePred p] {s : Slice}
{pos pos' : s.Pos} :
IsLongestMatchAt p pos pos' h, pos' = pos.next h p (pos.get h) := by
@@ -411,9 +319,6 @@ theorem dropPrefix_prop_eq_dropPrefix_decide {p : Char → Prop} [DecidablePred
theorem skipPrefix?_prop_eq_skipPrefix?_decide {p : Char Prop} [DecidablePred p] {s : Slice} :
s.skipPrefix? p = s.skipPrefix? (decide <| p ·) := (rfl)
theorem Pos.skip?_prop_eq_skip?_decide {p : Char Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
pos.skip? p = pos.skip? (decide <| p ·) := (rfl)
theorem Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide
{p : Char Prop} [DecidablePred p] {s : Slice} :
skipPrefix? p s = skipPrefix? (decide <| p ·) s := (rfl)
@@ -424,13 +329,13 @@ theorem Pos.skipWhile_prop_eq_skipWhile_decide {p : Char → Prop} [DecidablePre
fun_induction Pos.skipWhile curr p with
| case1 pos nextCurr h₁ h₂ ih =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_prop_eq_skip?_decide, h₁, h₂, ih]
simp [ Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h₁, h₂, ih]
| case2 pos nextCurr h ih =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_prop_eq_skip?_decide, h, ih]
simp [ Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h, ih]
| case3 pos h =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_prop_eq_skip?_decide, h]
simp [ Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide]
theorem skipPrefixWhile_prop_eq_skipPrefixWhile_decide {p : Char Prop} [DecidablePred p]
{s : Slice} :
@@ -447,7 +352,7 @@ theorem takeWhile_prop_eq_takeWhile_decide {p : Char → Prop} [DecidablePred p]
theorem all_prop_eq_all_decide {p : Char Prop} [DecidablePred p] {s : Slice} :
s.all p = s.all (decide <| p ·) := by
simp only [all, skipPrefixWhile_prop_eq_skipPrefixWhile_decide]
simp only [all, dropWhile_prop_eq_dropWhile_decide]
theorem find?_prop_eq_find?_decide {p : Char Prop} [DecidablePred p] {s : Slice} :
s.find? p = s.find? (decide <| p ·) :=
@@ -478,22 +383,19 @@ theorem Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide
{p : Char Prop} [DecidablePred p] {s : Slice} :
skipSuffix? p s = skipSuffix? (decide <| p ·) s := (rfl)
theorem Pos.revSkip?_prop_eq_revSkip?_decide {p : Char Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
pos.revSkip? p = pos.revSkip? (decide <| p ·) := (rfl)
theorem Pos.revSkipWhile_prop_eq_revSkipWhile_decide {p : Char Prop} [DecidablePred p]
{s : Slice} (curr : s.Pos) :
Pos.revSkipWhile curr p = Pos.revSkipWhile curr (decide <| p ·) := by
fun_induction Pos.revSkipWhile curr p with
| case1 pos nextCurr h₁ h₂ ih =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_prop_eq_revSkip?_decide, h₁, h₂, ih]
simp [ Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide, h₁, h₂, ih]
| case2 pos nextCurr h ih =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_prop_eq_revSkip?_decide, h, ih]
simp [ Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide, h, ih]
| case3 pos h =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_prop_eq_revSkip?_decide, h]
simp [ Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide]
theorem skipSuffixWhile_prop_eq_skipSuffixWhile_decide {p : Char Prop} [DecidablePred p]
{s : Slice} :
@@ -510,8 +412,4 @@ theorem takeEndWhile_prop_eq_takeEndWhile_decide {p : Char → Prop} [DecidableP
s.takeEndWhile p = s.takeEndWhile (decide <| p ·) := by
simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_prop_eq_skipSuffixWhile_decide
theorem revAll_prop_eq_revAll_decide {p : Char Prop} [DecidablePred p] {s : Slice} :
s.revAll p = s.revAll (decide <| p ·) := by
simp only [revAll, skipSuffixWhile_prop_eq_skipSuffixWhile_decide]
end String.Slice

View File

@@ -36,7 +36,7 @@ This gives a low-level correctness proof from which higher-level API lemmas can
namespace String.Slice.Pattern.Model
@[cbv_opaque]
public protected noncomputable def split {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat] {s : Slice}
public protected noncomputable def split {ρ : Type} (pat : ρ) [PatternModel pat] {s : Slice}
(firstRejected curr : s.Pos) (hle : firstRejected curr) : List s.Subslice :=
if h : curr = s.endPos then
[s.subslice _ _ hle]
@@ -49,12 +49,12 @@ public protected noncomputable def split {ρ : Type} (pat : ρ) [PatternModel pa
termination_by curr
@[simp]
public theorem split_endPos {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] {s : Slice}
public theorem split_endPos {ρ : Type} {pat : ρ} [PatternModel pat] {s : Slice}
{firstRejected : s.Pos} :
Model.split (s := s) pat firstRejected s.endPos (by simp) = [s.subslice firstRejected s.endPos (by simp)] := by
simp [Model.split]
public theorem split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat]
public theorem split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [PatternModel pat]
{s : Slice} {firstRejected start stop : s.Pos} {hle} (h : IsLongestMatchAt pat start stop) :
Model.split pat firstRejected start hle =
s.subslice _ _ hle :: Model.split pat stop stop (by exact Std.le_refl _) := by
@@ -63,7 +63,7 @@ public theorem split_eq_of_isLongestMatchAt {ρ : Type} {pat : ρ} [PatternModel
· congr <;> exact (matchAt?_eq_some_iff.1 _).eq h
· simp [matchAt?_eq_some_iff.2 _] at *
public theorem split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat]
public theorem split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat]
{s : Slice} {firstRejected start} (stop : s.Pos) (h₀ : start stop) {hle}
(h : p, start p p < stop ¬ MatchesAt pat p) :
Model.split pat firstRejected start hle =
@@ -80,7 +80,7 @@ public theorem split_eq_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pa
· obtain rfl : start = stop := Std.le_antisymm h₀ (Std.not_lt.1 h')
simp
public theorem split_eq_next_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat]
public theorem split_eq_next_of_not_matchesAt {ρ : Type} {pat : ρ} [PatternModel pat]
{s : Slice} {firstRejected start} {hle} (hs : start s.endPos) (h : ¬ MatchesAt pat start) :
Model.split pat firstRejected start hle =
Model.split pat firstRejected (start.next hs) (by exact Std.le_trans hle (by simp)) := by
@@ -103,7 +103,7 @@ def splitFromSteps {s : Slice} (currPos : s.Pos) (l : List (SearchStep s)) : Lis
| .matched p q :: l => s.subslice! currPos p :: splitFromSteps q l
theorem IsValidSearchFrom.splitFromSteps_eq_extend_split {ρ : Type} (pat : ρ)
[PatternModel pat] [StrictPatternModel pat] (l : List (SearchStep s)) (pos pos' : s.Pos) (h₀ : pos pos')
[PatternModel pat] (l : List (SearchStep s)) (pos pos' : s.Pos) (h₀ : pos pos')
(h' : p, pos p p < pos' ¬ MatchesAt pat p)
(h : IsValidSearchFrom pat pos' l) :
splitFromSteps pos l = Model.split pat pos pos' h₀ := by
@@ -155,7 +155,7 @@ end Model
open Model
@[cbv_eval]
public theorem toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat]
public theorem toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [PatternModel pat]
{σ : Slice Type} [ToForwardSearcher pat σ] [ s, Std.Iterator (σ s) Id (SearchStep s)]
[ s, Std.Iterators.Finite (σ s) Id] [LawfulToForwardSearcherModel pat] (s : Slice) :
(s.splitToSubslice pat).toList = Model.split pat s.startPos s.startPos (by exact Std.le_refl _) := by
@@ -168,7 +168,7 @@ end Pattern
open Pattern
public theorem toList_splitToSubslice_of_isEmpty {ρ : Type} (pat : ρ)
[Model.PatternModel pat] [Model.StrictPatternModel pat] {σ : Slice Type}
[Model.PatternModel pat] {σ : Slice Type}
[ToForwardSearcher pat σ] [ s, Std.Iterator (σ s) Id (SearchStep s)]
[ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] {s : Slice}
(h : s.isEmpty = true) :
@@ -182,7 +182,7 @@ public theorem toList_split_eq_splitToSubslice {ρ : Type} (pat : ρ) {σ : Slic
simp [split, Std.Iter.toList_map]
public theorem toList_split_of_isEmpty {ρ : Type} (pat : ρ)
[Model.PatternModel pat] [Model.StrictPatternModel pat] {σ : Slice Type}
[Model.PatternModel pat] {σ : Slice Type}
[ToForwardSearcher pat σ] [ s, Std.Iterator (σ s) Id (SearchStep s)]
[ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] {s : Slice}
(h : s.isEmpty = true) :
@@ -200,7 +200,7 @@ public theorem split_eq_split_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Typ
@[simp]
public theorem toList_split_empty {ρ : Type} (pat : ρ)
[Model.PatternModel pat] [Model.StrictPatternModel pat] {σ : Slice Type}
[Model.PatternModel pat] {σ : Slice Type}
[ToForwardSearcher pat σ] [ s, Std.Iterator (σ s) Id (SearchStep s)]
[ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] :
("".split pat).toList.map Slice.copy = [""] := by

View File

@@ -10,9 +10,6 @@ public import Init.Data.String.Pattern.String
public import Init.Data.String.Lemmas.Pattern.Basic
import Init.Data.String.Lemmas.IsEmpty
import Init.Data.String.Lemmas.Basic
import Init.Data.String.Lemmas.Intercalate
import Init.Data.String.OrderInstances
import Init.Data.String.Lemmas.Splits
import Init.Data.ByteArray.Lemmas
import Init.Omega
@@ -23,10 +20,17 @@ namespace String.Slice.Pattern.Model
namespace ForwardSliceSearcher
instance {pat : Slice} : PatternModel pat where
Matches s := s = pat.copy
/-
See the docstring of `PatternModel` for an explanation about why we disallow matching the
empty string.
theorem strictPatternModel {pat : Slice} (hpat : pat.isEmpty = false) : StrictPatternModel pat where
not_matches_empty := by simpa [PatternModel.Matches]
Requiring `s ≠ ""` is a trick that allows us to give a `PatternModel` instance
unconditionally, without forcing `pat.copy` to be non-empty (which would make it very awkward
to state theorems about the instance). It does not change anything about the fact that all lemmas
about this instance require `pat.isEmpty = false`.
-/
Matches s := s "" s = pat.copy
not_matches_empty := by simp
instance {pat : Slice} : NoPrefixPatternModel pat :=
.of_length_eq (by simp +contextual [PatternModel.Matches])
@@ -34,111 +38,59 @@ instance {pat : Slice} : NoPrefixPatternModel pat :=
instance {pat : Slice} : NoSuffixPatternModel pat :=
.of_length_eq (by simp +contextual [PatternModel.Matches])
theorem isMatch_iff {pat s : Slice} {pos : s.Pos} :
theorem isMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
IsMatch pat pos (s.sliceTo pos).copy = pat.copy := by
simp [Model.isMatch_iff, PatternModel.Matches]
simp only [Model.isMatch_iff, PatternModel.Matches, ne_eq, copy_eq_empty_iff,
Bool.not_eq_true, and_iff_right_iff_imp]
intro h'
rw [ isEmpty_copy (s := s.sliceTo pos), h', isEmpty_copy, h]
theorem isRevMatch_iff {pat s : Slice} {pos : s.Pos} :
theorem isRevMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
IsRevMatch pat pos (s.sliceFrom pos).copy = pat.copy := by
simp [Model.isRevMatch_iff, PatternModel.Matches]
simp only [Model.isRevMatch_iff, PatternModel.Matches, ne_eq, copy_eq_empty_iff,
Bool.not_eq_true, and_iff_right_iff_imp]
intro h'
rw [ isEmpty_copy (s := s.sliceFrom pos), h', isEmpty_copy, h]
theorem isLongestMatch_iff {pat s : Slice} {pos : s.Pos} :
theorem isLongestMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
IsLongestMatch pat pos (s.sliceTo pos).copy = pat.copy := by
rw [isLongestMatch_iff_isMatch, isMatch_iff]
rw [isLongestMatch_iff_isMatch, isMatch_iff h]
theorem isLongestRevMatch_iff {pat s : Slice} {pos : s.Pos} :
theorem isLongestRevMatch_iff {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
IsLongestRevMatch pat pos (s.sliceFrom pos).copy = pat.copy := by
rw [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff]
rw [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff h]
theorem isLongestMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
IsLongestMatchAt pat pos₁ pos₂ h, (s.slice pos₁ pos₂ h).copy = pat.copy := by
simp [Model.isLongestMatchAt_iff, isLongestMatch_iff]
simp [Model.isLongestMatchAt_iff, isLongestMatch_iff h]
theorem isLongestMatchAtChain_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} :
IsLongestMatchAtChain pat pos₁ pos₂
h n, (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat.copy) := by
refine fun h => h.le, ?_, fun h, n, h' => ?_
· induction h with
| nil => simpa using 0, by simp
| cons p₁ p₂ p₃ h₁ h₂ ih =>
rw [isLongestMatchAt_iff] at h₁
obtain n, ih := ih
obtain h₀, h₁ := h₁
have : (s.slice p₁ p₃ (Std.le_trans h₀ h₂.le)).copy = (s.slice p₁ p₂ h₀).copy ++ (s.slice p₂ p₃ h₂.le).copy := by
simp [(Slice.Pos.slice p₂ _ _ h₀ h₂.le).splits.eq_append]
refine n + 1, ?_
rw [this, h₁, ih]
simp [ String.join_cons, List.replicate_succ]
· induction n generalizing pos₁ pos₂ with
| zero => simp_all
| succ n ih =>
rw [List.replicate_succ, String.join_cons] at h'
refine .cons _ (Pos.ofSlice (Pos.ofEqAppend h')) _ ?_ (ih ?_ Pos.ofSlice_le ?_)
· simpa [isLongestMatchAt_iff] using (Pos.splits_ofEqAppend h').copy_sliceTo_eq
· simpa [sliceFrom_slice (Pos.splits_ofEqAppend h').copy_sliceFrom_eq] using n, rfl
· simpa using (Pos.splits_ofEqAppend h').copy_sliceFrom_eq
theorem isLongestMatchAtChain_startPos_endPos_iff {pat s : Slice} :
IsLongestMatchAtChain pat s.startPos s.endPos
n, s.copy = String.join (List.replicate n pat.copy) := by
simp [isLongestMatchAtChain_iff]
theorem isLongestRevMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestRevMatchAt_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
IsLongestRevMatchAt pat pos₁ pos₂ h, (s.slice pos₁ pos₂ h).copy = pat.copy := by
simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff]
simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff h]
theorem isLongestRevMatchAtChain_iff {pat s : Slice} {pos₁ pos₂ : s.Pos} :
IsLongestRevMatchAtChain pat pos₁ pos₂
h n, (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat.copy) := by
refine fun h => h.le, ?_, fun h, n, h' => ?_
· induction h with
| nil => simpa using 0, by simp
| cons p₂ p₃ h₁ h₂ ih =>
rw [isLongestRevMatchAt_iff] at h₂
obtain n, ih := ih
obtain h₀, h₂ := h₂
have : (s.slice pos₁ p₃ (Std.le_trans h₁.le h₀)).copy = (s.slice pos₁ p₂ h₁.le).copy ++ (s.slice p₂ p₃ h₀).copy := by
simp [(Slice.Pos.slice p₂ _ _ (IsLongestRevMatchAtChain.le _) h₀).splits.eq_append]
refine n + 1, ?_
rw [this, h₂, ih]
simp [ List.replicate_append_replicate]
· induction n generalizing pos₁ pos₂ with
| zero => simp_all
| succ n ih =>
have h'' : (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat.copy) ++ pat.copy := by
rw [h', List.replicate_succ', String.join_append]; simp
refine .cons _ (Pos.ofSlice (Pos.ofEqAppend h'')) _ (ih ?_ Pos.le_ofSlice ?_) ?_
· simpa [sliceTo_slice (Pos.splits_ofEqAppend h'').copy_sliceTo_eq] using n, rfl
· simpa using (Pos.splits_ofEqAppend h'').copy_sliceTo_eq
· simpa [isLongestRevMatchAt_iff] using (Pos.splits_ofEqAppend h'').copy_sliceFrom_eq
theorem isLongestRevMatchAtChain_startPos_endPos_iff {pat s : Slice} :
IsLongestRevMatchAtChain pat s.startPos s.endPos
n, s.copy = String.join (List.replicate n pat.copy) := by
simp [isLongestRevMatchAtChain_iff]
theorem isLongestMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
IsLongestMatchAt pat pos₁ pos₂ t₁ t₂, pos₁.Splits t₁ (pat.copy ++ t₂)
pos₂.Splits (t₁ ++ pat.copy) t₂ := by
simp only [isLongestMatchAt_iff, copy_slice_eq_iff_splits]
simp only [isLongestMatchAt_iff h, copy_slice_eq_iff_splits]
theorem isLongestRevMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestRevMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos}
(h : pat.isEmpty = false) :
IsLongestRevMatchAt pat pos₁ pos₂ t₁ t₂, pos₁.Splits t₁ (pat.copy ++ t₂)
pos₂.Splits (t₁ ++ pat.copy) t₂ := by
simp only [isLongestRevMatchAt_iff, copy_slice_eq_iff_splits]
simp only [isLongestRevMatchAt_iff h, copy_slice_eq_iff_splits]
theorem isLongestMatch_iff_splits {pat s : Slice} {pos : s.Pos} :
theorem isLongestMatch_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
IsLongestMatch pat pos t, pos.Splits pat.copy t := by
rw [isLongestMatch_iff, copy_sliceTo_eq_iff_exists_splits]
rw [isLongestMatch_iff h, copy_sliceTo_eq_iff_exists_splits]
theorem isLongestRevMatch_iff_splits {pat s : Slice} {pos : s.Pos} :
theorem isLongestRevMatch_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
IsLongestRevMatch pat pos t, pos.Splits t pat.copy := by
rw [isLongestRevMatch_iff, copy_sliceFrom_eq_iff_exists_splits]
rw [isLongestRevMatch_iff h, copy_sliceFrom_eq_iff_exists_splits]
theorem isLongestMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
IsLongestMatchAt pat pos₁ pos₂
s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.copy.toByteArray := by
rw [isLongestMatchAt_iff]
rw [isLongestMatchAt_iff h]
refine fun h, h' => ?_, fun h' => ?_
· simp [ h', toByteArray_copy_slice]
· rw [ Slice.toByteArray_copy_ne_empty_iff, h', ne_eq, ByteArray.extract_eq_empty_iff] at h
@@ -150,7 +102,7 @@ theorem isLongestRevMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos}
IsLongestRevMatchAt pat pos₁ pos₂
s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx =
pat.copy.toByteArray := by
rw [isLongestRevMatchAt_iff]
rw [isLongestRevMatchAt_iff h]
refine fun h, h' => ?_, fun h' => ?_
· simp [ h', toByteArray_copy_slice]
· rw [ Slice.toByteArray_copy_ne_empty_iff, h', ne_eq, ByteArray.extract_eq_empty_iff] at h
@@ -178,21 +130,21 @@ theorem offset_of_isLongestRevMatchAt {pat s : Slice} {pos₁ pos₂ : s.Pos}
suffices pos₂.offset.byteIdx s.utf8ByteSize by omega
simpa [Pos.le_iff, Pos.Raw.le_iff] using pos₂.le_endPos
theorem matchesAt_iff_splits {pat s : Slice} {pos : s.Pos} :
theorem matchesAt_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
MatchesAt pat pos t₁ t₂, pos.Splits t₁ (pat.copy ++ t₂) := by
simp only [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_splits]
simp only [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_splits h]
exact fun e, t₁, t₂, ht₁, ht₂ => t₁, t₂, ht₁,
fun t₁, t₂, ht => ht.rotateRight, t₁, t₂, ht, ht.splits_rotateRight
theorem revMatchesAt_iff_splits {pat s : Slice} {pos : s.Pos} :
theorem revMatchesAt_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
RevMatchesAt pat pos t₁ t₂, pos.Splits (t₁ ++ pat.copy) t₂ := by
simp only [revMatchesAt_iff_exists_isLongestRevMatchAt, isLongestRevMatchAt_iff_splits]
simp only [revMatchesAt_iff_exists_isLongestRevMatchAt, isLongestRevMatchAt_iff_splits h]
exact fun e, t₁, t₂, ht₁, ht₂ => t₁, t₂, ht₂,
fun t₁, t₂, ht => ht.rotateLeft, t₁, t₂, ht.splits_rotateLeft, ht
theorem exists_matchesAt_iff_eq_append {pat s : Slice} :
theorem exists_matchesAt_iff_eq_append {pat s : Slice} (h : pat.isEmpty = false) :
( (pos : s.Pos), MatchesAt pat pos) t₁ t₂, s.copy = t₁ ++ pat.copy ++ t₂ := by
simp only [matchesAt_iff_splits]
simp only [matchesAt_iff_splits h]
constructor
· rintro pos, t₁, t₂, hsplit
exact t₁, t₂, by rw [hsplit.eq_append, append_assoc]
@@ -202,9 +154,9 @@ theorem exists_matchesAt_iff_eq_append {pat s : Slice} :
t₁, pat.copy ++ t₂, by rw [ append_assoc]; exact heq, rfl
exact s.pos _ hvalid, t₁, t₂, by rw [ append_assoc]; exact heq, by simp
theorem exists_revMatchesAt_iff_eq_append {pat s : Slice} :
theorem exists_revMatchesAt_iff_eq_append {pat s : Slice} (h : pat.isEmpty = false) :
( (pos : s.Pos), RevMatchesAt pat pos) t₁ t₂, s.copy = t₁ ++ pat.copy ++ t₂ := by
simp only [revMatchesAt_iff_splits]
simp only [revMatchesAt_iff_splits h]
constructor
· rintro pos, t₁, t₂, hsplit
exact t₁, t₂, by rw [hsplit.eq_append, append_assoc]
@@ -281,10 +233,8 @@ end ForwardSliceSearcher
namespace ForwardStringSearcher
instance {pat : String} : PatternModel pat where
Matches s := s = pat
theorem strictPatternModel {pat : String} (h : pat "") : StrictPatternModel pat where
not_matches_empty := by simpa [PatternModel.Matches]
Matches s := s "" s = pat
not_matches_empty := by simp
instance {pat : String} : NoPrefixPatternModel pat :=
.of_length_eq (by simp +contextual [PatternModel.Matches])
@@ -317,60 +267,12 @@ theorem isLongestMatchAt_iff_isLongestMatchAt_toSlice {pat : String} {s : Slice}
IsLongestMatchAt (ρ := Slice) pat.toSlice pos₁ pos₂ := by
simp [Model.isLongestMatchAt_iff, isLongestMatch_iff_isLongestMatch_toSlice]
theorem isLongestMatchAtChain_iff_isLongestMatchAtChain_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
IsLongestMatchAtChain pat pos₁ pos₂
IsLongestMatchAtChain pat.toSlice pos₁ pos₂ := by
refine fun h => ?_, fun h => ?_
· induction h with
| nil => simp
| cons p₁ p₂ p₃ h₁ h₂ ih =>
exact .cons _ _ _ (isLongestMatchAt_iff_isLongestMatchAt_toSlice.1 h₁) ih
· induction h with
| nil => simp
| cons p₁ p₂ p₃ h₁ h₂ ih =>
exact .cons _ _ _ (isLongestMatchAt_iff_isLongestMatchAt_toSlice.2 h₁) ih
theorem isLongestMatchAtChain_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
IsLongestMatchAtChain pat pos₁ pos₂
h n, (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat) := by
simp [isLongestMatchAtChain_iff_isLongestMatchAtChain_toSlice,
ForwardSliceSearcher.isLongestMatchAtChain_iff]
theorem isLongestMatchAtChain_startPos_endPos_iff {pat : String} {s : Slice} :
IsLongestMatchAtChain pat s.startPos s.endPos
n, s.copy = String.join (List.replicate n pat) := by
simp [isLongestMatchAtChain_iff]
theorem isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice {pat : String} {s : Slice}
{pos₁ pos₂ : s.Pos} :
IsLongestRevMatchAt (ρ := String) pat pos₁ pos₂
IsLongestRevMatchAt (ρ := Slice) pat.toSlice pos₁ pos₂ := by
simp [Model.isLongestRevMatchAt_iff, isLongestRevMatch_iff_isLongestRevMatch_toSlice]
theorem isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_toSlice {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
IsLongestRevMatchAtChain pat pos₁ pos₂
IsLongestRevMatchAtChain pat.toSlice pos₁ pos₂ := by
refine fun h => ?_, fun h => ?_
· induction h with
| nil => simp
| cons p₂ p₃ _ hmatch ih =>
exact .cons _ _ _ ih (isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice.1 hmatch)
· induction h with
| nil => simp
| cons p₂ p₃ _ hmatch ih =>
exact .cons _ _ _ ih (isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice.2 hmatch)
theorem isLongestRevMatchAtChain_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
IsLongestRevMatchAtChain pat pos₁ pos₂
h n, (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat) := by
simp [isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_toSlice,
ForwardSliceSearcher.isLongestRevMatchAtChain_iff]
theorem isLongestRevMatchAtChain_startPos_endPos_iff {pat : String} {s : Slice} :
IsLongestRevMatchAtChain pat s.startPos s.endPos
n, s.copy = String.join (List.replicate n pat) := by
simp [isLongestRevMatchAtChain_iff]
theorem matchesAt_iff_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
MatchesAt (ρ := String) pat pos MatchesAt (ρ := Slice) pat.toSlice pos := by
simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff_isLongestMatchAt_toSlice]
@@ -380,55 +282,61 @@ theorem revMatchesAt_iff_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
simp [revMatchesAt_iff_exists_isLongestRevMatchAt,
isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice]
theorem isMatch_iff {pat : String} {s : Slice} {pos : s.Pos} :
private theorem toSlice_isEmpty (h : pat "") : pat.toSlice.isEmpty = false := by
rwa [isEmpty_toSlice, isEmpty_eq_false_iff]
theorem isMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat "") :
IsMatch pat pos (s.sliceTo pos).copy = pat := by
rw [isMatch_iff_slice, ForwardSliceSearcher.isMatch_iff]
rw [isMatch_iff_slice, ForwardSliceSearcher.isMatch_iff (toSlice_isEmpty h)]
simp
theorem isRevMatch_iff {pat : String} {s : Slice} {pos : s.Pos} :
theorem isRevMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat "") :
IsRevMatch pat pos (s.sliceFrom pos).copy = pat := by
rw [isRevMatch_iff_slice, ForwardSliceSearcher.isRevMatch_iff]
rw [isRevMatch_iff_slice, ForwardSliceSearcher.isRevMatch_iff (toSlice_isEmpty h)]
simp
theorem isLongestMatch_iff {pat : String} {s : Slice} {pos : s.Pos} :
theorem isLongestMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat "") :
IsLongestMatch pat pos (s.sliceTo pos).copy = pat := by
rw [isLongestMatch_iff_isMatch, isMatch_iff]
rw [isLongestMatch_iff_isMatch, isMatch_iff h]
theorem isLongestRevMatch_iff {pat : String} {s : Slice} {pos : s.Pos} :
theorem isLongestRevMatch_iff {pat : String} {s : Slice} {pos : s.Pos} (h : pat "") :
IsLongestRevMatch pat pos (s.sliceFrom pos).copy = pat := by
rw [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff]
rw [isLongestRevMatch_iff_isRevMatch, isRevMatch_iff h]
theorem isLongestMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat "") :
IsLongestMatchAt pat pos₁ pos₂ h, (s.slice pos₁ pos₂ h).copy = pat := by
rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice,
ForwardSliceSearcher.isLongestMatchAt_iff]
ForwardSliceSearcher.isLongestMatchAt_iff (toSlice_isEmpty h)]
simp
theorem isLongestRevMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestRevMatchAt_iff {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat "") :
IsLongestRevMatchAt pat pos₁ pos₂ h, (s.slice pos₁ pos₂ h).copy = pat := by
rw [isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice,
ForwardSliceSearcher.isLongestRevMatchAt_iff]
ForwardSliceSearcher.isLongestRevMatchAt_iff (toSlice_isEmpty h)]
simp
theorem isLongestMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
(h : pat "") :
IsLongestMatchAt pat pos₁ pos₂
t₁ t₂, pos₁.Splits t₁ (pat ++ t₂) pos₂.Splits (t₁ ++ pat) t₂ := by
rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice,
ForwardSliceSearcher.isLongestMatchAt_iff_splits]
ForwardSliceSearcher.isLongestMatchAt_iff_splits (toSlice_isEmpty h)]
simp
theorem isLongestRevMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} :
theorem isLongestRevMatchAt_iff_splits {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
(h : pat "") :
IsLongestRevMatchAt pat pos₁ pos₂
t₁ t₂, pos₁.Splits t₁ (pat ++ t₂) pos₂.Splits (t₁ ++ pat) t₂ := by
rw [isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice,
ForwardSliceSearcher.isLongestRevMatchAt_iff_splits]
ForwardSliceSearcher.isLongestRevMatchAt_iff_splits (toSlice_isEmpty h)]
simp
theorem isLongestMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos} (h : pat "") :
theorem isLongestMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
(h : pat "") :
IsLongestMatchAt pat pos₁ pos₂
s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray := by
rw [isLongestMatchAt_iff_isLongestMatchAt_toSlice,
ForwardSliceSearcher.isLongestMatchAt_iff_extract (by simpa)]
ForwardSliceSearcher.isLongestMatchAt_iff_extract (toSlice_isEmpty h)]
simp
theorem isLongestRevMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
@@ -436,38 +344,38 @@ theorem isLongestRevMatchAt_iff_extract {pat : String} {s : Slice} {pos₁ pos
IsLongestRevMatchAt pat pos₁ pos₂
s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray := by
rw [isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice,
ForwardSliceSearcher.isLongestRevMatchAt_iff_extract (by simpa)]
ForwardSliceSearcher.isLongestRevMatchAt_iff_extract (toSlice_isEmpty h)]
simp
theorem offset_of_isLongestMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
(h : pat "") (h' : IsLongestMatchAt pat pos₁ pos₂) :
pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize := by
rw [show pat.utf8ByteSize = pat.toSlice.utf8ByteSize from utf8ByteSize_toSlice.symm]
exact ForwardSliceSearcher.offset_of_isLongestMatchAt (by simpa)
exact ForwardSliceSearcher.offset_of_isLongestMatchAt (toSlice_isEmpty h)
(isLongestMatchAt_iff_isLongestMatchAt_toSlice.1 h')
theorem offset_of_isLongestRevMatchAt {pat : String} {s : Slice} {pos₁ pos₂ : s.Pos}
(h : pat "") (h' : IsLongestRevMatchAt pat pos₁ pos₂) :
pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize := by
rw [show pat.utf8ByteSize = pat.toSlice.utf8ByteSize from utf8ByteSize_toSlice.symm]
exact ForwardSliceSearcher.offset_of_isLongestRevMatchAt (by simpa)
exact ForwardSliceSearcher.offset_of_isLongestRevMatchAt (toSlice_isEmpty h)
(isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice.1 h')
theorem matchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} :
theorem matchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} (h : pat "") :
MatchesAt pat pos t₁ t₂, pos.Splits t₁ (pat ++ t₂) := by
rw [matchesAt_iff_toSlice,
ForwardSliceSearcher.matchesAt_iff_splits]
ForwardSliceSearcher.matchesAt_iff_splits (toSlice_isEmpty h)]
simp
theorem revMatchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} :
theorem revMatchesAt_iff_splits {pat : String} {s : Slice} {pos : s.Pos} (h : pat "") :
RevMatchesAt pat pos t₁ t₂, pos.Splits (t₁ ++ pat) t₂ := by
rw [revMatchesAt_iff_toSlice,
ForwardSliceSearcher.revMatchesAt_iff_splits]
ForwardSliceSearcher.revMatchesAt_iff_splits (toSlice_isEmpty h)]
simp
theorem exists_matchesAt_iff_eq_append {pat : String} {s : Slice} :
theorem exists_matchesAt_iff_eq_append {pat : String} {s : Slice} (h : pat "") :
( (pos : s.Pos), MatchesAt pat pos) t₁ t₂, s.copy = t₁ ++ pat ++ t₂ := by
simp only [matchesAt_iff_splits]
simp only [matchesAt_iff_splits h]
constructor
· rintro pos, t₁, t₂, hsplit
exact t₁, t₂, by rw [hsplit.eq_append, append_assoc]
@@ -477,12 +385,12 @@ theorem exists_matchesAt_iff_eq_append {pat : String} {s : Slice} :
t₁, pat ++ t₂, by rw [ append_assoc]; exact heq, rfl
exact s.pos _ hvalid, t₁, t₂, by rw [ append_assoc]; exact heq, by simp
theorem exists_revMatchesAt_iff_eq_append {pat : String} {s : Slice} :
theorem exists_revMatchesAt_iff_eq_append {pat : String} {s : Slice} (h : pat "") :
( (pos : s.Pos), RevMatchesAt pat pos) t₁ t₂, s.copy = t₁ ++ pat ++ t₂ := by
rw [show ( (pos : s.Pos), RevMatchesAt (ρ := String) pat pos)
( (pos : s.Pos), RevMatchesAt (ρ := Slice) pat.toSlice pos) from by
simp [revMatchesAt_iff_toSlice],
ForwardSliceSearcher.exists_revMatchesAt_iff_eq_append]
ForwardSliceSearcher.exists_revMatchesAt_iff_eq_append (toSlice_isEmpty h)]
simp
theorem matchesAt_iff_isLongestMatchAt {pat : String} {s : Slice} {pos : s.Pos}
@@ -490,7 +398,7 @@ theorem matchesAt_iff_isLongestMatchAt {pat : String} {s : Slice} {pos : s.Pos}
MatchesAt pat pos (h : (pos.offset.increaseBy pat.utf8ByteSize).IsValidForSlice s),
IsLongestMatchAt pat pos (s.pos _ h) := by
have key := ForwardSliceSearcher.matchesAt_iff_isLongestMatchAt (pat := pat.toSlice)
(by simpa) (pos := pos)
(toSlice_isEmpty h) (pos := pos)
simp only [utf8ByteSize_toSlice, isLongestMatchAt_iff_isLongestMatchAt_toSlice] at key
rwa [matchesAt_iff_toSlice]
@@ -500,7 +408,7 @@ theorem revMatchesAt_iff_isLongestRevMatchAt {pat : String} {s : Slice} {pos : s
(h : (pos.offset.decreaseBy pat.utf8ByteSize).IsValidForSlice s),
IsLongestRevMatchAt pat (s.pos _ h) pos := by
have key := ForwardSliceSearcher.revMatchesAt_iff_isLongestRevMatchAt (pat := pat.toSlice)
(by simpa) (pos := pos)
(toSlice_isEmpty h) (pos := pos)
simp only [utf8ByteSize_toSlice, isLongestRevMatchAt_iff_isLongestRevMatchAt_toSlice] at key
rwa [revMatchesAt_iff_toSlice]
@@ -510,14 +418,14 @@ theorem matchesAt_iff_getElem {pat : String} {s : Slice} {pos : s.Pos} (h : pat
(j), (hj : j < pat.toByteArray.size)
pat.toByteArray[j] = s.copy.toByteArray[pos.offset.byteIdx + j] := by
have key := ForwardSliceSearcher.matchesAt_iff_getElem (pat := pat.toSlice)
(by simpa) (pos := pos)
(toSlice_isEmpty h) (pos := pos)
simp only [copy_toSlice] at key
rwa [matchesAt_iff_toSlice]
theorem le_of_matchesAt {pat : String} {s : Slice} {pos : s.Pos} (h : pat "")
(h' : MatchesAt pat pos) : pos.offset.increaseBy pat.utf8ByteSize s.rawEndPos := by
rw [show pat.utf8ByteSize = pat.toSlice.utf8ByteSize from utf8ByteSize_toSlice.symm]
exact ForwardSliceSearcher.le_of_matchesAt (by simpa)
exact ForwardSliceSearcher.le_of_matchesAt (toSlice_isEmpty h)
(matchesAt_iff_toSlice.1 h')
theorem matchesAt_iff_matchesAt_toSlice {pat : String} {s : Slice}

View File

@@ -56,7 +56,7 @@ theorem skipPrefix?_eq_some_iff {pat s : Slice} {pos : s.Pos} :
simp only [reduceCtorEq, false_iff]
intro heq
have := h (s.sliceFrom pos).copy
simp [ heq, -sliceTo_append_sliceFrom, pos.splits.eq_append] at this
simp [ heq, pos.splits.eq_append] at this
theorem isSome_skipPrefix? {pat s : Slice} : (skipPrefix? pat s).isSome = startsWith pat s := by
fun_cases skipPrefix? <;> simp_all
@@ -76,11 +76,14 @@ namespace Model.ForwardSliceSearcher
open Pattern.ForwardSliceSearcher
public instance {pat : Slice} : LawfulForwardPatternModel pat where
public instance {pat : Slice} : LawfulForwardPattern pat where
skipPrefixOfNonempty?_eq _ := rfl
startsWith_eq _ := isSome_skipPrefix?.symm
public theorem lawfulForwardPatternModel {pat : Slice} (hpat : pat.isEmpty = false) :
LawfulForwardPatternModel pat where
skipPrefix?_eq_some_iff pos := by
simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff]
simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff hpat]
end Model.ForwardSliceSearcher
@@ -88,11 +91,14 @@ namespace Model.ForwardStringSearcher
open Pattern.ForwardSliceSearcher
public instance {pat : String} : LawfulForwardPatternModel pat where
public instance {pat : String} : LawfulForwardPattern pat where
skipPrefixOfNonempty?_eq _ := rfl
startsWith_eq _ := isSome_skipPrefix?.symm
public theorem lawfulForwardPatternModel {pat : String} (hpat : pat "") :
LawfulForwardPatternModel pat where
skipPrefix?_eq_some_iff pos := by
simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff]
simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff hpat]
end Model.ForwardStringSearcher
@@ -147,7 +153,7 @@ theorem skipSuffix?_eq_some_iff {pat s : Slice} {pos : s.Pos} :
simp only [reduceCtorEq, false_iff]
intro heq
have := h (s.sliceTo pos).copy
simp [ heq, -sliceTo_append_sliceFrom, pos.splits.eq_append] at this
simp [ heq, pos.splits.eq_append] at this
theorem isSome_skipSuffix? {pat s : Slice} : (skipSuffix? pat s).isSome = endsWith pat s := by
fun_cases skipSuffix? <;> simp_all
@@ -167,12 +173,15 @@ namespace Model.BackwardSliceSearcher
open Pattern.BackwardSliceSearcher
public instance {pat : Slice} : LawfulBackwardPatternModel pat where
public instance {pat : Slice} : LawfulBackwardPattern pat where
skipSuffixOfNonempty?_eq _ := rfl
endsWith_eq _ := isSome_skipSuffix?.symm
public theorem lawfulBackwardPatternModel {pat : Slice} (hpat : pat.isEmpty = false) :
LawfulBackwardPatternModel pat where
skipSuffix?_eq_some_iff pos := by
simp [BackwardPattern.skipSuffix?, skipSuffix?_eq_some_iff,
ForwardSliceSearcher.isLongestRevMatch_iff]
ForwardSliceSearcher.isLongestRevMatch_iff hpat]
end Model.BackwardSliceSearcher
@@ -180,12 +189,15 @@ namespace Model.BackwardStringSearcher
open Pattern.BackwardSliceSearcher
public instance {pat : String} : LawfulBackwardPatternModel pat where
public instance {pat : String} : LawfulBackwardPattern pat where
skipSuffixOfNonempty?_eq _ := rfl
endsWith_eq _ := isSome_skipSuffix?.symm
public theorem lawfulBackwardPatternModel {pat : String} (hpat : pat "") :
LawfulBackwardPatternModel pat where
skipSuffix?_eq_some_iff pos := by
simp [BackwardPattern.skipSuffix?, skipSuffix?_eq_some_iff,
ForwardStringSearcher.isLongestRevMatch_iff]
ForwardStringSearcher.isLongestRevMatch_iff hpat]
end Model.BackwardStringSearcher
@@ -207,22 +219,19 @@ public theorem Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice
{pat : String} {s : Slice} :
skipPrefix? pat s = skipPrefix? pat.toSlice s := (rfl)
public theorem Pos.skip?_string_eq_skip?_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
pos.skip? pat = pos.skip? pat.toSlice := (rfl)
public theorem Pos.skipWhile_string_eq_skipWhile_toSlice {pat : String} {s : Slice}
(curr : s.Pos) :
Pos.skipWhile curr pat = Pos.skipWhile curr pat.toSlice := by
fun_induction Pos.skipWhile curr pat with
| case1 pos nextCurr h₁ h₂ ih =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_string_eq_skip?_toSlice, h₁, h₂, ih]
simp [ Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h₁, h₂, ih]
| case2 pos nextCurr h ih =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_string_eq_skip?_toSlice, h, ih]
simp [ Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h, ih]
| case3 pos h =>
conv => rhs; rw [Pos.skipWhile]
simp [ Pos.skip?_string_eq_skip?_toSlice, h]
simp [ Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice]
public theorem skipPrefixWhile_string_eq_skipPrefixWhile_toSlice {pat : String} {s : Slice} :
s.skipPrefixWhile pat = s.skipPrefixWhile pat.toSlice :=
@@ -238,7 +247,7 @@ public theorem takeWhile_string_eq_takeWhile_toSlice {pat : String} {s : Slice}
public theorem all_string_eq_all_toSlice {pat : String} {s : Slice} :
s.all pat = s.all pat.toSlice := by
simp only [all, skipPrefixWhile_string_eq_skipPrefixWhile_toSlice]
simp only [all, dropWhile_string_eq_dropWhile_toSlice]
public theorem endsWith_string_eq_endsWith_toSlice {pat : String} {s : Slice} :
s.endsWith pat = s.endsWith pat.toSlice := (rfl)
@@ -256,22 +265,19 @@ public theorem Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice
{pat : String} {s : Slice} :
skipSuffix? pat s = skipSuffix? pat.toSlice s := (rfl)
public theorem Pos.revSkip?_string_eq_revSkip?_toSlice {pat : String} {s : Slice} {pos : s.Pos} :
pos.revSkip? pat = pos.revSkip? pat.toSlice := (rfl)
public theorem Pos.revSkipWhile_string_eq_revSkipWhile_toSlice {pat : String} {s : Slice}
(curr : s.Pos) :
Pos.revSkipWhile curr pat = Pos.revSkipWhile curr pat.toSlice := by
fun_induction Pos.revSkipWhile curr pat with
| case1 pos nextCurr h₁ h₂ ih =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_string_eq_revSkip?_toSlice, h₁, h₂, ih]
simp [ Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice, h₁, h₂, ih]
| case2 pos nextCurr h ih =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_string_eq_revSkip?_toSlice, h, ih]
simp [ Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice, h, ih]
| case3 pos h =>
conv => rhs; rw [Pos.revSkipWhile]
simp [ Pos.revSkip?_string_eq_revSkip?_toSlice, h]
simp [ Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice]
public theorem skipSuffixWhile_string_eq_skipSuffixWhile_toSlice {pat : String} {s : Slice} :
s.skipSuffixWhile pat = s.skipSuffixWhile pat.toSlice :=
@@ -285,8 +291,4 @@ public theorem takeEndWhile_string_eq_takeEndWhile_toSlice {pat : String} {s : S
s.takeEndWhile pat = s.takeEndWhile pat.toSlice := by
simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_string_eq_skipSuffixWhile_toSlice
public theorem revAll_string_eq_revAll_toSlice {pat : String} {s : Slice} :
s.revAll pat = s.revAll pat.toSlice := by
simp [revAll, skipSuffixWhile_string_eq_skipSuffixWhile_toSlice]
end String.Slice

File diff suppressed because it is too large Load Diff

View File

@@ -56,77 +56,6 @@ theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s res : Slice} (h : s.
s.copy = singleton c ++ res.copy := by
simpa [PatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
theorem Pos.skip?_char_eq_some_iff {c : Char} {s : Slice} {pos res : s.Pos} :
pos.skip? c = some res h, res = pos.next h pos.get h = c := by
simp [Pattern.Model.Pos.skip?_eq_some_iff, Char.isLongestMatchAt_iff]
@[simp]
theorem Pos.skip?_char_eq_none_iff {c : Char} {s : Slice} {pos : s.Pos} :
pos.skip? c = none h, pos.get h c := by
simp [Pattern.Model.Pos.skip?_eq_none_iff, Char.matchesAt_iff]
theorem Pos.get_skipWhile_char_ne {c : Char} {s : Slice} {pos : s.Pos} {h} :
(pos.skipWhile c).get h c := by
have := Pattern.Model.Pos.not_matchesAt_skipWhile c pos
simp_all [Char.matchesAt_iff]
theorem Pos.skipWhile_char_eq_self_iff_get {c : Char} {s : Slice} {pos : s.Pos} :
pos.skipWhile c = pos h, pos.get h c := by
simp [Pattern.Model.Pos.skipWhile_eq_self_iff, Char.matchesAt_iff]
theorem Pos.get_eq_of_lt_skipWhile_char {c : Char} {s : Slice} {pos pos' : s.Pos}
(h₁ : pos pos') (h₂ : pos' < pos.skipWhile c) : pos'.get (ne_endPos_of_lt h₂) = c :=
(Char.isLongestMatchAtChain_iff.1 (Pattern.Model.Pos.isLongestMatchAtChain_skipWhile c pos)).2 _ h₁ h₂
theorem get_skipPrefixWhile_char_ne {c : Char} {s : Slice} {h} :
(s.skipPrefixWhile c).get h c := by
simp [skipPrefixWhile_eq_skipWhile_startPos, Pos.get_skipWhile_char_ne]
theorem get_eq_of_lt_skipPrefixWhile_char {c : Char} {s : Slice} {pos : s.Pos} (h : pos < s.skipPrefixWhile c) :
pos.get (Pos.ne_endPos_of_lt h) = c :=
Pos.get_eq_of_lt_skipWhile_char (Pos.startPos_le _) (by rwa [skipPrefixWhile_eq_skipWhile_startPos] at h)
@[simp]
theorem all_char_iff {c : Char} {s : Slice} : s.all c s.copy.toList = List.replicate s.copy.length c := by
rw [Bool.eq_iff_iff]
simp [Pattern.Model.all_eq_true_iff, Char.isLongestMatchAtChain_startPos_endPos_iff_toList]
theorem Pos.revSkip?_char_eq_some_iff {c : Char} {s : Slice} {pos res : s.Pos} :
pos.revSkip? c = some res h, res = pos.prev h (pos.prev h).get (by simp) = c := by
simp [Pattern.Model.Pos.revSkip?_eq_some_iff, Char.isLongestRevMatchAt_iff]
@[simp]
theorem Pos.revSkip?_char_eq_none_iff {c : Char} {s : Slice} {pos : s.Pos} :
pos.revSkip? c = none h, (pos.prev h).get (by simp) c := by
simp [Pattern.Model.Pos.revSkip?_eq_none_iff, Char.revMatchesAt_iff]
theorem Pos.get_revSkipWhile_char_ne {c : Char} {s : Slice} {pos : s.Pos} {h} :
((pos.revSkipWhile c).prev h).get (by simp) c := by
have := Pattern.Model.Pos.not_revMatchesAt_revSkipWhile c pos
simp_all [Char.revMatchesAt_iff]
theorem Pos.revSkipWhile_char_eq_self_iff_get {c : Char} {s : Slice} {pos : s.Pos} :
pos.revSkipWhile c = pos h, (pos.prev h).get (by simp) c := by
simp [Pattern.Model.Pos.revSkipWhile_eq_self_iff, Char.revMatchesAt_iff]
theorem Pos.get_eq_of_revSkipWhile_le_char {c : Char} {s : Slice} {pos pos' : s.Pos}
(h₁ : pos' < pos) (h₂ : pos.revSkipWhile c pos') : pos'.get (Pos.ne_endPos_of_lt h₁) = c :=
(Char.isLongestRevMatchAtChain_iff.1 (Pattern.Model.Pos.isLongestRevMatchAtChain_revSkipWhile c pos)).2 _ h₂ h₁
theorem get_skipSuffixWhile_char_ne {c : Char} {s : Slice} {h} :
((s.skipSuffixWhile c).prev h).get (by simp) c := by
simp [skipSuffixWhile_eq_revSkipWhile_endPos, Pos.get_revSkipWhile_char_ne]
theorem get_eq_of_skipSuffixWhile_le_char {c : Char} {s : Slice} {pos : s.Pos}
(h : s.skipSuffixWhile c pos) (h' : pos < s.endPos) :
pos.get (Pos.ne_endPos_of_lt h') = c :=
Pos.get_eq_of_revSkipWhile_le_char h' (by rwa [skipSuffixWhile_eq_revSkipWhile_endPos] at h)
@[simp]
theorem revAll_char_iff {c : Char} {s : Slice} : s.revAll c s.copy.toList = List.replicate s.copy.length c := by
rw [Bool.eq_iff_iff]
simp [Pattern.Model.revAll_eq_true_iff, Char.isLongestRevMatchAtChain_startPos_endPos_iff_toList]
theorem skipSuffix?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} :
s.skipSuffix? c = some pos h, pos = s.endPos.prev h (s.endPos.prev h).get (by simp) = c := by
rw [Pattern.Model.skipSuffix?_eq_some_iff, Char.isLongestRevMatch_iff]
@@ -171,19 +100,19 @@ theorem skipPrefix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} :
theorem startsWith_char_iff_get {c : Char} {s : String} :
s.startsWith c h, s.startPos.get h = c := by
simp [ startsWith_toSlice, Slice.startsWith_char_iff_get]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_iff_get]
theorem startsWith_char_eq_false_iff_get {c : Char} {s : String} :
s.startsWith c = false h, s.startPos.get h c := by
simp [ startsWith_toSlice, Slice.startsWith_char_eq_false_iff_get]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_eq_false_iff_get]
theorem startsWith_char_eq_head? {c : Char} {s : String} :
s.startsWith c = (s.toList.head? == some c) := by
simp [ startsWith_toSlice, Slice.startsWith_char_eq_head?]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_eq_head?]
theorem startsWith_char_iff_exists_append {c : Char} {s : String} :
s.startsWith c t, s = singleton c ++ t := by
simp [ startsWith_toSlice, Slice.startsWith_char_iff_exists_append]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_iff_exists_append]
theorem startsWith_char_eq_false_iff_forall_append {c : Char} {s : String} :
s.startsWith c = false t, s singleton c ++ t := by
@@ -201,19 +130,19 @@ theorem skipSuffix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} :
theorem endsWith_char_iff_get {c : Char} {s : String} :
s.endsWith c h, (s.endPos.prev h).get (by simp) = c := by
simp [ endsWith_toSlice, Slice.endsWith_char_iff_get, Pos.prev_toSlice]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_char_iff_get, Pos.prev_toSlice]
theorem endsWith_char_eq_false_iff_get {c : Char} {s : String} :
s.endsWith c = false h, (s.endPos.prev h).get (by simp) c := by
simp [ endsWith_toSlice, Slice.endsWith_char_eq_false_iff_get, Pos.prev_toSlice]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_char_eq_false_iff_get, Pos.prev_toSlice]
theorem endsWith_char_eq_getLast? {c : Char} {s : String} :
s.endsWith c = (s.toList.getLast? == some c) := by
simp [ endsWith_toSlice, Slice.endsWith_char_eq_getLast?]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_char_eq_getLast?]
theorem endsWith_char_iff_exists_append {c : Char} {s : String} :
s.endsWith c t, s = t ++ singleton c := by
simp [ endsWith_toSlice, Slice.endsWith_char_iff_exists_append]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_char_iff_exists_append]
theorem endsWith_char_eq_false_iff_forall_append {c : Char} {s : String} :
s.endsWith c = false t, s t ++ singleton c := by

View File

@@ -8,16 +8,11 @@ module
prelude
public import Init.Data.String.Slice
public import Init.Data.String.TakeDrop
public import Init.Data.String.Lemmas.Order
import Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
import Init.Data.String.Lemmas.Pattern.Pred
import Init.Data.Option.Lemmas
import Init.Data.String.Lemmas.FindPos
import Init.Data.String.Lemmas.Intercalate
import Init.ByCases
import Init.Data.Order.Lemmas
import Init.Data.String.OrderInstances
import Init.Data.String.Lemmas.Basic
public section
@@ -54,80 +49,6 @@ theorem eq_append_of_dropPrefix?_bool_eq_some {p : Char → Bool} {s res : Slice
obtain _, c, rfl, h₁, h₂ := by simpa [PatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
exact _, h₂, h₁
@[simp]
theorem Pos.skip?_bool_eq_some_iff {p : Char Bool} {s : Slice} {pos res : s.Pos} :
pos.skip? p = some res h, res = pos.next h p (pos.get h) := by
simp [Pattern.Model.Pos.skip?_eq_some_iff, CharPred.isLongestMatchAt_iff]
@[simp]
theorem Pos.skip?_bool_eq_none_iff {p : Char Bool} {s : Slice} {pos : s.Pos} :
pos.skip? p = none h, p (pos.get h) = false := by
simp [Pattern.Model.Pos.skip?_eq_none_iff, CharPred.matchesAt_iff]
theorem Pos.apply_skipWhile_bool_eq_false {p : Char Bool} {s : Slice} {pos : s.Pos} {h} :
p ((pos.skipWhile p).get h) = false := by
have := Pattern.Model.Pos.not_matchesAt_skipWhile p pos
simp_all [CharPred.matchesAt_iff]
theorem Pos.skipWhile_bool_eq_self_iff_get {p : Char Bool} {s : Slice} {pos : s.Pos} :
pos.skipWhile p = pos h, p (pos.get h) = false := by
simp [Pattern.Model.Pos.skipWhile_eq_self_iff, CharPred.matchesAt_iff]
theorem Pos.apply_eq_true_of_lt_skipWhile_bool {p : Char Bool} {s : Slice} {pos pos' : s.Pos}
(h₁ : pos pos') (h₂ : pos' < pos.skipWhile p) : p (pos'.get (ne_endPos_of_lt h₂)) = true :=
(CharPred.isLongestMatchAtChain_iff.1 (Pattern.Model.Pos.isLongestMatchAtChain_skipWhile p pos)).2 _ h₁ h₂
theorem apply_skipPrefixWhile_bool_eq_false {p : Char Bool} {s : Slice} {h} :
p ((s.skipPrefixWhile p).get h) = false := by
simp [skipPrefixWhile_eq_skipWhile_startPos, Pos.apply_skipWhile_bool_eq_false]
theorem apply_eq_true_of_lt_skipPrefixWhile_bool {p : Char Bool} {s : Slice} {pos : s.Pos} (h : pos < s.skipPrefixWhile p) :
p (pos.get (Pos.ne_endPos_of_lt h)) = true :=
Pos.apply_eq_true_of_lt_skipWhile_bool (Pos.startPos_le _) (skipPrefixWhile_eq_skipWhile_startPos h)
@[simp]
theorem all_bool_eq {p : Char Bool} {s : Slice} : s.all p = s.copy.toList.all p := by
rw [Bool.eq_iff_iff, Pattern.Model.all_eq_true_iff,
CharPred.isLongestMatchAtChain_startPos_endPos_iff_toList, List.all_eq_true]
@[simp]
theorem Pos.skip?_prop_eq_some_iff {P : Char Prop} [DecidablePred P] {s : Slice} {pos res : s.Pos} :
pos.skip? P = some res h, res = pos.next h P (pos.get h) := by
simp [Pos.skip?_prop_eq_skip?_decide, skip?_bool_eq_some_iff]
@[simp]
theorem Pos.skip?_prop_eq_none_iff {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
pos.skip? P = none h, ¬ P (pos.get h) := by
simp [Pos.skip?_prop_eq_skip?_decide, skip?_bool_eq_none_iff]
theorem Pos.apply_skipWhile_prop {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} {h} :
¬ P ((pos.skipWhile P).get h) := by
have := Pattern.Model.Pos.not_matchesAt_skipWhile P pos
simp_all [CharPred.Decidable.matchesAt_iff]
theorem Pos.skipWhile_prop_eq_self_iff_get {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
pos.skipWhile P = pos h, ¬ P (pos.get h) := by
simp [Pos.skipWhile_prop_eq_skipWhile_decide, skipWhile_bool_eq_self_iff_get]
theorem Pos.apply_of_lt_skipWhile_prop {P : Char Prop} [DecidablePred P] {s : Slice} {pos pos' : s.Pos}
(h₁ : pos pos') (h₂ : pos' < pos.skipWhile P) : P (pos'.get (ne_endPos_of_lt h₂)) := by
simp [Pos.skipWhile_prop_eq_skipWhile_decide] at h₂
simpa using apply_eq_true_of_lt_skipWhile_bool h₁ h₂
theorem apply_skipPrefixWhile_prop {P : Char Prop} [DecidablePred P] {s : Slice} {h} :
¬ P ((s.skipPrefixWhile P).get h) := by
simp [skipPrefixWhile_eq_skipWhile_startPos, Pos.apply_skipWhile_prop]
theorem apply_of_lt_skipPrefixWhile_prop {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos}
(h : pos < s.skipPrefixWhile P) : P (pos.get (Pos.ne_endPos_of_lt h)) := by
simp [skipPrefixWhile_prop_eq_skipPrefixWhile_decide] at h
simpa using apply_eq_true_of_lt_skipPrefixWhile_bool h
@[simp]
theorem all_prop_eq {P : Char Prop} [DecidablePred P] {s : Slice} :
s.all P = s.copy.toList.all (decide <| P ·) := by
simp [all_prop_eq_all_decide]
theorem skipPrefix?_prop_eq_some_iff {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
s.skipPrefix? P = some pos h, pos = s.startPos.next h P (s.startPos.get h) := by
simp [skipPrefix?_prop_eq_skipPrefix?_decide, skipPrefix?_bool_eq_some_iff]
@@ -197,83 +118,6 @@ theorem eq_append_of_dropSuffix?_prop_eq_some {P : Char → Prop} [DecidablePred
rw [dropSuffix?_prop_eq_dropSuffix?_decide] at h
simpa using eq_append_of_dropSuffix?_bool_eq_some h
@[simp]
theorem Pos.revSkip?_bool_eq_some_iff {p : Char Bool} {s : Slice} {pos res : s.Pos} :
pos.revSkip? p = some res h, res = pos.prev h p ((pos.prev h).get (by simp)) := by
simp [Pattern.Model.Pos.revSkip?_eq_some_iff, CharPred.isLongestRevMatchAt_iff]
@[simp]
theorem Pos.revSkip?_bool_eq_none_iff {p : Char Bool} {s : Slice} {pos : s.Pos} :
pos.revSkip? p = none h, p ((pos.prev h).get (by simp)) = false := by
simp [Pattern.Model.Pos.revSkip?_eq_none_iff, CharPred.revMatchesAt_iff]
theorem Pos.apply_revSkipWhile_bool_eq_false {p : Char Bool} {s : Slice} {pos : s.Pos} {h} :
p (((pos.revSkipWhile p).prev h).get (by simp)) = false := by
have := Pattern.Model.Pos.not_revMatchesAt_revSkipWhile p pos
simp_all [CharPred.revMatchesAt_iff]
theorem Pos.revSkipWhile_bool_eq_self_iff_get {p : Char Bool} {s : Slice} {pos : s.Pos} :
pos.revSkipWhile p = pos h, p ((pos.prev h).get (by simp)) = false := by
simp [Pattern.Model.Pos.revSkipWhile_eq_self_iff, CharPred.revMatchesAt_iff]
theorem Pos.apply_eq_true_of_revSkipWhile_le_bool {p : Char Bool} {s : Slice} {pos pos' : s.Pos}
(h₁ : pos' < pos) (h₂ : pos.revSkipWhile p pos') : p (pos'.get (Pos.ne_endPos_of_lt h₁)) = true :=
(CharPred.isLongestRevMatchAtChain_iff.1 (Pattern.Model.Pos.isLongestRevMatchAtChain_revSkipWhile p pos)).2 _ h₂ h₁
theorem apply_skipSuffixWhile_bool_eq_false {p : Char Bool} {s : Slice} {h} :
p (((s.skipSuffixWhile p).prev h).get (by simp)) = false := by
simp [skipSuffixWhile_eq_revSkipWhile_endPos, Pos.apply_revSkipWhile_bool_eq_false]
theorem apply_eq_true_of_skipSuffixWhile_le_bool {p : Char Bool} {s : Slice} {pos : s.Pos}
(h : s.skipSuffixWhile p pos) (h' : pos < s.endPos) :
p (pos.get (Pos.ne_endPos_of_lt h')) = true :=
Pos.apply_eq_true_of_revSkipWhile_le_bool h' (skipSuffixWhile_eq_revSkipWhile_endPos h)
@[simp]
theorem revAll_bool_eq {p : Char Bool} {s : Slice} : s.revAll p = s.copy.toList.all p := by
rw [Bool.eq_iff_iff, Pattern.Model.revAll_eq_true_iff,
CharPred.isLongestRevMatchAtChain_startPos_endPos_iff_toList, List.all_eq_true]
@[simp]
theorem Pos.revSkip?_prop_eq_some_iff {P : Char Prop} [DecidablePred P] {s : Slice} {pos res : s.Pos} :
pos.revSkip? P = some res h, res = pos.prev h P ((pos.prev h).get (by simp)) := by
simp [Pos.revSkip?_prop_eq_revSkip?_decide, revSkip?_bool_eq_some_iff]
@[simp]
theorem Pos.revSkip?_prop_eq_none_iff {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
pos.revSkip? P = none h, ¬ P ((pos.prev h).get (by simp)) := by
simp [Pos.revSkip?_prop_eq_revSkip?_decide, revSkip?_bool_eq_none_iff]
theorem Pos.apply_revSkipWhile_prop {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} {h} :
¬ P (((pos.revSkipWhile P).prev h).get (by simp)) := by
have := Pattern.Model.Pos.not_revMatchesAt_revSkipWhile P pos
simp_all [CharPred.Decidable.revMatchesAt_iff]
theorem Pos.revSkipWhile_prop_eq_self_iff_get {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
pos.revSkipWhile P = pos h, ¬ P ((pos.prev h).get (by simp)) := by
simp [Pos.revSkipWhile_prop_eq_revSkipWhile_decide, revSkipWhile_bool_eq_self_iff_get]
theorem Pos.apply_of_revSkipWhile_le_prop {P : Char Prop} [DecidablePred P] {s : Slice} {pos pos' : s.Pos}
(h₁ : pos' < pos) (h₂ : pos.revSkipWhile P pos') : P (pos'.get (Pos.ne_endPos_of_lt h₁)) := by
have h₂' : pos.revSkipWhile (decide <| P ·) pos' :=
Pos.revSkipWhile_prop_eq_revSkipWhile_decide (p := P) pos h₂
simpa using Pos.apply_eq_true_of_revSkipWhile_le_bool h₁ h₂'
theorem apply_skipSuffixWhile_prop {P : Char Prop} [DecidablePred P] {s : Slice} {h} :
¬ P (((s.skipSuffixWhile P).prev h).get (by simp)) := by
have := Pattern.Model.Pos.not_revMatchesAt_revSkipWhile P s.endPos
simp_all [CharPred.Decidable.revMatchesAt_iff, skipSuffixWhile_eq_revSkipWhile_endPos]
theorem apply_of_skipSuffixWhile_le_prop {P : Char Prop} [DecidablePred P] {s : Slice} {pos : s.Pos}
(h : s.skipSuffixWhile P pos) (h' : pos < s.endPos) :
P (pos.get (Pos.ne_endPos_of_lt h')) :=
Pos.apply_of_revSkipWhile_le_prop h' (skipSuffixWhile_eq_revSkipWhile_endPos (pat := P) h)
@[simp]
theorem revAll_prop_eq {P : Char Prop} [DecidablePred P] {s : Slice} :
s.revAll P = s.copy.toList.all (decide <| P ·) := by
simp [revAll_prop_eq_revAll_decide, revAll_bool_eq]
end Slice
theorem skipPrefix?_bool_eq_some_iff {p : Char Bool} {s : String} {pos : s.Pos} :
@@ -283,58 +127,21 @@ theorem skipPrefix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.P
theorem startsWith_bool_iff_get {p : Char Bool} {s : String} :
s.startsWith p h, p (s.startPos.get h) = true := by
simp [ startsWith_toSlice, Slice.startsWith_bool_iff_get]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_bool_iff_get]
theorem startsWith_bool_eq_false_iff_get {p : Char Bool} {s : String} :
s.startsWith p = false h, p (s.startPos.get h) = false := by
simp [ startsWith_toSlice, Slice.startsWith_bool_eq_false_iff_get]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_bool_eq_false_iff_get]
theorem startsWith_bool_eq_head? {p : Char Bool} {s : String} :
s.startsWith p = s.toList.head?.any p := by
simp [ startsWith_toSlice, Slice.startsWith_bool_eq_head?]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_bool_eq_head?]
theorem eq_append_of_dropPrefix?_bool_eq_some {p : Char Bool} {s : String} {res : Slice} (h : s.dropPrefix? p = some res) :
c, s = singleton c ++ res.copy p c = true := by
rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
simpa using Slice.eq_append_of_dropPrefix?_bool_eq_some h
@[simp]
theorem Pos.skip?_bool_eq_some_iff {p : Char Bool} {s : String} {pos res : s.Pos} :
pos.skip? p = some res h, res = pos.next h p (pos.get h) := by
simp [skip?_eq_skip?_toSlice, toSlice_inj, toSlice_next]
@[simp]
theorem Pos.skip?_bool_eq_none_iff {p : Char Bool} {s : String} {pos : s.Pos} :
pos.skip? p = none h, p (pos.get h) = false := by
simp [skip?_eq_skip?_toSlice]
theorem Pos.apply_skipWhile_bool_eq_false {p : Char Bool} {s : String} {pos : s.Pos} {h} :
p ((pos.skipWhile p).get h) = false := by
simp [skipWhile_eq_skipWhile_toSlice, Slice.Pos.apply_skipWhile_bool_eq_false]
theorem Pos.skipWhile_bool_eq_self_iff_get {p : Char Bool} {s : String} {pos : s.Pos} :
pos.skipWhile p = pos h, p (pos.get h) = false := by
simp [skipWhile_eq_skipWhile_toSlice, toSlice_inj, Slice.Pos.skipWhile_bool_eq_self_iff_get]
theorem Pos.apply_eq_true_of_lt_skipWhile_bool {p : Char Bool} {s : String} {pos pos' : s.Pos}
(h₁ : pos pos') (h₂ : pos' < pos.skipWhile p) : p (pos'.get (ne_endPos_of_lt h₂)) = true := by
rw [Pos.get_eq_get_toSlice]
exact Slice.Pos.apply_eq_true_of_lt_skipWhile_bool (toSlice_le_toSlice_iff.2 h₁)
(by simpa [skipWhile_eq_skipWhile_toSlice] using h₂)
theorem apply_skipPrefixWhile_bool_eq_false {p : Char Bool} {s : String} {h} :
p ((s.skipPrefixWhile p).get h) = false := by
simp [skipPrefixWhile_eq_skipPrefixWhile_toSlice, Slice.apply_skipPrefixWhile_bool_eq_false]
theorem apply_eq_true_of_lt_skipPrefixWhile_bool {p : Char Bool} {s : String} {pos : s.Pos} (h : pos < s.skipPrefixWhile p) :
p (pos.get (Pos.ne_endPos_of_lt h)) = true := by
rw [Pos.get_eq_get_toSlice]
exact Slice.apply_eq_true_of_lt_skipPrefixWhile_bool (by simpa [skipPrefixWhile_eq_skipPrefixWhile_toSlice] using h)
@[simp]
theorem all_bool_eq {p : Char Bool} {s : String} : s.all p = s.toList.all p := by
simp [ all_toSlice]
theorem skipPrefix?_prop_eq_some_iff {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos} :
s.skipPrefix? P = some pos h, pos = s.startPos.next h P (s.startPos.get h) := by
simp [skipPrefix?_eq_skipPrefix?_toSlice, Slice.skipPrefix?_prop_eq_some_iff, Pos.toSlice_inj,
@@ -342,15 +149,15 @@ theorem skipPrefix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s :
theorem startsWith_prop_iff_get {P : Char Prop} [DecidablePred P] {s : String} :
s.startsWith P h, P (s.startPos.get h) := by
simp [ startsWith_toSlice, Slice.startsWith_prop_iff_get]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_prop_iff_get]
theorem startsWith_prop_eq_false_iff_get {P : Char Prop} [DecidablePred P] {s : String} :
s.startsWith P = false h, ¬ P (s.startPos.get h) := by
simp [ startsWith_toSlice, Slice.startsWith_prop_eq_false_iff_get]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_prop_eq_false_iff_get]
theorem startsWith_prop_eq_head? {P : Char Prop} [DecidablePred P] {s : String} :
s.startsWith P = s.toList.head?.any (decide <| P ·) := by
simp [ startsWith_toSlice, Slice.startsWith_prop_eq_head?]
simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_prop_eq_head?]
theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char Prop} [DecidablePred P] {s : String} {res : Slice}
(h : s.dropPrefix? P = some res) : c, s = singleton c ++ res.copy P c := by
@@ -364,15 +171,15 @@ theorem skipSuffix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.P
theorem endsWith_bool_iff_get {p : Char Bool} {s : String} :
s.endsWith p h, p ((s.endPos.prev h).get (by simp)) = true := by
simp [ endsWith_toSlice, Slice.endsWith_bool_iff_get, Pos.prev_toSlice]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_bool_iff_get, Pos.prev_toSlice]
theorem endsWith_bool_eq_false_iff_get {p : Char Bool} {s : String} :
s.endsWith p = false h, p ((s.endPos.prev h).get (by simp)) = false := by
simp [ endsWith_toSlice, Slice.endsWith_bool_eq_false_iff_get, Pos.prev_toSlice]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_bool_eq_false_iff_get, Pos.prev_toSlice]
theorem endsWith_bool_eq_getLast? {p : Char Bool} {s : String} :
s.endsWith p = s.toList.getLast?.any p := by
simp [ endsWith_toSlice, Slice.endsWith_bool_eq_getLast?]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_bool_eq_getLast?]
theorem eq_append_of_dropSuffix?_bool_eq_some {p : Char Bool} {s : String} {res : Slice} (h : s.dropSuffix? p = some res) :
c, s = res.copy ++ singleton c p c = true := by
@@ -386,154 +193,19 @@ theorem skipSuffix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s :
theorem endsWith_prop_iff_get {P : Char Prop} [DecidablePred P] {s : String} :
s.endsWith P h, P ((s.endPos.prev h).get (by simp)) := by
simp [ endsWith_toSlice, Slice.endsWith_prop_iff_get, Pos.prev_toSlice]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_prop_iff_get, Pos.prev_toSlice]
theorem endsWith_prop_eq_false_iff_get {P : Char Prop} [DecidablePred P] {s : String} :
s.endsWith P = false h, ¬ P ((s.endPos.prev h).get (by simp)) := by
simp [ endsWith_toSlice, Slice.endsWith_prop_eq_false_iff_get, Pos.prev_toSlice]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_prop_eq_false_iff_get, Pos.prev_toSlice]
theorem endsWith_prop_eq_getLast? {P : Char Prop} [DecidablePred P] {s : String} :
s.endsWith P = s.toList.getLast?.any (decide <| P ·) := by
simp [ endsWith_toSlice, Slice.endsWith_prop_eq_getLast?]
simp [endsWith_eq_endsWith_toSlice, Slice.endsWith_prop_eq_getLast?]
theorem eq_append_of_dropSuffix?_prop_eq_some {P : Char Prop} [DecidablePred P] {s : String} {res : Slice}
(h : s.dropSuffix? P = some res) : c, s = res.copy ++ singleton c P c := by
rw [dropSuffix?_eq_dropSuffix?_toSlice] at h
simpa using Slice.eq_append_of_dropSuffix?_prop_eq_some h
@[simp]
theorem Pos.skip?_prop_eq_some_iff {P : Char Prop} [DecidablePred P] {s : String} {pos res : s.Pos} :
pos.skip? P = some res h, res = pos.next h P (pos.get h) := by
simp [skip?_eq_skip?_toSlice, toSlice_inj, toSlice_next]
@[simp]
theorem Pos.skip?_prop_eq_none_iff {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos} :
pos.skip? P = none h, ¬ P (pos.get h) := by
simp [skip?_eq_skip?_toSlice]
theorem Pos.apply_skipWhile_prop {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos} {h} :
¬ P ((pos.skipWhile P).get h) := by
simp [skipWhile_eq_skipWhile_toSlice, Slice.Pos.apply_skipWhile_prop]
theorem Pos.skipWhile_prop_eq_self_iff_get {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos} :
pos.skipWhile P = pos h, ¬ P (pos.get h) := by
simp [skipWhile_eq_skipWhile_toSlice, toSlice_inj, Slice.Pos.skipWhile_prop_eq_self_iff_get]
theorem Pos.apply_of_lt_skipWhile_prop {P : Char Prop} [DecidablePred P] {s : String} {pos pos' : s.Pos}
(h₁ : pos pos') (h₂ : pos' < pos.skipWhile P) : P (pos'.get (ne_endPos_of_lt h₂)) := by
rw [Pos.get_eq_get_toSlice]
exact Slice.Pos.apply_of_lt_skipWhile_prop (toSlice_le_toSlice_iff.2 h₁)
(by simpa [skipWhile_eq_skipWhile_toSlice] using h₂)
theorem apply_skipPrefixWhile_prop {P : Char Prop} [DecidablePred P] {s : String} {h} :
¬ P ((s.skipPrefixWhile P).get h) := by
simp [skipPrefixWhile_eq_skipPrefixWhile_toSlice, Slice.apply_skipPrefixWhile_prop]
theorem apply_of_lt_skipPrefixWhile_prop {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos}
(h : pos < s.skipPrefixWhile P) : P (pos.get (Pos.ne_endPos_of_lt h)) := by
rw [Pos.get_eq_get_toSlice]
exact Slice.apply_of_lt_skipPrefixWhile_prop (by simpa [skipPrefixWhile_eq_skipPrefixWhile_toSlice] using h)
@[simp]
theorem all_prop_eq {P : Char Prop} [DecidablePred P] {s : String} :
s.all P = s.toList.all (decide <| P ·) := by
simp [ all_toSlice]
@[simp]
theorem Pos.revSkip?_bool_eq_some_iff {p : Char Bool} {s : String} {pos res : s.Pos} :
pos.revSkip? p = some res h, res = pos.prev h p ((pos.prev h).get (by simp)) := by
simp [revSkip?_eq_revSkip?_toSlice, toSlice_inj, toSlice_prev, get_eq_get_toSlice]
@[simp]
theorem Pos.revSkip?_bool_eq_none_iff {p : Char Bool} {s : String} {pos : s.Pos} :
pos.revSkip? p = none h, p ((pos.prev h).get (by simp)) = false := by
simp [revSkip?_eq_revSkip?_toSlice, Pos.prev_toSlice]
theorem Pos.apply_revSkipWhile_bool_eq_false {p : Char Bool} {s : String} {pos : s.Pos} {h} :
p (((pos.revSkipWhile p).prev h).get (by simp)) = false := by
have h' : pos.toSlice.revSkipWhile p s.toSlice.startPos := by
simpa [Pos.revSkipWhile_eq_revSkipWhile_toSlice, toSlice_inj] using h
have := Slice.Pos.apply_revSkipWhile_bool_eq_false (pos := pos.toSlice) (h := h')
simpa [Pos.revSkipWhile_eq_revSkipWhile_toSlice, Pos.prev_ofToSlice]
theorem Pos.revSkipWhile_bool_eq_self_iff_get {p : Char Bool} {s : String} {pos : s.Pos} :
pos.revSkipWhile p = pos h, p ((pos.prev h).get (by simp)) = false := by
simp [Pos.revSkipWhile_eq_revSkipWhile_toSlice, toSlice_inj, Slice.Pos.revSkipWhile_bool_eq_self_iff_get,
Pos.prev_toSlice]
theorem Pos.apply_eq_true_of_revSkipWhile_le_bool {p : Char Bool} {s : String} {pos pos' : s.Pos}
(h₁ : pos' < pos) (h₂ : pos.revSkipWhile p pos') : p (pos'.get (ne_endPos_of_lt h₁)) = true := by
rw [Pos.get_eq_get_toSlice]
exact Slice.Pos.apply_eq_true_of_revSkipWhile_le_bool
(Pos.toSlice_lt_toSlice_iff.2 h₁)
(by simpa [Pos.revSkipWhile_eq_revSkipWhile_toSlice, Pos.ofToSlice_le_iff] using h₂)
theorem apply_skipSuffixWhile_bool_eq_false {p : Char Bool} {s : String} {h} :
p (((s.skipSuffixWhile p).prev h).get (by simp)) = false := by
have h' : s.toSlice.skipSuffixWhile p s.toSlice.startPos := by
simpa [skipSuffixWhile_eq_skipSuffixWhile_toSlice, Pos.toSlice_inj] using h
have := Slice.apply_skipSuffixWhile_bool_eq_false (s := s.toSlice) (h := h')
simpa [skipSuffixWhile_eq_skipSuffixWhile_toSlice, Pos.prev_ofToSlice]
theorem apply_eq_true_of_skipSuffixWhile_le_bool {p : Char Bool} {s : String} {pos : s.Pos}
(h : s.skipSuffixWhile p pos) (h' : pos < s.endPos) :
p (pos.get (Pos.ne_endPos_of_lt h')) = true := by
rw [Pos.get_eq_get_toSlice]
exact Slice.apply_eq_true_of_skipSuffixWhile_le_bool
(by simpa [skipSuffixWhile_eq_skipSuffixWhile_toSlice, Pos.ofToSlice_le_iff] using h)
(by simpa [Pos.toSlice_lt_toSlice_iff] using h')
@[simp]
theorem revAll_bool_eq {p : Char Bool} {s : String} : s.revAll p = s.toList.all p := by
simp [ revAll_toSlice]
@[simp]
theorem Pos.revSkip?_prop_eq_some_iff {P : Char Prop} [DecidablePred P] {s : String} {pos res : s.Pos} :
pos.revSkip? P = some res h, res = pos.prev h P ((pos.prev h).get (by simp)) := by
simp [revSkip?_eq_revSkip?_toSlice, toSlice_inj, toSlice_prev, get_eq_get_toSlice]
@[simp]
theorem Pos.revSkip?_prop_eq_none_iff {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos} :
pos.revSkip? P = none h, ¬ P ((pos.prev h).get (by simp)) := by
simp [revSkip?_eq_revSkip?_toSlice, Pos.prev_toSlice]
theorem Pos.apply_revSkipWhile_prop {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos} {h} :
¬ P (((pos.revSkipWhile P).prev h).get (by simp)) := by
have h' : pos.toSlice.revSkipWhile P s.toSlice.startPos := by
simpa [Pos.revSkipWhile_eq_revSkipWhile_toSlice, toSlice_inj] using h
have := Slice.Pos.apply_revSkipWhile_prop (pos := pos.toSlice) (h := h')
simpa [Pos.revSkipWhile_eq_revSkipWhile_toSlice, Pos.prev_ofToSlice]
theorem Pos.revSkipWhile_prop_eq_self_iff_get {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos} :
pos.revSkipWhile P = pos h, ¬ P ((pos.prev h).get (by simp)) := by
simp [Pos.revSkipWhile_eq_revSkipWhile_toSlice, toSlice_inj,
Slice.Pos.revSkipWhile_prop_eq_self_iff_get, Pos.prev_toSlice]
theorem Pos.apply_of_revSkipWhile_le_prop {P : Char Prop} [DecidablePred P] {s : String} {pos pos' : s.Pos}
(h₁ : pos' < pos) (h₂ : pos.revSkipWhile P pos') : P (pos'.get (ne_endPos_of_lt h₁)) := by
rw [Pos.get_eq_get_toSlice]
exact Slice.Pos.apply_of_revSkipWhile_le_prop
(Pos.toSlice_lt_toSlice_iff.2 h₁)
(by simpa [Pos.revSkipWhile_eq_revSkipWhile_toSlice, Pos.ofToSlice_le_iff] using h₂)
theorem apply_skipSuffixWhile_prop {P : Char Prop} [DecidablePred P] {s : String} {h} :
¬ P (((s.skipSuffixWhile P).prev h).get (by simp)) := by
have h' : s.toSlice.skipSuffixWhile P s.toSlice.startPos := by
simpa [skipSuffixWhile_eq_skipSuffixWhile_toSlice, Pos.toSlice_inj] using h
have := Slice.apply_skipSuffixWhile_prop (s := s.toSlice) (h := h')
simpa [skipSuffixWhile_eq_skipSuffixWhile_toSlice, Pos.prev_ofToSlice]
theorem apply_of_skipSuffixWhile_le_prop {P : Char Prop} [DecidablePred P] {s : String} {pos : s.Pos}
(h : s.skipSuffixWhile P pos) (h' : pos < s.endPos) :
P (pos.get (Pos.ne_endPos_of_lt h')) := by
rw [Pos.get_eq_get_toSlice]
exact Slice.apply_of_skipSuffixWhile_le_prop
(by simpa [skipSuffixWhile_eq_skipSuffixWhile_toSlice, Pos.ofToSlice_le_iff] using h)
(by simpa [Pos.toSlice_lt_toSlice_iff] using h')
@[simp]
theorem revAll_prop_eq {P : Char Prop} [DecidablePred P] {s : String} :
s.revAll P = s.toList.all (decide <| P ·) := by
simp [ revAll_toSlice]
end String

View File

@@ -30,7 +30,11 @@ theorem skipPrefix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true)
@[simp]
theorem skipPrefix?_slice_eq_some_iff {pat s : Slice} {pos : s.Pos} :
s.skipPrefix? pat = some pos t, pos.Splits pat.copy t := by
rw [Pattern.Model.skipPrefix?_eq_some_iff, ForwardSliceSearcher.isLongestMatch_iff_splits]
match h : pat.isEmpty with
| false =>
have := ForwardSliceSearcher.lawfulForwardPatternModel h
rw [Pattern.Model.skipPrefix?_eq_some_iff, ForwardSliceSearcher.isLongestMatch_iff_splits h]
| true => simp [skipPrefix?_slice_of_isEmpty h, (show pat.copy = "" by simpa), eq_comm]
theorem startsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
s.startsWith pat = true := by
@@ -39,10 +43,14 @@ theorem startsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true)
@[simp]
theorem startsWith_slice_iff {pat s : Slice} :
s.startsWith pat pat.copy.toList <+: s.copy.toList := by
simp only [Model.startsWith_iff, ForwardSliceSearcher.matchesAt_iff_splits,
splits_startPos_iff, exists_and_left, exists_eq_left]
simp only [ toList_inj, toList_append, List.prefix_iff_exists_append_eq]
exact fun t, ht => t.toList, by simp [ht], fun t, ht => String.ofList t, by simp [ ht]
match h : pat.isEmpty with
| false =>
have := ForwardSliceSearcher.lawfulForwardPatternModel h
simp only [Model.startsWith_iff, ForwardSliceSearcher.matchesAt_iff_splits h,
splits_startPos_iff, exists_and_left, exists_eq_left]
simp only [ toList_inj, toList_append, List.prefix_iff_exists_append_eq]
exact fun t, ht => t.toList, by simp [ht], fun t, ht => String.ofList t, by simp [ ht]
| true => simp [startsWith_slice_of_isEmpty h, (show pat.copy = "" by simpa)]
@[simp]
theorem startsWith_slice_eq_false_iff {pat s : Slice} :
@@ -55,18 +63,14 @@ theorem dropPrefix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true)
theorem eq_append_of_dropPrefix?_slice_eq_some {pat s res : Slice} (h : s.dropPrefix? pat = some res) :
s.copy = pat.copy ++ res.copy := by
have := Pattern.Model.eq_append_of_dropPrefix?_eq_some h
simp only [PatternModel.Matches] at this
obtain _, -, rfl, h := this
exact h
@[simp]
theorem all_slice_iff {pat s : Slice} : s.all pat n, s.copy = String.join (List.replicate n pat.copy) := by
simp [Pattern.Model.all_eq_true_iff, ForwardSliceSearcher.isLongestMatchAtChain_startPos_endPos_iff]
@[simp]
theorem revAll_slice_iff {pat s : Slice} : s.revAll pat n, s.copy = String.join (List.replicate n pat.copy) := by
simp [Pattern.Model.revAll_eq_true_iff, ForwardSliceSearcher.isLongestRevMatchAtChain_startPos_endPos_iff]
match hpat : pat.isEmpty with
| false =>
have := ForwardSliceSearcher.lawfulForwardPatternModel hpat
have := Pattern.Model.eq_append_of_dropPrefix?_eq_some h
simp only [PatternModel.Matches] at this
obtain _, -, rfl, h := this
exact h
| true => simp [Option.some.inj (h dropPrefix?_slice_of_isEmpty hpat), (show pat.copy = "" by simpa)]
@[simp]
theorem skipPrefix?_string_eq_some_iff {pat : String} {s : Slice} {pos : s.Pos} :
@@ -100,7 +104,6 @@ theorem eq_append_of_dropPrefix?_string_eq_some {pat : String} {s res : Slice} (
rw [dropPrefix?_string_eq_dropPrefix?_toSlice] at h
simpa using eq_append_of_dropPrefix?_slice_eq_some h
theorem skipSuffix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
s.skipSuffix? pat = some s.endPos := by
rw [skipSuffix?_eq_backwardPatternSkipSuffix?, BackwardSliceSearcher.skipSuffix?_of_isEmpty hpat]
@@ -108,7 +111,11 @@ theorem skipSuffix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true)
@[simp]
theorem skipSuffix?_slice_eq_some_iff {pat s : Slice} {pos : s.Pos} :
s.skipSuffix? pat = some pos t, pos.Splits t pat.copy := by
rw [Pattern.Model.skipSuffix?_eq_some_iff, ForwardSliceSearcher.isLongestRevMatch_iff_splits]
match h : pat.isEmpty with
| false =>
have := BackwardSliceSearcher.lawfulBackwardPatternModel h
rw [Pattern.Model.skipSuffix?_eq_some_iff, ForwardSliceSearcher.isLongestRevMatch_iff_splits h]
| true => simp [skipSuffix?_slice_of_isEmpty h, (show pat.copy = "" by simpa), eq_comm]
theorem endsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
s.endsWith pat = true := by
@@ -117,10 +124,14 @@ theorem endsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
@[simp]
theorem endsWith_slice_iff {pat s : Slice} :
s.endsWith pat pat.copy.toList <:+ s.copy.toList := by
simp only [Model.endsWith_iff, ForwardSliceSearcher.revMatchesAt_iff_splits,
splits_endPos_iff, exists_eq_right]
simp only [ toList_inj, toList_append, List.suffix_iff_exists_append_eq]
exact fun t, ht => t.toList, by simp [ht], fun t, ht => String.ofList t, by simp [ ht]
match h : pat.isEmpty with
| false =>
have := BackwardSliceSearcher.lawfulBackwardPatternModel h
simp only [Model.endsWith_iff, ForwardSliceSearcher.revMatchesAt_iff_splits h,
splits_endPos_iff, exists_eq_right]
simp only [ toList_inj, toList_append, List.suffix_iff_exists_append_eq]
exact fun t, ht => t.toList, by simp [ht], fun t, ht => String.ofList t, by simp [ ht]
| true => simp [endsWith_slice_of_isEmpty h, (show pat.copy = "" by simpa)]
@[simp]
theorem endsWith_slice_eq_false_iff {pat s : Slice} :
@@ -133,10 +144,14 @@ theorem dropSuffix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true)
theorem eq_append_of_dropSuffix?_slice_eq_some {pat s res : Slice} (h : s.dropSuffix? pat = some res) :
s.copy = res.copy ++ pat.copy := by
have := Pattern.Model.eq_append_of_dropSuffix?_eq_some h
simp only [PatternModel.Matches] at this
obtain _, -, rfl, h := this
exact h
match hpat : pat.isEmpty with
| false =>
have := BackwardSliceSearcher.lawfulBackwardPatternModel hpat
have := Pattern.Model.eq_append_of_dropSuffix?_eq_some h
simp only [PatternModel.Matches] at this
obtain _, -, rfl, h := this
exact h
| true => simp [Option.some.inj (h dropSuffix?_slice_of_isEmpty hpat), (show pat.copy = "" by simpa)]
@[simp]
theorem skipSuffix?_string_eq_some_iff' {pat : String} {s : Slice} {pos : s.Pos} :
@@ -193,12 +208,12 @@ theorem startsWith_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmp
@[simp]
theorem startsWith_slice_iff {pat : Slice} {s : String} :
s.startsWith pat pat.copy.toList <+: s.toList := by
simp [ startsWith_toSlice]
simp [startsWith_eq_startsWith_toSlice]
@[simp]
theorem startsWith_slice_eq_false_iff {pat : Slice} {s : String} :
s.startsWith pat = false ¬ (pat.copy.toList <+: s.toList) := by
simp [ startsWith_toSlice]
simp [startsWith_eq_startsWith_toSlice]
theorem dropPrefix?_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) :
s.dropPrefix? pat = some s.toSlice := by
@@ -224,21 +239,21 @@ theorem skipPrefix?_string_eq_some_iff {pat s : String} {pos : s.Pos} :
@[simp]
theorem startsWith_string_empty {s : String} : s.startsWith "" = true := by
simp [ startsWith_toSlice]
simp [startsWith_eq_startsWith_toSlice]
@[simp]
theorem startsWith_string_iff {pat s : String} :
s.startsWith pat pat.toList <+: s.toList := by
simp [ startsWith_toSlice]
simp [startsWith_eq_startsWith_toSlice]
@[simp]
theorem startsWith_string_eq_false_iff {pat s : String} :
s.startsWith pat = false ¬ (pat.toList <+: s.toList) := by
simp [ startsWith_toSlice]
simp [startsWith_eq_startsWith_toSlice]
@[simp]
theorem dropPrefix?_string_empty {s : String} : s.dropPrefix? "" = some s.toSlice := by
simp [ dropPrefix?_toSlice]
simp [dropPrefix?_eq_dropPrefix?_toSlice]
theorem eq_append_of_dropPrefix?_string_eq_some {s pat : String} {res : Slice} (h : s.dropPrefix? pat = some res) :
s = pat ++ res.copy := by

View File

@@ -99,11 +99,6 @@ theorem Pos.splits {s : String} (p : s.Pos) :
eq_append := by simp [ toByteArray_inj, Slice.toByteArray_copy, size_toByteArray]
offset_eq_rawEndPos := by simp
@[simp]
theorem sliceTo_append_sliceFrom {s : String} {pos : s.Pos} :
(s.sliceTo pos).copy ++ (s.sliceFrom pos).copy = s :=
pos.splits.eq_append.symm
theorem Slice.Pos.splits {s : Slice} (p : s.Pos) :
p.Splits (s.sliceTo p).copy (s.sliceFrom p).copy where
eq_append := copy_eq_copy_sliceTo
@@ -380,10 +375,6 @@ theorem Slice.copy_sliceTo_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₁ :
· rintro t₂, h
exact p.splits.eq_left h
theorem Slice.copy_sliceTo_eq_iff_splits {s : Slice} {p : s.Pos} {t₁ : String} :
(s.sliceTo p).copy = t₁ p.Splits t₁ (s.sliceFrom p).copy :=
fun h => h p.splits, p.splits.eq_left
theorem Slice.copy_sliceFrom_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₂ : String} :
(s.sliceFrom p).copy = t₂ t₁, p.Splits t₁ t₂ := by
refine ?_, ?_
@@ -392,26 +383,14 @@ theorem Slice.copy_sliceFrom_eq_iff_exists_splits {s : Slice} {p : s.Pos} {t₂
· rintro t₂, h
exact p.splits.eq_right h
theorem Slice.copy_sliceFrom_eq_iff_splits {s : Slice} {p : s.Pos} {t₂ : String} :
(s.sliceFrom p).copy = t₂ p.Splits (s.sliceTo p).copy t₂ :=
fun h => h p.splits, p.splits.eq_right
theorem copy_sliceTo_eq_iff_exists_splits {s : String} {p : s.Pos} {t₁ : String} :
(s.sliceTo p).copy = t₁ t₂, p.Splits t₁ t₂ := by
simp [ Pos.splits_toSlice_iff, Slice.copy_sliceTo_eq_iff_exists_splits]
theorem copy_sliceTo_eq_iff_splits {s : String} {p : s.Pos} {t₁ : String} :
(s.sliceTo p).copy = t₁ p.Splits t₁ (s.sliceFrom p).copy :=
fun h => h p.splits, p.splits.eq_left
theorem copy_sliceFrom_eq_iff_exists_splits {s : String} {p : s.Pos} {t₂ : String} :
(s.sliceFrom p).copy = t₂ t₁, p.Splits t₁ t₂ := by
simp [ Pos.splits_toSlice_iff, Slice.copy_sliceFrom_eq_iff_exists_splits]
theorem copy_sliceFrom_eq_iff_splits {s : String} {p : s.Pos} {t₂ : String} :
(s.sliceFrom p).copy = t₂ p.Splits (s.sliceTo p).copy t₂ :=
fun h => h p.splits, p.splits.eq_right
theorem Pos.Splits.offset_eq_decreaseBy {s : String} {p : s.Pos} (h : p.Splits t₁ t₂) :
p.offset = s.rawEndPos.decreaseBy t₂.utf8ByteSize := by
simp [h.offset_eq_rawEndPos, h.eq_append, Pos.Raw.ext_iff]
@@ -662,28 +641,6 @@ theorem Pos.splits_append_rawEndPos {s t : String} :
eq_append := rfl
offset_eq_rawEndPos := rfl
/--
Given a slice `s` such that `s.copy = t₁ ++ t₂`, obtain the position sitting between `t₁` and `t₂`.
-/
def Slice.Pos.ofEqAppend {s : Slice} {t₁ t₂ : String} (h : s.copy = t₁ ++ t₂) : s.Pos :=
s.pos t₁.rawEndPos
(by simpa [ Pos.Raw.isValid_copy_iff, h] using ((Pos.Raw.isValid_rawEndPos).append_right t₂))
theorem Slice.Pos.splits_ofEqAppend {s : Slice} {t₁ t₂ : String} (h : s.copy = t₁ ++ t₂) :
(ofEqAppend h).Splits t₁ t₂ where
eq_append := h
offset_eq_rawEndPos := by simp [ofEqAppend]
/--
Given a string `s` such that `s = t₁ ++ t₂`, obtain the position sitting between `t₁` and `t₂`.
-/
def Pos.ofEqAppend {s t₁ t₂ : String} (h : s = t₁ ++ t₂) : s.Pos :=
((t₁ ++ t₂).pos t₁.rawEndPos ((Pos.Raw.isValid_rawEndPos).append_right t₂)).cast h.symm
theorem Pos.splits_ofEqAppend {s t₁ t₂ : String} (h : s = t₁ ++ t₂) : (ofEqAppend h).Splits t₁ t₂ where
eq_append := h
offset_eq_rawEndPos := by simp [ofEqAppend]
theorem Pos.Splits.copy_sliceTo_eq {s : String} {p : s.Pos} (h : p.Splits t₁ t₂) :
(s.sliceTo p).copy = t₁ :=
p.splits.eq_left h
@@ -783,44 +740,4 @@ theorem splits_prevn_endPos (s : String) (n : Nat) :
(s.endPos.prevn n).Splits (String.ofList (s.toList.take (s.length - n))) (String.ofList (s.toList.drop (s.length - n))) := by
simpa using s.splits_endPos.prevn n
@[simp]
theorem Slice.copy_sliceFrom_cast {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} :
(t.sliceFrom (pos.cast hst)).copy = (s.sliceFrom pos).copy := by
simpa [copy_sliceFrom_eq_iff_exists_splits] using _, pos.splits
@[simp]
theorem Slice.copy_sliceTo_cast {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} :
(t.sliceTo (pos.cast hst)).copy = (s.sliceTo pos).copy := by
simpa [copy_sliceTo_eq_iff_exists_splits] using _, pos.splits
@[simp]
theorem copy_sliceFrom_cast {s t : String} (hst : s = t) {pos : s.Pos} :
(t.sliceFrom (pos.cast hst)).copy = (s.sliceFrom pos).copy := by
simpa [copy_sliceFrom_eq_iff_exists_splits] using _, pos.splits
@[simp]
theorem copy_sliceTo_cast {s t : String} (hst : s = t) {pos : s.Pos} :
(t.sliceTo (pos.cast hst)).copy = (s.sliceTo pos).copy := by
simpa [copy_sliceTo_eq_iff_exists_splits] using _, pos.splits
theorem Slice.Pos.sliceFrom_cast {s t : Slice} {hst : s.copy = t.copy} (p q : s.Pos) {h} :
Slice.Pos.sliceFrom (p.cast hst) (q.cast hst) h =
(Slice.Pos.sliceFrom p q (by simpa using h)).cast (by simp) := by
ext1; simp
theorem Slice.Pos.sliceTo_cast {s t : Slice} {hst : s.copy = t.copy} (p q : s.Pos) {h} :
Slice.Pos.sliceTo (p.cast hst) (q.cast hst) h =
(Slice.Pos.sliceTo p q (by simpa using h)).cast (by simp) := by
ext1; simp
theorem Pos.sliceFrom_cast {s t : String} {hst : s = t} (p q : s.Pos) {h} :
Pos.sliceFrom (p.cast hst) (q.cast hst) h =
(Pos.sliceFrom p q (by simpa using h)).cast (by simp) := by
ext1; simp
theorem Pos.sliceTo_cast {s t : String} {hst : s = t} (p q : s.Pos) {h} :
Pos.sliceTo (p.cast hst) (q.cast hst) h =
(Pos.sliceTo p q (by simpa using h)).cast (by simp) := by
ext1; simp
end String

View File

@@ -96,44 +96,6 @@ theorem endPos_ofSliceFrom {s : Slice} {p : s.Pos} {st : SearchStep (s.sliceFrom
st.ofSliceFrom.endPos = Slice.Pos.ofSliceFrom st.endPos := by
cases st <;> simp [ofSliceFrom]
/--
Converts a {lean}`SearchStep s` into a {lean}`SearchStep t` by applying {name}`Slice.Pos.cast` to the
start and end position.
-/
@[inline]
def cast {s t : Slice} (hst : s.copy = t.copy) : SearchStep s SearchStep t
| .rejected startPos endPos => .rejected (startPos.cast hst) (endPos.cast hst)
| .matched startPos endPos => .matched (startPos.cast hst) (endPos.cast hst)
@[simp]
theorem cast_rejected {s t : Slice} {hst : s.copy = t.copy} {startPos endPos : s.Pos} :
(SearchStep.rejected startPos endPos).cast hst = .rejected (startPos.cast hst) (endPos.cast hst) :=
(rfl)
@[simp]
theorem cast_matched {s t : Slice} {hst : s.copy = t.copy} {startPos endPos : s.Pos} :
(SearchStep.matched startPos endPos).cast hst = .matched (startPos.cast hst) (endPos.cast hst) :=
(rfl)
@[simp]
theorem startPos_cast {s t : Slice} (hst : s.copy = t.copy) {st : SearchStep s} :
(st.cast hst).startPos = st.startPos.cast hst := by
cases st <;> simp
@[simp]
theorem endPos_cast {s t : Slice} (hst : s.copy = t.copy) {st : SearchStep s} :
(st.cast hst).endPos = st.endPos.cast hst := by
cases st <;> simp
@[simp]
theorem cast_rfl {s : Slice} {st : SearchStep s} : st.cast rfl = st := by
cases st <;> simp
@[simp]
theorem cast_cast {s t u : Slice} {hst : s.copy = t.copy} {htu : t.copy = u.copy} {st : SearchStep s} :
(st.cast hst).cast htu = st.cast (hst.trans htu) := by
cases st <;> simp
end SearchStep
/--

View File

@@ -311,6 +311,23 @@ def Internal.containsImpl (s : String) (c : Char) : Bool :=
def Internal.anyImpl (s : String) (p : Char Bool) :=
String.any s p
/--
Checks whether a slice only consists of matches of the pattern {name}`pat`.
Short-circuits at the first pattern mis-match.
This function is generic over all currently supported patterns.
Examples:
* {lean}`"brown".all Char.isLower = true`
* {lean}`"brown and orange".all Char.isLower = false`
* {lean}`"aaaaaa".all 'a' = true`
* {lean}`"aaaaaa".all "aa" = true`
* {lean}`"aaaaaaa".all "aa" = false`
-/
@[inline, suggest_for String.every] def all (s : String) (pat : ρ) [ForwardPattern pat] : Bool :=
s.toSlice.all pat
/--
Checks whether the string can be interpreted as the decimal representation of a natural number.

View File

@@ -426,13 +426,13 @@ Advances {name}`pos` as long as {name}`pat` matches.
-/
@[specialize pat]
def Pos.skipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : s.Pos :=
match pos.skip? pat with
| some nextCurr =>
if pos < nextCurr then
skipWhile nextCurr pat
if let some nextCurr := ForwardPattern.skipPrefix? pat (s.sliceFrom pos) then
if pos < Pos.ofSliceFrom nextCurr then
skipWhile (Pos.ofSliceFrom nextCurr) pat
else
pos
| none => pos
else
pos
termination_by pos
/--
@@ -572,7 +572,7 @@ Examples:
-/
@[inline]
def all (s : Slice) (pat : ρ) [ForwardPattern pat] : Bool :=
s.skipPrefixWhile pat == s.endPos
s.dropWhile pat |>.isEmpty
end ForwardPatternUsers
@@ -707,7 +707,7 @@ This function is generic over all currently supported patterns.
-/
@[inline]
def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
((s.sliceTo pos).skipSuffix? pat).map Pos.ofSliceTo
((s.sliceFrom pos).skipSuffix? pat).map Pos.ofSliceFrom
/--
If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
@@ -765,13 +765,13 @@ Rewinds {name}`pos` as long as {name}`pat` matches.
-/
@[specialize pat]
def Pos.revSkipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : s.Pos :=
match pos.revSkip? pat with
| some nextCurr =>
if nextCurr < pos then
revSkipWhile nextCurr pat
if let some nextCurr := BackwardPattern.skipSuffix? pat (s.sliceTo pos) then
if Pos.ofSliceTo nextCurr < pos then
revSkipWhile (Pos.ofSliceTo nextCurr) pat
else
pos
| none => pos
else
pos
termination_by pos.down
/--
@@ -782,36 +782,6 @@ Returns the position at the start of the longest suffix of {name}`s` for which {
def skipSuffixWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : s.Pos :=
s.endPos.revSkipWhile pat
/--
Checks whether a slice only consists of matches of the pattern {name}`pat`, starting from the back
of the string.
Short-circuits at the first pattern mis-match.
This function is generic over all currently supported patterns.
For many types of patterns, this function can be expected to return the same result as
{name}`Slice.all`. If mismatches are expected to occur close to the end of the string, this function
might be more efficient.
For some types of patterns, this function will return a different result than {name}`Slice.all`.
Consider, for example, a pattern that matches the longest string at the given position that matches
the regular expression {lean}`"a|aa|ab"`. Then, given the input string {lean}`"aab"`, performing
{name}`Slice.all` will greedily match the prefix {lean}`"aa"` and then get stuck on the remainder
{lean}`"b"`, causing it to return {lean}`false`. On the other hand, {name}`Slice.revAll` will match
the suffix {lean}`"ab"` and then match the remainder {lean}`"a"`, so it will return {lean}`true`.
Examples:
* {lean}`"brown".toSlice.revAll Char.isLower = true`
* {lean}`"brown and orange".toSlice.revAll Char.isLower = false`
* {lean}`"aaaaaa".toSlice.revAll 'a' = true`
* {lean}`"aaaaaa".toSlice.revAll "aa" = true`
* {lean}`"aaaaaaa".toSlice.revAll "aa" = false`
-/
@[inline]
def revAll (s : Slice) (pat : ρ) [BackwardPattern pat] : Bool :=
s.skipSuffixWhile pat == s.startPos
/--
Creates a new slice that contains the longest suffix of {name}`s` for which {name}`pat` matched
(potentially repeatedly).

View File

@@ -224,53 +224,6 @@ Returns the position after the longest prefix of {name}`s` for which {name}`pat`
@[inline] def skipPrefixWhile (s : String) (pat : ρ) [ForwardPattern pat] : s.Pos :=
Pos.ofToSlice (s.toSlice.skipPrefixWhile pat)
/--
Checks whether a string only consists of matches of the pattern {name}`pat`.
Short-circuits at the first pattern mis-match.
This function is generic over all currently supported patterns.
Examples:
* {lean}`"brown".all Char.isLower = true`
* {lean}`"brown and orange".all Char.isLower = false`
* {lean}`"aaaaaa".all 'a' = true`
* {lean}`"aaaaaa".all "aa" = true`
* {lean}`"aaaaaaa".all "aa" = false`
-/
@[inline, suggest_for String.every] def all (s : String) (pat : ρ) [ForwardPattern pat] : Bool :=
s.toSlice.all pat
/--
Checks whether a string only consists of matches of the pattern {name}`pat`, starting from the back
of the string.
Short-circuits at the first pattern mis-match.
This function is generic over all currently supported patterns.
For many types of patterns, this function can be expected to return the same result as
{name}`String.all`. If mismatches are expected to occur close to the end of the string, this function
might be more efficient.
For some types of patterns, this function will return a different result than {name}`String.all`.
Consider, for example, a pattern that matches the longest string at the given position that matches
the regular expression {lean}`"a|aa|ab"`. Then, given the input string {lean}`"aab"`, performing
{name}`String.all` will greedily match the prefix {lean}`"aa"` and then get stuck on the remainder
{lean}`"b"`, causing it to return {lean}`false`. On the other hand, {name}`String.revAll` will match
the suffix {lean}`"ab"` and then match the remainder {lean}`"a"`, so it will return {lean}`true`.
Examples:
* {lean}`"brown".revAll Char.isLower = true`
* {lean}`"brown and orange".revAll Char.isLower = false`
* {lean}`"aaaaaa".revAll 'a' = true`
* {lean}`"aaaaaa".revAll "aa" = true`
* {lean}`"aaaaaaa".revAll "aa" = false`
-/
@[inline]
def revAll (s : String) (pat : ρ) [BackwardPattern pat] : Bool :=
s.toSlice.revAll pat
/--
If {name}`pat` matches at {name}`pos`, returns the position after the end of the match.
Returns {name}`none` otherwise.

View File

@@ -1230,14 +1230,7 @@ def instantiateRevRangeArgs (e : Expr) (beginIdx endIdx : Nat) (args : Array (Ar
else
e.instantiateRevRange beginIdx endIdx (args.map (·.toExpr))
/--
Lookup function for compiler extensions with sorted persisted state that works in both `lean` and
`leanir`.
`preferImported` defaults to false because in `leanir`, we do not want to mix information from
`meta` compilation in `lean` with our own state. But in `lean`, setting `preferImported` can help
with avoiding unnecessary task blocks.
-/
/-- Lookup function for compiler extensions with sorted persisted state that works in both `lean` and `leanir`. -/
@[inline] def findExtEntry? [Inhabited σ] (env : Environment) (ext : PersistentEnvExtension α β σ) (declName : Name)
(findAtSorted? : Array α Name Option α')
(findInState? : σ Name Option α') : Option α' :=

View File

@@ -78,13 +78,9 @@ def isValidMainType (type : Expr) : Bool :=
isValidResultName resultName
| _ => false
/-- A postponed call of `compileDecls`. -/
structure PostponedCompileDecls where
/-- Declaration names of this mutual group. -/
declNames : Array Name
/-- Options at time of original call, to be restored for tracing etc. -/
options : Options
deriving BEq
deriving BEq, Hashable
/--
Saves postponed `compileDecls` calls.
@@ -105,20 +101,16 @@ builtin_initialize postponedCompileDeclsExt : SimplePersistentEnvExtension Postp
{ exported := #[], server := #[], «private» := es.toArray }
}
def resumeCompilation (declName : Name) (baseOpts : Options) : CoreM Unit := do
def resumeCompilation (declName : Name) : CoreM Unit := do
let some decls := postponedCompileDeclsExt.getState ( getEnv) |>.find? declName | return
let opts := baseOpts.mergeBy (fun _ base _ => base) decls.options
let opts := compiler.postponeCompile.set opts false
modifyEnv (postponedCompileDeclsExt.modifyState · fun s => decls.declNames.foldl (·.erase) s)
-- NOTE: we *must* throw away the current options as they could depend on the specific recursion
-- we did to get here.
withOptions (fun _ => opts) do
withOptions (compiler.postponeCompile.set · false) do
Core.prependError m!"Failed to compile `{declName}`" do
( compileDeclsRef.get) decls.declNames baseOpts
( compileDeclsRef.get) decls.declNames
namespace PassManager
partial def run (declNames : Array Name) (baseOpts : Options) : CompilerM Unit := withAtLeastMaxRecDepth 8192 do
partial def run (declNames : Array Name) : CompilerM Unit := withAtLeastMaxRecDepth 8192 do
/-
Note: we need to increase the recursion depth because we currently do to save phase1
declarations in .olean files. Then, we have to recursively compile all dependencies,
@@ -149,14 +141,11 @@ partial def run (declNames : Array Name) (baseOpts : Options) : CompilerM Unit :
-- Now that we have done all input checks, check for postponement
if ( getEnv).header.isModule && ( compiler.postponeCompile.getM) then
modifyEnv (postponedCompileDeclsExt.addEntry · { declNames := decls.map (·.name), options := getOptions })
modifyEnv (postponedCompileDeclsExt.addEntry · { declNames := decls.map (·.name) })
-- meta defs are compiled locally so they are available for execution/compilation without
-- importing `.ir` but still marked for `leanir` compilation so that we do not have to persist
-- module-local compilation information between the two processes
if decls.any (isMarkedMeta ( getEnv) ·.name) then
-- avoid re-compiling the meta defs in this process; the entry for `leanir` is not affected
modifyEnv (postponedCompileDeclsExt.modifyState · fun s => decls.foldl (·.erase ·.name) s)
else
if !decls.any (isMarkedMeta ( getEnv) ·.name) then
trace[Compiler] "postponing compilation of {decls.map (·.name)}"
return
@@ -168,7 +157,7 @@ partial def run (declNames : Array Name) (baseOpts : Options) : CompilerM Unit :
let .let { value := .const c .., .. } .. := c | return
-- Need to do some lookups to get the actual name passed to `compileDecls`
let c := Compiler.getImplementedBy? ( getEnv) c |>.getD c
resumeCompilation c baseOpts
resumeCompilation c
let decls := markRecDecls decls
let manager getPassManager
@@ -211,9 +200,9 @@ where
end PassManager
def main (declNames : Array Name) (baseOpts : Options) : CoreM Unit := do
def main (declNames : Array Name) : CoreM Unit := do
withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
CompilerM.run <| PassManager.run declNames baseOpts
CompilerM.run <| PassManager.run declNames
builtin_initialize
compileDeclsRef.set main

View File

@@ -279,13 +279,13 @@ partial def casesFloatArrayToMono (c : Cases .pure) (_ : c.typeName == ``FloatAr
let k k.toMono
return .let decl k
/-- Eliminate `cases` for `String`. -/
/-- Eliminate `cases` for `String. -/
partial def casesStringToMono (c : Cases .pure) (_ : c.typeName == ``String) : ToMonoM (Code .pure) := do
assert! c.alts.size == 1
let .alt _ ps k := c.alts[0]! | unreachable!
eraseParams ps
let p := ps[0]!
let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``String.toByteArray [] #[.fvar c.discr] }
let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``String.toList [] #[.fvar c.discr] }
modifyLCtx fun lctx => lctx.addLetDecl decl
let k k.toMono
return .let decl k

View File

@@ -19,7 +19,7 @@ that fulfill the requirements of `shouldGenerateCode`.
def compile (declNames : Array Name) : CoreM Unit := do profileitM Exception "compiler new" ( getOptions) do
withOptions (compiler.postponeCompile.set · false) do
withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
LCNF.main declNames {}
LCNF.main declNames
builtin_initialize
registerTraceClass `Compiler

View File

@@ -711,11 +711,11 @@ breaks the cycle by making `compileDeclsImpl` a "dynamic" call through the ref t
to the linker. In the compiler there is a matching `builtin_initialize` to set this ref to the
actual implementation of compileDeclsRef.
-/
builtin_initialize compileDeclsRef : IO.Ref (Array Name Options CoreM Unit)
IO.mkRef (fun _ _ => throwError m!"call to compileDecls with uninitialized compileDeclsRef")
builtin_initialize compileDeclsRef : IO.Ref (Array Name CoreM Unit)
IO.mkRef (fun _ => throwError m!"call to compileDecls with uninitialized compileDeclsRef")
private def compileDeclsImpl (declNames : Array Name) : CoreM Unit := do
( compileDeclsRef.get) declNames {}
( compileDeclsRef.get) declNames
-- `ref?` is used for error reporting if available
def compileDecls (decls : Array Name) (logErrors := true) : CoreM Unit := do

View File

@@ -82,17 +82,11 @@ def mergeBy (f : Name → DataValue → DataValue → DataValue) (o1 o2 : Option
end Options
structure OptionDeprecation where
since : String
text? : Option String := none
deriving Inhabited
structure OptionDecl where
name : Name
declName : Name := by exact decl_name%
defValue : DataValue
descr : String := ""
deprecation? : Option OptionDeprecation := none
deriving Inhabited
def OptionDecl.fullDescr (self : OptionDecl) : String := Id.run do
@@ -189,7 +183,6 @@ namespace Option
protected structure Decl (α : Type) where
defValue : α
descr : String := ""
deprecation? : Option OptionDeprecation := none
protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Option α :=
opts.get? opt.name
@@ -221,7 +214,6 @@ protected def register [KVMap.Value α] (name : Name) (decl : Lean.Option.Decl
declName := ref
defValue := KVMap.Value.toDataValue decl.defValue
descr := decl.descr
deprecation? := decl.deprecation?
}
return { name := name, defValue := decl.defValue }

View File

@@ -1832,15 +1832,13 @@ To infer a namespace from the expected type, we do the following operations:
- if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace,
and if that doesn't work, try unfolding the expression and continuing.
-/
private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
unless id.isAtomic do
throwError "Invalid dotted identifier notation: The name `{id}` must be atomic"
tryPostponeIfNoneOrMVar expectedType?
let some expectedType := expectedType?
| throwNoExpectedType
addCompletionInfo <| CompletionInfo.dotId idRef id ( getLCtx) expectedType?
-- We will check deprecations in `elabAppFnResolutions`.
withoutCheckDeprecated do
withForallBody expectedType fun resultType => do
go resultType expectedType #[]
where
@@ -1880,10 +1878,8 @@ where
|>.filter (fun (_, fieldList) => fieldList.isEmpty)
|>.map Prod.fst
if !candidates.isEmpty then
candidates.mapM fun resolvedName => return ( mkConst resolvedName explicitUnivs, getRef, [])
candidates.mapM fun resolvedName => return ( mkConst resolvedName, getRef, [])
else if let some (fvar, []) resolveLocalName fullName then
unless explicitUnivs.isEmpty do
throwInvalidExplicitUniversesForLocal fvar
return [(fvar, getRef, [])]
else
throwUnknownIdentifierAt ( getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`"
@@ -1923,10 +1919,6 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
let some idx := idxStx.isFieldIdx?
| throwError "Internal error: Unexpected field index syntax `{idxStx}`"
elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) (explicit : Bool) : TermElabM (Array (TermElabResult Expr)) := do
let res withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes explicitUnivs expectedType?
-- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
match f with
| `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
| `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
@@ -1942,17 +1934,16 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
| `($id:ident.{$us,*}) => do
let us elabExplicitUnivs us
elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
| `(.$id:ident) => elabDottedIdent id [] explicit
| `(.$id:ident.{$us,*}) =>
let us elabExplicitUnivs us
elabDottedIdent id us explicit
| `(@$_:ident)
| `(@$_:ident.{$_us,*})
| `(@.$_:ident)
| `(@.$_:ident.{$_us,*}) =>
| `(@$id:ident) =>
elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
| `(@$_:ident.{$_us,*}) =>
elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
| `(@$_) => throwUnsupportedSyntax -- invalid occurrence of `@`
| `(_) => throwError "A placeholder `_` cannot be used where a function is expected"
| `(.$id:ident) =>
let res withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes expectedType?
-- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
| _ => do
let catchPostpone := !overloaded
/- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms.
@@ -2095,15 +2086,13 @@ private def elabAtom : TermElab := fun stx expectedType? => do
@[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
match stx with
| `(@$_:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@`
| `(@$_:ident.{$_us,*}) => elabAtom stx expectedType?
| `(@$(_).$_:fieldIdx) => elabAtom stx expectedType?
| `(@$(_).$_:ident) => elabAtom stx expectedType?
| `(@.$_:ident) => elabAtom stx expectedType?
| `(@.$_:ident.{$_us,*}) => elabAtom stx expectedType?
| `(@($t)) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas
| `(@$t) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas
| _ => throwUnsupportedSyntax
| `(@$_:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@`
| `(@$_:ident.{$_us,*}) => elabAtom stx expectedType?
| `(@$(_).$_:fieldIdx) => elabAtom stx expectedType?
| `(@$(_).$_:ident) => elabAtom stx expectedType?
| `(@($t)) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas
| `(@$t) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas
| _ => throwUnsupportedSyntax
@[builtin_term_elab choice] def elabChoice : TermElab := elabAtom
@[builtin_term_elab proj] def elabProj : TermElab := elabAtom

View File

@@ -510,8 +510,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
pure ()
@[builtin_command_elab «set_option»] def elabSetOption : CommandElab := fun stx => do
let (options, decl) Elab.elabSetOption stx[1] stx[3]
withRef stx[1] <| Elab.checkDeprecatedOption (stx[1].getId.eraseMacroScopes) decl
let options Elab.elabSetOption stx[1] stx[3]
modify fun s => { s with maxRecDepth := maxRecDepth.get options }
modifyScope fun scope => { scope with opts := options }

View File

@@ -81,15 +81,8 @@ private def pushTypeIntoReassignment (letOrReassign : LetOrReassign) (decl : TSy
else
pure decl
private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
if config.postponeValue then
throwError "`+postponeValue` is not supported in `do` blocks"
if config.generalize then
throwError "`+generalize` is not supported in `do` blocks"
partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
partial def elabDoLetOrReassign (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
(dec : DoElemCont) : DoElabM Expr := do
checkLetConfigInDo config
let vars getLetDeclVars decl
letOrReassign.checkMutVars vars
-- Some decl preprocessing on the patterns and expected types:
@@ -98,7 +91,7 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
match decl with
| `(letDecl| $decl:letEqnsDecl) =>
let declNew `(letDecl| $( liftMacroM <| Term.expandLetEqnsDecl decl):letIdDecl)
return Term.withMacroExpansion decl declNew <| elabDoLetOrReassign config letOrReassign declNew dec
return Term.withMacroExpansion decl declNew <| elabDoLetOrReassign letOrReassign declNew dec
| `(letDecl| $pattern:term $[: $xType?]? := $rhs) =>
let rhs match xType? with | some xType => `(($rhs : $xType)) | none => pure rhs
let contElab : DoElabM Expr := elabWithReassignments letOrReassign vars dec.continueWithUnit
@@ -106,21 +99,15 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
-- The infamous MVar postponement trick below popularized by `if` is necessary in Lake.CLI.Main.
-- We need it because we specify a constant motive, otherwise the `match` elaborator would have postponed.
let mvar Lean.withRef rhs `(?m)
let term if let some h := config.eq? then
`(let_mvar% ?m := $rhs;
wait_if_type_mvar% ?m;
match $h:ident : $mvar:term with
| $pattern:term => $body)
else
`(let_mvar% ?m := $rhs;
wait_if_type_mvar% ?m;
match (motive := _, $( Term.exprToSyntax mγ)) $mvar:term with
| $pattern:term => $body)
let term `(let_mvar% ?m := $rhs;
wait_if_type_mvar% ?m;
match (motive := _, $( Term.exprToSyntax mγ)) $mvar:term with
| $pattern:term => $body)
Term.withMacroExpansion ( getRef) term do Term.elabTermEnsuringType term (some mγ)
| `(letDecl| $decl:letIdDecl) =>
let { id, binders, type, value } := Term.mkLetIdDeclView decl
let id if id.isIdent then pure id else Term.mkFreshIdent id (canonical := true)
let nondep := config.nondep || letOrReassign matches .have
let nondep := letOrReassign matches .have
-- Only non-`mut` lets will be elaborated as `let`s; `let mut` and reassigns behave as `have`s.
-- See `elabLetDeclAux` for rationale.
let (type, val) Term.elabBindersEx binders fun xs => do
@@ -141,25 +128,8 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
withLetDecl id.getId (kind := kind) type val (nondep := nondep) fun x => do
Term.addLocalVarInfo id x
elabWithReassignments letOrReassign vars do
match config.eq? with
| none =>
let body dec.continueWithUnit
if config.zeta then
pure <| ( body.abstractM #[x]).instantiate1 val
else
mkLetFVars #[x] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
| some h =>
let hTy mkEq x val
withLetDecl h.getId hTy ( mkEqRefl x) (nondep := true) fun h' => do
Term.addLocalVarInfo h h'
let body dec.continueWithUnit
if config.zeta then
pure <| ( body.abstractM #[x, h']).instantiateRev #[val, mkEqRefl val]
else if nondep then
let f mkLambdaFVars #[x, h'] body
return mkApp2 f val ( mkEqRefl val)
else
mkLetFVars #[x, h'] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
let body dec.continueWithUnit
mkLetFVars #[x] body (usedLetOnly := false) (generalizeNondepLet := false)
| _ => throwUnsupportedSyntax
def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``doPatDecl]) (dec : DoElemCont) : DoElabM Expr := do
@@ -198,21 +168,13 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
elabDoElem ( `(doElem| $pattern:term := $x)) dec
| _ => throwUnsupportedSyntax
private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letConfig)
(mutTk? : Option Syntax) (initConfig : Term.LetConfig := {}) : DoElabM Term.LetConfig := do
if mutTk?.isSome && !letConfigStx.raw[0].getArgs.isEmpty then
throwErrorAt letConfigStx "configuration options are not allowed with `let mut`"
Term.mkLetConfig letConfigStx initConfig
@[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do
let `(doLet| let $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
let config getLetConfigAndCheckMut config mutTk?
elabDoLetOrReassign config (.let mutTk?) decl dec
let `(doLet| let $[mut%$mutTk?]? $decl:letDecl) := stx | throwUnsupportedSyntax
elabDoLetOrReassign (.let mutTk?) decl dec
@[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
let `(doHave| have $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
let config Term.mkLetConfig config { nondep := true }
elabDoLetOrReassign config .have decl dec
let `(doHave| have $decl:letDecl) := stx | throwUnsupportedSyntax
elabDoLetOrReassign .have decl dec
@[builtin_doElem_elab Lean.Parser.Term.doLetRec] def elabDoLetRec : DoElab := fun stx dec => do
let `(doLetRec| let rec $decls:letRecDecls) := stx | throwUnsupportedSyntax
@@ -230,17 +192,14 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
| `(doReassign| $x:ident $[: $xType?]? := $rhs) =>
let decl : TSyntax ``letIdDecl `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
let decl : TSyntax ``letDecl := mkNode ``letDecl #[decl]
elabDoLetOrReassign {} .reassign decl dec
elabDoLetOrReassign .reassign decl dec
| `(doReassign| $decl:letPatDecl) =>
let decl : TSyntax ``letDecl := mkNode ``letDecl #[decl]
elabDoLetOrReassign {} .reassign decl dec
elabDoLetOrReassign .reassign decl dec
| _ => throwUnsupportedSyntax
@[builtin_doElem_elab Lean.Parser.Term.doLetElse] def elabDoLetElse : DoElab := fun stx dec => do
let `(doLetElse| let $[mut%$mutTk?]? $cfg:letConfig $pattern := $rhs | $otherwise $(body?)?) := stx
| throwUnsupportedSyntax
let config getLetConfigAndCheckMut cfg mutTk?
checkLetConfigInDo config
let `(doLetElse| let $[mut%$mutTk?]? $pattern := $rhs | $otherwise $(body?)?) := stx | throwUnsupportedSyntax
let letOrReassign := LetOrReassign.let mutTk?
let vars getPatternVarsEx pattern
letOrReassign.checkMutVars vars
@@ -249,17 +208,10 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
if mutTk?.isSome then
for var in vars do
body `(doSeqIndent| let mut $var := $var; do $body:doSeqIndent)
if let some h := config.eq? then
elabDoElem ( `(doElem| match $h:ident : $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
else
elabDoElem ( `(doElem| match $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
elabDoElem ( `(doElem| match $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
@[builtin_doElem_elab Lean.Parser.Term.doLetArrow] def elabDoLetArrow : DoElab := fun stx dec => do
let `(doLetArrow| let $[mut%$mutTk?]? $cfg:letConfig $decl) := stx | throwUnsupportedSyntax
let config getLetConfigAndCheckMut cfg mutTk?
checkLetConfigInDo config
if config.nondep || config.usedOnly || config.zeta || config.eq?.isSome then
throwErrorAt cfg "configuration options are not supported with `←`"
let `(doLetArrow| let $[mut%$mutTk?]? $decl) := stx | throwUnsupportedSyntax
elabDoArrow (.let mutTk?) decl dec
@[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do

View File

@@ -371,8 +371,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
popScope
@[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
let (options, decl) Elab.elabSetOption stx[1] stx[3]
withRef stx[1] <| Elab.checkDeprecatedOption (stx[1].getId.eraseMacroScopes) decl
let options Elab.elabSetOption stx[1] stx[3]
withOptions (fun _ => options) do
try
elabTerm stx[5] expectedType?

View File

@@ -875,7 +875,7 @@ first evaluates any local `set_option ... in ...` clauses and then invokes `cmd`
partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
if stx.getKind == ``Lean.Parser.Command.in &&
stx[0].getKind == ``Lean.Parser.Command.set_option then
let (opts, _) Elab.elabSetOption stx[0][1] stx[0][3]
let opts Elab.elabSetOption stx[0][1] stx[0][3]
Command.withScope (fun scope => { scope with opts }) do
withSetOptionIn cmd stx[2]
else

View File

@@ -94,12 +94,12 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
| `(doExpr| $_:term) => return { numRegularExits := 1 }
| `(doElem| do $doSeq) => ofSeq doSeq
-- Let
| `(doElem| let $[mut]? $_:letConfig $_:letDecl) => return .pure
| `(doElem| have $_:letConfig $_:letDecl) => return .pure
| `(doElem| let $[mut]? $_:letDecl) => return .pure
| `(doElem| have $_:letDecl) => return .pure
| `(doElem| let rec $_:letRecDecl) => return .pure
| `(doElem| let $[mut]? $_:letConfig $_ := $_ | $otherwise $(body?)?) =>
| `(doElem| let $[mut]? $_ := $_ | $otherwise $(body?)?) =>
ofLetOrReassign #[] none otherwise body?
| `(doElem| let $[mut]? $_:letConfig $decl) =>
| `(doElem| let $[mut]? $decl) =>
ofLetOrReassignArrow false decl
| `(doElem| $decl:letIdDeclNoBinders) =>
ofLetOrReassign ( getLetIdDeclVars decl) none none none
@@ -169,16 +169,15 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
let bodyInfo match body? with | none => pure {} | some body => ofSeq body
return otherwiseInfo.alternative bodyInfo
| _ =>
let kind := stx.raw.getKind
let handlers := controlInfoElemAttribute.getEntries ( getEnv) kind
let handlers := controlInfoElemAttribute.getEntries ( getEnv) stx.raw.getKind
for handler in handlers do
let res catchInternalId unsupportedSyntaxExceptionId
(some <$> handler.value stx)
(fun _ => pure none)
if let some info := res then return info
throwError
"No `ControlInfo` inference handler found for `{kind}` in syntax {indentD stx}\n\
Register a handler with `@[doElem_control_info {kind}]`."
"No `ControlInfo` inference handler found for `{stx.raw.getKind}` in syntax {indentD stx}\n\
Register a handler with `@[doElem_control_info {stx.raw.getKind}]`."
partial def ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [``doIdDecl, ``doPatDecl]) : TermElabM ControlInfo := do
match decl with

View File

@@ -36,7 +36,6 @@ private def getDoSeq (doStx : Syntax) : Syntax :=
def elabLiftMethod : TermElab := fun stx _ =>
throwErrorAt stx "invalid use of `(<- ...)`, must be nested inside a 'do' expression"
/-- Return true if we should not lift `(<- ...)` actions nested in the syntax nodes with the given kind. -/
private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool :=
k == ``Parser.Term.do ||
@@ -77,9 +76,9 @@ private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
else if k == ``Parser.Term.let then
letDeclHasBinders stx[1]
else if k == ``Parser.Term.doLet then
letDeclHasBinders stx[3]
letDeclHasBinders stx[2]
else if k == ``Parser.Term.doLetArrow then
letDeclArgHasBinders stx[3]
letDeclArgHasBinders stx[2]
else
false
@@ -702,12 +701,12 @@ def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var) := do
throwError "unexpected kind of let declaration"
def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) :=
-- leading_parser "let " >> optional "mut " >> letConfig >> letDecl
getLetDeclVars doLet[3]
-- leading_parser "let " >> optional "mut " >> letDecl
getLetDeclVars doLet[2]
def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) :=
-- leading_parser "have" >> letConfig >> letDecl
getLetDeclVars doHave[2]
-- leading_parser "have" >> letDecl
getLetDeclVars doHave[1]
def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var) := do
-- letRecDecls is an array of `(group (optional attributes >> letDecl))`
@@ -728,9 +727,9 @@ def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var) := do
let pattern := doPatDecl[0]
getPatternVarsEx pattern
-- leading_parser "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
-- leading_parser "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var) := do
let decl := doLetArrow[3]
let decl := doLetArrow[2]
if decl.getKind == ``Parser.Term.doIdDecl then
return #[getDoIdDeclVar decl]
else if decl.getKind == ``Parser.Term.doPatDecl then
@@ -1061,15 +1060,14 @@ def seqToTerm (action : Syntax) (k : Syntax) : M Syntax := withRef action <| wit
def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFreshMacroScope do
let kind := decl.getKind
if kind == ``Parser.Term.doLet then
let letConfig : TSyntax ``Parser.Term.letConfig := decl[2]
let letDecl := decl[3]
`(let $letConfig:letConfig $letDecl:letDecl; $k)
let letDecl := decl[2]
`(let $letDecl:letDecl; $k)
else if kind == ``Parser.Term.doLetRec then
let letRecToken := decl[0]
let letRecDecls := decl[1]
return mkNode ``Parser.Term.letrec #[letRecToken, letRecDecls, mkNullNode, k]
else if kind == ``Parser.Term.doLetArrow then
let arg := decl[3]
let arg := decl[2]
if arg.getKind == ``Parser.Term.doIdDecl then
let id := arg[0]
let type := expandOptType id arg[1]
@@ -1417,7 +1415,7 @@ mutual
/-- Generate `CodeBlock` for `doLetArrow; doElems`
`doLetArrow` is of the form
```
"let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
"let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
```
where
```
@@ -1426,7 +1424,7 @@ mutual
```
-/
partial def doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do
let decl := doLetArrow[3]
let decl := doLetArrow[2]
if decl.getKind == ``Parser.Term.doIdDecl then
let y := decl[0]
checkNotShadowingMutable #[y]
@@ -1477,11 +1475,11 @@ mutual
throwError "unexpected kind of `do` declaration"
partial def doLetElseToCode (doLetElse : Syntax) (doElems : List Syntax) : M CodeBlock := do
-- "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >> (checkColGt >> " | " >> doSeq) >> optional doSeq
let pattern := doLetElse[3]
let val := doLetElse[5]
let elseSeq := doLetElse[7]
let bodySeq := doLetElse[8][0]
-- "let " >> optional "mut " >> termParser >> " := " >> termParser >> (checkColGt >> " | " >> doSeq) >> optional doSeq
let pattern := doLetElse[2]
let val := doLetElse[4]
let elseSeq := doLetElse[6]
let bodySeq := doLetElse[7][0]
let contSeq if isMutableLet doLetElse then
let vars ( getPatternVarsEx pattern).mapM fun var => `(doElem| let mut $var := $var)
pure (vars ++ (getDoSeqElems bodySeq).toArray)

View File

@@ -1042,16 +1042,7 @@ def mkRedundantAlternativeMsg (altName? : Option Name) (altMsg? : Option Message
def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : TermElabM Unit := do
unless result.counterExamples.isEmpty do
let maxCEx := Meta.Match.match.maxCounterExamples.get ( getOptions)
let (shown, truncated) :=
if result.counterExamples.size > maxCEx then
(result.counterExamples.take maxCEx, true)
else
(result.counterExamples, false)
let mut msg := m!"Missing cases:\n{Meta.Match.counterExamplesToMessageData shown}"
if truncated then
msg := msg ++ m!"\n(further cases omitted, increase `set_option match.maxCounterExamples {maxCEx}` to see more)"
withHeadRefOnly <| logError msg
withHeadRefOnly <| logError m!"Missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
return ()
unless match.ignoreUnusedAlts.get ( getOptions) || result.unusedAltIdxs.isEmpty do
let mut i := 0

View File

@@ -69,8 +69,6 @@ private def throwCtorExpected {α} (ident : Option Syntax) : M α := do
if candidates.size = 0 then
throwError message
-- Sort for deterministic output (iteration order of `env.constants` is not stable)
candidates := candidates.qsort Name.lt
let oneOfThese := if h : candidates.size = 1 then m!"`{candidates[0]}`" else m!"one of these"
let hint m!"Using {oneOfThese} would be valid:".hint (ref? := idStx) (candidates.map fun candidate => {
suggestion := mkIdent candidate
@@ -322,7 +320,7 @@ where
if f.getKind == ``Parser.Term.dotIdent then
let namedArgsNew namedArgs.mapM fun
-- We must ensure that `ref[1]` remains original to allow named-argument hints
| { ref, name, val := Arg.stx arg, .. } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(ref[1]) := $( collect arg)))
| { ref, name, val := Arg.stx arg } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(ref[1]) := $( collect arg)))
| _ => unreachable!
let mut argsNew args.mapM fun | Arg.stx arg => collect arg | _ => unreachable!
if ellipsis then

View File

@@ -12,11 +12,6 @@ public import Init.Syntax
public section
namespace Lean.Elab
register_builtin_option linter.deprecated.options : Bool := {
defValue := true
descr := "if true, generate deprecation warnings for deprecated options"
}
variable [Monad m] [MonadOptions m] [MonadError m] [MonadLiftT (EIO Exception) m] [MonadInfoTree m]
private def throwUnconfigurable {α} (optionName : Name) : m α :=
@@ -48,7 +43,7 @@ where
{indentExpr defValType}"
| _ => throwUnconfigurable optionName
def elabSetOption (id : Syntax) (val : Syntax) : m (Options × OptionDecl) := do
def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
let ref getRef
-- For completion purposes, we discard `val` and any later arguments.
-- We include the first argument (the keyword) for position information in case `id` is `missing`.
@@ -56,9 +51,9 @@ def elabSetOption (id : Syntax) (val : Syntax) : m (Options × OptionDecl) := do
let optionName := id.getId.eraseMacroScopes
let decl IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
let rec setOption (val : DataValue) : m (Options × OptionDecl) := do
let rec setOption (val : DataValue) : m Options := do
validateOptionValue optionName decl val
return (( getOptions).set optionName val, decl)
return ( getOptions).set optionName val
match val.isStrLit? with
| some str => setOption (DataValue.ofString str)
| none =>
@@ -75,17 +70,3 @@ def elabSetOption (id : Syntax) (val : Syntax) : m (Options × OptionDecl) := do
throwUnconfigurable optionName
end Lean.Elab
namespace Lean.Elab
variable {m : Type Type} [Monad m] [MonadOptions m] [MonadLog m] [AddMessageContext m]
def checkDeprecatedOption (optionName : Name) (decl : OptionDecl) : m Unit := do
unless linter.deprecated.options.get ( getOptions) do return
let some dep := decl.deprecation? | return
let extraMsg := match dep.text? with
| some text => m!": {text}"
| none => m!""
logWarning m!"`{optionName}` has been deprecated{extraMsg}"
end Lean.Elab

View File

@@ -574,14 +574,8 @@ private def addSourceFields (structName : Name) (sources : Array ExplicitSourceV
private structure StructInstContext where
view : StructInstView
/-- If true, then try using parent instances for missing fields. -/
useParentInstanceFields : Bool
/-- If true, then try using default values or autoParams for missing fields.
(Considered after `useParentInstanceFields`.) -/
useDefaults : Bool
/-- If true, then missing fields after default value synthesis remain as metavariables rather than yielding an error.
Only applies if `useDefaults` is true. -/
unsynthesizedAsMVars : Bool
/-- True if the structure instance has a trailing `..`. -/
ellipsis : Bool
structName : Name
structType : Expr
/-- Structure universe levels. -/
@@ -754,8 +748,6 @@ private structure PendingField where
deps : NameSet
val? : Option Expr
private def registerFieldMVarError (e : Expr) (ref : Syntax) (fieldName : Name) : StructInstM Unit :=
registerCustomErrorIfMVar e ref m!"Cannot synthesize placeholder for field `{fieldName}`"
/--
Synthesize pending optParams.
@@ -786,7 +778,7 @@ private def synthOptParamFields : StructInstM Unit := do
-- Process default values for pending optParam fields.
let mut pendingFields : Array PendingField optParamFields.filterMapM fun (fieldName, fieldType, required) => do
if required || ( isFieldNotSolved? fieldName).isSome then
let (deps, val?) if ( read).useDefaults then getFieldDefaultValue? fieldName else pure ({}, none)
let (deps, val?) getFieldDefaultValue? fieldName
if let some val := val? then
trace[Elab.struct] "default value for {fieldName}:{indentExpr val}"
else
@@ -839,46 +831,44 @@ private def synthOptParamFields : StructInstM Unit := do
pending
toRemove := toRemove.push selected.fieldName
if toRemove.isEmpty then
return handleStuck pendingFields assignErrors
if ( read).ellipsis then
for pendingField in pendingFields do
if let some mvarId isFieldNotSolved? pendingField.fieldName then
registerCustomErrorIfMVar (.mvar mvarId) ( read).view.ref m!"\
Cannot synthesize placeholder for field `{pendingField.fieldName}`"
return
let assignErrorsMsg := MessageData.joinSep (assignErrors.map (m!"\n\n" ++ ·)).toList ""
let mut requiredErrors : Array MessageData := #[]
let mut unsolvedFields : Std.HashSet Name := {}
for pendingField in pendingFields do
if ( isFieldNotSolved? pendingField.fieldName).isNone then
unsolvedFields := unsolvedFields.insert pendingField.fieldName
let e := ( get).fieldMap.get! pendingField.fieldName
requiredErrors := requiredErrors.push m!"\
Field `{pendingField.fieldName}` must be explicitly provided; its synthesized value is{indentExpr e}"
let requiredErrorsMsg := MessageData.joinSep (requiredErrors.map (m!"\n\n" ++ ·)).toList ""
let missingFields := pendingFields |>.filter (fun pending => pending.val?.isNone)
-- TODO(kmill): when fields are all stuck, report better.
-- For now, just report all pending fields in case there are no obviously missing ones.
let missingFields := if missingFields.isEmpty then pendingFields else missingFields
let missing := missingFields |>.map (s!"`{·.fieldName}`") |>.toList
let missingFieldsValues missingFields.mapM fun field => do
if unsolvedFields.contains field.fieldName then
pure <| (field.fieldName, some <| ( get).fieldMap.get! field.fieldName)
else pure (field.fieldName, none)
let missingFieldsHint mkMissingFieldsHint missingFieldsValues ( read).view.ref
let msg := m!"Fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}{missingFieldsHint}"
if ( readThe Term.Context).errToSorry then
-- Assign all pending problems using synthetic sorries and log an error.
for pendingField in pendingFields do
if let some mvarId isFieldNotSolved? pendingField.fieldName then
mvarId.assign <| mkLabeledSorry ( mvarId.getType) (synthetic := true) (unique := true)
logError msg
return
else
throwError msg
pendingSet := pendingSet.filter (!toRemove.contains ·)
pendingFields := pendingFields.filter fun pendingField => pendingField.val?.isNone || !toRemove.contains pendingField.fieldName
where
handleStuck (pendingFields : Array PendingField) (assignErrors : Array MessageData) : StructInstM Unit := do
if ( read).unsynthesizedAsMVars then
for pendingField in pendingFields do
if let some mvarId isFieldNotSolved? pendingField.fieldName then
registerFieldMVarError (.mvar mvarId) ( read).view.ref pendingField.fieldName
return
let assignErrorsMsg := MessageData.joinSep (assignErrors.map (m!"\n\n" ++ ·)).toList ""
let mut requiredErrors : Array MessageData := #[]
let mut unsolvedFields : Std.HashSet Name := {}
for pendingField in pendingFields do
if ( isFieldNotSolved? pendingField.fieldName).isNone then
unsolvedFields := unsolvedFields.insert pendingField.fieldName
let e := ( get).fieldMap.get! pendingField.fieldName
requiredErrors := requiredErrors.push m!"\
Field `{pendingField.fieldName}` must be explicitly provided; its synthesized value is{indentExpr e}"
let requiredErrorsMsg := MessageData.joinSep (requiredErrors.map (m!"\n\n" ++ ·)).toList ""
let missingFields := pendingFields |>.filter (fun pending => pending.val?.isNone)
-- TODO(kmill): when fields are all stuck, report better.
-- For now, just report all pending fields in case there are no obviously missing ones.
let missingFields := if missingFields.isEmpty then pendingFields else missingFields
let missing := missingFields |>.map (s!"`{·.fieldName}`") |>.toList
let missingFieldsValues missingFields.mapM fun field => do
if unsolvedFields.contains field.fieldName then
pure <| (field.fieldName, some <| ( get).fieldMap.get! field.fieldName)
else pure (field.fieldName, none)
let missingFieldsHint mkMissingFieldsHint missingFieldsValues ( read).view.ref
let msg := m!"Fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}{missingFieldsHint}"
if ( readThe Term.Context).errToSorry then
-- Assign all pending problems using synthetic sorries and log an error.
for pendingField in pendingFields do
if let some mvarId isFieldNotSolved? pendingField.fieldName then
mvarId.assign <| mkLabeledSorry ( mvarId.getType) (synthetic := true) (unique := true)
logError msg
return
else
throwError msg
private def finalize : StructInstM Expr := withViewRef do
let val := ( read).val.beta ( get).fields
@@ -1059,13 +1049,19 @@ These fields can still be solved for by parent instance synthesis later.
-/
private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : BinderInfo) (fieldType : Expr) : StructInstM α := do
trace[Elab.struct] "processNoField `{fieldName}` of type {fieldType}"
if ( read).useDefaults then
if ( read).ellipsis && ( readThe Term.Context).inPattern then
-- See the note in `ElabAppArgs.processExplicitArg`
-- In ellipsis & pattern mode, do not use optParams or autoParams.
let e addStructFieldMVar fieldName fieldType
registerCustomErrorIfMVar e ( read).view.ref m!"don't know how to synthesize placeholder for field `{fieldName}`"
loop
else
let autoParam? := fieldType.getAutoParamTactic?
let fieldType := fieldType.consumeTypeAnnotations
if binfo.isInstImplicit then
let e addStructFieldMVar fieldName fieldType .synthetic
modify fun s => { s with instMVars := s.instMVars.push e.mvarId! }
return loop
loop
else if let some (.const tacticDecl ..) := autoParam? then
match evalSyntaxConstant ( getEnv) ( getOptions) tacticDecl with
| .error err => throwError err
@@ -1082,11 +1078,12 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
-- (See `processExplicitArg` for a comment about this.)
addTermInfo' stx mvar
addStructFieldAux fieldName mvar
return loop
-- Default case: natural metavariable, register it for optParams
discard <| addStructFieldMVar fieldName fieldType
modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
loop
loop
else
-- Default case: natural metavariable, register it for optParams
discard <| addStructFieldMVar fieldName fieldType
modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
loop
private partial def loop : StructInstM Expr := withViewRef do
let type := ( get).type
@@ -1181,7 +1178,8 @@ private partial def addParentInstanceFields : StructInstM Unit := do
private def main : StructInstM Expr := do
initializeState
if ( read).useParentInstanceFields then
unless ( read).ellipsis && ( readThe Term.Context).inPattern do
-- Inside a pattern with ellipsis mode, users expect to match just the fields provided.
addParentInstanceFields
loop
@@ -1200,17 +1198,7 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
trace[Elab.struct] "expanded fields:\n{MessageData.joinSep (fields.toList.map (fun (_, field) => m!"- {MessageData.nestD (toMessageData field)}")) "\n"}"
let ellipsis := s.sources.implicit.isSome
let (val, _) main
|>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn
-- See the note in `ElabAppArgs.processExplicitArg`
-- For structure instances though, there's a sense in which app-style ellipsis mode is always enabled,
-- so we do not specifically check for it to disable defaults.
-- An effect of this is that if a user forgets `..` they'll be reminded with a "Fields missing" error.
useDefaults := !( readThe Term.Context).inPattern
-- Similarly, for patterns we disable using parent instances to fill in fields
useParentInstanceFields := !( readThe Term.Context).inPattern
-- In ellipsis mode, unsynthesized missing fields become metavariables, rather than being an error
unsynthesizedAsMVars := ellipsis
}
|>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn, ellipsis }
|>.run { type := ctorFnType }
return val

View File

@@ -190,8 +190,7 @@ private def getOptRotation (stx : Syntax) : Nat :=
popScope
@[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
let (options, decl) Elab.elabSetOption stx[1] stx[3]
withRef stx[1] <| Elab.checkDeprecatedOption (stx[1].getId.eraseMacroScopes) decl
let options Elab.elabSetOption stx[1] stx[3]
withOptions (fun _ => options) do
try
evalTactic stx[5]

View File

@@ -437,8 +437,7 @@ where
replaceMainGoal [{ goal with mvarId }]
@[builtin_grind_tactic setOption] def elabSetOption : GrindTactic := fun stx => do
let (options, decl) Elab.elabSetOption stx[1] stx[3]
withRef stx[1] <| Elab.checkDeprecatedOption (stx[1].getId.eraseMacroScopes) decl
let options Elab.elabSetOption stx[1] stx[3]
withOptions (fun _ => options) do evalGrindTactic stx[5]
@[builtin_grind_tactic setConfig] def elabSetConfig : GrindTactic := fun stx => do

View File

@@ -2124,14 +2124,11 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
let const withoutCheckDeprecated <| mkConst declName explicitLevels
return (const, projs) :: result
def throwInvalidExplicitUniversesForLocal {α} (e : Expr) : TermElabM α :=
throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) ( getLCtx) expectedType?
if let some (e, projs) resolveLocalName n then
unless explicitLevels.isEmpty do
throwInvalidExplicitUniversesForLocal e
throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
return [(e, projs)]
let preresolved := preresolved.filterMap fun
| .decl n projs => some (n, projs)

View File

@@ -2255,13 +2255,13 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
return data
let numPrivateConsts := moduleData.foldl (init := 0) fun numPrivateConsts data =>
numPrivateConsts + data.constants.size
let numExtraConsts := irData.foldl (init := 0) fun numExtraConsts data =>
numExtraConsts + data.extraConstNames.size
let numPrivateConsts := irData.foldl (init := numPrivateConsts) fun numPrivateConsts data =>
numPrivateConsts + data.extraConstNames.size
let numPublicConsts := modules.foldl (init := 0) fun numPublicConsts mod => Id.run do
if !mod.isExported then numPublicConsts else
let some data := mod.publicModule? | numPublicConsts
numPublicConsts + data.constants.size
let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts + numExtraConsts)
let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts + numPublicConsts)
let mut privateConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts)
let mut publicConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPublicConsts)
for h : modIdx in *...moduleData.size do

View File

@@ -314,7 +314,7 @@ def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"
@[builtin_missing_docs_handler «in»]
def handleIn : Handler := fun _ stx => do
if stx[0].getKind == ``«set_option» then
let (opts, _) Elab.elabSetOption stx[0][1] stx[0][3]
let opts Elab.elabSetOption stx[0][1] stx[0][3]
withScope (fun scope => { scope with opts }) do
missingDocs.run stx[2]
else

View File

@@ -19,7 +19,6 @@ namespace Lean.Meta
register_builtin_option backward.eqns.nonrecursive : Bool := {
defValue := true
descr := "Create fine-grained equational lemmas even for non-recursive definitions."
deprecation? := some { since := "2026-03-30" }
}
register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
@@ -29,7 +28,6 @@ register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
that do not contain recursive calls do not cause further splits in the \
equational lemmas. This was the behavior before Lean 4.12, and the purpose of \
this option is to help migrating old code."
deprecation? := some { since := "2026-03-30" }
}

View File

@@ -180,14 +180,12 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
@[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do
if !( read).cacheInferType || e.hasMVar then
Core.checkInterrupted
inferType
else
let key mkExprConfigCacheKey e
match ( get).cache.inferType.find? key with
| some type => return type
| none =>
Core.checkInterrupted
let type inferType
unless type.hasMVar do
modifyInferTypeCache fun c => c.insert key type

View File

@@ -256,12 +256,12 @@ abbrev CounterExample := List Example
def counterExampleToMessageData (cex : CounterExample) : MessageData :=
examplesToMessageData cex
def counterExamplesToMessageData (cexs : Array CounterExample) : MessageData :=
MessageData.joinSep (cexs.toList.map counterExampleToMessageData) Format.line
def counterExamplesToMessageData (cexs : List CounterExample) : MessageData :=
MessageData.joinSep (cexs.map counterExampleToMessageData) Format.line
structure MatcherResult where
matcher : Expr -- The matcher. It is not just `Expr.const matcherName` because the type of the major premises may contain free variables.
counterExamples : Array CounterExample
counterExamples : List CounterExample
unusedAltIdxs : List Nat
addMatcher : MetaM Unit

View File

@@ -78,14 +78,6 @@ register_builtin_option backward.match.rowMajor : Bool := {
it splits them from left to right, which can lead to unnecessary code bloat."
}
register_builtin_option match.maxCounterExamples : Nat := {
defValue := 5
descr := "Maximum number of missing-case counter-examples to generate. \
When this limit is reached, the match compiler stops exploring further \
case splits for counter-example generation. Increase if you need to see \
all missing cases."
}
private def mkIncorrectNumberOfPatternsMsg [ToMessageData α]
(discrepancyKind : String) (expected actual : Nat) (pats : List α) :=
let patternsMsg := MessageData.joinSep (pats.map toMessageData) ", "
@@ -210,7 +202,7 @@ structure State where
Used during splitter generation to avoid going through all pairs of patterns.
-/
overlaps : Overlaps := {}
counterExamples : Array (List Example) := #[]
counterExamples : List (List Example) := []
/-- Return true if the given (sub-)problem has been solved. -/
private def isDone (p : Problem) : Bool :=
@@ -277,16 +269,10 @@ def isCurrVarInductive (p : Problem) : MetaM Bool := do
let val? getInductiveVal? x
return val?.isSome
private def isConstructorTransition (p : Problem) : StateRefT State MetaM Bool := do
if !( isCurrVarInductive p) then return false
if p.alts.isEmpty then
/- When there are no alternatives left and we have already accumulated enough
counter-examples, stop exploring further case splits. This prevents
combinatorial explosion when generating "missing cases" diagnostics. -/
let maxCEx := match.maxCounterExamples.get ( getOptions)
return ( get).counterExamples.size < maxCEx
else
return hasCtorPattern p && p.alts.all fun alt => match alt.patterns with
private def isConstructorTransition (p : Problem) : MetaM Bool := do
return ( isCurrVarInductive p)
&& (hasCtorPattern p || p.alts.isEmpty)
&& p.alts.all fun alt => match alt.patterns with
| .ctor .. :: _ => true
| .inaccessible _ :: _ => true -- should be a done pattern by now
| _ => false
@@ -481,7 +467,7 @@ where
trace[Meta.Match.match] "contradiction succeeded"
else
trace[Meta.Match.match] "contradiction failed, missing alternative"
modify fun s => { s with counterExamples := s.counterExamples.push p.examples }
modify fun s => { s with counterExamples := p.examples :: s.counterExamples }
| alt :: overlapped =>
solveCnstrs p.mvarId alt
for otherAlt in overlapped do

View File

@@ -97,16 +97,4 @@ public def mkLambdaFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
let type abstractFVarsRange decl.type i xs
mkLambdaS decl.userName decl.binderInfo type b
/--
Similar to `mkForallFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`,
and makes the same assumption made by these functions.
-/
public def mkForallFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
let b abstractFVars e xs
xs.size.foldRevM (init := b) fun i _ b => do
let x := xs[i]
let decl x.fvarId!.getDecl
let type abstractFVarsRange decl.type i xs
mkForallS decl.userName decl.binderInfo type b
end Lean.Meta.Sym

View File

@@ -189,48 +189,4 @@ def mkAppS₄ (f a₁ a₂ a₃ a₄ : Expr) : m Expr := do
def mkAppS₅ (f a₁ a₂ a₃ a₄ a₅ : Expr) : m Expr := do
mkAppS ( mkAppS₄ f a₁ a₂ a₃ a₄) a₅
def mkAppS₆ (f a₁ a₂ a₃ a₄ a₅ a₆ : Expr) : m Expr := do
mkAppS ( mkAppS₅ f a₁ a₂ a₃ a₄ a₅) a₆
def mkAppS₇ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ : Expr) : m Expr := do
mkAppS ( mkAppS₆ f a₁ a₂ a₃ a₄ a₅ a₆) a₇
def mkAppS₈ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : Expr) : m Expr := do
mkAppS ( mkAppS₇ f a₁ a₂ a₃ a₄ a₅ a₆ a₇) a₈
def mkAppS₉ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : Expr) : m Expr := do
mkAppS ( mkAppS₈ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈) a₉
def mkAppS₁₀ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ : Expr) : m Expr := do
mkAppS ( mkAppS₉ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) a₁₀
def mkAppS₁₁ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ a₁₁ : Expr) : m Expr := do
mkAppS ( mkAppS₁₀ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀) a₁₁
/-- `mkAppRangeS f i j #[a₀, ..., aᵢ, ..., aⱼ, ...]` ==> `f aᵢ ... aⱼ₋₁` with max sharing. -/
partial def mkAppRangeS (f : Expr) (beginIdx endIdx : Nat) (args : Array Expr) : m Expr :=
go endIdx f beginIdx
where
go (endIdx : Nat) (b : Expr) (i : Nat) : m Expr := do
if endIdx i then return b
else go endIdx ( mkAppS b args[i]!) (i + 1)
/-- `mkAppNS f #[a₀, ..., aₙ]` constructs `f a₀ ... aₙ` with max sharing. -/
def mkAppNS (f : Expr) (args : Array Expr) : m Expr :=
mkAppRangeS f 0 args.size args
/-- `mkAppRevRangeS f b e revArgs` ==> `mkAppRev f (revArgs.extract b e)` with max sharing. -/
partial def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : m Expr :=
go revArgs beginIdx f endIdx
where
go (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : m Expr := do
if i start then return b
else
let i := i - 1
go revArgs start ( mkAppS b revArgs[i]!) i
/-- Same as `mkAppS f args` but reversing `args`, with max sharing. -/
def mkAppRevS (f : Expr) (revArgs : Array Expr) : m Expr :=
mkAppRevRangeS f 0 revArgs.size revArgs
end Lean.Meta.Sym.Internal

View File

@@ -24,19 +24,14 @@ builtin_initialize registerTraceClass `sym.debug.canon
Canonicalizes expressions by normalizing types and instances. At the top level, it traverses
applications, foralls, lambdas, and let-bindings, classifying each argument as a type, instance,
implicit, or value using `shouldCanon`. Targeted reductions (projection, match/ite/cond, Nat
arithmetic) are applied to all positions; instances are re-synthesized.
implicit, or value using `shouldCanon`. Values are recursively visited but not normalized.
Types and instances receive targeted reductions.
**Note about types:** `grind` is not built for reasoning about types that are not propositions.
We assume that definitionally equal types will be structurally identical after we apply the
canonicalizer. We also erase most of the subsingleton markers occurring inside types.
## Reductions
It also normalizes expressions using the following reductions. We can view it as a cheap/custom `dsimp`.
We used to reduce only terms inside types, but it restricted important normalizations that were important
when, for example, a term had a forward dependency. That is, the term is not directly in a type, but
there is a type that depends on it.
## Reductions (applied only in type positions)
- **Eta**: `fun x => f x` → `f`
- **Projection**: `⟨a, b⟩.1` → `a` (structure projections, not class projections)
@@ -44,9 +39,6 @@ there is a type that depends on it.
- **Nat arithmetic**: ground evaluation (`2 + 1` → `3`) and offset normalization
(`n.succ + 1` → `n + 2`)
**Note**: Eta is applied only if the lambda is occurring inside of a type. For lambdas occurring
in non type positions, we want to leverage the support in `grind` for lambda-expressions.
## Instance canonicalization
Instances are re-synthesized via `synthInstance`. The instance type is first normalized
@@ -63,11 +55,7 @@ produce the same canonical instance. Two special cases:
canonicalized, then the proof is re-synthesized. If resynthesis fails, the original
proof is kept. No definitional-equality check is needed thanks to proof irrelevance.
In both cases, resynthesis failure is silent — the original instance or proof is kept.
Ideally we would report an issue when resynthesis fails inside a type (where structural
agreement matters most), but in practice users provide non-synthesizable instances via `haveI`,
and these instances propagate into types through forward dependencies. Reporting failures
for such instances produces noise that obscures real issues.
Inside types, both cases are strict: resynthesis failure is reported as an issue.
## Two caches
@@ -241,7 +229,7 @@ def checkDefEqInst (e : Expr) (inst : Expr) : SymM Expr := do
return e
return inst
/-- Canonicalize `e`. Applies targeted reductions and re-synthesizes instances. -/
/-- Canonicalize `e`. Applies targeted reductions in type positions; recursively visits value positions. -/
partial def canon (e : Expr) : CanonM Expr := do
match e with
| .forallE .. => withCaching e <| canonForall #[] e
@@ -276,12 +264,11 @@ where
/--
Canonicalize `e : type` where `e` is an instance by trying to resynthesize `type`.
If `report` is `true`, we report an issue when the instance cannot be resynthesized.
We report an issue if the instance cannot be resynthesized.
-/
canonInstCore (e : Expr) (type : Expr) (report := true) : CanonM Expr := do
canonInstCore (e : Expr) (type : Expr) : CanonM Expr := do
let some inst Sym.synthInstance? type |
if report then
reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type}"
reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type}"
return e
checkDefEqInst e inst
@@ -289,18 +276,18 @@ where
Canonicalize an instance by trying to resynthesize it without caching.
Recall that we have special support for `Decidable` and propositional instances.
-/
canonInst' (e : Expr) (report := true) : CanonM Expr := do
canonInst' (e : Expr) : CanonM Expr := do
/-
We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
the same instances.
-/
let type inferType e
let type' canonInsideType' type
canonInstCore e type' report
canonInstCore e type'
/-- `withCaching` + `canonInst'` -/
canonInst (e : Expr) (report := true) : CanonM Expr := withCaching e do
canonInst' e report
canonInst (e : Expr) : CanonM Expr := withCaching e do
canonInst' e
/--
Canonicalize a proposition that is also a term instance.
@@ -313,9 +300,7 @@ where
canonInstProp (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
let prop' canon prop
if ( read).insideType then
/- We suppress reporting here because `haveI`-provided instances propagate into types
through forward dependencies, and reporting them produces noise. See module doc. -/
canonInstCore h prop' (report := false)
canonInstCore h prop'
else
/-
**Note**: We try to resynthesize the proposition, but if it fails we keep the current one.
@@ -337,8 +322,7 @@ where
let prop' canon prop
let type := mkApp (mkConst ``Decidable) prop'
if ( read).insideType then
/- See comment in `canonInstProp` for why we suppress reporting here. -/
canonInstCore inst type (report := false)
canonInstCore inst type
else
/-
**Note**: We try to resynthesize the instance, but if it fails we keep the current one.
@@ -354,12 +338,6 @@ where
canonInstDec (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
canonInstDec' g prop h e
/-- `canonInstDec` variant for normalizing `if-then-else` expressions. -/
canonInstDecCore (e : Expr) : CanonM Expr := do
match_expr e with
| g@Grind.nestedDecidable prop inst => canonInstDec g prop inst e
| _ => canonInst e (report := false)
canonLambda (e : Expr) : CanonM Expr := do
if ( read).insideType then
canonLambdaLoop #[] (etaReduce e)
@@ -440,7 +418,7 @@ where
let c canon c
if isTrueCond c then canon a
else if isFalseCond c then canon b
else return mkApp5 f ( canonInsideType α) c ( canonInstDecCore inst) ( canon a) ( canon b)
else return mkApp5 f ( canonInsideType α) c ( canonInst inst) ( canon a) ( canon b)
canonCond (f : Expr) (α c a b : Expr) : CanonM Expr := do
let c canon c
@@ -481,21 +459,27 @@ where
return e
canonApp (e : Expr) : CanonM Expr := do
match_expr e with
| f@ite α c i a b => canonIte f α c i a b
| f@cond α c a b => canonCond f α c a b
-- Remark: We currently don't normalize dependent-if-then-else occurring in types.
| _ =>
let f := e.getAppFn
let .const declName _ := f | canonAppAndPost e
if ( isMatcher declName) then
canonMatch e
else
canonAppAndPost e
if ( read).insideType then
match_expr e with
| f@ite α c i a b => canonIte f α c i a b
| f@cond α c a b => canonCond f α c a b
-- Remark: We currently don't normalize dependent-if-then-else occurring in types.
| _ =>
let f := e.getAppFn
let .const declName _ := f | canonAppAndPost e
if ( isMatcher declName) then
canonMatch e
else
canonAppAndPost e
else
canonAppDefault e
canonProj (e : Expr) : CanonM Expr := do
let e := e.updateProj! ( canon e.projExpr!)
return ( reduceProj? e).getD e
if ( read).insideType then
return ( reduceProj? e).getD e
else
return e
/--
Returns `true` if `shouldCanon pinfos i arg` is not `.visit`.
@@ -509,8 +493,8 @@ end Canon
/--
Canonicalize `e` by normalizing types, instances, and support arguments.
Applies targeted reductions (projection, match/ite/cond, Nat arithmetic) in all positions;
eta reduction is applied only inside types. Instances are re-synthesized.
Types receive targeted reductions (eta, projection, match/ite, Nat arithmetic).
Instances are re-synthesized. Values are traversed but not reduced.
Runs at reducible transparency.
-/
public def canon (e : Expr) : SymM Expr := do profileitM Exception "sym canon" ( getOptions) do

View File

@@ -86,8 +86,22 @@ It assumes the input is maximally shared, and ensures the output is too.
public def instantiateS (e : Expr) (subst : Array Expr) : SymM Expr :=
liftBuilderM <| instantiateS' e subst
/-- Internal variant of `betaRevS` that runs in `AlphaShareBuilderM`. -/
private partial def betaRevS' (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
/-- `mkAppRevRangeS f b e args == mkAppRev f (revArgs.extract b e)` -/
def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
loop revArgs beginIdx f endIdx
where
loop (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : AlphaShareBuilderM Expr := do
if i start then
return b
else
let i := i - 1
loop revArgs start ( mkAppS b revArgs[i]!) i
/--
Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
-/
partial def betaRevS (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
if revArgs.size == 0 then
return f
else
@@ -159,7 +173,7 @@ where
| .bvar bidx =>
let f' visitBVar f bidx offset
if modified || !isSameExpr f f' then
betaRevS' f' argsRev
betaRevS f' argsRev
else
return e
| _ => unreachable!
@@ -201,18 +215,4 @@ public def instantiateRevBetaS (e : Expr) (subst : Array Expr) : SymM Expr := do
if !e.hasLooseBVars || subst.isEmpty then return e
else liftBuilderM <| instantiateRevBetaS' e subst
/--
Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
-/
public def betaRevS (f : Expr) (revArgs : Array Expr) : SymM Expr :=
liftBuilderM <| betaRevS' f revArgs
/--
Apply the given arguments to `f`, beta-reducing if `f` is a lambda expression,
ensuring maximally shared terms. See `betaRevS` for details.
-/
public def betaS (f : Expr) (args : Array Expr) : SymM Expr :=
betaRevS f args.reverse
end Lean.Meta.Sym

View File

@@ -283,7 +283,6 @@ def handleProj : Simproc := fun e => do
let newProof mkEqOfHEq newProof (check := false)
return .step ( Lean.Expr.updateProjS! e e') newProof
open Sym.Internal in
/--
For an application whose head is neither a constant nor a lambda (e.g. a projection
like `p.1 x`), simplify the function head and lift the proof via `congrArg`.

View File

@@ -24,6 +24,9 @@ namespace Lean.Meta.Tactic.Cbv
open Lean.Meta.Sym.Simp
public def mkAppNS (f : Expr) (args : Array Expr) : Sym.SymM Expr := do
args.foldlM Sym.Internal.mkAppS f
abbrev isNatValue (e : Expr) : Bool := (Sym.getNatValue? e).isSome
abbrev isStringValue (e : Expr) : Bool := (Sym.getStringValue? e).isSome
abbrev isIntValue (e : Expr) : Bool := (Sym.getIntValue? e).isSome

View File

@@ -67,9 +67,9 @@ def notFollowedByRedefinedTermToken :=
"token at 'do' element"
@[builtin_doElem_parser] def doLet := leading_parser
"let " >> optional "mut " >> letConfig >> letDecl
"let " >> optional "mut " >> letDecl
@[builtin_doElem_parser] def doLetElse := leading_parser withPosition <|
"let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >>
"let " >> optional "mut " >> termParser >> " := " >> termParser >>
(checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent)
@[builtin_doElem_parser] def doLetExpr := leading_parser withPosition <|
@@ -89,7 +89,7 @@ def doPatDecl := leading_parser
atomic (termParser >> optType >> ppSpace >> leftArrow) >>
doElemParser >> optional ((checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent))
@[builtin_doElem_parser] def doLetArrow := leading_parser withPosition <|
"let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
"let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
/-
We use `letIdDeclNoBinders` to define `doReassign`.
@@ -114,7 +114,7 @@ def letIdDeclNoBinders := leading_parser
@[builtin_doElem_parser] def doReassignArrow := leading_parser
notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
@[builtin_doElem_parser] def doHave := leading_parser
"have" >> Term.letConfig >> Term.letDecl
"have" >> Term.letDecl
/-
In `do` blocks, we support `if` without an `else`.
Thus, we use indentation to prevent examples such as

View File

@@ -882,19 +882,13 @@ the available context).
-/
def identProjKind := `Lean.Parser.Term.identProj
@[builtin_term_parser] def dotIdent := leading_parser
"." >> checkNoWsBefore >> rawIdent
def isIdent (stx : Syntax) : Bool :=
-- antiquotations should also be allowed where an identifier is expected
stx.isAntiquot || stx.isIdent
def isIdentOrDotIdent (stx : Syntax) : Bool :=
isIdent stx || stx.isOfKind ``dotIdent
/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
checkStackTop isIdentOrDotIdent "expected preceding identifier" >>
checkStackTop isIdent "expected preceding identifier" >>
checkNoWsBefore "no space before '.{'" >> ".{" >>
sepBy1 levelParser ", " >> "}"
/-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
@@ -982,6 +976,9 @@ appropriate parameter for the underlying monad's `ST` effects, then passes it to
@[builtin_term_parser] def dynamicQuot := withoutPosition <| leading_parser
"`(" >> ident >> "| " >> incQuotDepth (parserOfStack 1) >> ")"
@[builtin_term_parser] def dotIdent := leading_parser
"." >> checkNoWsBefore >> rawIdent
/--
Implementation of the `show_term` term elaborator.
-/

View File

@@ -619,9 +619,8 @@ private partial def collectStructFields
if s'.induct == parentName then
let (fieldValues, fields) collectStructFields structName levels params fields fieldValues s'
return (i + 1, fieldValues, fields)
/- Does this field have a default value? and if so, can we omit the field?
We cannot omit fields for patterns, since default values do not apply for them. -/
unless pure ( read).inPattern <||> getPPOption getPPStructureInstancesDefaults do
/- Does this field have a default value? and if so, can we omit the field? -/
unless getPPOption getPPStructureInstancesDefaults do
if let some defFn := getEffectiveDefaultFnForField? ( getEnv) structName fieldName then
-- Use `withNewMCtxDepth` to prevent delaborator from solving metavariables.
if let some (_, defValue) withNewMCtxDepth <| instantiateStructDefaultValueFn? defFn levels params (pure fieldValues.get?) then

View File

@@ -641,13 +641,13 @@ def processGenericRequest : RunnerM Unit := do
let params := params.setObjVal! "position" (toJson s.pos)
logResponse s.method params
def processDirective (_ws directive : String) (directiveTargetLineNo : Nat)
(directiveTargetColumn : Nat) : RunnerM Unit := do
def processDirective (ws directive : String) (directiveTargetLineNo : Nat) : RunnerM Unit := do
let directive := directive.drop 1
let colon := directive.find ':'
let method := directive.sliceTo colon |>.trimAscii |>.copy
-- TODO: correctly compute in presence of Unicode
let pos : Lsp.Position := { line := directiveTargetLineNo, character := directiveTargetColumn }
let directiveTargetColumn := ws.rawEndPos + "--"
let pos : Lsp.Position := { line := directiveTargetLineNo, character := directiveTargetColumn.byteIdx }
let params :=
if h : ¬colon.IsAtEnd then
directive.sliceFrom (colon.next h) |>.trimAscii.copy
@@ -686,15 +686,10 @@ def processLine (line : String) : RunnerM Unit := do
match directive.front with
| 'v' => pure <| ( get).lineNo + 1 -- TODO: support subsequent 'v'... or not
| '^' => pure <| ( get).lastActualLineNo
-- `⬑` is like `^` but targets the column of the `--` marker itself (i.e. column 0 when the
-- marker is at the start of the line), rather than the column after `--`.
| '' => pure <| ( get).lastActualLineNo
| _ =>
skipLineWithoutDirective
return
let directiveTargetColumn :=
if directive.front == '' then ws.rawEndPos.byteIdx else (ws.rawEndPos + "--").byteIdx
processDirective ws directive directiveTargetLineNo (directiveTargetColumn := directiveTargetColumn)
processDirective ws directive directiveTargetLineNo
skipLineWithDirective

View File

@@ -12,7 +12,6 @@ import Lean.Server.Watchdog
import Lean.Server.FileWorker
import Lean.Compiler.LCNF.EmitC
import Init.System.Platform
import Lean.Compiler.Options
/- Lean companion to `shell.cpp` -/
@@ -341,10 +340,7 @@ def ShellOptions.process (opts : ShellOptions)
| 'I' => -- `-I, --stdin`
return {opts with useStdin := true}
| 'r' => -- `--run`
return {opts with
run := true
-- can't get IR if it's postponed
leanOpts := Compiler.compiler.postponeCompile.set opts.leanOpts false }
return {opts with run := true}
| 'o' => -- `--o, olean=fname`
return {opts with oleanFileName? := checkOptArg "o" optArg?}
| 'i' => -- `--i, ilean=fname`

View File

@@ -57,19 +57,15 @@ def setConfigOption (opts : Options) (arg : String) : IO Options := do
public def main (args : List String) : IO UInt32 := do
let setupFile::irFile::c::optArgs := args | do
IO.println s!"usage: leanir <setup.json> <output.ir> <output.c> [--stat] <-Dopt=val>..."
IO.println s!"usage: leanir <setup.json> <module> <output.ir> <output.c> <-Dopt=val>..."
return 1
let setup ModuleSetup.load setupFile
let modName := setup.name
let mut printStats := false
let mut opts := setup.options.toOptions
for optArg in optArgs do
if optArg == "--stat" then
printStats := true
else
opts setConfigOption opts optArg
opts setConfigOption opts optArg
opts := Compiler.compiler.inLeanIR.set opts true
opts := maxHeartbeats.set opts 0
@@ -131,15 +127,12 @@ public def main (args : List String) : IO UInt32 := do
modifyEnv (postponedCompileDeclsExt.setState · (decls.foldl (fun s e => e.declNames.foldl (·.insert · e) s) {}))
for decl in decls do
for decl in decl.declNames do
try
resumeCompilation decl ( getOptions)
finally
addTraceAsMessages
for msg in ( Core.getAndEmptyMessageLog).unreported do
IO.eprintln ( msg.toString)
resumeCompilation decl
catch e =>
unless e.isInterrupt do
logError e.toMessageData
finally
addTraceAsMessages
let .ok (_, s) := res? | unreachable!
let env := s.env
@@ -162,6 +155,4 @@ public def main (args : List String) : IO UInt32 := do
out.write data.toUTF8
displayCumulativeProfilingTimes
if printStats then
env.displayStats
return 0

View File

@@ -7,7 +7,7 @@ module
prelude
public import Init.Dynamic
public import Init.Data.String.Basic
public import Init.Data.String
public import Std.Data.TreeMap
open Lean

View File

@@ -9,7 +9,6 @@ prelude
public import Std.Internal.Http.Data.Headers.Name
public import Std.Internal.Http.Data.Headers.Value
public import Std.Internal.Parsec.Basic
import Init.Data.String.Search
public section

View File

@@ -8,8 +8,6 @@ module
prelude
public import Init.Data.ToString
public import Std.Internal.Http.Internal
import Init.Data.String.Search
import Init.Data.String.Iter
public section
@@ -109,10 +107,10 @@ but since HTTP header names are case-insensitive, this always uses simple capita
-/
@[inline]
def toCanonical (name : Name) : String :=
let it := name.value.split '-'
|>.map (·.copy.capitalize)
let it := name.value.splitOn "-"
|>.map (·.capitalize)
it.intercalateString "-"
String.intercalate "-" it
/--
Performs a case-insensitive comparison between a `Name` and a `String`. Returns `true` if they match.

View File

@@ -10,7 +10,6 @@ import Init.Data.ToString
public import Std.Net
public import Std.Internal.Http.Internal
public import Std.Internal.Http.Data.URI.Encoding
public import Init.Data.String.Search
public section
@@ -165,8 +164,8 @@ Proposition that asserts `s` is a valid dot-separated domain name.
Each label must satisfy `IsValidDomainLabel`, and the full name must be at most 255 characters.
-/
abbrev IsValidDomainName (s : String) : Prop :=
let labels := s.split '.'
¬labels.isEmpty labels.all (fun s => isValidDomainLabel s.copy) s.length 255
let labels := s.splitOn "."
¬labels.isEmpty labels.all isValidDomainLabel s.length 255
/--
A domain name represented as a validated, lowercase-normalized string.

View File

@@ -12,7 +12,7 @@ import Init.Data.SInt.Lemmas
import Init.Data.UInt.Lemmas
import Init.Data.UInt.Bitwise
import Init.Data.Array.Lemmas
public import Init.Data.String.Basic
public import Init.Data.String
public import Std.Internal.Http.Internal.Char
public section

View File

@@ -7,12 +7,11 @@ module
prelude
import Init.While
public import Init.Data.String.Basic
public import Init.Data.String
public import Std.Internal.Parsec
public import Std.Internal.Parsec.ByteArray
public import Std.Internal.Http.Data.URI.Basic
public import Std.Internal.Http.Data.URI.Config
import Init.Data.String.Search
public section
@@ -280,13 +279,13 @@ private def parseQuery (config : URI.Config) : Parser URI.Query := do
if queryStr.isEmpty then
return URI.Query.empty
let rawPairs := queryStr.split '&'
let rawPairs := queryStr.splitOn "&"
if rawPairs.length > config.maxQueryParams then
fail s!"too many query parameters (limit: {config.maxQueryParams})"
let pairs : Option URI.Query := rawPairs.foldM (init := URI.Query.empty) fun acc pair => do
match pair.split '=' |>.toStringList with
let pairs : Option URI.Query := rawPairs.foldlM (init := URI.Query.empty) fun acc pair => do
match pair.splitOn "=" with
| [key] =>
let key URI.EncodedQueryParam.fromString? key
pure (acc.insertEncoded key none)

View File

@@ -7,7 +7,7 @@ module
prelude
import Init.Data.ToString
public import Init.Data.String.Basic
public import Init.Data.String
public section

View File

@@ -7,7 +7,7 @@ module
prelude
public import Init.Data.Char
public import Init.Data.String.Basic
public import Init.Data.String
public import Init.Data.Int
public import Init.Grind

View File

@@ -8,7 +8,7 @@ module
prelude
import Init.Data.ToString
import Init.Data.Array.Lemmas
public import Init.Data.String.Basic
public import Init.Data.String
public import Init.Data.ByteArray
public section

View File

@@ -9,8 +9,7 @@ prelude
import Init.Grind
import Init.Data.Int.OfNat
import Init.Data.UInt.Lemmas
public import Init.Data.String.Modify
import Init.Data.String.Lemmas.Modify
public import Init.Data.String
@[expose]
public section

View File

@@ -7,7 +7,7 @@ module
prelude
import Init.Grind
public import Init.Data.String.TakeDrop
public import Init.Data.String
public import Std.Internal.Http.Internal.Char
public section

View File

@@ -49,7 +49,7 @@ data_value mk_data_value(data_value_kind k, char const * val) {
extern "C" object * lean_register_option(obj_arg name, obj_arg decl);
void register_option(name const & n, name const & decl_name, data_value_kind k, char const * default_value, char const * description) {
object_ref decl = mk_cnstr(0, n, decl_name, mk_data_value(k, default_value), string_ref(description), object_ref(lean_box(0)));
object_ref decl = mk_cnstr(0, n, decl_name, mk_data_value(k, default_value), string_ref(description));
consume_io_result(lean_register_option(n.to_obj_arg(), decl.to_obj_arg()));
}
}

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

Binary file not shown.

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