Scott topology in seq

Stream: new members

[Andrés Goens]

Hi everyone!

I've been playing around with Lean a bit and want to prove some simple (old) stuff about Scott continuous functions on sequences. After some digging around mathlib I found some very nice definitions of the Scott topology already and order.omega_complete_partial_order. The instances of omega_complete_partial_order honestly did confuse me a bit, and after struggling to understand what roption.seq is supposed to be, I decided it would be a nice exercise to prove that seq \a for some type \a is an omega complete partial order (with respect to prefixes). I'm struggling with even defining prefixes on seq. What I would need to do is separate by cases for an infinite sequence and a finite one (which gives me a list). There is a function seq.to_list_or_stream that maps to the sum type of list and stream, but I cannot figure out how to do a pattern matching on the this sum type for defining prefixes on seq.

The other option I thought of was to define finite sequences and then infinite sequences (as not finite ones), and go from there. I think I have a decent definition of a finite sequence:

def seq.finite (s : seq α) := ∃ N : ℕ, s.1 N = none

The only step I can think of from here is to do four definitions of prefix, for both finite, both infinite and the two cases where one is infinite and one is not, and then finally one for the general case where I would combine these four somehow by cases. This sounds like it might work if I dig around enough to understand how to construct this four cases but it seems kind of the wrong way of doing things. Also, I guess to do the four cases should require the same type of definition by cases that I need for the sum data type that I get from seq.to_list_or_stream.

Or perhaps I'm going down the wrong path with seq? Should I define sequences differently for proving things with them this way? I thought I might ask this here before I go too far astray.

Thanks!

[Patrick Massot]

@Simon Hudon :up:

[Mario Carneiro]

What does prefix mean here?

[Mario Carneiro]

Oh these are potentially infinite lists

[Mario Carneiro]

Instead of defining by cases, you can just describe it elementwise.

def seq.prefix (s t : seq α) := ∀ n a, s.val n = some a → t.val n = some a

[Mario Carneiro]

this formulation makes a lot of theorems easy to prove

[Mario Carneiro]

seq works best when you deal with the finite and infinite cases uniformly

[Mario Carneiro]

fyi seq.finite is called src#seq.terminates in mathlib

[Andrés Goens]

that makes a lot of sense! thanks @Mario Carneiro