chore: cleanup of Cslib.Languages.LambdaCalculus.LocallyNameless.* (#250)

With the somewhat recent change to allow passing arbitrary expressions
to `grind` and other improvements, some cleanup of locally nameless
lambda calculus is possible.

Author: chenson2018

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

@@ -87,7 +87,7 @@ lemma openRec_neq_eq {σ τ γ : Ty Var} (neq : X ≠ Y) (h : σ⟦Y ↝ τ⟧
 /-- A locally closed type is unchanged by opening. -/
 lemma openRec_lc {σ τ : Ty Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ᵞ := by
   induction lc generalizing X with
-  | all => have := fresh_exists <| free_union Var; grind [openRec_neq_eq]
+  | all => grind [fresh_exists <| free_union Var, openRec_neq_eq]
   | _ => grind
 
 omit [HasFresh Var] in
@@ -102,8 +102,7 @@ lemma subst_fresh (nmem : X ∉ γ.fv) (δ : Ty Var) : γ = γ[X := δ] := by
 /-- Substitution of a locally closed type distributes with opening. -/
 lemma openRec_subst (Y : ℕ) (σ τ : Ty Var) (lc : δ.LC) (X : Var) :
     (σ⟦Y ↝ τ⟧ᵞ)[X := δ] = σ[X := δ]⟦Y ↝ τ[X := δ]⟧ᵞ := by
-  induction σ generalizing Y
-  all_goals grind [openRec_lc]
+  induction σ generalizing Y <;> grind [openRec_lc]
 
 /-- Specialize `Ty.openRec_subst` to the first opening. -/
 lemma open_subst (σ τ : Ty Var) (lc : δ.LC) (X : Var) : (σ ^ᵞ τ)[X := δ] = σ[X := δ] ^ᵞ τ[X := δ]
@@ -125,9 +124,9 @@ lemma open_subst_intro (δ : Ty Var) (nmem : X ∉ γ.fv) : γ ^ᵞ δ = (γ ^
   openRec_subst_intro _ _ nmem
 
 lemma subst_lc (σ_lc : σ.LC) (τ_lc : τ.LC) (X : Var) : σ[X := τ].LC := by
-  induction σ_lc
-  case all => apply LC.all (free_union Var) <;> grind [openRec_subst]
-  all_goals grind [openRec_subst]
+  induction σ_lc with
+  | all => grind [LC.all (free_union Var), openRec_subst]
+  | _ => grind [openRec_subst]
 
 omit [HasFresh Var] in
 lemma nmem_fv_openRec (nmem : X ∉ (σ⟦k ↝ γ⟧ᵞ).fv) : X ∉ σ.fv := by
@@ -226,11 +225,10 @@ lemma openRec_tm_ty_eq (eq : t⟦x ↝ s⟧ᵗᵗ = t⟦x ↝ s⟧ᵗᵗ⟦y ↝
 /-- A locally closed term is unchanged by type opening. -/
 @[scoped grind =_]
 lemma openRec_ty_lc {t : Term Var} (lc : t.LC) : t = t⟦X ↝ σ⟧ᵗᵞ := by
-  induction lc generalizing X
-  case let' | case | tabs | abs =>
-    have := fresh_exists <| free_union Var
-    congr <;> grind [Ty.openRec_lc, openRec_ty_neq_eq]
-  all_goals grind [Ty.openRec_lc]
+  induction lc generalizing X with
+  | let' | case | tabs | abs =>
+    grind [fresh_exists <| free_union Var, Ty.openRec_lc, openRec_ty_neq_eq]
+  | _ => grind [Ty.openRec_lc]
 
 /-- Substitution of a type within a term. -/
 @[scoped grind =]
@@ -318,11 +316,10 @@ variable [HasFresh Var]
 /-- A locally closed term is unchanged by term opening. -/
 @[scoped grind =_]
 lemma openRec_tm_lc (lc : t.LC) : t = t⟦x ↝ s⟧ᵗᵗ := by
-  induction lc generalizing x
-  case let' | case | tabs | abs =>
-    have := fresh_exists <| free_union Var
-    congr <;> grind [openRec_tm_neq_eq, openRec_ty_tm_eq]
-  all_goals grind
+  induction lc generalizing x with
+  | let' | case | tabs | abs =>
+    grind [fresh_exists <| free_union Var, openRec_tm_neq_eq, openRec_ty_tm_eq]
+  | _ => grind
 
 variable {t s : Term Var} {δ : Ty Var} {x : Var}
 

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

@@ -48,36 +48,27 @@ variable [DecidableEq Var]
 @[scoped grind _=_]
 lemma body_let : (let' t₁ t₂).LC ↔ t₁.LC ∧ t₂.body := by
   constructor <;> intro h <;> cases h
-  case mp.let' L _ _ =>
-    split_ands
-    · grind
-    · exists L
+  case mp.let' L t₁_lc h => exact ⟨t₁_lc, L, h⟩
   case mpr.intro body =>
     obtain ⟨_, _⟩ := body
-    apply LC.let' (free_union Var) <;> grind
+    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 =>
-    split_ands
-    · grind
-    · exists L
-    · exists L
+  case mp => cases h with | case L t₁_lc h₂ h₃ => exact ⟨t₁_lc, ⟨L, h₂⟩, ⟨L, h₃⟩⟩
   case mpr =>
     obtain ⟨_, ⟨_, _⟩, ⟨_, _⟩⟩ := h
-    apply LC.case (free_union Var) <;> grind
+    grind [LC.case <| free_union Var]
 
 variable [HasFresh Var]
 
 /-- Opening a body preserves local closure. -/
 @[scoped grind <=]
 lemma open_tm_body (body : t₁.body) (lc : t₂.LC) : (t₁ ^ᵗᵗ t₂).LC := by
   cases body
-  have := fresh_exists <| free_union [fv_tm] Var
-  grind [subst_tm_lc, open_tm_subst_tm_intro]
+  grind [fresh_exists <| free_union [fv_tm] Var, subst_tm_lc, open_tm_subst_tm_intro]
 
 end
 
@@ -111,8 +102,7 @@ inductive Red : Term Var → Term Var → Prop
 
 @[grind _=_]
 lemma rs_eq {t t' : Term Var} : t ⭢βᵛ t' ↔ Red t t' := by
-  have : (@rs Var).Red = Red := by rfl
-  simp_all
+  rfl
 
 variable [HasFresh Var] [DecidableEq Var] in
 /-- Terms of a reduction are locally closed. -/
@@ -122,8 +112,9 @@ lemma Red.lc {t t' : Term Var} (red : t ⭢βᵛ t') : t.LC ∧ t'.LC := by
     split_ands
     · grind
     · cases lc
-      have := fresh_exists <| free_union [fv_tm, fv_ty] Var
-      grind [subst_tm_lc, subst_ty_lc, open_tm_subst_tm_intro, open_ty_subst_ty_intro]
+      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
 
 end Term

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

@@ -42,36 +42,32 @@ lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing
     case abs der _ _ =>
       have sub : Sub Γ (σ.arrow τ) (σ.arrow τ) := by grind [Sub.refl]
       have ⟨_, _, ⟨_, _⟩⟩ := der.abs_inv sub
-      have ⟨_, _⟩ := fresh_exists <| free_union [fv_tm] Var
-      grind [open_tm_subst_tm_intro, subst_tm, Sub.weaken]
+      grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm, Sub.weaken]
   case tapp Γ _ σ τ σ' _ _ _ =>
     cases step
     case tabs der _ _ =>
       have sub : Sub Γ (σ.all τ) (σ.all τ) := by grind [Sub.refl]
       have ⟨_, _, ⟨_, _⟩⟩ := der.tabs_inv sub
       have ⟨X, _⟩ := fresh_exists <| free_union [Ty.fv, fv_ty] Var
-      have : Γ = (Context.map_val (·[X:=σ']) []) ++ Γ := by simp
+      have : Γ = (Context.map_val (·[X:=σ']) []) ++ Γ := by grind
       rw [open_ty_subst_ty_intro (X := X), open_subst_intro (X := X)] <;> grind [subst_ty]
     case tapp => grind
   case let' Γ _ _ _ _ L der _ ih₁ _ =>
     cases step
     case let_bind red₁ _ => apply Typing.let' L (ih₁ red₁); grind
     case let_body =>
-      have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var
-      grind [open_tm_subst_tm_intro, subst_tm]
+      grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm]
   case case Γ _ σ τ _ _ _ L _ _ _ ih₁ _ _ =>
     have sub : Sub Γ (σ.sum τ) (σ.sum τ) := by grind [Sub.refl]
     have : Γ = [] ++ Γ := by rfl
     cases step
     case «case» red₁ _ _ => apply Typing.case L (ih₁ red₁) <;> grind
     case case_inl der _ _ =>
       have ⟨_, ⟨_, _⟩⟩ := der.inl_inv sub
-      have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var
-      grind [open_tm_subst_tm_intro, subst_tm]
+      grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm]
     case case_inr der _ _ =>
       have ⟨_, ⟨_, _⟩⟩ := der.inr_inv sub
-      have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var
-      grind [open_tm_subst_tm_intro, subst_tm]
+      grind [fresh_exists <| free_union [fv_tm] Var, open_tm_subst_tm_intro, subst_tm]
   all_goals grind [cases Red]
 
 /-- Any typable term either has a reduction step or is a value. -/

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

@@ -55,15 +55,13 @@ variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var}
 @[grind →]
 lemma wf (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.Wf Γ ∧ σ'.Wf Γ := by
   induction sub with
-  | all =>
-    refine ⟨by grind, ?_, ?_⟩ <;>
-    apply Wf.all (free_union Var) <;> grind [Wf.narrow_cons, cases Env.Wf, cases LC]
+  | all => grind [Wf.all (free_union Var), Wf.narrow_cons, cases Env.Wf, cases LC]
   | _ => grind
 
 /-- Subtypes are reflexive when well-formed. -/
 lemma refl (wf_Γ : Γ.Wf) (wf_σ : σ.Wf Γ) : Sub Γ σ σ := by
   induction wf_σ with
-  | all => apply all (free_union [Context.dom] Var) <;> grind
+  | all => grind [all (free_union [Context.dom] Var)]
   | _ => grind
 
 /-- Weakening of subtypes. -/
@@ -125,7 +123,7 @@ lemma trans : Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ := by
       cases eq
       cases sub₂
       case refl.top Γ σ'' τ'' _ _ _ _ _ _ _ =>
-        have : Sub Γ (σ''.all τ'') (σ'.all τ') := by apply all (free_union Var) <;> grind
+        have : Sub Γ (σ''.all τ'') (σ'.all τ') := by grind [all <| free_union Var]
         grind
       case refl.all Γ _ _ _ _ _ σ _ _ _ _ _ _ =>
         apply all (free_union Var)
@@ -141,7 +139,7 @@ instance (Γ : Env Var) : Trans (Sub Γ) (Sub Γ) (Sub Γ) :=
 /-- Narrowing of subtypes. -/
 lemma narrow (sub_δ : Sub Δ δ δ') (sub_narrow : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) :
     Sub (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) σ τ := by
-  apply narrow_aux (δ := δ') <;> grind
+  grind [narrow_aux (δ := δ')]
 
 variable [HasFresh Var] in
 /-- Subtyping of substitutions. -/
@@ -164,9 +162,9 @@ lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub
 /-- Strengthening of subtypes. -/
 lemma strengthen (sub : Sub (Γ ++ ⟨X, Binding.ty δ⟩ :: Δ) σ τ) :  Sub (Γ ++ Δ) σ τ := by
   generalize eq : Γ ++ ⟨X, Binding.ty δ⟩ :: Δ = Θ at sub
-  induction sub generalizing Γ
-  case all => apply Sub.all (free_union Var) <;> grind
-  all_goals grind [to_ok, Wf.strengthen, Env.Wf.strengthen]
+  induction sub generalizing Γ with
+  | all => grind [Sub.all (free_union Var)]
+  | _ => grind [to_ok, Wf.strengthen, Env.Wf.strengthen]
 
 end Sub
 

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

@@ -65,12 +65,16 @@ attribute [grind .] Typing.var Typing.app Typing.tapp Typing.sub Typing.inl Typi
 /-- Typings have well-formed contexts and types. -/
 @[grind →]
 lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : Γ.Wf ∧ t.LC ∧ τ.Wf Γ := by
-  induction der <;> let L := free_union Var <;> have := fresh_exists L
-  case tabs => refine ⟨?_, LC.tabs L ?_ ?_, Ty.Wf.all L ?_ ?_⟩ <;> grind [cases Env.Wf]
-  case abs => refine ⟨?_, LC.abs L ?_ ?_, ?_⟩ <;> grind [Wf.strengthen, cases Env.Wf]
-  case let' => refine ⟨?_, LC.let' L ?_ ?_, ?_⟩ <;> grind [Ty.Wf.strengthen]
+  induction der <;> let L := free_union Var <;> have ⟨x, nmem⟩ := fresh_exists L
+  case tabs ih =>
+    cases (ih x (by grind)).left
+    grind [LC.tabs L, Ty.Wf.all L]
+  case abs ih =>
+    cases (ih x (by grind)).left
+    grind [LC.abs L, Wf.strengthen]
+  case let' => grind [LC.let' L, Ty.Wf.strengthen]
   case case => refine ⟨?_, LC.case L ?_ ?_ ?_, ?_⟩ <;> grind [Ty.Wf.strengthen]
-  all_goals grind [of_bind_ty, open_lc, cases Env.Wf, cases Ty.Wf]
+  all_goals grind [of_bind_ty, open_lc, cases Ty.Wf]
 
 /-- Weakening of typings. -/
 lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :
@@ -89,8 +93,7 @@ lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) :
     Typing (Γ ++ Δ) t τ := by
   have eq : Δ = [] ++ Δ := by rfl
   rw [eq] at der
-  have := Typing.weaken der wf
-  grind
+  grind [Typing.weaken der wf]
 
 /-- Narrowing of typings. -/
 lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) :
@@ -121,15 +124,9 @@ lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typi
       -/
       grind [→ List.mem_dlookup, weaken_head, Env.Wf.strengthen, -append_assoc]
     · grind [Env.Wf.strengthen, => List.perm_dlookup]
-  case abs =>
-    apply abs (free_union Var)
-    grind [open_tm_subst_tm_var]
-  case tabs =>
-    apply tabs (free_union Var)
-    grind [open_ty_subst_tm_var]
-  case let' der _ =>
-    apply let' (free_union Var) (der eq)
-    grind [open_tm_subst_tm_var]
+  case abs => grind [abs (free_union Var), open_tm_subst_tm_var]
+  case tabs => grind [tabs (free_union Var), open_ty_subst_tm_var]
+  case let' der _ => grind [let' (free_union Var) (der eq), open_tm_subst_tm_var]
   case case der _ _ =>
     apply case (free_union Var) (der eq) <;> grind [open_tm_subst_tm_var]
   all_goals grind [Env.Wf.strengthen, Ty.Wf.strengthen, Sub.strengthen]
@@ -141,16 +138,10 @@ lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub :
   induction der generalizing Γ X
   case var σ _ X' _ mem =>
     have := map_subst_nmem Δ X δ
-    have : Γ ++ ⟨X, .sub δ'⟩ :: Δ ~ ⟨X, .sub δ'⟩ :: (Γ ++ Δ) := perm_middle
-    have : .ty σ ∈ dlookup X' (⟨X, .sub δ'⟩ :: (Γ ++ Δ)) := by grind [perm_dlookup]
     have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var))
     grind [Env.Wf.map_subst, → notMem_keys_of_nodupKeys_cons]
-  case abs =>
-    apply abs (free_union [Ty.fv] Var)
-    grind [Ty.subst_fresh, open_tm_subst_ty_var]
-  case tabs =>
-    apply tabs (free_union Var)
-    grind [open_ty_subst_ty_var, open_subst_var]
+  case abs => grind [abs (free_union [Ty.fv] Var), Ty.subst_fresh, open_tm_subst_ty_var]
+  case tabs => grind [tabs (free_union Var), open_ty_subst_ty_var, open_subst_var]
   case let' der _ =>
     apply let' (free_union Var) (der eq)
     grind [open_tm_subst_ty_var]

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

@@ -68,13 +68,13 @@ open scoped Env.Wf
 @[grind →]
 theorem lc (wf : σ.Wf Γ) : σ.LC := by
   induction wf with
-  | all => apply LC.all (free_union Var) <;> grind
+  | all => grind [LC.all (free_union Var)]
   | _ => grind
 
 /-- A type remains well-formed under context permutation. -/
 theorem perm_env (wf : σ.Wf Γ) (perm : Γ ~ Δ) (ok_Γ : Γ✓) (ok_Δ : Δ✓) : σ.Wf Δ := by
   induction wf generalizing Δ with
-  | all => apply all (free_union [dom] Var) <;> grind [Perm.cons, nodupKeys_cons]
+  | all => grind [all <| free_union [dom] Var, Perm.cons, nodupKeys_cons]
   | _ => grind [perm_dlookup]
 
 /-- A type remains well-formed under context weakening (in the middle). -/
@@ -109,14 +109,13 @@ lemma narrow (wf : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (ok : (Γ ++ ⟨
 
 lemma narrow_cons (wf : σ.Wf (⟨X, Binding.sub τ⟩ :: Δ)) (ok : (⟨X, Binding.sub τ'⟩ :: Δ)✓) :
     σ.Wf (⟨X, Binding.sub τ'⟩ :: Δ) := by
-  rw [←List.nil_append (⟨X, sub τ'⟩ :: Δ)]
-  grind [narrow]
+  grind [List.nil_append (⟨X, sub τ'⟩ :: Δ), narrow]
 
 /-- A type remains well-formed under context strengthening. -/
 lemma strengthen (wf : σ.Wf (Γ ++ ⟨X, Binding.ty τ⟩ :: Δ)) : σ.Wf (Γ ++ Δ) := by
   generalize eq : Γ ++ ⟨X, Binding.ty τ⟩ :: Δ = Θ at wf
   induction wf generalizing Γ with
-  | all => apply all (free_union [Context.dom] Var) <;> grind
+  | all => grind [all <| free_union [Context.dom] Var]
   | _ => grind
 
 variable [HasFresh Var] in
@@ -125,13 +124,9 @@ lemma map_subst (wf_σ : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' :
     (ok : (Γ.map_val (·[X:=τ']) ++ Δ)✓) : σ[X:=τ'].Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by
   have := @map_val_mem Var (Binding Var)
   generalize eq : Γ ++ ⟨X, Binding.sub τ⟩ :: Δ = Θ at wf_σ
-  induction wf_σ generalizing Γ τ'
-  case all γ _ _ _ _ _ _ =>
-    subst eq
-    apply all (free_union [dom] Var)
-    · grind
-    · grind [open_subst_var]
-  all_goals grind [weaken_head]
+  induction wf_σ generalizing Γ τ' with
+  | all => apply all (free_union [dom] Var) <;> grind [open_subst_var]
+  | _ => grind [weaken_head]
 
 variable [HasFresh Var] in
 /-- A type remains well-formed under opening (to a well-formed type). -/
@@ -159,7 +154,7 @@ variable [HasFresh Var] in
 /-- A variable not appearing in a context does not appear in its well-formed types. -/
 lemma nmem_fv {σ : Ty Var} (wf : σ.Wf Γ) (nmem : X ∉ Γ.dom) : X ∉ σ.fv := by
   induction wf with
-  | all => have := fresh_exists <| free_union [dom] Var; grind [nmem_fv_open, openRec_lc]
+  | all => grind [fresh_exists <| free_union [dom] Var, nmem_fv_open, openRec_lc]
   | _ => grind [dlookup_isSome]
 
 end Ty.Wf