perf: PR for radar testing of Fsub

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean

@@ -45,7 +45,6 @@ variable {t₁ t₂ t₃ : Term Var}
 variable [DecidableEq Var]
 
 /-- Locally closed let bindings have a locally closed body. -/
-@[scoped grind _=_]
 lemma body_let : (let' t₁ t₂).LC ↔ t₁.LC ∧ t₂.body := by
   constructor <;> intro h <;> cases h
   case mp.let' L t₁_lc h => exact ⟨t₁_lc, L, h⟩
@@ -54,7 +53,6 @@ lemma body_let : (let' t₁ t₂).LC ↔ t₁.LC ∧ t₂.body := by
     grind [LC.let' <| free_union Var]
 
 /-- Locally closed case bindings have a locally closed bodies. -/
-@[scoped grind _=_]
 lemma body_case : (case t₁ t₂ t₃).LC ↔ t₁.LC ∧ t₂.body ∧ t₃.body := by
   constructor <;> intro h
   case mp => cases h with | case L t₁_lc h₂ h₃ => exact ⟨t₁_lc, ⟨L, h₂⟩, ⟨L, h₃⟩⟩
@@ -115,7 +113,7 @@ lemma Red.lc {t t' : Term Var} (red : t ⭢βᵛ t') : t.LC ∧ t'.LC := by
       grind [
         fresh_exists <| free_union [fv_tm, fv_ty] Var, subst_tm_lc,
         subst_ty_lc, open_tm_subst_tm_intro, open_ty_subst_ty_intro]
-  all_goals grind
+  all_goals grind [body_let, body_case]
 
 end Term
 

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean

@@ -68,7 +68,7 @@ lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing
     case case_inr der _ _ =>
       have ⟨_, ⟨_, _⟩⟩ := der.inr_inv sub
       grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm]
-  all_goals grind [cases Red]
+  all_goals grind
 
 /-- Any typable term either has a reduction step or is a value. -/
 lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' := by
@@ -110,11 +110,11 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t'
     cases ih der with
     | inl _ =>
         exists t₂ ^ᵗᵗ t₁
-        grind
+        grind [body_let]
     | inr red =>
         obtain ⟨t₁', _⟩ := red
         exists t₁'.let' t₂
-        grind
+        grind [body_let]
   case inl der _ ih =>
     cases (ih der) with
     | inl val => grind
@@ -136,20 +136,20 @@ lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t'
     cases ih der with
     | inl val =>
         have ⟨t₁, lr⟩ := der.canonical_form_sum val
-        cases lr <;> [exists t₂ ^ᵗᵗ t₁; exists t₃ ^ᵗᵗ t₁] <;> grind
+        cases lr <;> [exists t₂ ^ᵗᵗ t₁; exists t₃ ^ᵗᵗ t₁] <;> grind [body_case]
     | inr red =>
         obtain ⟨t₁', _⟩ := red
         exists t₁'.case t₂ t₃
-        grind
+        grind [body_case]
   case sub => grind
   case abs σ _ τ L _ _=>
     left
     constructor
-    apply LC.abs L <;> grind [cases Env.Wf, cases Term.LC]
+    apply LC.abs L <;> grind [cases Term.LC]
   case tabs L _ _=>
     left
     constructor
-    apply LC.tabs L <;> grind [cases Env.Wf, cases Term.LC]
+    apply LC.tabs L <;> grind [cases Term.LC]
 
 end LambdaCalculus.LocallyNameless.Fsub
 

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean

@@ -55,13 +55,13 @@ variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var}
 @[grind →]
 lemma wf (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.Wf Γ ∧ σ'.Wf Γ := by
   induction sub with
-  | all => grind [Wf.all (free_union Var), Wf.narrow_cons, cases Env.Wf, cases LC]
+  | all => grind [Wf.all (free_union Var), Wf.narrow_cons]
   | _ => grind
 
 /-- Subtypes are reflexive when well-formed. -/
 lemma refl (wf_Γ : Γ.Wf) (wf_σ : σ.Wf Γ) : Sub Γ σ σ := by
   induction wf_σ with
-  | all => grind [all (free_union [Context.dom] Var)]
+  | all => grind [all (free_union [Context.dom] Var), Env.Wf.sub, Env.Wf.ty]
   | _ => grind
 
 /-- Weakening of subtypes. -/
@@ -70,7 +70,7 @@ lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ
   induction sub generalizing Γ
   case all =>
     subst eq
-    apply all (free_union [Context.dom] Var) <;> grind
+    apply all (free_union [Context.dom] Var) <;> grind [Env.Wf.sub, Env.Wf.ty]
   all_goals grind [Ty.Wf.weaken, <= sublist_dlookup]
 
 lemma weaken_head (sub : Sub Δ σ σ') (wf : (Γ ++ Δ).Wf) : Sub (Γ ++ Δ) σ σ' := by
@@ -109,7 +109,7 @@ lemma trans : Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ := by
   case top => cases sub₁ <;> cases sub₂ <;> grind
   case var X =>
     generalize eq : fvar X = γ at sub₁
-    induction sub₁ <;> grind [cases Sub]
+    induction sub₁ <;> grind
   case arrow σ' τ' _ _ _ _ =>
     generalize eq : σ'.arrow τ' = γ at sub₁
     induction sub₁ <;> grind [cases Sub]

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean

@@ -85,8 +85,8 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :
   case' tabs => apply tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
   case' let' der _ => apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
   case' case der _ _ => apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
-  all_goals
-    grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, <= sublist_dlookup]
+  all_goals grind
+    [Env.Wf.sub, Env.Wf.ty, Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, <= sublist_dlookup]
 
 /-- Weakening of typings (at the front). -/
 lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) :

Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean

@@ -49,8 +49,6 @@ inductive Env.Wf : Env Var → Prop
   | sub : Wf Γ → τ.Wf Γ → X ∉ Γ.dom → Wf (⟨X, Binding.sub τ⟩ :: Γ)
   | ty : Wf Γ → τ.Wf Γ → x ∉ Γ.dom → Wf (⟨x, Binding.ty τ⟩ :: Γ)
 
-attribute [scoped grind! .] Env.Wf.sub Env.Wf.ty
-
 variable {Γ Δ Θ : Env Var} {σ τ τ' γ δ : Ty Var}
 
 open scoped Context in
@@ -167,11 +165,11 @@ open Context List Binding
 lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) :
     Env.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by
   induction Γ <;> cases wf_env <;>
-  grind [Ty.Wf.narrow, eq_nil_of_append_eq_nil, cases Env.Wf]
+  grind [Env.Wf.sub, Env.Wf.ty, Ty.Wf.narrow]
 
 /-- A context remains well-formed under strengthening. -/
 lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by
-  induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen]
+  induction Γ <;> cases wf <;> grind [Env.Wf.sub, Env.Wf.ty, Ty.Wf.strengthen]
 
 variable [HasFresh Var] in
 /-- A context remains well-formed under substitution (of a well-formed type). -/

CslibTests/GrindLint.lean

@@ -59,8 +59,6 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.arrow
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.sum
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.trans_tvar
-#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.body_case
-#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.body_let
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Term.open_tm_body
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.app
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.inl
@@ -69,8 +67,6 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Typing.tapp
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.para_subst
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.subst_intro
-#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.sub
-#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.ty
 
 #guard_msgs in
 #grind_lint check (min := 20) in Cslib