Tm.lam as name abstraction

The binder Tm.lam a factors through name abstraction: Tm.lam a t = tmLam (abs a t). The fv-based α-rename Tm.lam_rename_fresh and the some=any principle Tm.lam_some_any follow from abs_rename.

Main results

• avoid — an α-equivalent representative that avoids a chosen non-free atom.
• Tm.lam_rename_fresh — rename the bound name to any atom fresh for the term.
• tmLam and Tm.lam_eq_tmLam — the binder factors through NameAbs Tm.
• Tm.lam_some_any — the Gabbay–Pitts some=any principle for the binder.

theorem CatCrypt.Nominal.Lambda.avoid (c : Atom) (r : Raw) : c ∉ fv r → ∃ (r' : Raw), AEq r r' ∧ c ∉ atoms r'

Rename a bound name away. If c is not free in r, some α-equivalent r' avoids c entirely (as a bound name too).

theorem CatCrypt.Nominal.Lambda.Tm.lam_rename_fresh (a c : Atom) (t : Tm) (hc : c ∉ t.freeVars) (_hca : c ≠ a) : lam a t = lam c (FinPerm.swap a c • t)

fv-based α-rename for Tm.lam. Changing the bound name to any atom fresh for the term (not only for a representative) gives an equal term.

theorem CatCrypt.Nominal.Lambda.Tm.lam_absRel {a a' : Atom} {t t' : Tm} (h : AbsRel (a, t) (a', t')) : lam a t = lam a' t'

The compatibility of Tm.lam with α-equivalence of the abstraction.

noncomputable def CatCrypt.Nominal.Lambda.tmLam : NameAbs Tm → Tm

Tm.lam factors through name abstraction.

Equations

• CatCrypt.Nominal.Lambda.tmLam = CatCrypt.Nominal.NameAbs.lift (fun (a : CatCrypt.Nominal.Atom) (t : CatCrypt.Nominal.Lambda.Tm) => CatCrypt.Nominal.Lambda.Tm.lam a t) ⋯

@[simp]

theorem CatCrypt.Nominal.Lambda.tmLam_abs (a : Atom) (t : Tm) : tmLam (abs a t) = Tm.lam a t

theorem CatCrypt.Nominal.Lambda.Tm.lam_eq_tmLam (a : Atom) (t : Tm) : lam a t = tmLam (abs a t)

The syntactic binder is the nominal abstraction: Tm.lam a t = tmLam (abs a t).

theorem CatCrypt.Nominal.Lambda.Tm.lam_some_any (a b c : Atom) (t : Tm) (hb : b ∉ t.freeVars) (hc : c ∉ t.freeVars) (hba : b ≠ a) (hca : c ≠ a) : lam b (FinPerm.swap a b • t) = lam c (FinPerm.swap a c • t)

Some = any (freshness) for the binder. Two atoms fresh for the term give the same abstraction after the corresponding renaming — the Gabbay–Pitts principle, inherited from abs.