feat: Add BetaAt uniqueness, FV preservation, and left redex-count bound

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

@@ -152,8 +152,24 @@ lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt i M N) (lc : LC M) : M ⭢β
 
 variable [HasFresh Var]
 
+lemma BetaAt.le_countRedexes_l (h : BetaAt i M N) : i < countRedexes M := by
+  induction h with
+  | outer => grind
+  | appL step =>
+    split
+    · grind
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | appR =>
+    split
+    · rw [countRedexes_app_abs (by assumption)]
+      omega
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | abs xs =>
+    have := fresh_exists xs
+    grind [countRedexes_open_fvar]
+
 /-- The position of a contracted redex is at most the redex count of the result. -/
-lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
+lemma BetaAt.le_countRedexes_r (h : BetaAt i M N) : i ≤ countRedexes N := by
   induction h with
   | outer => exact Nat.zero_le _
   | appL step =>
@@ -172,6 +188,16 @@ lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
 
 variable [DecidableEq Var]
 
+lemma BetaAt.step_fv (h : BetaAt i M M') : M'.fv ⊆ M.fv := by
+  induction h with
+  | outer _ _ => grind [open_preserve_not_fvar]
+  | appL _ _ => grind
+  | appR _ _ => grind
+  | abs xs _ _ =>
+    have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+    have := open_close x
+    grind [open_preserve_not_fvar 0 M M']
+
 /-- Renaming a free variable preserves the position of the contracted redex. -/
 lemma BetaAt.rename (h : BetaAt i M M') (x y : Var) :
     BetaAt i (M[x := fvar y]) (M'[x := fvar y]) := by
@@ -218,6 +244,33 @@ lemma BetaAt.abs_close {x : Var} (h : BetaAt i M M') (lc : LC M) :
   have hr : BetaAt i (M[x := fvar z]) (M'[x := fvar z]) := h.rename x z
   grind
 
+lemma BetaAt.unique (hn : BetaAt i M N) (hp : BetaAt i M P) : N = P := by
+  induction hn generalizing P with
+  | outer _ _ =>
+      generalize hi : 0 = i at hp
+      cases hp <;> grind
+  | appL hn ih =>
+      generalize hi : ( _ +  if (IsAbs _) then 1 else 0) = i at hp
+      cases hp with
+      | outer => grind
+      | appL => grind
+      | appR hp =>
+          apply BetaAt.le_countRedexes_l at hn
+          omega
+  | appR hn ih =>
+      generalize hi : ( _ +  if (IsAbs _) then 1 else 0) = i at hp
+      cases hp with
+      | outer => grind
+      | appR => grind
+      | appL hp =>
+          apply BetaAt.le_countRedexes_l at hp
+          omega
+  | abs xs _ ih => cases hp with | abs xs hp =>
+      have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+      specialize ih x (by grind) (hp x (by grind))
+      apply_fun (fun t => close t x) at ih
+      rw [<- open_close_var, <- open_close_var] at ih <;> grind
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

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

@@ -92,6 +92,12 @@ lemma Leftmost.of_cbn (h : M ↠ₙ N) : M ↠ℓ N := by
 
 variable [DecidableEq Var] [HasFresh Var]
 
+lemma Leftmost.steps_fv (steps : M ↠ℓ M') : M'.fv ⊆ M.fv := by
+  induction steps with
+  | refl => grind
+  | tail _ h _ => apply BetaAt.step_fv at h
+                  grind
+
 /-- Leftmost reduction preserves local closure. -/
 lemma Leftmost.steps_lc_r (h : M ↠ℓ M') (lc : LC M) : LC M' := by
   induction h with

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

@@ -163,7 +163,7 @@ lemma StandardSeq.le_countRedexes_of_ne (h : StandardSeq n M N) (hne : M ≠ N)
     n ≤ countRedexes N := by
   cases h with
   | refl => contradiction
-  | tail _ step _ => exact step.le_countRedexes
+  | tail _ step _ => exact step.le_countRedexes_r
 
 omit [HasFresh Var] in
 /-- Reducing the operator of an application yields a standard sequence, with the final position