refactor: define FullBeta using Xi (#455)

I have tested this branch and can confirm that this refactor provides
the necessary for proving $\beta \eta$-confluence.

---------

Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

Author: m-ow

Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean

@@ -88,6 +88,7 @@ lemma weaken (der : Γ ⊢ t ∶ τ) (ok : (Γ ++ Δ)✓) : Γ ++ Δ ⊢ t ∶ 
 
 omit [DecidableEq Var] in
 /-- Typing derivations exist only for locally closed terms. -/
+@[scoped grind →]
 lemma lc (der : Γ ⊢ t ∶ τ) : t.LC := by
   induction der <;> constructor
   case abs ih => exact ih

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

@@ -67,9 +67,9 @@ set_option linter.unusedDecidableInType false in
 theorem preservation (der : Γ ⊢ t ∶ τ) (step : t ⭢βᶠ t') : Γ ⊢ t' ∶ τ := by
   induction der generalizing t' <;> cases step
   case abs.abs xs _ _ _ xs' _ => apply Typing.abs (free_union Var); grind
-  case app.beta der _ _ _ der_l _ _ =>
-    -- TODO: this is a regression from aesop, where `preservation_open` was a forward rule
-    cases der_l with | abs _ cofin => simp [preservation_open cofin der]
+  case app.base h der _ _ der_l =>
+    cases der_l
+    cases h with | abs _ cofin => exact preservation_open cofin der
   all_goals grind
 
 open scoped Term in
@@ -88,15 +88,14 @@ theorem progress {t : Term Var} {τ : Ty Base} (ht : [] ⊢ t ∶ τ) : t.Value
   case app Γ M σ τ N der_l der_r ih_l ih_r =>
     simp only [eq, forall_const] at *
     right
-    cases ih_l
+    cases ih_l with
     -- if the lhs is a value, beta reduce the application
-    next val =>
-      cases val
-      next M M_abs_lc => exact ⟨M ^ N, Term.FullBeta.beta M_abs_lc der_r.lc⟩
+    | inl val => cases val with | abs M _ => use M ^ N, by grind
     -- otherwise, propogate the step to the lhs of the application
-    next step =>
-      obtain ⟨M', stepM⟩ := step
-      exact ⟨M'.app N, Term.FullBeta.appR der_r.lc stepM⟩
+    | inr step =>
+      obtain ⟨M', _⟩ := step
+      use M'.app N
+      grind
 
 end FullBeta
 

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean

@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
 
 public section
 
@@ -32,28 +33,25 @@ variable {Var : Type u}
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
 /-- A single β-reduction step. -/
-@[reduction_sys "βᶠ"]
-inductive FullBeta : Term Var → Term Var → Prop
+@[scoped grind]
+inductive Beta : Term Var → Term Var → Prop
 /-- Reduce an application to a lambda term. -/
-| beta : LC (abs M)→ LC N → FullBeta (app (abs M) N) (M ^ N)
-/-- Left congruence rule for application. -/
-| appL: LC Z → FullBeta M N → FullBeta (app Z M) (app Z N)
-/-- Right congruence rule for application. -/
-| appR : LC Z → FullBeta M N → FullBeta (app M Z) (app N Z)
-/-- Congruence rule for lambda terms. -/
-| abs (xs : Finset Var) : (∀ x ∉ xs, FullBeta (M ^ fvar x) (N ^ fvar x)) → FullBeta (abs M) (abs N)
+| beta : LC (abs M)→ LC N → Beta (app (abs M) N) (M ^ N)
 
-namespace FullBeta
+/-- Full β-reduction. -/
+@[reduction_sys "βᶠ"]
+abbrev FullBeta : Term Var → Term Var → Prop := Xi Beta
 
-attribute [scoped grind .] appL appR
+namespace FullBeta
 
 variable {M M' N N' : Term Var}
 
 /-- The left side of a reduction is locally closed. -/
 @[scoped grind →]
 lemma step_lc_l (step : M ⭢βᶠ M') : LC M := by
-  induction step <;> constructor
-  all_goals assumption
+  induction step with
+  | abs => constructor; assumption
+  | _ => grind
 
 /-- Left congruence rule for application in multiple reduction. -/
 @[scoped grind ←]
@@ -81,8 +79,8 @@ lemma steps_lc_or_rfl {M M' : Term Var} (redex : M ↠βᶠ M') : (LC M ∧ LC M
 lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) :
     s [ x := t ] ⭢βᶠ s' [ x := t ] := by
   induction step with
-  | beta => grind [subst_open, beta]
-  | abs  => grind [abs <| free_union Var]
+  | base => grind [subst_open]
+  | abs  => grind [Xi.abs <| free_union Var]
   | _ => grind
 
 /-- Substitution respects a single reduction step of a free variable. -/
@@ -92,7 +90,7 @@ lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
 
 /-- Abstracting then closing preserves a single reduction. -/
 lemma step_abs_close {x : Var} (step : M ⭢βᶠ M') : M⟦0 ↜ x⟧.abs ⭢βᶠ M'⟦0 ↜ x⟧.abs := by
-  grind [abs ∅, redex_subst_cong]
+  grind [Xi.abs ∅, redex_subst_cong]
 
 /-- Abstracting then closing preserves multiple reductions. -/
 lemma redex_abs_close {x : Var} (step : M ↠βᶠ M') : (M⟦0 ↜ x⟧.abs ↠βᶠ M'⟦0 ↜ x⟧.abs) :=  by

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean

@@ -74,10 +74,13 @@ lemma para_lc_r (step : M ⭢ₚ N) : LC N := by
 omit [HasFresh Var] [DecidableEq Var] in
 /-- A single β-reduction implies a single parallel reduction. -/
 lemma step_to_para (step : M ⭢βᶠ N) : M ⭢ₚ N := by
-  induction step
-  case beta _ abs_lc _ => cases abs_lc with | abs xs _ => apply Parallel.beta xs <;> grind
-  case abs xs _ _ => apply Parallel.abs xs; grind
-  all_goals grind
+  induction step with
+  | base h =>
+    cases h with | beta abs_lc _ =>
+    cases abs_lc with | abs xs _ =>
+    apply Parallel.beta xs <;> grind
+  | abs xs _ _ => apply Parallel.abs xs; grind
+  | _ => grind
 
 open FullBeta in
 /-- A single parallel reduction implies a multiple β-reduction. -/
@@ -99,7 +102,7 @@ lemma para_to_redex (para : M ⭢ₚ N) : M ↠βᶠ N := by
       m'.abs.app n :=
         redex_app_l_cong (redex_abs_cong xs (fun _ mem ↦ redex_ih _ mem)) (para_lc_l para_n)
       _           ↠βᶠ m'.abs.app n' := by grind
-      _           ⭢βᶠ m' ^ n'       := beta m'_abs_lc (by grind)
+      _           ⭢βᶠ m' ^ n'       := by grind
 
 /-- Multiple parallel reduction is equivalent to multiple β-reduction. -/
 theorem parachain_iff_redex : M ↠ₚ N ↔ M ↠βᶠ N := by

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean

@@ -55,7 +55,7 @@ lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by
 @[scoped grind ←]
 lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
     M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by
-  induction Ns <;> grind [FullBeta.appR]
+  induction Ns <;> grind
 
 /-- Congruence lemma for multi reduction of the left most term of a multi-application -/
 lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
@@ -65,11 +65,11 @@ lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) :
 /-- Congruence lemma for single reduction of one of the arguments of a multi-application -/
 @[scoped grind ←]
 lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by
-  induction steps <;> grind [FullBeta.appL, FullBeta.appR]
+  induction steps <;> grind
 
 /-- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/
 lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by
-  induction steps <;> grind [FullBeta.appL, FullBeta.appR]
+  induction steps <;> grind
 
 /-- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then
     Q must be one of the following forms:
@@ -85,13 +85,13 @@ lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var}
     (∃ Ps', Ps ⭢lβᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨
     (Q = multiApp (M ^ N) Ps) := by
   induction Ps generalizing M N Q with
-  | nil => grind [cases FullBeta]
+  | nil => grind [cases Xi]
   | cons P Ps ih =>
     generalize Heq : (M.abs.app N).multiApp Ps = Q'
     have : ∀ P', Q'.app P' = (M.abs.app N).multiApp (P' :: Ps) := by grind
     rw [multiApp, Heq] at h_red
     cases h_red with
-    | beta => cases Ps <;> contradiction
+    | base => cases Ps <;> grind
     | appR => grind [→ ListFullBeta.cons]
     | appL => grind
 

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean

@@ -43,7 +43,7 @@ lemma sn_steps (t_st_t' : t ↠βᶠ t') (sn_t : SN t) : SN t' := by
 
 /-- Free variables are strongly normalizing. -/
 lemma sn_fvar {x : Var} : SN (fvar x) := by
-  grind [cases FullBeta]
+  grind only [cases Xi, cases Beta, SN]
 
 /-- An application is strongly normalizing if the left and right terms are strongly normalizing,
     as well as all possible future top level abstraction application beta reductions -/
@@ -56,7 +56,7 @@ lemma sn_app (t s : Term Var) (sn_t : SN t) (sn_s : SN s)
       constructor
       intro u hstep
       cases hstep with
-      | beta _ _       => grind
+      | base h => cases h; grind
       | appL _ h_s_red => apply ih_s _ h_s_red
                           grind [Relation.ReflTransGen.head]
       | appR _ h_t_red => apply ih_t _ h_t_red _ (SN.sn s hs)
@@ -91,7 +91,7 @@ inductive Neutral : Term Var → Prop
 
 /-- Neutral terms only reduce to other neutral terms in a single step -/
 lemma neutral_step (Hneut : Neutral t) (Hstep : t ⭢βᶠ t') : Neutral t' := by
-  induction Hneut generalizing t' with grind [cases FullBeta, sn_step]
+  induction Hneut generalizing t' with grind only [Neutral, cases Xi, sn_step]
 
 /-- Neutral terms only reduce to other neutral terms in multiple steps -/
 lemma neutral_steps (Hneut : Neutral t) (Hsteps : t ↠βᶠ t') : Neutral t' := by
@@ -101,7 +101,7 @@ lemma neutral_steps (Hneut : Neutral t) (Hsteps : t ↠βᶠ t') : Neutral t' :=
 lemma sn_neutral (Hneut : Neutral t) : SN t := by
   induction Hneut with
   | app => grind [→ neutral_steps, sn_app]
-  | _ => grind [cases FullBeta]
+  | _ => grind only [SN, cases Xi]
 
 /-- A lambda abstraction is strongly normalizing if its body is strongly normalizing. -/
 lemma sn_abs [DecidableEq Var] [HasFresh Var] {M N : Term Var} (sn_MN : SN (M ^ N)) (lc_N : LC N) :
@@ -111,7 +111,9 @@ lemma sn_abs [DecidableEq Var] [HasFresh Var] {M N : Term Var} (sn_MN : SN (M ^
   | sn =>
     constructor
     intro _ h_step
-    cases h_step with | abs _ H => grind [step_open_cong_l _ _ _ _ H]
+    cases h_step with
+    | abs _ H => grind [step_open_cong_l _ _ _ _ H]
+    | base _ => contradiction
 
 /-- A term of the form λ M N P_1 … P_n is strongly normalizing if
       1. N is strongly normalizing,
@@ -141,12 +143,16 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var}
           · apply steps_multiApp_l
             · apply steps_open_cong_abs M M' N N' <;> grind [open_abs_lc]
             · grind [multiApp_steps_lc]
-        apply sn_steps
+        refine sn_steps ?_ sn_MNPs
         · calc ((M ^ N).multiApp Ps).app P
             _ ↠βᶠ ((M ^ N).multiApp Ps).app P' := by grind
             _ ↠βᶠ Q'.abs.app P' := redex_app_l_cong (.trans innerSteps h_st2) (by grind)
-            _ ↠βᶠ Q' ^ P' := by grind [beta]
-        · grind
+            _ ↠βᶠ Q' ^ P' := by
+              rw [Relation.reflTransGen_iff_eq_or_transGen] at ⊢ innerSteps h_st2
+              right
+              cases lc_MNPs
+              refine Relation.TransGen.single (Xi.base (Beta.beta ?_ ?_))
+              all_goals grind only [→ step_lc_r]
 
 end LambdaCalculus.LocallyNameless.Untyped.Term
 

CslibTests/GrindLint.lean

@@ -78,6 +78,7 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.ty
 #grind_lint skip Cslib.Logic.HML.bisimulation_satisfies
 #grind_lint skip Cslib.Logic.HML.Satisfies.diamond
+#grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.step_multiApp_l
 
 #guard_msgs in
 #grind_lint check (min := 20) in Cslib