[Merged by Bors] - feat(Tactic/ComputeAsymptotics/Multiseries): non-primitive corecursion for Seq: FriendlyOperation API

Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean

@@ -42,6 +42,11 @@ where f is friendly.
   are friendly.
 * `gcorec`: a generalization of `Seq.corec` that allows a corecursive call to be guarded by
   a friendly function.
+* `FriendlyOperation.coind`, `FriendlyOperation.coind_comp_friend_left`,
+  `FriendlyOperation.coind_comp_friend_right`: coinduction principles for proving that an operation
+  is friendly.
+* `FriendlyOperation.eq_of_bisim`: a generalisation of `Seq.eq_of_bisim'` that allows using a
+  friendly operation in the tail of the sequences.
 
 ## Implementation details
 
@@ -163,6 +168,14 @@ theorem dist_nil_cons (x : α) (s : Seq α) : dist nil (cons x s) = 1 := by
   rw [dist_comm]
   simp
 
+theorem dist_le_half_iff {s t : Seq α} :
+    dist s t ≤ 2⁻¹ ↔ (s = .nil ∧ t = .nil) ∨ ∃ hd s' t', s = .cons hd s' ∧ t = .cons hd t' where
+  mp h := by
+    cases s <;> cases t <;> norm_num at h <;> simp
+    grind [dist_cons_cons_eq_one]
+  mpr h := by
+    obtain ⟨rfl, rfl⟩ | ⟨hd, s', t', rfl, rfl⟩ := h <;> simp
+
 /-- A function on sequences is called a "friend" if any `n`-prefix of its output depends only on
 the `n`-prefix of the input. Such functions can be used in the tail of (non-primitive) corecursive
 definitions. -/
@@ -172,6 +185,10 @@ def FriendlyOperation (op : Seq α → Seq α) : Prop := LipschitzWith 1 op
 class FriendlyOperationClass (F : γ → Seq α → Seq α) : Prop where
   friend : ∀ c : γ, FriendlyOperation (F c)
 
+theorem friendlyOperation_iff_dist_le_dist (op : Seq α → Seq α) :
+    FriendlyOperation op ↔ ∀ s t, dist (op s) (op t) ≤ dist s t := by
+  simp [FriendlyOperation, lipschitzWith_iff_dist_le_mul]
+
 theorem FriendlyOperation.id : FriendlyOperation (id : Seq α → Seq α) :=
   LipschitzWith.id
 
