|
| 1 | +/- |
| 2 | +Copyright (c) 2025 David Wegmann. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: David Wegmann |
| 5 | +-/ |
| 6 | + |
| 7 | + |
| 8 | +module |
| 9 | + |
| 10 | + |
| 11 | +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta |
| 12 | + |
| 13 | +set_option linter.unusedDecidableInType false |
| 14 | + |
| 15 | +@[expose] public section |
| 16 | + |
| 17 | +namespace Cslib |
| 18 | + |
| 19 | +universe u |
| 20 | + |
| 21 | +variable {Var : Type u} |
| 22 | + |
| 23 | +namespace LambdaCalculus.LocallyNameless.Untyped.Term |
| 24 | + |
| 25 | +/-- multiApp f [x₁, x₂, ..., xₙ] applies the arguments x₁, x₂, ..., xₙ |
| 26 | + to f in left-associative order, i.e. as (((f x₁) x₂) ... xₙ). -/ |
| 27 | +@[simp, scoped grind =] |
| 28 | +def multiApp (f : Term Var) : List (Term Var) → Term Var |
| 29 | +| [] => f |
| 30 | +| a :: as => Term.app (multiApp f as) a |
| 31 | + |
| 32 | +/-- A list of arguments performs a single reduction step |
| 33 | +
|
| 34 | + [x₁, ..., xᵢ ..., xₙ] ⭢βᶠ [x₁, ..., xᵢ', ..., xₙ] |
| 35 | +
|
| 36 | + if one of the arguments performs a single step xᵢ ⭢βᶠ xᵢ' |
| 37 | + and the rest of the arguments are locally closed. -/ |
| 38 | +@[scoped grind, reduction_sys "lβᶠ"] |
| 39 | +inductive ListFullBeta : List (Term Var) → List (Term Var) → Prop where |
| 40 | +/-- head of the list performs a single reduction step, the rest are locally closed -/ |
| 41 | +| step : N ⭢βᶠ N' → (∀ N ∈ Ns, LC N) → ListFullBeta (N :: Ns) (N' :: Ns) |
| 42 | +/-- given a list that already contains a step, we can add locally closed terms to the front -/ |
| 43 | +| cons : LC N → ListFullBeta Ns Ns' → ListFullBeta (N :: Ns) (N :: Ns') |
| 44 | + |
| 45 | +variable {M M' : Term Var} {Ns Ns' : List (Term Var)} |
| 46 | + |
| 47 | +/-- A term resulting from a multi-application is locally closed if |
| 48 | + and only if the leftmost term and all arguments applied to it are locally closed -/ |
| 49 | +@[scoped grind ←] |
| 50 | +lemma multiApp_lc : LC (M.multiApp Ns) ↔ LC M ∧ (∀ N ∈ Ns, LC N) := by |
| 51 | + induction Ns with grind [cases LC] |
| 52 | + |
| 53 | +/-- Just like ordinary beta reduction, the left-hand side |
| 54 | + of a multi-application step is locally closed -/ |
| 55 | +@[scoped grind ←] |
| 56 | +lemma step_multiApp_l (steps : M ⭢βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) : |
| 57 | + M.multiApp Ns ⭢βᶠ M'.multiApp Ns := by |
| 58 | + induction Ns <;> grind [FullBeta.appR] |
| 59 | + |
| 60 | +/-- Congruence lemma for multi reduction of the left most term of a multi-application -/ |
| 61 | +lemma steps_multiApp_l (steps : M ↠βᶠ M') (lc_Ns : ∀ N ∈ Ns, LC N) : |
| 62 | + M.multiApp Ns ↠βᶠ M'.multiApp Ns := by |
| 63 | + induction steps <;> grind |
| 64 | + |
| 65 | +/-- Congruence lemma for single reduction of one of the arguments of a multi-application -/ |
| 66 | +@[scoped grind ←] |
| 67 | +lemma step_multiApp_r (steps : Ns ⭢lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ⭢βᶠ M.multiApp Ns' := by |
| 68 | + induction steps <;> grind [FullBeta.appL, FullBeta.appR] |
| 69 | + |
| 70 | +/-- Congruence lemma for multiple reduction of one of the arguments of a multi-application -/ |
| 71 | +lemma steps_multiApp_r (steps : Ns ↠lβᶠ Ns') (lc_M : LC M) : M.multiApp Ns ↠βᶠ M.multiApp Ns' := by |
| 72 | + induction steps <;> grind [FullBeta.appL, FullBeta.appR] |
| 73 | + |
| 74 | +/-- If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then |
| 75 | + Q must be one of the following forms: |
| 76 | +
|
| 77 | + Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or |
| 78 | + Q = (λ M) N' P₁ ... Pₙ where N ⭢βᶠ N' or |
| 79 | + Q = (λ M) N P₁' ... Pₙ' where P_i ⭢βᶠ P_i' for some i or |
| 80 | + Q = (M ^ N) P₁ ... Pₙ -/ |
| 81 | +lemma invert_abs_multiApp_st {Ps} {M N Q : Term Var} |
| 82 | + (h_red : multiApp (M.abs.app N) Ps ⭢βᶠ Q) : |
| 83 | + (∃ M', M.abs ⭢βᶠ Term.abs M' ∧ Q = multiApp (M'.abs.app N) Ps) ∨ |
| 84 | + (∃ N', N ⭢βᶠ N' ∧ Q = multiApp (M.abs.app N') Ps) ∨ |
| 85 | + (∃ Ps', Ps ⭢lβᶠ Ps' ∧ Q = multiApp (M.abs.app N) Ps') ∨ |
| 86 | + (Q = multiApp (M ^ N) Ps) := by |
| 87 | + induction Ps generalizing M N Q with |
| 88 | + | nil => grind [cases FullBeta] |
| 89 | + | cons P Ps ih => |
| 90 | + generalize Heq : (M.abs.app N).multiApp Ps = Q' |
| 91 | + have : ∀ P', Q'.app P' = (M.abs.app N).multiApp (P' :: Ps) := by grind |
| 92 | + rw [multiApp, Heq] at h_red |
| 93 | + cases h_red with |
| 94 | + | beta => cases Ps <;> contradiction |
| 95 | + | appR => grind [→ ListFullBeta.cons] |
| 96 | + | appL => grind |
| 97 | + |
| 98 | +/-- If a term (λ M) N P₁ ... Pₙ reduces in multiple steps to Q, then either Q if of the form |
| 99 | +
|
| 100 | + Q = (λ M') N' P'₁ ... P'ₙ |
| 101 | +
|
| 102 | + or |
| 103 | +
|
| 104 | + we first reach an intermediate term of this shape, |
| 105 | +
|
| 106 | + (λ M) N P₁ ... Pₙ ↠βᶠ (λ M') N' P'₁ ... P'ₙ |
| 107 | +
|
| 108 | + then perform a beta reduction and reduce further to Q |
| 109 | +
|
| 110 | + (λ M') N' P'₁ ... P'ₙ ↠βᶠ M' ^ N' P'_₁ ... P'_ₙ ↠βᶠ Q |
| 111 | +
|
| 112 | + where M ↠βᶠ M' and N ↠βᶠ N' and P_i ↠βᶠ P_i' for all i -/ |
| 113 | +lemma invert_abs_multiApp_mst {Ps} {M N Q : Term Var} |
| 114 | + (h_red : multiApp (M.abs.app N) Ps ↠βᶠ Q) : |
| 115 | + ∃ M' N' Ns', M.abs ↠βᶠ M'.abs ∧ N ↠βᶠ N' ∧ Ps ↠lβᶠ Ns' ∧ |
| 116 | + (Q = multiApp (M'.abs.app N') Ns' ∨ |
| 117 | + (multiApp (M.abs.app N) Ps ↠βᶠ multiApp (M' ^ N') Ns' ∧ |
| 118 | + multiApp (M' ^ N') Ns' ↠βᶠ Q)) := by |
| 119 | + induction h_red with |
| 120 | + | refl => grind |
| 121 | + | tail _ step ih => |
| 122 | + obtain ⟨_, _, _, _, _, _, h⟩ := ih |
| 123 | + rcases h with heq | _ |
| 124 | + · subst heq |
| 125 | + grind [invert_abs_multiApp_st step] |
| 126 | + · grind [Relation.ReflTransGen.single] |
| 127 | + |
| 128 | +variable [DecidableEq Var] [HasFresh Var] |
| 129 | + |
| 130 | +/-- Just like ordinary beta reduction, the right-hand side |
| 131 | + of a multi-application step is locally closed -/ |
| 132 | +lemma multiApp_step_lc_r (step : Ns ⭢lβᶠ Ns') : ∀ N ∈ Ns', LC N := by |
| 133 | + induction step <;> grind [FullBeta.step_lc_r] |
| 134 | + |
| 135 | +/-- Just like ordinary beta reduction, multiple steps of a argument list preserves local closure -/ |
| 136 | +lemma multiApp_steps_lc (step : Ns ↠lβᶠ Ns') (H : ∀ N ∈ Ns, LC N) : ∀ N ∈ Ns', LC N := by |
| 137 | + induction step <;> grind [FullBeta.step_lc_r, multiApp_step_lc_r] |
| 138 | + |
| 139 | +end LambdaCalculus.LocallyNameless.Untyped.Term |
| 140 | + |
| 141 | +end Cslib |
0 commit comments