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.

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.

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

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

Equations

• Tactic.ComputeAsymptotics.Seq.instMetricSpaceStream' = PiNat.metricSpace

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

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

Equations

• Tactic.ComputeAsymptotics.Seq.instMetricSpaceSeq = Subtype.metricSpace

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

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.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 funcion 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'))