@@ -183,7 +200,7 @@ theorem FriendlyOperation.comp {op op' : Seq α → Seq α}
   simp
 
 theorem FriendlyOperation.const {s : Seq α} : FriendlyOperation (fun _ ↦ s) := by
-  simp [FriendlyOperation, lipschitzWith_iff_dist_le_mul]
+  simp [friendlyOperation_iff_dist_le_dist]
 
 theorem FriendlyOperationClass.comp (F : γ → Seq α → Seq α) (g : γ' → γ)
     [h : FriendlyOperationClass F] : FriendlyOperationClass (fun c ↦ F (g c)) := by
@@ -193,7 +210,7 @@ theorem FriendlyOperation.ite {op₁ op₂ : Seq α → Seq α}
     (h₁ : FriendlyOperation op₁) (h₂ : FriendlyOperation op₂)
     {P : Option α → Prop} [DecidablePred P] :
     FriendlyOperation (fun s ↦ if P s.head then op₁ s else op₂ s) := by
-  rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul, NNReal.coe_one] at h₁ h₂ ⊢
+  rw [friendlyOperation_iff_dist_le_dist] at h₁ h₂ ⊢
   intro s t
   by_cases! h_head : s.head ≠ t.head
   · simp [dist_eq_one_of_head h_head]
@@ -291,4 +308,110 @@ theorem gcorec_some {F : β → Option (α × γ × β)} {op : γ → Seq α →
   have := (FriendlyOperation.exists_fixed_point F op).choose_spec b
   simpa [h] using this
 
+/-- The operation `cons hd ·` is friendly. -/
+theorem FriendlyOperation.cons (hd : α) : FriendlyOperation (cons hd) := by
+  simp only [friendlyOperation_iff_dist_le_dist, dist_cons_cons]
+  intro x y
+  linarith [dist_nonneg (x := x) (y := y)]
+
+/-- If two sequences have the same head and applying `op` reduces their distance, then
+it also reduces the distance of their tails. -/
+lemma dist_const_tail_cons_tail_le
+    {op : Seq α → Seq α} {hd : α} {x y : Stream'.Seq α}
+    (h : dist (op (cons hd x)) (op (cons hd y)) ≤ dist (cons hd x) (cons hd y)) :
+    dist (op (cons hd x)).tail (op (cons hd y)).tail ≤ dist x y := by
+  rwa [dist_cons_cons, dist_eq_half_of_head, mul_le_mul_iff_right₀ (by norm_num)] at h
+  grw [dist_le_one x y, mul_one] at h
+  obtain (⟨hx, hy⟩ | ⟨_, _, _, hx, hy⟩) := dist_le_half_iff.mp h <;> simp [hx, hy]
+
+/-- The operation `(op (.cons hd ·)).tail` is friendly if `op` is friendly. -/
+theorem FriendlyOperation.cons_tail {op : Seq α → Seq α} {hd : α} (h : FriendlyOperation op) :
+    FriendlyOperation (fun s ↦ (op (.cons hd s)).tail) := by
+  simp_rw [friendlyOperation_iff_dist_le_dist] at h ⊢
+  intro x y
+  specialize h (.cons hd x) (.cons hd y)
+  exact dist_const_tail_cons_tail_le h
+
+/-- The first element of `op (a :: s)` depends only on `a`. -/
+theorem FriendlyOperation.op_cons_head_eq {op : Seq α → Seq α} (h : FriendlyOperation op) {a : α}
+    {s t : Seq α} : (op <| .cons a s).head = (op <| .cons a t).head := by
+  rw [friendlyOperation_iff_dist_le_dist] at h
+  specialize h (.cons a s) (.cons a t)
+  simp only [dist_cons_cons] at h
+  replace h : dist (op (.cons a s)) (op (.cons a t)) ≤ 2⁻¹ := by
+    apply h.trans
+    simp
+  rw [dist_le_half_iff] at h
+  generalize op (Seq.cons a s) = s' at *
+  generalize op (Seq.cons a t) = t' at *
+  obtain ⟨rfl, rfl⟩ | ⟨hd, s_tl, t_tl, rfl, rfl⟩ := h <;> rfl
+
+/-- Decomposes a friendly operation by the head of the input sequence. Returns `none` if the output
+is `nil`, or `some (out_hd, op')` where `out_hd` is the head of the output and `op'` is a friendly
+operation mapping the tail of the input to the tail of the output. See
+`destruct_apply_eq_unfold` for the correctness statement. -/
+def FriendlyOperation.unfold {op : Seq α → Seq α} (h : FriendlyOperation op) (hd? : Option α) :
+    Option (α × Subtype (@FriendlyOperation α)) :=
+  match hd? with
+  | none =>
+    match (op nil).destruct with
+    | none => none
+    | some (t_hd, t_tl) =>
+      some (t_hd, ⟨fun _ ↦ t_tl, FriendlyOperation.const⟩)
+  | some s_hd =>
+    match (op <| .cons s_hd nil).destruct with
+    | none => none
+    | some (t_hd, _) =>
+      some (t_hd, ⟨fun s_tl ↦ (op (.cons s_hd s_tl)).tail, FriendlyOperation.cons_tail h⟩)
+
+set_option backward.isDefEq.respectTransparency false in
+/-- `unfold` correctly decomposes a friendly operation: the head of `op s` depends only on the
+head of `s` (and is given by `unfold`), while the tail of `op s` is obtained by applying the
+friendly operation returned by `unfold` to the tail of `s`. This gives a coinductive
+characterization of `FriendlyOperation`. For the coinduction principle, see
+`FriendlyOperation.coind`. -/
+theorem FriendlyOperation.destruct_apply_eq_unfold {op : Seq α → Seq α} (h : FriendlyOperation op)
+    {s : Seq α} :
+    destruct (op s) = (h.unfold s.head).map (fun (hd, op') => (hd, op'.val s.tail)) := by
+  unfold unfold
+  cases s with
+  | nil =>
+    generalize op nil = t
+    cases t <;> simp
+  | cons s_hd s_tl =>
+    simp only [Seq.tail_cons, Seq.head_cons]
+    generalize ht0 : op (.cons s_hd nil) = t0 at *
+    generalize ht : op (.cons s_hd s_tl) = t at *
+    have : t0.head = t.head := by
+      rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
+    cases t0 with
+    | nil =>
+      cases t with
+      | nil => simp
+      | cons => simp at this
+    | cons =>
+      cases t with
+      | nil => simp at this
+      | cons => simp_all
+
+set_option backward.isDefEq.respectTransparency false in
+/-- If `op` is friendly, then `op s` and `op t` have the same head if `s` and `t`
+have the same head. -/
+theorem FriendlyOperation.op_head_eq {op : Seq α → Seq α} (h : FriendlyOperation op) {s t : Seq α}
+    (h_head : s.head = t.head) : (op s).head = (op t).head := by
+  simp only [head_eq_destruct, Option.map_eq_map, h.destruct_apply_eq_unfold, Option.map_map]
+    at h_head ⊢
+  simp [h_head]
+  rfl
+
+theorem FriendlyOperation.of_dist_le_pow {op : Seq α → Seq α}
+    (h : ∀ s t n, dist s t ≤ (2⁻¹ : ℝ) ^ n → dist (op s) (op t) ≤ (2⁻¹ : ℝ) ^ n) :
+    FriendlyOperation op := by
+  rw [friendlyOperation_iff_dist_le_dist]
+  intro s t
+  by_cases hst : s = t
+  · simp [hst]
+  obtain ⟨n, hst⟩ := dist_eq_two_inv_pow hst
+  grind
+
 end Tactic.ComputeAsymptotics.Seq