From 5d5adcb78e9e395c37a053a74eb86a374fc30367 Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Sat, 8 Aug 2026 12:31:41 +0700 Subject: [PATCH] =?UTF-8?q?feat(#20):=20Replace=20=E2=96=A1=20with=20a=20d?= =?UTF-8?q?ot-like=20Unicode=20symbol=20=E2=AC=9D=20for=20term=20applicati?= =?UTF-8?q?on=20(Black=20Very=20Small=20Square,=20U+2B1D,=20\tr=20,=20\con?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .vscode/settings.json | 4 +- Plfl/DeBruijn.lean | 40 ++++----- Plfl/Lambda.lean | 70 +++++++-------- Plfl/Lambda/Properties.lean | 20 ++--- Plfl/More.lean | 42 ++++----- Plfl/More/Bisimulation.lean | 2 +- Plfl/More/DoubleSubst.lean | 10 +-- Plfl/More/Inference.lean | 26 +++--- Plfl/Untyped.lean | 92 ++++++++++---------- Plfl/Untyped/BigStep.lean | 16 ++-- Plfl/Untyped/Confluence.lean | 24 ++--- Plfl/Untyped/Denotational.lean | 6 +- Plfl/Untyped/Denotational/Adequacy.lean | 2 +- Plfl/Untyped/Denotational/Compositional.lean | 18 ++-- Plfl/Untyped/Denotational/Soundness.lean | 6 +- Plfl/Untyped/Substitution.lean | 12 +-- 16 files changed, 195 insertions(+), 195 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 1406c16..86c4cb4 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -13,8 +13,8 @@ "~~": "~~", "~~e": "~~ₑ", "$n": "$ₙ", - "ap": "□", - "apn": "□ₙ", + "ap": "⬝", + "apn": "⬝ₙ", "d-": "↧", "d2": "￬", "Fun": "ƛ", diff --git a/Plfl/DeBruijn.lean b/Plfl/DeBruijn.lean index c50c6b0..b95f827 100644 --- a/Plfl/DeBruijn.lean +++ b/Plfl/DeBruijn.lean @@ -84,7 +84,7 @@ namespace Term prefix:50 "μ " => mu notation "𝟘? " => case infixr:min " $ " => ap - infixl:70 " □ " => ap + infixl:70 " ⬝ " => ap prefix:80 "ι " => succ prefix:90 "‵" => var notation "𝟘" => zero @@ -110,10 +110,10 @@ namespace Term example : Γ ⊢ ℕt := ι ι 𝟘 example : Γ ⊢ ℕt := 2 - @[simp] abbrev add : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) (#0) (ι (#3 □ #0 □ #1))) - @[simp] abbrev mul : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) 𝟘 (add □ #1 $ #3 □ #0 □ #1)) + @[simp] abbrev add : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) (#0) (ι (#3 ⬝ #0 ⬝ #1))) + @[simp] abbrev mul : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) 𝟘 (add ⬝ #1 $ #3 ⬝ #0 ⬝ #1)) - example : Γ ⊢ ℕt := add □ 2 □ 2 + example : Γ ⊢ ℕt := add ⬝ 2 ⬝ 2 /-- The Church numeral Ty. @@ -122,11 +122,11 @@ namespace Term @[simp] abbrev succC : Γ ⊢ ℕt =⇒ ℕt := ƛ ι #0 @[simp] abbrev twoC : Γ ⊢ Ch a := ƛ ƛ (#1 $ #1 $ #0) - @[simp] abbrev addC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 □ #1 $ #2 □ #1 □ #0) - example : Γ ⊢ ℕt := addC □ twoC □ twoC □ succC □ 𝟘 + @[simp] abbrev addC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 ⬝ #1 $ #2 ⬝ #1 ⬝ #0) + example : Γ ⊢ ℕt := addC ⬝ twoC ⬝ twoC ⬝ succC ⬝ 𝟘 -- https://plfa.github.io/DeBruijn/#exercise-mul-recommended - @[simp] abbrev mulC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 □ (#2 □ #1) □ #0) + @[simp] abbrev mulC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 ⬝ (#2 ⬝ #1) ⬝ #0) end Term -- https://plfa.github.io/DeBruijn/#renaming @@ -147,7 +147,7 @@ def rename : (∀ {a}, Γ ∋ a → Δ ∋ a) → Γ ⊢ a → Δ ⊢ a := by intro ρ; intro | ‵ x => exact ‵ (ρ x) | ƛ n => refine .lam ?_; refine rename ?_ n; exact ext ρ - | l □ m => + | l ⬝ m => apply Term.ap · exact rename ρ l · exact rename ρ m @@ -186,7 +186,7 @@ def subst : (∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ ⊢ a → Δ ⊢ a := by intro σ; intro | ‵ x => exact σ x | ƛ n => refine .lam ?_; refine subst ?_ n; exact exts σ - | l □ m => + | l ⬝ m => apply Term.ap · exact subst σ l · exact subst σ m @@ -212,7 +212,7 @@ notation:90 n "⟦" m "⟧" => subst₁ m n example : let m : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ι #0) let m' : ∅‚ ℕt =⇒ ℕt ⊢ ℕt =⇒ ℕt := ƛ (#1 $ #1 $ #0) - let n : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ƛ ι #0) □ ((ƛ ι #0) □ #0) + let n : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ƛ ι #0) ⬝ ((ƛ ι #0) ⬝ #0) m'⟦m⟧ = n := rfl @@ -242,9 +242,9 @@ end Value `Reduce t t'` says that `t` reduces to `t'`. -/ inductive Reduce : (Γ ⊢ a) → (Γ ⊢ a) → Type where -| lamβ : Value w → Reduce ((ƛ n) □ w) (n⟦w⟧) -| apξ₁ : Reduce l l' → Reduce (l □ m) (l' □ m) -| apξ₂ : Value v → Reduce m m' → Reduce (v □ m) (v □ m') +| lamβ : Value w → Reduce ((ƛ n) ⬝ w) (n⟦w⟧) +| apξ₁ : Reduce l l' → Reduce (l ⬝ m) (l' ⬝ m) +| apξ₂ : Value v → Reduce m m' → Reduce (v ⬝ m) (v ⬝ m') | zeroβ : Reduce (𝟘? 𝟘 m n) m | succβ : Value v → Reduce (𝟘? (ι v) m n) (n⟦v⟧) | succξ : Reduce m m' → Reduce (ι m) (ι m') @@ -299,11 +299,11 @@ namespace Reduce open Term -- https://plfa.github.io/DeBruijn/#examples - example : twoC □ succC □ @zero ∅ —↠ 2 := calc - twoC □ succC □ 𝟘 - _ —→ (ƛ (succC $ succC $ #0)) □ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam + example : twoC ⬝ succC ⬝ @zero ∅ —↠ 2 := calc + twoC ⬝ succC ⬝ 𝟘 + _ —→ (ƛ (succC $ succC $ #0)) ⬝ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam _ —→ (succC $ succC $ 𝟘) := by apply lamβ; exact V𝟘 - _ —→ succC □ 1 := by + _ —→ succC ⬝ 1 := by apply apξ₂ · apply Value.lam · unfold succC; exact lamβ V𝟘 @@ -332,7 +332,7 @@ def progress : (m : ∅ ⊢ a) → Progress m := open Progress Reduce in by intro | ‵ _ => contradiction | ƛ _ => exact .done Value.lam - | jl □ jm => cases progress jl with + | jl ⬝ jm => cases progress jl with | step => apply step; · apply apξ₁; trivial | done vl => cases progress jm with | step => apply step; apply apξ₂ <;> trivial @@ -382,12 +382,12 @@ info: DeBruijn.Result.dnf info: DeBruijn.Result.done (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.zero))))) -/ -#guard_msgs in #eval eval 100 (add □ 2 □ 2) |> (·.3) +#guard_msgs in #eval eval 100 (add ⬝ 2 ⬝ 2) |> (·.3) /-- info: DeBruijn.Result.done (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.zero))))))) -/ -#guard_msgs in #eval eval 100 (mul □ 2 □ 3) |> (·.3) +#guard_msgs in #eval eval 100 (mul ⬝ 2 ⬝ 3) |> (·.3) end examples diff --git a/Plfl/Lambda.lean b/Plfl/Lambda.lean index 23192c5..cac4402 100644 --- a/Plfl/Lambda.lean +++ b/Plfl/Lambda.lean @@ -30,7 +30,7 @@ namespace Term notation:50 " μ " v " : " d => mu v d notation:max "𝟘? " e " [zero: " o " |succ " n " : " i " ] " => case e o n i infixr:min " $ " => ap - infixl:70 " □ " => ap + infixl:70 " ⬝ " => ap prefix:80 "ι " => succ prefix:90 "‵" => var notation "𝟘" => zero @@ -45,17 +45,17 @@ namespace Term example : Term := 1 example : Term := 42 - abbrev add : Term := μ "+" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (‵"+" □ ‵"m" □ ‵"n")] + abbrev add : Term := μ "+" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (‵"+" ⬝ ‵"m" ⬝ ‵"n")] -- https://plfa.github.io/Lambda/#exercise-mul-recommended - abbrev mul : Term := μ "*" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: 𝟘 |succ "m": add □ ‵"n" $ ‵"*" □ ‵"m" □ ‵"n"] + abbrev mul : Term := μ "*" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: 𝟘 |succ "m": add ⬝ ‵"n" $ ‵"*" ⬝ ‵"m" ⬝ ‵"n"] -- Church encoding... abbrev succC : Term := ƛ "n" : ι ‵"n" abbrev oneC : Term := ƛ "s" : ƛ "z" : ‵"s" $ ‵"z" abbrev twoC : Term := ƛ "s" : ƛ "z" : ‵"s" $ ‵"s" $ ‵"z" - abbrev addC : Term := ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" □ ‵"s" $ ‵"n" □ ‵"s" □ ‵"z" + abbrev addC : Term := ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" ⬝ ‵"s" $ ‵"n" ⬝ ‵"s" ⬝ ‵"z" -- https://plfa.github.io/Lambda/#exercise-mul%E1%B6%9C-practice - abbrev mulC : Term := ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" □ (‵"n" □ ‵"s") □ ‵"z" + abbrev mulC : Term := ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" ⬝ (‵"n" ⬝ ‵"s") ⬝ ‵"z" end Term -- https://plfa.github.io/Lambda/#values @@ -96,10 +96,10 @@ namespace Term -- https://plfa.github.io/Lambda/#examples example - : (ƛ "z" : ‵"s" □ ‵"s" □ ‵"z")["s" := succC] - = (ƛ "z" : succC □ succC □ ‵"z") := rfl + : (ƛ "z" : ‵"s" ⬝ ‵"s" ⬝ ‵"z")["s" := succC] + = (ƛ "z" : succC ⬝ succC ⬝ ‵"z") := rfl - example : (succC □ succC □ ‵"z")["z" := 𝟘] = succC □ succC □ 𝟘 := rfl + example : (succC ⬝ succC ⬝ ‵"z")["z" := 𝟘] = succC ⬝ succC ⬝ 𝟘 := rfl example : (ƛ "x" : ‵"y")["y" := 𝟘] = (ƛ "x" : 𝟘) := rfl example : (ƛ "x" : ‵"x")["x" := 𝟘] = (ƛ "x" : ‵"x") := rfl example : (ƛ "y" : ‵"y")["x" := 𝟘] = (ƛ "y" : ‵"y") := rfl @@ -115,9 +115,9 @@ namespace Term `Reduce t t'` says that `t` reduces to `t'`. -/ inductive Reduce : Term → Term → Type where - | lamβ : Value v → Reduce ((ƛ x : n) □ v) (n[x := v]) - | apξ₁ : Reduce l l' → Reduce (l □ m) (l' □ m) - | apξ₂ : Value v → Reduce m m' → Reduce (v □ m) (v □ m') + | lamβ : Value v → Reduce ((ƛ x : n) ⬝ v) (n[x := v]) + | apξ₁ : Reduce l l' → Reduce (l ⬝ m) (l' ⬝ m) + | apξ₂ : Value v → Reduce m m' → Reduce (v ⬝ m) (v ⬝ m') | zeroβ : Reduce (𝟘? 𝟘 [zero: m |succ x : n]) m | succβ : Value v → Reduce (𝟘? ι v [zero: m |succ x : n]) (n[x := v]) | succξ : Reduce m m' → Reduce (ι m) (ι m') @@ -130,13 +130,13 @@ end Term namespace Term.Reduce -- https://plfa.github.io/Lambda/#quiz-1 - example : (ƛ "x" : ‵"x") □ (ƛ "x" : ‵"x") —→ (ƛ "x" : ‵"x") := by + example : (ƛ "x" : ‵"x") ⬝ (ƛ "x" : ‵"x") —→ (ƛ "x" : ‵"x") := by apply lamβ; exact Value.lam - example : (ƛ "x" : ‵"x") □ (ƛ "x" : ‵"x") □ (ƛ "x" : ‵"x") —→ (ƛ "x" : ‵"x") □ (ƛ "x" : ‵"x") := by + example : (ƛ "x" : ‵"x") ⬝ (ƛ "x" : ‵"x") ⬝ (ƛ "x" : ‵"x") —→ (ƛ "x" : ‵"x") ⬝ (ƛ "x" : ‵"x") := by apply apξ₁; apply lamβ; exact Value.lam - example : twoC □ succC □ 𝟘 —→ (ƛ "z" : succC $ succC $ ‵"z") □ 𝟘 := by + example : twoC ⬝ succC ⬝ 𝟘 —→ (ƛ "z" : succC $ succC $ ‵"z") ⬝ 𝟘 := by unfold twoC; apply apξ₁; apply lamβ; exact Value.lam -- https://plfa.github.io/Lambda/#reflexive-and-transitive-closure @@ -246,29 +246,29 @@ end confluence section examples open Term Term.Reduce Term.Reduce.Clos - example : twoC □ succC □ 𝟘 —↠ 2 := calc - twoC □ succC □ 𝟘 - _ —→ (ƛ "z" : succC $ succC $ ‵"z") □ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam + example : twoC ⬝ succC ⬝ 𝟘 —↠ 2 := calc + twoC ⬝ succC ⬝ 𝟘 + _ —→ (ƛ "z" : succC $ succC $ ‵"z") ⬝ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam _ —→ (succC $ succC $ 𝟘) := by apply lamβ; exact Value.zero - _ —→ succC □ 1 := by apply apξ₂; apply Value.lam; apply lamβ; exact Value.zero + _ —→ succC ⬝ 1 := by apply apξ₂; apply Value.lam; apply lamβ; exact Value.zero _ —→ 2 := by apply lamβ; exact Value.ofNat 1 -- https://plfa.github.io/Lambda/#exercise-plus-example-practice - example : add □ 1 □ 1 —↠ 2 := calc - add □ 1 □ 1 - _ —→ (ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (add □ ‵"m" □ ‵"n")]) □ 1 □ 1 + example : add ⬝ 1 ⬝ 1 —↠ 2 := calc + add ⬝ 1 ⬝ 1 + _ —→ (ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (add ⬝ ‵"m" ⬝ ‵"n")]) ⬝ 1 ⬝ 1 := by apply apξ₁; apply apξ₁; apply muβ - _ —↠ (ƛ "n" : 𝟘? 1 [zero: ‵"n" |succ "m": ι (add □ ‵"m" □ ‵"n")]) □ 1 + _ —↠ (ƛ "n" : 𝟘? 1 [zero: ‵"n" |succ "m": ι (add ⬝ ‵"m" ⬝ ‵"n")]) ⬝ 1 := .one <| by apply apξ₁; apply lamβ; exact Value.ofNat 1 - _ —→ 𝟘? 1 [zero: 1 |succ "m": ι (add □ ‵"m" □ 1)] + _ —→ 𝟘? 1 [zero: 1 |succ "m": ι (add ⬝ ‵"m" ⬝ 1)] := lamβ <| Value.ofNat 1 - _ —→ ι (add □ 𝟘 □ 1) + _ —→ ι (add ⬝ 𝟘 ⬝ 1) := succβ Value.zero - _ —→ ι ((ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (add □ ‵"m" □ ‵"n")]) □ 𝟘 □ 1) + _ —→ ι ((ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (add ⬝ ‵"m" ⬝ ‵"n")]) ⬝ 𝟘 ⬝ 1) := by apply succξ; apply apξ₁; apply apξ₁; apply muβ - _ —→ ι ((ƛ "n" : 𝟘? 𝟘 [zero: ‵"n" |succ "m": ι (add □ ‵"m" □ ‵"n")]) □ 1) + _ —→ ι ((ƛ "n" : 𝟘? 𝟘 [zero: ‵"n" |succ "m": ι (add ⬝ ‵"m" ⬝ ‵"n")]) ⬝ 1) := by apply succξ; apply apξ₁; apply lamβ; exact V𝟘 - _ —→ ι (𝟘? 𝟘 [zero: 1 |succ "m": ι (add □ ‵"m" □ 1)]) + _ —→ ι (𝟘? 𝟘 [zero: 1 |succ "m": ι (add ⬝ ‵"m" ⬝ 1)]) := by apply succξ; apply lamβ; exact Value.ofNat 1 _ —→ 2 := succξ zeroβ end examples @@ -343,7 +343,7 @@ namespace Context inductive IsTy : Context → Term → Ty → Type where | tyVar : Γ ∋ x ⦂ t → IsTy Γ (‵x) t | tyLam : IsTy (Γ‚ x ⦂ t) n u → IsTy Γ (ƛ x : n) (t =⇒ u) - | tyAp : IsTy Γ l (t =⇒ u) → IsTy Γ x t → IsTy Γ (l □ x) u + | tyAp : IsTy Γ l (t =⇒ u) → IsTy Γ x t → IsTy Γ (l ⬝ x) u | tyZero : IsTy Γ 𝟘 ℕt | tySucc : IsTy Γ n ℕt → IsTy Γ (ι n) ℕt | tyCase : IsTy Γ l ℕt → IsTy Γ m t → IsTy (Γ‚ x ⦂ ℕt) n t → IsTy Γ (𝟘? l [zero: m |succ x: n]) t @@ -383,7 +383,7 @@ namespace Context · trivial · exact tyZero - def two_ty : Γ ⊢ (ƛ "s" : ‵"s" $ ‵"s" $ 𝟘) □ succC ⦂ ℕt := by + def two_ty : Γ ⊢ (ƛ "s" : ‵"s" $ ‵"s" $ 𝟘) ⬝ succC ⦂ ℕt := by apply tyAp twice_ty · apply tyLam; apply tySucc; trivial @@ -416,25 +416,25 @@ section examples open Term Context Lookup Context.IsTy -- https://plfa.github.io/Lambda/#non-examples - example : ∅ ⊬ 𝟘 □ 1 := + example : ∅ ⊬ 𝟘 ⬝ 1 := ⟨fun | .tyAp hl _ => by cases hl⟩ - abbrev illLam := ƛ "x" : ‵"x" □ ‵"x" + abbrev illLam := ƛ "x" : ‵"x" ⬝ ‵"x" lemma nty_illLam : ∅ ⊬ illLam := ⟨fun | .tyLam (.tyAp (.tyVar hx) (.tyVar hx')) => Ty.t_to_t'_ne_t _ _ (Lookup.functional hx hx')⟩ -- https://plfa.github.io/Lambda/#quiz-3 - example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊢ ‵"y" □ ‵"x" ⦂ ℕt := by + example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊢ ‵"y" ⬝ ‵"x" ⦂ ℕt := by apply tyAp <;> trivial - example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊬ ‵"x" □ ‵"y" := + example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊬ ‵"x" ⬝ ‵"y" := ⟨fun | .tyAp (.tyVar hx) _ => by cases hx with | s _ _ => contradiction⟩ - example : ∅‚ "y" ⦂ ℕt =⇒ ℕt ⊢ ƛ "x" : ‵"y" □ ‵"x" ⦂ ℕt =⇒ ℕt := by + example : ∅‚ "y" ⦂ ℕt =⇒ ℕt ⊢ ƛ "x" : ‵"y" ⬝ ‵"x" ⦂ ℕt =⇒ ℕt := by apply tyLam; apply tyAp <;> trivial - example : ∅‚ "x" ⦂ t ⊬ ‵"x" □ ‵"x" := + example : ∅‚ "x" ⦂ t ⊬ ‵"x" ⬝ ‵"x" := ⟨fun | .tyAp (.tyVar .z) (.tyVar (.s _ _)) => by contradiction | .tyAp (.tyVar (.s _ _)) _ => by contradiction⟩ diff --git a/Plfl/Lambda/Properties.lean b/Plfl/Lambda/Properties.lean index 0e22257..eeaa424 100644 --- a/Plfl/Lambda/Properties.lean +++ b/Plfl/Lambda/Properties.lean @@ -328,7 +328,7 @@ section examples -/ #guard_msgs in #eval eval 3 tySuccμ |>.3 - abbrev add_2_2 := add □ 2 □ 2 + abbrev add_2_2 := add ⬝ 2 ⬝ 2 abbrev two_ty : ∅ ⊢ 2 ⦂ ℕt := by iterate 2 (apply tySucc) @@ -372,7 +372,7 @@ section subject_expansion example : IsEmpty (∀ {n t m}, ∅ ⊢ n ⦂ t → (m —→ n) → ∅ ⊢ m ⦂ t) := by by_contra f simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff] - let illAp := (ƛ "x" : 𝟘) □ illLam + let illAp := (ƛ "x" : 𝟘) ⬝ illLam have nty_ill : ∅ ⊬ illAp := by intro tt refine ⟨fun j => ?_⟩ @@ -462,8 +462,8 @@ Which of the following properties remain true in the presence of these rules? Fo * Determinism Becomes false. -The term `(ƛ x ⇒ `"x") □ 𝟘` can both be reduced via: -· apξ₁, to zap □ 𝟘 +The term `(ƛ x ⇒ `"x") ⬝ 𝟘` can both be reduced via: +· apξ₁, to zap ⬝ 𝟘 · zepβ, to zap ... and they're not equal. @@ -488,17 +488,17 @@ Which of the following properties remain true in the presence of this rule? For Becomes false. -The term `(ƛ x ⇒ `"x") □ 𝟘` can both be reduced via: -· apξ₁, to foo □ 𝟘 +The term `(ƛ x ⇒ `"x") ⬝ 𝟘` can both be reduced via: +· apξ₁, to foo ⬝ 𝟘 · lamβ, to `"x" ... and they're not equal. * Progress Becomes false. -The term `(ƛ x ⇒ `"x") □ 𝟘` can be reduced via: -· apξ₁ fooβ₁, to foo □ 𝟘 -· then apξ₁ fooβ₂, to 𝟘 □ 𝟘 +The term `(ƛ x ⇒ `"x") ⬝ 𝟘` can be reduced via: +· apξ₁ fooβ₁, to foo ⬝ 𝟘 +· then apξ₁ fooβ₂, to 𝟘 ⬝ 𝟘 ... and now the term get's stuck. * Preservation @@ -522,7 +522,7 @@ Remains true. * Progress Becomes false. -The term `(ƛ x ⇒ `"x") □ 𝟘` is well-typed but gets stucked. +The term `(ƛ x ⇒ `"x") ⬝ 𝟘` is well-typed but gets stucked. -/ -- https://plfa.github.io/Properties/#quiz-3 diff --git a/Plfl/More.lean b/Plfl/More.lean index 96ce053..698d342 100644 --- a/Plfl/More.lean +++ b/Plfl/More.lean @@ -151,7 +151,7 @@ namespace Notation scoped prefix:50 "μ " => mu scoped notation "𝟘? " => case scoped infixr:min " $ " => ap - scoped infixl:70 " □ " => ap + scoped infixl:70 " ⬝ " => ap scoped infixl:70 " ⋄ " => mulP scoped prefix:80 "ι " => succ scoped prefix:90 "‵" => var @@ -181,8 +181,8 @@ namespace Term example : Γ ⊢ ℕt := ι ι 𝟘 example : Γ ⊢ ℕt := 2 - @[simp] abbrev add : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) (#0) (ι (#3 □ #0 □ #1))) - abbrev four : Γ ⊢ ℕt := add □ 2 □ 2 + @[simp] abbrev add : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) (#0) (ι (#3 ⬝ #0 ⬝ #1))) + abbrev four : Γ ⊢ ℕt := add ⬝ 2 ⬝ 2 /-- The Church numeral Ty. @@ -191,14 +191,14 @@ namespace Term @[simp] abbrev succC : Γ ⊢ ℕt =⇒ ℕt := ƛ ι #0 @[simp] abbrev twoC : Γ ⊢ Ch a := ƛ ƛ (#1 $ #1 $ #0) - @[simp] abbrev addC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 □ #1 $ #2 □ #1 □ #0) - abbrev four' : Γ ⊢ ℕt := addC □ twoC □ twoC □ succC □ 𝟘 + @[simp] abbrev addC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 ⬝ #1 $ #2 ⬝ #1 ⬝ #0) + abbrev four' : Γ ⊢ ℕt := addC ⬝ twoC ⬝ twoC ⬝ succC ⬝ 𝟘 - @[simp] abbrev mul : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) 𝟘 (add □ #1 $ #3 □ #0 □ #1)) - abbrev four'' : Γ ⊢ ℕt := mul □ 2 □ 2 + @[simp] abbrev mul : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) 𝟘 (add ⬝ #1 $ #3 ⬝ #0 ⬝ #1)) + abbrev four'' : Γ ⊢ ℕt := mul ⬝ 2 ⬝ 2 -- https://plfa.github.io/DeBruijn/#exercise-mul-recommended - @[simp] abbrev mulC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 □ (#2 □ #1) □ #0) + @[simp] abbrev mulC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 ⬝ (#2 ⬝ #1) ⬝ #0) -- https://plfa.github.io/More/#example example : ∅ ⊢ ℕp =⇒ ℕp := ƛ #0 ⋄ #0 ⋄ #0 @@ -223,7 +223,7 @@ namespace Subst intro ρ; intro | ‵ x => exact ‵ (ρ x) | ƛ n => exact ƛ (rename (ext ρ) n) - | l □ m => exact rename ρ l □ rename ρ m + | l ⬝ m => exact rename ρ l ⬝ rename ρ m | 𝟘 => exact 𝟘 | ι n => exact ι (rename ρ n) | 𝟘? l m n => exact 𝟘? (rename ρ l) (rename ρ m) (rename (ext ρ) n) @@ -271,7 +271,7 @@ namespace Subst intro σ; intro | ‵ i => exact σ i | ƛ n => exact ƛ (subst (exts σ) n) - | l □ m => exact subst σ l □ subst σ m + | l ⬝ m => exact subst σ l ⬝ subst σ m | 𝟘 => exact 𝟘 | ι n => exact ι (subst σ n) | 𝟘? l m n => exact 𝟘? (subst σ l) (subst σ m) (subst (exts σ) n) @@ -324,7 +324,7 @@ namespace Subst example : let m : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ι #0) let m' : ∅‚ ℕt =⇒ ℕt ⊢ ℕt =⇒ ℕt := ƛ (#1 $ #1 $ #0) - let n : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ƛ ι #0) □ ((ƛ ι #0) □ #0) + let n : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ƛ ι #0) ⬝ ((ƛ ι #0) ⬝ #0) m'⟦m⟧ = n := rfl @@ -364,9 +364,9 @@ end Value `Reduce t t'` says that `t` reduces to `t'` via a given step. -/ inductive Reduce : (Γ ⊢ a) → (Γ ⊢ a) → Prop where -| lamβ : Value v → Reduce ((ƛ n) □ v) (n⟦v⟧) -| apξ₁ : Reduce l l' → Reduce (l □ m) (l' □ m) -| apξ₂ : Value v → Reduce m m' → Reduce (v □ m) (v □ m') +| lamβ : Value v → Reduce ((ƛ n) ⬝ v) (n⟦v⟧) +| apξ₁ : Reduce l l' → Reduce (l ⬝ m) (l' ⬝ m) +| apξ₂ : Value v → Reduce m m' → Reduce (v ⬝ m) (v ⬝ m') | zeroβ : Reduce (𝟘? 𝟘 m n) m | succβ : Value v → Reduce (𝟘? (ι v) m n) (n⟦v⟧) | succξ : Reduce m m' → Reduce (ι m) (ι m') @@ -442,11 +442,11 @@ namespace Reduce -- https://plfa.github.io/DeBruijn/#examples open Term - example : twoC □ succC □ @zero ∅ —↠ 2 := calc - twoC □ succC □ 𝟘 - _ —→ (ƛ (succC $ succC $ #0)) □ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam + example : twoC ⬝ succC ⬝ @zero ∅ —↠ 2 := calc + twoC ⬝ succC ⬝ 𝟘 + _ —→ (ƛ (succC $ succC $ #0)) ⬝ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam _ —→ (succC $ succC $ 𝟘) := by apply lamβ; exact V𝟘 - _ —→ succC □ 1 := by + _ —→ succC ⬝ 1 := by apply apξ₂ · apply Value.lam · unfold succC; exact lamβ V𝟘 @@ -481,7 +481,7 @@ def Progress.progress : (m : ∅ ⊢ a) → Progress m := open Reduce in by intro | ‵ _ => contradiction | ƛ _ => exact .done .lam - | l □ m => match progress l with + | l ⬝ m => match progress l with | .step _ => apply step; apply apξ₁; trivial | .done l => match progress m with | .step _ => apply step; apply apξ₂ <;> trivial @@ -582,11 +582,11 @@ info: More.Result.dnf /-- info: More.Result.done (More.Value.succ (More.Value.succ (More.Value.succ (More.Value.zero)))) -/ -#guard_msgs in #eval evalRes <| add □ 2 □ 1 +#guard_msgs in #eval evalRes <| add ⬝ 2 ⬝ 1 /-- info: More.Result.done (More.Value.succ (More.Value.succ (More.Value.succ (More.Value.succ (More.Value.zero))))) -/ -#guard_msgs in #eval evalRes <| mul □ 2 □ 2 +#guard_msgs in #eval evalRes <| mul ⬝ 2 ⬝ 2 -- Prim /-- info: More.Result.done (More.Value.prim 6) diff --git a/Plfl/More/Bisimulation.lean b/Plfl/More/Bisimulation.lean index 73a2273..e6c690a 100644 --- a/Plfl/More/Bisimulation.lean +++ b/Plfl/More/Bisimulation.lean @@ -14,7 +14,7 @@ open Subst Notation inductive Sim : (Γ ⊢ a) → (Γ ⊢ a) → Prop where | var : Sim (‵ x) (‵ x) | lam : Sim n n' → Sim (ƛ n) (ƛ n') -| ap : Sim l l' → Sim m m' → Sim (l □ m) (l' □ m') +| ap : Sim l l' → Sim m m' → Sim (l ⬝ m) (l' ⬝ m') | let : Sim l l' → Sim m m' → Sim (.let l m) (.let l' m') namespace Sim diff --git a/Plfl/More/DoubleSubst.lean b/Plfl/More/DoubleSubst.lean index 798d67b..6e4e3b1 100644 --- a/Plfl/More/DoubleSubst.lean +++ b/Plfl/More/DoubleSubst.lean @@ -48,7 +48,7 @@ lemma subst_comp {ρ : ∀ {a}, Γ ∋ a → Δ ∋ a} {σ : ∀ {a}, Δ ∋ a | ƛ t => apply congr_arg lam; rw [subst_comp t] conv_lhs => arg 1; ext a t; simp only [Function.comp_apply, exts_comp t] - | l □ m => apply congr_arg₂ ap <;> apply subst_comp + | l ⬝ m => apply congr_arg₂ ap <;> apply subst_comp | 𝟘 => trivial | ι t => apply congr_arg succ; apply subst_comp | 𝟘? l m n => @@ -94,7 +94,7 @@ lemma subst_var (t : Γ ⊢ a) : subst var t = t := by apply congr_arg lam conv_lhs => arg 1; ext a i; rw [exts_var i] exact subst_var t - | l □ m => apply congr_arg₂ ap <;> apply subst_var + | l ⬝ m => apply congr_arg₂ ap <;> apply subst_var | 𝟘 => trivial | ι t => apply congr_arg succ; apply subst_var | 𝟘? l m n => @@ -189,7 +189,7 @@ lemma insert_twice {Γ Δ Φ : Context} {a b c : Ty} (t : Γ‚‚ Δ‚‚ Φ match t with | ‵ i => apply congr_arg var; exact insert_twice_idx i | ƛ t => apply congr_arg lam; rename_i a' b'; exact insert_twice (Φ := Φ‚ a') t - | l □ m => apply congr_arg₂ ap <;> apply insert_twice + | l ⬝ m => apply congr_arg₂ ap <;> apply insert_twice | 𝟘 => trivial | ι t => apply congr_arg succ; apply insert_twice | 𝟘? l m n => @@ -244,7 +244,7 @@ lemma insert_subst match t with | ‵ i => exact insert_subst_idx i | ƛ t => rename_i a b; apply congr_arg lam; exact insert_subst (Φ := Φ‚ a) t - | l □ m => apply congr_arg₂ ap <;> apply insert_subst + | l ⬝ m => apply congr_arg₂ ap <;> apply insert_subst | 𝟘 => trivial | ι t => apply congr_arg succ; apply insert_subst | 𝟘? l m n => @@ -303,7 +303,7 @@ theorem subst_subst_comp apply congr_arg lam rw [subst_subst_comp (σ := exts σ) (σ' := exts σ') t] congr; ext; apply exts_subst_comp - | l □ m => apply congr_arg₂ ap <;> apply subst_subst_comp + | l ⬝ m => apply congr_arg₂ ap <;> apply subst_subst_comp | 𝟘 => trivial | ι t => apply congr_arg succ; apply subst_subst_comp | 𝟘? l m n => diff --git a/Plfl/More/Inference.lean b/Plfl/More/Inference.lean index 96eb133..c9ae1e4 100644 --- a/Plfl/More/Inference.lean +++ b/Plfl/More/Inference.lean @@ -102,7 +102,7 @@ namespace Notation scoped infixr:min " $ " => ap -- scoped infix:60 " ↓ " => syn -- scoped postfix:60 "↑ " => inh - scoped infixl:70 " □ " => ap + scoped infixl:70 " ⬝ " => ap scoped prefix:80 "ι " => succ scoped prefix:90 "‵" => var scoped notation "𝟘" => zero @@ -121,18 +121,18 @@ abbrev add : TermS := (μ "+" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" - |succ "m" : ι (‵"+" □ ‵"m" □ ‵"n")] + |succ "m" : ι (‵"+" ⬝ ‵"m" ⬝ ‵"n")] ).the (ℕt =⇒ ℕt =⇒ ℕt) abbrev mul : TermS := (μ "*" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: 𝟘 - |succ "m": add □ ‵"n" $ ‵"*" □ ‵"m" □ ‵"n"] + |succ "m": add ⬝ ‵"n" $ ‵"*" ⬝ ‵"m" ⬝ ‵"n"] ).the (ℕt =⇒ ℕt =⇒ ℕt) -- Note that the typing is only required for `add` due to the rule for `ap`. -abbrev four : TermS := add □ two □ two +abbrev four : TermS := add ⬝ two ⬝ two /-- The Church numeral Ty. @@ -144,10 +144,10 @@ abbrev succC : TermI := ƛ "n" : ι ‵"n" abbrev oneC : TermI := ƛ "s" : ƛ "z" : ‵"s" $ ‵"z" abbrev twoC : TermI := ƛ "s" : ƛ "z" : ‵"s" $ ‵"s" $ ‵"z" abbrev addC : TermS := - (ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" □ ‵"s" $ ‵"n" □ ‵"s" □ ‵"z" + (ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" ⬝ ‵"s" $ ‵"n" ⬝ ‵"s" ⬝ ‵"z" ).the (Ch =⇒ Ch =⇒ Ch) -- Note that the typing is only required for `addC` due to the rule for `ap`. -abbrev four' : TermS := addC □ twoC □ twoC □ succC □ 𝟘 +abbrev four' : TermS := addC ⬝ twoC ⬝ twoC ⬝ succC ⬝ 𝟘 -- https://plfa.github.io/Inference/#bidirectional-type-checking /-- @@ -198,7 +198,7 @@ mutual -/ inductive TyS : Context → TermS → Ty → Type where | var : Γ ∋ x ⦂ a → TyS Γ (‵ x) a - | ap: TyS Γ l (a =⇒ b) → TyI Γ m a → TyS Γ (l □ m) b + | ap: TyS Γ l (a =⇒ b) → TyI Γ m a → TyS Γ (l ⬝ m) b | prod: TyS Γ m a → TyS Γ n b → TyS Γ (.prod m n) (a * b) | syn : TyI Γ m a → TyS Γ (m.the a) a deriving Repr @@ -326,7 +326,7 @@ def Lookup.lookup (Γ : Context) (x : Sym) : Decidable' (Σ a, Γ ∋ x ⦂ a) : lemma TyS.empty_arg : Γ ⊢ l ⇡ a =⇒ b → IsEmpty (Γ ⊢ m ⇣ a) -→ IsEmpty (Σ b', Γ ⊢ l □ m ⇡ b') +→ IsEmpty (Σ b', Γ ⊢ l ⬝ m ⇡ b') := by intro tl n; is_empty; intro ⟨b', .ap tl' tm'⟩ injection tl.unique tl'; rename_i h _; apply n.false; rwa [←h] at tm' @@ -340,7 +340,7 @@ mutual | ‵ x => match Lookup.lookup Γ x with | .inr ⟨a, i⟩ => right; exact ⟨a, .var i⟩ | .inl n => left; is_empty; intro ⟨a, .var i⟩; exact n.false ⟨a, i⟩ - | l □ m => match l.infer Γ with + | l ⬝ m => match l.infer Γ with | .inr ⟨a =⇒ b, tab⟩ => match m.infer Γ a with | .inr ta => right; exact ⟨b, .ap tab ta⟩ | .inl n => left; exact tab.empty_arg n @@ -434,7 +434,7 @@ abbrev four'Ty : Γ ⊢ four' ⇡ ℕt := open TyS TyI Lookup in by example : four'.infer ∅ = .inr ⟨ℕt, four'Ty⟩ := by rfl -abbrev four'': TermS := mul □ two □ two +abbrev four'': TermS := mul ⬝ two ⬝ two abbrev four''Ty : Γ ⊢ four'' ⇡ ℕt := open TyS TyI Lookup in by repeat apply_rules @@ -473,19 +473,19 @@ info: .inl _ /-- info: .inl _ -/ -#guard_msgs in #eval (add □ succC).infer ∅ +#guard_msgs in #eval (add ⬝ succC).infer ∅ -- Function in application is ill typed: /-- info: .inl _ -/ -#guard_msgs in #eval (add □ succC □ two).infer ∅ +#guard_msgs in #eval (add ⬝ succC ⬝ two).infer ∅ -- Function in application has type natural: /-- info: .inl _ -/ -#guard_msgs in #eval (two.the ℕt □ two).infer ∅ +#guard_msgs in #eval (two.the ℕt ⬝ two).infer ∅ -- Abstraction inherits type natural: /-- diff --git a/Plfl/Untyped.lean b/Plfl/Untyped.lean index 1d2fd34..42b98aa 100644 --- a/Plfl/Untyped.lean +++ b/Plfl/Untyped.lean @@ -106,7 +106,7 @@ namespace Notation scoped prefix:50 "ƛ " => lam scoped infixr:min " $ " => ap - scoped infixl:70 " □ " => ap + scoped infixl:70 " ⬝ " => ap scoped prefix:90 "‵" => var -- https://plfa.github.io/Untyped/#writing-variables-as-numerals @@ -117,14 +117,14 @@ namespace Term -- https://plfa.github.io/Untyped/#test-examples abbrev twoC : Γ ⊢ ✶ := ƛ ƛ (#1 $ #1 $ #0) abbrev fourC : Γ ⊢ ✶ := ƛ ƛ (#1 $ #1 $ #1 $ #1 $ #0) - abbrev addC : Γ ⊢ ✶ := ƛ ƛ ƛ ƛ (#3 □ #1 $ #2 □ #1 □ #0) - abbrev fourC' : Γ ⊢ ✶ := addC □ twoC □ twoC + abbrev addC : Γ ⊢ ✶ := ƛ ƛ ƛ ƛ (#3 ⬝ #1 $ #2 ⬝ #1 ⬝ #0) + abbrev fourC' : Γ ⊢ ✶ := addC ⬝ twoC ⬝ twoC def church (n : ℕ) : Γ ⊢ ✶ := ƛ ƛ applyN n where applyN | 0 => #0 - | n + 1 => #1 □ applyN n + | n + 1 => #1 ⬝ applyN n end Term namespace Subst @@ -145,7 +145,7 @@ namespace Subst intro ρ; intro | ‵ x => exact ‵ (ρ x) | ƛ n => exact ƛ (rename (ext ρ) n) - | l □ m => exact rename ρ l □ rename ρ m + | l ⬝ m => exact rename ρ l ⬝ rename ρ m abbrev shift : Γ ⊢ a → Γ‚ b ⊢ a := rename .s @@ -164,7 +164,7 @@ namespace Subst intro σ; intro | ‵ i => exact σ i | ƛ n => exact ƛ (subst (exts σ) n) - | l □ m => exact subst σ l □ subst σ m + | l ⬝ m => exact subst σ l ⬝ subst σ m -- https://plfa.github.io/Untyped/#single-substitution abbrev subst₁σ (v : Γ ⊢ b) : ∀ {a}, Γ‚ b ∋ a → Γ ⊢ a @@ -189,7 +189,7 @@ end Notation mutual inductive Neutral : Γ ⊢ a → Type | var : (x : Γ ∋ a) → Neutral (‵ x) - | ap : Neutral l → Normal m → Neutral (l □ m) + | ap : Neutral l → Normal m → Neutral (l ⬝ m) deriving Repr inductive Normal : Γ ⊢ a → Type @@ -208,11 +208,11 @@ namespace Notation scoped prefix:50 "ƛₙ " => lam scoped infixr:min " $ₙ " => ap - scoped infixl:70 " □ₙ " => ap + scoped infixl:70 " ⬝ₙ " => ap scoped prefix:90 "‵ₙ" => var end Notation -example : Normal (Term.twoC (Γ := ∅)) := ƛₙ ƛₙ (′#′1 □ₙ (′#′1 □ₙ (′#′0))) +example : Normal (Term.twoC (Γ := ∅)) := ƛₙ ƛₙ (′#′1 ⬝ₙ (′#′1 ⬝ₙ (′#′0))) -- https://plfa.github.io/Untyped/#reduction-step /-- @@ -222,26 +222,26 @@ _Note: This time there's no need to generate data out of `Reduce t t'`, so it can just be a `Prop`._ -/ inductive Reduce : (Γ ⊢ a) → (Γ ⊢ a) → Prop where -| lamβ : Reduce ((ƛ n) □ v) (n⟦v⟧) +| lamβ : Reduce ((ƛ n) ⬝ v) (n⟦v⟧) | lamζ : Reduce n n' → Reduce (ƛ n) (ƛ n') -| apξ₁ : Reduce l l' → Reduce (l □ m) (l' □ m) -| apξ₂ : Reduce m m' → Reduce (v □ m) (v □ m') +| apξ₁ : Reduce l l' → Reduce (l ⬝ m) (l' ⬝ m) +| apξ₂ : Reduce m m' → Reduce (v ⬝ m) (v ⬝ m') -- https://plfa.github.io/Untyped/#exercise-variant-1-practice inductive Reduce' : (Γ ⊢ a) → (Γ ⊢ a) → Type where -| lamβ : Normal (ƛ n) → Normal v → Reduce' ((ƛ n) □ v) (n⟦v⟧) +| lamβ : Normal (ƛ n) → Normal v → Reduce' ((ƛ n) ⬝ v) (n⟦v⟧) | lamζ : Reduce' n n' → Reduce' (ƛ n) (ƛ n') -| apξ₁ : Reduce' l l' → Reduce' (l □ m) (l' □ m) -| apξ₂ : Normal v → Reduce' m m' → Reduce' (v □ m) (v □ m') +| apξ₁ : Reduce' l l' → Reduce' (l ⬝ m) (l' ⬝ m) +| apξ₂ : Normal v → Reduce' m m' → Reduce' (v ⬝ m) (v ⬝ m') -- https://plfa.github.io/Untyped/#exercise-variant-2-practice inductive Reduce'' : (Γ ⊢ a) → (Γ ⊢ a) → Type where -| lamβ : Reduce'' ((ƛ n) □ (ƛ v)) (n⟦ƛ v⟧) -| apξ₁ : Reduce'' l l' → Reduce'' (l □ m) (l' □ m) -| apξ₂ : Reduce'' m m' → Reduce'' (v □ m) (v □ m') +| lamβ : Reduce'' ((ƛ n) ⬝ (ƛ v)) (n⟦ƛ v⟧) +| apξ₁ : Reduce'' l l' → Reduce'' (l ⬝ m) (l' ⬝ m) +| apξ₂ : Reduce'' m m' → Reduce'' (v ⬝ m) (v ⬝ m') /- Reduction of `four''C` under this variant might go as far as -`ƛ ƛ (twoC □ #1 $ (twoC □ #1 □ #0))` and get stuck, +`ƛ ƛ (twoC ⬝ #1 $ (twoC ⬝ #1 ⬝ #0))` and get stuck, since the next step uses `lamζ` which no longer exists. -/ @@ -282,14 +282,14 @@ namespace Reduce simp_all only [List.empty_eq] rfl - example : fourC' (Γ := ∅) —↠ fourC := calc addC □ twoC □ twoC - _ —→ (ƛ ƛ ƛ (twoC □ #1 $ (#2 □ #1 □ #0))) □ twoC := by + example : fourC' (Γ := ∅) —↠ fourC := calc addC ⬝ twoC ⬝ twoC + _ —→ (ƛ ƛ ƛ (twoC ⬝ #1 $ (#2 ⬝ #1 ⬝ #0))) ⬝ twoC := by apply apξ₁ exact lamβ - _ —→ ƛ ƛ (twoC □ #1 $ (twoC □ #1 □ #0)) := by exact lamβ - _ —→ ƛ ƛ ((ƛ (#2 $ #2 $ #0)) $ (twoC □ #1 □ #0)) := by apply_rules [lamζ, apξ₁, lamβ] - _ —→ ƛ ƛ (#1 $ #1 $ (twoC □ #1 □ #0)) := by apply_rules [lamζ, lamβ] - _ —→ ƛ ƛ (#1 $ #1 $ ((ƛ (#2 $ #2 $ #0)) □ #0)) := by apply_rules [lamζ, apξ₁, apξ₂, lamβ] + _ —→ ƛ ƛ (twoC ⬝ #1 $ (twoC ⬝ #1 ⬝ #0)) := by exact lamβ + _ —→ ƛ ƛ ((ƛ (#2 $ #2 $ #0)) $ (twoC ⬝ #1 ⬝ #0)) := by apply_rules [lamζ, apξ₁, lamβ] + _ —→ ƛ ƛ (#1 $ #1 $ (twoC ⬝ #1 ⬝ #0)) := by apply_rules [lamζ, lamβ] + _ —→ ƛ ƛ (#1 $ #1 $ ((ƛ (#2 $ #2 $ #0)) ⬝ #0)) := by apply_rules [lamζ, apξ₁, apξ₂, lamβ] _ —→ ƛ ƛ (#1 $ #1 $ #1 $ #1 $ #0) := by apply_rules [lamζ, apξ₁, apξ₂, lamβ] end Reduce @@ -313,20 +313,20 @@ def progress : (m : Γ ⊢ ✶) → Progress m match progress n with | .done n' => .done (ƛₙ n') | .step r => .step (Reduce.lamζ r) - | ‵ x □ m => - have : sizeOf m < sizeOf (‵ x □ m) := by simp only [Term.ap.sizeOf_spec]; omega + | ‵ x ⬝ m => + have : sizeOf m < sizeOf (‵ x ⬝ m) := by simp only [Term.ap.sizeOf_spec]; omega match progress m with - | .done m' => .done (′ ‵ₙ x □ₙ m') + | .done m' => .done (′ ‵ₙ x ⬝ₙ m') | .step r => .step (Reduce.apξ₂ r) - | (ƛ n) □ m => .step Reduce.lamβ - | (l' □ l'') □ m => - have : sizeOf (l' □ l'') < sizeOf ((l' □ l'') □ m) := by simp only [Term.ap.sizeOf_spec]; omega - match progress (l' □ l'') with + | (ƛ n) ⬝ m => .step Reduce.lamβ + | (l' ⬝ l'') ⬝ m => + have : sizeOf (l' ⬝ l'') < sizeOf ((l' ⬝ l'') ⬝ m) := by simp only [Term.ap.sizeOf_spec]; omega + match progress (l' ⬝ l'') with | .step r => .step (Reduce.apξ₁ r) | .done (′neutral_l) => - have : sizeOf m < sizeOf ((l' □ l'') □ m) := by simp only [Term.ap.sizeOf_spec]; omega + have : sizeOf m < sizeOf ((l' ⬝ l'') ⬝ m) := by simp only [Term.ap.sizeOf_spec]; omega match progress m with - | .done m' => .done (′neutral_l □ₙ m') + | .done m' => .done (′neutral_l ⬝ₙ m') | .step r => .step (Reduce.apξ₂ r) termination_by m => sizeOf m @@ -355,8 +355,8 @@ def eval (gas : ℕ) (l : ∅ ⊢ a) : Steps l := namespace Term abbrev id : Γ ⊢ ✶ := ƛ #0 - abbrev delta : Γ ⊢ ✶ := ƛ #0 □ #0 - abbrev omega : Γ ⊢ ✶ := delta □ delta + abbrev delta : Γ ⊢ ✶ := ƛ #0 ⬝ #0 + abbrev omega : Γ ⊢ ✶ := delta ⬝ delta -- https://plfa.github.io/Untyped/#naturals-and-fixpoint /- @@ -369,13 +369,13 @@ namespace Term = λ s _ => s (λ _ z => z) -/ abbrev zeroS : Γ ⊢ ✶ := ƛ ƛ #0 - abbrev succS (m : Γ ⊢ ✶) : Γ ⊢ ✶ := (ƛ ƛ ƛ (#1 □ #2)) □ m - abbrev caseS (l : Γ ⊢ ✶) (m : Γ ⊢ ✶) (n : Γ‚ ✶ ⊢ ✶) : Γ ⊢ ✶ := l □ (ƛ n) □ m + abbrev succS (m : Γ ⊢ ✶) : Γ ⊢ ✶ := (ƛ ƛ ƛ (#1 ⬝ #2)) ⬝ m + abbrev caseS (l : Γ ⊢ ✶) (m : Γ ⊢ ✶) (n : Γ‚ ✶ ⊢ ✶) : Γ ⊢ ✶ := l ⬝ (ƛ n) ⬝ m /-- The Y combinator: `Y f := (λ x => f (x x)) (λ x => f (x x))` -/ - abbrev mu (n : Γ‚ ✶ ⊢ ✶) : Γ ⊢ ✶ := (ƛ (ƛ (#1 $ #0 $ #0)) □ (ƛ (#1 $ #0 $ #0))) □ (ƛ n) + abbrev mu (n : Γ‚ ✶ ⊢ ✶) : Γ ⊢ ✶ := (ƛ (ƛ (#1 $ #0 $ #0)) ⬝ (ƛ (#1 $ #0 $ #0))) ⬝ (ƛ n) end Term namespace Notation @@ -391,19 +391,19 @@ end Notation section examples open Term - abbrev addS : Γ ⊢ ✶ := μ ƛ ƛ (𝟘? (#1) (#0) (ι (#3 □ #0 □ #1))) + abbrev addS : Γ ⊢ ✶ := μ ƛ ƛ (𝟘? (#1) (#0) (ι (#3 ⬝ #0 ⬝ #1))) -- https://plfa.github.io/Untyped/#exercise-multiplication-untyped-recommended - abbrev mulS : Γ ⊢ ✶ := μ ƛ ƛ (𝟘? (#1) 𝟘 (addS □ #1 $ #3 □ #0 □ #1)) + abbrev mulS : Γ ⊢ ✶ := μ ƛ ƛ (𝟘? (#1) 𝟘 (addS ⬝ #1 $ #3 ⬝ #0 ⬝ #1)) abbrev oneS : Γ ⊢ ✶ := ι 𝟘 abbrev twoS : Γ ⊢ ✶ := ι ι 𝟘 - abbrev twoS'' : Γ ⊢ ✶ := mulS □ twoS □ oneS + abbrev twoS'' : Γ ⊢ ✶ := mulS ⬝ twoS ⬝ oneS abbrev fourS : Γ ⊢ ✶ := ι ι twoS - abbrev fourS' : Γ ⊢ ✶ := addS □ twoS □ twoS - abbrev fourS'' : Γ ⊢ ✶ := mulS □ twoS □ twoS + abbrev fourS' : Γ ⊢ ✶ := addS ⬝ twoS ⬝ twoS + abbrev fourS'' : Γ ⊢ ✶ := mulS ⬝ twoS ⬝ twoS abbrev evalRes (l : ∅ ⊢ a) (gas := 100) := (eval gas l).3 -- abbrev evalResStar (l : ∅ ⊢ ✶) (gas := 100) := (eval gas l).3 @@ -568,11 +568,11 @@ Default structural recursion cannot be used since it depends on sizeOf, however this won't work for `Prop`. We have to find another way. -/ -theorem Reduce.ap_congr₁ (rs : l —↠ l') : (l □ m) —↠ (l' □ m) := by +theorem Reduce.ap_congr₁ (rs : l —↠ l') : (l ⬝ m) —↠ (l' ⬝ m) := by refine rs.head_induction_on .refl ?_ · introv; intro r _ rs; refine .head ?_ rs; exact apξ₁ r -theorem Reduce.ap_congr₂ (rs : m —↠ m') : (l □ m) —↠ (l □ m') := by +theorem Reduce.ap_congr₂ (rs : m —↠ m') : (l ⬝ m) —↠ (l ⬝ m') := by refine rs.head_induction_on .refl ?_ · introv; intro r _ rs; refine .head ?_ rs; exact apξ₂ r diff --git a/Plfl/Untyped/BigStep.lean b/Plfl/Untyped/BigStep.lean index 8110a4f..da1ae20 100644 --- a/Plfl/Untyped/BigStep.lean +++ b/Plfl/Untyped/BigStep.lean @@ -45,7 +45,7 @@ open Notation inductive Eval : ClosEnv Γ → (Γ ⊢ ✶) → Clos → Prop where | var : γ i = .clos m δ → Eval δ m v → Eval γ (‵ i) v | lam : Eval γ (ƛ m) (.clos (ƛ m) γ) -| ap : Eval γ l (.clos (ƛ n) δ) → Eval (δ‚' .clos m γ) n v → Eval γ (l □ m) v +| ap : Eval γ l (.clos (ƛ n) δ) → Eval (δ‚' .clos m γ) n v → Eval γ (l ⬝ m) v namespace Notation scoped notation:40 γ " ⊢ " m " ⇓ " c:51 => Eval γ m c @@ -53,9 +53,9 @@ end Notation -- https://plfa.github.io/BigStep/#exercise-big-step-eg-practice example -: γ ⊢ (ƛ ƛ #1) $ (ƛ #0 □ #0) $ (ƛ #0 □ #0) +: γ ⊢ (ƛ ƛ #1) $ (ƛ #0 ⬝ #0) $ (ƛ #0 ⬝ #0) -- (λ x y => x) ((λ f => f f) (λ f => f f)) ⇓ (λ y => ((λ f => f f) (λ f => f f))) -⇓ .clos (ƛ #1) (γ‚' .clos ((ƛ #0 □ #0) $ (ƛ #0 □ #0)) γ) +⇓ .clos (ƛ #1) (γ‚' .clos ((ƛ #0 ⬝ #0) $ (ƛ #0 ⬝ #0)) γ) := .ap .lam .lam -- https://plfa.github.io/BigStep/#the-big-step-semantics-is-deterministic @@ -115,8 +115,8 @@ section have ⟨n', rn', en'⟩ := ih' <| ClosEnv.ext eeτ ⟨σ, ee, rfl⟩ refine ⟨n', ?_, en'⟩; simp only [sub_ap]; rename_i n _ m _ apply (ap_congr₁ rn).trans; unfold ext_subst at rn' - calc ⟪τ⟫ (ƛ n) □ ⟪σ⟫ m - _ = (ƛ (⟪exts τ⟫ n)) □ ⟪σ⟫ m := rfl + calc ⟪τ⟫ (ƛ n) ⬝ ⟪σ⟫ m + _ = (ƛ (⟪exts τ⟫ n)) ⬝ ⟪σ⟫ m := rfl _ —→ ⟪subst₁σ (⟪σ⟫ m)⟫ (⟪exts τ⟫ n) := lamβ _ = ⟪⟪subst₁σ (⟪σ⟫ m)⟫ ∘ exts τ⟫ n := Substitution.sub_sub _ —↠ n' := rn' @@ -141,7 +141,7 @@ namespace BySubst inductive Eval : (Γ ⊢ ✶) → (Γ ⊢ ✶) → Prop where -- Hmmm, it's all ƛ's after all? | lam : ∀ {n : ∅‚ ✶ ⊢ ✶}, Eval (ƛ n) (ƛ n) -| ap : Eval l (ƛ m) → Eval (m⟦n⟧) v → Eval (l □ n) v +| ap : Eval l (ƛ m) → Eval (m⟦n⟧) v → Eval (l ⬝ n) v namespace Notation scoped infix:50 " ⇓' "=> Eval @@ -165,7 +165,7 @@ theorem Eval.reduce_of_cbn {n : Γ‚ ✶ ⊢ ✶} (ev : m ⇓' (ƛ n)) : m — generalize hx : (ƛ n) = x, hx' : m = x' at * induction ev with | lam => rfl - | ap _evl evmn' ih ih' => subst_vars; rename_i l m n'; calc l □ n' - _ —↠ (ƛ m) □ n' := ap_congr₁ <| ih rfl rfl + | ap _evl evmn' ih ih' => subst_vars; rename_i l m n'; calc l ⬝ n' + _ —↠ (ƛ m) ⬝ n' := ap_congr₁ <| ih rfl rfl _ —→ m⟦n'⟧ := lamβ _ —↠ (ƛ n) := ih' rfl rfl diff --git a/Plfl/Untyped/Confluence.lean b/Plfl/Untyped/Confluence.lean index 29ee8b5..85f25ca 100644 --- a/Plfl/Untyped/Confluence.lean +++ b/Plfl/Untyped/Confluence.lean @@ -17,9 +17,9 @@ Parallel reduction. -/ inductive PReduce : (Γ ⊢ a) → (Γ ⊢ a) → Prop where | var : PReduce (‵ x) (‵ x) -| lamβ : PReduce n n' → PReduce v v' → PReduce ((ƛ n) □ v) (n'⟦v'⟧) +| lamβ : PReduce n n' → PReduce v v' → PReduce ((ƛ n) ⬝ v) (n'⟦v'⟧) | lamζ : PReduce n n' → PReduce (ƛ n) (ƛ n') -| apξ : PReduce l l' → PReduce m m' → PReduce (l □ m) (l' □ m') +| apξ : PReduce l l' → PReduce m m' → PReduce (l ⬝ m) (l' ⬝ m') namespace PReduce @[refl] @@ -27,7 +27,7 @@ namespace PReduce match m with | ‵ i => exact .var | ƛ n => apply lamζ; apply refl - | l □ m => apply apξ <;> apply refl + | l ⬝ m => apply apξ <;> apply refl abbrev Clos {Γ a} := Relation.ReflTransGen (α := Γ ⊢ a) PReduce end PReduce @@ -67,15 +67,15 @@ namespace PReduce theorem toReduceClos : (m ⇛ n) → (m —↠ n) | .var => Untyped.Reduce.Clos.refl | .lamβ (n:=n) (n':=n') (v:=v) (v':=v') rn rv => - calc (ƛ n) □ v - _ —↠ (ƛ n') □ v := Untyped.Reduce.ap_congr₁ (toReduceClos (.lamζ rn)) - _ —↠ (ƛ n') □ v' := Untyped.Reduce.ap_congr₂ (toReduceClos rv) + calc (ƛ n) ⬝ v + _ —↠ (ƛ n') ⬝ v := Untyped.Reduce.ap_congr₁ (toReduceClos (.lamζ rn)) + _ —↠ (ƛ n') ⬝ v' := Untyped.Reduce.ap_congr₂ (toReduceClos rv) _ —→ n'⟦v'⟧ := Untyped.Reduce.lamβ | .lamζ rn => Untyped.Reduce.lam_congr (toReduceClos rn) | .apξ (l:=l) (l':=l') (m:=m) (m':=m') rl rm => - calc l □ m - _ —↠ l' □ m := Untyped.Reduce.ap_congr₁ (toReduceClos rl) - _ —↠ l' □ m' := Untyped.Reduce.ap_congr₂ (toReduceClos rm) + calc l ⬝ m + _ —↠ l' ⬝ m := Untyped.Reduce.ap_congr₁ (toReduceClos rl) + _ —↠ l' ⬝ m' := Untyped.Reduce.ap_congr₂ (toReduceClos rm) end PReduce def equivPReduceClosReduceClos : (m ⇛* n) ≃ (m —↠ n) where @@ -144,8 +144,8 @@ Many parallel reductions at once. abbrev PReduce.plus : (Γ ⊢ a) → (Γ ⊢ a) | ‵ i => ‵ i | ƛ n => ƛ (plus n) -| (ƛ n) □ m => plus n⟦plus m⟧ -| l □ m => plus l □ plus m +| (ƛ n) ⬝ m => plus n⟦plus m⟧ +| l ⬝ m => plus l ⬝ plus m namespace Notation postfix:max "⁺" => PReduce.plus @@ -158,7 +158,7 @@ theorem par_triangle {m n : Γ ⊢ a} : (m ⇛ n) → (n ⇛ m⁺) := open PRedu | .lamζ pn => exact lamζ (par_triangle pn) | .apξ pl pm => rename_i l l' m m'; match l with | ‵ _ => exact apξ (par_triangle pl) (par_triangle pm) - | _ □ _ => exact apξ (par_triangle pl) (par_triangle pm) + | _ ⬝ _ => exact apξ (par_triangle pl) (par_triangle pm) | ƛ _ => match pl with | .lamζ pl => exact lamβ (par_triangle pl) (par_triangle pm) theorem par_diamond {m n n' : Γ ⊢ a} (p : m ⇛ n) (p' : m ⇛ n') diff --git a/Plfl/Untyped/Denotational.lean b/Plfl/Untyped/Denotational.lean index 9c3e083..e372faf 100644 --- a/Plfl/Untyped/Denotational.lean +++ b/Plfl/Untyped/Denotational.lean @@ -151,7 +151,7 @@ end Env.Sub -/ inductive Eval : Env Γ → (Γ ⊢ ✶) → Value → Prop where | var : Eval γ (‵ i) (γ i) -| ap : Eval γ l (v ⇾ w) → Eval γ m v → Eval γ (l □ m) w +| ap : Eval γ l (v ⇾ w) → Eval γ m v → Eval γ (l ⬝ m) w | fn {v w} : Eval (γ`‚ v) n w → Eval γ (ƛ n) (v ⇾ w) | bot : Eval γ m ⊥ | conj : Eval γ m v → Eval γ m w → Eval γ m (v ⊔ w) @@ -165,7 +165,7 @@ end Notation Relaxation of table lookup in application, allowing an argument to match an input entry if the latter is less than the former. -/ -theorem Eval.ap_sub (d : γ ⊢ l ￬ v ⇾ w) (d' : γ ⊢ m ￬ v') (lt : v ⊑ v') : γ ⊢ l □ m ￬ w +theorem Eval.ap_sub (d : γ ⊢ l ￬ v ⇾ w) (d' : γ ⊢ m ￬ v') (lt : v ⊑ v') : γ ⊢ l ⬝ m ￬ w := d.ap <| d'.sub lt namespace Example @@ -180,7 +180,7 @@ namespace Example theorem denot_id₃ : γ ⊢ id ￬ (⊥ ⇾ ⊥) ⊔ ((⊥ ⇾ ⊥) ⇾ (⊥ ⇾ ⊥)) := denot_id₁.conj denot_id₂ -- Oops, self application! - theorem denot_id_ap_id : `∅ ⊢ id □ id ￬ v ⇾ v := .ap (.fn .var) (.fn .var) + theorem denot_id_ap_id : `∅ ⊢ id ⬝ id ￬ v ⇾ v := .ap (.fn .var) (.fn .var) -- In `def twoC f u := f (f u)`, -- `f`'s table must include two entries, both `u ⇾ v` and `v ⇾ w`. diff --git a/Plfl/Untyped/Denotational/Adequacy.lean b/Plfl/Untyped/Denotational/Adequacy.lean index 2b732d8..6050a8c 100644 --- a/Plfl/Untyped/Denotational/Adequacy.lean +++ b/Plfl/Untyped/Denotational/Adequacy.lean @@ -74,7 +74,7 @@ mutual -/ def 𝕍 : Value → Clos → Prop | _, .clos (‵ _) _ => ⊥ - | _, .clos (_ □ _) _ => ⊥ + | _, .clos (_ ⬝ _) _ => ⊥ | ⊥, .clos (ƛ _) _ => ⊤ | vw@(v ⇾ w), .clos (ƛ n) γ => have : sizeOf w < sizeOf vw := by subst_vars; simp only [Value.fn.sizeOf_spec, diff --git a/Plfl/Untyped/Denotational/Compositional.lean b/Plfl/Untyped/Denotational/Compositional.lean index 0b483f6..50f902c 100644 --- a/Plfl/Untyped/Denotational/Compositional.lean +++ b/Plfl/Untyped/Denotational/Compositional.lean @@ -53,8 +53,8 @@ end Notation open Notation -lemma 𝒜_ℰ (d : ℰ (l □ m) γ v) : (ℰ l ● ℰ m) γ v := by - generalize hx : l □ m = x at * +lemma 𝒜_ℰ (d : ℰ (l ⬝ m) γ v) : (ℰ l ● ℰ m) γ v := by + generalize hx : l ⬝ m = x at * induction d with try injection hx | bot => left; rfl | ap d d' => subst_vars; right; rename_i v' _ _ _ _; exists v' @@ -73,11 +73,11 @@ lemma 𝒜_ℰ (d : ℰ (l □ m) γ v) : (ℰ l ● ℰ m) γ v := by right; refine ⟨v' ⊔ v'', ?_, ev'.conj ev''⟩ exact (efv'.conj efv'').sub fn_conj_sub_conj_fn -lemma ℰ_ap : (ℰ l ● ℰ m) γ v → ℰ (l □ m) γ v +lemma ℰ_ap : (ℰ l ● ℰ m) γ v → ℰ (l ⬝ m) γ v | .inl lt => .sub .bot lt | .inr ⟨_, efv, ev⟩ => efv.ap ev -theorem ap_equiv : ℰ (l □ m) = (ℰ l ● ℰ m) := by ext; exact ⟨𝒜_ℰ, ℰ_ap⟩ +theorem ap_equiv : ℰ (l ⬝ m) = (ℰ l ● ℰ m) := by ext; exact ⟨𝒜_ℰ, ℰ_ap⟩ abbrev 𝒱 (i : Γ ∋ ✶) (γ : Env Γ) (v : Value) : Prop := v ⊑ γ i @@ -97,10 +97,10 @@ lemma lam_congr (h : ℰ n = ℰ n') : ℰ (ƛ n) = ℰ (ƛ n') := calc _ _ = ℱ (ℰ n') := by rw [h] _ = ℰ (ƛ n') := lam_equiv.symm -lemma ap_congr (hl : ℰ l = ℰ l') (hm : ℰ m = ℰ m') : ℰ (l □ m) = ℰ (l' □ m') := calc _ +lemma ap_congr (hl : ℰ l = ℰ l') (hm : ℰ m = ℰ m') : ℰ (l ⬝ m) = ℰ (l' ⬝ m') := calc _ _ = ℰ l ● ℰ m := ap_equiv _ = ℰ l' ● ℰ m' := by rw [hl, hm] - _ = ℰ (l' □ m') := ap_equiv.symm + _ = ℰ (l' ⬝ m') := ap_equiv.symm -- https://plfa.github.io/Compositional/#compositionality open Untyped (Context) @@ -124,8 +124,8 @@ inductive Holed : Context → Context → Type where def Holed.plug : Holed Γ Δ → (Γ ⊢ ✶) → (Δ ⊢ ✶) | .hole, m => m | .lam c, n => ƛ c.plug n -| .apL c n, l => c.plug l □ n -| .apR l c, m => l □ c.plug m +| .apL c n, l => c.plug l ⬝ n +| .apR l c, m => l ⬝ c.plug m /-- Given two terms that are denotationally equal, @@ -147,7 +147,7 @@ It is like `ℰ m`, but defined computationally. def ℰ₀ : (Γ ⊢ ✶) → Denot Γ | ‵ i => 𝒱 i | ƛ n => ℱ (ℰ₀ n) -| l □ m => ℰ₀ l ● ℰ₀ m +| l ⬝ m => ℰ₀ l ● ℰ₀ m /-- The two definitions of `ℰ` are equivalent. -/ theorem ℰ_eq_ℰ₀ : ℰ (Γ := Γ) = ℰ₀ := by ext; rw [impl] diff --git a/Plfl/Untyped/Denotational/Soundness.lean b/Plfl/Untyped/Denotational/Soundness.lean index dc6b059..21d7f0f 100644 --- a/Plfl/Untyped/Denotational/Soundness.lean +++ b/Plfl/Untyped/Denotational/Soundness.lean @@ -173,21 +173,21 @@ theorem reduce_reflect {γ : Env Γ} {m n : Γ ⊢ a} (d : γ ⊢ n ￬ v) (r : | conj _ _ ih ih' => exact (ih r ihᵣ hx).conj (ih' r ihᵣ hx) | sub _ lt ih => exact (ih r ihᵣ hx).sub lt | apξ₁ r ihᵣ => - rename_i l m; generalize hx : l □ m = x at * + rename_i l m; generalize hx : l ⬝ m = x at * induction d with try contradiction | ap d d' _ _ => injection hx; subst_vars; exact (ihᵣ d).ap d' | bot => exact .bot | conj _ _ ih ih' => exact (ih r ihᵣ hx).conj (ih' r ihᵣ hx) | sub _ lt ih => exact (ih r ihᵣ hx).sub lt | apξ₂ r ihᵣ => - rename_i m l; generalize hx : l □ m = x at * + rename_i m l; generalize hx : l ⬝ m = x at * induction d with try contradiction | ap d d' _ _ => injection hx; subst_vars; exact d.ap <| ihᵣ d' | bot => exact .bot | conj _ _ ih ih' => exact (ih r ihᵣ hx).conj (ih' r ihᵣ hx) | sub _ lt ih => exact (ih r ihᵣ hx).sub lt where - beta {Γ m n v} {γ : Env Γ} (d : γ ⊢ n⟦m⟧ ￬ v) : γ ⊢ (ƛ n) □ m ￬ v := by + beta {Γ m n v} {γ : Env Γ} (d : γ ⊢ n⟦m⟧ ￬ v) : γ ⊢ (ƛ n) ⬝ m ￬ v := by let ⟨v, dm, dn⟩ := subst₁_reflect d; exact dn.fn.ap dm -- https://plfa.github.io/Soundness/#reduction-implies-denotational-equality diff --git a/Plfl/Untyped/Substitution.lean b/Plfl/Untyped/Substitution.lean index c047b44..c296efa 100644 --- a/Plfl/Untyped/Substitution.lean +++ b/Plfl/Untyped/Substitution.lean @@ -45,7 +45,7 @@ section @[simp] theorem sub_η {σ : Subst (Γ‚ a) Δ} : (⟪σ⟫ (‵ .z) ⦂⦂ (shift ⨟ σ)) = σ (a := b) := by funext i; cases i <;> rfl @[simp] theorem z_shift : ((‵ .z) ⦂⦂ shift) = @ids (Γ‚ a) b := by funext i; cases i <;> rfl @[simp] theorem ids_seq : (ids ⨟ σ) = σ (a := a) := rfl - @[simp] theorem sub_ap {l m : Γ ⊢ ✶} : ⟪σ⟫ (l □ m) = (⟪σ⟫ l) □ (⟪σ⟫ m) := rfl + @[simp] theorem sub_ap {l m : Γ ⊢ ✶} : ⟪σ⟫ (l ⬝ m) = (⟪σ⟫ l) ⬝ (⟪σ⟫ m) := rfl @[simp] theorem sub_dist : @Eq (Γ‚ a ∋ b → Φ ⊢ b) ((m ⦂⦂ σ) ⨟ τ) ((⟪τ⟫ m) ⦂⦂ (σ ⨟ τ)) := by funext i; cases i <;> rfl end @@ -65,7 +65,7 @@ section match m with | ‵ _ => rfl | ƛ n => apply congr_arg Term.lam; rw [rename_subst_ren]; congr; funext _; exact ren_ext - | l □ m => simp only [sub_ap]; apply congr_arg₂ Term.ap <;> exact rename_subst_ren + | l ⬝ m => simp only [sub_ap]; apply congr_arg₂ Term.ap <;> exact rename_subst_ren theorem rename_shift : @Eq (Γ‚ ✶ ⊢ a) (rename .s m) (⟪shift⟫ m) := by simp only [rename_subst_ren]; congr @@ -93,7 +93,7 @@ section apply congr_arg Term.lam convert sub_ids simp_all only [exts_ids] - | l □ m => simp only [sub_ap]; apply congr_arg₂ Term.ap <;> exact sub_ids + | l ⬝ m => simp only [sub_ap]; apply congr_arg₂ Term.ap <;> exact sub_ids theorem rename_id : rename (λ {_} x => x) m = m := by rw [rename_subst_ren]; exact sub_ids @@ -115,7 +115,7 @@ section match m with | ‵ _ => rfl | ƛ n => apply congr_arg Term.lam; convert comp_rename; exact comp_ext.symm - | l □ m => apply congr_arg₂ Term.ap <;> exact comp_rename + | l ⬝ m => apply congr_arg₂ Term.ap <;> exact comp_rename theorem comm_subst_rename {Γ Δ} {σ : Subst Γ Δ} {ρ : ∀ {Γ}, Rename Γ (Γ‚ ✶)} (r : ∀ {x : Γ ∋ ✶}, exts σ (ρ x) = rename ρ (σ x)) {m : Γ ⊢ ✶} @@ -123,7 +123,7 @@ section := by match m with | ‵ _ => exact r - | l □ m => apply congr_arg₂ Term.ap <;> exact comm_subst_rename r + | l ⬝ m => apply congr_arg₂ Term.ap <;> exact comm_subst_rename r | ƛ n => apply congr_arg Term.lam @@ -156,7 +156,7 @@ section : ⟪τ⟫ (⟪σ⟫ m) = ⟪σ ⨟ τ⟫ m := by match m with | ‵ _ => rfl - | l □ m => apply congr_arg₂ Term.ap <;> exact sub_sub + | l ⬝ m => apply congr_arg₂ Term.ap <;> exact sub_sub | ƛ n => calc ⟪τ⟫ (⟪σ⟫ (ƛ n)) _ = (ƛ ⟪exts τ⟫ (⟪exts σ⟫ n)) := rfl _ = (ƛ (⟪exts σ ⨟ exts τ⟫ n)) := by apply congr_arg Term.lam; exact sub_sub