[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
 
@@ -292,4 +297,299 @@ 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, lipschitzWith_iff_dist_le_mul, dist_cons_cons, NNReal.coe_one,
+    one_mul]
+  intro x y
+  linarith [dist_nonneg (x := x) (y := y)]
+
+/-- 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, lipschitzWith_iff_dist_le_mul, NNReal.coe_one, one_mul] at h ⊢
+  intro x y
+  specialize h (.cons hd x) (.cons hd y)
+  simp only [dist_cons_cons] at h
+  cases hx : op (.cons hd x) with
+  | nil =>
+    cases hy : op (.cons hd y) with
+    | nil => simp
+    | cons y_hd y_tl =>
+      contrapose! h
+      grw [hx, hy, dist_le_one]
+      norm_num
+  | cons x_hd x_tl =>
+    cases hy : op (.cons hd y) with
+    | nil =>
+      contrapose! h
+      grw [hx, hy, dist_le_one]
+      norm_num
+    | cons y_hd y_tl =>
+      by_cases! h_hd : x_hd ≠ y_hd
+      · contrapose! h
+        grw [hx, hy, dist_cons_cons_eq_one h_hd, dist_le_one]
+        norm_num
+      simpa [hx, hy, h_hd] using 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, lipschitzWith_iff_dist_le_mul] at h
+  specialize h (.cons a s) (.cons a t)
+  simp only [NNReal.coe_one, dist_cons_cons, one_mul] at h
+  replace h : dist (op (.cons a s)) (op (.cons a t)) ≤ 2⁻¹ := by
+    apply h.trans
+    simp
+  cases hs : op (.cons a s) with
+  | nil =>
+    cases ht : op (.cons a t) with
+    | nil => simp
+    | cons t_hd t_tl => norm_num [hs, ht] at h
+  | cons s_hd s_tl =>
+    cases ht : op (.cons a t) with
+    | nil => norm_num [hs, ht] at h
+    | cons t_hd t_tl =>
+      simp only [Seq.head_cons, Option.some.injEq]
+      by_contra! h_hd
+      rw [hs, ht, dist_cons_cons_eq_one h_hd] at h
+      norm_num at h
+
+/-- 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 =>
+    let t := op nil
+    match t.destruct with
+    | none => none
+    | some (t_hd, t_tl) =>
+      some (t_hd, ⟨fun _ ↦ t_tl, FriendlyOperation.const⟩)
+  | some s_hd =>
+    let s := .cons s_hd nil
+    let t := op s
+    match t.destruct with
+    | none => none
+    | some (t_hd, _) =>
+      some (t_hd, ⟨fun s_tl ↦ (op (.cons s_hd s_tl)).tail, FriendlyOperation.cons_tail h⟩)
+
+/-- `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
+
+/-- 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
+
+attribute [-simp] inv_pow in
+/-- Coinduction principle for proving that an operation is friendly. -/
+theorem FriendlyOperation.coind (motive : (Seq α → Seq α) → Prop)
+    {op : Seq α → Seq α}
+    (h_base : motive op)
+    (h_step : ∀ op, motive op → ∃ T : Option α → Option (α × Subtype motive),
+      ∀ s, (op s).destruct = (T s.head).map (fun (hd, op') => (hd, op'.val s.tail))) :
+    FriendlyOperation op := by
+  rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul]
+  intro s t
+  simp only [NNReal.coe_one, one_mul]
+  suffices ∀ n, dist s t ≤ (2⁻¹ : ℝ) ^ n → dist (op s) (op t) ≤ (2⁻¹ : ℝ) ^ n by
+    by_cases h : s = t
+    · simp [h]
+    obtain ⟨n, hst⟩ := dist_eq_two_inv_pow h
+    rw [hst] at this ⊢
+    apply this
+    rfl
+  intro n hn
+  induction n generalizing op s t with
+  | zero => simp
+  | succ n ih =>
+  specialize h_step _ h_base
+  obtain ⟨T, hT⟩ := h_step
+  have hs := hT s
+  have ht := hT t
+  by_cases! h_head : s.head ≠ t.head
+  · contrapose! hn
+    norm_num [pow_succ, dist_eq_one_of_head h_head]
+    refine mul_lt_one_of_nonneg_of_lt_one_right (pow_le_one₀ ?_ ?_) ?_ ?_
+    all_goals norm_num
+  cases hT_head : T s.head with
+  | none =>
+    simp only [hT_head, Option.map_none, ← h_head] at hs ht
+    apply Stream'.Seq.destruct_eq_none at hs
+    apply Stream'.Seq.destruct_eq_none at ht
+    simp [hs,destruct_eq_none, ht]
+  | some v =>
+    obtain ⟨hd, op', h_next⟩ := v
+    simp only [hT_head, Option.map_some, ← h_head] at hs ht
+    apply Stream'.Seq.destruct_eq_cons at hs
+    apply Stream'.Seq.destruct_eq_cons at ht
+    simp only [hs, ht, dist_cons_cons, pow_succ', inv_pos, Nat.ofNat_pos, mul_le_mul_iff_right₀,
+      ge_iff_le]
+    apply ih h_next
+    simpa [dist_eq_half_of_head h_head, pow_succ'] using hn
+
+/-- A generalisation of `FriendlyOperation.coind` which allows using `opf ∘ op'` in the tail
+of `op s` where `opf` is friendly and `op'` is a function satisfying `motive`. -/
+theorem FriendlyOperation.coind_comp_friend_left {op : Seq α → Seq α}
+    (motive : (Seq α → Seq α) → Prop)
+    (h_base : motive op)
+    (h_step : ∀ op, motive op →
+      ∃ T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive),
+      ∀ s, (op s).destruct = (T s.head).map fun (hd, opf, op') => (hd, opf.val <| op'.val s.tail)) :
+    FriendlyOperation op := by
+  let motive' (op : Seq α → Seq α) : Prop :=
+    ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
+  apply FriendlyOperation.coind motive'
+  · exact ⟨_root_.id, op, rfl, FriendlyOperation.id, h_base⟩
+  clear h_base op
+  rintro _ ⟨opf, op, rfl, h_opf, h_op⟩
+  specialize h_step _ h_op
+  obtain ⟨T, hT⟩ := h_step
+  -- obtain ⟨F, hF⟩ := FriendlyOperation.destruct h_opf
+  use fun hd? ↦
+    match (T hd?) with
+    | none => (h_opf.unfold none).map fun (hd, opf') =>
+      (hd, ⟨_, fun _ ↦ opf'.val nil, op, rfl, FriendlyOperation.const, h_op⟩)
+    | some (hd, opf', op') => (h_opf.unfold (some hd)).map fun (hd', opf'') =>
+      (hd', ⟨_, opf''.val ∘ opf'.val, op'.val, rfl,
+        FriendlyOperation.comp opf''.prop opf'.prop, op'.prop⟩)
+  intro s
+  specialize hT s
+  simp only [Function.comp_apply]
+  generalize op s = s' at *
+  cases s' with
+  | nil =>
+    symm at hT
+    simp at hT
+    simp [hT, destruct_apply_eq_unfold h_opf]
+    rfl
+  | cons s_hd s_tl =>
+  simp only [destruct_cons] at hT
+  simp only [destruct_apply_eq_unfold h_opf, Seq.tail_cons, Seq.head_cons]
+  generalize T s.head = t? at *
+  cases t? with
+  | none => simp at hT
+  | some v =>
+  obtain ⟨hd, opf', op'⟩ := v
+  simp at hT
+  simp [hT]
+  rfl
+
+/-- A generalisation of `FriendlyOperation.coind` that allows using `op' ∘ opf` in the tail
+of `op s` where `opf` is friendly and `op'` is a function satisfying `motive`. -/
+theorem FriendlyOperation.coind_comp_friend_right {op : Seq α → Seq α}
+    (motive : (Seq α → Seq α) → Prop)
+    (h_base : motive op)
+    (h_step : ∀ op, motive op →
+      ∃ T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive),
+      ∀ s, (op s).destruct = (T s.head).map fun (hd, opf, op') => (hd, op'.val <| opf.val s.tail)) :
+    FriendlyOperation op := by
+  let motive' (op : Seq α → Seq α) : Prop :=
+    ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
+  apply FriendlyOperation.coind motive'
+  · exact ⟨_root_.id, op, rfl, FriendlyOperation.id, h_base⟩
+  clear h_base op
+  rintro _ ⟨opf, op, rfl, h_opf, h_op⟩
+  specialize h_step _ h_op
+  obtain ⟨T, hT⟩ := h_step
+  -- obtain ⟨F, hF⟩ := FriendlyOperation.destruct h_opf
+  use fun hd? ↦
+    match (h_opf.unfold hd?) with
+    | none => (T none).map fun (hd, opf', op') =>
+      (hd, ⟨_, fun _ ↦ opf'.val nil, op', rfl, FriendlyOperation.const, op'.prop⟩)
+    | some (hd, opf') => (T (some hd)).map fun (hd', opf'', op') =>
+      (hd', ⟨_, opf''.val ∘ opf'.val, op'.val, rfl,
+        FriendlyOperation.comp opf''.prop opf'.prop, op'.prop⟩)
+  intro s
+  simp only [Function.comp_apply]
+  have hF := h_opf.destruct_apply_eq_unfold (s := s)
+  generalize opf s = s' at *
+  cases s' with
+  | nil =>
+    symm at hF
+    simp only [destruct_nil, Option.map_eq_none_iff] at hF
+    simp only [hF, Option.map_map]
+    specialize hT nil
+    simp only [tail_nil, head_nil] at hT
+    simp [hT]
+    rfl
+  | cons s_hd s_tl =>
+  simp only [destruct_cons] at hF
+  generalize h_opf.unfold s.head = t? at *
+  cases t? with
+  | none => simp at hF
+  | some v =>
+  obtain ⟨hd, opf', op'⟩ := v
+  simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at hF
+  simp only [hF, Option.map_map]
+  rw [hT]
+  rfl
+
+/-- A generalisation of `Seq.eq_of_bisim'` that allows using a friendly operation in the tail
+of the sequences. -/
+theorem FriendlyOperationClass.eq_of_bisim {s t : Seq α} {op : γ → Seq α → Seq α}
+    [FriendlyOperationClass op]
+    (motive : Seq α → Seq α → Prop)
+    (base : motive s t)
+    (step : ∀ u v, motive u v → (u = v) ∨
+      ∃ hd u' v' c, u = cons hd (op c u') ∧ v = cons hd (op c v') ∧
+        motive u' v') :
+    s = t := by
+  suffices dist s t = 0 by simpa using this
+  suffices ∀ n, dist s t ≤ (2⁻¹ : ℝ) ^ n by
+    apply eq_of_le_of_ge
+    · apply ge_of_tendsto' (x := Filter.atTop) _ this
+      rw [tendsto_pow_atTop_nhds_zero_iff]
+      norm_num
+    · simp
+  intro n
+  induction n generalizing s t with
+  | zero => simp
+  | succ n ih =>
+    specialize step s t base
+    obtain step | ⟨hd, u, v, c, rfl, rfl, h_next⟩ := step
+    · simp [step]
+    simp only [dist_cons_cons]
+    specialize ih h_next
+    calc
+      _ ≤ 2⁻¹ * dist u v := by
+        gcongr
+        apply FriendlyOperation.dist_le
+        apply FriendlyOperationClass.friend
+      _ ≤ _ := by
+        grw [ih, pow_succ']
+
 end Tactic.ComputeAsymptotics.Seq