Skip to content

Commit 5ee0180

Browse files
LinyxusLinyxus
committed
Use simp only for a lot of cases
1 parent 25f0d62 commit 5ee0180

File tree

7 files changed

+59
-57
lines changed

7 files changed

+59
-57
lines changed

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/Core.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -43,15 +43,15 @@ structure Rebind (Γ : Ctx s1) (f : Rename s1 s2) (Δ : Ctx s2) where
4343
def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.rename f) where
4444
var := fun x P hb => by
4545
cases hb
46-
case here => simp [<-Ty.rename_succVar_comm]; constructor
46+
case here => simp only [<-Ty.rename_succVar_comm]; constructor
4747
case there_var hb =>
48-
simp [<-Ty.rename_succVar_comm]
48+
simp only [<-Ty.rename_succVar_comm]
4949
constructor
5050
apply ρ.var _ _ hb
5151
tvar := fun X S hb => by
5252
cases hb
5353
case there_var hb =>
54-
simp [<-Ty.rename_succVar_comm]
54+
simp only [<-Ty.rename_succVar_comm]
5555
constructor
5656
apply ρ.tvar _ _ hb
5757

@@ -62,14 +62,14 @@ def Rebind.liftVar (ρ : Rebind Γ f Δ) : Rebind (Γ,x:T) (f.liftVar) (Δ,x:T.r
6262
def Rebind.liftTVar (ρ : Rebind Γ f Δ) : Rebind (Γ,X<:T) (f.liftTVar) (Δ,X<:T.rename f) where
6363
tvar := fun X S hb => by
6464
cases hb
65-
case here => simp [<-Ty.rename_succTVar_comm]; constructor
65+
case here => simp only [<-Ty.rename_succTVar_comm]; constructor
6666
case there_tvar hb =>
67-
simp [<-Ty.rename_succTVar_comm]
67+
simp only [<-Ty.rename_succTVar_comm]
6868
constructor
6969
apply ρ.tvar _ _ hb
7070
var := fun x P hb => by
7171
cases hb
72-
case there_tvar hb => simp [<-Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb
72+
case there_tvar hb => simp only [<-Ty.rename_succTVar_comm]; constructor; apply ρ.var _ _ hb
7373

7474
/-- **Term variable weakening morphism**.
7575

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/RebindTheory/TypeSystem.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ theorem HasType.rebind {f : Rename s1 s2}
3737
{ apply ih ρ }
3838
case abs ih =>
3939
apply HasType.abs
40-
simp [Ty.rename_succVar_comm]
40+
simp only [Ty.rename_succVar_comm]
4141
apply ih ρ.liftVar
4242
case tabs ih =>
4343
apply HasType.tabs
@@ -47,6 +47,6 @@ theorem HasType.rebind {f : Rename s1 s2}
4747
{ apply ih1 ρ }
4848
{ apply ih2 ρ }
4949
case tapp ih =>
50-
simp [Ty.open_tvar_rename_comm]
50+
simp only [Ty.open_tvar_rename_comm]
5151
apply tapp
5252
aesop

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/Core.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -40,17 +40,17 @@ def Retype.liftVar (ρ : Retype Γ σ Δ) : Retype (Γ,x:P) (σ.liftVar) (Δ,x:P
4040
cases hb
4141
case here =>
4242
apply HasType.var
43-
simp [<-Ty.subst_succVar_comm_base]
43+
simp only [<-Ty.subst_succVar_comm_base]
4444
constructor
4545
case there_var hb0 =>
4646
have h0 := ρ.var _ _ hb0
47-
simp [<-Ty.subst_succVar_comm_base]
47+
simp only [<-Ty.subst_succVar_comm_base]
4848
apply h0.rebind Rebind.succVar
4949
tvar := fun X S hb => by
5050
cases hb
5151
case there_var hb0 =>
5252
have h0 := ρ.tvar _ _ hb0
53-
simp [<-Ty.subst_succVar_comm_base]
53+
simp only [<-Ty.subst_succVar_comm_base]
5454
apply h0.rebind Rebind.succVar
5555

5656
/-- Extends a retyping morphism to contexts with an additional type variable. -/
@@ -59,7 +59,7 @@ def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ,
5959
cases hb
6060
case there_tvar hb0 =>
6161
have h0 := ρ.var _ _ hb0
62-
simp [<-Ty.subst_succTVar_comm_base]
62+
simp only [<-Ty.subst_succTVar_comm_base]
6363
apply h0.rebind Rebind.succTVar
6464
tvar := fun X S hb => by
6565
cases hb
@@ -68,7 +68,7 @@ def Retype.liftTVar (ρ : Retype Γ σ Δ) : Retype (Γ,X<:P) (σ.liftTVar) (Δ,
6868
grind [Ty.subst_succTVar_comm_base]
6969
case there_tvar hb0 =>
7070
have h0 := ρ.tvar _ _ hb0
71-
simp [<-Ty.subst_succTVar_comm_base]
71+
simp only [<-Ty.subst_succTVar_comm_base]
7272
apply h0.rebind Rebind.succTVar
7373

7474
/-- Creates a retyping morphism that substitutes an expression for the newest term variable. -/
@@ -93,7 +93,7 @@ def Retype.narrow_tvar
9393
case here =>
9494
apply Subtyp.trans
9595
{ apply Subtyp.tvar; constructor }
96-
{ simp [Ty.subst_id]; apply hs.rebind Rebind.succTVar }
96+
{ simp only [Ty.subst_id]; apply hs.rebind Rebind.succTVar }
9797
case there_tvar hb0 => apply Subtyp.tvar; grind [Ty.subst_id]
9898

9999
/-- Creates a retyping morphism that substitutes a type for the newest type variable. -/

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/RetypeTheory/TypeSystem.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,4 +32,4 @@ theorem HasType.retype {σ : Subst s1 s2}
3232
case abs ih => apply HasType.abs; simpa [Ty.subst_succVar_comm_base] using ih ρ.liftVar
3333
case tabs ih => apply HasType.tabs; apply ih ρ.liftTVar
3434
case app ih1 ih2 => apply HasType.app <;> aesop
35-
case tapp ih => simp [Ty.open_tvar_subst_comm]; apply HasType.tapp; aesop
35+
case tapp ih => simp only [Ty.open_tvar_subst_comm]; apply HasType.tapp; aesop

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/Substitution/Properties.lean‎

Lines changed: 38 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -45,17 +45,17 @@ theorem Ty.tvar_subst_succVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) :
4545
case push_var s0 ih =>
4646
cases X
4747
case there_var X0 =>
48-
simp [Subst.lift, Ty.subst]
49-
conv => lhs; simp [Subst.liftVar]
50-
conv => rhs; simp [Subst.tvar_there_var_liftVar]
51-
simp [Rename.lift, <-Ty.rename_succVar_comm]
48+
simp only [Subst.lift, Ty.subst]
49+
conv => lhs; simp only [Subst.liftVar]
50+
conv => rhs; simp only [Subst.tvar_there_var_liftVar]
51+
simp only [Rename.lift, <-Ty.rename_succVar_comm]
5252
congr; exact (ih (X:=X0))
5353
case push_tvar s0 ih =>
5454
cases X <;> try rfl
5555
case there_tvar X0 =>
56-
conv => lhs; simp [Subst.lift, Ty.subst]
57-
conv => lhs; simp [Subst.liftTVar, Rename.lift]
58-
simp [<-Ty.rename_succTVar_comm]
56+
conv => lhs; simp only [Subst.lift, Ty.subst]
57+
conv => lhs; simp only [Subst.liftTVar, Rename.lift]
58+
simp only [<-Ty.rename_succTVar_comm]
5959
congr; exact (ih (X:=X0))
6060

6161
/-- Proves that substitution commutes with type variable weakening for type variables. -/
@@ -67,16 +67,16 @@ theorem Ty.tvar_subst_succTVar_comm {X : TVar (s1 ++ s0)} (σ : Subst s1 s2) :
6767
case push_var s0 ih =>
6868
cases X
6969
case there_var X0 =>
70-
conv => lhs; simp [Subst.lift, Ty.subst]
71-
conv => lhs; simp [Subst.liftVar, Rename.lift]
72-
simp [<-Ty.rename_succVar_comm]
70+
conv => lhs; simp only [Subst.lift, Ty.subst]
71+
conv => lhs; simp only [Subst.liftVar, Rename.lift]
72+
simp only [<-Ty.rename_succVar_comm]
7373
congr; exact (ih (X:=X0))
7474
case push_tvar s0 ih =>
7575
cases X <;> try rfl
7676
case there_tvar X0 =>
77-
conv => lhs; simp [Subst.lift, Ty.subst]
78-
conv => lhs; simp [Subst.liftTVar, Rename.lift]
79-
simp [<-Ty.rename_succTVar_comm]
77+
conv => lhs; simp only [Subst.lift, Ty.subst]
78+
conv => lhs; simp only [Subst.liftTVar, Rename.lift]
79+
simp only [<-Ty.rename_succTVar_comm]
8080
congr; exact (ih (X:=X0))
8181

8282
/-- Proves that substitution commutes with term variable weakening for types. -/
@@ -141,16 +141,16 @@ theorem Exp.var_subst_succTVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) :
141141
case push_var s0 ih =>
142142
cases x <;> try rfl
143143
case there_var x0 =>
144-
conv => lhs; simp [Subst.lift, Exp.subst]
145-
conv => lhs; simp [Subst.liftVar, Rename.lift]
146-
simp [<-Exp.rename_succVar_comm]
144+
conv => lhs; simp only [Subst.lift, Exp.subst]
145+
conv => lhs; simp only [Subst.liftVar, Rename.lift]
146+
simp only [<-Exp.rename_succVar_comm]
147147
congr; exact (ih (x:=x0))
148148
case push_tvar s0 ih =>
149149
cases x
150150
case there_tvar x0 =>
151-
conv => lhs; simp [Subst.liftVar, Subst.lift, Rename.lift]
152-
conv => lhs; simp [Exp.subst, Subst.liftTVar]
153-
simp [<-Exp.rename_succTVar_comm]
151+
conv => lhs; simp only [Subst.liftVar, Subst.lift, Rename.lift]
152+
conv => lhs; simp only [Exp.subst, Subst.liftTVar]
153+
simp only [<-Exp.rename_succTVar_comm]
154154
congr; exact (ih (x:=x0))
155155

156156
/-- Proves that substitution commutes with term variable weakening for variables. -/
@@ -161,14 +161,14 @@ theorem Exp.var_subst_succVar_comm {x : Var (s1 ++ s0)} (σ : Subst s1 s2) :
161161
case push_var s0 ih =>
162162
cases x <;> try rfl
163163
case there_var x0 =>
164-
conv => lhs; simp [Subst.lift, Exp.subst, Subst.liftVar, Rename.lift]
165-
simp [<-Exp.rename_succVar_comm]
164+
conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftVar, Rename.lift]
165+
simp only [<-Exp.rename_succVar_comm]
166166
congr; exact (ih (x:=x0))
167167
case push_tvar s0 ih =>
168168
cases x
169169
case there_tvar x0 =>
170-
conv => lhs; simp [Subst.lift, Exp.subst, Subst.liftTVar, Rename.lift]
171-
simp [<-Exp.rename_succTVar_comm]
170+
conv => lhs; simp only [Subst.lift, Exp.subst, Subst.liftTVar, Rename.lift]
171+
simp only [<-Exp.rename_succTVar_comm]
172172
congr; exact (ih (x:=x0))
173173

174174
/-- Proves that substitution commutes with type variable weakening for expressions. -/
@@ -180,11 +180,11 @@ theorem Exp.subst_succTVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) :
180180
| .abs A t =>
181181
have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ)
182182
have ih2 := Exp.subst_succTVar_comm (s0:=s0,x) (e:=t) (σ:=σ)
183-
simp [Exp.subst, Exp.rename, ih1]; congr
183+
simp only [Exp.subst, Exp.rename, ih1]; congr
184184
| .tabs A t =>
185185
have ih1 := Ty.subst_succTVar_comm (T:=A) (σ:=σ)
186186
have ih2 := Exp.subst_succTVar_comm (s0:=s0,X) (e:=t) (σ:=σ)
187-
simp [Exp.subst, Exp.rename, ih1]; congr
187+
simp only [Exp.subst, Exp.rename, ih1]; congr
188188
| .app t1 t2 =>
189189
have ih1 := Exp.subst_succTVar_comm (e:=t1) (σ:=σ)
190190
have ih2 := Exp.subst_succTVar_comm (e:=t2) (σ:=σ)
@@ -203,11 +203,11 @@ theorem Exp.subst_succVar_comm {e : Exp (s1 ++ s0)} (σ : Subst s1 s2) :
203203
| .abs A t =>
204204
have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ)
205205
have ih2 := Exp.subst_succVar_comm (s0:=s0,x) (e:=t) (σ:=σ)
206-
simp [Exp.subst, Exp.rename, ih1]; congr
206+
simp only [Exp.subst, Exp.rename, ih1]; congr
207207
| .tabs A t =>
208208
have ih1 := Ty.subst_succVar_comm (T:=A) (σ:=σ)
209209
have ih2 := Exp.subst_succVar_comm (s0:=s0,X) (e:=t) (σ:=σ)
210-
simp [Exp.subst, Exp.rename, ih1]; congr
210+
simp only [Exp.subst, Exp.rename, ih1]; congr
211211
| .app t1 t2 =>
212212
have ih1 := Exp.subst_succVar_comm (e:=t1) (σ:=σ)
213213
have ih2 := Exp.subst_succVar_comm (e:=t2) (σ:=σ)
@@ -257,7 +257,7 @@ theorem Subst.liftVar_comp {σ1 : Subst s1 s2} {σ2 : Subst s2 s3} :
257257
theorem Ty.subst_comp {T : Ty s1} (σ1 : Subst s1 s2) (σ2 : Subst s2 s3) :
258258
(T.subst σ1).subst σ2 = T.subst (σ1.comp σ2) := by
259259
induction T generalizing s2 s3 <;> try (solve | rfl)
260-
all_goals simp [Ty.subst, Subst.liftTVar_comp]; grind
260+
all_goals simp only [Ty.subst, Subst.liftTVar_comp]; grind
261261

