simple functional queue from Okasaki

[c-cube]

Hi, this is my first attempt at contributing Lean code.

I dug out the old Okasaki, and started off with the simple queue. This should
contain a correctness proof, a complexity proof, and a mapping to a ghost list
of elements. TimeM doesn't seem to be enough for amortized complexity so
I added a module for that, and I also removed the ZeroAdd typeclass constraint
because \N doesn't implement it(!).

AI disclosure: all code is mine, but I had some assistance from GLM 5.1 to
tidy up proof terms and get unstuck.

[c-cube]

this is ready for re-review

[eric-wieser]

This has no docstring; and this only makse sense if you are saying "for any given pair of types α o, there is exactly one possible operation".

[c-cube]

how else should I write this? no typeclass at all?

[eric-wieser]

Yes, I think drop the typeclass entirely.

[eric-wieser]

In my opinion, the TimeM stuff clutters the API here; especially if you find yourself wanting to execute this code, and now end up computing a bunch of counters that you have no interest in. I'd suggest something like

Suggested change

	/-- Enqueue an element. -/
	def push {α : Type u} (x : α) (q : FunctionalQueue α)
	: TimeM ℕ (FunctionalQueue α) := do
	TimeM.tick 1
	rebalance ⟨ q.front, x :: q.back ⟩
	/-- Enqueue an element. -/
	def push {α : Type u} (x : α) (q : FunctionalQueue α) : FunctionalQueue α :=
	rebalance ⟨q.front, x :: q.back⟩
	/-- Push as an algorithm
	def pushAlg {α : Type u} (x : α) (q : FunctionalQueue α)
	: TimeM ℕ (FunctionalQueue α) := do
	TimeM.tick 1
	rebalanceAlg ⟨ q.front, x :: q.back ⟩
	@[simp] theorem run_pushAlg : (pushAlg x q).ret = pushAlg x q := sorry

and similar for the others.

Perhaps this needs discussion on Zulip.

[eric-wieser]

Suggested change

	def invariant {α : Type u} (q : Raw.FunctionalQueue α) : Prop :=
	def Invariant {α : Type u} (q : Raw.FunctionalQueue α) : Prop :=

since this is a Prop

[eric-wieser]

This should be called Invariant.push

[eric-wieser]

Note that you can change this to

Suggested change

	class Potential (φ α : Type*) [CommRing φ] [LinearOrder φ] [IsStrictOrderedRing φ] where
	class Potential (φ α : Type*) where