From 4a941eb9471798ba849f203f03a7c5dab21da509 Mon Sep 17 00:00:00 2001 From: Vasily Nesterov Date: Mon, 9 Dec 2024 11:52:32 +0300 Subject: [PATCH 1/2] make Seq.recOn cases_eliminator --- Mathlib/Data/Seq/Parallel.lean | 4 +- Mathlib/Data/Seq/Seq.lean | 130 +++++++++++++++------------------ 2 files changed, 60 insertions(+), 74 deletions(-) diff --git a/Mathlib/Data/Seq/Parallel.lean b/Mathlib/Data/Seq/Parallel.lean index ee4bdac0f33db6..16ea3f436d55d5 100644 --- a/Mathlib/Data/Seq/Parallel.lean +++ b/Mathlib/Data/Seq/Parallel.lean @@ -157,9 +157,7 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T have TT : ∀ l', Terminates (corec parallel.aux1 (l', S.tail)) := by intro apply IH _ _ _ (Or.inr _) T - rw [a] - cases' S with f al - rfl + rw [a, Seq.get?_tail] induction' e : Seq.get? S 0 with o · have D : Seq.destruct S = none := by dsimp [Seq.destruct] diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean index 8b25a1d0c7c0a5..d45af9a0910ef3 100644 --- a/Mathlib/Data/Seq/Seq.lean +++ b/Mathlib/Data/Seq/Seq.lean @@ -150,8 +150,10 @@ theorem ge_stable (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n) have : s.get? m ≠ none := mt (s.le_stable m_le_n) this Option.ne_none_iff_exists'.mp this +@[simp] theorem not_mem_nil (a : α) : a ∉ @nil α := fun ⟨_, (h : some a = none)⟩ => by injection h +@[simp] theorem mem_cons (a : α) : ∀ s : Seq α, a ∈ cons a s | ⟨_, _⟩ => Stream'.mem_cons (some a) _ @@ -230,14 +232,16 @@ theorem get?_tail (s : Seq α) (n) : get? (tail s) n = get? s (n + 1) := rfl /-- Recursion principle for sequences, compare with `List.recOn`. -/ -def recOn {C : Seq α → Sort v} (s : Seq α) (h1 : C nil) (h2 : ∀ x s, C (cons x s)) : - C s := by +@[cases_eliminator] +def recOn {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil) + (cons : ∀ x s, motive (cons x s)) : + motive s := by cases' H : destruct s with v · rw [destruct_eq_nil H] - apply h1 + apply nil · cases' v with a s' rw [destruct_eq_cons H] - apply h2 + apply cons theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s) (h1 : ∀ b s', a = b ∨ C s' → C (cons b s')) : C s := by @@ -251,10 +255,9 @@ theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s) rw [TH] apply h1 _ _ (Or.inl rfl) -- Porting note: had to reshuffle `intro` - revert e; apply s.recOn _ fun b s' => _ - · intro e; injection e - · intro b s' e - have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s'; rfl + cases' s with b s' + · injection e + · have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl rw [h_eq] at e apply h1 _ _ (Or.inr (IH e)) @@ -331,20 +334,21 @@ theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s match t₁, t₂, e with | _, _, ⟨s, s', rfl, rfl, r⟩ => by suffices head s = head s' ∧ R (tail s) (tail s') from - And.imp id (fun r => ⟨tail s, tail s', by cases s; rfl, by cases s'; rfl, r⟩) this + And.imp id (fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl, + by cases s' using Subtype.recOn; rfl, r⟩) this have := bisim r; revert r this - apply recOn s _ _ <;> apply recOn s' _ _ + cases' s with x s <;> cases' s' with x' s' · intro r _ constructor · rfl · assumption - · intro x s _ this + · intro _ this rw [destruct_nil, destruct_cons] at this exact False.elim this - · intro x s _ this + · intro _ this rw [destruct_nil, destruct_cons] at this exact False.elim this - · intro x s x' s' _ this + · intro _ this rw [destruct_cons, destruct_cons] at this rw [head_cons, head_cons, tail_cons, tail_cons] cases' this with h1 h2 @@ -568,10 +572,10 @@ def toListOrStream (s : Seq α) [Decidable s.Terminates] : List α ⊕ Stream' theorem nil_append (s : Seq α) : append nil s = s := by apply coinduction2; intro s dsimp [append]; rw [corec_eq] - dsimp [append]; apply recOn s _ _ + dsimp [append] + cases' s with x s · trivial - · intro x s - rw [destruct_cons] + · rw [destruct_cons] dsimp exact ⟨rfl, s, rfl, rfl⟩ @@ -718,10 +722,9 @@ theorem cons_append (a : α) (s t) : append (cons a s) t = cons a (append s t) : @[simp] theorem append_nil (s : Seq α) : append s nil = s := by apply coinduction2 s; intro s - apply recOn s _ _ + cases' s with x s · trivial - · intro x s - rw [cons_append, destruct_cons, destruct_cons] + · rw [cons_append, destruct_cons, destruct_cons] dsimp exact ⟨rfl, s, rfl, rfl⟩ @@ -732,15 +735,12 @@ theorem append_assoc (s t u : Seq α) : append (append s t) u = append s (append exact match s1, s2, h with | _, _, ⟨s, t, u, rfl, rfl⟩ => by - apply recOn s <;> simp - · apply recOn t <;> simp - · apply recOn u <;> simp - · intro _ u - refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp - · intro _ t - refine ⟨nil, t, u, ?_, ?_⟩ <;> simp - · intro _ s - exact ⟨s, t, u, rfl, rfl⟩ + cases' s with _ s <;> simp + · cases' t with _ t <;> simp + · cases' u with _ u <;> simp + · refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp + · refine ⟨nil, t, u, ?_, ?_⟩ <;> simp + · exact ⟨s, t, u, rfl, rfl⟩ · exact ⟨s, t, u, rfl, rfl⟩ @[simp] @@ -776,12 +776,10 @@ theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) exact match s1, s2, h with | _, _, ⟨s, t, rfl, rfl⟩ => by - apply recOn s <;> simp - · apply recOn t <;> simp - · intro _ t - refine ⟨nil, t, ?_, ?_⟩ <;> simp - · intro _ s - exact ⟨s, t, rfl, rfl⟩ + cases' s with _ s <;> simp + · cases' t with _ t <;> simp + · refine ⟨nil, t, ?_, ?_⟩ <;> simp + · exact ⟨s, t, rfl, rfl⟩ @[simp] theorem map_get? (f : α → β) : ∀ s n, get? (map f s) n = (get? s n).map f @@ -835,15 +833,13 @@ theorem join_cons (a : α) (s S) : join (cons (a, s) S) = cons a (append s (join exact match s1, s2, h with | s, _, Or.inl <| Eq.refl s => by - apply recOn s; · trivial - · intro x s - rw [destruct_cons] + cases' s with x s; · trivial + · rw [destruct_cons] exact ⟨rfl, Or.inl rfl⟩ | _, _, Or.inr ⟨a, s, S, rfl, rfl⟩ => by - apply recOn s + cases' s with x s · simp [join_cons_cons, join_cons_nil] - · intro x s - simpa [join_cons_cons, join_cons_nil] using Or.inr ⟨x, s, S, rfl, rfl⟩ + · simpa [join_cons_cons, join_cons_nil] using Or.inr ⟨x, s, S, rfl, rfl⟩ @[simp] theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S) (join T) := by @@ -854,18 +850,15 @@ theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S) exact match s1, s2, h with | _, _, ⟨s, S, T, rfl, rfl⟩ => by - apply recOn s <;> simp - · apply recOn S <;> simp - · apply recOn T + cases' s with _ s <;> simp + · cases' S with s S <;> simp + · cases' T with s T · simp - · intro s T - cases' s with a s; simp only [join_cons, destruct_cons, true_and] + · cases' s with a s; simp only [join_cons, destruct_cons, true_and] refine ⟨s, nil, T, ?_, ?_⟩ <;> simp - · intro s S - cases' s with a s + · cases' s with a s simpa using ⟨s, S, T, rfl, rfl⟩ - · intro _ s - exact ⟨s, S, T, rfl, rfl⟩ + · exact ⟨s, S, T, rfl, rfl⟩ · refine ⟨nil, S, T, ?_, ?_⟩ <;> simp @[simp] @@ -920,11 +913,11 @@ theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂) generalize e : append s₁ s₂ = ss; intro h; revert s₁ apply mem_rec_on h _ intro b s' o s₁ - apply s₁.recOn _ fun c t₁ => _ + cases' s₁ with c t₁ · intro m _ apply Or.inr simpa using m - · intro c t₁ m e + · intro m e have this := congr_arg destruct e cases' show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' m · rw [e'] @@ -1002,7 +995,7 @@ def bind (s : Seq1 α) (f : α → Seq1 β) : Seq1 β := @[simp] theorem join_map_ret (s : Seq α) : Seq.join (Seq.map ret s) = s := by - apply coinduction2 s; intro s; apply recOn s <;> simp [ret] + apply coinduction2 s; intro s; cases s <;> simp [ret] @[simp] theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s @@ -1016,7 +1009,7 @@ theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s theorem ret_bind (a : α) (f : α → Seq1 β) : bind (ret a) f = f a := by simp only [bind, map, ret.eq_1, map_nil] cases' f a with a s - apply recOn s <;> intros <;> simp + cases s <;> simp @[simp] theorem map_join' (f : α → β) (S) : Seq.map f (Seq.join S) = Seq.join (Seq.map (map f) S) := by @@ -1028,18 +1021,16 @@ theorem map_join' (f : α → β) (S) : Seq.map f (Seq.join S) = Seq.join (Seq.m exact match s1, s2, h with | _, _, ⟨s, S, rfl, rfl⟩ => by - apply recOn s <;> simp - · apply recOn S <;> simp - · intro x S - cases' x with a s + cases' s with _ s <;> simp + · cases' S with x S <;> simp + · cases' x with a s simpa [map] using ⟨_, _, rfl, rfl⟩ - · intro _ s - exact ⟨s, S, rfl, rfl⟩ + · exact ⟨s, S, rfl, rfl⟩ · refine ⟨nil, S, ?_, ?_⟩ <;> simp @[simp] theorem map_join (f : α → β) : ∀ S, map f (join S) = join (map (map f) S) - | ((a, s), S) => by apply recOn s <;> intros <;> simp [map] + | ((a, s), S) => by cases s <;> simp [map] @[simp] theorem join_join (SS : Seq (Seq1 (Seq1 α))) : @@ -1052,24 +1043,21 @@ theorem join_join (SS : Seq (Seq1 (Seq1 α))) : exact match s1, s2, h with | _, _, ⟨s, SS, rfl, rfl⟩ => by - apply recOn s <;> simp - · apply recOn SS <;> simp - · intro S SS - cases' S with s S; cases' s with x s + cases' s with _ s <;> simp + · cases' SS with S SS <;> simp + · cases' S with s S; cases' s with x s simp only [Seq.join_cons, join_append, destruct_cons] - apply recOn s <;> simp + cases' s with x s <;> simp · exact ⟨_, _, rfl, rfl⟩ - · intro x s - refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp - · intro _ s - exact ⟨s, SS, rfl, rfl⟩ + · refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp + · exact ⟨s, SS, rfl, rfl⟩ · refine ⟨nil, SS, ?_, ?_⟩ <;> simp @[simp] theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) : bind (bind s f) g = bind s fun x : α => bind (f x) g := by cases' s with a s - -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [bind, map]`. + -- porting note (#10745): was `simp [bind, map]`. simp only [bind, map_pair, map_join] rw [← map_comp] simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl] @@ -1080,7 +1068,7 @@ theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) : -- give names to variables. induction' s using recOn with x s_1 <;> induction' S using recOn with x_1 s_2 <;> simp · cases' x_1 with x t - apply recOn t <;> intros <;> simp + cases t <;> simp · cases' x_1 with y t; simp instance monad : Monad Seq1 where From e7dd2f69282018159226b0473c04f7ac57ed8de0 Mon Sep 17 00:00:00 2001 From: Vasily Nesterov Date: Mon, 9 Dec 2024 12:41:09 +0300 Subject: [PATCH 2/2] revert some --- Mathlib/Data/Seq/Seq.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean index d45af9a0910ef3..78a7c424856dbd 100644 --- a/Mathlib/Data/Seq/Seq.lean +++ b/Mathlib/Data/Seq/Seq.lean @@ -150,10 +150,8 @@ theorem ge_stable (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n) have : s.get? m ≠ none := mt (s.le_stable m_le_n) this Option.ne_none_iff_exists'.mp this -@[simp] theorem not_mem_nil (a : α) : a ∉ @nil α := fun ⟨_, (h : some a = none)⟩ => by injection h -@[simp] theorem mem_cons (a : α) : ∀ s : Seq α, a ∈ cons a s | ⟨_, _⟩ => Stream'.mem_cons (some a) _ @@ -1057,7 +1055,7 @@ theorem join_join (SS : Seq (Seq1 (Seq1 α))) : theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) : bind (bind s f) g = bind s fun x : α => bind (f x) g := by cases' s with a s - -- porting note (#10745): was `simp [bind, map]`. + -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [bind, map]`. simp only [bind, map_pair, map_join] rw [← map_comp] simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]