Non-primitive corecursion for sequences

Primitive corecursive definition of the form

def foo (x : X) := hd x :: foo (tlArg x)

(where hd and tlArg are arbitrary functions) can be encoded via the corecursor Seq.corec.

It is not enough, however, to define multiplication and powser operation for multiseries.

This file implements a more general form of corecursion in the spirit of [BPT15]. This is a bare minimum that needed for the tactic, it justifies a weaker class of corecursive definitions than [BPT15] does, and only works for Seq.

A function f : Seq α → Seq α is called friendly if for all n : ℕ the n-prefix of its result f s depends only on the n-prefix of its input s.

In this file we develop a theory that justifies corecursive definitions of the form

def foo (x : X) := hd x :: f (foo (tlArg x))

where f is friendly.

Main definitions

• FriendlyOperation f means that f is friendly.
• FriendlyOperationClass is a typeclass meaning that some indexed family of operations 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

To prove that the definition of the form

def foo (x : X) := hd x :: f (foo (tlArg x))

is correct we prove that there exists a function satisfying this equation. For that we employ a Banach fixed point theorem. We treat Seq α as a metric space here with the metric d(s, t) := 2 ^ (-n) where n is the minimal index where s and t differ.

Then f is friendly iff it is 1-Lipschitz.

@[implicit_reducible]

noncomputable def Tactic.ComputeAsymptotics.Seq.instMetricSpaceStream' {α : Type u_1} : MetricSpace (Stream' α)

Metric space structure on Stream' α considering α as a discrete metric space.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable def Tactic.ComputeAsymptotics.Seq.instMetricSpaceSeq {α : Type u_1} : MetricSpace (Stream'.Seq α)

Metric space structure on Seq α considering α as a discrete metric space.

Equations

• One or more equations did not get rendered due to their size.

theorem Tactic.ComputeAsymptotics.Seq.instCompleteSpaceStream' {α : Type u_1} : CompleteSpace (Stream' α)

theorem Tactic.ComputeAsymptotics.Seq.instCompleteSpaceSeq {α : Type u_1} : CompleteSpace (Stream'.Seq α)

theorem Tactic.ComputeAsymptotics.Seq.Stream'.dist_le_one {α : Type u_1} (s t : Stream' α) : dist s t ≤ 1

@[simp]

theorem Tactic.ComputeAsymptotics.Seq.dist_le_one {α : Type u_1} (s t : Stream'.Seq α) : dist s t ≤ 1

theorem Tactic.ComputeAsymptotics.Seq.instBoundedSpaceStream' {α : Type u_1} : BoundedSpace (Stream' α)

