feat: add Cslib/Foundations/Data/OmegaSequence/* #90
Conversation
|
Removed a bunch of API functions and associated theorems which probably won't be needed. |
ctchou
force-pushed
the
omega-sequence-candidate
branch
from
87b4bf0 to
d45f253
Compare
There was a problem hiding this comment.
I have mostly just reviewed the new extract code, as I don't want to spend too much time re-reviewing the old Stream'.
I didn't suggest explicit choices for what should be annotated as grind and simp, but you can see some recurring theorems I use in the suggestions. If they seem okay, consider adding them so they don't have to be specified every time.
| coe s := s.get | ||
| coe_injective' := by | ||
| rintro ⟨get1⟩ ⟨get2⟩ | ||
| grind |
There was a problem hiding this comment.
I find this more readable:
| coe s := s.get | |
| coe_injective' := by | |
| rintro ⟨get1⟩ ⟨get2⟩ | |
| grind | |
| coe := ωSequence.get | |
| coe_injective' := by grind [ωSequence, Function.Injective] |
|
|
||
| /-- Iterates of a function as an ω-sequence. -/ | ||
| def iterate (f : α → α) (a : α) : ωSequence α := iterate' f a | ||
| where iterate' (f : α → α) (a : α) : ℕ → α |
There was a problem hiding this comment.
Maybe it would be best to move the where to a separate Function.iterate? Then I think the theorem below would just be equality with that by rfl. It seems awkward to have a theorem about equality to a match.
| (fun s₁ s₂ ⟨h₁, h₂, h₃⟩ => by rw [← h₂, ← h₃] ; grind) | ||
| (And.intro hh (And.intro ht₁ ht₂)) | ||
|
|
||
| theorem coinduction {s₁ s₂ : ωSequence α} : |
There was a problem hiding this comment.
If ωSequence is not meant to be emulating a coinductive type, do we need to port this from Stream'? Or is it useful in some other way?
|
|
||
| theorem extract_eq_take {xs : ωSequence α} {n : ℕ} : | ||
| xs.extract 0 n = xs.take n := by | ||
| simp only [extract_eq_drop_take, Nat.sub_zero, drop_zero] |
There was a problem hiding this comment.
Mathlib style is to not "squeeze terminal simps" i.e at the end of a proof not use only. Can you please remove all of these and minimize the the theorems specified in the [...]? This is considered to make these proofs a bit less fragile.
There was a problem hiding this comment.
(I ended up leaving exact suggestions for all of these, hopefully that makes it easier. As a reminder, you can commit suggestions from the UI here)
| rw [← h_eq] at h_fun ; simp only [heq_eq_eq, funext_iff, Fin.forall_iff] at h_fun | ||
| simp only [← h_eq, true_and] ; intro k h_k ; simp only [h_fun k h_k] |
There was a problem hiding this comment.
The HEq here is a pain, this is the most I could simplify:
| rw [← h_eq] at h_fun ; simp only [heq_eq_eq, funext_iff, Fin.forall_iff] at h_fun | |
| simp only [← h_eq, true_and] ; intro k h_k ; simp only [h_fun k h_k] | |
| rw [← h_eq] at h_fun | |
| simp_all [funext_iff, Fin.forall_iff] |
| ext k x ; rcases (show k < j - i ∨ ¬ k < j - i by omega) with h_k | h_k | ||
| <;> simp [extract_eq_ofFn, h_k] | ||
| · simp [(show i + k < n - m by omega), (show k < m + j - (m + i) by omega), Nat.add_assoc] | ||
| · simp only [(show ¬k < m + j - (m + i) by omega), IsEmpty.forall_iff] |
There was a problem hiding this comment.
| ext k x ; rcases (show k < j - i ∨ ¬ k < j - i by omega) with h_k | h_k | |
| <;> simp [extract_eq_ofFn, h_k] | |
| · simp [(show i + k < n - m by omega), (show k < m + j - (m + i) by omega), Nat.add_assoc] | |
| · simp only [(show ¬k < m + j - (m + i) by omega), IsEmpty.forall_iff] | |
| ext k | |
| cases Decidable.em (k < j - i) <;> grind [extract_eq_ofFn] |
|
|
||
| theorem extract_extract2 {xs : ωSequence α} {n i j : ℕ} (h : j ≤ n) : | ||
| (xs.extract 0 n).extract i j = xs.extract i j := by | ||
| simp only [extract_extract2' (show j ≤ n - 0 by omega), Nat.zero_add] |
There was a problem hiding this comment.
| simp only [extract_extract2' (show j ≤ n - 0 by omega), Nat.zero_add] | |
| grind [extract_extract2'] |
|
|
||
| theorem extract_extract1 {xs : ωSequence α} {n i : ℕ} : | ||
| (xs.extract 0 n).extract i = xs.extract i n := by | ||
| simp only [length_extract, extract_extract2 (show n ≤ n by omega), Nat.sub_zero] |
There was a problem hiding this comment.
| simp only [length_extract, extract_extract2 (show n ≤ n by omega), Nat.sub_zero] | |
| grind [extract_extract2, length_extract] |
| ext k x ; rcases (show k < n - m ∨ ¬ k < n - m by omega) with h_k | h_k | ||
| <;> simp (disch := omega) [extract_eq_drop_take, getElem?_take, get_drop] | ||
| <;> aesop |
There was a problem hiding this comment.
| ext k x ; rcases (show k < n - m ∨ ¬ k < n - m by omega) with h_k | h_k | |
| <;> simp (disch := omega) [extract_eq_drop_take, getElem?_take, get_drop] | |
| <;> aesop | |
| ext k | |
| cases Decidable.em (k < n - m) <;> | |
| grind [extract_eq_drop_take, getElem?_take, get_drop, length_take] |
| rw [← append_extract_extract h_mn (show n ≤ n + 1 by omega)] ; congr | ||
| simp only [extract_eq_drop_take, Nat.add_sub_cancel_left, take_one, get_drop, Nat.add_zero] | ||
|
|
||
| theorem extract_extract2' {xs : ωSequence α} {m n i j : ℕ} (h : j ≤ n - m) : |
There was a problem hiding this comment.
The names of these last theorems could be better, at minimum replacing the prime and maybe using subscripts for the numbers of there isn't a more descriptive name.
2 participants
This is the initial version of ωSequence with reference to:
https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Automata/near/543709917
This PR supercedes #80 and #86.
I would appreciate feedbacks on which theorems should be labeled with @[simp] and @[grind], especially those involving
extract, as I am not familiar with how that should be done.