Skip to content

feat(LambdaCalculus/Named/Untyped): Alpha equivalence equalities #741

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
chris-anto-froeschl wants to merge 12 commits into
base: main
Choose a base branch
from
+1,770 −214
Open

feat(LambdaCalculus/Named/Untyped): Alpha equivalence equalities #741

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
3b229d2
add named representation update from https://github.com/leanprover/cs…
chris-anto-froeschl Jun 1, 2026
a307463
adds paper to be formalized
chris-anto-froeschl Jun 1, 2026
5445d35
solves alphaEquiv_iff_alphaEquivPFresh while adding necessary swap pr…
chris-anto-froeschl Jun 8, 2026
7208fb7
converges theorem 4.1 much closer to how the paper proof is structure…
chris-anto-froeschl Jun 27, 2026
1a33860
refactors AlphaEquiv.swap_preserve to align more with 27 cases paper …
chris-anto-froeschl Jul 20, 2026
5e12d6f
removes lemma 6.6 for now
chris-anto-froeschl Jul 20, 2026
3197953
adjusts lemma 6.2 to be more general using actual permutations
chris-anto-froeschl Jul 20, 2026
d8a4a68
simplifies proof structures, moves major definitions into bundled file
chris-anto-froeschl Jul 20, 2026
3a3fd8f
removes paper from repo
chris-anto-froeschl Jul 20, 2026
ed8d98b
switches to mathlibs Equiv.swap to build coherent picture wrt permuta…
chris-anto-froeschl Jul 21, 2026
fc711a7
simplifies minor proof notions
chris-anto-froeschl Jul 22, 2026
351b37e
runs lake exe mk_all
chris-anto-froeschl Jul 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
246 changes: 124 additions & 122 deletions Cslib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,122 +1,124 @@
module -- shake: keep-all

