feat(untyped): the Leftmost Reduction Theorem

[m-ow]

Introduces leftmost reduction ⭢ℓ, a beta-step contracting the redex at position 0, together with normal forms, and proves the Leftmost Reduction Theorem: if a term beta-reduces to a normal form, the leftmost strategy reaches it too.
The result falls out of standardization, following Copes (2018).

Builds on top of #679

[lengyijun]

Can you add 2 theorems :

1. NormalForm M <-> Normal FullBeta M
2. Decidable Normal FullBeta

[m-ow]

@lengyijun Sounds good, I'll get both into a separate PR soon :)

[lengyijun]

Should we rename Normal to NormalBeta ?
Or put it in namespace "FullBeta"

Normal may also refer to Normal FullBetaEta or Normal FullEta

[lengyijun]

@m-ow Hi, what's your plan after this pr

[m-ow]

Honestly, no fixed plan yet, but your project sounds really interesting. Feel free to point me at what's the priority on your side, happy to take a look!

[lengyijun]

We will formalize "2 vars are not enough" after this pr is merged.

There will still be 1400 cases unprocessed. I haven't even studied them at all.

You can randomly pick a few and research them.

I will also pr my fork step by step.
Perhaps you can help me optimize the proof.

[chenson2018]

@m-ow Before I review for more detailed changes, I think I'm missing some high-level points about the defintions (some of which I maybe should have asked in earlier PRs, sorry!).

BetaAt seems to clearly align with the literature, but I think I'm missing where the connection to the usual definition of standard reduction is happening. I am expecting to somewhere see that if we have BetaAt A B x and BetaAt B C y with x <= y this is a standard reduction and that this is equivalent to Standard. Am I missing where this appears in a different form or otherwise misunderstanding something? (I'm following along with https://www.is.c.titech.ac.jp/~kashima/pub/C-145.pdf that's mentioned in your reference)

[m-ow]

You're right, it's not there. The results here only rely on the inductive Standard relation, both sources I followed actually keep the sequence definition as a separate development. It's clearly worth having though, sorry for the gap! If you think it's best, I'll open a new PR to add the sequence definition and its equivalence with Standard.

[chenson2018]

Yeah, it is pretty standard to use some equivalent inductive that's easier to work with (I assume this is why we have Standard not directly written in terms of BetaAt?), but I think we should have this proof of equivalence to make sure the definition corresponds to what we want informally.

Maybe because these are so closely related they should just go in the same module? Feel free to move things around as needed.