theorem Tactic.ComputeAsymptotics.Seq.instBoundedSpaceSeq {α : Type u_1} : BoundedSpace (Stream'.Seq α)

theorem Tactic.ComputeAsymptotics.Seq.dist_eq_two_inv_pow {α : Type u_1} {s t : Stream'.Seq α} (h : s ≠ t) : ∃ (n : ℕ), dist s t = 2⁻¹ ^ n

@[simp]

theorem Tactic.ComputeAsymptotics.Seq.dist_cons_cons {α : Type u_1} (x : α) (s t : Stream'.Seq α) : dist (Stream'.Seq.cons x s) (Stream'.Seq.cons x t) = 2⁻¹ * dist s t

theorem Tactic.ComputeAsymptotics.Seq.dist_eq_half_of_head {α : Type u_1} {s t : Stream'.Seq α} (h : s.head = t.head) : dist s t = 2⁻¹ * dist s.tail t.tail

theorem Tactic.ComputeAsymptotics.Seq.dist_eq_one_of_head {α : Type u_1} {s t : Stream'.Seq α} (h : s.head ≠ t.head) : dist s t = 1

theorem Tactic.ComputeAsymptotics.Seq.dist_cons_cons_eq_one {α : Type u_1} {x y : α} {s t : Stream'.Seq α} (h : x ≠ y) : dist (Stream'.Seq.cons x s) (Stream'.Seq.cons y t) = 1

@[simp]

theorem Tactic.ComputeAsymptotics.Seq.dist_cons_nil {α : Type u_1} (x : α) (s : Stream'.Seq α) : dist (Stream'.Seq.cons x s) Stream'.Seq.nil = 1

@[simp]

theorem Tactic.ComputeAsymptotics.Seq.dist_nil_cons {α : Type u_1} (x : α) (s : Stream'.Seq α) : dist Stream'.Seq.nil (Stream'.Seq.cons x s) = 1

theorem Tactic.ComputeAsymptotics.Seq.dist_le_half_iff {α : Type u_1} {s t : Stream'.Seq α} : dist s t ≤ 2⁻¹ ↔ s = Stream'.Seq.nil ∧ t = Stream'.Seq.nil ∨ ∃ (hd : α) (s' : Stream'.Seq α) (t' : Stream'.Seq α), s = Stream'.Seq.cons hd s' ∧ t = Stream'.Seq.cons hd t'

def Tactic.ComputeAsymptotics.Seq.FriendlyOperation {α : Type u_1} (op : Stream'.Seq α → Stream'.Seq α) : Prop

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.

Equations

• Tactic.ComputeAsymptotics.Seq.FriendlyOperation op = LipschitzWith 1 op

class Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass {α : Type u_1} {γ : Type u_3} (F : γ → Stream'.Seq α → Stream'.Seq α) : Prop

A family of friendly operations on sequences indexed by a type γ.

• friend (c : γ) : FriendlyOperation (F c)

theorem Tactic.ComputeAsymptotics.Seq.friendlyOperation_iff_dist_le_dist {α : Type u_1} (op : Stream'.Seq α → Stream'.Seq α) : FriendlyOperation op ↔ ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.id {α : Type u_1} : FriendlyOperation _root_.id

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.comp {α : Type u_1} {op op' : Stream'.Seq α → Stream'.Seq α} (h : FriendlyOperation op) (h' : FriendlyOperation op') : FriendlyOperation (op ∘ op')

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.const {α : Type u_1} {s : Stream'.Seq α} : FriendlyOperation fun (x : Stream'.Seq α) => s

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass.comp {α : Type u_1} {γ : Type u_3} {γ' : Type u_4} (F : γ → Stream'.Seq α → Stream'.Seq α) (g : γ' → γ) [h : FriendlyOperationClass F] : FriendlyOperationClass fun (c : γ') => F (g c)

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.ite {α : Type u_1} {op₁ op₂ : Stream'.Seq α → Stream'.Seq α} (h₁ : FriendlyOperation op₁) (h₂ : FriendlyOperation op₂) {P : Option α → Prop} [DecidablePred P] : FriendlyOperation fun (s : Stream'.Seq α) => if P s.head then op₁ s else op₂ s

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.dist_le {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (h : FriendlyOperation op) {s t : Stream'.Seq α} : dist (op s) (op t) ≤ dist s t

theorem Tactic.ComputeAsymptotics.Seq.exists_fixed_point_of_contractible {α : Type u_1} {β : Type u_2} (F : UniformFun β (Stream'.Seq α) → UniformFun β (Stream'.Seq α)) (h : LipschitzWith 2⁻¹ F) : ∃ (f : β → Stream'.Seq α), Function.IsFixedPt F f

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.exists_fixed_point {α : Type u_1} {β : Type u_2} {γ : Type u_3} (F : β → Option (α × γ × β)) (op : γ → Stream'.Seq α → Stream'.Seq α) [h : FriendlyOperationClass op] : ∃ (f : β → Stream'.Seq α), ∀ (b : β), match F b with | none => f b = Stream'.Seq.nil | some (a, c, b') => f b = Stream'.Seq.cons a (op c (f b'))

Main theorem of this file. It shows that there exists a function satisfying the corecursive definition of the form def foo (x : X) := hd x :: op (foo (tlArg x)) where f is friendly.

noncomputable def Tactic.ComputeAsymptotics.Seq.gcorec {α : Type u_1} {β : Type u_2} {γ : Type u_3} (F : β → Option (α × γ × β)) (op : γ → Stream'.Seq α → Stream'.Seq α) [FriendlyOperationClass op] : β → Stream'.Seq α

(General) non-primitive corecursor for Seq α that allows using a friendly operation in the tail of the corecursive definition.

Equations

• Tactic.ComputeAsymptotics.Seq.gcorec F op = ⋯.choose

theorem Tactic.ComputeAsymptotics.Seq.gcorec_nil {α : Type u_1} {β : Type u_2} {γ : Type u_3} {F : β → Option (α × γ × β)} {op : γ → Stream'.Seq α → Stream'.Seq α} [FriendlyOperationClass op] {b : β} (h : F b = none) : gcorec F op b = Stream'.Seq.nil

theorem Tactic.ComputeAsymptotics.Seq.gcorec_some {α : Type u_1} {β : Type u_2} {γ : Type u_3} {F : β → Option (α × γ × β)} {op : γ → Stream'.Seq α → Stream'.Seq α} [FriendlyOperationClass op] {b : β} {a : α} {c : γ} {b' : β} (h : F b = some (a, c, b')) : gcorec F op b = Stream'.Seq.cons a (op c (gcorec F op b'))

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.cons {α : Type u_1} (hd : α) : FriendlyOperation (Stream'.Seq.cons hd)

The operation cons hd · is friendly.

theorem Tactic.ComputeAsymptotics.Seq.dist_const_tail_cons_tail_le {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} {hd : α} {x y : Stream'.Seq α} (h : dist (op (Stream'.Seq.cons hd x)) (op (Stream'.Seq.cons hd y)) ≤ dist (Stream'.Seq.cons hd x) (Stream'.Seq.cons hd y)) : dist (op (Stream'.Seq.cons hd x)).tail (op (Stream'.Seq.cons hd y)).tail ≤ dist x y

If two sequences have the same head and applying op reduces their distance, then it also reduces the distance of their tails.

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.cons_tail {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} {hd : α} (h : FriendlyOperation op) : FriendlyOperation fun (s : Stream'.Seq α) => (op (Stream'.Seq.cons hd s)).tail

The operation (op (.cons hd ·)).tail is friendly if op is friendly.

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.op_cons_head_eq {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (h : FriendlyOperation op) {a : α} {s t : Stream'.Seq α} : (op (Stream'.Seq.cons a s)).head = (op (Stream'.Seq.cons a t)).head

The first element of op (a :: s) depends only on a.

def Tactic.ComputeAsymptotics.Seq.FriendlyOperation.unfold {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (h : FriendlyOperation op) (hd? : Option α) : Option (α × Subtype FriendlyOperation)

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.

Equations

• One or more equations did not get rendered due to their size.
• h.unfold none = match (op Stream'.Seq.nil).destruct with | none => none | some (t_hd, t_tl) => some (t_hd, ⟨fun (x : Stream'.Seq α) => t_tl, ⋯⟩)

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.destruct_apply_eq_unfold {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (h : FriendlyOperation op) {s : Stream'.Seq α} : (op s).destruct = Option.map (fun (x : α × Subtype FriendlyOperation) => match x with | (hd, op') => (hd, ↑op' s.tail)) (h.unfold s.head)

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 Tactic.ComputeAsymptotics.Seq.FriendlyOperation.op_head_eq {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (h : FriendlyOperation op) {s t : Stream'.Seq α} (h_head : s.head = t.head) : (op s).head = (op t).head

If op is friendly, then op s and op t have the same head if s and t have the same head.

theorem Tactic.ComputeAsymptotics.Seq.FriendlyOperation.of_dist_le_pow {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (h : ∀ (s t : Stream'.Seq α) (n : ℕ), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n) : FriendlyOperation op