feat: sn_eta_steps_inv

Cslib.lean

@@ -239,7 +239,9 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LeftmostReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.ParEtaC
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Size
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic

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

@@ -9,6 +9,7 @@ module
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.ParEtaC
 
 /-! # βη-Confluence for the λ-calculus
 
@@ -33,62 +34,12 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
 open Relation
 
-open FullEta FullBeta in
 /-- η-reduction and β-reduction strongly commute. -/
 lemma stronglyCommute_eta_beta : StronglyCommute (@FullEta Var) FullBeta := by
   intro x y₁ y₂ h₁ st_beta
-  induction st_beta generalizing y₁
-  case base h1_b =>
-    cases h1_b
-    case beta M N _ _ =>
-      cases h₁
-      case base h => cases h
-      case appL v _ _ =>
-        use M ^ v
-        grind [step_open_cong_r]
-      case appR u st_eta_absM _ =>
-        have := step_lc_r st_eta_absM
-        cases st_eta_absM
-        case base h => use (disch := grind) app u N
-        case abs M_eta xs _ =>
-          have ⟨_, hz⟩ := fresh_exists (xs ∪ N.fv ∪ M.fv ∪ M_eta.fv)
-          use M_eta ^ N
-          grind [step_subst_cong_l]
-  case appL Z _ N _ _ ih =>
-    cases h₁
-    case base h => cases h
-    case appL _ _ st =>
-      use app Z (ih st).choose
-      grind [FullEta.redex_app_r_cong]
-    case appR z_red _ _ => use (disch := grind) app z_red N
-  case appR M _ Z _ _ ih =>
-    cases h₁
-    case base h => cases h
-    case appL z_red _ _ => use (disch := grind) app Z z_red
-    case appR _ st _ =>
-      use app (ih st).choose M
-      grind [FullEta.redex_app_l_cong]
-  case abs M N xs st_body_beta ih =>
-    cases h₁
-    case base h_eta =>
-      cases h_eta with | eta =>
-        have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
-        have st_beta_w : app y₁ (fvar w) ⭢βᶠ N ^ fvar w := by grind [st_body_beta w]
-        rcases invert_step_app_fvar st_beta_w with ⟨u', h, st_u⟩ | ⟨u1, _, _⟩
-        · use u'
-          apply open_eq_app at h <;> grind [FullBeta.step_not_fv st_u]
-        · use abs u1
-          grind [open_injective w N u1]
-    case abs S ys st_body_eta =>
-      have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
-      obtain ⟨K, h_beta, h_eta⟩ := ih w (by grind) (st_body_eta w (by grind))
-      use abs (K ^* w)
-      constructor
-      · cases h_beta with
-        | refl => grind [open_close]
-        | single => exact .single (Xi.abs {w} (by grind [FullBeta.redex_subst_cong]))
-      · rw [open_close w N 0 (by grind)]
-        exact FullEta.redex_abs_close h_eta
+  rcases interaction _ 1 _ _ (parEtaC_of_fullEta h₁) st_beta with ⟨s', m, h, g⟩|⟨m, _, h⟩
+  · exact ⟨s', .single g, ParEtaC.toFullEtaStar h⟩
+  · exact ⟨y₁, .refl, ParEtaC.toFullEtaStar h⟩
 
 open Commute in
 /-- βη-reduction is confluent. -/

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

@@ -7,8 +7,10 @@ Authors: Maximiliano Onofre Martínez
 module
 
 public import Cslib.Foundations.Relation.Attr
+public import Cslib.Foundations.Relation.Defs
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Size
 
 /-! # η-reduction for the λ-calculus -/
 
@@ -149,6 +151,13 @@ lemma steps_open_cong_r {s t t' : Term Var} (lc_s : LC s.abs) (steps : t ↠η
   case refl => rfl
   case head _ _ st _ ih => exact .trans (step_open_cong_r lc_s st) ih
 
+lemma step_size (step : M ⭢ηᶠ M') : M'.size < M.size := by
+  induction step with
+  | abs xs _ =>
+    have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+    grind
+  | _ => grind
+
 /- Closing a sequence of η-reduction steps over a fresh variable preserves the steps. -/
 open Relation in
 lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N) :
@@ -158,6 +167,16 @@ lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N
   | single st =>
     exact .single (Xi.abs {x} (by grind [step_subst_cong_l]))
 
+open Relation in
+lemma terminating : Terminating (@FullEta Var) := by
+  apply WellFounded.intro
+  intros t
+  induction h : t.size using Nat.strong_induction_on generalizing t with | h n ih =>
+  apply Acc.intro
+  intros y hy
+  apply FullEta.step_size at hy
+  exact ih y.size (by omega) _ rfl
+
 end LambdaCalculus.LocallyNameless.Untyped.Term.FullEta
 
 end Cslib