diff --git a/Cslib.lean b/Cslib.lean index 3e5977af2..7e34ab53e 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -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 diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivDefs.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivDefs.lean new file mode 100644 index 000000000..4de0bab5e --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivDefs.lean @@ -0,0 +1,162 @@ +/- +Copyright (c) 2026 Chris Anto Fröschl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Anto Fröschl +-/ + +module + +public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic + +/-! # Definitions of α-equivalence + +Five definitions of α-equivalence from [Crole2012], each capturing the same equivalence +relation on expressions: + +* `∼p` (Definition 3.1): Permutation-based with non-occurrence side condition (`AlphaEquiv`) +* `∼p#` (Definition 3.2): Permutation-based with freshness side condition (`AlphaEquivPFresh`) +* `∼¹p` (Definition 3.3): Permutation-based with non-occurrence on bodies only (`AlphaEquivP1`) +* `∼r` (Definition 3.4): Traditional renaming axiom with non-occurrence (`AlphaEquivR`) +* `∼r#` (Definition 3.5): Renaming axiom with freshness (`AlphaEquivRFresh`) + +The first three definitions use the notion of *atom swapping* (transposition), introduced in +[Gabbay2002] (Section 2, page 3), as a primitive operation for defining α-equivalence. The +key observation from [Gabbay2002] is that α-equivalence can be defined using the notion of +atom swapping in lieu of the traditional renaming/substitution approach. + +The last two definitions use the traditional capture-avoiding substitution (renaming) axiom. + +## References + +* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012] +* [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with Variable Binding*][Gabbay2002] + +## Notation + +Following the paper [Crole2012], we use the following correspondence between the paper's +abstract syntax and the λ-calculus terms: + +| Paper | Lean | +|---------------|---------------------| +| `a` | `Term.var x` | +| `P(E₁, E₂)` | `Term.app m1 m2` | +| `B([a]E)` | `Term.abs x m` | +| `(z a) · E` | `m.swap x z` | +| `E{a'/a}` | `m.subst a (var a')`| +| `π · E` | `m.permute π` | + +-/ + +@[expose] public section + +namespace Cslib + +universe u + +variable {Var : Type u} [DecidableEq Var] [HasFresh Var] + +namespace LambdaCalculus.Named.Untyped.Term + +/-- The action `π · E` of a permutation on a term, as used in [Crole2012]. + +Since some lemmas in section 6 are proven for general permutations, we have to introduce +this notion here aswell and derive the special case using `swap` accordingly. +-/ +def permute (m : Term Var) (π : Equiv.Perm Var) : Term Var := + match m with + | var x => var (π x) + | abs x m => abs (π x) (m.permute π) + | app m n => app (m.permute π) (n.permute π) + +/-- The action of the transposition `(x y)` on a term: simultaneously swaps all occurrences +of `x` and `y`. Corresponds to `(x y) · E` in [Crole2012] (Section 2). + +`swap` is is one special case of a permutation: the transposition that exchanges exactly two atoms +a and b and fixes everything else. +-/ +def swap (m : Term Var) (x y : Var) : Term Var := m.permute (Equiv.swap x y) + +/-- **Definition 3.2** [Crole2012]: `∼p#` - α-equivalence via permutation with freshness +side condition. + +The rule `pi#` uses the freshness condition `z # a, b, E, E'` +(i.e., `z ∉ fv(E) ∪ fv(E') ∪ {a, b}`) instead of the non-occurrence condition +`z ∉ vars(E) ∪ vars(E') ∪ {a, b}` used in Definition 3.1 (`AlphaEquiv`). +-/ +inductive AlphaEquivPFresh : Term Var → Term Var → Prop where + | var {x : Var} : AlphaEquivPFresh (var x) (var x) + | abs {y x1 x2 : Var} {m1 m2 : Term Var} : + y ∉ ({x1, x2} : Finset Var) ∪ m1.fv ∪ m2.fv → + AlphaEquivPFresh (m1.swap x1 y) (m2.swap x2 y) → + AlphaEquivPFresh (abs x1 m1) (abs x2 m2) + | app {m1 n1 m2 n2 : Term Var} : + AlphaEquivPFresh m1 n1 → AlphaEquivPFresh m2 n2 → + AlphaEquivPFresh (app m1 m2) (app n1 n2) + +/-- **Definition 3.3** [Crole2012]: `∼¹p` - α-equivalence via permutation with non-occurrence +restricted to the bodies only. + +This definition is analogous to the definition of α-equivalence for λ-expressions in +[Gabbay1999a] (Theorem 2.1, page 216). The notation `∼¹p` arises from three variants `∼ⁱp` +of `∼p` considered in Proposition 4.3 of [Crole2012]. +-/ +inductive AlphaEquivP1 : Term Var → Term Var → Prop where + | var {x : Var} : AlphaEquivP1 (var x) (var x) + | abs {y x1 x2 m1 m2} : + y ∉ m1.vars ∪ m2.vars → + AlphaEquivP1 (m1.rename x1 y) (m2.rename x2 y) → + AlphaEquivP1 (abs x1 m1) (abs x2 m2) + | app {m1 n1 m2 n2 : Term Var} : + AlphaEquivP1 m1 n1 → AlphaEquivP1 m2 n2 → + AlphaEquivP1 (app m1 m2) (app n1 n2) + +/-- **Definition 3.4** [Crole2012]: `∼r` - α-equivalence via the traditional renaming axiom +with non-occurrence side condition. + +This definition is analogous to the definition of α-equivalence for λ-expressions most commonly +found in the literature. One of the first formal presentations is in [Church1941] and the same, +though rather less formal approach is taken by [Barendregt1985] (Definition 2.1.11). +-/ +inductive AlphaEquivR : Term Var → Term Var → Prop where + | refl {m : Term Var} : AlphaEquivR m m + | symm {m1 m2 : Term Var} : AlphaEquivR m1 m2 → AlphaEquivR m2 m1 + | trans {m1 m2 m3 : Term Var} : AlphaEquivR m1 m2 → AlphaEquivR m2 m3 → AlphaEquivR m1 m3 + | app {m1 n1 m2 n2 : Term Var} : + AlphaEquivR m1 n1 → AlphaEquivR m2 n2 → + AlphaEquivR (app m1 m2) (app n1 n2) + | abs_congr {x : Var} {m m' : Term Var} : + AlphaEquivR m m' → + AlphaEquivR (abs x m) (abs x m') + | alpha {x x' : Var} {m : Term Var} : + x' ∉ ({x} : Finset Var) ∪ m.vars → + AlphaEquivR (abs x m) (abs x' (m.subst x (var x'))) + +/-- **Definition 3.5** [Crole2012]: `∼r#` - α-equivalence via the renaming axiom with +freshness side condition. + +Same as `∼r` (Definition 3.4), but the renaming axiom uses a freshness side condition +(`a' ∉ {a} ∪ fv(E)`) instead of a non-occurrence condition (`a' ∉ {a} ∪ vars(E)`). + +This is analogous to the definition of α-equivalence for λ-expressions one finds in +[Hindley1988] (Section 1B, page 9). +-/ +inductive AlphaEquivRFresh : Term Var → Term Var → Prop where + | refl {m : Term Var} : AlphaEquivRFresh m m + | symm {m1 m2 : Term Var} : + AlphaEquivRFresh m1 m2 → AlphaEquivRFresh m2 m1 + | trans {m1 m2 m3 : Term Var} : + AlphaEquivRFresh m1 m2 → AlphaEquivRFresh m2 m3 → + AlphaEquivRFresh m1 m3 + | app {m1 m1' m2 m2' : Term Var} : + AlphaEquivRFresh m1 m1' → AlphaEquivRFresh m2 m2' → + AlphaEquivRFresh (app m1 m2) (app m1' m2') + | abs_congr {x : Var} {m m' : Term Var} : + AlphaEquivRFresh m m' → + AlphaEquivRFresh (abs x m) (abs x m') + | alpha {x x' : Var} {m : Term Var} : + x' ∉ ({x} : Finset Var) ∪ m.fv → + AlphaEquivRFresh (abs x m) (abs x' (m.subst x (var x'))) + +end LambdaCalculus.Named.Untyped.Term + +end Cslib diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivEquiv.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivEquiv.lean new file mode 100644 index 000000000..6369289ad --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/AlphaEquivEquiv.lean @@ -0,0 +1,128 @@ +/- +Copyright (c) 2026 Chris Anto Fröschl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Anto Fröschl +-/ + +module + +public import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties +public import Cslib.Languages.LambdaCalculus.Named.Untyped.SwapProperties + +/-! # Equivalence of α-equivalence definitions + +Theorems showing equivalence of the five definitions of α-equivalence from [Crole2012]: + +* `∼p` (Definition 3.1): permutation with non-occurrence side condition (`AlphaEquiv`) +* `∼p#` (Definition 3.2): permutation with freshness side condition (`AlphaEquivPFresh`) +* `∼¹p` (Definition 3.3): permutation with non-occurrence on bodies only (`AlphaEquivP1`) +* `∼r` (Definition 3.4): traditional renaming axiom with non-occurrence (`AlphaEquivR`) +* `∼r#` (Definition 3.5): renaming axiom with freshness (`AlphaEquivRFresh`) + +The main results are: + +* **Theorem 4.1** [Crole2012]: `∼p = ∼p#` (`alphaEquiv_iff_alphaEquivPFresh`) +* **Theorem 4.2** [Crole2012]: `∼p = ∼¹p` (`alphaEquiv_iff_alphaEquivP1`) +* **Theorem 4.4** [Crole2012]: `∼p = ∼r` (`alphaEquiv_iff_alphaEquivR`) +* **Theorem 4.5** [Crole2012]: `∼p = ∼r#` (`alphaEquiv_iff_alphaEquivRFresh`) +* **Theorem 4.6** [Crole2012]: `∼r = ∼r#` (`alphaEquivR_iff_alphaEquivRFresh`) + +## References + +* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012] +-/ + +@[expose] public section + +namespace Cslib + +universe u + +variable {Var : Type u} [DecidableEq Var] [HasFresh Var] + +namespace LambdaCalculus.Named.Untyped.Term + +omit [HasFresh Var] in +/-- Non-occurrence obviously implies freshness, and the `swap` operation coincides with +`rename` when the target variable does not occur in the term. +-/ +lemma alphaEquiv_of_alphaEquivPFresh {m n : Term Var} : AlphaEquiv m n → AlphaEquivPFresh m n := by + intro h + induction h with + | var => constructor + | abs z_h1 ih1 ih2 => + rename_i x z x1 x2 m1 m2 + have h1 : z ∉ ({x1, x2} : Finset Var) ∪ m1.fv ∪ m2.fv := by + simp_all [vars_either_fv_or_bv] + have h2 : AlphaEquivPFresh (m1.swap x1 z) (m2.swap x2 z) := by + grind [swap_eq_rename_of_not_mem_vars] + apply AlphaEquivPFresh.abs h1 h2 + | app h1 h2 ih1 ih2 => exact AlphaEquivPFresh.app ih1 ih2 + +lemma alphaEquivPFresh_of_alphaEquiv {m n : Term Var} : AlphaEquivPFresh m n → AlphaEquiv m n := by + intro h + induction h with + | var => constructor + | abs hy _h ih => + rename_i u a b E E' + -- We have: (u a) · E ∼p (u b) · E' (by induction: ih) and u # a, b, E, E' (by hy). + -- Extract freshness conditions from hy. + have hu_E : u ∉ E.fv := by aesop + have hu_E' : u ∉ E'.fv := by aesop + -- Pick z ≠ u with z ∉ vars(E) ∪ vars(E') ∪ {a, b} (stronger than freshness). + obtain ⟨z, hz⟩ : ∃ z : Var, z ∉ E.vars ∪ E'.vars ∪ {a, b, u} := by + exact Infinite.exists_notMem_finset (E.vars ∪ E'.vars ∪ {a, b, u}) + have hz_E : z ∉ E.vars := by aesop + have hz_E' : z ∉ E'.vars := by aesop + have hz_fv_E : z ∉ E.fv := by simp_all [vars_either_fv_or_bv] + have hz_fv_E' : z ∉ E'.fv := by simp_all [vars_either_fv_or_bv] + -- Using Lemma 6.1 we get + have h_swap : ((E.swap u a).swap z u) =α ((E'.swap u b).swap z u) := by + nth_rw 2 [swap_comm] + nth_rw 4 [swap_comm] + exact AlphaEquiv.swap_preserve ih + -- From Lemma 6.2 part 2 via agreement sets + have h_agree_E : ((E.swap u a).swap z u) =α (E.swap z a) := + swap_comp_alphaEquiv_of_not_mem_fv hu_E hz_fv_E + have h_agree_E' : ((E'.swap u b).swap z u) =α (E'.swap z b) := + swap_comp_alphaEquiv_of_not_mem_fv hu_E' hz_fv_E' + -- Chain by symmetry and transitivity of ∼p + -- (z a) · E ∼p (z u)·(u a)·E ∼p (z u)·(u b)·E' ∼p (z b) · E' + have h_chain : (E.swap z a) =α (E'.swap z b) := + AlphaEquiv.trans (AlphaEquiv.symm h_agree_E) (AlphaEquiv.trans h_swap h_agree_E') + -- Convert swap to rename (since z ∉ vars) and apply the pi rule. + -- Since z ∉ vars(E), swap z a = rename a z (by swap_comm + swap_eq_rename). + rw [swap_comm, swap_eq_rename_of_not_mem_vars hz_E] at h_chain + rw [swap_comm, swap_eq_rename_of_not_mem_vars hz_E'] at h_chain + exact AlphaEquiv.abs (by aesop) h_chain + | app _ _ ih1 ih2 => exact AlphaEquiv.app ih1 ih2 + +/-! ## Theorem 4.1 [Crole2012] -/ +theorem alphaEquiv_iff_alphaEquivPFresh (m n : Term Var) : AlphaEquiv m n ↔ AlphaEquivPFresh m n := + ⟨alphaEquiv_of_alphaEquivPFresh, alphaEquivPFresh_of_alphaEquiv⟩ + +/- +/-! ## Theorem 4.2 [Crole2012] -/ +theorem alphaEquiv_iff_alphaEquivP1 (m n : Term Var) : + AlphaEquiv m n ↔ AlphaEquivP1 m n := by + sorry + +/-! ## Theorem 4.4 [Crole2012] -/ +theorem alphaEquiv_iff_alphaEquivR (m n : Term Var) : + AlphaEquiv m n ↔ AlphaEquivR m n := by + sorry + +/-! ## Theorem 4.5 [Crole2012] -/ +theorem alphaEquiv_iff_alphaEquivRFresh (m n : Term Var) : + AlphaEquiv m n ↔ AlphaEquivRFresh m n := by + sorry + +/-! ## Theorem 4.6 [Crole2012] -/ +theorem alphaEquivR_iff_alphaEquivRFresh (m n : Term Var) : + AlphaEquivR m n ↔ AlphaEquivRFresh m n := by + sorry +-/ + +end LambdaCalculus.Named.Untyped.Term + +end Cslib diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean index c6adcca35..1f90634ef 100644 --- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Fabrizio Montesi. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi +Authors: Fabrizio Montesi, Haoxuan Yin -/ module @@ -10,25 +10,29 @@ public import Cslib.Foundations.Data.HasFresh public import Cslib.Foundations.Syntax.HasAlphaEquiv public import Cslib.Foundations.Syntax.HasSubstitution -@[expose] public section - /-! # λ-calculus -The untyped λ-calculus. +The untyped λ-calculus, with a named representation of variables. ## References * [H. Barendregt, *Introduction to Lambda Calculus*][Barendregt1984] +* Definition of α-equivalence [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with + Variable Binding*][Gabbay2002] +* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012] — the `AlphaEquiv` definition + corresponds to Definition 3.1 (∼p) in this paper -/ +@[expose] public section + namespace Cslib universe u -variable {Var : Type u} +variable {Var : Type u} [DecidableEq Var] [HasFresh Var] -namespace LambdaCalculus.Named +namespace LambdaCalculus.Named.Untyped /-- Syntax of terms. -/ inductive Term (Var : Type u) : Type u where @@ -37,52 +41,76 @@ inductive Term (Var : Type u) : Type u where | app (m n : Term Var) deriving DecidableEq +namespace Term + /-- Free variables. -/ -def Term.fv [DecidableEq Var] : Term Var → Finset Var +def fv : Term Var → Finset Var | var x => {x} - | abs x m => m.fv.erase x + | abs x m => m.fv \ {x} | app m n => m.fv ∪ n.fv /-- Bound variables. -/ -def Term.bv [DecidableEq Var] : Term Var → Finset Var +def bv : Term Var → Finset Var | var _ => ∅ - | abs x m => m.bv ∪ {x} -- Could also be `insert x m.bv` + | abs x m => m.bv ∪ {x} | app m n => m.bv ∪ n.bv /-- Variable names (free and bound) in a term. -/ -def Term.vars [DecidableEq Var] (m : Term Var) : Finset Var := - m.fv ∪ m.bv +def vars : Term Var → Finset Var + | var x => {x} + | abs x m => m.vars ∪ {x} + | app m n => m.vars ∪ n.vars -/-- Capture-avoiding substitution, as an inference system. -/ -inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term Var → Prop where - | varHit : (var x).Subst x r r - | varMiss : x ≠ y → (var y).Subst x r (var y) - | absShadow : (abs x m).Subst x r (abs x m) - | absIn : x ≠ y → y ∉ r.fv → m.Subst x r m' → (abs y m).Subst x r (abs y m') - | app : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n') - -/-- Renaming, or variable substitution. `m.rename x y` renames `x` into `y` in `m`. -/ -def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var := +/-- Variable renaming, applying to both free and bound variables. + `m.rename x y` changes all occurrences of `x` into `y` in `m`. -/ +def rename (m : Term Var) (x y : Var) : Term Var := match m with - | var z => if z = x then (var y) else (var z) - | abs z m' => - if z = x then - -- Shadowing - abs z m' - else - abs z (m'.rename x y) + | var z => var (if z = x then y else z) + | abs z m' => abs (if z = x then y else z) (m'.rename x y) | app n1 n2 => app (n1.rename x y) (n2.rename x y) +omit [HasFresh Var] in /-- 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 +theorem rename_eq_sizeOf {m : Term Var} {x y : Var} : sizeOf (m.rename x y) = sizeOf m := by induction m <;> aesop (add simp [Term.rename]) +/-- **Definition 3.1** [Crole2012]: `∼p` — α-equivalence via permutation (swapping) with +non-occurrence side condition. + +This definition is analogous to the definition of α-equivalence for λ-expressions in +[Gabbay2002] (Section 2, page 3). The `abs` rule uses the `rename` operation, which +coincides with `swap` when the witness variable `y` does not occur in the term. -/ +inductive AlphaEquiv : Term Var → Term Var → Prop where + | var {x} : AlphaEquiv (var x) (var x) + | abs {y x1 x2 m1 m2} : y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} → + AlphaEquiv (m1.rename x1 y) (m2.rename x2 y) → AlphaEquiv (abs x1 m1) (abs x2 m2) + | app {m1 n1 m2 n2} : AlphaEquiv m1 n1 → AlphaEquiv m2 n2 → AlphaEquiv (app m1 m2) (app n1 n2) + +/-- Instance for the notation `m =α n`. -/ +instance instHasAlphaEquivTerm : HasAlphaEquiv (Term Var) where + AlphaEquiv := AlphaEquiv + +omit [HasFresh Var] in +/-- Allow grind to recognise the notation of α-equivalence. -/ +@[grind ←] +theorem AlphaEquiv_def (m n : Term Var) : AlphaEquiv m n ↔ m =α n := by + rfl + +/-- Capture-avoiding substitution, as an inference system. -/ +inductive Subst : Term Var → Var → Term Var → Term Var → Prop where + | varHit {x r} : (var x).Subst x r r + | varMiss {x y r} : y ≠ x → (var y).Subst x r (var y) + | absShadow {x m r} : (abs x m).Subst x r (abs x m) + | absIn {x y m r m'} : y ∉ r.fv ∪ {x} → m.Subst x r m' → (abs y m).Subst x r (abs y m') + | app {m n x r m' n'} : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n') + | alpha {m m' r r' n n' x} : m =α m' → r =α r' → n =α n' → Subst m x r n → m'.Subst x r' n' + /-- Capture-avoiding substitution. `m.subst x r` replaces the free occurrences of variable `x` in `m` with `r`. -/ -def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) : - Term Var := +@[grind, simp] +def subst (m : Term Var) (x : Var) (r : Term Var) : + Term Var := match m with | var y => if y = x then r else var y | abs y m' => @@ -91,25 +119,21 @@ def Term.subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Te else if y ∉ r.fv then abs y (m'.subst x r) else - let z := HasFresh.fresh (m'.vars ∪ r.vars ∪ {x}) + let z := HasFresh.fresh (m'.vars ∪ r.vars ∪ {x, y}) abs z ((m'.rename y z).subst x r) | app m1 m2 => app (m1.subst x r) (m2.subst x r) termination_by m -decreasing_by all_goals grind [rename.eq_sizeOf, abs.sizeOf_spec, app.sizeOf_spec] +decreasing_by all_goals grind [rename_eq_sizeOf, abs.sizeOf_spec, app.sizeOf_spec] /-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/ -instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] : +instance instHasSubstitutionTerm : HasSubstitution (Term Var) Var (Term Var) where - subst := Term.subst + subst := subst --- TODO --- theorem Term.subst_comm --- [DecidableEq Var] [HasFresh Var] --- {m : Term Var} {x : Var} {n1 : Term Var} {y : Var} {n2 : Term Var} : --- (m[x := n1])[y := n2] = (m[y := n2])[x := n1] := by --- induction m --- -- case var z => --- sorry +/-- Allow grind to recognise the notation of substitution. -/ +@[grind ←] +theorem subst_def (m r : Term Var) (x : Var) : m.subst x r = m[x := r] := by + rfl /-- Contexts. -/ inductive Context (Var : Type u) : Type u where @@ -127,39 +151,13 @@ def Context.fill (c : Context Var) (m : Term Var) : Term Var := | appL c n => Term.app (c.fill m) n | appR n c => Term.app n (c.fill m) -/-- Any `Term` can be obtained by filling a `Context` with a variable. This proves that `Context` -completely captures the syntax of terms. -/ -theorem Context.complete (m : Term Var) : - ∃ (c : Context Var) (x : Var), m = (c.fill (Term.var x)) := by - induction m with - | var x => exists hole, x - | abs x n ih => - obtain ⟨c', y, ih⟩ := ih - exists Context.abs x c', y - rw [ih, fill] - | app n₁ n₂ ih₁ ih₂ => - obtain ⟨c₁, x₁, ih₁⟩ := ih₁ - exists Context.appL c₁ n₂, x₁ - rw [ih₁, fill] - -open Term - -/-- α-equivalence. -/ -inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where --- The α-axiom -| ax {m : Term Var} {x y : Var} : - y ∉ m.fv → AlphaEquiv (abs x m) (abs y (m.rename x y)) --- Equivalence relation rules -| refl : AlphaEquiv m m -| symm : AlphaEquiv m n → AlphaEquiv n m -| trans : AlphaEquiv m1 m2 → AlphaEquiv m2 m3 → AlphaEquiv m1 m3 --- Context closure -| ctx {c : Context Var} {m n : Term Var} : AlphaEquiv m n → AlphaEquiv (c.fill m) (c.fill n) - -/-- Instance for the notation `m =α n`. -/ -instance instHasAlphaEquivTerm [DecidableEq Var] : HasAlphaEquiv (Term Var) where - AlphaEquiv := Term.AlphaEquiv +/-- Variables (both free and bound) in a context. -/ +def Context.vars : Context Var → Finset Var + | hole => ∅ + | abs x c => c.vars ∪ {x} + | appL c m => c.vars ∪ m.vars + | appR m c => m.vars ∪ c.vars -end LambdaCalculus.Named +end LambdaCalculus.Named.Untyped.Term end Cslib diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean new file mode 100644 index 000000000..1b849f035 --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Properties.lean @@ -0,0 +1,685 @@ +/- +Copyright (c) 2026 Haoxuan Yin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Haoxuan Yin, Fabrizio Montesi +-/ + +module + +public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic + +/-! # Properties of λ-calculus terms and α-equivalence + +Basic properties of renaming, variable sets, and α-equivalence. + +The reflexivity, symmetry, and transitivity of `AlphaEquiv` (`∼p`, Definition 3.1) +follow from Theorem 4.4 in [Crole2012], which establishes that `∼p` coincides with +`∼r` (Definition 3.4), the latter being defined as an equivalence relation. +Here they are proved directly for `∼p` by structural/well-founded induction. + +## References + +* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012] +-/ + +public section + +namespace Cslib + +universe u + +variable {Var : Type u} [DecidableEq Var] + +namespace LambdaCalculus.Named.Untyped.Term + +/-- A variable in a term is either free or bound. -/ +theorem vars_either_fv_or_bv {m : Term Var} : + m.vars = m.fv ∪ m.bv := by + induction m <;> grind [fv, bv, vars] + +/-- Renaming an unused variable has no effect. -/ +@[simp] +theorem rename_unused {m : Term Var} {x y : Var} : + x ∉ m.vars → m.rename x y = m := by + induction m <;> grind [vars, rename] + +/-- Renaming a variable to itself has no effect. -/ +@[simp] +theorem rename_same {m : Term Var} {x : Var} : + m.rename x x = m := by + induction m <;> grind [vars, rename] + +/-- Renaming a used variable changes the set of variables. -/ +@[simp] +theorem rename_vars_used {m : Term Var} {x y : Var} : + x ∈ m.vars → (m.rename x y).vars = m.vars.erase x ∪ {y} := by + induction m with + | var z => grind [vars, rename] + | abs z m ih => + intro hx + by_cases hxm : x ∈ m.vars <;> grind [vars, rename, rename_unused] + | app m n ihm ihn => + intro hx + by_cases hxm : x ∈ m.vars + · by_cases hxn : x ∈ n.vars <;> grind [vars, rename, rename_unused] + · have hxn : x ∈ n.vars := by grind [vars] + grind [vars, rename, rename_unused] + +/-- Renaming removes the variable. -/ +theorem rename_remove {m : Term Var} {x y : Var} : + x ≠ y → x ∉ (m.rename x y).vars := by + intro hxy + by_cases hx : x ∈ m.vars <;> grind [rename_vars_used, rename_unused] + +/-- The set of variables after renaming. -/ +theorem rename_vars {m : Term Var} {x y : Var} : + (m.rename x y).vars = m.vars \ {x} ∪ (if x ∈ m.vars then {y} else ∅) := by + by_cases x ∈ m.vars <;> grind [vars, rename, rename_unused, rename_vars_used] + +/-- The set of free variables after renaming. -/ +theorem rename_fv {m : Term Var} {x y : Var} : + y ∉ m.vars → (m.rename x y).fv = m.fv \ {x} ∪ (if x ∈ m.fv then {y} else ∅) := by + induction m <;> grind [fv, vars, rename, vars_either_fv_or_bv] + +/-- Concatenation of renaming. -/ +@[simp] +theorem rename_concat {m : Term Var} {x y z : Var} : + y ∉ m.vars → (m.rename x y).rename y z = m.rename x z := by + induction m <;> grind [vars, rename] + +/-- Commutativity of renaming, simpler version. -/ +theorem rename_comm {m : Term Var} {x y z w : Var} : + x ≠ z → y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, z} → + (m.rename x y).rename z w = (m.rename z w).rename x y := by + induction m <;> grind [vars, rename] + +/-- Commutativity of renaming, more general version. -/ +theorem rename_comm2 {m : Term Var} {x y z w : Var} : + y ∉ m.vars ∪ {x, z} → w ∉ m.vars ∪ {x, y, z} → + (m.rename x y).rename (if z = x then y else z) w = (m.rename z w).rename x y := by + intro hy hw + by_cases hzx : z = x + · grind [rename_same, rename_unused, rename_concat, rename_vars] + · grind [rename_comm] + +omit [DecidableEq Var] in +@[grind norm↓← ] +lemma induction_by_sizeOf {m n : Term Var} : sizeOf m < sizeOf n ↔ WellFoundedRelation.rel m n := by + rfl + +/-- α-equivalent terms have the same size. -/ +theorem AlphaEquiv.eq_sizeOf {m n : Term Var} : m =α n → sizeOf m = sizeOf n := by + intro h + induction h with + | @var x => rfl + | @abs y x1 x2 m1 m2 hy h ih => + simpa using ih + | @app m1 n1 m2 n2 _ hm hn => + grind + +/-- α-equivalent terms have the same free variables. + +Related to [Crole2012], Proposition 2.1 part 2, which shows that `free(E)` is the +support of `[E]α`. -/ +theorem AlphaEquiv.same_fv {m n : Term Var} : m =α n → m.fv = n.fv := by + intro h + induction h with + | @var x => rfl + | @abs y x1 x2 m1 m2 hy h ih => + rw [Term.fv, Term.fv] + have h1 : m1.fv \ {x1} = (m1.rename x1 y).fv \ {y} := by + grind [rename_fv, vars_either_fv_or_bv] + have h2 : (m2.rename x2 y).fv \ {y} = m2.fv \ {x2} := by + grind [rename_fv, vars_either_fv_or_bv] + grind + | @app m1 n1 m2 n2 h1 h2 ih1 ih2 => grind [Term.fv] + +variable [HasFresh Var] + +/-- Reflexivity of α-equivalence. + +This follows from Theorem 4.4 [Crole2012] (which shows `∼p = ∼r`, and `∼r` is +reflexive by definition), but is proved here directly by well-founded induction. -/ +theorem AlphaEquiv.refl (m : Term Var) : m =α m := by + refine WellFounded.induction (C := fun m => m =α m) sizeOfWFRel.wf m ?_ + simp only; intro m ih + cases m with + | var x => apply AlphaEquiv.var + | abs x m => + obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x}) + apply AlphaEquiv.abs (y := z) + · grind [rename_vars] + apply ih + grind [rename_eq_sizeOf] + | app m n => + apply AlphaEquiv.app <;> apply ih <;> grind + +omit [HasFresh Var] in +/-- Symmetry of α-equivalence. + +This follows from Theorem 4.4 [Crole2012] (which shows `∼p = ∼r`, and `∼r` +includes an explicit symmetry rule), but is proved here directly. -/ +theorem AlphaEquiv.symm {m n : Term Var} : m =α n → n =α m := by + intro h + induction h with + | @var x => apply AlphaEquiv.var + | @abs y x1 x2 m1 m2 hy h ih => + apply AlphaEquiv.abs (y := y) <;> grind [rename_unused, rename_vars, rename_concat] + | @app m1 n1 m2 n2 hwm1 hwn1 hwm2 hwn2 => + apply AlphaEquiv.app <;> assumption + +/-- Renaming α-equivalent terms produces α-equivalent terms. -/ +theorem AlphaEquiv.rename_preserve (m n : Term Var) (x y : Var) : + y ∉ m.vars ∪ n.vars → m =α n → (m.rename x y) =α (n.rename x y) := by + refine (WellFounded.induction sizeOfWFRel.wf m + (C := fun m => ∀ (n : Term Var) (x y : Var), y ∉ m.vars ∪ n.vars → + m =α n → (m.rename x y) =α (n.rename x y)) ?_) n x y + intro m ih n x y hy h + by_cases hyx : y = x + · grind [rename_same] + cases h with + | @var z => apply AlphaEquiv.refl + | @abs z x1 x2 m1 m2 hz hbody => + obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m1.vars ∪ m2.vars ∪ {x1, x2, x, y, z}) + apply AlphaEquiv.abs (y := w) + · grind [rename_vars] + rw [rename_comm2, rename_comm2] + case neg.abs.a => + apply ih + · grind [rename_eq_sizeOf] + · grind [vars, rename_vars] + · have hxzw : ((m1.rename x1 z).rename z w) =α ((m2.rename x2 z).rename z w) := by + apply ih <;> grind [vars, rename_vars, rename_eq_sizeOf] + grind [rename_concat] + all_goals grind [vars] + | @app m1 n1 m2 n2 hm hn => + apply AlphaEquiv.app <;> apply ih <;> grind [vars] + +/-- Elimination rule for α-equivalence of abstractions. + It states that if two abstractions are α-equivalent, + then their bodies can be renamed to ``any'' fresh variable y and remain α-equivalent. + This is sometimes easier to use than using by_cases on the equivalence, + which can only produce the claim for ``some'' fresh y. -/ +theorem AlphaEquiv.abs_elim {m1 m2 : Term Var} {x1 x2 y : Var} : + y ∉ m1.vars ∪ m2.vars ∪ {x1, x2} → (Term.abs x1 m1) =α (Term.abs x2 m2) → + (m1.rename x1 y) =α (m2.rename x2 y) := by + intro hy h + cases h with + | @abs z _ _ _ _ hz h1 => + by_cases hzy : z = y + · grind + · have hxzy : ((m1.rename x1 z).rename z y) =α ((m2.rename x2 z).rename z y) := by + apply AlphaEquiv.rename_preserve <;> grind [AlphaEquiv.rename_preserve, rename_vars] + grind [rename_concat, rename_vars] + +/-- Transitivity of α-equivalence. + +This follows from Theorem 4.4 [Crole2012] (which shows `∼p = ∼r`, and `∼r` +includes an explicit transitivity rule), but is proved here directly +by well-founded induction. -/ +theorem AlphaEquiv.trans {m n p : Term Var} : + m =α n → n =α p → m =α p := by + refine (WellFounded.induction sizeOfWFRel.wf m + (C := fun m => ∀ (n p : Term Var), + m =α n → n =α p → m =α p) ?_) n p + intro m ih n p hmn hnp + cases m with + | var x => + cases hmn with + | @var x => assumption + | abs x1 m1 => + obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m1.vars ∪ {x1} ∪ n.vars ∪ p.vars) + have hmn' := hmn + cases hmn' with + | @abs y x1 x2 m1 m2 hy h1 => + have hnp' := hnp + cases hnp' with + | @abs z x2 x3 m2 m3 hz h2 => + apply AlphaEquiv.abs (y := w) + · grind [vars, rename_unused, rename_vars, rename_concat] + apply ih _ ?_ (m2.rename x2 w) <;> + grind [AlphaEquiv.abs_elim, vars, rename_vars, rename_eq_sizeOf] + | app m1 m2 => + cases hmn with + | @app m1 n1 m2 n2 hmn1 hmn2 => + cases hnp with + | @app n1 p1 n2 p2 hnp1 hnp2 => + apply AlphaEquiv.app + · apply ih _ ?_ n1 <;> grind [vars, rename_vars] + · apply ih _ ?_ n2 <;> grind [vars, rename_vars] + +/-- Renaming a non-free variable results in an α-equivalent term -/ +theorem AlphaEquiv.rename_non_fv {m : Term Var} {x y : Var} : + x ∉ m.fv → y ∉ m.vars → m =α (m.rename x y) := by + intro hx hy + induction m with + | var z => + have hzx : z ≠ x := by + grind [fv] + simpa [rename, hzx] using AlphaEquiv.var + | abs z m ih => + by_cases hzx : z = x + · subst z + simp only [rename, ↓reduceIte] + obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y}) + apply AlphaEquiv.abs (y := w) + · grind [rename_unused, rename_vars] + rw [rename_concat] <;> grind [vars, AlphaEquiv.refl] + · simp only [rename, hzx, ↓reduceIte] + obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y, z}) + apply AlphaEquiv.abs (y := w) + · grind [rename_unused, rename_vars] + apply AlphaEquiv.rename_preserve <;> grind [vars, rename_vars, fv] + | app m1 m2 ih1 ih2 => + apply AlphaEquiv.app + · apply ih1 <;> grind [vars, fv] + · apply ih2 <;> grind [vars, fv] + +/-- Abstracting over an arbitrary non-free variable results in the same term, + modulo α-equivalence. -/ +theorem AlphaEquiv.abs_non_fv {m1 m2 : Term Var} {x1 x2 : Var} : + m1 =α m2 → x1 ∉ m1.fv → x2 ∉ m2.fv → (Term.abs x1 m1) =α (Term.abs x2 m2) := by + intro hm hx1 hx2 + obtain ⟨y, hy⟩ := HasFresh.fresh_exists (m1.vars ∪ m2.vars ∪ {x1, x2}) + apply AlphaEquiv.abs (y := y) + · grind + apply AlphaEquiv.trans (n := m1) + · grind [rename_non_fv, AlphaEquiv.symm] + apply AlphaEquiv.trans (n := m2) <;> grind [rename_non_fv] + +/-- Renaming an abstraction leads to an α-equivalent term. -/ +theorem AlphaEquiv.abs_rename {m : Term Var} {x y : Var} : + y ∉ m.vars ∪ {x} → (Term.abs x m) =α (Term.abs y (m.rename x y)) := by + intro hy + obtain ⟨z, hz⟩ := HasFresh.fresh_exists (m.vars ∪ {x, y}) + apply AlphaEquiv.abs (y := z) <;> grind [vars, rename_vars, rename_concat, AlphaEquiv.refl] + +omit [DecidableEq Var] [HasFresh Var] in +/-- Any `Term` can be obtained by filling a `Context` with a variable. This proves that `Context` +completely captures the syntax of terms. -/ +theorem Context.complete (m : Term Var) : + ∃ (c : Context Var) (x : Var), m = (c.fill (var x)) := by + induction m with + | var x => exists hole, x + | abs x n ih => + obtain ⟨c', y, ih⟩ := ih + exists Context.abs x c', y + rw [ih, fill] + | app n₁ n₂ ih₁ ih₂ => + obtain ⟨c₁, x₁, ih₁⟩ := ih₁ + exists Context.appL c₁ n₂, x₁ + rw [ih₁, fill] + +omit [HasFresh Var] in +/-- The set of variables after filling a context. -/ +theorem Context.fill_vars {c : Context Var} {m : Term Var} : + (c.fill m).vars = c.vars ∪ m.vars := by + induction c <;> grind [Context.fill, Context.vars, Term.vars] + +/-- α-equivalence is preserved under context filling. -/ +theorem AlphaEquiv.context {m n : Term Var} {c : Context Var} : + m =α n → (c.fill m) =α (c.fill n) := by + intro h + induction c with + | hole => assumption + | abs x c ih => + simp only [Context.fill] + obtain ⟨y, hy⟩ := HasFresh.fresh_exists (m.vars ∪ n.vars ∪ c.vars ∪ {x}) + apply AlphaEquiv.abs (y := y) <;> grind [Context.fill_vars, rename_preserve] + | appL c m ih => + apply AlphaEquiv.app <;> grind [AlphaEquiv.app, AlphaEquiv.refl, vars] + | appR m c ih => + apply AlphaEquiv.app <;> grind [AlphaEquiv.app, AlphaEquiv.refl, vars] + +/-- The functional definition of substitution satisfies the relational definition of substitution. +-/ +theorem Subst.function_to_relation {m r : Term Var} {x : Var} : + m.Subst x r (m[x := r]) := by + refine WellFounded.induction (C := fun m => m.Subst x r (m[x := r])) sizeOfWFRel.wf m ?_ + simp only; intro m ih + cases m with + | var y => + by_cases hyx : y = x + · subst y + simp only [← subst_def, subst.eq_1, ↓reduceIte] + apply Subst.varHit + · simp [hyx, ← subst_def] + grind [Subst.varMiss] + | abs y m => + by_cases hyx : y = x + · subst y + simp only [← subst_def, subst.eq_2, ↓reduceIte] + apply Subst.absShadow + · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, Finset.union_insert] + by_cases hyr : y ∈ r.fv + · simp only [hyr] + have hz := fresh_notMem (insert x (insert y (m.vars ∪ r.vars))) + set z := fresh (insert x (insert y (m.vars ∪ r.vars))) + apply Subst.alpha (m := abs z (m.rename y z)) (r := r) (n := abs z ((m.rename y z)[x := r])) + · have h1 : abs z (m.rename y z) = (abs y m).rename y z := by + simp [rename] + grind [AlphaEquiv.symm, AlphaEquiv.rename_non_fv, vars, fv] + · grind [AlphaEquiv.refl] + · grind [AlphaEquiv.refl] + · apply Subst.absIn + · grind [vars, fv, vars_either_fv_or_bv] + apply ih + grind [rename_eq_sizeOf] + · simp only [hyr] + apply Subst.absIn + · grind [vars, fv, vars_either_fv_or_bv] + apply ih + grind + | app m1 m2 => + simp only [← subst_def, subst.eq_3] + apply Subst.app <;> apply ih <;> grind + +/-- Substituting a non-free variable has no effect. -/ +theorem subst.non_free {m r : Term Var} {x : Var} : + x ∉ m.fv → (m[x := r]) =α m := by + refine WellFounded.induction (C := fun m => x ∉ m.fv → (m[x := r]) =α m) sizeOfWFRel.wf m ?_ + simp only; intro m ih hx + cases m with + | var y => + have hyx : y ≠ x := by + grind [fv] + simp only [← subst_def, subst.eq_1, hyx, ↓reduceIte] + apply AlphaEquiv.var + | abs y m => + by_cases hyx : y = x + · subst y + simp only [← subst_def, subst.eq_2, ↓reduceIte] + apply AlphaEquiv.refl + · by_cases hyr : y ∈ r.fv + · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_true_eq_false, + Finset.union_insert, Finset.union_singleton] + have hz := fresh_notMem (insert x (insert y (m.vars ∪ r.vars))) + set z := fresh (insert x (insert y (m.vars ∪ r.vars))) + obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ r.vars ∪ ((m.rename y z).subst x r).vars + ∪ {x, y, z}) + apply AlphaEquiv.abs (y := w) + · grind [vars, rename_unused, rename_vars] + apply AlphaEquiv.trans (n := ((m.rename y z).rename z w)) + · apply AlphaEquiv.rename_preserve + · grind [vars, rename_vars, fv] + apply ih <;> grind [fv, rename_fv, rename_eq_sizeOf] + · grind [rename_concat, AlphaEquiv.refl] + · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true] + apply AlphaEquiv.context (c := Context.abs y Context.hole) + apply ih <;> grind [fv] + | app m1 m2 => + simp only [← subst_def, subst.eq_3] + apply AlphaEquiv.app <;> apply ih <;> grind [fv] + +lemma subst.abs_fresh_helper {m r : Term Var} {x y z : Var} : + z ∉ m.vars ∪ r.vars ∪ {x, y} → + ((Term.abs y m)[x := r]) =α (Term.abs z ((m.rename y z)[x := r])) + ∧ (y ∉ r.fv ∪ {x} → (Term.abs y (m[x := r])) =α (Term.abs z ((m.rename y z)[x := r]))) := by + refine (WellFounded.induction sizeOfWFRel.wf m + (C := fun m => ∀ (r : Term Var) (x y z : Var), + z ∉ m.vars ∪ r.vars ∪ {x, y} → + ((Term.abs y m)[x := r]) =α (Term.abs z ((m.rename y z)[x := r])) + ∧ (y ∉ r.fv ∪ {x} → (Term.abs y (m[x := r])) =α (Term.abs z ((m.rename y z)[x := r])))) ?_) + r x y z + intro m ih r x y z hz + have hright : ∀ (m' : Term Var) (y' : Var), sizeOf m' = sizeOf m → z ∉ m'.vars ∪ r.vars ∪ {x, y'} + → y' ∉ r.fv ∪ {x} → (Term.abs y' (m'[x:=r])) =α (Term.abs z ((m'.rename y' z)[x:=r])) := by + intro m' y' hm' hz hy' + cases m' with + | var w => + by_cases hwx : w = x + · subst w + have hxy' : x ≠ y' := by grind + rw [rename] + simp only [← subst_def, subst.eq_1, ↓reduceIte, hxy'] + apply AlphaEquiv.abs_non_fv <;> grind [vars_either_fv_or_bv, AlphaEquiv.refl] + · simp only [← subst_def, subst.eq_1, hwx, ↓reduceIte] + rw [rename] + by_cases hwy' : w = y' + · subst w + have hzx : z ≠ x := by grind + simp only [↓reduceIte, subst.eq_1, hzx] + obtain ⟨v, hv⟩ := HasFresh.fresh_exists ({y', z}) + apply AlphaEquiv.abs (y := v) <;> grind [vars, rename, AlphaEquiv.var] + · simp only [hwy', ↓reduceIte, subst.eq_1, hwx] + apply AlphaEquiv.abs_non_fv <;> grind [vars_either_fv_or_bv, AlphaEquiv.refl, Term.fv] + | app m1 m2 => + obtain ⟨w, hw⟩ := HasFresh.fresh_exists + ((m1.app m2)[x := r].vars ∪ (((m1.app m2).rename y' z)[x := r]).vars + ∪ m1[x := r].vars ∪ m2[x := r].vars ∪ (m1.rename y' z)[x := r].vars + ∪ (m2.rename y' z)[x := r].vars ∪ {y', z}) + apply AlphaEquiv.abs (y := w) + · grind + simp only [← subst_def, subst.eq_3, rename] + apply AlphaEquiv.app <;> apply AlphaEquiv.abs_elim <;> grind [vars, rename_vars] + | abs w m1 => + by_cases hwy' : w = y' + · subst w + rw [rename] + have hy'x : y' ≠ x := by grind + have hy'r : y' ∉ r.fv := by grind + have hzx : z ≠ x := by grind + have hzr : z ∉ r.fv := by grind [vars_either_fv_or_bv] + simp only [← subst_def, subst.eq_2, hy'x, ↓reduceIte, hy'r, not_false_eq_true, hzx, hzr] + apply AlphaEquiv.abs_non_fv + · apply (ih _ _ _ _ _ _ _).right <;> grind [vars] + · grind [fv] + · grind [fv] + · rw [rename] + simp only [hwy', ↓reduceIte] + by_cases hwx : w = x + · subst w + simp only [← subst_def, subst, ↓reduceIte] + apply AlphaEquiv.trans (n := Term.abs z ((Term.abs x m1).rename y' z)) + · grind [AlphaEquiv.abs_rename] + · grind [rename, AlphaEquiv.refl] + · by_cases hwr : w ∈ r.fv + · obtain ⟨v, hv⟩ := HasFresh.fresh_exists (m1.vars ∪ r.vars ∪ {x, y', z, w}) + have hl : (Term.abs y' (((Term.abs w m1)[x := r]))) =α + (Term.abs y' (Term.abs v ((m1.rename w v)[x := r]))) := by + apply AlphaEquiv.context (c := Context.abs y' Context.hole) + apply (ih _ _ _ _ _ _ _).left <;> grind + have hr : (Term.abs z (Term.abs v (((m1.rename y' z).rename w v)[x := r]))) + =α (Term.abs z ((Term.abs w (m1.rename y' z))[x := r])) := by + apply AlphaEquiv.context (c := Context.abs z Context.hole) + apply AlphaEquiv.symm + apply (ih _ _ _ _ _ _ _).left <;> grind [rename_vars, rename_eq_sizeOf] + have hmid : (Term.abs y' (Term.abs v ((m1.rename w v)[x := r]))) =α + (Term.abs z (Term.abs v (((m1.rename y' z).rename w v)[x := r]))) := by + obtain ⟨u, hu⟩ := HasFresh.fresh_exists + ((Term.abs v ((m1.rename w v)[x := r])).vars ∪ + (Term.abs v (((m1.rename y' z).rename w v)[x := r])).vars ∪ + ((m1.rename w v).rename y' z)[x:=r].vars ∪ {y', z}) + apply AlphaEquiv.abs (y := u) + · grind + · have hvy' : v ≠ y' := by grind + have hvz : v ≠ z := by grind + simp only [rename, hvy', hvz, ↓reduceIte] + apply AlphaEquiv.context (c := Context.abs v Context.hole) + apply AlphaEquiv.trans (n := (((m1.rename w v).rename y' z)[x := r]).rename z u) + · apply AlphaEquiv.abs_elim + · grind [vars] + · apply (ih _ _ _ _ _ _ _).right <;> grind [vars, rename_vars, rename_eq_sizeOf] + · apply AlphaEquiv.rename_preserve + · grind [vars] + · rw [rename_comm] <;> grind [vars, AlphaEquiv.refl] + exact AlphaEquiv.trans hl <| AlphaEquiv.trans hmid hr + · obtain ⟨v, hv⟩ := HasFresh.fresh_exists + (m1[x:=r].vars ∪ (m1.rename y' z)[x:=r].vars ∪ ((Term.abs w m1)[x := r]).vars ∪ + ((Term.abs w (m1.rename y' z))[x := r]).vars ∪ {y', z}) + apply AlphaEquiv.abs (y := v) + · grind [vars, rename_vars] + · have hwz : w ≠ z := by grind [vars] + simp only [← subst_def, subst, hwx, ↓reduceIte, hwr, not_false_eq_true, rename, hwy', + hwz] + apply AlphaEquiv.context (c := Context.abs w Context.hole) + apply AlphaEquiv.abs_elim <;> grind [vars] + have hleft : ((Term.abs y m)[x:=r]) =α (Term.abs z ((m.rename y z)[x:=r])) := by + by_cases hyx : y = x + · subst y + simp only [← subst_def, subst.eq_2, ↓reduceIte] + obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ r.vars ∪ ((m.rename x z).subst x r).vars ∪ + {x, z}) + apply AlphaEquiv.abs (y := w) + · grind [vars, rename_unused, rename_vars] + · apply AlphaEquiv.trans (n := ((m.rename x z).rename z w)) + · grind [AlphaEquiv.refl, rename_concat] + · apply AlphaEquiv.rename_preserve + · grind [rename_vars] + · apply AlphaEquiv.symm + apply subst.non_free + grind [fv, rename_fv, rename_eq_sizeOf] + · by_cases hyr : y ∈ r.fv + · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_true_eq_false, + Finset.union_insert, Finset.union_singleton] + have hw := fresh_notMem (insert x (insert y (m.vars ∪ r.vars))) + set w := fresh (insert x (insert y (m.vars ∪ r.vars))) + by_cases hzw' : z = w + · subst z + apply AlphaEquiv.refl + · apply AlphaEquiv.trans (n := (Term.abs z (((m.rename y w).rename w z)[x := r]))) + · apply hright <;> + grind [rename_eq_sizeOf, vars_either_fv_or_bv, rename_vars] + · rw [rename_concat] <;> grind [AlphaEquiv.refl] + · simp only [← subst_def, subst.eq_2, hyx, ↓reduceIte, hyr, not_false_eq_true] + apply hright <;> grind + exact ⟨hleft, hright m y (by rfl) (by grind)⟩ + +/-- Modulo α-equivalence, substituting an abstraction falls back to the fresh variable case only. + With this lemma, the three cases in the definition of subst can be reduced to one. +-/ +theorem subst.abs_fresh {m r : Term Var} {x y z : Var} : + z ∉ m.vars ∪ r.vars ∪ {x, y} → + ((Term.abs y m)[x := r]) =α (Term.abs z ((m.rename y z)[x := r])) := by + grind [subst.abs_fresh_helper] + +/-- Substituting α-equivalent terms produces α-equivalent terms. -/ +theorem subst.preserve_AlphaEquiv {m m' r r' : Term Var} {x : Var} : + m =α m' → r =α r' → (m[x := r]) =α (m'[x := r']) := by + refine (WellFounded.induction sizeOfWFRel.wf m + (C := fun m => ∀ (m' r r' : Term Var) (x : Var), + m =α m' → r =α r' → (m[x := r]) =α (m'[x := r'])) ?_) m' r r' x + intro m ih m' r r' x hmm' hrr' + have hmm'' := hmm' + cases hmm'' with + | @var y => + by_cases hyx : y = x + · simp only [← subst_def, subst, ↓reduceIte, hyx] + assumption + · simp only [← subst_def, subst, hyx] + apply AlphaEquiv.refl + | @abs z y y' m m' hz h1 => + obtain ⟨w, hw⟩ := HasFresh.fresh_exists (m.vars ∪ m'.vars ∪ r.vars ∪ r'.vars ∪ {x, y, y'}) + have h2 : ((Term.abs y m)[x := r]) =α (Term.abs w ((m.rename y w)[x := r])) := by + grind [subst.abs_fresh] + have h2' : ((Term.abs y' m')[x := r']) =α + (Term.abs w ((m'.rename y' w)[x := r'])) := by + grind [subst.abs_fresh] + have hbody : (m.rename y w) =α (m'.rename y' w) := by + apply AlphaEquiv.abs_elim <;> grind + have h3 : + (Term.abs w ((m.rename y w)[x := r])) =α (Term.abs w ((m'.rename y' w)[x := r'])) := by + apply AlphaEquiv.context (c := Context.abs w Context.hole) + apply ih <;> grind [rename_eq_sizeOf] + apply AlphaEquiv.trans (n := (Term.abs w ((m.rename y w)[x := r]))) <;> try assumption + apply AlphaEquiv.trans (n := (Term.abs w ((m'.rename y' w)[x := r']))) <;> try assumption + apply AlphaEquiv.symm + assumption + | @app m m' n n' hm hn => + simp only [← subst_def, subst] + apply AlphaEquiv.app <;> apply ih <;> grind + +/-- The relational definition of substitution coincides with the functional definition of + substitution, modulo α-equivalence. -/ +theorem Subst.relation_iff_function {m n r : Term Var} {x : Var} : + m.Subst x r n ↔ n =α (m[x := r]) := by + constructor + · intro h + induction h with + | @varHit x r => + simp only [← subst_def, subst, ↓reduceIte] + apply AlphaEquiv.refl + | @varMiss x y r hyx => + simp only [← subst_def, subst, hyx, ↓reduceIte] + apply AlphaEquiv.refl + | @absShadow x m r => + simp only [← subst_def, subst, ↓reduceIte] + apply AlphaEquiv.refl + | @absIn x y m r m' hy h ih => + have hyx : y ≠ x := by grind + have hyr : y ∉ r.fv := by grind + simp only [← subst_def, subst, hyx, ↓reduceIte, hyr, not_false_eq_true] + apply AlphaEquiv.context (c := Context.abs y Context.hole) + assumption + | @app m n x r m' n' h1 h2 ih1 ih2 => + simp only [← subst_def, subst] + apply AlphaEquiv.app <;> assumption + | @alpha m m' r r' n n' x hm hr hn h ih => + apply AlphaEquiv.trans (n := n) + · grind [AlphaEquiv.symm] + apply AlphaEquiv.trans (n := m[x := r]) <;> grind [subst.preserve_AlphaEquiv] + · intro h + apply Subst.alpha (m := m) (r := r) (n := m[x := r]) <;> grind [AlphaEquiv.symm, + AlphaEquiv.refl, Subst.function_to_relation] + +/-- Commutativity of substitution (a.k.a. the substitution lemma) -/ +theorem subst.commutativity {m r1 r2 : Term Var} {x y : Var} : + x ∉ r2.fv ∪ {y} → ((m[x := r1])[y := r2]) =α ((m[y := r2])[x := (r1[y := r2])]) := by + refine WellFounded.induction sizeOfWFRel.wf m + (C := fun m => ∀ (r1 r2 : Term Var) (x y : Var), + x ∉ r2.fv ∪ {y} → + ((m[x := r1])[y := r2]) =α ((m[y := r2])[x := (r1[y := r2])])) ?_ r1 r2 x y + intro m ih r1 r2 x y hxy + cases m with + | var z => + by_cases hzx : z = x + · subst z + have hxy' : x ≠ y := by grind + simp only [← subst_def, subst.eq_1, ↓reduceIte, hxy'] + apply AlphaEquiv.refl + · by_cases hzy : z = y + · subst z + simp only [← subst_def, subst.eq_1, hzx, ↓reduceIte] + apply AlphaEquiv.symm + apply subst.non_free + grind + · simp only [← subst_def, subst.eq_1, hzx, hzy, ↓reduceIte] + apply AlphaEquiv.refl + | abs z m => + obtain ⟨w, hw⟩ := HasFresh.fresh_exists + (m.vars ∪ r1.vars ∪ r2.vars ∪ (r1[y := r2]).vars ∪ {x, y, z}) + have hl : (((Term.abs z m)[x := r1])[y := r2]) =α + (Term.abs w (((m.rename z w)[x := r1])[y := r2])) := by + apply AlphaEquiv.trans (n := (((Term.abs w ((m.rename z w)[x := r1]))[y := r2]))) + · apply subst.preserve_AlphaEquiv + · apply subst.abs_fresh + grind + · apply AlphaEquiv.refl + · have hwy : w ≠ y := by grind + have hwr2 : w ∉ r2.fv := by grind [vars_either_fv_or_bv] + simp only [← subst_def, subst.eq_2, hwy, ↓reduceIte, hwr2, not_false_eq_true] + apply AlphaEquiv.refl + have hr : (Term.abs w (((m.rename z w)[y := r2])[x := (r1[y := r2])])) + =α (((Term.abs z m)[y := r2])[x := (r1[y := r2])]) := by + apply AlphaEquiv.symm + apply AlphaEquiv.trans (n := ((Term.abs w ((m.rename z w)[y := r2]))[x := (r1[y := r2])])) + · apply subst.preserve_AlphaEquiv + · apply subst.abs_fresh + grind + · apply AlphaEquiv.refl + · have hwx : w ≠ x := by grind + have hwr : w ∉ (r1.subst y r2).fv := by grind [vars_either_fv_or_bv] + simp only [← subst_def, subst.eq_2, hwx, ↓reduceIte, hwr, not_false_eq_true] + apply AlphaEquiv.refl + have hmid : (Term.abs w (((m.rename z w)[x := r1])[y := r2])) =α + (Term.abs w (((m.rename z w)[y := r2])[x := (r1[y := r2])])) := by + apply AlphaEquiv.context (c := Context.abs w Context.hole) + apply ih <;> grind [rename_eq_sizeOf] + exact AlphaEquiv.trans hl <| AlphaEquiv.trans hmid hr + | app m1 m2 => + simp only [← subst_def, subst.eq_3] + apply AlphaEquiv.app <;> apply ih <;> grind + +end LambdaCalculus.Named.Untyped.Term + +end Cslib diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/SwapProperties.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/SwapProperties.lean new file mode 100644 index 000000000..565406419 --- /dev/null +++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/SwapProperties.lean @@ -0,0 +1,506 @@ +/- +Copyright (c) 2026 Chris Anto Fröschl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Anto Fröschl +-/ + +module + +public import Cslib.Languages.LambdaCalculus.Named.Untyped.AlphaEquivDefs +public import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties + +/-! # Properties of the swap (transposition) operation on lambda terms + +Helper lemmas for reasoning about `Term.swap` and its interaction with +`AlphaEquiv`, `rename`, `vars`, and `fv`. + +The notion of *atom swapping* (transposition) as the basis for defining α-equivalence +originates from [Gabbay and Pitts, *A New Approach to Abstract Syntax with Variable +Binding*][Gabbay2002] (Section 2, page 3). The key observation is that α-equivalence can +be defined using the notion of atom swapping in lieu of the traditional +renaming/substitution approach. + +The swap (transposition) operation `m.swap x y` implements the permutation action +`(x y) · E` from [Crole2012] (Section 2). It simultaneously replaces all occurrences +of `x` with `y` and vice versa throughout a term. + +## References + +* [Roy L. Crole, *Alpha equivalence equalities*][Crole2012], Sections 2 and 6 +* [M. Gabbay and A. Pitts, *A New Approach to Abstract Syntax with Variable + Binding*][Gabbay2002], Section 2 +-/ + +@[expose] public section + +namespace Cslib + +universe u + +variable {Var : Type u} [DecidableEq Var] + +namespace LambdaCalculus.Named.Untyped.Term + +def agreementSet (f g : Var → Var) : Set Var := { x | f x = g x } +def disagreementSet (f g : Var → Var) : Set Var := { x | f x ≠ g x } + +@[simp] +lemma swap_self {m : Term Var} {x : Var} : m.swap x x = m := by + induction m <;> simp_all [swap, permute] + +lemma swap_comm {m : Term Var} {x y : Var} : m.swap x y = m.swap y x := by + unfold swap + rw [Equiv.swap_comm] + +@[simp] +lemma swap_involutive {m : Term Var} {x y : Var} : (m.swap x y).swap x y = m := by + induction m <;> simp_all [swap, permute] + +@[simp] +lemma swap_preserves_sizeOf {m : Term Var} {x y : Var} : sizeOf (m.swap x y) = sizeOf m := by + induction m <;> simp_all [swap, permute] + +@[simp] +lemma swap_unused {m : Term Var} {x y : Var} : x ∉ m.vars → y ∉ m.vars → m.swap x y = m := by + induction m <;> grind [swap, permute, vars] + +/-- When `y ∉ m.vars`, `swap x y` and `rename x y` coincide. + +This is because `rename x y` only changes `x` to `y` (not `y` to `x`), and when `y` does +not occur in `m`, swapping and renaming produce the same result. -/ +lemma swap_eq_rename_of_not_mem_vars {m : Term Var} {x y : Var} + (hy : y ∉ m.vars) : m.swap x y = m.rename x y := by + induction m with + | var z => + unfold swap rename + grind [Term.vars, permute] + | abs z m ih => + simp_all [Term.swap, Term.rename, Term.vars, permute] + grind + | app n1 n2 ih1 ih2 => + simp_all [Term.swap, Term.rename, Term.vars, permute] + +/-- The set of free variables after a swap. -/ +lemma swap_fv {m : Term Var} {x y : Var} : + (m.swap x y).fv = m.fv.image fun z => if z = x then y else if z = y then x else z := by + induction m with + | var z => aesop + | abs z m ih => + simp_all [Term.swap, Term.fv, Finset.ext_iff, Finset.mem_image, Finset.mem_sdiff, permute] + grind + | app m n ih1 ih2 => + simp_all only [Term.swap, Term.fv, permute] + rw [Finset.image_union] + +/-- Swapping preserves non-membership in `fv`. -/ +lemma fresh_swap {m : Term Var} {x y z : Var} (hzx : z ≠ x) (hzy : z ≠ y) (hzm : z ∉ m.fv) : + z ∉ (m.swap x y).fv := by + rw [swap_fv] + grind + +/-- The set of vars after a swap. -/ +lemma swap_vars {m : Term Var} {x y z : Var} (hzm : z ∉ m.vars) : + (m.swap x y).vars = m.vars.image fun z => if z = x then y else if z = y then x else z := by + induction m with + | var w => aesop + | abs w m ih => simp_all [Term.swap, Term.vars, permute]; grind + | app m n ih1 ih2 => + simp_all only [Term.swap, Term.vars, Finset.image_union, permute] + grind + +/-- Swapping preserves non-membership in `vars`. -/ +lemma not_mem_vars_swap {m : Term Var} {x y z : Var} + (hzx : z ≠ x) (hzy : z ≠ y) (hzm : z ∉ m.vars) : z ∉ (m.swap x y).vars := by + rw [swap_vars hzm] + grind + +/-- `swap` and `rename` commute (modulo the permutation action on the variable arguments). -/ +lemma swap_rename_comm {m : Term Var} {u v x y : Var} : + (m.swap u v).rename (Equiv.swap u v x) (Equiv.swap u v y) = (m.rename x y).swap u v := by + induction m with + | var z => + simp_all [Term.swap, Term.rename, permute] + grind + | abs z m ih => + simp_all [Term.swap, Term.rename, permute] + grind + | app m n ih1 ih2 => + simp_all [Term.swap, Term.rename, permute] + +lemma swap_rename_comm' {m : Term Var} {u v x z : Var} (hzu : z ≠ u) (hzv : z ≠ v) : + (m.swap u v).rename (Equiv.swap u v x) z = (m.rename x z).swap u v := by + rw [← @swap_rename_comm _ _ m u v x z] + simp_all + grind + +lemma swap_comp_eq_of_not_mem_vars {m : Term Var} {a u z : Var} + (hu : u ∉ m.vars) (hz : z ∉ m.vars) : + (m.swap u a).swap z u = m.swap z a := by + induction m + · simp_all [Term.swap, Term.vars, permute] + grind + · simp_all [Term.swap, Term.vars, permute] + grind + · simp_all [Term.swap, Term.vars, permute] + +/-- Term-level conjugation identity: `(m.swap u v).swap v a = (m.swap u a).swap u v` +when `a ∉ {u, v}`. + +Unlike `swap_comp_eq_of_not_mem_vars`, this holds unconditionally (no freshness needed). -/ +lemma swap_comp_eq_of_ne {m : Term Var} {a u v : Var} (hau : a ≠ u) (hav : a ≠ v) : + (m.swap u v).swap v a = (m.swap u a).swap u v := by + induction m with + | var x => simp_all [Term.swap, permute]; grind + | app m n ihm ihn => simp_all [Term.swap, permute] + | abs x m ih => simp_all [Term.swap, permute]; grind + +/-- If `u` is not among `m`'s variables, then `v` cannot appear in `m.swap u v` +(the only way `v` could show up is as the image of `u`). -/ +lemma not_mem_swap_target {m : Term Var} {u v : Var} (hu : u ∉ m.vars) : v ∉ (m.swap u v).vars := by + rw [swap_vars hu] + grind + +/-- Permuting a term transports its free variables pointwise. -/ +lemma permute_fv (m : Term Var) (π : Equiv.Perm Var) : + (m.permute π).fv = m.fv.image π := by + induction m with + | var x => simp [permute, fv] + | app m n ihm ihn => simp [permute, fv, ihm, ihn, Finset.image_union] + | abs x m ih => + simp only [permute, fv, ih] + rw [Finset.image_sdiff _ _ π.injective] + simp + +omit [DecidableEq Var] in +/-- Permuting successively by `π` and `π'` is permutation by their composition. -/ +lemma permute_trans (m : Term Var) (π π' : Equiv.Perm Var) : + (m.permute π).permute π' = m.permute (π.trans π') := by + induction m <;> simp_all [permute] + +/-- A transposition acts on terms in the same way as `Term.swap`. -/ +lemma permute_swap (m : Term Var) (x y : Var) : m.permute (Equiv.swap x y) = m.swap x y := by + induction m <;> simp_all [permute, swap, Equiv.swap_apply_def] + +-- First 4 case examination of example 1 +lemma desired_condition_cases_z_ne_u_or_v {E E' : Term Var} {a b u v z : Var} + (hm1 : z ∉ E.vars ∪ E'.vars ∪ {a, b}) + (h2 : ((E.rename a z).swap u v) =α ((E'.rename b z).swap u v)) + (hzu : z ≠ u) + (hzv : z ≠ v) + : ((E.swap u v).swap (Equiv.swap u v a) z) =α ((E'.swap u v).swap (Equiv.swap u v b) z) := by + have hzb : z ≠ b := by simp_all + have hza : z ≠ a := by simp_all + have z_h1 : z ∉ (E.swap u v).vars := by exact not_mem_vars_swap hzu hzv (by simp_all) + have z_h2 : z ∉ (E'.swap u v).vars := by exact not_mem_vars_swap hzu hzv (by simp_all) + rw [swap_eq_rename_of_not_mem_vars z_h1] + rw [swap_eq_rename_of_not_mem_vars z_h2] + rw [← swap_rename_comm' (by grind) (by grind)] at h2 + rw [← swap_rename_comm' (by grind) (by grind)] at h2 + have ha : a = u ∨ a = v ∨ (a ≠ u ∧ a ≠ v) := by grind + have hb : b = u ∨ b = v ∨ (b ≠ u ∧ b ≠ v) := by grind + rcases ha with h' | h' | ⟨hau, hav⟩ + · rcases hb with h'' | h'' | ⟨hbu, hbv⟩ <;> simp_all + · rcases hb with h'' | h'' | ⟨hbu, hbv⟩ <;> simp_all + · rcases hb with h'' | h'' | ⟨hbu, hbv⟩ <;> simp_all + +-- example 1: use z as witness +lemma alphaEquiv_swap_preserve_abs_fresh {E E' : Term Var} {a b u v z : Var} + (hm : z ∉ E.vars ∪ E'.vars ∪ {a, b}) + (hbody : ((E.rename a z).swap u v) =α ((E'.rename b z).swap u v)) + (hzu : z ≠ u) (hzv : z ≠ v) : + ((Term.abs a E).swap u v) =α ((Term.abs b E').swap u v) := by + have hzE : z ∉ (E.swap u v).vars := not_mem_vars_swap hzu hzv (by simp_all) + have hzE' : z ∉ (E'.swap u v).vars := not_mem_vars_swap hzu hzv (by simp_all) + have hren := desired_condition_cases_z_ne_u_or_v hm hbody hzu hzv + rw [swap_eq_rename_of_not_mem_vars hzE, swap_eq_rename_of_not_mem_vars hzE'] at hren + simp only [Term.swap] + apply AlphaEquiv.abs (y := z) + · simp_all [Finset.mem_union, Finset.mem_insert, swap] + grind + · exact hren + +-- example 2: use v as witness +lemma alphaEquiv_swap_preserve_abs_fresh_z_eq_u {E E' : Term Var} {a b u v : Var} + (hm : u ∉ E.vars ∪ E'.vars ∪ {a, b}) + (hbody : ((E.rename a u).swap u v) =α ((E'.rename b u).swap u v)) + (hau : a ≠ u) (hav : a ≠ v) (hbu : b ≠ u) (hbv : b ≠ v) : + ((Term.abs a E).swap u v) =α ((Term.abs b E').swap u v) := by + have huE : u ∉ E.vars := by simp_all + have huE' : u ∉ E'.vars := by simp_all + rw [← swap_eq_rename_of_not_mem_vars huE, ← swap_eq_rename_of_not_mem_vars huE'] at hbody + rw [swap_comm (m := E) (x := a) (y := u), swap_comm (m := E') (x := b) (y := u)] at hbody + rw [← swap_comp_eq_of_ne hau hav, ← swap_comp_eq_of_ne hbu hbv] at hbody + rw [swap_comm (m := E.swap u v) (x := v) (y := a)] at hbody + rw [swap_comm (m := E'.swap u v) (x := v) (y := b)] at hbody + have hvE : v ∉ (E.swap u v).vars := not_mem_swap_target huE + have hvE' : v ∉ (E'.swap u v).vars := not_mem_swap_target huE' + rw [swap_eq_rename_of_not_mem_vars hvE, swap_eq_rename_of_not_mem_vars hvE'] at hbody + apply AlphaEquiv.abs (y := v) <;> (simp_all [swap]; grind) + +-- example 3 +lemma alphaEquiv_swap_preserve_abs_b_eq_u {E E' : Term Var} {a u v : Var} + (hm : v ∉ E.vars ∪ E'.vars ∪ {a}) + (hbody : ((E.rename a v).swap u v) =α ((E'.rename u v).swap u v)) + (hau : a ≠ u) (hav : a ≠ v) (huv : u ≠ v) : + ((Term.abs a E).swap u v) =α ((Term.abs u E').swap u v) := by + have hvE : v ∉ E.vars := by simp_all + have hvE' : v ∉ E'.vars := by simp_all + have huE : u ∉ (E.swap u v).vars := by rw [swap_comm]; exact not_mem_swap_target hvE + have huE' : u ∉ (E'.swap u v).vars := by rw [swap_comm]; exact not_mem_swap_target hvE' + have hL : (E.swap u v).rename a u = (E.rename a v).swap u v := by + have h := @swap_rename_comm _ _ E u v a v + simp_all + grind + have hR : (E'.swap u v).rename v u = (E'.rename u v).swap u v := by + have h := @swap_rename_comm _ _ E' u v u v + simp_all + have hbody' : ((E.swap u v).rename a u) =α ((E'.swap u v).rename v u) := by + rw [hL, hR] + exact hbody + apply AlphaEquiv.abs (y := u) + · simp_all [Finset.mem_union, Finset.mem_insert, swap] + grind + · simp_all [swap] + grind + +-- example 4 +lemma alphaEquiv_swap_preserve_abs_a_eq_b_eq_u {E E' : Term Var} {u v : Var} + (hm : v ∉ E.vars ∪ E'.vars ∪ {u}) + (ih : ((E.rename u v).swap u v) =α ((E'.rename u v).swap u v)) (huv : u ≠ v) : + ((Term.abs u E).swap u v) =α ((Term.abs u E').swap u v) := by + have hvE : v ∉ E.vars := by simp_all + have hvE' : v ∉ E'.vars := by simp_all + rw [← swap_eq_rename_of_not_mem_vars hvE, ← swap_eq_rename_of_not_mem_vars hvE'] at ih + rw [swap_involutive, swap_involutive] at ih + -- now have ih : E =α E' + have huE : u ∉ (E.swap u v).vars := by + have h := not_mem_swap_target (u := v) (v := u) hvE + rwa [swap_comm] at h + have huE' : u ∉ (E'.swap u v).vars := by + have h := not_mem_swap_target (u := v) (v := u) hvE' + rw [swap_comm] at h + exact h + apply AlphaEquiv.abs (y := u) + · simp_all [swap] + · simp only [Equiv.swap_apply_left] + change ((E.swap u v).rename v u) =α ((E'.swap u v).rename v u) + rw [← swap_eq_rename_of_not_mem_vars (m := E.swap u v) (x := v) (y := u) huE] + rw [← swap_eq_rename_of_not_mem_vars (m := E'.swap u v) (x := v) (y := u) huE'] + nth_rw 2 [swap_comm] + nth_rw 4 [swap_comm] + rw [swap_involutive, swap_involutive] + exact ih + +variable [HasFresh Var] + +lemma AlphaEquiv.abs_congr {m m' : Term Var} {x : Var} : + m =α m' → (Term.abs x m) =α (Term.abs x m') := by + intro h + obtain ⟨y, hy⟩ := HasFresh.fresh_exists (m.vars ∪ m'.vars ∪ {x}) + apply AlphaEquiv.abs (y := y) + · grind + · apply AlphaEquiv.rename_preserve <;> grind + +/-- Lemma 6.1 [Crole2012]: Swap (transposition) preserves α-equivalence. -/ +lemma AlphaEquiv.swap_preserve {m m' : Term Var} {u v : Var} : + m =α m' → (m.swap u v) =α (m'.swap u v) := by + intro h1 + by_cases h2 : u = v + · simp_all + · change u ≠ v at h2 + induction h1 with + | var => simp_all [AlphaEquiv.refl] + | abs hm1 hm2 ih => + rename_i z a b E E' + have z_h1 : z ≠ a := by simp_all + have z_h2 : z ≠ b := by simp_all + have h3 : a = u ∨ a = v ∨ (a ≠ u ∧ a ≠ v) := by grind + have h4 : b = u ∨ b = v ∨ (b ≠ u ∧ b ≠ v) := by grind + have h5 : z = u ∨ z = v ∨ (z ≠ u ∧ z ≠ v) := by grind + -- we've got 27 cases to consider + rcases h3 with ha | ha | ⟨hau, hav⟩ + · rcases h4 with hb | hb | ⟨hbu, hbv⟩ + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + · simp_all + -- representative example 4 case of: a = u; b = u; z = v + · subst ha; subst hb; subst hz + exact alphaEquiv_swap_preserve_abs_a_eq_b_eq_u (by simp_all) ih h2 + -- example 1 reuse + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + · simp_all + · simp_all + -- example 1 reuse + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + · simp_all + -- example 3 reuse + · subst ha; subst hz + apply AlphaEquiv.symm + exact (alphaEquiv_swap_preserve_abs_b_eq_u (by grind) (AlphaEquiv.symm ih) hbu hbv h2) + -- example 1 reuse + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + · rcases h4 with hb | hb | ⟨hbu, hbv⟩ + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + · simp_all + · simp_all + -- example 1 reuse + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + -- example 4 reuse + · subst ha; subst hb; subst hz + nth_rw 1 [swap_comm] + nth_rw 2 [swap_comm] + symm at z_h2 + nth_rw 1 [swap_comm] at ih + nth_rw 2 [swap_comm] at ih + apply alphaEquiv_swap_preserve_abs_a_eq_b_eq_u (by simp_all) ih z_h2 + · simp_all + -- example 1 reuse + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + -- example 3 reuse + · subst ha; subst hz + nth_rw 1 [swap_comm] + nth_rw 2 [swap_comm] + apply AlphaEquiv.symm + symm at h2 + apply alphaEquiv_swap_preserve_abs_b_eq_u (by simp_all) _ hbv hbu h2 + apply AlphaEquiv.symm + nth_rw 1 [swap_comm] + nth_rw 2 [swap_comm] + exact ih + · simp_all + -- example 1 reuse + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + · rcases h4 with hb | hb | ⟨hbu, hbv⟩ + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + · simp_all + -- representative example 3 case of: a ≠ u, v; b = u; z = v + · subst hb; subst hz + exact alphaEquiv_swap_preserve_abs_b_eq_u (by simp_all) ih hau hav h2 + -- example 1 reuse + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + -- example 3 reuse + · subst hb; subst hz + nth_rw 1 [swap_comm] + nth_rw 2 [swap_comm] + symm at h2 + apply alphaEquiv_swap_preserve_abs_b_eq_u (by simp_all) _ hav hau h2 + nth_rw 1 [swap_comm] + nth_rw 2 [swap_comm] + exact ih + · simp_all + -- example 1 reuse + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + · rcases h5 with hz | hz | ⟨hzu, hzv⟩ + -- representative example 2 case of: a ≠ u, v; b ≠ u, v; z = u + -- use z' = v + · subst hz + exact alphaEquiv_swap_preserve_abs_fresh_z_eq_u hm1 ih hau hav hbu hbv + -- example 2 reuse after adjusting via swap commutativity and choosing z' = u + · rw [swap_comm (m := Term.abs a E) (x := u) (y := v), + swap_comm (m := Term.abs b E') (x := u) (y := v)] + subst hz + nth_rw 1 [swap_comm] at ih + nth_rw 2 [swap_comm] at ih + exact alphaEquiv_swap_preserve_abs_fresh_z_eq_u hm1 ih hav hau hbv hbu + -- representative example 1 case of: z ≠ u, v + -- use z' = z + · exact alphaEquiv_swap_preserve_abs_fresh hm1 ih hzu hzv + | app hm1 hm2 ih1 ih2 => exact AlphaEquiv.app ih1 ih2 + +omit [HasFresh Var] in +/-- **Lemma 6.2 part 1** [Crole2012]. -/ +lemma permute_eq_of_vars_subset_agreementSet (m : Term Var) (π π' : Equiv.Perm Var) + (h : (m.vars : Set Var) ⊆ agreementSet π π') : + m.permute π = m.permute π' := by + induction m with + | var x => simp_all [permute, vars, agreementSet, vars] + | abs x m ih => + have hx : π x = π' x := h (by simp [vars]) + have hm : m.permute π = m.permute π' := ih fun y hy => h (by simp [vars, hy]) + simp [permute, hx, hm] + | app m n ihm ihn => + have hm : m.permute π = m.permute π' := ihm fun y hy => h (by simp [vars, hy]) + have hn : n.permute π = n.permute π' := ihn fun y hy => h (by simp [vars, hy]) + simp [permute, hm, hn] + +/-- **Lemma 6.2 part 2** [Crole2012]. -/ +lemma permute_alphaEquiv_of_fv_subset_agreementSet (m : Term Var) (π π' : Equiv.Perm Var) + (h : (m.fv : Set Var) ⊆ agreementSet π π') : + (m.permute π) =α (m.permute π') := by + induction m generalizing π π' with + | var x => + unfold permute + have hx : π x = π' x := by + unfold agreementSet at h + apply h + unfold fv + rw [Finset.coe_singleton, Set.mem_singleton_iff] + rw [hx] + exact AlphaEquiv.var + | app m n ihm ihn => + have hm : (m.permute π) =α (m.permute π') := by + apply ihm + intro x hx + apply h + unfold fv + simp_all + have hn : (n.permute π) =α (n.permute π') := by + apply ihn + intro x hx + apply h + unfold fv + simp_all + apply AlphaEquiv.app hm hn + | abs a m ih => + let z := HasFresh.fresh ((m.permute π).vars ∪ (m.permute π').vars ∪ {π a, π' a}) + have hz := HasFresh.fresh_notMem ((m.permute π).vars ∪ (m.permute π').vars ∪ {π a, π' a}) + have hzπ : z ∉ (m.permute π).vars := by simp_all [z] + have hzπ' : z ∉ (m.permute π').vars := by simp_all [z] + have hbody : + (m.permute (π.trans (Equiv.swap (π a) z))) =α (m.permute (π'.trans (Equiv.swap (π' a) z))) + := by + apply ih + intro x hx + simp only [agreementSet, Set.mem_setOf_eq, Equiv.trans_apply] + by_cases hxa : x = a + · simp_all + · have hagree : π x = π' x := h (by simp [fv, hx, hxa]) + have hπxa : π x ≠ π a := fun he => hxa (π.injective he) + have hπ'xa : π' x ≠ π' a := fun he => hxa (π'.injective he) + have hπ'xπa : π' x ≠ π a := by simp_all + have hπxz : π x ≠ z := by + intro he + apply hzπ + rw [← he, vars_either_fv_or_bv] + apply Finset.mem_union_left + rw [permute_fv] + exact Finset.mem_image.mpr ⟨x, hx, rfl⟩ + have hπ'xz : π' x ≠ z := by simp_all + simp [Equiv.swap_apply_def, hπ'xa, hπ'xπa, hπ'xz, hagree] + rw [← permute_trans, ← permute_trans, permute_swap, permute_swap] at hbody + rw [swap_eq_rename_of_not_mem_vars hzπ, swap_eq_rename_of_not_mem_vars hzπ'] at hbody + unfold permute + apply AlphaEquiv.abs (y := z) (by simp_all [z]) hbody + +/-- **Lemma 6.2 part 2** [Crole2012] (specialized). -/ +lemma swap_comp_alphaEquiv_of_not_mem_fv {m : Term Var} {a u z : Var} + (hu : u ∉ m.fv) (hz : z ∉ m.fv) : + ((m.swap u a).swap z u) =α (m.swap z a) := by + let π := (Equiv.swap u a).trans (Equiv.swap z u) + let π' := Equiv.swap z a + have h : (m.fv : Set Var) ⊆ agreementSet π π' := by + intro x hx + unfold agreementSet + rw [Set.mem_setOf_eq] + grind + have h' := permute_alphaEquiv_of_fv_subset_agreementSet m π π' h + rw [← permute_trans, permute_swap, permute_swap, permute_swap] at h' + exact h' + +end LambdaCalculus.Named.Untyped.Term + +end Cslib diff --git a/CslibTests.lean b/CslibTests.lean index 73292aef3..af319a190 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -1,14 +1,12 @@ -module -- shake: keep-all - -public import CslibTests.Bisimulation -public import CslibTests.CCS -public import CslibTests.CLL -public import CslibTests.DFA -public import CslibTests.FreeMonad -public import CslibTests.GrindLint -public import CslibTests.HML -public import CslibTests.HasFresh -public import CslibTests.ImportWithMathlib -public import CslibTests.LTS -public import CslibTests.LambdaCalculus -public import CslibTests.Reduction +import CslibTests.Bisimulation +import CslibTests.CCS +import CslibTests.CLL +import CslibTests.DFA +import CslibTests.FreeMonad +import CslibTests.GrindLint +import CslibTests.HML +import CslibTests.HasFresh +import CslibTests.ImportWithMathlib +import CslibTests.LTS +import CslibTests.LambdaCalculus +import CslibTests.Reduction diff --git a/references.bib b/references.bib index 2cccb928f..55239bb1b 100644 --- a/references.bib +++ b/references.bib @@ -277,3 +277,80 @@ @incollection{WinskelNielsen1995 url = {https://doi.org/10.1093/oso/9780198537809.003.0001}, eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf}, } + +@article{Crole2012, + title={Alpha equivalence equalities}, + journal={Theoretical Computer Science}, + volume={433}, + pages={1-19}, + year={2012}, + issn={0304-3975}, + doi={https://doi.org/10.1016/j.tcs.2012.01.030}, + url={https://www.sciencedirect.com/science/article/pii/S0304397512000667}, + author={Roy L. Crole}, + keywords={-equivalence, Atom, Context, -expression, Permutation action, Renaming, Variable binding}, + abstract={Programming languages and logics, which are pervasive in Computer Science, have syntax which involves variable binding constructors. As such, reasoning about such languages in general, and formal reasoning in particular (such as within a theorem prover), requires frameworks within which the syntax may be properly represented. One key requirement is a correct representation of α-equivalence. The current literature provides a number of different definitions of the notion of α-equivalence. The formal definitions may be nameless as in the approach of de Bruijn, or have explicit names, as in the approaches that use either a renaming/substitution axiom, or instead use a notion of variable swapping. The first contribution of this paper is to draw together five definitions of α-equivalence relations and to prove formally and in detail, but using mathematics, that the relations are all equal. There are two key reasons for doing this: Firstly, the literature has many examples of proofs of results involving α-equivalence which contain technical errors. Such examples concern both the application of α-equivalence, and the meta-theory of α-equivalence itself. Secondly, the literature does not currently contain detailed presentations of such results. The point of giving the detail is partly to avoid falling into common error-traps, but mainly to provide clear mathematical machinery that will be useful to those working in the area. This includes systems of inductive rules and proofs by induction, and clear accounts of the key lemmas that support the main proofs. The second contribution is to provide two definitions of α-equivalence relations over (program) contexts, namely expressions with a single meta-variable (or “hole”). One of the definitions is already in the literature, and the other is new. We prove some basic properties of α-equivalence on contexts, and show that the two definitions give rise to the same relation.} +} + +@InProceedings{Gabbay1999, + author={Murdoch Gabbay and Andrew Pitts}, + title={A New Approach to Abstract Syntax Involving Binders}, + booktitle={Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999}, + year=1999, + editor={Giuseppe Longo}, + month={July}, + pages={214--224}, + location={Trento, Italy}, + publisher={IEEE Computer Society Press} +} + +@article{Gabbay2002, + author={Gabbay, Murdoch J. and Pitts, Andrew M.}, + title={A New Approach to Abstract Syntax with Variable Binding}, + year={2002}, + issue_date={Jul 2002}, + publisher={Springer-Verlag}, + address={Berlin, Heidelberg}, + volume={13}, + number={3–5}, + issn={0934-5043}, + url={https://doi.org/10.1007/s001650200016}, + doi={10.1007/s001650200016}, + abstract={The permutation model of set theory with atoms (FM-sets), devised by Fraenkel and Mostowski in the 1930s, supports notions of ‘name-abstraction’ and ‘fresh name’ that provide a new way to represent, compute with, and reason about the syntax of formal systems involving variable-binding operations. Inductively defined FM-sets involving the name-abstraction set former (together with Cartesian product and disjoint union) can correctly encode syntax modulo renaming of bound variables. In this way, the standard theory of algebraic data types can be extended to encompass signatures involving binding operators. In particular, there is an associated notion of structural recursion for defining syntax-manipulating functions (such as capture avoiding substitution, set of free variables, etc.) and a notion of proof by structural induction, both of which remain pleasingly close to informal practice in computer science.}, + journal={Form. Asp. Comput.}, + month=jul, + pages={341–363}, + numpages={23}, + keywords={Keywords: Abstract syntax; Alpha-conversion; Permutation actions; Set theory; Structural induction} +} + +@book{Barendregt1985, + author={Hendrik Pieter Barendregt}, + title={The lambda calculus - its syntax and semantics}, + series={Studies in logic and the foundations of mathematics}, + volume={103}, + publisher={North-Holland}, + year={1985}, + isbn={978-0-444-86748-3}, + timestamp={Fri, 28 Jun 2019 12:45:52 +0200}, + biburl={https://dblp.org/rec/books/daglib/0067558.bib}, + bibsource={dblp computer science bibliography, https://dblp.org} +} + +@book{Church1941, + ISBN={9780691083940}, + author={ALONZO CHURCH}, + publisher={Princeton University Press}, + title={The Calculi of Lambda Conversion. (AM-6)}, + year={1941} +} + +@book{Hindley1988, + title={Introduction to Combinators and $\lambda$-Calculus}, + author={Hindley, J. Roger and Seldin, Jonathan P.}, + series={London Mathematical Society Student Texts}, + volume={1}, + year={1988}, + publisher={Cambridge University Press}, + address={Cambridge, UK} +}