Skip to content

Commit 1001e7d

Browse files
amarmadukeamarmaduke
committed
add grind annotations
1 parent 49a61b2 commit 1001e7d

5 files changed

Lines changed: 49 additions & 48 deletions

File tree

‎Examples/LambdaCalc.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -15,18 +15,18 @@ namespace LeanSubst.Examples.LambdaCalc
1515
| re y => var y
1616
| su t => t
1717

18-
@[simp]
18+
@[simp, grind =]
1919
theorem Term.from_action_id {n} : from_action (+0 n) = var n := by
2020
simp [from_action, Subst.id]
2121

22-
@[simp]
22+
@[simp, grind =]
2323
theorem Term.from_action_succ {n} : from_action (+1 n) = var (n + 1) := by
2424
simp [from_action, Subst.succ]
2525

26-
@[simp]
26+
@[simp, grind =]
2727
theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action]
2828

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

3232
instance instCoe_SubstActionTerm_Term : Coe (Subst.Action Term) Term where
@@ -50,15 +50,15 @@ namespace LeanSubst.Examples.LambdaCalc
5050
instance SubstMap_Term : SubstMap Term Term where
5151
smap := smap
5252

53-
@[simp]
53+
@[simp, grind =]
5454
theorem subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ x := by
5555
simp [SubstMap.smap]
5656

57-
@[simp]
57+
@[simp, grind =]
5858
theorem subst_app {t1 t2} {σ : Subst Term} : (t1 :@ t2)[σ] = t1[σ] :@ t2[σ] := by
5959
simp [SubstMap.smap]
6060

61-
@[simp]
61+
@[simp, grind =]
6262
theorem subst_lam {t} {σ : Subst Term} : (:λ t)[σ] = :λ t[σ.lift] := by
6363
simp [SubstMap.smap]
6464

