Skip to content

Commit 38ab5aa

Browse files
amarmadukeamarmaduke
committed
experiment with kits
1 parent 1ade351 commit 38ab5aa

3 files changed

Lines changed: 171 additions & 1 deletion

File tree

‎Examples/LambdaCalcKit.lean‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
import LeanSubst
2+
3+
namespace LeanSubst.Examples.LambdaCalc
4+
5+
inductive Term where
6+
| var : Nat -> Term
7+
| app : Term -> Term -> Term
8+
| lam : Term -> Term
9+
10+
prefix:100 ":λ " => Term.lam
11+
infixl:65 " :@ " => Term.app
12+
13+
@[coe]
14+
def Term.from_action : Subst.Action Term -> Term
15+
| re y => var y
16+
| su t => t
17+
18+
@[simp, grind =]
19+
theorem Term.from_action_id {n} : from_action (+0 n) = var n := by
20+
simp [from_action, Subst.id]
21+
22+
@[simp, grind =]
23+
theorem Term.from_action_succ {n} : from_action (+1 n) = var (n + 1) := by
24+
simp [from_action, Subst.succ]
25+
26+
@[simp, grind =]
27+
theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action]
28+
29+
@[simp, grind =]
30+
theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action]
31+
32+
instance instCoe_SubstActionTerm_Term : Coe (Subst.Action Term) Term where
33+
coe := Term.from_action
34+
35+
class Kit (A : Type) where
36+
coe : A -> Term
37+
lift : (Nat -> A) -> Nat -> A
38+
39+
instance : Kit Nat where
40+
coe := Term.var
41+
lift := Ren.lift
42+
43+
instance [RenMap Term] : Kit (Subst.Action Term) where
44+
coe := Term.from_action
45+
lift := Subst.lift
46+
47+
@[simp]
48+
def kitmap {A} (σ : Nat -> A) [kit : Kit A] : Term -> Term
49+
| .var x => kit.coe (σ x)
50+
| t1 :@ t2 => kitmap σ t1 :@ kitmap σ t2
51+
| :λ t => :λ kitmap (kit.lift σ) t
52+
53+
@[simp]
54+
def rmap (r : Ren) : Term -> Term := kitmap r
55+
56+
instance : RenMap Term where
57+
rmap := rmap
58+
59+
@[simp]
60+
def smap (σ : Subst Term) : Term -> Term := kitmap σ
61+
62+
instance SubstMap_Term : SubstMap Term Term where
63+
smap := smap
64+
65+
@[simp, grind =]
66+
theorem subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ x := by
67+
simp [SubstMap.smap]
68+
69+
@[simp, grind =]
70+
theorem subst_app {t1 t2} {σ : Subst Term} : (t1 :@ t2)[σ] = t1[σ] :@ t2[σ] := by
71+
simp [SubstMap.smap]
72+
73+
@[simp, grind =]
74+
theorem subst_lam {t} {σ : Subst Term} : (:λ t)[σ] = :λ t[σ.lift] := by
75+
simp [SubstMap.smap]
76+
77+
@[simp]
78+
theorem Term.from_action_compose {x} {σ τ : Subst Term}
79+
: (from_action (σ x))[τ] = from_action ((σ ∘ τ) x)
80+
:= by
81+
simp [Term.from_action, Subst.compose]
82+
generalize zdef : σ x = z
83+
cases z <;> simp [Term.from_action]
84+
85+
theorem apply_id {t : Term} : t[+0] = t := by
86+
induction t
87+
all_goals (simp at * <;> try simp [*])
88+
89+
instance : SubstMapId Term Term where
90+
apply_id := apply_id
91+
92+
theorem apply_stable (r : Ren) (σ : Subst Term)
93+
: r = σ -> rmap r = smap σ
94+
:= by subst_solve_stable r, σ
95+
96+
instance : SubstMapStable Term where
97+
apply_stable := apply_stable
98+
99+
theorem apply_compose {s : Term} {σ τ : Subst Term} : s[σ][τ] = s[σ ∘ τ] := by
100+
subst_solve_compose Term, s, σ, τ
101+
102+
instance : SubstMapCompose Term Term where
103+
apply_compose := apply_compose
104+
105+
end LeanSubst.Examples.LambdaCalc

‎LeanSubst/Basic.lean‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,18 @@ namespace LeanSubst
101101
unfold Subst.compose; simp
102102
unfold Subst.id; rfl
103103

