Skip to content

feat(LocallyNameless): FullBetaEta, Normal.sup_iff #862

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lengyijun wants to merge 1 commit into
base: main
Choose a base branch
from
+48 −15
Open

feat(LocallyNameless): FullBetaEta, Normal.sup_iff #862

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions Cslib/Foundations/Relation/Confluence.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,6 +131,13 @@ theorem Normal_iff (r : α → α → Prop) (x : α) : Normal r x ↔ ∀ y, ¬
theorem Normal.reflTransGen_eq (h : Normal r x) (xy : ReflTransGen r x y) : x = y := by
induction xy <;> grind

theorem Normal.sup_iff (x : α) : Normal (r₁ ⊔ r₂) x ↔ Normal r₁ x /\ Normal r₂ x := by
constructor
· intros g
constructor <;> intros h <;> apply g <;> obtain ⟨t, _⟩ := h <;> exists t <;> tauto
· rintro _ ⟨t, h⟩
cases h <;> grind

/-- For a Church-Rosser relation, elements in an equivalence class must be multi-step related. -/
theorem ChurchRosser.normal_eqvGen_reflTransGen (cr : ChurchRosser r) (norm : Normal r x)
(xy : EqvGen r y x) : ReflTransGen r y x := by
Expand Down
56 changes: 41 additions & 15 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEta.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,23 +37,49 @@ abbrev FullBetaEta : Term Var → Term Var → Prop := FullBeta ⊔ FullEta

namespace FullBetaEta

theorem redex_app_l_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app M N ↠βηᶠ app M' N := by
induction redex with
variable {M M' N N' : Term Var}

theorem step_app_l_cong (step : M ⭢βηᶠ M') (h_lc : LC N) : app M N ⭢βηᶠ app M' N := by
rcases step with h | h
· exact join_inl (h.appR h_lc)
· exact join_inr (h.appR h_lc)

theorem step_app_r_cong (step : M ⭢βηᶠ M') (h_lc : LC N) : app N M ⭢βηᶠ app N M' := by
rcases step with h | h
· exact join_inl (h.appL h_lc)
· exact join_inr (h.appL h_lc)

theorem steps_app_l_cong (steps : M ↠βηᶠ M') (h_lc : LC N) : app M N ↠βηᶠ app M' N := by
induction steps with
| refl => grind
| tail _ h ih => exact ih.tail (step_app_l_cong h h_lc)

theorem steps_app_r_cong (steps : M ↠βηᶠ M') (h_lc : LC N) : app N M ↠βηᶠ app N M' := by
induction steps with
| refl => grind
| tail _ h ih =>
refine .tail ih ?_
rcases h with h | h
· exact join_inl (h.appR lc_N)
· exact join_inr (h.appR lc_N)

theorem redex_app_r_cong (redex : M ↠βηᶠ M') (lc_N : LC N) : app N M ↠βηᶠ app N M' := by
induction redex with
| tail _ h ih => exact ih.tail (step_app_r_cong h h_lc)

variable [HasFresh Var] [DecidableEq Var]

lemma step_fv (step : M ⭢βηᶠ M') : M'.fv ⊆ M.fv := by
cases step with
| inl h => grind [FullBeta.step_not_fv h]
| inr h => grind [FullEta.step_not_fv h]

lemma steps_fv (steps : M ↠βηᶠ M') : M'.fv ⊆ M.fv := by
induction steps with
| refl => grind
| tail _ h ih =>
refine .tail ih ?_
rcases h with h | h
· exact join_inl (h.appL lc_N)
· exact join_inr (h.appL lc_N)
| tail _ step _ => grind [step_fv step]

lemma step_subst_cong_l (x : Var) (step : M ⭢βηᶠ M') (h_lc : LC N) :
M[x := N] ⭢βηᶠ M'[x := N] := by
cases step with
| inl h => exact Or.inl (FullBeta.redex_subst_cong_lc _ _ _ _ h h_lc)
| inr h => exact Or.inr (FullEta.step_subst_cong_l _ _ _ h h_lc)

lemma steps_subst_cong_l (x : Var) (steps : M ↠βηᶠ M') (h_lc : LC N) :
M[x := N] ↠βηᶠ M'[x := N] := by
induction steps with grind [step_subst_cong_l]

end FullBetaEta

Expand Down
Loading