Lambda calculus

Stream: computer science

[Alexander Bentkamp]

Hello,
Does anyone know of a formalization of the lambda calculus in Lean?
In particular termination of beta/eta reduction?

[Patrick Massot]

I would have a look at https://github.com/leanprover/mathlib/tree/master/computability (but maybe this is something else)

[Patrick Massot]

And, if it doesn't exist, maybe having a look at https://github.com/leanprover/mathlib/blob/5613d2ecc92ce8fae9555745bd94756dec61a323/group_theory/free_group.lean#L127 and https://github.com/leanprover/mathlib/blob/57194fa57e76721a517d6969ee88a6007f0722b3/logic/relation.lean#L288 could be a good idea

[Mario Carneiro]

I don't think lambda calculus has been done, although there are several projects in the same space

[Mario Carneiro]

I assume you are talking about simply typed lambda calculus, since of course the regular kind doesn't terminate

[Mario Carneiro]

I believe Jeremy has a formalization of lambda calculus, although he intended it for different purposes and I don't think he proved this property

[Mario Carneiro]

aha, here it is: https://github.com/avigad/embed/blob/master/src/exp.lean

[Mario Carneiro]

it's not much more than the definition

[Mario Carneiro]

I guess he never defined typechecking for lambda terms, since he was going for FOL

[Alexander Bentkamp]

Ok, thanks for the pointers. I will think about whether I'd like to work on this then. Actually, I'd like to formalize a unification procedure for lambda-terms, but I will need a formalization of the lambda-calculus for that first :-)

[Kenny Lau]

I might be missing something obvious here

[Kenny Lau]

but what happened to the Y-combinator?

[Kenny Lau]

oh, that's what "simply typed" rules out isn't it

[Alexander Bentkamp]

Yes, I wasn't very precise. I meant simply typed lambda calculus.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hey, I'm actually working on this right now! Is there any particular formulation that you want to use? I'm trying to figure out inherently typed terms at the moment, but I have a formulation in raw terms with a typechecking procedure and a proof of progress, basically following "Software Foundations".

[Alexander Bentkamp]

Oh, that's great! As I said, I actually would like to formalize a unification procedure for lambda-terms. So if I could build on your library once it's finished, that would be perfect. I find it hard to predict which formulation would be more suitable for this, but I guess it doesn't matter too much.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It's not pretty code and definitely not suitable for a library, but I can upload it somewhere like git when I have a bit more time if that helps your project :)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

By the way, you mean unification of the entire term assuming some holes on one (or both?) sides, not just types, right?

[Alexander Bentkamp]

Yes, with holes on both sides, but the holes are realized as free variables. In addition to that, there are also constant symbols. So for example, one could ask for unifiers of f (X a) b and f c (Y d), where uppercase letters are variables and lowercase letters are constants. A unifier would be {X ↦ λZ. c; Y ↦ λZ. b}. The procedure is described here: https://www.sciencedirect.com/science/article/pii/0304397576900219

[Alexander Bentkamp]

So it sounds like you don't plan / don't have time to improve your code such that it would be usable as a library? If I decide to formalize lambda calculus myself, I will ask you again for what you've done. But currently, I tend to using Isabelle/HOL instead for this project (Oh, oh, high treason in this chat I suppose).

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oh, I do hope to make it fairly readable, just not the very partial raw-term formulation, which is what I have currently, but rather the inherently-typed one which I only started on. That said, I'm using quantified type theory to support linear typing, which is more general than simply-typed lambda, but can be instantiated (I think..) to simply-typed lambda.

[Josh Pollock]

We actually did some stlc in lean in the University of Washington's graduate PL class last fall: https://courses.cs.washington.edu/courses/cse505/17au/lec11/lean/stlc.lean

[Alexander Bentkamp]

Thanks! I'll have a closer look next year. Happy holidays :-)

[Paige Thomas]

I just started learning lambda calculus. If you don't mind explaining, I was wondering why the condition x2 \notin FV (e1) \/ x1 \notin FV (e) is not a part of the definition for lam_diff in is_subst?

[Mario Carneiro]

are you referring to a particular formalization?

[Paige Thomas]

Sorry, yes. The one that Josh Pollock posted a link to earlier in the thread.

[Mario Carneiro]