‎LeanSubst/Basic.lean‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -77,33 +77,33 @@ namespace LeanSubst
7777
notation "-1" => Subst.pred
7878
macro "-1@" noWs T:term : term =>`(@Subst.pred $T)
7979

80-
@[simp]
80+
@[simp, grind =]
8181
theorem Subst.id_action {n} : (+0@T) n = re n := by simp [Subst.id]
8282

83-
@[simp]
83+
@[simp, grind =]
8484
theorem Subst.succ_action {n} : (+1@T) n = re (n + 1) := by simp [Subst.succ]
8585

86-
@[simp]
86+
@[simp, grind =]
8787
theorem Subst.pred_action {n} : (-1@T) n = re (n - 1) := by simp [Subst.pred]
8888

89-
@[simp]
89+
@[simp, grind =]
9090
theorem Ren.to_id : Ren.to (T := T) id = +0 := by
9191
unfold Ren.to; unfold Subst.id; simp
9292

93-
@[simp]
93+
@[simp, grind =]
9494
theorem Ren.to_succ : Ren.to (T := T) (· + 1) = +1 := by
9595
unfold Ren.to; simp; unfold Subst.succ; simp
9696

97-
@[simp]
97+
@[simp, grind =]
9898
theorem Ren.to_pred : Ren.to (T := T) (· - 1) = -1 := by
9999
unfold Ren.to; simp; unfold Subst.pred; simp
100100

101-
@[simp]
101+
@[simp, grind =]
102102
theorem Ren.pred_succ [RenMap T] [SubstMap T T] : Subst.compose (T := T) +1 -1 = +0 := by
103103
unfold Subst.compose; simp
104104
unfold Subst.id; rfl
105105

106-
@[simp]
106+
@[grind =]
107107
theorem Ren.to_lift [RenMap T] {r : Ren} : r.lift.to = (@Ren.to T r).lift := by
108108
funext; case _ x =>
109109
cases x
@@ -118,7 +118,7 @@ namespace LeanSubst
118118
unfold Subst.lift at rhsdef; simp at *
119119
subst lhsdef; subst rhsdef; rfl
120120

121-
@[simp]
121+
@[simp, grind =]
122122
theorem Ren.to_compose {r1 r2 : Ren} [RenMap T] [SubstMap T T]
123123
: Ren.to (T := T) (r2 ∘ r1) = Subst.compose r1 r2
124124
:= by

‎LeanSubst/Laws.lean‎

Lines changed: 26 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -30,57 +30,57 @@ namespace LeanSubst
3030

3131
namespace Subst
3232
section
33-
@[simp]
33+
@[simp, grind =]
3434
theorem rewrite1 : re 0 :: +1 = +0@T := by
3535
funext; case _ x =>
3636
cases x; all_goals (simp [Subst.id, Subst.succ])
3737

3838
open SubstMap
3939
variable [RenMap T]
4040

41-
@[simp]
41+
@[simp, grind =]
4242
theorem I_lift : +0.lift = +0@T := by
4343
funext; case _ x =>
4444
cases x; all_goals (simp [Subst.lift, Subst.id])
4545

46-
@[simp]
46+
@[simp, grind =]
4747
theorem rewrite2 [SubstMap T T] {σ : Subst T} : +0 ∘ σ = σ := by
4848
funext; case _ x =>
4949
unfold Subst.compose; simp [Subst.id]
5050

51-
@[simp]
51+
@[simp, grind =]
5252
theorem rewrite3_replace [SubstMap T T] {σ τ : Subst T} {s : T}
5353
: (su s :: σ) ∘ τ = su s[τ] :: (σ ∘ τ)
5454
:= by
5555
funext; case _ x =>
5656
cases x; all_goals (simp [Subst.compose])
5757

58-
@[simp]
58+
@[simp, grind =]
5959
theorem rewrite3_rename [SubstMap T T] {s} {σ τ : Subst T}
6060
: (re s :: σ) ∘ τ = (τ s) :: (σ ∘ τ)
6161
:= by
6262
funext; case _ x =>
6363
cases x; all_goals (simp [Subst.compose])
6464

65-
@[simp]
65+
@[simp, grind =]
6666
theorem rewrite4 [SubstMap T T] {s} {σ : Subst T} : +1 ∘ (s :: σ) = σ := by
6767
funext; case _ x =>
6868
cases x; all_goals (simp [Subst.compose, Subst.succ])
6969

70-
@[simp]
70+
@[simp, grind =]
7171
theorem rewrite5 [SubstMap T T] {σ : Subst T} : σ 0 :: (+1 ∘ σ) = σ := by
7272
funext; case _ x =>
7373
cases x
7474
case _ => simp
7575
case _ => simp [Subst.succ, Subst.compose]
7676
end
7777

78-
@[simp]
78+
@[simp, grind =]
7979
theorem apply_I_is_id [RenMap T] [SubstMap S T] [SubstMapId S T] {s : S}
8080
: s[+0:T] = s
8181
:= SubstMapId.apply_id
8282

83-
@[simp]
83+
@[simp, grind =]
8484
theorem rewrite_lift [RenMap T] [SubstMap T T] [SubstMapStable T] {σ : Subst T}
8585
: σ.lift = re 0 :: (σ ∘ +1)
8686
:= by
@@ -95,7 +95,7 @@ namespace LeanSubst
9595
rw [apply_stable (σ := +1)]
9696
funext; case _ i => simp [Ren.to, Subst.succ]
9797

98-
@[simp]
98+
@[simp, grind =]
9999
theorem rewrite6 [RenMap T] [SubstMap T T] [SubstMapId T T] {σ : Subst T}
100100
: σ ∘ +0 = σ
101101
:= by
@@ -104,14 +104,14 @@ namespace LeanSubst
104104
generalize zdef : σ x = z
105105
cases z <;> simp at *;
106106

107-
@[simp]
107+
@[simp, grind =]
108108
theorem apply_compose_commute
109109
[RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T]
110110
{s : S} {σ τ : Subst T}
111111
: s[σ:T][τ:_] = s[σ ∘ τ:T]
112112
:= SubstMapCompose.apply_compose
113113

114-
@[simp]
114+
@[simp, grind =]
115115
theorem rewrite7
116116
[RenMap T] [SubstMap T T] [SubstMapCompose T T]
117117
{σ τ μ : Subst T}
@@ -121,7 +121,7 @@ namespace LeanSubst
121121
simp [Subst.compose]
122122
cases σ x <;> simp
123123

124-
@[simp]
124+
@[simp, grind =]
125125
theorem hrewrite1
126126
[RenMap T] [SubstMap S T] [SubstMapId S T]
127127
{σ : Subst S}
@@ -132,7 +132,7 @@ namespace LeanSubst
132132
generalize zdef : σ x = z
133133
cases z <;> simp
134134

135-
@[simp]
135+
@[simp, grind =]
136136
theorem hcomp_ren_left
137137
[RenMap S] [RenMap T] [SubstMap S T]
138138
(r : Ren) (σ : Subst T)
@@ -141,15 +141,15 @@ namespace LeanSubst
141141
funext; case _ x =>
142142
induction x <;> simp [Subst.hcompose, Ren.to]
143143

144-
@[simp]
144+
@[simp, grind =]
145145
theorem hrewrite2
146146
[RenMap S] [RenMap T] [SubstMap S T]
147147
{σ : Subst T}
148148
: (+0@S) ◾ σ = +0
149149
:= by
150150
apply hcomp_ren_left (S := S) (T := T) (λ x => x) σ
151151

152-
@[simp]
152+
@[simp, grind =]
153153
theorem hrewrite3
154154
[RenMap S] [RenMap T] [SubstMap S T]
155155
{σ : Subst T}
@@ -158,7 +158,7 @@ namespace LeanSubst
158158
have lem := hcomp_ren_left (S := S) (T := T) (· + 1) σ
159159
simp at lem; exact lem
160160

161-
@[simp]
161+
@[simp, grind =]
162162
theorem hrewrite4
163163
[RenMap T] [SubstMap S T]
164164
{x} {σ : Subst S} {τ : Subst T}
@@ -167,6 +167,7 @@ namespace LeanSubst
167167
funext; case _ i =>
168168
cases i <;> simp [Subst.hcompose]
169169

170+
@[grind =]
170171
theorem hcomp_dist_ren_left
171172
[RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T]
172173
(r : Ren) {σ : Subst S} {τ : Subst T}
@@ -175,7 +176,7 @@ namespace LeanSubst
175176
funext; case _ x =>
176177
simp [Subst.hcompose, Subst.compose, Ren.to]
177178

178-
@[simp]
179+
@[simp, grind =]
179180
theorem hrewrite5
180181
[RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T]
181182
{σ : Subst S} {τ μ : Subst T}
@@ -186,6 +187,7 @@ namespace LeanSubst
186187
generalize zdef : σ x = z
187188
cases z <;> simp
188189

190+
@[grind =]
189191
theorem hcomp_distr_ren_right
190192
[RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T]
191193
(r : Ren) (σ : Subst S) (μ : Subst T)
@@ -197,7 +199,7 @@ namespace LeanSubst
197199
cases z <;> simp
198200
rw [SubstMapRenCommute.apply_ren_commute r μ]
199201

200-
@[simp]
202+
@[simp, grind =]
201203
theorem hrewrite6
202204
[RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T]
203205
(r : Ren) (σ : Subst S)
@@ -206,14 +208,14 @@ namespace LeanSubst
206208
have lem := hcomp_distr_ren_right (T := T) r σ +1
207209
simp at lem; exact lem
208210

209-
@[simp]
211+
@[simp, grind =]
210212
theorem apply_hcompose
211213
[RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T]
212214
{s : S} {σ : Subst S} {τ : Subst T}
213215
: s[σ][τ:T] = s[τ:T][σ ◾ τ]
214216
:= by exact SubstMapHetCompose.apply_hcompose
215217

216-
@[simp]
218+
@[simp, grind =]
217219
theorem hrewrite7
218220
[RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T]
219221
{σ τ : Subst S} (μ : Subst T)
@@ -238,9 +240,8 @@ namespace LeanSubst
238240
funext; case _ t =>
239241
induction t generalizing $r $σ
240242
all_goals simp [rmap, smap, *] at *; try simp [*]
241-
-- any_goals solve | (
242-
-- rw [<-Ren.lift_eq_from_eq (r := r) h])
243243
any_goals solve | (rw [<-h]; simp [Ren.to])
244+
all_goals grind
244245
})
245246

246247
macro "subst_solve_hcompose"
@@ -288,7 +289,7 @@ namespace LeanSubst
288289
try any_goals solve | (
289290
simp [-Subst.rewrite_lift, *]
290291
rw [<-Ren.to_lift]
291-
simp [-Subst.rewrite_lift, -Ren.to_lift, *])
292+
simp [-Subst.rewrite_lift, *])
292293
have lem3s {σ : Subst $Ty} {t : $Ty} : t[+1:$Ty][σ:_] = t[+1 ∘ σ:_] := by
293294
rw [<-Ren.to_succ, lem3]
294295
have lem4 {σ τ : Subst $Ty} : +1 ∘ τ ∘ σ = (+1 ∘ τ) ∘ σ := by
@@ -312,7 +313,7 @@ namespace LeanSubst
312313
try any_goals solve | (
313314
simp [-Subst.rewrite_lift, *]
314315
rw [<-Ren.to_lift]
315-
simp [-Subst.rewrite_lift, -Ren.to_lift, *])
316+
simp [-Subst.rewrite_lift, *])
316317
have lem7s {τ : Subst $Ty} {t : $Ty} : t[τ:_][+1:$Ty] = t[τ ∘ +1:_] := by
317318
rw [<-Ren.to_succ, lem7]
318319
have lem8 {σ τ : Subst $Ty} : (σ ∘ +1) ∘ τ = σ ∘ +1 ∘ τ := by

‎LeanSubst/List.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,11 @@ def List.smap [SubstMap S T] (σ : Subst T) : List S -> List S
2020
instance [SubstMap S T] : SubstMap (List S) T where
2121
smap := List.smap
2222

23-
@[simp]
23+
@[simp, grind =]
2424
theorem List.smap_nil [SubstMap S T] {σ : Subst T} : (@List.nil S)[σ:_] = [] := by
2525
simp [SubstMap.smap, List.smap]
2626

27-
@[simp]
27+
@[simp, grind =]
2828
theorem List.smap_cons [SubstMap S T] {x} {tl : List S} {σ : Subst T}
2929
: (x :: tl)[σ:_] = x[σ:_] :: tl[σ:_]
3030
:= by
@@ -40,7 +40,7 @@ instance [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S
4040
where
4141
apply_compose := by intro s σ τ; induction s <;> simp [*]
4242

43-
@[simp]
43+
@[simp, grind =]
4444
def List.dep_subst_get [SubstMap S T] (σ : Subst T) : List S -> Nat -> Option S
4545
| .nil, _ => none
4646
| .cons h _, 0 => return h[σ:_]
@@ -66,13 +66,13 @@ def unexpand_list_dep_subst_get : Lean.PrettyPrinter.Unexpander
6666
| `($_ (T := $T) $σ $t $x) => `($t[$x|$σ : $T])
6767
| _ => throw ()
6868

69-
@[simp]
69+
@[simp, grind =]
7070
theorem List.dep_subst_get_zero [SubstMap S T] {σ : Subst T} {A : S} {Γ : List S}
7171
: (A::Γ)[0|σ:_] = A[σ:_]
7272
:= by
7373
simp [dep_subst_get]
7474

75-
@[simp]
75+
@[simp, grind =]
7676
theorem List.dep_subst_get_succ [SubstMap S T] {σ : Subst T} {A : S} {Γ : List S} {x}
7777
: (A::Γ)[x + 1|σ:_] = Γ[x|σ:_][σ:_]
7878
:= by

‎LeanSubst/Option.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,13 +19,13 @@ def Option.smap [SubstMap S T] (σ : Subst T) : Option S -> Option S
1919
instance [SubstMap S T] : SubstMap (Option S) T where
2020
smap := Option.smap
2121

22-
@[simp]
22+
@[simp, grind =]
2323
theorem Option.smap_none [SubstMap S T] {σ : Subst T}
2424
: (@Option.none S)[σ:_] = none
2525
:= by
2626
simp [SubstMap.smap, Option.smap]
2727

28-
@[simp]
28+
@[simp, grind =]
2929
theorem Option.smap_some [SubstMap S T] {x : S} {σ : Subst T}
3030
: (some x)[σ:_] = some x[σ:_]
3131
:= by

0 commit comments

Comments
 (0)