diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean new file mode 100644 index 00000000..1e43b5ba --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean @@ -0,0 +1,3 @@ +import Aesop + +declare_aesop_rule_sets [LambdaCalculus.LocallyNameless.ruleSet] (default := true) diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean index 7b3038e2..646cae50 100644 --- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean +++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean @@ -6,6 +6,7 @@ Authors: Chris Henson import Cslib.Data.HasFresh import Cslib.Syntax.HasSubstitution +import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.AesopRuleset /-! # λ-calculus @@ -36,9 +37,10 @@ inductive Term (Var : Type u) /-- Function application. -/ | app : Term Var → Term Var → Term Var +namespace Term + /-- Variable opening of the ith bound variable. -/ -@[simp] -def Term.openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var +def openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var | bvar i' => if i = i' then sub else bvar i' | fvar x => fvar x | app l r => app (openRec i sub l) (openRec i sub r) @@ -46,15 +48,25 @@ def Term.openRec (i : ℕ) (sub : Term Var) : Term Var → Term Var scoped notation:68 e "⟦" i " ↝ " sub "⟧"=> Term.openRec i sub e +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma openRec_bvar : (bvar i')⟦i ↝ s⟧ = if i = i' then s else bvar i' := by rfl + +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma openRec_fvar : (fvar x)⟦i ↝ s⟧ = fvar x := by rfl + +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma openRec_app : (app l r)⟦i ↝ s⟧ = app (l⟦i ↝ s⟧) (r⟦i ↝ s⟧) := by rfl + +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma openRec_abs : M.abs⟦i ↝ s⟧ = M⟦i + 1 ↝ s⟧.abs := by rfl + /-- Variable opening of the closest binding. -/ -@[simp] -def Term.open' {X} (e u):= @Term.openRec X 0 u e +def open' {X} (e u):= @Term.openRec X 0 u e infixr:80 " ^ " => Term.open' /-- Variable closing, replacing a free `fvar x` with `bvar k` -/ -@[simp] -def Term.closeRec (k : ℕ) (x : Var) : Term Var → Term Var +def closeRec (k : ℕ) (x : Var) : Term Var → Term Var | fvar x' => if x = x' then bvar k else fvar x' | bvar i => bvar i | app l r => app (closeRec k x l) (closeRec k x r) @@ -62,15 +74,31 @@ def Term.closeRec (k : ℕ) (x : Var) : Term Var → Term Var scoped notation:68 e "⟦" k " ↜ " x "⟧"=> Term.closeRec k x e +variable {x : Var} + +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma closeRec_bvar : (bvar i)⟦k ↜ x⟧ = bvar i := by rfl + +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma closeRec_fvar : (fvar x')⟦k ↜ x⟧ = if x = x' then bvar k else fvar x' := by rfl + +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma closeRec_app : (app l r)⟦k ↜ x⟧ = app (l⟦k ↜ x⟧) (r⟦k ↜ x⟧) := by rfl + +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma closeRec_abs : t.abs⟦k ↜ x⟧ = t⟦k + 1 ↜ x⟧.abs := by rfl + /-- Variable closing of the closest binding. -/ -@[simp] -def Term.close {Var} [DecidableEq Var] (e u):= @Term.closeRec Var _ 0 u e +def close {Var} [DecidableEq Var] (e u):= @Term.closeRec Var _ 0 u e infixr:80 " ^* " => Term.close /- Substitution of a free variable to a term. -/ -@[simp] -def Term.subst (m : Term Var) (x : Var) (sub : Term Var) : Term Var := +def subst (m : Term Var) (x : Var) (sub : Term Var) : Term Var := match m with | bvar i => bvar i | fvar x' => if x = x' then sub else fvar x' @@ -78,20 +106,40 @@ def Term.subst (m : Term Var) (x : Var) (sub : Term Var) : Term Var := | abs M => abs $ M.subst x sub /-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/ -@[simp] instance instHasSubstitutionTerm : HasSubstitution (Term Var) Var where subst := Term.subst +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma subst_bvar {n : Term Var} : (bvar i)[x := n] = bvar i := by rfl + +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma subst_fvar : (fvar x')[x := n] = if x = x' then n else fvar x' := by rfl + +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma subst_app {l r : Term Var} : (app l r)[x := n] = app (l[x := n]) (r[x := n]) := by rfl + +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma subst_abs {M : Term Var} : M.abs[x := n] = M[x := n].abs := by rfl + +omit [HasFresh Var] in +@[aesop norm (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma subst_def (m : Term Var) (x : Var) (n : Term Var) : m.subst x n = m[x := n] := by rfl + /-- Free variables of a term. -/ @[simp] -def Term.fv : Term Var → Finset Var +def fv : Term Var → Finset Var | bvar _ => {} | fvar x => {x} | abs e1 => e1.fv | app l r => l.fv ∪ r.fv /-- Locally closed terms. -/ -inductive Term.LC : Term Var → Prop +@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet]) [constructors]] +inductive LC : Term Var → Prop | fvar (x) : LC (fvar x) | abs (L : Finset Var) (e : Term Var) : (∀ x : Var, x ∉ L → LC (e ^ fvar x)) → LC (abs e) | app {l r} : l.LC → r.LC → LC (app l r) diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean new file mode 100644 index 00000000..35bc61bc --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean @@ -0,0 +1,122 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic +import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties +import Cslib.Semantics.ReductionSystem.Basic + +/-! # β-reduction for the λ-calculus + +## References + +* [A. Chargueraud, *The Locally Nameless Representation*] [Chargueraud2012] +* See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which + this is partially adapted + +-/ + +universe u + +variable {Var : Type u} + +namespace LambdaCalculus.LocallyNameless.Term + +/-- A single β-reduction step. -/ +@[reduction_sys fullBetaRs "βᶠ"] +inductive FullBeta : 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) + +namespace FullBeta + +variable {M M' N N' : Term Var} + +/-- The left side of a reduction is locally closed. -/ +lemma step_lc_l (step : M ⭢βᶠ M') : LC M := by + induction step <;> constructor + all_goals assumption + +/-- Left congruence rule for application in multiple reduction.-/ +theorem redex_app_l_cong : (M ↠βᶠ M') → LC N → (app M N ↠βᶠ app M' N) := by + intros redex lc_N + induction' redex + case refl => rfl + case tail ih r => exact Relation.ReflTransGen.tail r (appR lc_N ih) + +/-- Right congruence rule for application in multiple reduction.-/ +theorem redex_app_r_cong : (M ↠βᶠ M') → LC N → (app N M ↠βᶠ app N M') := by + intros redex lc_N + induction' redex + case refl => rfl + case tail ih r => exact Relation.ReflTransGen.tail r (appL lc_N ih) + +variable [HasFresh Var] [DecidableEq Var] + +/-- The right side of a reduction is locally closed. -/ +lemma step_lc_r (step : M ⭢βᶠ M') : LC M' := by + induction step + case beta => apply beta_lc <;> assumption + all_goals try constructor <;> assumption + +/-- Substitution respects a single reduction step. -/ +lemma redex_subst_cong (s s' : Term Var) (x y : Var) : (s ⭢βᶠ s') → (s [ x := fvar y ]) ⭢βᶠ (s' [ x := fvar y ]) := by + intros step + induction step + case appL ih => exact appL (subst_lc (by assumption) (by constructor)) ih + case appR ih => exact appR (subst_lc (by assumption) (by constructor)) ih + case beta m n abs_lc n_lc => + cases abs_lc with | abs xs _ mem => + simp only [open'] + rw [subst_open x (fvar y) 0 n m (by constructor)] + refine beta ?_ (subst_lc n_lc (by constructor)) + exact subst_lc (LC.abs xs m mem) (LC.fvar y) + case abs m' m xs mem ih => + apply abs ({x} ∪ xs) + intros z z_mem + simp only [open'] + rw [ + subst_def, subst_def, + ←subst_fresh x (fvar z) (fvar y), ←subst_open x (fvar y) 0 (fvar z) m (by constructor), + subst_fresh x (fvar z) (fvar y), ←subst_fresh x (fvar z) (fvar y), + ←subst_open x (fvar y) 0 (fvar z) m' (by constructor), subst_fresh x (fvar z) (fvar y) + ] + apply ih + all_goals aesop + +/-- Abstracting then closing preserves a single reduction. -/ +lemma step_abs_close {x : Var} : (M ⭢βᶠ M') → (M⟦0 ↜ x⟧.abs ⭢βᶠ M'⟦0 ↜ x⟧.abs) := by + intros step + apply abs ∅ + intros y _ + simp only [open'] + repeat rw [open_close_to_subst] + exact redex_subst_cong M M' x y step + exact step_lc_r step + exact step_lc_l step + +/-- Abstracting then closing preserves multiple reductions. -/ +lemma redex_abs_close {x : Var} : (M ↠βᶠ M') → (M⟦0 ↜ x⟧.abs ↠βᶠ M'⟦0 ↜ x⟧.abs) := by + intros step + induction step using Relation.ReflTransGen.trans_induction_on + case ih₁ => rfl + case ih₂ ih => exact Relation.ReflTransGen.single (step_abs_close ih) + case ih₃ l r => trans; exact l; exact r + +/-- Multiple reduction of opening implies multiple reduction of abstraction. -/ +theorem redex_abs_cong (xs : Finset Var) : (∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) → M.abs ↠βᶠ M'.abs := by + intros mem + have ⟨fresh, union⟩ := fresh_exists (xs ∪ M.fv ∪ M'.fv) + simp only [Finset.union_assoc, Finset.mem_union, not_or] at union + obtain ⟨_, _, _⟩ := union + rw [←open_close fresh M 0 ?_, ←open_close fresh M' 0 ?_] + refine redex_abs_close (mem fresh ?_) + all_goals assumption diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean new file mode 100644 index 00000000..5dfc85ba --- /dev/null +++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean @@ -0,0 +1,254 @@ +/- +Copyright (c) 2025 Chris Henson. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Henson +-/ + +import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic +import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties +import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBeta +import Cslib.Utils.Relation + +/-! # β-confluence for the λ-calculus -/ + +universe u + +variable {Var : Type u} + +namespace LambdaCalculus.LocallyNameless.Term + +/-- A parallel β-reduction step. -/ +@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet]) [constructors], reduction_sys paraRs "ₚ"] +inductive Parallel : Term Var → Term Var → Prop +/-- Free variables parallel step to themselves. -/ +| fvar (x : Var) : Parallel (fvar x) (fvar x) +/-- A parallel left and right congruence rule for application. -/ +| app : Parallel L L' → Parallel M M' → Parallel (app L M) (app L' M') +/-- Congruence rule for lambda terms. -/ +| abs (xs : Finset Var) : (∀ x ∉ xs, Parallel (m ^ fvar x) (m' ^ fvar x)) → Parallel (abs m) (abs m') +/-- A parallel β-reduction. -/ +| beta (xs : Finset Var) : + (∀ x ∉ xs, Parallel (m ^ fvar x) (m' ^ fvar x) ) → + Parallel n n' → + Parallel (app (abs m) n) (m' ^ n') + +-- TODO: I think this could be generated along with `para_rs` +lemma para_rs_Red_eq {α} : (@paraRs α).Red = Parallel := by rfl + +variable {M M' N N' : Term Var} + +/-- The left side of a parallel reduction is locally closed. -/ +@[aesop unsafe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma para_lc_l (step : M ⭢ₚ N) : LC M := by + induction step + case abs _ _ xs _ ih => exact LC.abs xs _ ih + case beta => refine LC.app (LC.abs ?_ _ ?_) ?_ <;> assumption + all_goals constructor <;> assumption + +variable [HasFresh Var] [DecidableEq Var] + +/-- The right side of a parallel reduction is locally closed. -/ +@[aesop unsafe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +lemma para_lc_r (step : M ⭢ₚ N) : LC N := by + induction step + case abs _ _ xs _ ih => exact LC.abs xs _ ih + case beta => refine beta_lc (LC.abs ?_ _ ?_) ?_ <;> assumption + all_goals constructor <;> assumption + +/-- Parallel reduction is reflexive for locally closed terms. -/ +@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +def Parallel.lc_refl (M : Term Var) : LC M → M ⭢ₚ M := by + intros lc + induction lc + all_goals constructor <;> assumption + +-- TODO: better ways to handle this? +-- The problem is that sometimes when we apply a theorem we get out of our notation, so aesop can't +-- see they are the same, including constructors. +@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] +def Parallel.lc_refl' (M : Term Var) : LC M → Parallel M M := Parallel.lc_refl M + +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 <;> simp only [para_rs_Red_eq] + case beta _ abs_lc _ => cases abs_lc with | abs xs _ => + apply Parallel.beta xs <;> intros <;> apply Parallel.lc_refl <;> aesop + all_goals aesop (config := {enableSimp := false}) + +open FullBeta in +/-- A single parallel reduction implies a multiple β-reduction. -/ +lemma para_to_redex (para : M ⭢ₚ N) : (M ↠βᶠ N) := by + induction para + case fvar => constructor + case app _ _ _ _ l_para m_para redex_l redex_m => + trans + exact redex_app_l_cong redex_l (para_lc_l m_para) + exact redex_app_r_cong redex_m (para_lc_r l_para) + case abs t t' xs _ ih => + apply redex_abs_cong xs + intros x mem + exact ih x mem + case beta m m' n n' xs para_ih para_n redex_ih redex_n => + have m'_abs_lc : LC m'.abs := by + apply LC.abs xs + intros _ mem + exact para_lc_r (para_ih _ mem) + calc + m.abs.app n ↠βᶠ m'.abs.app n := redex_app_l_cong (redex_abs_cong xs (λ _ mem ↦ redex_ih _ mem)) (para_lc_l para_n) + _ ↠βᶠ m'.abs.app n' := redex_app_r_cong redex_n m'_abs_lc + _ ⭢βᶠ m' ^ n' := beta m'_abs_lc (para_lc_r para_n) + +/-- Multiple parallel reduction is equivalent to multiple β-reduction. -/ +theorem parachain_iff_redex : (M ↠ₚ N) ↔ (M ↠βᶠ N) := by + refine Iff.intro ?chain_to_redex ?redex_to_chain <;> intros h <;> induction' h <;> try rfl + case redex_to_chain.tail redex chain => exact Relation.ReflTransGen.tail chain (step_to_para redex) + case chain_to_redex.tail para redex => exact Relation.ReflTransGen.trans redex (para_to_redex para) + +/-- Parallel reduction respects substitution. -/ +lemma para_subst (x : Var) : (M ⭢ₚ M') → (N ⭢ₚ N') → (M[x := N] ⭢ₚ M'[x := N']) := by + intros pm pn + induction pm + case fvar => aesop + case beta _ _ _ _ xs _ _ ih _ => + simp only [open'] + rw [subst_open _ _ _ _ _ (para_lc_r pn)] + apply Parallel.beta (xs ∪ {x}) + intros y ymem + simp only [Finset.mem_union, Finset.mem_singleton, not_or] at ymem + push_neg at ymem + rw [ + subst_def, + subst_open_var _ _ _ _ _ (para_lc_r pn), + subst_open_var _ _ _ _ _ (para_lc_l pn) + ] + apply ih + all_goals aesop + case app => constructor <;> assumption + case abs u u' xs mem ih => + apply Parallel.abs (xs ∪ {x}) + intros y ymem + simp only [Finset.mem_union, Finset.mem_singleton, not_or] at ymem + repeat rw [subst_def] + rw [subst_open_var _ _ _ _ ?_ (para_lc_l pn), subst_open_var _ _ _ _ ?_ (para_lc_r pn)] + push_neg at ymem + apply ih + all_goals aesop + +/-- Parallel substitution respects closing and opening. -/ +lemma para_open_close (x y z) : + (M ⭢ₚ M') → + y ∉ (M.fv ∪ M'.fv ∪ {x}) → + M⟦z ↜ x⟧⟦z ↝ fvar y⟧ ⭢ₚ M'⟦z ↜ x⟧⟦z ↝ fvar y⟧ + := by + intros para vars + simp only [Finset.union_assoc, Finset.mem_union, Finset.mem_singleton, not_or] at vars + rw [open_close_to_subst, open_close_to_subst] + apply para_subst + exact para + constructor + exact para_lc_r para + exact para_lc_l para + +/-- Parallel substitution respects fresh opening. -/ +lemma para_open_out (L : Finset Var) : + (∀ x, x ∉ L → (M ^ fvar x) ⭢ₚ (N ^ fvar x)) + → (M' ⭢ₚ N') → (M ^ M') ⭢ₚ (N ^ N') := by + intros mem para + let ⟨x, qx⟩ := fresh_exists (L ∪ N.fv ∪ M.fv) + simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx + obtain ⟨q1, q2, q3⟩ := qx + rw [subst_intro x M' _ q3 (para_lc_l para), subst_intro x N' _ q2 (para_lc_r para)] + exact para_subst x (mem x q1) para + +-- TODO: the Takahashi translation would be a much nicer and shorter proof, but I had difficultly +-- writing it for locally nameless terms. + +-- adapted from https://github.com/ElifUskuplu/Stlc_deBruijn/blob/main/Stlc/confluence.lean +/-- Parallel reduction has the diamond property. -/ +theorem para_diamond : Diamond (@Parallel Var) := by + intros t t1 t2 tpt1 + revert t2 + induction tpt1 <;> intros t2 tpt2 + case fvar x => exact ⟨t2, by aesop⟩ + case abs s1 s2' xs mem ih => + cases tpt2 + case abs t2' xs' mem' => + have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ t2'.fv ∪ s2'.fv) + simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx + have ⟨q1, q2, q3, q4⟩ := qx + have ⟨t', qt'_l, qt'_r⟩ := ih x q1 (mem' _ q2) + exists abs (t' ^* x) + constructor + <;> [let z := s2'; let z := t2'] + <;> apply Parallel.abs ((z ^ fvar x).fv ∪ t'.fv ∪ {x}) + <;> intros y qy <;> simp only [open', close] + <;> [rw [←open_close x _ 0 q4]; rw [←open_close x _ 0 q3]] + <;> refine para_open_close x y 0 ?_ qy <;> [exact qt'_l; exact qt'_r] + case beta s1 s1' s2 s2' xs mem ps ih1 ih2 => + cases tpt2 + case app u2 u2' s1pu2 s2pu2' => + cases s1pu2 + case abs s1'' xs' mem' => + have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ s1''.fv ∪ s1'.fv) + simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx + obtain ⟨q1, q2, q3, q4⟩ := qx + have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2' + have ⟨t'', qt''_l, qt''_r⟩ := @ih1 x q1 _ (mem' _ q2) + exists (t'' ^* x) ^ t' + constructor + · rw [subst_intro x s2' _ q4 (para_lc_l qt'_l), + subst_intro x t' _ (close_var_not_fvar x t'') (para_lc_r qt'_l)] + simp only [open', close] + rw [close_open _ _ _ (para_lc_r qt''_l)] + exact para_subst x qt''_l qt'_l + · apply Parallel.beta ((s1'' ^ fvar x).fv ∪ t''.fv ∪ {x}) + intros y qy + rw [←open_close x s1'' 0] + apply para_open_close + all_goals aesop + case beta u1' u2' xs' mem' s2pu2' => + have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ u1'.fv ∪ s1'.fv ∪ s2'.fv ∪ u2'.fv) + simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx + have ⟨q1, q2, q3, q4, q5, q6⟩ := qx + have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2' + have ⟨t'', qt''_l, qt''_r⟩ := @ih1 x q1 _ (mem' _ q2) + rw [subst_intro x u2' u1' _ (para_lc_l qt'_r), subst_intro x s2' s1' _ (para_lc_l qt'_l)] + exists t'' [x := t'] + exact ⟨para_subst x qt''_l qt'_l, para_subst x qt''_r qt'_r⟩ + all_goals aesop + case app s1 s1' s2 s2' s1ps1' _ ih1 ih2 => + cases tpt2 + case app u1 u2' s1 s2 => + have ⟨l, _, _⟩ := ih1 s1 + have ⟨r, _, _⟩ := ih2 s2 + exact ⟨app l r, by aesop⟩ + case beta t1' u1' u2' xs mem s2pu2' => + cases s1ps1' + case abs s1'' xs' mem' => + have ⟨x, qx⟩ := fresh_exists (xs ∪ xs' ∪ s1''.fv ∪ u1'.fv) + simp only [Finset.union_assoc, Finset.mem_union, not_or] at qx + obtain ⟨q1, q2, q3, q4⟩ := qx + have ⟨t', qt'_l, qt'_r⟩ := ih2 s2pu2' + have ⟨t'', qt''_l, qt''_r⟩ := @ih1 (abs u1') (Parallel.abs xs mem) + cases qt''_l + next w1 xs'' mem'' => + cases qt''_r + case abs xs''' mem''' => + exists w1 ^ t' + constructor + · aesop (config := {enableSimp := false}) + · exact para_open_out xs''' mem''' qt'_r + +/-- Parallel reduction is confluent. -/ +theorem para_confluence : Confluence (@Parallel Var) := + Relation.ReflTransGen.diamond_confluence para_diamond + +/-- β-reduction is confluent. -/ +theorem confluence_beta : Confluence (@FullBeta Var) := by + simp only [Confluence] + have eq : Relation.ReflTransGen (@Parallel Var) = Relation.ReflTransGen (@FullBeta Var) := by + ext + exact parachain_iff_redex + rw [←eq] + exact @para_confluence Var _ _ diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean index 2ca6e005..69fbb9b2 100644 --- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean +++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean @@ -12,44 +12,43 @@ variable {Var : Type u} namespace LambdaCalculus.LocallyNameless.Term +lemma open_app_inj : app l r = (app l r)⟦i ↝ s⟧ ↔ l = l⟦i ↝ s⟧ ∧ r = r⟦i ↝ s⟧ := by + simp [openRec] + +lemma open_abs_inj : M.abs = M⟦i + 1 ↝ s⟧.abs ↔ M = M⟦i + 1 ↝ s⟧ := by + simp + /-- An opening appearing in both sides of an equality of terms can be removed. -/ lemma open_lc_aux (e : Term Var) : ∀ (j v i u), - i ≠ j -> - e ⟦j ↝ v⟧ = (e ⟦j ↝ v⟧) ⟦i ↝ u⟧ -> + i ≠ j → + e ⟦j ↝ v⟧ = (e ⟦j ↝ v⟧) ⟦i ↝ u⟧ → e = e ⟦i ↝ u⟧ := by - induction' e - <;> intros j v i u neq h - <;> simp only [openRec, app.injEq, abs.injEq] at * - case bvar => aesop - case app ih_l ih_r => - obtain ⟨hl, hr⟩ := h + induction' e <;> intros j v i u neq h + case app l r ih_l ih_r => + obtain ⟨hl, hr⟩ := open_app_inj.mp h + simp only [open_app_inj] exact ⟨ih_l j v i u neq hl, ih_r j v i u neq hr⟩ - case abs ih => exact ih (j+1) v (i+1) u (by aesop) h + case abs ih => + simp only [openRec_abs, open_abs_inj] at * + exact ih (j+1) v (i+1) u (by aesop) h + all_goals aesop /-- Opening is associative for nonclashing free variables. -/ lemma swap_open_fvars (k n : ℕ) (x y : Var) (m : Term Var) : k ≠ n → x ≠ y → m⟦n ↝ fvar y⟧⟦k ↝ fvar x⟧ = m⟦k ↝ fvar x⟧⟦n ↝ fvar y⟧ := by revert k n - induction' m <;> intros k n ne_kn ne_xy <;> simp only [openRec, app.injEq, abs.injEq] - case bvar n' => aesop - case abs ih => apply ih <;> aesop - case app => aesop + induction' m <;> aesop variable [DecidableEq Var] /-- Substitution of a free variable not present in a term leaves it unchanged. -/ theorem subst_fresh (x : Var) (t sub : Term Var) : x ∉ t.fv → (t [x := sub]) = t := by - induction t <;> intros <;> aesop + induction t <;> aesop /- Opening and closing are inverses. -/ lemma open_close (x : Var) (t : Term Var) (k : ℕ) : x ∉ t.fv → t⟦k ↝ fvar x⟧⟦k ↜ x⟧ = t := by - intros mem revert k - induction t <;> intros k <;> simp only [openRec, closeRec, app.injEq, abs.injEq] - case bvar n => split <;> simp_all - case abs t ih => exact ih mem (k + 1) - case app l r ih_l ih_r => refine ⟨ih_l ?_ k, ih_r ?_ k⟩ <;> aesop - all_goals aesop + induction t <;> aesop /-- Opening is injective. -/ lemma open_injective (x : Var) (M M' : Term Var) : x ∉ M.fv → x ∉ M'.fv → M ^ fvar x = M' ^ fvar x → M = M' := by @@ -61,49 +60,27 @@ lemma open_injective (x : Var) (M M' : Term Var) : x ∉ M.fv → x ∉ M'.fv lemma swap_open_fvar_close (k n: ℕ) (x y : Var) (m : Term Var) : k ≠ n → x ≠ y → m⟦n ↝ fvar y⟧⟦k ↜ x⟧ = m⟦k ↜ x⟧⟦n ↝ fvar y⟧ := by revert k n - induction' m - <;> intros k n ne_kn ne_xy - <;> simp only [openRec, closeRec, app.injEq, abs.injEq] - case bvar n' => split <;> aesop - case fvar x' => split <;> aesop - case abs ih => apply ih <;> aesop - case app => aesop + induction' m <;> aesop /-- Closing preserves free variables. -/ lemma close_preserve_not_fvar {k x y} (m : Term Var) : x ∉ m.fv → x ∉ (m⟦k ↜ y⟧).fv := by - intros mem revert k - induction m <;> intros k <;> simp only [closeRec] - case fvar y' => split <;> aesop - case abs ih => exact ih mem - all_goals aesop + induction m <;> aesop /-- Opening to a fresh free variable preserves free variables. -/ lemma open_fresh_preserve_not_fvar {k x y} (m : Term Var) : x ∉ m.fv → x ≠ y → x ∉ (m⟦k ↝ fvar y⟧).fv := by - intros mem neq revert k - induction m <;> intros k <;> simp only [openRec] - case bvar n' => split <;> aesop - case fvar => aesop - case abs ih => exact ih mem - all_goals aesop + induction m <;> aesop /-- Substitution preserves free variables. -/ lemma subst_preserve_not_fvar {x y : Var} (m n : Term Var) : x ∉ m.fv ∪ n.fv → x ∉ (m [y := n]).fv := by - intros mem - simp only [Finset.mem_union, not_or] at mem - induction m <;> simp only [instHasSubstitutionTerm, subst] - case fvar y' => split <;> simp only [fv, Finset.mem_singleton, mem] <;> aesop - case abs ih => exact ih mem + induction m all_goals aesop /-- Closing removes a free variable. -/ lemma close_var_not_fvar_rec (x) (k) (t : Term Var) : x ∉ (t⟦k ↜ x⟧).fv := by revert k - induction t <;> intros k <;> simp only [closeRec] - case fvar x' => split <;> simp_all - case abs ih => exact ih (k + 1) - all_goals aesop + induction t <;> aesop /-- Specializes `close_var_not_fvar_rec` to first closing. -/ lemma close_var_not_fvar (x) (t : Term Var) : x ∉ (t ^* x).fv := close_var_not_fvar_rec x 0 t @@ -112,55 +89,47 @@ variable [HasFresh Var] omit [DecidableEq Var] in /-- A locally closed term is unchanged by opening. -/ +@[aesop safe (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])] lemma open_lc (k t) (e : Term Var) : e.LC → e = e⟦k ↝ t⟧ := by intros e_lc revert k - induction e_lc <;> intros k <;> simp only [openRec, app.injEq, abs.injEq] - case app => aesop - case abs xs e _ ih => refine open_lc_aux e 0 (fvar (fresh xs)) (k+1) t ?_ ?_ <;> aesop + induction e_lc + case abs xs e _ ih => + intros k + simp only [openRec_abs, abs.injEq] + refine open_lc_aux e 0 (fvar (fresh xs)) (k+1) t ?_ ?_ <;> aesop + all_goals aesop /-- Substitution of a locally closed term distributes with opening. -/ lemma subst_open (x : Var) (t : Term Var) (k : ℕ) (u e) : LC t → (e ⟦ k ↝ u ⟧) [ x := t ] = (e [ x := t ]) ⟦k ↝ u [ x := t ]⟧ := by revert k - induction' e - <;> intros k t_lv - <;> simp only [openRec, instHasSubstitutionTerm, subst, app.injEq, abs.injEq] - case bvar k' => aesop - case fvar x' => - split <;> simp_all - exact open_lc k (u[x':=t]) t t_lv - case abs ih => exact ih (k + 1) t_lv - case app ih_l ih_r => exact ⟨ih_l k t_lv, ih_r k t_lv⟩ + induction' e <;> aesop /-- Specialize `subst_open` to the first opening. -/ theorem subst_open_var (x y : Var) (u e : Term Var) : y ≠ x → LC u → (e [y := u]) ^ fvar x = (e ^ fvar x) [y := u] := by intros neq u_lc - have := subst_open y u 0 (fvar x) e u_lc + have h : (e ^ fvar x)[y:=u] = e[y:=u] ^ (fvar x)[y:=u] := subst_open y u 0 (fvar x) e u_lc aesop /-- Substitution of locally closed terms is locally closed. -/ theorem subst_lc {x : Var} {e u : Term Var} : LC e → LC u → LC (e [x := u]) := by intros lc_e lc_u - induction lc_e <;> simp only [instHasSubstitutionTerm, subst] - case fvar => split <;> [assumption; constructor] - case app ih_l ih_r => exact LC.app ih_l ih_r + induction lc_e case abs xs e _ ih => refine LC.abs ({x} ∪ xs) _ (?_ : ∀ y ∉ {x} ∪ xs, (e[x := u] ^ fvar y).LC) intros y mem rw [subst_open_var y x u e ?_ lc_u] - apply ih all_goals aesop + all_goals aesop /-- Opening to a term `t` is equivalent to opening to a free variable and substituting it for `t`. -/ lemma subst_intro (x : Var) (t e : Term Var) : x ∉ e.fv → LC t → e ^ t = (e ^ fvar x) [ x := t ] := by intros mem t_lc simp only [open'] - rw [subst_open x t 0 (fvar x) e t_lc] - have s := subst_fresh _ _ t mem - simp only [instHasSubstitutionTerm, subst, ↓reduceIte] at * - rw [s] + rw [subst_open x t 0 (fvar x) e t_lc, subst_fresh _ _ t mem] + aesop /-- Opening of locally closed terms is locally closed. -/ theorem beta_lc {M N : Term Var} : LC (abs M) → LC N → LC (M ^ N) := by @@ -174,23 +143,20 @@ theorem beta_lc {M N : Term Var} : LC (abs M) → LC N → LC (M ^ N) := by rw [subst_intro y N M] apply subst_lc apply mem - all_goals aesop + all_goals aesop /-- Opening then closing is equivalent to substitution. -/ lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) : LC m → m ⟦k ↜ x⟧⟦k ↝ fvar y⟧ = m [x := fvar y] := by intros m_lc revert k induction' m_lc - <;> intros k - <;> simp only [closeRec, openRec, instHasSubstitutionTerm, subst, abs.injEq, app.injEq] - case fvar x' => split <;> simp - case app ih_l ih_r => exact ⟨ih_l _, ih_r _⟩ case abs xs t x_mem ih => + intros k have ⟨x', x'_mem⟩ := fresh_exists ({x} ∪ {y} ∪ t.fv ∪ xs) have s := subst_open_var x' x (fvar y) t ?_ (by constructor) - simp only [open', Finset.union_assoc, Finset.mem_union, Finset.mem_singleton, not_or] at * - rw [←open_close x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ fvar y⟧) 0 ?f₁, ←open_close x' (t.subst x (fvar y)) 0 ?f₂] - simp [instHasSubstitutionTerm] at s + simp only [closeRec_abs, openRec_abs, subst_abs] + rw [←open_close x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ fvar y⟧) 0 ?f₁, ←open_close x' (t[x := fvar y]) 0 ?f₂] + simp only [open'] at * rw [swap_open_fvars, ←swap_open_fvar_close, s, ih] case f₁ => apply open_fresh_preserve_not_fvar @@ -200,14 +166,16 @@ lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) : LC m → m ⟦k apply subst_preserve_not_fvar aesop all_goals aesop + all_goals aesop /-- Closing and opening are inverses. -/ lemma close_open (x : Var) (t : Term Var) (k : ℕ) : LC t → t⟦k ↜ x⟧⟦k ↝ fvar x⟧ = t := by intros lc_t revert k - induction lc_t <;> intros k <;> simp only [closeRec, openRec, abs.injEq, app.injEq] - case fvar x' => split <;> simp_all + induction lc_t case abs xs t t_open_lc ih => + intros k + simp only [closeRec_abs, openRec_abs, abs.injEq] have ⟨y, hy⟩ := fresh_exists (xs ∪ t.fv ∪ (t⟦k + 1 ↜ x⟧⟦k + 1 ↝ fvar x⟧).fv ∪ {x}) simp only [Finset.union_assoc, Finset.mem_union, Finset.mem_singleton, not_or] at hy obtain ⟨q1, q2, q3, q4⟩ := hy @@ -216,4 +184,4 @@ lemma close_open (x : Var) (t : Term Var) (k : ℕ) : LC t → t⟦k ↜ x⟧⟦ simp only [open'] rw [swap_open_fvar_close, swap_open_fvars] all_goals aesop - case app => aesop + all_goals aesop diff --git a/Cslib/Semantics/ReductionSystem/Basic.lean b/Cslib/Semantics/ReductionSystem/Basic.lean index f5c277d1..0df9f59b 100644 --- a/Cslib/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Semantics/ReductionSystem/Basic.lean @@ -42,17 +42,13 @@ theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b) open Relation Relation.ReflTransGen --- these instance allow us to switch between single and multistep reductions in a `calc` block -instance {α} (R : α → α → Prop) : Trans R R (ReflTransGen R) where - trans hab hbc := head hab (single hbc) - +-- these instances allow us to switch between single and multistep reductions in a `calc` block instance {α} (R : α → α → Prop) : Trans R (ReflTransGen R) (ReflTransGen R) where trans := head instance {α} (R : α → α → Prop) : Trans (ReflTransGen R) R (ReflTransGen R) where trans := tail -instance (rs : ReductionSystem Term) : Trans rs.Red rs.Red rs.MRed := by infer_instance instance (rs : ReductionSystem Term) : Trans rs.Red rs.MRed rs.MRed := by infer_instance instance (rs : ReductionSystem Term) : Trans rs.MRed rs.Red rs.MRed := by infer_instance diff --git a/Cslib/Utils/Relation.lean b/Cslib/Utils/Relation.lean index 43ea0b19..ceaf7382 100644 --- a/Cslib/Utils/Relation.lean +++ b/Cslib/Utils/Relation.lean @@ -1,10 +1,45 @@ /- Copyright (c) 2025 Thomas Waring. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Thomas Waring +Authors: Thomas Waring, Chris Henson -/ import Mathlib.Logic.Relation +universe u + +variable {α : Type u} {R R' : α → α → Prop} + +/-- A relation has the diamond property when all reductions with a common origin are joinable -/ +abbrev Diamond (R : α → α → Prop) := ∀ {A B C : α}, R A B → R A C → (∃ D, R B D ∧ R C D) + +/-- A relation is confluent when its reflexive transitive closure has the diamond property. -/ +abbrev Confluence (R : α → α → Prop) := Diamond (Relation.ReflTransGen R) + +/-- Extending a multistep reduction by a single step preserves multi-joinability. -/ +lemma Relation.ReflTransGen.diamond_extend (h : Diamond R) : + Relation.ReflTransGen R A B → + R A C → + ∃ D, Relation.ReflTransGen R B D ∧ Relation.ReflTransGen R C D := by + intros AB _ + revert C + induction AB using Relation.ReflTransGen.head_induction_on <;> intros C AC + case refl => exact ⟨C, ⟨single AC, by rfl⟩⟩ + case head A'_C' _ ih => + obtain ⟨D, ⟨CD, C'_D⟩⟩ := h AC A'_C' + obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D + exact ⟨D', ⟨B_D', head CD D_D'⟩⟩ + +/-- The diamond property implies confluence. -/ +theorem Relation.ReflTransGen.diamond_confluence (h : Diamond R) : Confluence R := by + intros A B C AB BC + revert C + induction AB using Relation.ReflTransGen.head_induction_on <;> intros C BC + case refl => exists C + case head _ _ A'_C' _ ih => + obtain ⟨D, ⟨CD, C'_D⟩⟩ := diamond_extend h BC A'_C' + obtain ⟨D', ⟨B_D', D_D'⟩⟩ := ih C'_D + exact ⟨D', ⟨B_D', trans CD D_D'⟩⟩ + -- not sure why this doesn't compile as an "instance" but oh well def trans_of_subrelation {α : Type _} (s s' r : α → α → Prop) (hr : Transitive r) (h : ∀ a b : α, s a b → r a b) (h' : ∀ a b : α, s' a b → r a b) : Trans s s' r where diff --git a/CslibTests/ReductionSystem.lean b/CslibTests/ReductionSystem.lean index 727bcbc3..f31e6342 100644 --- a/CslibTests/ReductionSystem.lean +++ b/CslibTests/ReductionSystem.lean @@ -15,7 +15,7 @@ lemma multiple_step : 5 ↠ₙ 1 := by 5 ⭢ₙ 4 := by simp [h] _ ↠ₙ 2 := by calc - 4 ⭢ₙ 3 := by simp [h] + 4 ↠ₙ 3 := by apply ReductionSystem.MRed.single; simp [h] _ ⭢ₙ 2 := by simp [h] _ ⭢ₙ 1 := by simp [h]