I think you are right. There are variable capturing substitutions that are admitted by is_subst

[Paige Thomas]

If that is the case, would adding that condition be the simplest fix?

[Paige Thomas]

If I try to add connectives like ∧ and ∨ to the inductive definition, I seem to get an error of "...contains variables that are not parameters". Are these permitted in inductive definitions?

[Paige Thomas]

Would this work?

inductive is_subst : expr → string → expr → expr → Prop
-- (λ y . P)[ x := N ] = (λ y . P [ x := N ]) if x ≠ y and y ∉ FV (N) or x ∉ FV (P)
| lam_diff : ∀ (y : string) (P : expr) (x : string) (N : expr) (e : expr),
    x ≠ y
    → ((¬ is_free N y) ∨ (¬ is_free P x))
    → is_subst P x N e
    → is_subst (expr.lam y P) x N (expr.lam y e)

[Kenny Lau]

meta constant is_free : expr → string → Prop

meta inductive is_subst : expr → string → expr → expr → Prop
-- (λ y . P)[ x := N ] = (λ y . P [ x := N ]) if x ≠ y and y ∉ FV (N) or x ∉ FV (P)
| lam_diff : ∀ (y : string) (P : expr) (x : string) (N : expr) (e : expr),
    x ≠ y
    → ((¬ is_free N y) ∨ (¬ is_free P x))
    → is_subst P x N e
    → is_subst (expr.lam y sorry P sorry) x N (expr.lam y sorry e sorry)

[Kenny Lau]

this works for me verbatim

[Paige Thomas]

Thank you. Do you think this would be a good fix for the definition?

[Kenny Lau]

no because it has sorry

[Paige Thomas]

I'm sorry, I didn't mean verbatim, but if the definition was amended in this manner.

[Kenny Lau]

my point is that I didn't change the part you complained about

[Kenny Lau]

i.e. your diagnosis is not very accurate

[Paige Thomas]

The diagnosis about the error message or about the definition in the link that Josh posted? My post may have been confusing. I don't get error messages for the code I posted, it was changed to avoid them. I was asking if it worked to fix the definition that Josh posted.

[Kenny Lau]

oh... context...

[Paige Thomas]

Sorry about that.

[Fabrizio Montesi]

Moving the discussion with @Chris Henson on an 'upstream' Lambda calculus from #general > cslib to here, hope it's ok.

@Chris Henson To make the discussion more concrete, I've kickstarted a 'Computability' directory with a plain old definition for the syntax of lambda-calculus and free/bound variables: https://github.com/cs-lean/cslib/blob/main/Cslib/Computability/LambdaCalculus/Untyped/Basic.lean

