Skip to content

Commit 9126d76

Browse files
amarmadukeamarmaduke
authored
Restructure to make renamings primary (#1)
1 parent 705cab3 commit 9126d76

15 files changed

Lines changed: 981 additions & 958 deletions

File tree

LeanSubst/List.lean renamed to Archive/List.lean

File renamed without changes.

‎Examples/LambdaCalc.lean‎

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ namespace LeanSubst.Examples.LambdaCalc
1111
infixl:65 " :@ " => Term.app
1212

1313
@[coe]
14-
def Term.from_action : Subst.Action Term -> Term
14+
def Term.from_action : Action Term -> Term
1515
| re y => var y
1616
| su t => t
1717

@@ -29,34 +29,34 @@ namespace LeanSubst.Examples.LambdaCalc
2929
@[simp, grind =]
3030
theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action]
3131

32-
instance instCoe_SubstActionTerm_Term : Coe (Subst.Action Term) Term where
32+
instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where
3333
coe := Term.from_action
3434

3535
@[simp]
36-
def rmap (r : Ren) : Term -> Term
36+
def rmap (r : Ren Term) : Term -> Term
3737
| .var x => .var (r.act x)
3838
| t1 :@ t2 => rmap r t1 :@ rmap r t2
3939
| :λ t => :λ rmap r.lift t
4040

41-
instance : RenMap Term where
41+
instance : RenMap Term Term where
4242
rmap := rmap
4343

4444
@[simp, grind =]
45-
theorem ren_var {x} {r : Ren} : (Term.var x)⟨r⟩ = .var (r.act x) := by
45+
theorem ren_var {x} {r : Ren Term} : (Term.var x)⟨r⟩ = .var (r.act x) := by
4646
simp [RenMap.rmap]
4747

4848
@[simp, grind =]
49-
theorem ren_app {t1 t2} {r : Ren} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by
49+
theorem ren_app {t1 t2} {r : Ren Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by
5050
simp [RenMap.rmap]
5151

5252
@[simp, grind =]
53-
theorem ren_lam {t} {r : Ren} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by
53+
theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by
5454
simp [RenMap.rmap]
5555

56-
instance : RenMapId Term where
56+
instance : RenMapId Term Term where
5757
apply_id := by subst_solve_id
5858

59-
instance : RenMapCompose Term where
59+
instance : RenMapCompose Term Term where
6060
apply_compose := by subst_solve_compose
6161

6262
@[simp]
@@ -88,16 +88,24 @@ namespace LeanSubst.Examples.LambdaCalc
8888
generalize zdef : σ.act x = z
8989
cases z <;> simp [Term.from_action]
9090

91+
@[simp]
92+
theorem Term.from_action_compose_ren {x} {σ : Subst Term} {r : Ren Term}
93+
: (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x)
94+
:= by
95+
simp [Term.from_action]
96+
generalize zdef : σ.act x = z
97+
cases z <;> simp
98+
9199
instance : SubstMapId Term Term where
92100
apply_id := by subst_solve_id
93101

94-
instance : SubstMapStable Term where
102+
instance : SubstMapStable Term Term where
95103
apply_stable := by subst_solve_stable
96104

97105
instance : SubstMapRenComposeLeft Term Term where
98106
apply_ren_compose_left := by subst_solve_compose
99107

100-
instance : SubstMapRenComposeRight Term Term where
108+
instance : SubstMapRenComposeRight Term where
101109
apply_ren_compose_right := by subst_solve_compose
102110

103111
instance : SubstMapCompose Term Term where

‎Examples/LambdaCalcKit.lean‎

Lines changed: 22 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ namespace LeanSubst.Examples.LambdaCalc
1111
infixl:65 " :@ " => Term.app
1212

1313
@[coe]
14-
def Term.from_action : Subst.Action Term -> Term
14+
def Term.from_action : Action Term -> Term
1515
| re y => var y
1616
| su t => t
1717

@@ -29,11 +29,11 @@ namespace LeanSubst.Examples.LambdaCalc
2929
@[simp, grind =]
3030
theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action]
3131

32-
instance instCoe_SubstActionTerm_Term : Coe (Subst.Action Term) Term where
32+
instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where
3333
coe := Term.from_action
3434

3535
@[simp]
36-
def Term.ren_act (r : Ren) : Term -> Term
36+
def Term.ren_act (r : Ren Term) : Term -> Term
3737
| .var x => .var (r.act x)
3838
| t => t
3939

@@ -47,12 +47,12 @@ namespace LeanSubst.Examples.LambdaCalc
4747
lift (f : A) (k : Nat := 1) : A
4848

4949
@[simp]
50-
instance : Kit Term Ren where
50+
instance : Kit Term (Ren Term) where
5151
act := Term.ren_act
5252
lift f n := Ren.lift f n
5353

