Zulip Chat Archive

Stream: new members

Topic: Scott topology in seq


view this post on Zulip Andrés Goens (Dec 06 2020 at 20:49):

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!

view this post on Zulip Patrick Massot (Dec 06 2020 at 20:56):

@Simon Hudon :up:

view this post on Zulip Mario Carneiro (Dec 06 2020 at 20:57):

What does prefix mean here?

view this post on Zulip Mario Carneiro (Dec 06 2020 at 20:58):

Oh these are potentially infinite lists

view this post on Zulip Mario Carneiro (Dec 06 2020 at 21:00):

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

view this post on Zulip Mario Carneiro (Dec 06 2020 at 21:00):

this formulation makes a lot of theorems easy to prove

view this post on Zulip Mario Carneiro (Dec 06 2020 at 21:01):

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

view this post on Zulip Mario Carneiro (Dec 06 2020 at 21:02):

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

view this post on Zulip Andrés Goens (Dec 06 2020 at 21:10):

that makes a lot of sense! thanks @Mario Carneiro


Last updated: May 14 2021 at 05:20 UTC