refactor: abbrev open'/close

[lengyijun]

Dropped the [HasFresh Var]
Moved [DecidableEq Var] later, where it is actually needed
open' and close turned into abbrevs (instead of defs)

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for c0b6289 against 809bb39 are in. No significant results found. @chenson2018

• 🟥 build//instructions: +7.3G (+0.33%)

Small changes (2🟥)

• 🟥 build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.StrongNorm//instructions: +2.1G (+17.38%)
• 🟥 build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm//instructions: +1.2G (+5.52%)

[chenson2018]

Can I ask what the motivation is for this change? It's unclear to me what benefit this has.

[lengyijun]

24 less unfold open' in fokker_challenge

awesome-lambda-calculus/Fokker_challenge@b85418a

---

Update: more example :

awesome-lambda-calculus@c4b274c

[lengyijun]

One example :

hM : LcAt 0 M✝.abs = true
hN : LcAt 0 N✝ = true
⊢ LcAt 0 (M✝ ^ N✝) = true

                  unfold open'
                  rw [lcAt_openRec_iff_lcAt _ _ _ hN]
                  grind

[lengyijun]

Another example:

h2 : Q₀⟦0 ↜ x⟧.abs ⭢ₚ A' ^ Term.fvar x⟦0 ↜ x⟧.abs

            unfold open' at h2
            rw [<- open_close] at h2
            grind

rw [open_close_var] not work here

[chenson2018]

I'm skeptical that making these abbrev is what we want, because it seems that outside the abstraction case we don't want this unfolding. Maybe instead we should add lemmas rewriting into the (open|close)Rec versions?

[lengyijun]

we don't want this unfolding

Is there any example?

we should add lemmas rewriting into the (open|close)Rec versions

Do we really want to add two equivalent versions of open_close? That would only confuse users and force them into trial-and-error among four different variants.

[lengyijun]

#799