104+
@[simp, grind =]
105+
theorem Ren.lift_zero {r : Ren} : r.lift 0 = r := by
106+
unfold Ren.lift; funext; case _ i => grind
107+
108+
@[simp, grind =]
109+
theorem Ren.lift_succ {r : Ren} {k} : r.lift (k + 1) = (r.lift k).lift := by
110+
induction k; simp
111+
case _ n ih =>
112+
unfold Ren.lift; funext; case _ i =>
113+
simp; unfold Ren.lift at ih; simp at ih
114+
grind
115+
104116
@[grind =]
105117
theorem Ren.to_lift [RenMap T] {r : Ren} {k} : (r.lift k).to = (@Ren.to T r).lift k := by
106118
funext; case _ x =>

‎LeanSubst/Laws.lean‎

Lines changed: 54 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,31 @@ namespace LeanSubst
9696
rw [apply_stable (σ := +1)]
9797
funext; case _ i => simp [Ren.to, Subst.succ]
9898

99+
@[simp, grind =]
100+
theorem rewrite_lift_zero [RenMap S] [SubstMap S S] [SubstMapId S S] [SubstMapStable S] {σ : Subst S}
101+
: σ.lift 0 = σ
102+
:= by
103+
unfold Subst.lift; funext; case _ i =>
104+
simp; generalize zdef : σ i = z
105+
cases z <;> simp
106+
rw [SubstMapStable.apply_stable (λ x => x) +0 rfl]
107+
simp
108+
109+
@[simp, grind =]
110+
theorem rewrite_lift_succ [RenMap S] [SubstMap S S] [SubstMapId S S] [SubstMapStable S] {k} {σ : Subst S}
111+
: σ.lift (k + 1) = (σ.lift k).lift
112+
:= by
113+
induction k; simp
114+
case _ n ih =>
115+
replace ih i : σ.lift (n + 1) i = (σ.lift n).lift 1 i := by rw [ih]
116+
funext; case _ i =>
117+
cases i <;> simp [Subst.lift]
118+
case _ i =>
119+
replace ih := ih i
120+
unfold Subst.lift at ih; simp at ih
121+
122+
sorry
123+
99124
@[simp, grind =]
100125
theorem rewrite6 [RenMap T] [SubstMap T T] [SubstMapId T T] {σ : Subst T}
101126
: σ ∘ +0 = σ
@@ -227,6 +252,34 @@ namespace LeanSubst
227252
generalize zdef : σ x = z
228253
cases z <;> simp
229254

255+
theorem hrewrite_lift1
256+
[RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
257+
[SubstMapId S S] [SubstMapStable S] [SubstMapRenCommute S T]
258+
{σ : Subst S} {τ : Subst T}
259+
: (σ ◾ τ).lift = σ.lift ◾ τ
260+
:= by
261+
unfold Subst.lift; funext; case _ i =>
262+
cases i <;> simp [hcompose]
263+
case _ n =>
264+
generalize zdef : σ n = z
265+
cases z <;> simp; case _ t =>
266+
rw [apply_stable (· + 1) (Ren.to (· + 1)) rfl]
267+
rw [SubstMapRenCommute.apply_ren_commute]
268+
269+
@[simp, grind =]
270+
theorem hrewrite_lift
271+
[RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
272+
[SubstMapId S S] [SubstMapStable S] [SubstMapRenCommute S T]
273+
{k} {σ : Subst S} {τ : Subst T}
274+
: (σ ◾ τ).lift k = σ.lift k ◾ τ
275+
:= by
276+
induction k generalizing σ τ
277+
case _ => simp
278+
case _ i ih =>
279+
simp; rw [ih]
280+
rw [rewrite_lift_zero]
281+
rw [rewrite_lift_zero]
282+
rw [hrewrite_lift1]
230283
end Subst
231284

232285
macro "subst_solve_id" S:term "," T:term "," t:term : tactic => `(tactic| {
@@ -242,7 +295,7 @@ namespace LeanSubst
242295
induction t generalizing $r $σ
243296
all_goals simp [rmap, smap, *] at *; try simp [*]
244297
any_goals solve | (rw [<-h]; simp [Ren.to])
245-
all_goals grind
298+
all_goals try repeat funext; grind
246299
})
247300

248301
macro "subst_solve_hcompose"

0 commit comments

Comments
 (0)