Changing `Stream.Seq` to use `GetElem`

Stream: mathlib4

[Eric Wieser]

Would this be a desirable change? docs#Stream' describes itself as an infinite list, so presumably it shoudl present s[i] notation to match lsits?

[Eric Wieser]

(I guess this is a question for @Mario Carneiro)

[Jakub Nowak]

You mean to add GetElem to Stream' or Stream'.Seq?

[Mario Carneiro]

I think it's fine to offer that. I don't like it as the default because it will have bad defeqs in the latter case

[Eric Wieser]

What would be bad about the defeq?

[Eric Wieser]

Does #29484 look like a viable direction?

[Eric Wieser]

This also switches it to a one-field structure to prevent accidentally mixing s i and s[i]

[Eric Wieser]

Unfortunately this gets quite annoying for recursive stream definitions, since the termination checker doesn't like

def Fix.approx : Stream' (∀ a, Part (β a)) where
  get'
  | 0 => ⊥
  | Nat.succ i => f approx[i] -- `(approx i)` was no problem before

[Aaron Liu]

uhoh

[Aaron Liu]

can we rewrite that as a function Nat -> ∀ a, Part (β a)

[Eric Wieser]

Sure, I can write

def Fix.approx : Stream' (∀ a, Part (β a)) where
  get'
where
  get'
  | 0 => ⊥
  | Nat.succ i => f (get' i)

@[simp] theorem Fix.get_succ_approx (n : ℕ) : (Fix.approx f)[n + 1] = f ((Fix.approx f)[n]) :=
  rfl

but I have to write the equation lemma manually

[Eric Wieser]

Or a slightly more cursed spelling,

def Fix.approx : Stream' (∀ a, Part (β a)) where get' where
  get'
  | 0 => ⊥
  | Nat.succ i => f (get' i)
-- still need the simp lemma

[Aaron Liu]

I like the cursed version

[Aaron Liu]

can we get @[simps] to do these equations for us

[Eric Wieser]

It would have to know to replace the inner get' with the high-level notation operator

[Eric Wieser]

I'd rather the equation compiler could do it for me

[Aaron Liu]

which one

[Aaron Liu]

the structural recursion or the well-founded recursion

[Eric Wieser]

Let's move this to #lean4 > Termination-checking of one field structures @ 💬