5454
@[simp]
55-
instance [RenMap Term] : Kit Term (Subst Term) where
55+
instance [RenMap Term Term] : Kit Term (Subst Term) where
5656
act := Term.subst_act
5757
lift f n := Subst.lift f n
5858

@@ -63,27 +63,27 @@ namespace LeanSubst.Examples.LambdaCalc
6363
| :λ t => :λ kitmap (kit.lift σ) t
6464

6565
@[simp]
66-
def rmap (r : Ren) : Term -> Term := kitmap r
66+
def rmap (r : Ren Term) : Term -> Term := kitmap r
6767

68-
instance : RenMap Term where
68+
instance : RenMap Term Term where
6969
rmap := rmap
7070

7171
@[simp, grind =]
72-
theorem ren_var {x} {r : Ren} : (Term.var x)⟨r⟩ = .var (r.act x) := by
72+
theorem ren_var {x} {r : Ren Term} : (Term.var x)⟨r⟩ = .var (r.act x) := by
7373
simp +instances [RenMap.rmap]
7474

7575
@[simp, grind =]
76-
theorem ren_app {t1 t2} {r : Ren} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by
76+
theorem ren_app {t1 t2} {r : Ren Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by
7777
simp [RenMap.rmap]
7878

7979
@[simp, grind =]
80-
theorem ren_lam {t} {r : Ren} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by
80+
theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by
8181
simp +instances [RenMap.rmap]
8282

83-
instance : RenMapId Term where
83+
instance : RenMapId Term Term where
8484
apply_id := by intro t; induction t <;> simp [*]
8585

86-
instance : RenMapCompose Term where
86+
instance : RenMapCompose Term Term where
8787
apply_compose := by subst_solve_compose
8888

8989
@[simp]
@@ -112,16 +112,24 @@ namespace LeanSubst.Examples.LambdaCalc
112112
generalize zdef : σ.act x = z
113113
cases z <;> simp [Term.from_action]
114114

115+
@[simp]
116+
theorem Term.from_action_compose_ren {x} {σ : Subst Term} {r : Ren Term}
117+
: (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x)
118+
:= by
119+
simp [Term.from_action]
120+
generalize zdef : σ.act x = z
121+
cases z <;> simp
122+
115123
instance : SubstMapId Term Term where
116124
apply_id := by subst_solve_id
117125

118-
instance : SubstMapStable Term where
126+
instance : SubstMapStable Term Term where
119127
apply_stable := by subst_solve_stable
120128

121129
instance : SubstMapRenComposeLeft Term Term where
122130
apply_ren_compose_left := by subst_solve_compose
123131

124-
instance : SubstMapRenComposeRight Term Term where
132+
instance : SubstMapRenComposeRight Term where
125133
apply_ren_compose_right := by subst_solve_compose
126134

127135
instance : SubstMapCompose Term Term where

‎LeanSubst.lean‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
11

2-
import LeanSubst.Ren
3-
import LeanSubst.HetRen
4-
import LeanSubst.Subst
2+
import LeanSubst.Basic
3+
import LeanSubst.Ops
54
import LeanSubst.Laws
6-
import LeanSubst.Option
7-
import LeanSubst.List
8-
import LeanSubst.Reduction
9-
import LeanSubst.Normal
5+
import LeanSubst.Types.Option
6+
import LeanSubst.Types.List
7+
import LeanSubst.Rewriting.Reduction
8+
import LeanSubst.Rewriting.Normal

‎LeanSubst/Basic.lean‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
2+
namespace LeanSubst
3+
4+
universe u1 u2
5+
variable {S : Type u1} {T : Type u2}
6+
7+
structure Ren (T : Type u2) where
8+
act : Nat -> Nat
9+
10+
class RenMap (S : Type u1) (T : Type u2) where
11+
rmap : Ren T -> S -> S
12+
13+
export RenMap (rmap)
14+
15+
macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t)
16+
17+
@[app_unexpander rmap]
18+
def unexpand_rmap : Lean.PrettyPrinter.Unexpander
19+
| `($_ $r $t) => `($t⟨$r⟩)
20+
| _ => throw ()
21+
22+
inductive Action (T : Type u2) where
23+
| re : Nat -> Action T
24+
| su : T -> Action T
25+
deriving Repr
26+
27+
export Action (re su)
28+
29+
structure Subst (T : Type u2) where
30+
act : Nat -> Action T
31+
32+
class SubstMap (S : Type u1) (T : Type u2) where
33+
smap : Subst T -> S -> S
34+
35+
export SubstMap (smap)
36+
37+
macro:max t:term noWs "[" σ:term "]" : term => `(smap $σ $t)
38+
39+
@[app_unexpander smap]
40+
def unexpand_smap : Lean.PrettyPrinter.Unexpander
41+
| `($_ $σ $t) => `($t[$σ])
42+
| _ => throw ()
43+
44+
end LeanSubst

‎LeanSubst/HetRen.lean‎

Lines changed: 0 additions & 123 deletions
This file was deleted.

0 commit comments

Comments
 (0)