262262
/-- **Fundamental associativity law for substitution composition on expressions**:
263263
Sequential application of substitutions equals composition.
@@ -309,22 +309,23 @@ theorem Subst.id_liftTVar :
309309
categorical structure with identity morphisms. -/
310310
theorem Ty.subst_id {T : Ty s} : T.subst Subst.id = T := by
311311
induction T <;> try (solve | rfl)
312-
all_goals (simp [Ty.subst, Subst.id_liftTVar]; grind)
312+
all_goals (simp only [Ty.subst, Subst.id_liftTVar]; grind)
313313

314314
/-- **Identity law for expressions**: The identity substitution acts as neutral element.
315315
This extends the identity property to expressions, completing the algebraic
316316
structure of the substitution category. -/
317317
theorem Exp.subst_id {e : Exp s} : e.subst Subst.id = e := by
318318
induction e <;> try (solve | rfl)
319-
all_goals (simp [Exp.subst, Ty.subst_id, Subst.id_liftVar, Subst.id_liftTVar]; grind)
319+
all_goals (simp only [Exp.subst, Ty.subst_id, Subst.id_liftVar, Subst.id_liftTVar]; grind)
320320

321321
/-- Proves that opening a type variable commutes with renaming for substitutions. -/
322322
theorem Subst.open_tvar_rename_comm {T : Ty s} {f : Rename s s'} :
323323
(Subst.open_tvar T).comp (f.asSubst)
324324
= f.liftTVar.asSubst.comp (Subst.open_tvar (T.rename f)) := by
325325
apply Subst.funext
326326
case var => intro x; cases x; rfl
327-
case tvar => intro X; cases X <;> try (solve | rfl | simp [Subst.comp, Ty.subst_asSubst]; rfl)
327+
case tvar =>
328+
intro X; cases X <;> try (solve | rfl | simp only [Subst.comp, Ty.subst_asSubst]; rfl)
328329

329330
/-- Proves that opening a type variable commutes with renaming for types. -/
330331
theorem Ty.open_tvar_rename_comm {T : Ty (s,X)} {U : Ty s} {f : Rename s s'} :
@@ -374,15 +375,15 @@ theorem Subst.open_tvar_subst_comm {T : Ty s} {σ : Subst s s'} :
374375
apply Subst.funext
375376
case var =>
376377
intro x; cases x
377-
conv => lhs; simp [Subst.comp, Subst.open_tvar]
378-
conv => rhs; simp [Subst.comp, Subst.liftTVar]
379-
simp [Exp.rename_succTVar_open_tvar]; rfl
378+
conv => lhs; simp only [Subst.comp, Subst.open_tvar]
379+
conv => rhs; simp only [Subst.comp, Subst.liftTVar]
380+
simp only [Exp.rename_succTVar_open_tvar]; rfl
380381
case tvar =>
381382
intro X; cases X <;> try rfl
382383
case there_tvar X0 =>
383-
conv => lhs; simp [Subst.comp, Subst.open_tvar]
384-
conv => rhs; simp [Subst.comp, Subst.liftTVar]
385-
simp [Ty.rename_succTVar_open_tvar]; rfl
384+
conv => lhs; simp only [Subst.comp, Subst.open_tvar]
385+
conv => rhs; simp only [Subst.comp, Subst.liftTVar]
386+
simp only [Ty.rename_succTVar_open_tvar]; rfl
386387

387388
/-- Proves that opening a type variable commutes with substitution for types. -/
388389
theorem Ty.open_tvar_subst_comm {T : Ty (s,X)} {U : Ty s} {σ : Subst s s'} :

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/Syntax/Core.lean‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -74,25 +74,26 @@ def Exp.rename : Exp s1 -> Rename s1 s2 -> Exp s2
7474

7575
/-- Renaming with the identity renaming leaves a type unchanged. -/
7676
theorem Ty.rename_id {T : Ty s} : T.rename Rename.id = T := by
77-
induction T <;> try (solve | rfl | simp [Ty.rename]; grind)
77+
induction T <;> try (solve | rfl | simp only [Ty.rename, Rename.id_liftTVar_eq_id]; grind)
7878

7979
/-- Renaming with the identity renaming leaves an expression unchanged. -/
8080
theorem Exp.rename_id {e : Exp s} : e.rename Rename.id = e := by
81-
induction e <;> try (solve | rfl | simp [Exp.rename, Ty.rename_id]; grind)
81+
induction e <;> try (solve | rfl |
82+
simp only [Exp.rename, Ty.rename_id, Rename.id_liftVar_eq_id, Rename.id_liftTVar_eq_id]; grind)
8283

8384
/-- Composition of renamings: renaming by f₁ then f₂ equals renaming by their composition. -/
8485
theorem Ty.rename_comp {T : Ty s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} :
8586
(T.rename f1).rename f2 = T.rename (f1.comp f2) := by
8687
induction T generalizing s2 s3 <;>
87-
try (solve | rfl | simp [Ty.rename, Rename.comp_liftTVar]; grind)
88+
try (solve | rfl | simp only [Ty.rename, Rename.comp_liftTVar]; grind)
8889

8990
/-- Composition of renamings: renaming by f₁ then f₂ equals renaming by their composition. -/
9091
theorem Exp.rename_comp {e : Exp s1} {f1 : Rename s1 s2} {f2 : Rename s2 s3} :
9192
(e.rename f1).rename f2 = e.rename (f1.comp f2) := by
9293
induction e generalizing s2 s3 <;>
9394
try (solve | rfl)
9495
all_goals
95-
simp [Exp.rename, Ty.rename_comp, Rename.comp_liftVar, Rename.comp_liftTVar]; grind
96+
simp only [Exp.rename, Ty.rename_comp, Rename.comp_liftVar, Rename.comp_liftTVar]; grind
9697

9798
/-- Commutativity law for term variable weakening and general renamings. -/
9899
theorem Ty.rename_succVar_comm {T : Ty s} :

‎Cslib/Computability/LambdaCalculus/WellScoped/FSub/TypeSoundness/Preservation.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ theorem preservation
4444
have ⟨U0, h1, h2, h3⟩ := HasType.abs_inv ht1
4545
have ht2' := HasType.sub h2 ht2
4646
have h1' := h1.retype (Retype.open_var ht2')
47-
simp [Ty.rename_succVar_open_var] at h1'
47+
simp only [Ty.rename_succVar_open_var] at h1'
4848
apply HasType.sub _ h1'
4949
apply Subtyp.trans h3 hs0
5050
case red_tapp_fun ih =>

0 commit comments

Comments
 (0)