public import Cslib.Algorithms.Lean.MergeSort.MergeSort
public import Cslib.Algorithms.Lean.TimeM
public import Cslib.Computability.Automata.Acceptors.Acceptor
public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
public import Cslib.Computability.Automata.DA.Basic
public import Cslib.Computability.Automata.DA.Buchi
public import Cslib.Computability.Automata.DA.Congr
public import Cslib.Computability.Automata.DA.Prod
public import Cslib.Computability.Automata.DA.ToNA
public import Cslib.Computability.Automata.EpsilonNA.Basic
public import Cslib.Computability.Automata.EpsilonNA.ToNA
public import Cslib.Computability.Automata.NA.Basic
public import Cslib.Computability.Automata.NA.BuchiEquiv
public import Cslib.Computability.Automata.NA.BuchiInter
public import Cslib.Computability.Automata.NA.Concat
public import Cslib.Computability.Automata.NA.Hist
public import Cslib.Computability.Automata.NA.Loop
public import Cslib.Computability.Automata.NA.Pair
public import Cslib.Computability.Automata.NA.Prod
public import Cslib.Computability.Automata.NA.Sum
public import Cslib.Computability.Automata.NA.ToDA
public import Cslib.Computability.Automata.NA.Total
public import Cslib.Computability.Languages.Congruences.BuchiCongruence
public import Cslib.Computability.Languages.Congruences.RightCongruence
public import Cslib.Computability.Languages.ExampleEventuallyZero
public import Cslib.Computability.Languages.Language
public import Cslib.Computability.Languages.OmegaLanguage
public import Cslib.Computability.Languages.OmegaRegularLanguage
public import Cslib.Computability.Languages.RegularLanguage
public import Cslib.Computability.Machines.SingleTapeTuring.Basic
public import Cslib.Computability.URM.Basic
public import Cslib.Computability.URM.Computable
public import Cslib.Computability.URM.Defs
public import Cslib.Computability.URM.Execution
public import Cslib.Computability.URM.StandardForm
public import Cslib.Computability.URM.StraightLine
public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
public import Cslib.Foundations.Control.Monad.Free
public import Cslib.Foundations.Control.Monad.Free.Effects
public import Cslib.Foundations.Control.Monad.Free.Fold
public import Cslib.Foundations.Data.BiTape
public import Cslib.Foundations.Data.FinFun
public import Cslib.Foundations.Data.HasFresh
public import Cslib.Foundations.Data.Nat.Segment
public import Cslib.Foundations.Data.OmegaSequence.Defs
public import Cslib.Foundations.Data.OmegaSequence.Flatten
public import Cslib.Foundations.Data.OmegaSequence.InfOcc
public import Cslib.Foundations.Data.OmegaSequence.Init
public import Cslib.Foundations.Data.OmegaSequence.Temporal
public import Cslib.Foundations.Data.RelatesInSteps
public import Cslib.Foundations.Data.Relation
public import Cslib.Foundations.Data.Set.Saturation
public import Cslib.Foundations.Data.StackTape
public import Cslib.Foundations.Lint.Basic
public import Cslib.Foundations.Logic.InferenceSystem
public import Cslib.Foundations.Logic.LogicalEquivalence
public import Cslib.Foundations.Semantics.FLTS.Basic
public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
public import Cslib.Foundations.Semantics.FLTS.Prod
public import Cslib.Foundations.Semantics.LTS.Basic
public import Cslib.Foundations.Semantics.LTS.Bisimulation
public import Cslib.Foundations.Semantics.LTS.Divergence
public import Cslib.Foundations.Semantics.LTS.Execution
public import Cslib.Foundations.Semantics.LTS.HasTau
public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic
public import Cslib.Foundations.Semantics.LTS.Notation
public import Cslib.Foundations.Semantics.LTS.OmegaExecution
public import Cslib.Foundations.Semantics.LTS.Relation
public import Cslib.Foundations.Semantics.LTS.Simulation
public import Cslib.Foundations.Semantics.LTS.Termination
public import Cslib.Foundations.Semantics.LTS.Total
public import Cslib.Foundations.Semantics.LTS.TraceEq
public import Cslib.Foundations.Semantics.LTS.Union
public import Cslib.Foundations.Syntax.Congruence
public import Cslib.Foundations.Syntax.Context
public import Cslib.Foundations.Syntax.HasAlphaEquiv
public import Cslib.Foundations.Syntax.HasSubstitution
public import Cslib.Foundations.Syntax.HasWellFormed
public import Cslib.Init
public import Cslib.Languages.CCS.Basic
public import Cslib.Languages.CCS.BehaviouralTheory
public import Cslib.Languages.CCS.Semantics
public import Cslib.Languages.CombinatoryLogic.Basic
public import Cslib.Languages.CombinatoryLogic.Confluence
public import Cslib.Languages.CombinatoryLogic.Defs
public import Cslib.Languages.CombinatoryLogic.Evaluation
public import Cslib.Languages.CombinatoryLogic.List
public import Cslib.Languages.CombinatoryLogic.Recursion
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.StrongNorm
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
public import Cslib.Logics.HML.Basic
public import Cslib.Logics.HML.LogicalEquivalence
public import Cslib.Logics.LinearLogic.CLL.Basic
public import Cslib.Logics.LinearLogic.CLL.CutElimination
public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
public import Cslib.Logics.Propositional.Defs
import Cslib.Algorithms.Lean.MergeSort.MergeSort
import Cslib.Algorithms.Lean.TimeM
import Cslib.Computability.Automata.Acceptors.Acceptor
import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
import Cslib.Computability.Automata.DA.Basic
import Cslib.Computability.Automata.DA.Buchi
import Cslib.Computability.Automata.DA.Congr
import Cslib.Computability.Automata.DA.Prod
import Cslib.Computability.Automata.DA.ToNA
import Cslib.Computability.Automata.EpsilonNA.Basic
import Cslib.Computability.Automata.EpsilonNA.ToNA
import Cslib.Computability.Automata.NA.Basic
import Cslib.Computability.Automata.NA.BuchiEquiv
import Cslib.Computability.Automata.NA.BuchiInter
import Cslib.Computability.Automata.NA.Concat
import Cslib.Computability.Automata.NA.Hist
import Cslib.Computability.Automata.NA.Loop
import Cslib.Computability.Automata.NA.Pair
import Cslib.Computability.Automata.NA.Prod
import Cslib.Computability.Automata.NA.Sum
import Cslib.Computability.Automata.NA.ToDA
import Cslib.Computability.Automata.NA.Total
import Cslib.Computability.Languages.Congruences.BuchiCongruence
import Cslib.Computability.Languages.Congruences.RightCongruence
import Cslib.Computability.Languages.ExampleEventuallyZero
import Cslib.Computability.Languages.Language
import Cslib.Computability.Languages.OmegaLanguage
import Cslib.Computability.Languages.OmegaRegularLanguage
import Cslib.Computability.Languages.RegularLanguage
import Cslib.Computability.Machines.SingleTapeTuring.Basic
import Cslib.Computability.URM.Basic
import Cslib.Computability.URM.Computable
import Cslib.Computability.URM.Defs
import Cslib.Computability.URM.Execution
import Cslib.Computability.URM.StandardForm
import Cslib.Computability.URM.StraightLine
import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
import Cslib.Foundations.Control.Monad.Free
import Cslib.Foundations.Control.Monad.Free.Effects
import Cslib.Foundations.Control.Monad.Free.Fold
import Cslib.Foundations.Data.BiTape
import Cslib.Foundations.Data.FinFun
import Cslib.Foundations.Data.HasFresh
import Cslib.Foundations.Data.Nat.Segment
import Cslib.Foundations.Data.OmegaSequence.Defs
import Cslib.Foundations.Data.OmegaSequence.Flatten
import Cslib.Foundations.Data.OmegaSequence.InfOcc
import Cslib.Foundations.Data.OmegaSequence.Init
import Cslib.Foundations.Data.OmegaSequence.Temporal
import Cslib.Foundations.Data.RelatesInSteps
import Cslib.Foundations.Data.Relation
import Cslib.Foundations.Data.Set.Saturation
import Cslib.Foundations.Data.StackTape
import Cslib.Foundations.Lint.Basic
import Cslib.Foundations.Logic.InferenceSystem
import Cslib.Foundations.Logic.LogicalEquivalence
import Cslib.Foundations.Semantics.FLTS.Basic
import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
import Cslib.Foundations.Semantics.FLTS.Prod
import Cslib.Foundations.Semantics.LTS.Basic
import Cslib.Foundations.Semantics.LTS.Bisimulation
import Cslib.Foundations.Semantics.LTS.Divergence
import Cslib.Foundations.Semantics.LTS.Execution
import Cslib.Foundations.Semantics.LTS.HasTau
import Cslib.Foundations.Semantics.LTS.LTSCat.Basic
import Cslib.Foundations.Semantics.LTS.Notation
import Cslib.Foundations.Semantics.LTS.OmegaExecution
import Cslib.Foundations.Semantics.LTS.Relation
import Cslib.Foundations.Semantics.LTS.Simulation
import Cslib.Foundations.Semantics.LTS.Termination
import Cslib.Foundations.Semantics.LTS.Total
import Cslib.Foundations.Semantics.LTS.TraceEq
import Cslib.Foundations.Semantics.LTS.Union
import Cslib.Foundations.Syntax.Congruence
import Cslib.Foundations.Syntax.Context
import Cslib.Foundations.Syntax.HasAlphaEquiv
import Cslib.Foundations.Syntax.HasSubstitution
import Cslib.Foundations.Syntax.HasWellFormed
import Cslib.Init
import Cslib.Languages.CCS.Basic
import Cslib.Languages.CCS.BehaviouralTheory
import Cslib.Languages.CCS.Semantics
import Cslib.Languages.CombinatoryLogic.Basic
import Cslib.Languages.CombinatoryLogic.Confluence
import Cslib.Languages.CombinatoryLogic.Defs
import Cslib.Languages.CombinatoryLogic.Evaluation
import Cslib.Languages.CombinatoryLogic.List
import Cslib.Languages.CombinatoryLogic.Recursion
import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.StrongNorm
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivDefs
import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivEquiv
import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
import Cslib.Languages.LambdaCalculus.Named.Untyped.SwapProperties
import Cslib.Logics.HML.Basic
import Cslib.Logics.HML.LogicalEquivalence
import Cslib.Logics.LinearLogic.CLL.Basic
import Cslib.Logics.LinearLogic.CLL.CutElimination
import Cslib.Logics.LinearLogic.CLL.EtaExpansion
import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
import Cslib.Logics.Propositional.Defs
Loading