The strategy I'm proposing is that we define in there the presentation that most people are used to, even if it will of course give the expected complications with capture-avoiding substitution. I would then like to have alternative syntaxes (De Brujin indeces, nameless, etc.) living in separate files as well. This will enable formally proving that these alternative presentations are 'correct'.
It doesn't need to be done all at once, I'd be perfectly ok with having the alternatives proceed at different speeds (also because there's potentially a lot of stuff to do, which will likely require multiple people: on top of syntax, there are several established evaluation strategies, which we should allow for side-by-side as well). So if you have some particular definition, we can go ahead with it while the 'plain old' definition still cooks.
I think it's valuable to discuss the outlook though.

What do you think?

[Fabrizio Montesi]

(you'll find in there a substitution relation, that should become a function to an Option, I guess.. will hack it later)

[Yicheng Qian]

I have a formalization of untyped lambda calculus and a proof of the substitution lemma written a while ago: https://github.com/PratherConid/LeanLambda. It uses the "plain old definition" where free/bound variables are strings instead of de-brujin indices. readme.md gives an extensive sketch of the proof. The proof can definitely be simplified.

[Fabrizio Montesi]

Yicheng Qian said:

I have a formalization of untyped lambda calculus and a proof of the substitution lemma written a while ago: https://github.com/PratherConid/LeanLambda. It uses the "plain old definition" where free/bound variables are strings instead of de-brujin indices. readme.md gives an extensive sketch of the proof. The proof can definitely be simplified.

very nice! it's pretty near to the direction i'm following (modulo some minor differences, like I'm abstracting from what the type of variables is, but that's likely easily fixable).

What are you doing in subst here?

| .lam y M => if y = x then .lam y M else
  let z := List.find_string_not_in (x :: (avar M ++ avar N))
  .lam z (subst x N (rename y z M))

in particular, could you explain how you're making subst a total function? What happens when there's capturing?

[Yicheng Qian]

List.find_string_not_in xs returns a string that's not in xs, so using this here prevents capturing.

[Yicheng Qian]

It's not efficient though, but we could define a version which uses cache and prove that they are equivalence.

[Fabrizio Montesi]

Ah, I see! This means assuming that the type of variables is not finite, and that there is a way of getting one such 'fresh' name. (This is often done in pen-and-paper presentations as well.) I don't have these assumptions but we could add them for sure.

[Chris Henson]

I have done deBrujin indices and locally nameless, both currently with proofs of confluence for a beta reduction. (It has pairs and a unit type because I need that for my research, but this could be removed for upstreaming). I think it would be nice to have a normalization proof too. https://github.com/chenson2018/LeanScratch/tree/main/LeanScratch

It sounds like the desire is to have multiple formulations for representing syntax, so a subdirectory for each? Maybe proofs that they preserve certain proofs? I will also be working on System F in the near future.

[Fabrizio Montesi]

Chris Henson said:

I have done deBrujin indices and locally nameless, both currently with proofs of confluence for a beta reduction. (It has pairs and a unit type because I need that for my research, but this could be removed for upstreaming). I think it would be nice to have a normalization proof too. https://github.com/chenson2018/LeanScratch/tree/main/LeanScratch

It sounds like the desire is to have multiple formulations for representing syntax, so a subdirectory for each? Maybe proofs that they preserve certain proofs? I will also be working on System F in the near future.

Agree on the multiple subdirs ('HOAS'? 'nameless'?).
I think we're gonna encounter this situation again and again (e.g., pi-calculus), so it's good to use this as a testbed.
Say that the formalisation that aims to be near to the plain pen and paper presentation is called 'Plain'. What I'm currently doing is that the plain presentation is in the main directory (currently Computability/LambdaCalculus/Untyped, which contains only a Basic file for now). We could also make a 'Plain' subdirectory, I guess. I wonder if Plain is a good name though, hence why I'm simply putting the plain presentation in the main directory for now.

[Fabrizio Montesi]

And I've been looking at your repo, nice stuff.

[Fabrizio Montesi]

I've tried to draft the 'subst that gets a fresh name' here, akin to what @Yicheng Qian's subst: https://github.com/cs-lean/cslib/blob/1dc4c6fefe6715d3f0e11a84d9bf99ee09b6bfa3/Cslib/Computability/LambdaCalculus/Untyped/Basic.lean#L57

Any idea on how to elegantly define that Term.freshVar function that I'm invoking there, without fixing type Var? Maybe there's something useful in mathlib about infinite types for that? (I've asked here as well: #Is there code for X? > Get a 'fresh' element not in a Finset.)

[Fabrizio Montesi]

We could of course make our own class, but I'd rather reuse something if it exists.

[Yicheng Qian]

I'd also like to point out that the fact that variables might be captured made the proof much more complicated than I expected. There are several theorems that are supposed to be proven by induction, where I had to apply variable renaming to some lambda terms in the middle of the proof to avoid variable capturing, and that had the inadvertent effect of making the induction hypothesis unapplicable, which forced me to change the statement of the theorem to strengthen the induction hypothesis.
But I think most of this could be avoided if I had't decided to stick to the named approach throughout the entire proof. I imagine the proof would be much shorter if we define a translation between named terms and nameless terms and transfer the properties.

[Fabrizio Montesi]

Right!
I think I've reached something reasonable to define substitution and the assumption that we need a fresh variable generator. See https://github.com/cs-lean/cslib/blob/2439f43103a78c5dc02f8530b7923248cf8795d3/Cslib/Computability/LambdaCalculus/Untyped/Basic.lean#L86

Next steps would probably be to define one of the thousand semantics in a subdir (I guess cbv for starters) and a more convenient formulation (HOASLambdaCalculus?) in another subdir. Then establish an encoding from LambdaCalculus.Term to HOASLambdaCalculus.Term, and we could even try to prove that the encoding is a Bisimulation (e.g., on the lts obtained by lifting the reduction relation to a transition relation where all labels are tau; I could make this more convenient from the LTS files).

Let me know if anybody is up for working a bit on that.

Some of these names are getting long... :-)

[Thomas Waring]

Hi all — would there be any interest in a formalisation of combinator logic? Coincidentally I have been working on one for the past few days as an exercise (I'm quite fresh to lean) — see here — & modulo a LOT of tidying up I might have something that is useful.

So far I've formalised:

• Definitions, using the "SKI" basis, of single-step and large reduction.
• The Church-Rosser theorem: that the relation of having a common reduct is an equivalence (using Tait & Martin-Löf's parallel reduction).
• "Bracket abstraction" (as it is termed here): for a term $T(x_1, \dots, x_n)$ with some number of "holes" $x_i$ (I've called such an object a "context"), a combinatory term $[x]T$ such that $T \cdot t_1 \cdot \dots \cdot t_n$ reduces to $T(t_1,\dots,t_n)$ for any terms $t_i$.
• Definitions of all the usual auxiliary combinators, pairs and (a start on) booleans — I did this before bracket abstraction, so I could make those proofs a lot shorter now.
• Church numerals: I defined a term $t$ to represent a natural number $n$ iff for any terms $f,x$, $t \cdot f \cdot x$ reduces to $f \cdot (f \cdot \dots (f \cdot x) \dots ))$, with $n$ $f$ in the middle. With this I have addition, multiplication, predecessor (urgh), ordering and primitive recursion — again this could be cleaned up with bracket abstraction.
• Unbounded root finding: a term $\texttt{RFind}$ such that, given a function $f_\mathbb{N} : \mathbb{N} \to \mathbb{N}$ and a term $f$ representing it (in the obvious Church-numeral sense), if there exists $n$ such that $f_\mathbb{N} (n) = 0$, $\texttt{RFind} \cdot f$ reduces to a term representing the minimum such $n$.

I'm not sure exactly the right way to formalise this idea, but all of those together more-or-less express that combinators have the same power as general recursive functions as formalised in Mathlib.

Obviously combinators are a pretty arcane way to program, but it does avoid the many problems & choices related to syntax conventions, free / bound variables / etc that has been discussed above. Let me know if there's any interest!

[Fabrizio Montesi]

Definitely intersting! SKI is used, among other things, in a lot of recent and very interesting research on higher-order mathematical semantics.

[Fabrizio Montesi]

I'm near enough for reviewing it, but I'm gonna try to get an expert on board for discussing this. We have at least one in our same section at the workplace.

[Thomas Waring]

Wonderful news — keep me updated on what my next steps should be, in the meantime I'll start tidying up my code in a way that seems reasonable to me. I'd also be very interested in seeing that research! It sounds close to the area of my PhD

[Fabrizio Montesi]

You can just create a fork when you like and start adding definitions.

We're trying to be careful with notation, using type classes when possible to reuse them across different models. But don't think too much about it for now. Just try to be economical with new notations.

[Fabrizio Montesi]

It'd be very good if you could add a reference to a pen-and-paper presentation (or other useful refs) at the beginning, so that one can compare to the formalisation.

[Thomas Waring]

Great, will do. I haven’t been working from a particular pen-and-paper presentation, but I will have a look for one or else write up something rough of my own.

[Fabrizio Montesi]

It's SKI, hopefully Google will be able to help. :⁠-⁠)

[Chris Henson]

One thing that could be shared between all the lambda calculi and SKI are a few notations and theorems about reflexive transitive relations. As an example, in my own repo I have this file separated out: https://github.com/chenson2018/LeanScratch/blob/main/LeanScratch/Confluence/Basic.lean

I see similar patterns in your SKI formalization (which I think looks pretty good btw!), so maybe we can extract some pieces that are general.

[Fabrizio Montesi]

Absolutely.
Some of those things are also very similar to what I have for LTSs (see mtr and str): https://github.com/cs-lean/cslib/blob/main/Cslib/Semantics/LTS/Basic.lean

Further, a reduction relation can be seen as an LTS with only tau-labels.

We'll need Diamond and Confluence also for LTSs, and then also definitions for non-interference, serialisable... we should try to keep these concepts as general as possible.

[Fabrizio Montesi]

The opposite is also true: if one restricts the transition relation of an LTS to a single label (e.g., tau), then one gets a relation.

I just wonder if it can be made to work nicely. That is, I wouldn't want to force people interested only in simple reduction relations to see the LTS API. Maybe we can at least have 'to' and 'from' defs between Rel and LTS and then use the LTS API internally to prove
theorems about reductions

[Thomas Waring]

Chris Henson said:

One thing that could be shared between all the lambda calculi and SKI are a few notations and theorems about reflexive transitive relations.

I agree — there were even a couple of things that felt like they should be in (or at least semi-trivially derivable from) Mathlib, I'm thinking specifically of the Transitive instances between single step and multi reduction.

For the moment I think I'll try to split off the relevant lemmas into their own file, and prove them in a reasonably general form — with the understanding that later they might become corollaries of LTS results etc

[Fabrizio Montesi]

formalised my mesg a bit (toRel and toLTS): https://github.com/cs-lean/cslib/blob/f07cd5d92bee90aa09fabf3d8112d1c87e867477/Cslib/Semantics/LTS/Basic.lean#L71

At the very least we should be able to prove that rel.toLTS.Diamond <-> rel.Diamond.

[Fabrizio Montesi]

(I still have to define Diamond for lts but it's as for Rel, just add transition labels)

[Chris Henson]

I just opened a PR adding some definitions for a locally nameless lambda calculus. My intent would be to follow up with definitions for reduction and proofs of confluence and strong normalization.

[Thomas Waring]

I'll have a (rather large) PR up tomorrow I think, formalising the things I mentioned in my first message (plus documentation, some major tidying, etc)

[Fabrizio Montesi]

Chris Henson said:

I just opened a PR adding some definitions for a locally nameless lambda calculus. My intent would be to follow up with definitions for reduction and proofs of confluence and strong normalization.

Great, thank you! I'm in the process of trying to figure out how to manage notation across all these languages, I'll open a topic about that so that we can discuss it together.

RE your use of simp attributes: I've tried to avoid annotating stuff for aesop and simp so far because (1) sometimes simping too much makes using theorems harder, and (2) grind has arrived. I wonder if it's a good opportunity to learn grind, but we don't need to do that now ofc. But if you're adding simp-annotations for aesop, I'd suggest to create a ruleset with the simps you need instead of annotating the lemmas. This has been very useful in one of our internal projects.

RE the notation for substitution: you can instantiate the class HasSubstitution to get the notation.

[Chris Henson]

@Fabrizio Montesi I have addressed each of your comments on the PR. I've not very advanced in my aesop usage, could you clarify a bit about using a ruleset here? Is what you're suggesting to remove all of the simp attributes I currently have on definitions in LocallyNameless/Basic.lean and place them in a ruleset? Besides these, the only lemma I annotated was HasFresh.fresh_notMem.

[Tristan Figueroa-Reid]

I'm not sure if golfing is welcome, but there's some opportunity for automation just within this untyped lambda calculus file itself in CSLib:

/-- Renaming preserves size. -/
@[simp]
theorem Term.rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] : sizeOf (m.rename x y) = sizeOf m := by
  induction m <;> aesop (add simp [Term.rename])

-- or, the decreasing_by proof for Term.subst - should grind be attached to eq_sizeOf calls?
decreasing_by all_goals grind [rename.eq_sizeOf, abs.sizeOf_spec, app.sizeOf_spec]

[Fabrizio Montesi]

@Chris Henson @Tristan Figueroa-Reid In an internal project over-annotating with simp made our codebase brittle, so I might've become over-conservative. Admittedly, that might've been because we used simp in the middle of proofs, which I read somewhere is discouraged in mathlib. Is there a guide somewhere on how to manage simp-annotations and golfing wrt maintainability?

[Chris Henson]

Are you meaning this page that includes a section on non-terminal simp? Happy to update to adhere to this, I just wasn't really thinking about it when I originally wrote this in a repo only I used.

[Fabrizio Montesi]

Chris Henson said:

Are you meaning this page that includes a section on non-terminal simp? Happy to update to adhere to this, I just wasn't really thinking about it when I originally wrote this in a repo only I used.

Yes, that's the one, thanks.
I think it makes very good sense, so I'd follow it (not sure I've been following it 100% myself, I'll have a look at my own code later).

[Fabrizio Montesi]

@Tristan Figueroa-Reid that means golfing is welcome, as long as proofs remain understandable and fast. In fact, I'd be very interested in leveraging grind in the codebase.

[Fabrizio Montesi]

@Chris Henson Your simp annotations also seem to make sense, now that I'm a bit wiser from reading the docs. As long as we don't use simp mid-proof, so that's good to avoid. Let me know when you've done a pass at your pr.

[Chris Henson]

@Fabrizio Montesi I have pushed a commit that makes all simps either terminal or limited to simp only.

[Fabrizio Montesi]

Chris Henson said:

Fabrizio Montesi I have pushed a commit that makes all simps either terminal or limited to simp only.

I put a couple of minor comments, please feel free to correct me if I understood the mathlib styling wrong. They're very simple stuff, and after those I think it's ready to be merged.

[Chris Henson]

@Fabrizio Montesi Thanks for merging! I see I broke a test by changing the directory structure, I'll make a quick PR to fix. I see there is a workflow that might have caught this, but I think you have to approve it to run on our PRs?

[Fabrizio Montesi]

Oh, it should just run for all PRs.. I'll double check, thanks for spotting this.

[Notification Bot]

This topic was moved here from #general > Lambda calculus by Bryan Gin-ge Chen.

[Ka Wing Li]

It would be great if we can have one for fresh string, particularly in locally nameless setting.

[Fabrizio Montesi]

One what? Do you mean an instance of HasFresh?

[Ka Wing Li]

Yes

[Ka Wing Li]

@Fabrizio Montesi Such as

instance : HasFresh String :=

[Fabrizio Montesi]

It'd definitely be nice to have it. For something legible, one could go by alphabetical ordering on ascii characters and get the 'next one' (resetting and suffixing with an additional character whenever the end is reached). But we could also just take the longest string in the set and add a suffix character.

[Fabrizio Montesi]

@Chris Henson Do I understand correctly that locally closed nameless lambda terms should correspond to named lambda terms?

[Chris Henson]

They should both represent the "same" STLC, yes. We could prove this at some point! We have named and locally nameless, I think the other common representation we're missing would be regular de Bruijn indices. All three should be able to soundly be transformed into each other.

[Fabrizio Montesi]

That's one of the things I was hoping we could do at some point. Let me sketch a thing...

[Chris Henson]

There was recently an interesting thesis that touches on this, deriving each of these three approaches from a common monadic framework formalized in Rocq. (Not saying I want to replicate this per se, just mentioning since it's relevant)

[Fabrizio Montesi]

Something like this: https://github.com/cs-lean/cslib/blob/lambda-nameless-adequacy/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Adequacy.lean

[Chris Henson]

Yes, something like that. Maybe more idiomatic to say something with docs#Mathlib.Logic.Equiv.Defs.Equiv? Going both directions is potentially annoying though. Would be nice to state equivalent reductions as well.

[Fabrizio Montesi]

the other direction is trickier, we could either refer to the image of toNameless or try to make a (requires nonobvious design choices) deterministic toNamed function.

[Fabrizio Montesi]

I'll sketch what the first looks like.

[Fabrizio Montesi]

For the semantics, we could state a bisimulation or even an isomorphism result.

[Fabrizio Montesi]

Something like (for alpha-equiv):

/-- Two named terms are α-equivalent iff their locally nameless variants are equal. -/
theorem named_locallyNameless_alphaEquiv_iff_eq (m n : Named.Term Var) :
  m =α n ↔ m.toLocallyNameless = n.toLocallyNameless := by
  sorry

/-- Two locally-closed nameless terms are equal iff they are the nameless translation of
α-equivalent named terms. -/
theorem locallyNameless_lc_named_eq_iff_alphaEquiv (m n : LocallyNameless.Term Var) (hmlc : m.LC) (hnlc : n.LC) :
  m = n ↔ (∃ m' n' : Named.Term Var,
    m = m'.toLocallyNameless ∧ n = n'.toLocallyNameless ∧
    m' =α n') := by
  sorry

(Updated https://github.com/cs-lean/cslib/blob/lambda-nameless-adequacy/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Adequacy.lean)