diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index 6b1e8f387f..03cdfe2d80 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -66,7 +66,8 @@ lemma semanticMap_saturated (τ : Ty Base) : @Saturated Var (semanticMap τ) := · grind [sn_app_left (Var := Var) (N := fvar <| fresh {})] · grind · intro M N P _ _ _ s _ - grind [ih₂.multiApp M N (P ++ [s]), multiApp_tail] + grind only [semanticMap, = List.foldl_append, = List.foldl_cons, usr Set.mem_ofPred_eq, + = List.foldl_nil, ih₂.multiApp M N (P ++ [s])] /-- The `entailsContext` predicate ensures that each variable in the context is mapped to a term in the corresponding semantic map. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean index 509b4a52c6..6737deb297 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean @@ -26,9 +26,7 @@ namespace LambdaCalculus.LocallyNameless.Untyped.Term /-- multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ). -/ @[simp, scoped grind =] -def multiApp (f : Term Var) : List (Term Var) → Term Var -| [] => f -| a :: as => multiApp (app f a) as +abbrev multiApp (f : Term Var) (Ns : List (Term Var)) := Ns.foldl app f /-- A list of arguments performs a single reduction step @@ -45,16 +43,11 @@ inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where variable {M M' : Term Var} {Ns Ns' : List (Term Var)} -lemma multiApp_tail {N} : (M.multiApp (Ns ++ [N])) = (M.multiApp Ns).app N:= by - induction Ns generalizing M with - | nil => grind - | cons head tail ih => rw [List.cons_append]; apply ih - /-- A term resulting from a multi-application is locally closed if and only if the leftmost term and all arguments applied to it are locally closed -/ @[scoped grind ←] lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by - induction Ns generalizing M with grind [cases LC] + induction Ns using List.reverseRecOn with grind [cases LC] /-- Just like ordinary beta reduction, the left-hand side of a multi-application step is locally closed -/ @@ -71,6 +64,22 @@ lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) : M.multiApp Ns ↠βᶠ M'.multiApp Ns := by induction steps <;> grind +lemma step_multiApp_l_union {R1 R2} (step : (Xi R1 ⊔ Xi R2) M M') (lc_Ns : ∀ N ∈ Ns, LC N) : + (Xi R1 ⊔ Xi R2) (multiApp M Ns) (multiApp M' Ns) := by + induction Ns generalizing M M' with + | nil => grind + | cons head tail ih => + apply ih ?_ (by grind) + cases step with + | inl h => left; grind + | inr h => right; grind + +lemma steps_multiApp_l_union {R1 R2} + (steps : Relation.ReflTransGen (Xi R1 ⊔ Xi R2) M M') + (lc_Ns : ∀ N ∈ Ns, LC N) : + Relation.ReflTransGen (Xi R1 ⊔ Xi R2) (multiApp M Ns) (multiApp M' Ns) := by + induction steps <;> grind [step_multiApp_l_union] + /-- 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 @@ -80,12 +89,33 @@ lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by induction steps <;> grind -lemma listFullBeta_cons_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by +lemma multiapp_openRec {i} : + (multiApp M Ns)⟦i ↝ M'⟧ = multiApp (M⟦i ↝ M'⟧) (Ns.map (openRec i M')) := by + induction Ns generalizing M with + | nil => grind + | cons head tail ih => grind [@ih (M.app head)] + +lemma multiapp_fv [DecidableEq Var] : (multiApp M Ns).fv = (Ns.map fv).foldl Union.union M.fv := by + induction Ns generalizing M with + | nil => grind + | cons head tail ih => grind [@ih (M.app head)] + +lemma listFullBeta_append_r (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : + (l ++ Ns) ⭢lβᶠ (l ++ Ns') := by induction l using List.reverseRecOn generalizing Ns Ns' with grind -lemma listFullBeta_cons_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by +lemma listFullBeta_append_l (h : Ns ⭢lβᶠ Ns') (h_lc : ∀ M ∈ l, LC M) : + (Ns ++ l) ⭢lβᶠ (Ns' ++ l) := by induction h with grind +lemma listFullBeta_cons_r (h : Ns ↠lβᶠ Ns') (h_lc : LC M) : (M :: Ns) ↠lβᶠ (M :: Ns') := by + induction h with grind + +lemma listFullBeta_cons_l (h : M ↠βᶠ M') (h_lc : ∀ M ∈ Ns, LC M) : (M :: Ns) ↠lβᶠ (M' :: Ns) := by + induction h with + | refl => grind + | tail _ h ih => exact .tail ih (.step h h_lc) + set_option linter.tacticAnalysis.verifyGrindOnly false in /-- 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: @@ -101,17 +131,17 @@ 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 using List.reverseRecOn generalizing M N Q with - | nil => grind only [cases Xi, multiApp] + | nil => grind [cases Xi] | append_singleton Ps P ih => - rw [multiApp_tail] at h_red + simp only [List.foldl_concat] at h_red cases h_red with | @appL _ _ P' _ P_P' => - have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_cons_r (.step P_P' ?_) <;> grind - grind [multiApp_tail] + have : (Ps ++ [P]) ⭢lβᶠ Ps ++ [P'] := by apply listFullBeta_append_r (.step P_P' ?_) <;> grind + grind | appR _ h => - have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_cons_l h (by grind) - grind [multiApp_tail] - | base => induction Ps using List.reverseRecOn with grind [multiApp_tail] + have {Ps'} (h : Ps ⭢lβᶠ Ps') : (Ps ++ [P]) ⭢lβᶠ Ps' ++ [P] := listFullBeta_append_l h (by grind) + grind + | base => induction Ps using List.reverseRecOn with grind /-- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index b54be7de11..1654c8d5d2 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -129,16 +129,16 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var} · exact sn_N · grind [→ steps_open_cong_abs, open_abs_lc, sn_steps] | append_singleton Ps P ih => - rw [multiApp_tail] + simp only [List.foldl_concat] apply sn_app - · rw [multiApp_tail] at sn_MNPs lc_MNPs + · simp only [List.foldl_concat] at sn_MNPs lc_MNPs cases lc_MNPs grind [sn_app_left] - · grind [multiApp_tail, sn_app_right] + · grind [sn_app_right] · intro Q' P' hstep1 hstep2 have ⟨M', N', Ps', h_M_red, h_N_red, h_Ps_red, h_cases⟩ := invert_abs_multiApp_mst hstep1 rcases h_cases with h_P | ⟨h_st1, h_st2⟩ - · induction Ps' using List.reverseRecOn with grind [multiApp_tail] + · induction Ps' using List.reverseRecOn with grind · have innerSteps : (M ^ N).multiApp Ps ↠βᶠ (M' ^ N').multiApp Ps' := by trans · exact steps_multiApp_r h_Ps_red (by grind) @@ -146,7 +146,7 @@ lemma sn_abs_app_multiApp [DecidableEq Var] [HasFresh Var] {Ps} {M N : Term Var} · apply steps_open_cong_abs M M' N N' <;> grind [open_abs_lc] · grind [multiApp_steps_lc] refine sn_steps ?_ sn_MNPs - rw [multiApp_tail] + simp only [List.foldl_concat] · 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)