1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
import Mathlib
import Nominal.Permutations
import Nominal.Support
import Nominal.Helpers.CountableString
/-!
# λ-Preterms
As a practical example for nominal sets, this file defines λ-preterms (that is, λ-terms without α-equivalence).
-/
namespace Lambda
/-!
## Basic Syntax Definition
Define the AST and a parser for it.
-/
section Syntax
/-- We will use strings as the set of atoms, representing variable names. -/
def Var := String
deriving DecidableEq, Countable, Infinite
/-- Basic λ-preterm definition.
We furthermore allow defining λ-terms as ⟫ t ⟪ with
t, u ::= x | λ x y ..., t | t u,
where x, y, ... are variables. -/
inductive Preterm
| var : Var → Preterm
| abs : Var → Preterm → Preterm
| app : Preterm → Preterm → Preterm
deriving DecidableEq
open Lean Elab Meta
declare_syntax_cat lam
syntax ident : lam
syntax "(" lam ")" : lam
syntax:10 (name := stxabs) "λ " ident+ ", " lam : lam
syntax:45 lam:45 lam:46 : lam
partial def elabLam : Syntax → MetaM Expr
| `(lam | $x:ident) => mkAppM ``Preterm.var #[mkStrLit x.getId.toString]
| `(lam | ($t:lam)) => elabLam t
| `(lam | $t:lam $u:lam) => do mkAppM ``Preterm.app #[← elabLam t, ← elabLam u]
| `(lam | λ $xs:ident*, $t:lam) => do
xs.foldrM (fun x t' => mkAppM ``Preterm.abs #[mkStrLit x.getId.toString, t']) (← elabLam t)
| _ => throwUnsupportedSyntax
elab "⟫ " t:lam " ⟪" : term => elabLam t
example : ⟫ x y z ⟪ = ⟫ (x y) z ⟪ := by decide
example : ⟫ λ x, λ y, x ⟪ = ⟫ λ x y, x ⟪ := by decide
end Syntax
/-!
## Nominal Set Instance
The set of preterms forms a nominal set, where the permutation action just renames all occurrences of a variable.
-/
section NominalSet
namespace Preterm
private def rename (π : FPerm Var) : Preterm → Preterm
| .var x => .var (π • x)
| .abs x t => .abs (π • x) (rename π t)
| .app t u => .app (rename π t) (rename π u)
private lemma one_rename (t : Preterm) : rename 1 t = t := by
induction' t <;> all_goals simp [rename, *]
private lemma mul_rename (π τ : FPerm Var) (t : Preterm) : rename (π * τ) t = rename π (rename τ t) := by
induction' t <;> all_goals simp [rename, mul_smul, *]
instance : PermSet Var Preterm where
smul := rename
one_smul := one_rename
mul_smul := mul_rename
@[simp] lemma smul_var {π : FPerm Var} {x : Var} : π • Preterm.var x = Preterm.var (π • x) := rfl
@[simp] lemma smul_abs {π : FPerm Var} {x : Var} {t : Preterm} : π • Preterm.abs x t = Preterm.abs (π • x) (π • t) := rfl
@[simp] lemma smul_app {π : FPerm Var} {t u : Preterm} : π • Preterm.app t u = Preterm.app (π • t) (π • u) := rfl
private def aSupport : Preterm → Set Var
| .var x => {x}
| .abs x t => {x} ∪ aSupport t
| .app t u => aSupport t ∪ aSupport u
instance : NominalSet Var Preterm where
fin_supp t := by
use aSupport t
induction' t <;> all_goals expose_names
· constructor
· simp [PermSet.HasSupport, PermSet.fix, aSupport, PermSet.fix']
· simp [aSupport]
· constructor
· intro π hπ
simp only [PermSet.fix', smul_abs, Preterm.abs.injEq, Set.mem_setOf_eq]
simp only [PermSet.fix, aSupport, Set.singleton_union, Set.mem_insert_iff, forall_eq_or_imp, Set.mem_setOf_eq] at hπ
exact ⟨hπ.left, a_ih.left hπ.right⟩
· simp [aSupport, Set.Finite.insert, a_ih]
· constructor
· intro π hπ
simp only [PermSet.fix', smul_app, Preterm.app.injEq, Set.mem_setOf_eq]
simp only [PermSet.fix, aSupport, Set.mem_union, Set.mem_setOf_eq] at hπ
constructor
· exact a_ih.left (fun x hx => hπ x (Or.inl hx))
· exact a_ih_1.left (fun x hx => hπ x (Or.inr hx))
· simp [aSupport, a_ih, a_ih_1]
end Preterm
end NominalSet
end Lambda
|
