From c97f067a19d342598215ad7acc4793723481073a Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Sat, 23 May 2026 02:07:33 +0700 Subject: [PATCH 1/8] feat: update to latest lean --- Plfl.lean | 6 +- Plfl/DeBruijn.lean | 25 +-- Plfl/Init.lean | 19 +-- Plfl/Lambda.lean | 153 +++++++++++-------- Plfl/Lambda/Properties.lean | 110 +++++++------ Plfl/More.lean | 60 ++++++-- Plfl/More/Bisimulation.lean | 4 +- Plfl/More/DoubleSubst.lean | 22 +-- Plfl/More/Inference.lean | 80 +++++----- Plfl/Untyped.lean | 139 +++++++++-------- Plfl/Untyped/BigStep.lean | 10 +- Plfl/Untyped/Confluence.lean | 14 +- Plfl/Untyped/Denotational.lean | 125 +++++++++------ Plfl/Untyped/Denotational/Adequacy.lean | 11 +- Plfl/Untyped/Denotational/Compositional.lean | 8 +- Plfl/Untyped/Denotational/Soundness.lean | 6 +- Plfl/Untyped/Substitution.lean | 72 +++++---- lake-manifest.json | 94 ++++++++---- lakefile.lean | 19 --- lakefile.toml | 31 ++++ lean-toolchain | 2 +- 21 files changed, 589 insertions(+), 421 deletions(-) delete mode 100644 lakefile.lean create mode 100644 lakefile.toml diff --git a/Plfl.lean b/Plfl.lean index 657eeef..d18fae5 100644 --- a/Plfl.lean +++ b/Plfl.lean @@ -1,3 +1,7 @@ +-- module +-- prelude + +import Plfl.Init import Plfl.Lambda import Plfl.Lambda.Properties import Plfl.DeBruijn @@ -6,8 +10,8 @@ import Plfl.More.DoubleSubst import Plfl.More.Bisimulation import Plfl.More.Inference import Plfl.Untyped -import Plfl.Untyped.Confluence import Plfl.Untyped.Substitution +import Plfl.Untyped.Confluence import Plfl.Untyped.BigStep import Plfl.Untyped.Denotational import Plfl.Untyped.Denotational.Compositional diff --git a/Plfl/DeBruijn.lean b/Plfl/DeBruijn.lean index 3efad76..1ac5c5e 100644 --- a/Plfl/DeBruijn.lean +++ b/Plfl/DeBruijn.lean @@ -78,11 +78,11 @@ namespace Term infixr:min " $ " => ap infixl:70 " □ " => ap prefix:80 "ι " => succ - prefix:90 "` " => var + prefix:90 "‵" => var notation "𝟘" => zero -- https://plfa.github.io/DeBruijn/#abbreviating-de-bruijn-indices - macro "# " n:term:90 : term => `(`♯$n) + macro "# " n:term:90 : term => `(‵ ♯$n) example : ∅‚ ℕt =⇒ ℕt‚ ℕt ⊢ ℕt := #0 example : ∅‚ ℕt =⇒ ℕt‚ ℕt ⊢ ℕt =⇒ ℕt := #1 @@ -137,7 +137,7 @@ then the type judgements are the same in both contexts. -/ def rename : (∀ {a}, Γ ∋ a → Δ ∋ a) → Γ ⊢ a → Δ ⊢ a := by intro ρ; intro - | ` x => exact ` (ρ x) + | ‵ x => exact ‵ (ρ x) | ƛ n => refine .lam ?_; refine rename ?_ n; exact ext ρ | l □ m => apply Term.ap @@ -165,7 +165,7 @@ the mapping holds after adding the same variable to both contexts. -/ def exts : (∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ‚ b ∋ a → Δ‚ b ⊢ a := by intro σ; intro - | .z => exact `.z + | .z => exact ‵.z | .s x => apply rename .s; exact σ x /-- @@ -176,7 +176,7 @@ i.e. after replacing the free variables in the former with (expanded) terms. -/ def subst : (∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ ⊢ a → Δ ⊢ a := by intro σ; intro - | ` x => exact σ x + | ‵ x => exact σ x | ƛ n => refine .lam ?_; refine subst ?_ n; exact exts σ | l □ m => apply Term.ap @@ -197,7 +197,7 @@ Substitution for one free variable `m` in the term `n`. abbrev subst₁ (m : Γ ⊢ b) (n : Γ‚ b ⊢ a) : Γ ⊢ a := by refine subst ?_ n; introv; intro | .z => exact m - | .s x => exact ` x + | .s x => exact ‵ x notation:90 n "⟦" m "⟧" => subst₁ m n @@ -295,17 +295,20 @@ namespace Reduce twoC □ succC □ 𝟘 _ —→ (ƛ (succC $ succC $ #0)) □ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam _ —→ (succC $ succC $ 𝟘) := by apply lamβ; exact V𝟘 - _ —→ succC □ 1 := by apply apξ₂; apply Value.lam; exact lamβ V𝟘 - _ —→ 2 := by apply lamβ; exact Value.ofNat 1 + _ —→ succC □ 1 := by + apply apξ₂ + · apply Value.lam + · unfold succC; exact lamβ V𝟘 + _ —→ 2 := by unfold succC; apply lamβ; exact Value.ofNat 1 end Reduce -- https://plfa.github.io/DeBruijn/#values-do-not-reduce -def Value.empty_reduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by +theorem Value.empty_reduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by introv v; is_empty; intro r cases v <;> try contradiction · case succ v => cases r; · case succξ => apply (empty_reduce v).false; trivial -def Reduce.empty_value : m —→ n → IsEmpty (Value m) := by +theorem Reduce.empty_value : m —→ n → IsEmpty (Value m) := by intro r; is_empty; intro v have : ∀ {n}, IsEmpty (m —→ n) := Value.empty_reduce v exact this.false r @@ -319,7 +322,7 @@ inductive Progress (m : ∅ ⊢ a) where def progress : (m : ∅ ⊢ a) → Progress m := open Progress Reduce in by intro - | ` _ => contradiction + | ‵ _ => contradiction | ƛ _ => exact .done Value.lam | jl □ jm => cases progress jl with | step => apply step; · apply apξ₁; trivial diff --git a/Plfl/Init.lean b/Plfl/Init.lean index 13989b8..8a92b4a 100644 --- a/Plfl/Init.lean +++ b/Plfl/Init.lean @@ -1,7 +1,7 @@ -import Std.Data.List.Lemmas +-- module -import Mathlib.Data.Vector -import Mathlib.Logic.IsEmpty +import Mathlib.Logic.Function.Basic +import Mathlib.Logic.Relator import Mathlib.Tactic /-- @@ -33,15 +33,10 @@ theorem congr_arg₃ := by subst hx hy hz; rfl namespace Vector - def dropLast (v : Vector α n) : Vector α (n - 1) := by - exists v.1.dropLast; simp only [List.length_dropLast, Vector.length_val] + def dropLast (v : Vector α n) : Vector α (n - 1) := v.pop theorem get_dropLast (v : Vector α (n + 1)) (i : Fin n) - : v.dropLast.get i = v.get i.1 - := by - simp only [ - Vector.get, dropLast, v.1.dropLast_eq_take, - Vector.length_val, Nat.pred_succ, Fin.coe_eq_castSucc - ] - change List.get _ _ = List.get _ _; rw [List.get_dropLast]; rfl + -- : v.dropLast[i] = v[i.val]'(by omega) + : v.dropLast.get i = v.get ⟨i.val, by omega⟩ + := by simp [dropLast, Vector.get, Vector.pop] end Vector diff --git a/Plfl/Lambda.lean b/Plfl/Lambda.lean index f6e2124..8844391 100644 --- a/Plfl/Lambda.lean +++ b/Plfl/Lambda.lean @@ -1,3 +1,4 @@ +-- module -- https://plfa.github.io/Lambda/ import Plfl.Init @@ -26,11 +27,11 @@ namespace Term infixr:min " $ " => ap infixl:70 " □ " => ap prefix:80 "ι " => succ - prefix:90 "` " => var + prefix:90 "‵" => var notation "𝟘" => zero - example : Term := `"foo" - example : Term := 𝟘? `"bar" [zero: 𝟘 |succ "n" : ι 𝟘] + example : Term := ‵"foo" + example : Term := 𝟘? ‵"bar" [zero: 𝟘 |succ "n" : ι 𝟘] @[simp] def ofNat | 0 => zero | n + 1 => succ <| ofNat n instance : Coe ℕ Term where coe := ofNat @@ -39,17 +40,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 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" -- 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 @@ -76,7 +77,7 @@ namespace Term `x.subst y v` substitutes term `v` for all free occurrences of variable `y` in term `x`. -/ def subst : Term → Sym → Term → Term - | ` x, y, v => if x = y then v else ` x + | ‵x, y, v => if x = y then v else ‵x | ƛ x : n, y, v => if x = y then ƛ x : n else ƛ x : n.subst y v | ap l m, y, v => l.subst y v $ m.subst y v | 𝟘, _, _ => 𝟘 @@ -90,18 +91,18 @@ 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 : (ƛ "x" : `"y")["y" := 𝟘] = (ƛ "x" : 𝟘) := rfl - example : (ƛ "x" : `"x")["x" := 𝟘] = (ƛ "x" : `"x") := rfl - example : (ƛ "y" : `"y")["x" := 𝟘] = (ƛ "y" : `"y") := 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 -- https://plfa.github.io/Lambda/#quiz example - : (ƛ "y" : `"x" $ ƛ "x" : `"x")["x" := 𝟘] - = (ƛ "y" : 𝟘 $ ƛ "x" : `"x") + : (ƛ "y" : ‵"x" $ ƛ "x" : ‵"x")["x" := 𝟘] + = (ƛ "y" : 𝟘 $ ƛ "x" : ‵"x") := rfl -- https://plfa.github.io/Lambda/#reduction @@ -124,13 +125,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 @@ -196,7 +197,7 @@ namespace Term.Reduce lemma Clos.toClos'_left_inv : ∀ {x : m —↠ n}, x.toClos'.toClos = x := by intro | nil => rfl | cons car cdr => - simp_all only [Clos'.toClos, trans, cons.injEq, heq_eq_eq, true_and] + simp_all only [Clos.toClos', Clos'.toClos, Clos.trans, Clos.cons.injEq, heq_eq_eq, true_and] exact toClos'_left_inv (x := cdr) lemma Clos.toClos'_inj @@ -242,7 +243,7 @@ section examples example : twoC □ succC □ 𝟘 —↠ 2 := calc twoC □ succC □ 𝟘 - _ —→ (ƛ "z" : succC $ succC $ `"z") □ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam + _ —→ (ƛ "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 _ —→ 2 := by apply lamβ; exact Value.ofNat 1 @@ -250,19 +251,19 @@ section examples -- 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 + _ —→ (ƛ "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) := 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 @@ -335,7 +336,7 @@ namespace Context `IsTy c t tt` means that `t` can be inferred to be of type `tt` in the context `c`. -/ inductive IsTy : Context → Term → Ty → Type where - | tyVar : Γ ∋ x ⦂ t → IsTy Γ (` x) t + | 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 | tyZero : IsTy Γ 𝟘 ℕt @@ -344,6 +345,7 @@ namespace Context | tyMu : IsTy (Γ‚ x ⦂ t) m t → IsTy Γ (μ x : m) t deriving DecidableEq + -- set_option quotPrecheck false in notation:40 c " ⊢ " t " ⦂ " tt:51 => IsTy c t tt /-- @@ -366,24 +368,24 @@ namespace Context -- Inform `trivial` of our new tactic. macro_rules | `(tactic| trivial) => `(tactic| lookup_var) - open IsTy + open Context.IsTy -- https://plfa.github.io/Lambda/#quiz-2 - lemma twice_ty : Γ ⊢ (ƛ "s" : `"s" $ `"s" $ 𝟘) ⦂ ((ℕt =⇒ ℕt) =⇒ ℕt) := by + def twice_ty : Γ ⊢ (ƛ "s" : ‵"s" $ ‵"s" $ 𝟘) ⦂ ((ℕt =⇒ ℕt) =⇒ ℕt) := by apply tyLam; apply tyAp · trivial · apply tyAp · trivial · exact tyZero - theorem 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 -- https://plfa.github.io/Lambda/#derivation abbrev NatC (t : Ty) : Ty := (t =⇒ t) =⇒ t =⇒ t - theorem twoC_ty : Γ ⊢ twoC ⦂ NatC t := by + def twoC_ty : Γ ⊢ twoC ⦂ NatC t := by apply tyLam; apply tyLam; apply tyAp · trivial · apply tyAp <;> trivial @@ -391,7 +393,7 @@ namespace Context def addTy : Γ ⊢ add ⦂ ℕt =⇒ ℕt =⇒ ℕt := by repeat apply_rules [tyAp, tyMu, tyLam, tyCase, tySucc, tyZero] <;> trivial - theorem addC_ty : Γ ⊢ addC ⦂ NatC t =⇒ NatC t =⇒ NatC t := by + def addC_ty : Γ ⊢ addC ⦂ NatC t =⇒ NatC t =⇒ NatC t := by repeat apply tyLam <;> try trivial · repeat apply tyAp <;> try trivial @@ -400,50 +402,81 @@ namespace Context repeat apply_rules [tyAp, tyMu, tyLam, tyCase, tySucc, tyZero] <;> trivial -- https://plfa.github.io/Lambda/#exercise-mul%E1%B6%9C-practice-1 - theorem mulC_ty : Γ ⊢ mulC ⦂ NatC t =⇒ NatC t =⇒ NatC t := by + def mulC_ty : Γ ⊢ mulC ⦂ NatC t =⇒ NatC t =⇒ NatC t := by repeat apply tyLam <;> try trivial · repeat apply tyAp <;> try trivial end Context section examples - open Term Context Lookup IsTy + open Term Context Lookup Context.IsTy -- https://plfa.github.io/Lambda/#non-examples example : ∅ ⊬ 𝟘 □ 1 := by - by_contra h; simp_all only [not_isEmpty_iff] - cases h.some; contradiction + by_contra h; unfold NoTy at h; push Not at h + let ⟨tt, ht⟩ := h + cases ht with + | intro ht => + cases ht with + | tyAp hl hr => + cases hl - abbrev illLam := ƛ "x" : `"x" □ `"x" + abbrev illLam := ƛ "x" : ‵"x" □ ‵"x" lemma nty_illLam : ∅ ⊬ illLam := by - by_contra h; simp_all only [not_isEmpty_iff] - let tyLam (tyAp (tyVar hx) (tyVar hx')) := h.some - have := Lookup.functional hx hx'; simp_all only [Ty.t_to_t'_ne_t] + by_contra h; unfold NoTy at h; push Not at h + let ⟨tt, ht⟩ := h + cases ht with + | intro ht => + cases ht with + | tyLam ht' => + cases ht' with + | tyAp hl hr => + cases hl with + | tyVar hx => + cases hr with + | tyVar hx' => + have heq := Lookup.functional hx hx' + exact Ty.t_to_t'_ne_t _ _ heq -- 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" := by - by_contra h; simp_all only [not_isEmpty_iff] - let ⟨ht⟩ := h - cases ht; rename_i hy hx - · cases hx; rename_i ty hx - · cases hx; contradiction - - example : ∅‚ "y" ⦂ ℕt =⇒ ℕt ⊢ ƛ "x" : `"y" □ `"x" ⦂ ℕt =⇒ ℕt := by + example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊬ ‵"x" □ ‵"y" := by + by_contra h; unfold NoTy at h; push Not at h + let ⟨tt, ht⟩ := h + cases ht with + | intro ht => + cases ht with + | tyAp hl hr => + cases hl with + | tyVar hx => + cases hx with + | s hne _ => contradiction + + example : ∅‚ "y" ⦂ ℕt =⇒ ℕt ⊢ ƛ "x" : ‵"y" □ ‵"x" ⦂ ℕt =⇒ ℕt := by apply tyLam; apply tyAp <;> trivial - example : ∅‚ "x" ⦂ t ⊬ `"x" □ `"x" := by - by_contra h; simp_all only [not_isEmpty_iff] - let ⟨ht⟩ := h - cases ht; rename_i hx - · cases hx; rename_i hx - · cases hx <;> contradiction + example : ∅‚ "x" ⦂ t ⊬ ‵"x" □ ‵"x" := by + by_contra h; unfold NoTy at h; push Not at h + let ⟨tt, ht⟩ := h + cases ht with + | intro ht => + cases ht with + | tyAp hl hr => + cases hl with + | tyVar hl' => + cases hr with + | tyVar hr' => + cases hl' with + | z => + cases hr' with + | s hne _ => contradiction + | s hne _ => contradiction example : ∅‚ "x" ⦂ ℕt =⇒ ℕt‚ "y" ⦂ ℕt =⇒ ℕt - ⊢ ƛ "z" : (`"x" $ `"y" $ `"z") ⦂ ℕt =⇒ ℕt + ⊢ ƛ "z" : (‵"x" $ ‵"y" $ ‵"z") ⦂ ℕt =⇒ ℕt := by apply tyLam; apply tyAp <;> try trivial · apply tyAp <;> trivial diff --git a/Plfl/Lambda/Properties.lean b/Plfl/Lambda/Properties.lean index 285c3c2..d148aae 100644 --- a/Plfl/Lambda/Properties.lean +++ b/Plfl/Lambda/Properties.lean @@ -11,12 +11,12 @@ open Context Context.IsTy Term.Reduce open Sum -- https://plfa.github.io/Properties/#values-do-not-reduce -def Value.empty_reduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by +theorem Value.empty_reduce : Value m → ∀ {n}, IsEmpty (m —→ n) := by introv v; is_empty; intro r cases v <;> try contradiction · case succ v => cases r; · case succξ => apply (empty_reduce v).false; trivial -def Reduce.empty_value : m —→ n → IsEmpty (Value m) := by +theorem Reduce.empty_value : m —→ n → IsEmpty (Value m) := by intro r; is_empty; intro v have : ∀ {n}, IsEmpty (m —→ n) := Value.empty_reduce v exact this.false r @@ -33,34 +33,47 @@ namespace Canonical | tyZero, V𝟘 => canZero | tySucc t, Value.succ m => canSucc <| ofIsTy t m - def wellTyped : Canonical v t → ∅ ⊢ v ⦂ t × Value v := by - intro - | canLam h => exact ⟨tyLam h, Value.lam⟩ - | canZero => exact ⟨tyZero, V𝟘⟩ - | canSucc h => have ⟨ty, v⟩ := wellTyped h; exact ⟨tySucc ty, Value.succ v⟩ + def wellTyped : Canonical v t → ∅ ⊢ v ⦂ t × Value v + | canLam h => ⟨tyLam h, Value.lam⟩ + | canZero => ⟨tyZero, Value.zero⟩ + | canSucc h => ⟨tySucc (wellTyped h).1, Value.succ (wellTyped h).2⟩ - def wellTypedInv : ∅ ⊢ v ⦂ t × Value v → Canonical v t := by - intro - | ⟨tyLam ty, Value.lam⟩ => exact canLam ty - | ⟨tyZero, Value.zero⟩ => exact canZero - | ⟨tySucc ty, Value.succ v⟩ => apply canSucc; exact wellTypedInv ⟨ty, v⟩ + def wellTypedInv : ∅ ⊢ v ⦂ t × Value v → Canonical v t + | ⟨tyLam ty, Value.lam⟩ => canLam ty + | ⟨tyZero, Value.zero⟩ => canZero + | ⟨tySucc ty, Value.succ v⟩ => canSucc (wellTypedInv ⟨ty, v⟩) lemma wellTyped_left_inv (c : Canonical v t) : wellTypedInv (wellTyped c) = c := by - cases c with simp_all only [wellTypedInv, Prod.mk.eta, canSucc.injEq] - | canSucc c' => rename_i v'; exact @wellTyped_left_inv v' ℕt c' + induction c with + | canLam h => rfl + | canZero => rfl + | canSucc c' ih => + unfold wellTyped + generalize h_eq : wellTyped c' = pair + cases pair with + | mk ty v => + change canSucc (wellTypedInv ⟨ty, v⟩) = canSucc c' + rw [h_eq] at ih + rw [ih] lemma wellTyped_right_inv (c : ∅ ⊢ v ⦂ t × Value v) : wellTyped (wellTypedInv c) = c := by - match c with - | ⟨tyLam ty, Value.lam⟩ => simp_all only [wellTyped] - | ⟨tyZero, Value.zero⟩ => simp_all only [wellTyped] - | ⟨tySucc ty, Value.succ n⟩ => - rename_i v'; have := @wellTyped_right_inv v' ℕt ⟨ty, n⟩; - rw [wellTypedInv, wellTyped]; split - · simp_all only [Prod.mk.injEq] + rcases c with ⟨ty, v⟩ + cases v with + | lam => + cases ty with + | tyLam ty => rfl + | zero => + cases ty with + | tyZero => rfl + | succ n => + cases ty with + | tySucc ty => + have ih := @wellTyped_right_inv _ _ ⟨ty, n⟩ + simp only [wellTypedInv, wellTyped, ih] /-- The Canonical forms are exactly the well-typed values. @@ -152,8 +165,8 @@ namespace Progress instance : Progress m ≃ Progress' m where toFun := toProgress' invFun := fromProgress' - left_inv := by intro x; cases x <;> simp_all only [fromProgress', Progress', toProgress'] - right_inv := by intro x; cases x <;> simp_all only [Progress', toProgress', fromProgress'] + left_inv := by intro x; cases x <;> simp_all only [fromProgress', toProgress'] + right_inv := by intro x; cases x <;> simp_all only [toProgress', fromProgress'] end Progress -- https://plfa.github.io/Properties/#renaming @@ -192,7 +205,7 @@ namespace Renaming | tyMu j => apply tyMu; exact rename (ext ρ) j def Lookup.weaken : ∅ ∋ m ⦂ t → Γ ∋ m ⦂ t := by - intro. + intro h; cases h def weaken : ∅ ⊢ m ⦂ t → Γ ⊢ m ⦂ t := by intro j; refine rename ?_ j; exact Lookup.weaken @@ -305,7 +318,7 @@ section examples open Term -- def x : ℕ := x + 1 - abbrev succμ := μ "x" : ι `"x" + abbrev succμ := μ "x" : ι ‵"x" abbrev tySuccμ : ∅ ⊢ succμ ⦂ ℕt := by apply tyMu; apply tySucc; trivial @@ -333,35 +346,44 @@ end examples section subject_expansion open Term + abbrev illCase := 𝟘? 𝟘 [zero: 𝟘 |succ "x" : add] + -- https://plfa.github.io/Properties/#exercise-subject_expansion-practice example : IsEmpty (∀ {n t m}, ∅ ⊢ n ⦂ t → (m —→ n) → ∅ ⊢ m ⦂ t) := by - by_contra; simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff] - let illCase := 𝟘? 𝟘 [zero: 𝟘 |succ "x" : add] + refine ⟨fun f => ?_⟩ have nty_ill : ∅ ⊬ illCase := by - by_contra; simp_all only [not_isEmpty_iff]; rename_i t j - cases t <;> (simp only [illCase] at j; cases j; · contradiction) - rename_i f; have := f 𝟘 ℕt illCase tyZero zeroβ - exact nty_ill.false this.some + intro tt + refine ⟨fun j => ?_⟩ + cases j with + | tyCase _ jm jn => + cases jm with + | tyZero => + cases jn with + | tyMu jn' => + cases jn' + exact nty_ill.false (f tyZero zeroβ) + + abbrev illAp := (ƛ "x" : 𝟘) □ illLam example : IsEmpty (∀ {n t m}, ∅ ⊢ n ⦂ t → (m —→ n) → ∅ ⊢ m ⦂ t) := by - by_contra; simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff] - let illAp := (ƛ "x" : 𝟘) □ illLam + refine ⟨fun f => ?_⟩ have nty_ill : ∅ ⊬ illAp := by - by_contra; simp_all only [not_isEmpty_iff]; rename_i t j - cases t <;> ( - · cases j - · rename_i j; simp only [illAp] at j; cases j - · apply nty_illLam.false <;> trivial - ) - rename_i f; have := f 𝟘 ℕt illAp tyZero (lamβ Value.lam) - exact nty_ill.false this.some + intro tt + refine ⟨fun j => ?_⟩ + cases j with + | tyAp _ jr => + exact nty_illLam.false jr + have h_red : illAp —→ 𝟘 := by + apply lamβ + exact Value.lam + exact nty_ill.false (f tyZero h_red) end subject_expansion -- https://plfa.github.io/Properties/#well-typed-terms-dont-get-stuck abbrev Normal m := ∀ {n}, IsEmpty (m —→ n) abbrev Stuck m := Normal m ∧ IsEmpty (Value m) -example : Stuck (` "x") := by +example : Stuck (‵"x") := by unfold Stuck Normal; constructor · intro n; is_empty; nofun · is_empty; nofun @@ -370,7 +392,7 @@ example : Stuck (` "x") := by /-- No well-typed term can be stuck. -/ -def unstuck : ∅ ⊢ m ⦂ t → IsEmpty (Stuck m) := by +theorem unstuck : ∅ ⊢ m ⦂ t → IsEmpty (Stuck m) := by intro j; is_empty; simp_all only [and_imp] intro n ns; cases progress j · case step s => exact n.false s @@ -388,7 +410,7 @@ def preserves : ∅ ⊢ m ⦂ t → (m —↠ n) → ∅ ⊢ n ⦂ t := by _Well-typed terms don't get stuck_ (WTTDGS): starting from a well-typed term, taking any number of reduction steps leads to a term that is not stuck. -/ -def preserves_unstuck : ∅ ⊢ m ⦂ t → (m —↠ n) → IsEmpty (Stuck n) := by +theorem preserves_unstuck : ∅ ⊢ m ⦂ t → (m —↠ n) → IsEmpty (Stuck n) := by intro j r; have := preserves j r; exact unstuck this -- https://plfa.github.io/Properties/#reduction-is-deterministic diff --git a/Plfl/More.lean b/Plfl/More.lean index 42eb8b7..4892654 100644 --- a/Plfl/More.lean +++ b/Plfl/More.lean @@ -136,6 +136,31 @@ inductive Term : Context → Ty → Type where | caseList : Term Γ (.list a) → Term Γ b → Term (Γ‚ a‚ .list a) b → Term Γ b deriving DecidableEq, Repr +@[simp] +def Term.size : Term Γ a → Nat + | .var _ => 1 + | .lam t => t.size + 1 + | .ap l m => l.size + m.size + 1 + | .zero => 1 + | .succ t => t.size + 1 + | .case l m n => l.size + m.size + n.size + 1 + | .mu t => t.size + 1 + | .prim _ => 1 + | .mulP m n => m.size + n.size + 1 + | .let m n => m.size + n.size + 1 + | .prod m n => m.size + n.size + 1 + | .fst t => t.size + 1 + | .snd t => t.size + 1 + | .left t => t.size + 1 + | .right t => t.size + 1 + | .caseSum s l r => s.size + l.size + r.size + 1 + | .caseVoid v => v.size + 1 + | .unit => 1 + | .nil => 1 + | .cons m n => m.size + n.size + 1 + | .caseList l m n => l.size + m.size + n.size + 1 + + namespace Notation open Term @@ -148,13 +173,13 @@ namespace Notation scoped infixl:70 " □ " => ap scoped infixl:70 " ⋄ " => mulP scoped prefix:80 "ι " => succ - scoped prefix:90 "` " => var + scoped prefix:90 "‵" => var scoped notation "𝟘" => zero scoped notation "◯" => unit -- https://plfa.github.io/DeBruijn/#abbreviating-de-bruijn-indices - scoped macro "#" n:term:90 : term => `(`♯$n) + scoped macro "#" n:term:90 : term => `(‵♯$n) end Notation namespace Term @@ -215,7 +240,7 @@ namespace Subst -/ def rename : (∀ {a}, Γ ∋ a → Δ ∋ a) → Γ ⊢ a → Δ ⊢ a := by intro ρ; intro - | ` x => exact ` (ρ x) + | ‵ x => exact ‵ (ρ x) | ƛ n => exact ƛ (rename (ext ρ) n) | l □ m => exact rename ρ l □ rename ρ m | 𝟘 => exact 𝟘 @@ -252,7 +277,7 @@ namespace Subst -/ def exts : (∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ‚ b ∋ a → Δ‚ b ⊢ a := by intro σ; intro - | .z => exact `.z + | .z => exact ‵.z | .s x => apply shift; exact σ x /-- @@ -263,7 +288,7 @@ namespace Subst -/ def subst : (∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ ⊢ a → Δ ⊢ a := by intro σ; intro - | ` i => exact σ i + | ‵ i => exact σ i | ƛ n => exact ƛ (subst (exts σ) n) | l □ m => exact subst σ l □ subst σ m | 𝟘 => exact 𝟘 @@ -288,7 +313,7 @@ namespace Subst abbrev subst₁σ (v : Γ ⊢ b) : ∀ {a}, Γ‚ b ∋ a → Γ ⊢ a := by introv; intro | .z => exact v - | .s x => exact ` x + | .s x => exact ‵ x /-- Substitution for one free variable `v` in the term `n`. @@ -303,7 +328,7 @@ namespace Subst refine subst ?_ n; introv; intro | .z => exact w | .s .z => exact v - | .s (.s x) => exact ` x + | .s (.s x) => exact ‵ x end Subst namespace Notation @@ -420,10 +445,10 @@ namespace Notation end Notation namespace Reduce.Clos - abbrev refl : m —↠ m := .refl - abbrev tail : (m —↠ n) → (n —→ n') → (m —↠ n') := .tail - abbrev head : (m —→ n) → (n —↠ n') → (m —↠ n') := .head - abbrev single : (m —→ n) → (m —↠ n) := .single + abbrev refl : m —↠ m := Relation.ReflTransGen.refl + abbrev tail : (m —↠ n) → (n —→ n') → (m —↠ n') := Relation.ReflTransGen.tail + abbrev head : (m —→ n) → (n —↠ n') → (m —↠ n') := Relation.ReflTransGen.head + abbrev single : (m —→ n) → (m —↠ n) := Relation.ReflTransGen.single instance : Coe (m —→ n) (m —↠ n) where coe r := .single r @@ -440,12 +465,15 @@ namespace Reduce twoC □ succC □ 𝟘 _ —→ (ƛ (succC $ succC $ #0)) □ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam _ —→ (succC $ succC $ 𝟘) := by apply lamβ; exact V𝟘 - _ —→ succC □ 1 := by apply apξ₂; apply Value.lam; exact lamβ V𝟘 - _ —→ 2 := by apply lamβ; exact Value.ofNat 1 + _ —→ succC □ 1 := by + apply apξ₂ + · apply Value.lam + · unfold succC; exact lamβ V𝟘 + _ —→ 2 := by unfold succC; apply lamβ; exact Value.ofNat 1 end Reduce -- https://plfa.github.io/DeBruijn/#values-do-not-reduce -def Value.not_reduce : Value m → ∀ {n}, ¬ m —→ n := by +theorem Value.not_reduce : Value m → ∀ {n}, ¬ m —→ n := by introv v; intro r cases v with try contradiction | succ v => cases r; · case succξ => apply not_reduce v; trivial @@ -458,7 +486,7 @@ def Value.not_reduce : Value m → ∀ {n}, ¬ m —→ n := by | consξ₁ r => rename_i v _ _; apply not_reduce v; trivial | consξ₂ r => rename_i v _; apply not_reduce v; trivial -def Reduce.empty_value : m —→ n → IsEmpty (Value m) := by +theorem Reduce.empty_value : m —→ n → IsEmpty (Value m) := by intro r; is_empty; intro v; exact Value.not_reduce v r /-- @@ -470,7 +498,7 @@ inductive Progress (m : ∅ ⊢ a) where def Progress.progress : (m : ∅ ⊢ a) → Progress m := open Reduce in by intro - | ` _ => contradiction + | ‵ _ => contradiction | ƛ _ => exact .done .lam | l □ m => match progress l with | .step _ => apply step; apply apξ₁; trivial diff --git a/Plfl/More/Bisimulation.lean b/Plfl/More/Bisimulation.lean index 2e6f63b..40c401d 100644 --- a/Plfl/More/Bisimulation.lean +++ b/Plfl/More/Bisimulation.lean @@ -8,7 +8,7 @@ open Subst Notation -- https://plfa.github.io/Bisimulation/#simulation inductive Sim : (Γ ⊢ a) → (Γ ⊢ a) → Prop where -| var : Sim (` x) (` x) +| var : Sim (‵ x) (‵ x) | lam : Sim n n' → Sim (ƛ n) (ƛ n') | 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') @@ -16,7 +16,7 @@ inductive Sim : (Γ ⊢ a) → (Γ ⊢ a) → Prop where namespace Sim scoped infix:40 " ~ " => Sim - theorem refl_dec (t : Γ ⊢ a) : Decidable (t ~ t) := by + noncomputable def refl_dec (t : Γ ⊢ a) : Decidable (t ~ t) := by cases t with try (apply isFalse; intro s; contradiction) | var i => exact isTrue .var | lam t => diff --git a/Plfl/More/DoubleSubst.lean b/Plfl/More/DoubleSubst.lean index 76bf124..860b64a 100644 --- a/Plfl/More/DoubleSubst.lean +++ b/Plfl/More/DoubleSubst.lean @@ -32,14 +32,14 @@ lemma exts_comp {ρ : ∀ {a}, Γ ∋ a → Δ ∋ a} {σ : ∀ {a}, Δ ∋ a := by cases i <;> rfl -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L87 -lemma exts_var (i : Γ‚ b ∋ a) : exts var i = ` i := by cases i <;> rfl +lemma exts_var (i : Γ‚ b ∋ a) : exts var i = ‵ i := by cases i <;> rfl -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L73 lemma subst_comp {ρ : ∀ {a}, Γ ∋ a → Δ ∋ a} {σ : ∀ {a}, Δ ∋ a → Φ ⊢ a} (t : Γ ⊢ a) : subst σ (rename ρ t) = subst (σ ∘ ρ) t := by match t with - | ` i => trivial + | ‵ i => trivial | ƛ t => apply congr_arg lam; rw [subst_comp t] conv_lhs => arg 1; ext a t; simp only [Function.comp_apply, exts_comp t] @@ -84,7 +84,7 @@ lemma subst_comp {ρ : ∀ {a}, Γ ∋ a → Δ ∋ a} {σ : ∀ {a}, Δ ∋ a -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L93 lemma subst_var (t : Γ ⊢ a) : subst var t = t := by match t with - | ` i => apply congr_arg var; trivial + | ‵ i => apply congr_arg var; trivial | ƛ t => apply congr_arg lam conv_lhs => arg 1; ext a i; rw [exts_var i] @@ -129,8 +129,8 @@ lemma subst_var (t : Γ ⊢ a) : subst var t = t := by -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L104 theorem subst₁_shift : (shift (t : Γ ⊢ a))⟦(t' : Γ ⊢ b)⟧ = t := by - simp_all only [subst₁, subst₁σ, subst_comp] - conv_lhs => arg 1; ext a t'; simp + simp only [subst₁, subst_comp] + change subst var t = t rw [subst_var] -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L112 @@ -153,7 +153,7 @@ lemma insert_twice {Γ Δ Φ : Context} {a b c : Ty} (t : Γ‚‚ Δ‚‚ Φ = (rename (ext' (ext (ext' .s))) (rename (ext' .s) t) : (Γ‚ b‚‚ Δ)‚ c‚‚ Φ ⊢ a) := by match t with - | ` i => apply congr_arg var; exact insert_twice_idx i + | ‵ 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 | 𝟘 => trivial @@ -183,6 +183,7 @@ lemma insert_twice {Γ Δ Φ : Context} {a b c : Ty} (t : Γ‚‚ Δ‚‚ Φ | .caseList l m n => apply congr_arg₃ caseList <;> try apply insert_twice · rename_i a'; exact insert_twice (Φ := Φ‚ a'‚ .list a') n +termination_by t.size -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L132 lemma insert_subst_idx @@ -207,7 +208,7 @@ lemma insert_subst = rename (ext' .s) (subst (exts' σ) t) := by match t with - | ` i => exact insert_subst_idx i + | ‵ 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 | 𝟘 => trivial @@ -237,6 +238,7 @@ lemma insert_subst | .caseList l m n => apply congr_arg₃ caseList <;> try apply insert_subst · rename_i a'; exact insert_subst (Φ := Φ‚ a'‚ .list a') n +termination_by t.size -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L154 lemma shift_subst @@ -262,7 +264,7 @@ theorem subst_subst_comp : subst σ' (subst σ t) = subst (subst σ' ∘ σ) t := by match t with - | ` _ => trivial + | ‵ _ => trivial | ƛ t => apply congr_arg lam rw [subst_subst_comp (σ := exts σ) (σ' := exts σ') t] @@ -317,5 +319,5 @@ theorem double_subst simp only [subst₂, subst₁, subst_subst_comp]; congr; ext simp only [Function.comp_apply, subst₁σ]; split · simp only [subst₁_shift] - · simp only [shift_subst]; rfl - · simp only [shift_subst]; rfl + · rfl + · rfl diff --git a/Plfl/More/Inference.lean b/Plfl/More/Inference.lean index 08294cd..517c1ea 100644 --- a/Plfl/More/Inference.lean +++ b/Plfl/More/Inference.lean @@ -98,7 +98,7 @@ namespace Notation -- scoped postfix:60 "↑ " => inh scoped infixl:70 " □ " => ap scoped prefix:80 "ι " => succ - scoped prefix:90 "` " => var + scoped prefix:90 "‵" => var scoped notation "𝟘" => zero end Notation @@ -113,16 +113,16 @@ instance : Coe TermS TermI where coe := TermI.inh abbrev add : TermS := (μ "+" : ƛ "m" : ƛ "n" : - 𝟘? `"m" - [zero: `"n" - |succ "m" : ι (`"+" □ `"m" □ `"n")] + 𝟘? ‵"m" + [zero: ‵"n" + |succ "m" : ι (‵"+" □ ‵"m" □ ‵"n")] ).the (ℕt =⇒ ℕt =⇒ ℕt) abbrev mul : TermS := (μ "*" : ƛ "m" : ƛ "n" : - 𝟘? `"m" + 𝟘? ‵"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`. @@ -134,11 +134,11 @@ The Church numeral Ty. @[simp] abbrev Ch (t : Ty := ℕt) : Ty := (t =⇒ t) =⇒ t =⇒ t -- Church encoding... -abbrev succC : TermI := ƛ "n" : ι `"n" -abbrev oneC : TermI := ƛ "s" : ƛ "z" : `"s" $ `"z" -abbrev twoC : TermI := ƛ "s" : ƛ "z" : `"s" $ `"s" $ `"z" +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 □ 𝟘 @@ -187,7 +187,7 @@ mutual Typing of `TermS` terms. -/ inductive TyS : Context → TermS → Ty → Type where - | var : Γ ∋ x ⦂ a → TyS Γ (` x) a + | var : Γ ∋ x ⦂ a → TyS Γ (‵ x) a | 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 @@ -280,11 +280,11 @@ Nothing to do. Relevant definitions have been derived. -/ -- https://plfa.github.io/Inference/#unique-types -theorem Lookup.unique (i : Γ ∋ x ⦂ a) (j : Γ ∋ x ⦂ b) : a = b := by - cases i with try trivial - | z => cases j <;> trivial - | s => cases j with try trivial - | s => apply unique <;> trivial +theorem Lookup.unique : (i : Γ ∋ x ⦂ a) → (j : Γ ∋ x ⦂ b) → a = b +| .z, .z => rfl +| .z, .s h _ => (h rfl).elim +| .s h _, .z => (h rfl).elim +| .s _ i, .s _ j => unique i j theorem TyS.unique (t : Γ ⊢ x ⇡ a) (u : Γ ⊢ x ⇡ b) : a = b := by match t with @@ -309,8 +309,8 @@ def Lookup.lookup (Γ : Context) (x : Sym) : Decidable' (Σ a, Γ ∋ x ⦂ a) : if h : x = y then right; subst h; exact ⟨b, .z⟩ else match lookup Γ x with - | .inr ⟨a, i⟩ => right; refine ⟨a, .s ?_ i⟩; trivial - | .inl n => left; refine empty_ext_empty ?_ n; trivial + | .inr ⟨a, i⟩ => right; exact ⟨a, .s h i⟩ + | .inl n => left; exact empty_ext_empty h n -- https://plfa.github.io/Inference/#promoting-negations lemma TyS.empty_arg @@ -327,9 +327,9 @@ lemma TyS.empty_switch : Γ ⊢ m ⇡ a → a ≠ b → IsEmpty (Γ ⊢ m ⇡ b) mutual def TermS.infer (m : TermS) (Γ : Context) : Decidable' (Σ a, Γ ⊢ m ⇡ a) := by match m with - | ` x => match Lookup.lookup Γ x with + | ‵ x => match Lookup.lookup Γ x with | .inr ⟨a, i⟩ => right; exact ⟨a, .var i⟩ - | .inl n => left; is_empty; intro ⟨a, .var _⟩; apply n.false; exists a + | .inl n => left; is_empty; intro ⟨a, .var i⟩; exact n.false ⟨a, i⟩ | l □ m => match l.infer Γ with | .inr ⟨a =⇒ b, tab⟩ => match m.infer Γ a with | .inr ta => right; exact ⟨b, .ap tab ta⟩ @@ -339,11 +339,11 @@ mutual | .inl n => left; is_empty; intro ⟨a, .ap tl _⟩; rename_i b _; exact n.false ⟨b =⇒ a, tl⟩ | .prod m n => match m.infer Γ, n.infer Γ with | .inr ⟨a, tm⟩, .inr ⟨b, tn⟩ => right; exact ⟨a * b, tm.prod tn⟩ - | .inr _, .inl nn => left; is_empty; intro ⟨_, tmn⟩; cases tmn; apply nn.false; constructor <;> trivial - | .inl nm, _ => left; is_empty; intro ⟨_, .prod tm _⟩; apply nm.false; constructor <;> trivial + | .inr _, .inl nn => left; is_empty; intro ⟨_, .prod tm tn⟩; exact nn.false ⟨_, tn⟩ + | .inl nm, _ => left; is_empty; intro ⟨_, .prod tm _⟩; exact nm.false ⟨_, tm⟩ | .syn m a => match m.infer Γ a with | .inr t => right; exact ⟨a, t⟩ - | .inl n => left; is_empty; intro ⟨a', t'⟩; cases t'; apply n.false; trivial + | .inl n => left; is_empty; intro ⟨a', t'⟩; cases t' with | syn t' => exact n.false t' def TermI.infer (m : TermI) (Γ : Context) (a : Ty) : Decidable' (Γ ⊢ m ⇣ a) := by match m with @@ -366,11 +366,11 @@ mutual | .case l m x n => match l.infer Γ with | .inr ⟨ℕt, tl⟩ => match m.infer Γ a, n.infer (Γ‚ x ⦂ ℕt) a with | .inr tm, .inr tn => right; exact .case tl tm tn - | .inl nm, _ => left; is_empty; intro (.case _ _ _); apply nm.false; trivial - | .inr _, .inl nn => left; is_empty; intro (.case _ _ _); apply nn.false; trivial + | .inl nm, _ => left; is_empty; intro (.case _ tm _); exact nm.false tm + | .inr _, .inl nn => left; is_empty; intro (.case _ _ tn); exact nn.false tn | .inr ⟨_ =⇒ _, tl⟩ => left; is_empty; intro (.case t _ _); injection t.unique tl | .inr ⟨.prod _ _, tl⟩ => left; is_empty; intro (.case t _ _); injection t.unique tl - | .inl nl => left; is_empty; intro (.case _ _ _); apply nl.false; constructor <;> trivial + | .inl nl => left; is_empty; intro (.case tl' _ _); exact nl.false ⟨ℕt, tl'⟩ | μ x : n => match n.infer (Γ‚ x ⦂ a) a with | .inr t => right; exact .mu t | .inl n => left; is_empty; intro (.mu t); exact n.false t @@ -378,7 +378,10 @@ mutual | .inr ⟨.prod b _, tm⟩ => if h : a = b then right; subst h; exact .fst tm else - left; is_empty; intro (.fst t); injection t.unique tm; contradiction + left; is_empty; intro (.fst tm') + have eq := tm'.unique tm + injection eq with eq' + exact h eq' | .inr ⟨ℕt, tm⟩ => left; is_empty; intro (.fst t); injection t.unique tm | .inr ⟨_ =⇒ _, tm⟩ => left; is_empty; intro (.fst t); injection t.unique tm | .inl n => left; is_empty; intro (.fst t); apply n.false; constructor <;> trivial @@ -386,7 +389,10 @@ mutual | .inr ⟨.prod _ b, tm⟩ => if h : a = b then right; subst h; exact .snd tm else - left; is_empty; intro (.snd t); injection t.unique tm; contradiction + left; is_empty; intro (.snd tm') + have eq := tm'.unique tm + injection eq with _ eq' + exact h eq' | .inr ⟨ℕt, tm⟩ => left; is_empty; intro (.snd t); injection t.unique tm | .inr ⟨_ =⇒ _, tm⟩ => left; is_empty; intro (.snd t); injection t.unique tm | .inl n => left; is_empty; intro (.snd t); apply n.false; constructor <;> trivial @@ -394,8 +400,8 @@ mutual | .inr ⟨b, tm⟩ => if h : a = b then right; subst h; exact .inh tm else - left; rw [←Ne.def] at h; is_empty; intro (.inh _) - apply (tm.empty_switch h.symm).false; trivial + left; is_empty; intro (.inh tm') + exact h (tm.unique tm').symm | .inl nm => left; is_empty; intro (.inh tm); apply nm.false; exists a end @@ -424,7 +430,7 @@ abbrev four''Ty : Γ ⊢ four'' ⇡ ℕt := open TyS TyI Lookup in by repeat apply_rules [var, ap, prod, syn, lam, zero, succ, case, mu, fst, snd, inh, - addCTy, twoCTy] + mulTy, twoTy] <;> elem example : four''.infer ∅ = .inr ⟨ℕt, four''Ty⟩ := by rfl @@ -436,7 +442,7 @@ Sadly this won't work for now due to limitations with mutual recursions. See: -/ --- example := show ((ƛ "x" : `"y").the (ℕt =⇒ ℕt)).infer ∅ = .inl _ by rfl +-- example := show ((ƛ "x" : ‵"y").the (ℕt =⇒ ℕt)).infer ∅ = .inl _ by rfl /- This won't work either, probably due to similar reasons... @@ -444,11 +450,11 @@ This won't work either, probably due to similar reasons... -- instance : Decidable (Nonempty (Σ a, Γ ⊢ m ⇡ a)) := (m.infer Γ).toDecidable --- example := let m := (ƛ "x" : `"y").the (ℕt =⇒ ℕt); show IsEmpty (Σ a, ∅ ⊢ m ⇡ a) by +-- example := let m := (ƛ "x" : ‵"y").the (ℕt =⇒ ℕt); show IsEmpty (Σ a, ∅ ⊢ m ⇡ a) by -- rw [←not_nonempty_iff]; decide -- Unbound variable: -#eval ((ƛ "x" : `"y").the (ℕt =⇒ ℕt)).infer ∅ +#eval ((ƛ "x" : ‵"y").the (ℕt =⇒ ℕt)).infer ∅ -- Argument in application is ill typed: #eval (add □ succC).infer ∅ @@ -472,13 +478,13 @@ This won't work either, probably due to similar reasons... #eval ((ι twoC).the ℕt).infer ∅ -- Case of a term with a function type: -#eval ((𝟘? twoC.the Ch [zero: 𝟘 |succ "x" : `"x"]).the ℕt).infer ∅ +#eval ((𝟘? twoC.the Ch [zero: 𝟘 |succ "x" : ‵"x"]).the ℕt).infer ∅ -- Case of an ill-typed term: -#eval ((𝟘? twoC.the ℕt [zero: 𝟘 |succ "x" : `"x"]).the ℕt).infer ∅ +#eval ((𝟘? twoC.the ℕt [zero: 𝟘 |succ "x" : ‵"x"]).the ℕt).infer ∅ -- Inherited and synthesized types disagree in a switch: -#eval ((ƛ "x" : `"x").the (ℕt =⇒ ℕt =⇒ ℕt)).infer ∅ +#eval ((ƛ "x" : ‵"x").the (ℕt =⇒ ℕt =⇒ ℕt)).infer ∅ -- https://plfa.github.io/Inference/#erasure def Ty.erase : Ty → More.Ty diff --git a/Plfl/Untyped.lean b/Plfl/Untyped.lean index f04d855..44af7ec 100644 --- a/Plfl/Untyped.lean +++ b/Plfl/Untyped.lean @@ -1,3 +1,5 @@ +-- module + -- https://plfa.github.io/Untyped/ import Plfl.Init @@ -45,16 +47,16 @@ end Notation -- https://plfa.github.io/Untyped/#exercise-context%E2%84%95-practice instance Context.equiv_nat : Context ≃ ℕ where toFun := List.length - invFun := (List.replicate · ✶) + invFun := (List.replicate · (✶)) left_inv := left_inv right_inv := by intro; simp only [List.length_replicate] where left_inv := by intro | [] => trivial - | ✶ :: ss => calc List.replicate (✶ :: ss).length ✶ - _ = List.replicate (ss.length + 1) ✶ := by rw [List.length_cons ✶ ss] - _ = ✶ :: List.replicate ss.length ✶ := by rw [List.replicate_succ ✶ ss.length] - _ = ✶ :: ss := by have := left_inv ss; simp_all only + | (✶) :: ss => calc List.replicate ((✶) :: ss).length (✶) + _ = List.replicate (ss.length + 1) (✶) := by rw [List.length_cons] + _ = (✶) :: List.replicate ss.length (✶) := by rw [List.replicate_succ] + _ = (✶) :: ss := by have := left_inv ss; simp_all only instance : Coe ℕ Context where coe := Context.equiv_nat.invFun @@ -89,8 +91,8 @@ inductive Term : Context → Ty → Type where -- Lookup | var : Γ ∋ a → Term Γ a -- Lambda -| lam : Term (Γ‚ ✶ /- a -/) ✶ /- b -/ → Term Γ ✶ /- (a =⇒ b) -/ -| ap : Term Γ ✶ /- (a =⇒ b) -/ → Term Γ ✶ /- a -/ → Term Γ ✶ /- b -/ +| lam : Term (Γ‚ (✶) /- a -/) (✶) /- b -/ → Term Γ (✶) /- (a =⇒ b) -/ +| ap : Term Γ (✶) /- (a =⇒ b) -/ → Term Γ (✶) /- a -/ → Term Γ (✶) /- b -/ deriving DecidableEq, Repr namespace Notation @@ -101,10 +103,10 @@ namespace Notation scoped prefix:50 "ƛ " => lam scoped infixr:min " $ " => ap scoped infixl:70 " □ " => ap - scoped prefix:90 "` " => var + scoped prefix:90 "‵" => var -- https://plfa.github.io/Untyped/#writing-variables-as-numerals - scoped macro "#" n:term:90 : term => `(`♯$n) + scoped macro "#" n:term:90 : term => `(‵ ♯$n) end Notation namespace Term @@ -127,28 +129,26 @@ namespace Subst If one context maps to another, the mapping holds after adding the same variable to both contexts. -/ - def ext : (∀ {a}, Γ ∋ a → Δ ∋ a) → Γ‚ b ∋ a → Δ‚ b ∋ a := by - intro ρ; intro - | .z => exact .z - | .s x => refine .s ?_; exact ρ x + def ext (Base : ∀ {a}, Γ ∋ a → Δ ∋ a) : ∀ {a}, Γ‚ b ∋ a → Δ‚ b ∋ a + | _, .z => .z + | _, .s x => .s (Base x) /-- If one context maps to another, then the type judgements are the same in both contexts. -/ - def rename : (∀ {a}, Γ ∋ a → Δ ∋ a) → Γ ⊢ a → Δ ⊢ a := by + def rename : (Base : ∀ {a}, Γ ∋ a → Δ ∋ a) → Γ ⊢ a → Δ ⊢ a := by intro ρ; intro - | ` x => exact ` (ρ x) + | ‵ x => exact ‵ (ρ x) | ƛ n => exact ƛ (rename (ext ρ) n) | l □ m => exact rename ρ l □ rename ρ m abbrev shift : Γ ⊢ a → Γ‚ b ⊢ a := rename .s -- https://plfa.github.io/Untyped/#simultaneous-substitution - def exts : (∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ‚ b ∋ a → Δ‚ b ⊢ a := by - intro σ; intro - | .z => exact `.z - | .s x => apply shift; exact σ x + def exts (Base : ∀ {a}, Γ ∋ a → Δ ⊢ a) : ∀ {a}, Γ‚ b ∋ a → Δ‚ b ⊢ a + | _, .z => ‵ .z + | _, .s x => shift (Base x) /-- General substitution for multiple free variables. @@ -156,23 +156,22 @@ namespace Subst then the type judgements are the same before and after the mapping, i.e. after replacing the free variables in the former with (expanded) terms. -/ - def subst : (∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ ⊢ a → Δ ⊢ a := by + def subst : (Base : ∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ ⊢ a → Δ ⊢ a := by intro σ; intro - | ` i => exact σ i + | ‵ i => exact σ i | ƛ n => exact ƛ (subst (exts σ) n) | l □ m => exact subst σ l □ subst σ m -- https://plfa.github.io/Untyped/#single-substitution - abbrev subst₁σ (v : Γ ⊢ b) : ∀ {a}, Γ‚ b ∋ a → Γ ⊢ a := by - introv; intro - | .z => exact v - | .s x => exact ` x + abbrev subst₁σ (v : Γ ⊢ b) : ∀ {a}, Γ‚ b ∋ a → Γ ⊢ a + | _, .z => v + | _, .s x => ‵ x /-- Substitution for one free variable `v` in the term `n`. -/ - abbrev subst₁ (v : Γ ⊢ b) (n : Γ‚ b ⊢ a) : Γ ⊢ a := by - refine subst ?_ n; exact subst₁σ v + abbrev subst₁ (v : Γ ⊢ b) (n : Γ‚ b ⊢ a) : Γ ⊢ a := + subst (subst₁σ v) n end Subst open Subst @@ -185,7 +184,7 @@ end Notation -- https://plfa.github.io/Untyped/#neutral-and-normal-terms mutual inductive Neutral : Γ ⊢ a → Type - | var : (x : Γ ∋ a) → Neutral (` x) + | var : (x : Γ ∋ a) → Neutral (‵ x) | ap : Neutral l → Normal m → Neutral (l □ m) deriving Repr @@ -206,7 +205,7 @@ namespace Notation scoped prefix:50 "ƛₙ " => lam scoped infixr:min " $ₙ " => ap scoped infixl:70 " □ₙ " => ap - scoped prefix:90 "`ₙ " => var + scoped prefix:90 "‵ₙ" => var end Notation example : Normal (Term.twoC (Γ := ∅)) := ƛₙ ƛₙ (′#′1 □ₙ (′#′1 □ₙ (′#′0))) @@ -258,25 +257,31 @@ namespace Notation end Notation namespace Reduce.Clos - @[refl] abbrev refl : m —↠ m := .refl - abbrev tail : (m —↠ n) → (n —→ n') → (m —↠ n') := .tail - abbrev head : (m —→ n) → (n —↠ n') → (m —↠ n') := .head - abbrev single : (m —→ n) → (m —↠ n) := .single + @[refl] abbrev refl : m —↠ m := Relation.ReflTransGen.refl + abbrev tail : (m —↠ n) → (n —→ n') → (m —↠ n') := Relation.ReflTransGen.tail + abbrev head : (m —→ n) → (n —↠ n') → (m —↠ n') := Relation.ReflTransGen.head + abbrev single : (m —→ n) → (m —↠ n) := Relation.ReflTransGen.single - instance : Coe (m —→ n) (m —↠ n) where coe r := .single r + instance : Coe (m —→ n) (m —↠ n) where coe r := Relation.ReflTransGen.single r - instance : Trans (α := Γ ⊢ a) Clos Clos Clos where trans := .trans - instance : Trans (α := Γ ⊢ a) Clos Reduce Clos where trans c r := c.tail r - instance : Trans (α := Γ ⊢ a) Reduce Reduce Clos where trans r r' := .tail r r' - instance : Trans (α := Γ ⊢ a) Reduce Clos Clos where trans r c := .head r c + instance : Trans (α := Γ ⊢ a) Clos Clos Clos where trans := Relation.ReflTransGen.trans + instance : Trans (α := Γ ⊢ a) Clos Reduce Clos where trans c r := Relation.ReflTransGen.tail c r + instance : Trans (α := Γ ⊢ a) Reduce Reduce Clos where trans r r' := Relation.ReflTransGen.tail (Relation.ReflTransGen.single r) r' + instance : Trans (α := Γ ⊢ a) Reduce Clos Clos where trans r c := Relation.ReflTransGen.head r c end Reduce.Clos namespace Reduce -- https://plfa.github.io/Untyped/#example-reduction-sequence open Term + theorem test_shift_twoC : shift (shift (shift (twoC (Γ := ∅)))) = twoC (Γ := ∅‚ ✶‚ ✶‚ ✶) := by + simp_all only [List.empty_eq] + rfl + example : fourC' (Γ := ∅) —↠ fourC := calc addC □ twoC □ twoC - _ —→ (ƛ ƛ ƛ (twoC □ #1 $ (#2 □ #1 □ #0))) □ twoC := by apply_rules [apξ₁, lamβ] + _ —→ (ƛ ƛ ƛ (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β] @@ -292,44 +297,36 @@ inductive Progress (m : Γ ⊢ a) where | step : (m —→ n) → Progress m | done : Normal m → Progress m +namespace Progress + /-- If a term is well-scoped, then it satisfies progress. -/ -def Progress.progress : (m : Γ ⊢ a) → Progress m := open Reduce in by - intro - | ` x => apply done; exact ′`ₙ x +def progress : (m : Γ ⊢ ✶) → Progress m + | ‵ x => .done (′ ‵ₙ x) | ƛ n => - have : sizeOf n < sizeOf (ƛ n) := by simp only [ - Term.lam.sizeOf_spec, lt_add_iff_pos_left, - add_pos_iff, zero_lt_one, true_or, - ] + have : sizeOf n < sizeOf (ƛ n) := by simp only [Term.lam.sizeOf_spec]; omega match progress n with - | .done n => apply done; exact ƛₙ n - | .step n => apply step; exact lamζ n - | ` x □ m => - have : sizeOf m < sizeOf (` x □ m) := by simp only [ - Term.ap.sizeOf_spec, Term.var.sizeOf_spec, - Ty.star.sizeOf_spec, lt_add_iff_pos_left, - add_pos_iff, zero_lt_one, true_or, or_self, - ] + | .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 match progress m with - | .done m => apply done; exact ′`ₙx □ₙ m - | .step m => apply step; exact apξ₂ m - | (ƛ n) □ m => apply step; exact lamβ - | l@(_ □ _) □ m => - have : sizeOf l < sizeOf (l □ m) := by simp_arith - match progress l with - | .step l => simp_all only [namedPattern]; apply step; exact apξ₁ l - | .done (′l') => - simp_all only [namedPattern]; rename_i h; simp only [h.symm, Term.ap.sizeOf_spec] - have : sizeOf m < sizeOf (l □ m) := by - aesop_subst h; simp only [ - Term.ap.sizeOf_spec, lt_add_iff_pos_left, add_pos_iff, - zero_lt_one, true_or, or_self, - ] + | .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 + | .step r => .step (Reduce.apξ₁ r) + | .done (′neutral_l) => + have : sizeOf m < sizeOf ((l' □ l'') □ m) := by simp only [Term.ap.sizeOf_spec]; omega match progress m with - | .done m => apply done; exact ′l' □ₙ m - | .step m => apply step; exact apξ₂ m + | .done m' => .done (′neutral_l □ₙ m') + | .step r => .step (Reduce.apξ₂ r) +termination_by m => sizeOf m + +end Progress open Progress (progress) @@ -405,7 +402,7 @@ section examples abbrev fourS'' : Γ ⊢ ✶ := mulS □ twoS □ twoS abbrev evalRes (l : ∅ ⊢ a) (gas := 100) := (eval gas l).3 - + -- abbrev evalResStar (l : ∅ ⊢ ✶) (gas := 100) := (eval gas l).3 #eval evalRes (gas := 3) fourC' #eval evalRes fourC' diff --git a/Plfl/Untyped/BigStep.lean b/Plfl/Untyped/BigStep.lean index 20bb1ea..f87d4d6 100644 --- a/Plfl/Untyped/BigStep.lean +++ b/Plfl/Untyped/BigStep.lean @@ -22,7 +22,7 @@ An environment in call-by-name is a mapping from variables to closures. -/ abbrev ClosEnv (Γ : Context) := (Γ ∋ ✶) → Clos -def ClosEnv.empty : ClosEnv ∅ := by intro. +def ClosEnv.empty : ClosEnv ∅ := nofun instance ClosEnv.instEmptyCollection : EmptyCollection (ClosEnv ∅) where emptyCollection := empty @@ -39,7 +39,7 @@ end Notation open Notation inductive Eval : ClosEnv Γ → (Γ ⊢ ✶) → Clos → Prop where -| var : γ i = .clos m δ → Eval δ m v → Eval γ (` i) v +| 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 @@ -59,7 +59,7 @@ theorem Eval.determ (e : γ ⊢ m ⇓ v) (e' : γ ⊢ m ⇓ v') : v = v' := by induction e generalizing v' with cases e' | lam => rfl | var h _ ih => - subst_vars; rename_i h' e'; injection h.symm.trans h' + rename_i h' e'; injection h.symm.trans h' rename_i h hh hh'; subst h; rw [←hh.eq, ←hh'.eq] at e'; exact ih e' | ap _ _ ih ih₁ => rename_i e' e₁'; apply ih₁; injection ih e' @@ -84,13 +84,13 @@ section open Untyped.Subst open Substitution - @[simp] lemma ClosEnv.empty_equiv_ids : ∅ ~~ₑ ids := by intro. + @[simp] lemma ClosEnv.empty_equiv_ids : ∅ ~~ₑ ids := nofun abbrev ext_subst (σ : Subst Γ Δ) (n : Δ ⊢ ✶) : Subst (Γ‚ ✶) Δ := (·⟦n⟧) ∘ exts σ lemma subst₁σ_exts {σ : Subst Γ Δ} {m : Δ ⊢ b} {i : Γ ∋ ✶} : (ext_subst σ m) (.s i) = σ i - := by simp only [subst₁σ_exts_cons] + := by simp only [subst₁σ_exts_cons]; simp_all only [cons] theorem ClosEnv.ext {γ : ClosEnv Γ} {σ : Subst Γ ∅} {n : ∅ ⊢ ✶} (ee : γ ~~ₑ σ) (e : v ~~ n) : (γ‚' v ~~ₑ ext_subst σ n) diff --git a/Plfl/Untyped/Confluence.lean b/Plfl/Untyped/Confluence.lean index a025a73..df77304 100644 --- a/Plfl/Untyped/Confluence.lean +++ b/Plfl/Untyped/Confluence.lean @@ -13,7 +13,7 @@ open Untyped.Notation Parallel reduction. -/ inductive PReduce : (Γ ⊢ a) → (Γ ⊢ a) → Prop where -| var : PReduce (` x) (` x) +| var : PReduce (‵ x) (‵ x) | 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') @@ -22,7 +22,7 @@ namespace PReduce @[refl] theorem refl (m : Γ ⊢ a) : PReduce m m := by match m with - | ` i => exact .var + | ‵ i => exact .var | ƛ n => apply lamζ; apply refl | l □ m => apply apξ <;> apply refl @@ -40,14 +40,14 @@ open Notation namespace PReduce.Clos abbrev single (p : m ⇛ n) : (m ⇛* n) := .head p .refl - abbrev tail : (m ⇛* n) → (n ⇛ n') → (m ⇛* n') := .tail - abbrev trans : (m ⇛* n) → (n ⇛* n') → (m ⇛* n') := .trans + abbrev tail : (m ⇛* n) → (n ⇛ n') → (m ⇛* n') := Relation.ReflTransGen.tail + abbrev trans : (m ⇛* n) → (n ⇛* n') → (m ⇛* n') := Relation.ReflTransGen.trans instance : Coe (m ⇛ n) (m ⇛* n) where coe := .single end PReduce.Clos namespace PReduce - instance : IsRefl (Γ ⊢ a) PReduce where refl := .refl + instance {Γ a} : Std.Refl (@PReduce Γ a) where refl := .refl instance : Trans (α := Γ ⊢ a) Clos Clos Clos where trans := .trans instance : Trans (α := Γ ⊢ a) Clos PReduce Clos where trans c r := c.tail r @@ -137,7 +137,7 @@ end Many parallel reductions at once. -/ abbrev PReduce.plus : (Γ ⊢ a) → (Γ ⊢ a) -| ` i => ` i +| ‵ i => ‵ i | ƛ n => ƛ (plus n) | (ƛ n) □ m => plus n⟦plus m⟧ | l □ m => plus l □ plus m @@ -152,7 +152,7 @@ intro | .lamβ pn pv => exact subst_par (par_subst₁σ (par_triangle pv)) (par_triangle pn) | .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) | ƛ _ => have .lamζ pl := pl; exact lamβ (par_triangle pl) (par_triangle pm) diff --git a/Plfl/Untyped/Denotational.lean b/Plfl/Untyped/Denotational.lean index 6d53ab9..456140c 100644 --- a/Plfl/Untyped/Denotational.lean +++ b/Plfl/Untyped/Denotational.lean @@ -18,7 +18,7 @@ deriving BEq, DecidableEq, Repr namespace Value instance instBot : Bot Value where bot := .bot - instance instSup : Sup Value where sup := .conj + instance instMax : Max Value where max := .conj end Value namespace Notation @@ -119,7 +119,7 @@ end Env namespace Notation instance : Bot (Env Γ) where bot _ := ⊥ - instance : Sup (Env γ) where sup := Env.conj + instance : Max (Env Γ) where max := Env.conj scoped infix:40 " `⊑ " => Env.Sub end Notation @@ -143,7 +143,7 @@ end Env.Sub `Eval γ m v` means that evaluating the term `m` in the environment `γ` gives `v`. -/ inductive Eval : Env Γ → (Γ ⊢ ✶) → Value → Prop where -| var : Eval γ (` i) (γ i) +| var : Eval γ (‵ i) (γ i) | 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 ⊥ @@ -276,18 +276,18 @@ A path consists of `n` edges (`⇾`s) and `n + 1` vertices (`Value`s). -/ def Value.path : (n : ℕ) → Vector Value (n + 1) → Value | 0, _ => ⊥ -| i + 1, vs => path i vs.dropLast ⊔ vs.get i ⇾ vs.get (i + 1) +| i + 1, vs => path i vs.dropLast ⊔ vs[i] ⇾ vs[i + 1] /-- Returns the denotation of the nth Church numeral for a given path. -/ def Value.church (n : ℕ) (vs : Vector Value (n + 1)) : Value := - path n vs ⇾ vs.get 0 ⇾ vs.get n + path n vs ⇾ vs[0] ⇾ vs[n] namespace Example - example : Value.church 0 ⟨[u], rfl⟩ = (⊥ ⇾ u ⇾ u) := rfl - example : Value.church 1 ⟨[u, v], rfl⟩ = ((⊥ ⊔ u ⇾ v) ⇾ u ⇾ v) := rfl - example : Value.church 2 ⟨[u, v, w], rfl⟩ = ((⊥ ⊔ u ⇾ v ⊔ v ⇾ w) ⇾ u ⇾ w) := rfl + example : Value.church 0 #v[u] = (⊥ ⇾ u ⇾ u) := rfl + example : Value.church 1 #v[u, v] = ((⊥ ⊔ u ⇾ v) ⇾ u ⇾ v) := rfl + example : Value.church 2 #v[u, v, w] = ((⊥ ⊔ u ⇾ v ⊔ v ⇾ w) ⇾ u ⇾ w) := rfl end Example section @@ -297,16 +297,20 @@ section def denot_church {vs} : `∅ ⊢ church n ￬ Value.church n vs := by apply_rules [fn]; induction n with - | zero => let ⟨_ :: [], _⟩ := vs; exact var + | zero => exact var | succ n r => unfold church.applyN; apply ap · apply sub var; simp only [Env.snoc, Value.path]; convert Sub.refl.conjR₂ - rw [←Fin.instAddMonoidWithOne.proof_2] · convert sub_env (@r vs.dropLast) ?_ using 1 - · simp only [vs.get_dropLast n, Fin.coe_ofNat_eq_mod] - congr; simp_arith [Nat.mod_eq_of_lt] - · simp only [vs.get_dropLast 0, Fin.coe_ofNat_eq_mod] - apply_rules [le_ext, ext_le]; exact .conjR₁ .refl + · exact (Vector.get_dropLast vs ⟨n, by omega⟩).symm + · intro x; cases x with + | z => + have : vs.dropLast[0] = vs[0] := by exact Vector.get_dropLast vs ⟨0, by omega⟩ + exact this ▸ Sub.refl + | s i => + cases i with + | z => exact .conjR₁ .refl + | s i' => cases i' end -- https://plfa.github.io/Denotational/#inversion-of-the-less-than-relation-for-functions @@ -314,7 +318,7 @@ def Value.Elem (u v : Value) : Prop := match v with | .conj v w => u.Elem v ∨ u.Elem w | v => u = v -instance Value.membership : Membership Value Value where mem := Value.Elem +instance Value.membership : Membership Value Value where mem y x := Value.Elem x y namespace Value def Included (v w : Value) : Prop := ∀ {u}, u ∈ v → u ∈ w @@ -325,23 +329,26 @@ namespace Value instance : Trans Subset Subset Included where trans := instTrans.trans variable {u v w : Value} - def Included.fst (s : Included (u ⊔ v) w) : u ⊆ w := s ∘ .inl - def Included.snd (s : Included (u ⊔ v) w) : v ⊆ w := s ∘ .inr + def Included.fst (s : Included (u ⊔ v) w) : u ⊆ w := fun h => s (Or.inl h) + def Included.snd (s : Included (u ⊔ v) w) : v ⊆ w := fun h => s (Or.inr h) end Value -theorem sub_of_elem (e : u ∈ v) : u ⊑ v := by induction v with cases e -| bot => exact .bot -| fn => rfl -| conj _ _ ih ih' => - all_goals (rename_i h; first | exact (ih h).conjR₁ | exact (ih' h).conjR₂) +theorem sub_of_elem (e : u ∈ v) : u ⊑ v := by + induction v with + | bot => subst e; exact .bot + | fn v w => subst e; exact .refl + | conj v w ih ih' => + rcases e with h | h + · exact .conjR₁ (ih h) + · exact .conjR₂ (ih' h) theorem sub_of_included (s : u ⊆ v) : u ⊑ v := by induction u with | bot => exact .bot | fn => apply sub_of_elem; apply s; rfl | conj _ _ ih ih' => apply Sub.conjL - · apply ih; intro _ e; apply s; left; exact e - · apply ih'; intro _ e; apply s; right; exact e + · apply ih; intro _ e; apply s; exact Or.inl e + · apply ih'; intro _ e; apply s; exact Or.inr e theorem conj_included_inv {u v w : Value} (s : u ⊔ v ⊆ w) : u ⊆ w ∧ v ⊆ w := by constructor <;> (intro _ _; apply s; first | left; trivial | right; trivial) @@ -356,19 +363,19 @@ inductive IsFn (u : Value) : Prop where | isFn (h : u = v ⇾ w) def AllFn (v : Value) : Prop := ∀ {u}, u ∈ v → IsFn u namespace AllFn - def fst (f : AllFn (u ⊔ v)) : AllFn u := f ∘ .inl - def snd (f : AllFn (u ⊔ v)) : AllFn v := f ∘ .inr + def fst (f : AllFn (u ⊔ v)) : AllFn u := fun h => f (Or.inl h) + def snd (f : AllFn (u ⊔ v)) : AllFn v := fun h => f (Or.inr h) end AllFn lemma not_isFn_bot : ¬ IsFn ⊥ := nofun lemma elem_of_allFn (f : AllFn u) : ∃ v w, v ⇾ w ∈ u := by induction u with -| bot => exact (not_isFn_bot <| f rfl).elim +| bot => exact (not_isFn_bot <| f (u := ⊥) rfl).elim | fn v w => exists v, w | conj v w ih _ => -- In fact, the proof is also possible on the `.snd` side. -- There is some information loss in this step. - have ⟨v, w, i⟩ := ih f.fst; exists v, w; left; exact i + have ⟨v, w, i⟩ := ih f.fst; exists v, w; exact Or.inl i -- https://plfa.github.io/Denotational/#domains-and-codomains /-- Given a set `u` of functions, `u.conjDom` returns the join of their domains. -/ @@ -386,22 +393,29 @@ def Value.conjCodom : Value → Value /-- Given an element `v ⇾ w` of a set of functions `u`, we know that `v` is in `u.conjDom`. -/ theorem included_conjDom (f : AllFn u) (i : v ⇾ w ∈ u) : v ⊆ u.conjDom := by induction u with | bot => cases i -| fn => cases i; exact id -| conj u u' ih ih' => match i with - | .inl h => calc v - _ ⊆ u.conjDom := ih f.fst h - _ ⊆ (u ⊔ u').conjDom := .inl - | .inr h => calc v - _ ⊆ u'.conjDom := ih' f.snd h - _ ⊆ (u ⊔ u').conjDom := .inr +| fn => cases i; intro _ hx; exact hx +| conj u u' ih ih' => + rcases i with h | h + · calc v + _ ⊆ u.conjDom := ih f.fst h + _ ⊆ (u ⊔ u').conjDom := fun h => Or.inl h + · calc v + _ ⊆ u'.conjDom := ih' f.snd h + _ ⊆ (u ⊔ u').conjDom := fun h => Or.inr h /-- Given a set `u` of identical terms `v ⇾ w`, we know that `u.conjCodom` is included in `w`. -/ theorem conjCodom_included (s : u ⊆ v ⇾ w) : u.conjCodom ⊆ w := by induction u with -| bot => cases s rfl -| fn => cases s rfl; exact id -| conj _ _ ih ih' => intro x; intro - | .inl i => exact ih s.fst i - | .inr i => exact ih' s.snd i +| bot => + have h := s (u := ⊥) rfl + cases h +| fn u₁ u₂ => + have h := s (u := u₁ ⇾ u₂) rfl + cases h; intro _ hx; exact hx +| conj _ _ ih ih' => + intro x h + rcases h with i | i + · exact ih s.fst i + · exact ih' s.snd i /-- We say that `v ⇾ w` factors `u` into `u`, if: @@ -420,13 +434,20 @@ def Factor (u u' v w : Value) : Prop := theorem sub_inv (lt : u ⊑ u') {v w} (i : v ⇾ w ∈ u) : ∃ u'', Factor u' u'' v w := by induction lt generalizing v w with | bot => cases i - | conjL _ _ ih ih' => exact i.elim ih ih' - | conjR₁ _ ih => have ⟨u'', f, s, ss⟩ := ih i; exists u'', f, .inl ∘ s - | conjR₂ _ ih => have ⟨u'', f, s, ss⟩ := ih i; exists u'', f, .inr ∘ s - | fn lt lt' => cases i; rename_i v v' w' w _ _; exists v ⇾ w, .isFn, id + | conjL _ _ ih ih' => + rcases i with h | h + · exact ih h + · exact ih' h + | conjR₁ _ ih => have ⟨u'', f, s, ss⟩ := ih i; exists u'', f, fun h => Or.inl (s h) + | conjR₂ _ ih => have ⟨u'', f, s, ss⟩ := ih i; exists u'', f, fun h => Or.inr (s h) + | fn lt lt' => cases i; rename_i v v' w' w _ _; exists v ⇾ w, (fun h => IsFn.isFn h), id | dist => cases i; rename_i v w w'; exists v ⇾ w ⊔ v ⇾ w' - refine ⟨(Or.elim · .isFn .isFn), id, ?_, .refl⟩; exact .conjL .refl .refl + refine ⟨?_, id, ?_, .refl⟩ + · intro _ h; rcases h with h' | h' + · exact .isFn h' + · exact .isFn h' + · exact .conjL .refl .refl | trans _ _ ih ih' => rename_i u' v' w'; have ⟨u'', f, s, ss⟩ := ih i; have ⟨u'', f, s, ss'⟩ := trans f s ih' exists u'', f, s; exact ⟨ss'.1.trans ss.1, ss.2.trans ss'.2⟩ @@ -435,13 +456,19 @@ theorem sub_inv (lt : u ⊑ u') {v w} (i : v ⇾ w ∈ u) : ∃ u'', Factor u' u trans {u u₁ u₂} (f : AllFn u₁) (s : u₁ ⊆ u) (ih : ∀ {v w}, v ⇾ w ∈ u → ∃ u₃, Factor u₂ u₃ v w) : ∃ u₃, Factor u₂ u₃ u₁.conjDom u₁.conjCodom := by induction u₁ with - | bot => exfalso; apply not_isFn_bot; exact f rfl + | bot => exfalso; apply not_isFn_bot; exact f (u := ⊥) rfl | fn => apply ih; apply fn_elem; exact s | conj _ _ ih ih' => have ⟨s, s'⟩ := conj_included_inv s have ⟨u₃, f₃, s, ss⟩ := ih f.fst s; have ⟨u₃', f₃', s', ss'⟩ := ih' f.snd s' - exists u₃ ⊔ u₃', (Or.elim · f₃ f₃'), (Or.elim · s s') - exact ⟨conj_sub_conj ss.1 ss'.1, conj_sub_conj ss.2 ss'.2⟩ + exists u₃ ⊔ u₃' + refine ⟨?_, ?_, conj_sub_conj ss.1 ss'.1, conj_sub_conj ss.2 ss'.2⟩ + · intro _ h; rcases h with h' | h' + · exact f₃ h' + · exact f₃' h' + · intro _ h; rcases h with h' | h' + · exact s h' + · exact s' h' lemma sub_inv_fn (lt : v ⇾ w ⊑ u) : ∃ u', diff --git a/Plfl/Untyped/Denotational/Adequacy.lean b/Plfl/Untyped/Denotational/Adequacy.lean index 3a63132..d50d9bc 100644 --- a/Plfl/Untyped/Denotational/Adequacy.lean +++ b/Plfl/Untyped/Denotational/Adequacy.lean @@ -66,7 +66,7 @@ mutual - `c`'s body evaluates according to `v`. -/ def 𝕍 : Value → Clos → Prop - | _, .clos (` _) _ => ⊥ + | _, .clos (‵ _) _ => ⊥ | _, .clos (_ □ _) _ => ⊥ | ⊥, .clos (ƛ _) _ => ⊤ | vw@(v ⇾ w), .clos (ƛ n) γ => @@ -113,7 +113,7 @@ lemma 𝕍.of_not_gtFn (nf : ¬ GtFn v) : 𝕍 v (.clos (ƛ n) γ') := by induct lemma 𝕍.sub {v v'} (vvc : 𝕍 v c) (lt : v' ⊑ v) : 𝕍 v' c := by let .clos m γ := c; cases m with (try simp [𝕍] at *; try contradiction) | lam m => rename_i Γ; induction lt generalizing Γ with - | bot => trivial + | bot => unfold 𝕍; trivial | conjL _ _ ih ih' => unfold 𝕍; exact ⟨ih _ _ _ vvc, ih' _ _ _ vvc⟩ | conjR₁ _ ih => apply ih; unfold 𝕍 at vvc; exact vvc.1 | conjR₂ _ ih => apply ih; unfold 𝕍 at vvc; exact vvc.2 @@ -150,8 +150,11 @@ theorem 𝔼.of_eval {Γ} {γ : Env Γ} {γ' : ClosEnv Γ} {m : Γ ⊢ ✶} (g : generalize hx : v = x at * induction d generalizing v with (unfold 𝔼; intro gt) | @var _ γ i => - unfold 𝔾 𝔼 at g; have := @g i; split at this - have ⟨c, em', vγi⟩ := this gt; refine ⟨c, ?_, vγi⟩; apply em'.var; trivial + unfold 𝔾 𝔼 at g; have := @g i + generalize h_clos : γ' i = ci at this + cases ci with | clos m' δ' => + have ⟨c, em', vγi⟩ := this gt; refine ⟨c, ?_, vγi⟩ + exact BigStep.Eval.var h_clos em' | @ap _ _ _ _ _ m _ _ ih ih' => unfold 𝔼 at ih; have ⟨.clos l' δ, e_cl', v_cl'⟩ := ih g rfl ⟨_, _, .refl⟩ have ⟨m', h'⟩ := WHNF.of_𝕍 v_cl'; subst h'; unfold 𝕍 at v_cl' diff --git a/Plfl/Untyped/Denotational/Compositional.lean b/Plfl/Untyped/Denotational/Compositional.lean index cd768a6..1a7420e 100644 --- a/Plfl/Untyped/Denotational/Compositional.lean +++ b/Plfl/Untyped/Denotational/Compositional.lean @@ -77,15 +77,15 @@ theorem ap_equiv : ℰ (l □ m) = (ℰ l ● ℰ m) := by ext; exact ⟨𝒜_ abbrev 𝒱 (i : Γ ∋ ✶) (γ : Env Γ) (v : Value) : Prop := v ⊑ γ i -theorem var_inv (d : ℰ (` i) γ v) : 𝒱 i γ v := by - generalize hx : (` i) = x at * +theorem var_inv (d : ℰ (‵ i) γ v) : 𝒱 i γ v := by + generalize hx : (‵ i) = x at * induction d with try injection hx | var => subst_vars; rfl | bot => exact .bot | conj _ _ ih ih' => exact (ih hx).conjL (ih' hx) | sub _ lt ih => exact lt.trans (ih hx) -theorem var_equiv : ℰ (` i) = 𝒱 i := by ext; exact ⟨var_inv, .sub .var⟩ +theorem var_equiv : ℰ (‵ i) = 𝒱 i := by ext; exact ⟨var_inv, .sub .var⟩ -- https://plfa.github.io/Compositional/#congruence lemma lam_congr (h : ℰ n = ℰ n') : ℰ (ƛ n) = ℰ (ƛ n') := calc _ @@ -141,7 +141,7 @@ theorem compositionality {c : Holed Γ Δ} (h : ℰ m = ℰ n) : ℰ (c.plug m) It is like `ℰ m`, but defined computationally. -/ def ℰ₀ : (Γ ⊢ ✶) → Denot Γ -| ` i => 𝒱 i +| ‵ i => 𝒱 i | ƛ n => ℱ (ℰ₀ n) | l □ m => ℰ₀ l ● ℰ₀ m diff --git a/Plfl/Untyped/Denotational/Soundness.lean b/Plfl/Untyped/Denotational/Soundness.lean index 461c1b7..4035482 100644 --- a/Plfl/Untyped/Denotational/Soundness.lean +++ b/Plfl/Untyped/Denotational/Soundness.lean @@ -47,7 +47,7 @@ section -- https://plfa.github.io/Soundness/#single-substitution-preserves-denotations /-- The result of evaluation is conserved after single substitution. -/ theorem subst₁_pres (dn : γ`‚ v ⊢ n ￬ w) (dm : γ ⊢ m ￬ v) : γ ⊢ n⟦m⟧ ￬ w - := subst_pres (subst₁σ m) (λ | .z => dm | .s _ => .var) dn + := subst_pres (σ := subst₁σ m) (γ := γ`‚ v) (δ := γ) (λ | .z => dm | .s _ => .var) dn -- https://plfa.github.io/Soundness/#reduction-preserves-denotations theorem reduce_pres (d : γ ⊢ m ￬ v) (r : m —→ n) : γ ⊢ n ￬ v := by induction d with @@ -89,13 +89,13 @@ section variable {γ δ : Env Δ} lemma subst_reflect_var {i : Γ ∋ ✶} {σ : Subst Γ Δ} (d : γ ⊢ σ i ￬ v) - : ∃ (δ : Env Γ), (γ `⊢ σ ￬ δ) ∧ (δ ⊢ ` i ￬ v) + : ∃ (δ : Env Γ), (γ `⊢ σ ￬ δ) ∧ (δ ⊢ ‵ i ￬ v) := by exists Env.const i v; unfold Env.const; constructor · intro j; by_cases h : i = j <;> simp only [h] at * · exact d · exact .bot - · convert Eval.var; simp only [Env.const, ite_true] + · convert Eval.var; simp only [ite_true] variable {γ₁ γ₂ : Env Γ} {σ : Subst Γ Δ} diff --git a/Plfl/Untyped/Substitution.lean b/Plfl/Untyped/Substitution.lean index 28af499..2417578 100644 --- a/Plfl/Untyped/Substitution.lean +++ b/Plfl/Untyped/Substitution.lean @@ -14,7 +14,7 @@ abbrev Subst (Γ Δ) := ∀ {a : Ty}, Γ ∋ a → Δ ⊢ a abbrev ids : Subst Γ Γ := .var abbrev shift : Subst Γ (Γ‚ a) := .var ∘ .s -abbrev cons (m : Δ ⊢ a) (σ : Subst Γ Δ) : Subst (Γ‚ a) Δ +@[simp] def cons (m : Δ ⊢ a) (σ : Subst Γ Δ) : Subst (Γ‚ a) Δ | _, .z => m | _, .s x => σ x @@ -35,13 +35,13 @@ section variable {m : Δ ⊢ a} {σ : Subst Γ Δ} {τ : Subst Δ Φ} -- https://plfa.github.io/Substitution/#proofs-of-sub-head-sub-tail-sub-η-z-shift-sub-idl-sub-dist-and-sub-app - @[simp] theorem sub_head : ⟪m ⦂⦂ σ⟫ (`.z) = m := rfl + @[simp] theorem sub_head : ⟪m ⦂⦂ σ⟫ (‵ .z) = m := rfl @[simp] theorem sub_tail : (shift ⨟ m ⦂⦂ σ) = σ (a := b) := rfl - @[simp] theorem sub_η {σ : Subst (Γ‚ a) Δ} : (⟪σ⟫ (`.z) ⦂⦂ (shift ⨟ σ)) = σ (a := b) := by ext i; cases i <;> rfl - @[simp] theorem z_shift : ((`.z) ⦂⦂ shift) = @ids (Γ‚ a) b := by ext i; cases i <;> rfl + @[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_dist : @Eq (Γ‚ a ∋ b → Φ ⊢ b) ((m ⦂⦂ σ) ⨟ τ) ((⟪τ⟫ m) ⦂⦂ (σ ⨟ τ)) := by ext i; cases i <;> rfl + @[simp] theorem sub_dist : @Eq (Γ‚ a ∋ b → Φ ⊢ b) ((m ⦂⦂ σ) ⨟ τ) ((⟪τ⟫ m) ⦂⦂ (σ ⨟ τ)) := by funext i; cases i <;> rfl end -- https://plfa.github.io/Substitution/#interlude-congruences @@ -53,40 +53,44 @@ section variable {m : Γ ⊢ a} {σ : Subst Γ Δ} {ρ : Rename Γ Δ} -- https://plfa.github.io/Substitution/#relating-rename-exts-ext-and-subst-zero-to-the-%CF%83-algebra - @[simp] theorem ren_ext : @Eq (Γ‚ b ∋ c → Δ‚ b ⊢ c) (ren (ext ρ)) (exts (ren ρ)) := by ext i; cases i <;> rfl + @[simp] theorem ren_ext : @Eq (Γ‚ b ∋ c → Δ‚ b ⊢ c) (ren (ext ρ)) (exts (ren ρ)) := by funext i; cases i <;> rfl @[simp] theorem ren_shift : @Eq (Γ ∋ a → Γ‚ b ⊢ a) (ren .s) shift := by congr theorem rename_subst_ren {Γ Δ} {ρ : Rename Γ Δ} {m : Γ ⊢ a} : rename ρ m = ⟪ren ρ⟫ m := by match m with - | ` _ => rfl + | ‵ _ => 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 theorem rename_shift : @Eq (Γ‚ ✶ ⊢ a) (rename .s m) (⟪shift⟫ m) := by simp only [rename_subst_ren]; congr - theorem exts_cons_shift : exts (a := a) (b := b) σ = (`.z ⦂⦂ (σ ⨟ shift)) := by - ext i; cases i <;> simp only [exts, rename_subst_ren, ren_shift]; rfl + theorem exts_cons_shift : exts (a := a) (b := b) σ = (‵ .z ⦂⦂ (σ ⨟ shift)) := by + funext i; cases i <;> simp [exts, seq, cons, rename_shift] - theorem ext_cons_z_shift : @Eq (Γ‚ b ∋ a → Δ‚ b ⊢ a) (ren (ext ρ)) (`.z ⦂⦂ (ren ρ ⨟ shift)) := by - ext i; cases i <;> simp only [ren_ext, exts, rename_subst_ren, ren_shift]; rfl + theorem ext_cons_z_shift : @Eq (Γ‚ b ∋ a → Δ‚ b ⊢ a) (ren (ext ρ)) (‵ .z ⦂⦂ (ren ρ ⨟ shift)) := by + funext i; cases i <;> simp only [ren_ext, exts, rename_subst_ren, ren_shift]; rfl + simp_all only [cons, Function.comp_apply] theorem subst_z_cons_ids {m : Γ ⊢ a} : @Eq (Γ‚ ✶ ∋ a → Γ ⊢ a) (subst₁σ m) (m ⦂⦂ ids) := by - ext i; cases i <;> rfl + funext i; cases i <;> rfl -- https://plfa.github.io/Substitution/#proofs-of-sub-abs-sub-id-and-rename-id - theorem sub_lam {σ : Subst Γ Δ} {n : Γ‚ ✶ ⊢ ✶} : ⟪σ⟫ (ƛ n) = (ƛ ⟪(`.z) ⦂⦂ (σ ⨟ shift)⟫ n) := by + theorem sub_lam {σ : Subst Γ Δ} {n : Γ‚ ✶ ⊢ ✶} : ⟪σ⟫ (ƛ n) = (ƛ ⟪(‵ .z) ⦂⦂ (σ ⨟ shift)⟫ n) := by change (ƛ ⟪exts σ⟫ n) = _; congr; funext _; exact exts_cons_shift @[simp] theorem exts_ids : @Eq (Γ‚ b ∋ a → _) (exts ids) ids := by ext i; cases i <;> rfl theorem sub_ids {Γ} {m : Γ ⊢ a} : ⟪ids (Γ := Γ)⟫ m = m := by match m with - | ` _ => rfl - | ƛ n => apply congr_arg Term.lam; convert sub_ids; exact exts_ids + | ‵ _ => rfl + | ƛ n => apply congr_arg Term.lam; convert sub_ids; + simp_all only + ext x_1 x_2 : 2 + simp_all only [exts_ids] | l □ m => simp only [sub_ap]; apply congr_arg₂ Term.ap <;> exact sub_ids - theorem rename_id : rename (λ {a} x => x) m = m := by + theorem rename_id : rename (λ {_} x => x) m = m := by convert sub_ids; ext; simp only [rename_subst_ren, ren]; congr -- https://plfa.github.io/Substitution/#proof-of-sub-idr @@ -99,12 +103,12 @@ section -- https://plfa.github.io/Substitution/#proof-of-sub-sub @[simp] theorem comp_ext : @Eq (Γ‚ b ∋ a → _) ((ext ρ) ∘ (ext ρ')) (ext (ρ ∘ ρ')) := by - ext i; cases i <;> rfl + funext i; cases i <;> rfl theorem comp_rename {Γ Δ Φ} {m : Γ ⊢ a} {ρ : Rename Δ Φ} {ρ' : Rename Γ Δ} : rename ρ (rename ρ' m) = rename (ρ ∘ ρ') m := by match m with - | ` _ => rfl + | ‵ _ => rfl | ƛ n => apply congr_arg Term.lam; convert comp_rename; exact comp_ext.symm | l □ m => apply congr_arg₂ Term.ap <;> exact comp_rename @@ -113,14 +117,14 @@ section : ⟪exts (b := ✶) σ⟫ (rename ρ m) = rename ρ (⟪σ⟫ m) := by match m with - | ` _ => exact r + | ‵ _ => exact r | l □ m => apply congr_arg₂ Term.ap <;> exact comm_subst_rename r | ƛ n => apply congr_arg Term.lam - let ρ' : ∀ {Γ}, Rename Γ (Γ‚ ✶) := by intro - | [] => intro; intro. - | ✶ :: Γ => intro; exact ext ρ + let ρ' : ∀ {Γ}, Rename Γ (Γ‚ ✶) + | [] => λ i => by cases i + | _ :: _ => ext ρ apply comm_subst_rename (Γ := Γ‚ ✶) (Δ := Δ‚ ✶) (σ := exts σ) (ρ := ρ') (m := n); intro | .z => rfl @@ -137,15 +141,16 @@ section variable {ρ : Rename Γ Δ} {σ : Subst Γ Δ} {τ : Subst Δ Φ} {θ : Subst Φ Ψ} theorem exts_seq_exts : @Eq (Γ‚ ✶ ∋ a → _) (exts σ ⨟ exts τ) (exts (σ ⨟ τ)) := by - ext i; match i with + funext i; match i with | .z => rfl - | .s i => conv_lhs => - change ⟪exts τ⟫ (rename .s (σ i)); rw [comm_subst_rename (σ := τ) (ρ := .s) rfl]; rfl + | .s i => + change ⟪exts τ⟫ (rename .s (σ i)) = rename .s (⟪τ⟫ (σ i)) + exact comm_subst_rename (m := σ i) (ρ := .s) (λ {x} => rfl) theorem sub_sub {Γ Δ Φ} {σ : Subst Γ Δ} {τ : Subst Δ Φ} {m : Γ ⊢ a} : ⟪τ⟫ (⟪σ⟫ m) = ⟪σ ⨟ τ⟫ m := by match m with - | ` _ => rfl + | ‵ _ => rfl | l □ m => apply congr_arg₂ Term.ap <;> exact sub_sub | ƛ n => calc ⟪τ⟫ (⟪σ⟫ (ƛ n)) _ = (ƛ ⟪exts τ⟫ (⟪exts σ⟫ n)) := rfl @@ -157,13 +162,16 @@ section -- https://plfa.github.io/Substitution/#proof-of-sub-assoc theorem sub_assoc : @Eq (Γ ∋ a → _) ((σ ⨟ τ) ⨟ θ) (σ ⨟ (τ ⨟ θ)) := by - ext; simp only [Function.comp_apply, sub_sub] + funext i; simp only [Function.comp_apply, sub_sub] -- https://plfa.github.io/Substitution/#proof-of-subst-zero-exts-cons theorem subst₁σ_exts_cons {m : Δ ⊢ b} : @Eq (Γ‚ ✶ ∋ a → _) (exts σ ⨟ subst₁σ m) (m ⦂⦂ σ) := by - simp only [ - exts_cons_shift, subst_z_cons_ids, sub_dist, sub_head, sub_assoc, sub_tail, seq_ids - ] + funext i; cases i + · rfl + · rename_i x + change ⟪fun {a} => subst₁σ m⟫ (exts (fun {a} => σ) (.s x)) = σ x + simp only [exts, Subst.shift, rename_subst] + convert sub_ids (m := σ x) using 2 variable {n : Γ‚ ✶ ⊢ ✶} {m : Γ ⊢ ✶} @@ -172,8 +180,8 @@ section _ = ⟪subst₁σ (⟪σ⟫ m)⟫ (⟪exts σ⟫ n) := rfl _ = ⟪⟪σ⟫ m ⦂⦂ ids⟫ (⟪exts σ⟫ n) := by congr; simp only [subst_z_cons_ids] _ = ⟪(exts σ) ⨟ ((⟪σ⟫ m) ⦂⦂ ids)⟫ n := sub_sub - _ = ⟪(`.z ⦂⦂ (σ ⨟ shift)) ⨟ (⟪σ⟫ m ⦂⦂ ids)⟫ n := by congr; simp only [exts_cons_shift] - _ = ⟪⟪⟪σ⟫ m ⦂⦂ ids⟫ (`.z) ⦂⦂ ((σ ⨟ shift) ⨟ (⟪σ⟫ m ⦂⦂ ids))⟫ n := by congr; simp only [sub_dist] + _ = ⟪(‵ .z ⦂⦂ (σ ⨟ shift)) ⨟ (⟪σ⟫ m ⦂⦂ ids)⟫ n := by congr; simp only [exts_cons_shift] + _ = ⟪⟪⟪σ⟫ m ⦂⦂ ids⟫ (‵ .z) ⦂⦂ ((σ ⨟ shift) ⨟ (⟪σ⟫ m ⦂⦂ ids))⟫ n := by congr; simp only [sub_dist] _ = ⟪⟪σ⟫ m ⦂⦂ ((σ ⨟ shift) ⨟ (⟪σ⟫ m ⦂⦂ ids))⟫ n := rfl _ = ⟪⟪σ⟫ m ⦂⦂ (σ ⨟ shift ⨟ ⟪σ⟫ m ⦂⦂ ids)⟫ n := by congr; simp only [sub_assoc] _ = ⟪⟪σ⟫ m ⦂⦂ (σ ⨟ ids)⟫ n := by congr diff --git a/lake-manifest.json b/lake-manifest.json index 05c00e2..2abc8b3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,68 +1,96 @@ -{"version": 7, +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4", + [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "rev": "f58165d3d6e0b048d89e56944e98d9054b223d9b", - "name": "std", + "scope": "leanprover-community", + "rev": "de0f6427233fc146b04b7a5faa4f303cae41149f", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "293af9b2a383eed4d04d66b898d608d0a44b750f", + "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/quote4", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, - "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", - "name": "Qq", + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", - "name": "aesop", + "scope": "leanprover-community", + "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef", + "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", + "scope": "leanprover-community", + "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", + "inputRev": "v0.0.98", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", - "name": "Cli", + "scope": "leanprover-community", + "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.30.0-rc2", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", - "name": "importGraph", + "scope": "leanprover-community", + "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4ee56e687ce2b9b51b097bfa65947a499da0c453", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "afdc7729cafc1ca476165b2ade89d4150bcb1dd2", - "name": "mathlib", + "scope": "leanprover", + "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}], + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "plfl", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.lean b/lakefile.lean deleted file mode 100644 index b57a3c1..0000000 --- a/lakefile.lean +++ /dev/null @@ -1,19 +0,0 @@ -import Lake -open Lake DSL - -package plfl { - leanOptions := #[⟨`relaxedAutoImplicit, false⟩] -} - -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" - -@[default_target] -lean_lib Plfl { - -- add library configuration options here -} - --- @[default_target] --- lean_exe plfl { --- root := `Main --- } diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..d666fd3 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,31 @@ +name = "plfl" +defaultTargets = ["Plfl"] + +[leanOptions] +# pp.unicode.fun = true # pretty-prints `fun a ↦ b` +# autoImplicit = false # no "assume a typo is a new variable" +relaxedAutoImplicit = false # no "assume a typo is a new variable" +maxSynthPendingDepth = 3 # same as mathlib, changes behaviour of typeclass inference +# weak.linter.flexible = true # no rigid tactic (e.g. `exact`) after a flexible tactic (e.g. `simp`) +# Enable all mathlib linters: automatically matches what mathlib uses. +# weak.linter.mathlibStandardSet = true +# Switch off warnings generated by `sorry` +# warn.sorry = false + +[[require]] +name = "mathlib" +scope = "leanprover-community" +# git = "https://github.com/leanprover-community/mathlib4.git" + +[[require]] +name = "aesop" +scope = "leanprover-community" +# git = "https://github.com/JLimperg/aesop" + +[[lean_lib]] +name = "Plfl" + +# [[lean_exe]] +# name = "plfl" +# root = "Main" +# defaultTarget = true diff --git a/lean-toolchain b/lean-toolchain index 9ad3040..6c7e31f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.30.0-rc2 From 486fb8fbc9adf123795b668522aaa8dbdb8f79f5 Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Sat, 23 May 2026 15:13:34 +0700 Subject: [PATCH 2/8] feat: use modules --- Plfl.lean | 39 ++--- Plfl/DeBruijn.lean | 37 ++-- Plfl/Init.lean | 8 +- Plfl/Lambda.lean | 7 +- Plfl/Lambda/Properties.lean | 18 +- Plfl/More.lean | 81 +++++++-- Plfl/More/Bisimulation.lean | 96 ++++------- Plfl/More/DoubleSubst.lean | 8 +- Plfl/More/Inference.lean | 68 ++++++-- Plfl/Untyped.lean | 163 ++++++++++++++++-- Plfl/Untyped/BigStep.lean | 10 +- Plfl/Untyped/Confluence.lean | 44 +++-- Plfl/Untyped/Denotational.lean | 10 +- Plfl/Untyped/Denotational/Adequacy.lean | 10 +- Plfl/Untyped/Denotational/Compositional.lean | 8 +- .../Denotational/ContextualEquivalence.lean | 8 +- Plfl/Untyped/Denotational/Soundness.lean | 8 +- Plfl/Untyped/Substitution.lean | 8 +- 18 files changed, 444 insertions(+), 187 deletions(-) diff --git a/Plfl.lean b/Plfl.lean index d18fae5..0bb1613 100644 --- a/Plfl.lean +++ b/Plfl.lean @@ -1,20 +1,19 @@ --- module --- prelude - -import Plfl.Init -import Plfl.Lambda -import Plfl.Lambda.Properties -import Plfl.DeBruijn -import Plfl.More -import Plfl.More.DoubleSubst -import Plfl.More.Bisimulation -import Plfl.More.Inference -import Plfl.Untyped -import Plfl.Untyped.Substitution -import Plfl.Untyped.Confluence -import Plfl.Untyped.BigStep -import Plfl.Untyped.Denotational -import Plfl.Untyped.Denotational.Compositional -import Plfl.Untyped.Denotational.Soundness -import Plfl.Untyped.Denotational.Adequacy -import Plfl.Untyped.Denotational.ContextualEquivalence +module +prelude +public import Plfl.Init +public import Plfl.Lambda +public import Plfl.Lambda.Properties +public import Plfl.DeBruijn +public import Plfl.More +public import Plfl.More.DoubleSubst +public import Plfl.More.Bisimulation +public import Plfl.More.Inference +public import Plfl.Untyped +public import Plfl.Untyped.Substitution +public import Plfl.Untyped.Confluence +public import Plfl.Untyped.BigStep +public import Plfl.Untyped.Denotational +public import Plfl.Untyped.Denotational.Compositional +public import Plfl.Untyped.Denotational.Soundness +public import Plfl.Untyped.Denotational.Adequacy +public import Plfl.Untyped.Denotational.ContextualEquivalence diff --git a/Plfl/DeBruijn.lean b/Plfl/DeBruijn.lean index 1ac5c5e..309f528 100644 --- a/Plfl/DeBruijn.lean +++ b/Plfl/DeBruijn.lean @@ -1,6 +1,10 @@ +module + -- https://plfa.github.io/DeBruijn/ -import Plfl.Init +public import Plfl.Init + +@[expose] public section -- Sorry, nothing is inherited from previous chapters here. We have to start over. namespace DeBruijn @@ -42,12 +46,12 @@ namespace Lookup infix:40 " ∋ " => Lookup -- https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/d6a227a63c55bf13d49d443f47c54c7a500ea27b/md/main/macros.md#simplifying-macro-declaration - syntax "get_elem" (ppSpace term) : tactic - macro_rules | `(tactic| get_elem $n) => match n.1.toNat with - | 0 => `(tactic | exact Lookup.z) - | n+1 => `(tactic| apply Lookup.s; get_elem $(Lean.quote n)) + syntax "get_elem" (ppSpace term) : term + macro_rules | `(term| get_elem $n) => match n.1.toNat with + | 0 => `(term| Lookup.z) + | n+1 => `(term| Lookup.s (get_elem $(Lean.quote n))) - macro "♯ " n:term:90 : term => `(by get_elem $n) + macro "♯ " n:term:90 : term => `(get_elem $n) example : ∅‚ ℕt =⇒ ℕt‚ ℕt ∋ ℕt := .z example : ∅‚ ℕt =⇒ ℕt‚ ℕt ∋ ℕt := ♯0 @@ -357,7 +361,7 @@ def eval (gas : ℕ) (l : ∅ ⊢ a) : Steps l := match progress l with | .done v => .steps .nil <| .done v | .step r => - let ⟨rs, res⟩ := eval (gas - 1) (by trivial) + let ⟨rs, res⟩ := eval (gas - 1) _ ⟨.cons r rs, res⟩ section examples @@ -366,7 +370,20 @@ section examples -- def x : ℕ := x + 1 abbrev succμ : ∅ ⊢ ℕt := μ ι #0 - #eval eval 3 succμ |> (·.3) - #eval eval 100 (add □ 2 □ 2) |> (·.3) - #eval eval 100 (mul □ 2 □ 3) |> (·.3) + /-- +info: DeBruijn.Result.dnf +-/ +#guard_msgs in #eval eval 3 succμ |> (·.3) + /-- +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) + /-- +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) end examples diff --git a/Plfl/Init.lean b/Plfl/Init.lean index 8a92b4a..d3c90fa 100644 --- a/Plfl/Init.lean +++ b/Plfl/Init.lean @@ -1,8 +1,8 @@ --- module +module -import Mathlib.Logic.Function.Basic -import Mathlib.Logic.Relator -import Mathlib.Tactic +public import Mathlib.Tactic + +@[expose] public section /-- `is_empty` converts `IsEmpty α` to `α → False`. diff --git a/Plfl/Lambda.lean b/Plfl/Lambda.lean index 8844391..2f8abc8 100644 --- a/Plfl/Lambda.lean +++ b/Plfl/Lambda.lean @@ -1,7 +1,10 @@ --- module +module + -- https://plfa.github.io/Lambda/ -import Plfl.Init +public import Plfl.Init + +@[expose] public section namespace Lambda diff --git a/Plfl/Lambda/Properties.lean b/Plfl/Lambda/Properties.lean index d148aae..9785dda 100644 --- a/Plfl/Lambda/Properties.lean +++ b/Plfl/Lambda/Properties.lean @@ -1,8 +1,13 @@ +module + -- https://plfa.github.io/Properties/ -import Plfl.Init +public meta import Plfl.Init +public meta import Plfl.Lambda import Plfl.Lambda +@[expose] public section + open Lambda namespace Properties @@ -323,7 +328,10 @@ section examples abbrev tySuccμ : ∅ ⊢ succμ ⦂ ℕt := by apply tyMu; apply tySucc; trivial - #eval eval 3 tySuccμ |>.3 + /-- + info: Properties.Result.dnf + -/ + #guard_msgs in #eval eval 3 tySuccμ |>.3 abbrev add_2_2 := add □ 2 □ 2 @@ -340,7 +348,11 @@ section examples · iterate 2 (apply tySucc) · exact tyZero - #eval eval 100 tyAdd_2_2 |>.3 + /-- + info: Properties.Result.done + (Lambda.Value.succ (Lambda.Value.succ (Lambda.Value.succ (Lambda.Value.succ (Lambda.Value.zero))))) + -/ + #guard_msgs in #eval eval 100 tyAdd_2_2 |>.3 end examples section subject_expansion diff --git a/Plfl/More.lean b/Plfl/More.lean index 4892654..8a6a169 100644 --- a/Plfl/More.lean +++ b/Plfl/More.lean @@ -1,6 +1,10 @@ +module + -- https://plfa.github.io/More/ -import Plfl.Init +public import Plfl.Init + +@[expose] public section -- This module was extended from the original one for . namespace More @@ -583,7 +587,7 @@ def eval (gas : ℕ) (l : ∅ ⊢ a) : Steps l := match progress l with | .done v => .steps .refl <| .done v | .step r => - let ⟨rs, res⟩ := eval (gas - 1) (by trivial) + let ⟨rs, res⟩ := eval (gas - 1) _ ⟨Trans.trans r rs, res⟩ section examples @@ -594,22 +598,63 @@ section examples abbrev evalRes (l : ∅ ⊢ a) (gas := 100) := (eval gas l).3 - #eval evalRes (gas := 3) succμ - #eval evalRes <| add □ 2 □ 1 - #eval evalRes <| mul □ 2 □ 2 + /-- +info: More.Result.dnf +-/ +#guard_msgs in #eval evalRes (gas := 3) succμ + /-- +info: More.Result.done (More.Value.succ (More.Value.succ (More.Value.succ (More.Value.zero)))) +-/ +#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 -- Prim - #eval evalRes <| .prim 2 ⋄ .prim 3 - -- Let - #eval evalRes <| .let (.prim 6) (#0 ⋄ .prim 7) - #eval evalRes <| .let (.prim 3) <| .let (.prim 4) (.prod (#1) (#0)) - -- Prod, Unit - #eval evalRes <| .fst <| .snd <| .prod ◯ (.prod (.prim 6) (ι ι 0)) - -- Sum - #eval evalRes <| (.left (.prim 3) : ∅ ⊢ ℕp + ℕt) - #eval evalRes <| (.right 4 : ∅ ⊢ ℕp + ℕt) - #eval evalRes <| .caseSum (.right 1 : ∅ ⊢ ℕp + ℕt) 𝟘 (.succ (#0)) + /-- +info: More.Result.done (More.Value.prim 6) +-/ +#guard_msgs in #eval evalRes <| .prim 2 ⋄ .prim 3 +-- Let +/-- +info: More.Result.done (More.Value.prim 42) +-/ +#guard_msgs in #eval evalRes <| .let (.prim 6) (#0 ⋄ .prim 7) +/-- +info: More.Result.done (More.Value.prod (More.Value.prim 3) (More.Value.prim 4)) +-/ +#guard_msgs in #eval evalRes <| .let (.prim 3) <| .let (.prim 4) (.prod (#1) (#0)) +-- Prod, Unit +/-- +info: More.Result.done (More.Value.prim 6) +-/ +#guard_msgs in #eval evalRes <| .fst <| .snd <| .prod ◯ (.prod (.prim 6) (ι ι 0)) +-- Sum +/-- +info: More.Result.done (More.Value.left (More.Value.prim 3)) +-/ +#guard_msgs in #eval evalRes <| (.left (.prim 3) : ∅ ⊢ ℕp + ℕt) +/-- +info: More.Result.done + (More.Value.right (More.Value.succ (More.Value.succ (More.Value.succ (More.Value.succ (More.Value.zero)))))) +-/ +#guard_msgs in #eval evalRes <| (.right 4 : ∅ ⊢ ℕp + ℕt) +/-- +info: More.Result.done (More.Value.succ (More.Value.succ (More.Value.zero))) +-/ +#guard_msgs in #eval evalRes <| .caseSum (.right 1 : ∅ ⊢ ℕp + ℕt) 𝟘 (.succ (#0)) -- List - #eval evalRes <| .nil (a := ℕt) - #eval evalRes <| .cons (ι 𝟘) <| .cons 𝟘 .nil - #eval evalRes <| .caseList (.cons (ι 𝟘) <| .cons 𝟘 .nil) 𝟘 (#1 /- 0:cdr, 1:car -/) + /-- +info: More.Result.done (More.Value.nil) +-/ +#guard_msgs in #eval evalRes <| .nil (a := ℕt) + /-- +info: More.Result.done + (More.Value.cons (More.Value.succ (More.Value.zero)) (More.Value.cons (More.Value.zero) (More.Value.nil))) +-/ +#guard_msgs in #eval evalRes <| .cons (ι 𝟘) <| .cons 𝟘 .nil + /-- +info: More.Result.done (More.Value.succ (More.Value.zero)) +-/ +#guard_msgs in #eval evalRes <| .caseList (.cons (ι 𝟘) <| .cons 𝟘 .nil) 𝟘 (#1 /- 0:cdr, 1:car -/) end examples diff --git a/Plfl/More/Bisimulation.lean b/Plfl/More/Bisimulation.lean index 40c401d..88d3cd6 100644 --- a/Plfl/More/Bisimulation.lean +++ b/Plfl/More/Bisimulation.lean @@ -1,7 +1,11 @@ +module + -- https://plfa.github.io/Bisimulation/ -import Plfl.Init -import Plfl.More +public import Plfl.Init +public import Plfl.More + +@[expose] public section open More open Subst Notation @@ -62,13 +66,10 @@ namespace Sim -- https://plfa.github.io/Bisimulation/#simulation-commutes-with-renaming def comm_rename (ρ : ∀ {a}, Γ ∋ a → Δ ∋ a) {m m' : Γ ⊢ a} : m ~ m' → rename ρ m ~ rename ρ m' - := by intro - | .var => exact .var - | .lam s => apply lam; exact comm_rename (ext ρ) s - | .ap sl sm => apply ap; repeat (apply comm_rename ρ; trivial) - | .let sl sm => apply «let»; repeat - first | apply comm_rename ρ | apply comm_rename (ext ρ) - trivial + | .var => .var + | .lam s => .lam (comm_rename (ext ρ) s) + | .ap sl sm => .ap (comm_rename ρ sl) (comm_rename ρ sm) + | .let sl sm => .let (comm_rename ρ sl) (comm_rename (ext ρ) sm) -- https://plfa.github.io/Bisimulation/#simulation-commutes-with-substitution def comm_exts {σ σ' : ∀ {a}, Γ ∋ a → Δ ⊢ a} @@ -82,13 +83,10 @@ namespace Sim (gs : ∀ {a}, (x : Γ ∋ a) → @σ a x ~ @σ' a x) {m m' : Γ ⊢ a} : m ~ m' → subst σ m ~ subst σ' m' - := by intro - | .var => apply gs - | .lam s => apply lam; exact comm_subst (comm_exts gs) s - | .ap sl sm => apply ap; repeat (apply comm_subst gs; trivial) - | .let sm sn => apply «let»; repeat - first | apply comm_subst gs | apply comm_subst (comm_exts gs) - trivial + | @Sim.var _ _ x => gs x + | .lam s => .lam (comm_subst (comm_exts gs) s) + | .ap sl sm => .ap (comm_subst gs sl) (comm_subst gs sm) + | .let sl sm => .let (comm_subst gs sl) (comm_subst (comm_exts gs) sm) def comm_subst₁ {m m' : Γ ⊢ b} {n n' : Γ‚ b ⊢ a} (sm : m ~ m') (sn : n ~ n') : n⟦m⟧ ~ n'⟦m'⟧ @@ -123,30 +121,15 @@ m' - —→ - n' inductive Leg (m' n : Γ ⊢ a) : Prop where | intro (sim : n ~ n') (red : m' —→ n') -def Leg.fromLegInv {m m' n : Γ ⊢ a} (s : m ~ m') (r : m —→ n) : Leg m' n := by - match s with - | .ap sl sm => match r with - | .lamβ v => cases sl with | lam sl => - constructor - · apply comm_subst₁ <;> trivial - · apply lamβ; exact commValue sm v - | .apξ₁ r => - have ⟨s', r'⟩ := fromLegInv sl r; constructor - · apply ap <;> trivial - · apply apξ₁ r' - | .apξ₂ v r => - have ⟨s', r'⟩ := fromLegInv sm r; constructor - · apply ap <;> trivial - · refine apξ₂ ?_ r'; exact commValue sl v - | .let sm sn => match r with - | .letξ r => - have ⟨s', r'⟩ := fromLegInv sm r; constructor - · apply «let» <;> trivial - · apply letξ; exact r' - | .letβ v => - constructor - · apply comm_subst₁ <;> trivial - · apply letβ; exact commValue sm v +def Leg.fromLegInv {m m' n : Γ ⊢ a} : (m ~ m') → (m —→ n) → Leg m' n + | .ap (.lam sl) sm, .lamβ v => .intro (comm_subst₁ sm sl) (.lamβ (commValue sm v)) + | .ap sl sm, .apξ₁ r => + let ⟨s', r'⟩ := fromLegInv sl r; .intro (.ap s' sm) (.apξ₁ r') + | .ap sl sm, .apξ₂ v r => + let ⟨s', r'⟩ := fromLegInv sm r; .intro (.ap sl s') (.apξ₂ (commValue sl v) r') + | .let sm sn, .letξ r => + let ⟨s', r'⟩ := fromLegInv sm r; .intro (.let s' sn) (.letξ r') + | .let sm sn, .letβ v => .intro (comm_subst₁ sm sn) (.letβ (commValue sm v)) -- https://plfa.github.io/Bisimulation/#exercise-sim¹-practice /-- @@ -162,27 +145,12 @@ m - —→ - n inductive LegInv (m n' : Γ ⊢ a) : Prop where | intro (sim : n ~ n') (red : m —→ n) -def LegInv.fromLeg {m m' n' : Γ ⊢ a} (s : m ~ m') (r : m' —→ n') : LegInv m n' := by - match s with - | .ap sl sm => match r with - | .lamβ v => cases sl with | lam sl => - constructor - · apply comm_subst₁ <;> trivial - · apply lamβ; exact commValue' sm v - | .apξ₁ r => - have ⟨s', r'⟩ := fromLeg sl r; constructor - · apply ap <;> trivial - · apply apξ₁ r' - | .apξ₂ v r => - have ⟨s', r'⟩ := fromLeg sm r; constructor - · apply ap <;> trivial - · refine apξ₂ ?_ r'; exact commValue' sl v - | .let sm sn => match r with - | .letξ r => - have ⟨s', r'⟩ := fromLeg sm r; constructor - · apply «let» <;> trivial - · apply letξ; exact r' - | .letβ v => - constructor - · apply comm_subst₁ <;> trivial - · apply letβ; exact commValue' sm v +def LegInv.fromLeg {m m' n' : Γ ⊢ a} : (m ~ m') → (m' —→ n') → LegInv m n' + | .ap (.lam sl) sm, .lamβ v => .intro (comm_subst₁ sm sl) (.lamβ (commValue' sm v)) + | .ap sl sm, .apξ₁ r => + let ⟨s', r'⟩ := fromLeg sl r; .intro (.ap s' sm) (.apξ₁ r') + | .ap sl sm, .apξ₂ v r => + let ⟨s', r'⟩ := fromLeg sm r; .intro (.ap sl s') (.apξ₂ (commValue' sl v) r') + | .let sm sn, .letξ r => + let ⟨s', r'⟩ := fromLeg sm r; .intro (.let s' sn) (.letξ r') + | .let sm sn, .letβ v => .intro (comm_subst₁ sm sn) (.letβ (commValue' sm v)) diff --git a/Plfl/More/DoubleSubst.lean b/Plfl/More/DoubleSubst.lean index 860b64a..2ca434d 100644 --- a/Plfl/More/DoubleSubst.lean +++ b/Plfl/More/DoubleSubst.lean @@ -1,9 +1,13 @@ +module + -- https://plfa.github.io/More/#exercise-double-subst-stretch -- Adapted from . -import Plfl.Init -import Plfl.More +public import Plfl.Init +public import Plfl.More + +@[expose] public section open More open Term Subst Notation diff --git a/Plfl/More/Inference.lean b/Plfl/More/Inference.lean index 517c1ea..387a2bf 100644 --- a/Plfl/More/Inference.lean +++ b/Plfl/More/Inference.lean @@ -1,7 +1,11 @@ +module + -- https://plfa.github.io/Inference/ -import Plfl.Init -import Plfl.More +public meta import Plfl.Init +public import Plfl.More + +@[expose] public section namespace Inference @@ -180,7 +184,10 @@ end Notation instance : Repr (Γ ∋ m ⦂ a) where reprPrec i n := "♯" ++ reprPrec n (sizeOf i) -#eval @Lookup.z (∅‚ "x" ⦂ ℕt) "x" ℕt +/-- +info: ♯0 +-/ +#guard_msgs in #eval @Lookup.z (∅‚ "x" ⦂ ℕt) "x" ℕt mutual /-- @@ -454,37 +461,70 @@ This won't work either, probably due to similar reasons... -- rw [←not_nonempty_iff]; decide -- Unbound variable: -#eval ((ƛ "x" : ‵"y").the (ℕt =⇒ ℕt)).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval ((ƛ "x" : ‵"y").the (ℕt =⇒ ℕt)).infer ∅ -- Argument in application is ill typed: -#eval (add □ succC).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval (add □ succC).infer ∅ -- Function in application is ill typed: -#eval (add □ succC □ two).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval (add □ succC □ two).infer ∅ -- Function in application has type natural: -#eval (two.the ℕt □ two).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval (two.the ℕt □ two).infer ∅ -- Abstraction inherits type natural: -#eval (twoC.the ℕt).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval (twoC.the ℕt).infer ∅ -- Zero inherits a function type: -#eval (𝟘.the (ℕt =⇒ ℕt)).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval (𝟘.the (ℕt =⇒ ℕt)).infer ∅ -- Successor inherits a function type: -#eval (two.the (ℕt =⇒ ℕt)).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval (two.the (ℕt =⇒ ℕt)).infer ∅ -- Successor of an ill-typed term: -#eval ((ι twoC).the ℕt).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval ((ι twoC).the ℕt).infer ∅ -- Case of a term with a function type: -#eval ((𝟘? twoC.the Ch [zero: 𝟘 |succ "x" : ‵"x"]).the ℕt).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval ((𝟘? twoC.the Ch [zero: 𝟘 |succ "x" : ‵"x"]).the ℕt).infer ∅ -- Case of an ill-typed term: -#eval ((𝟘? twoC.the ℕt [zero: 𝟘 |succ "x" : ‵"x"]).the ℕt).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval ((𝟘? twoC.the ℕt [zero: 𝟘 |succ "x" : ‵"x"]).the ℕt).infer ∅ -- Inherited and synthesized types disagree in a switch: -#eval ((ƛ "x" : ‵"x").the (ℕt =⇒ ℕt =⇒ ℕt)).infer ∅ +/-- +info: .inl _ +-/ +#guard_msgs in #eval ((ƛ "x" : ‵"x").the (ℕt =⇒ ℕt =⇒ ℕt)).infer ∅ -- https://plfa.github.io/Inference/#erasure def Ty.erase : Ty → More.Ty diff --git a/Plfl/Untyped.lean b/Plfl/Untyped.lean index 44af7ec..5d2e818 100644 --- a/Plfl/Untyped.lean +++ b/Plfl/Untyped.lean @@ -1,8 +1,10 @@ --- module +module -- https://plfa.github.io/Untyped/ -import Plfl.Init +public import Plfl.Init + +@[expose] public section namespace Untyped @@ -51,9 +53,9 @@ instance Context.equiv_nat : Context ≃ ℕ where left_inv := left_inv right_inv := by intro; simp only [List.length_replicate] where - left_inv := by intro - | [] => trivial - | (✶) :: ss => calc List.replicate ((✶) :: ss).length (✶) + left_inv : (c : Context) → List.replicate c.length (✶) = c + | [] => rfl + | (✶) :: ss => by calc List.replicate ((✶) :: ss).length (✶) _ = List.replicate (ss.length + 1) (✶) := by rw [List.length_cons] _ = (✶) :: List.replicate ss.length (✶) := by rw [List.replicate_succ] _ = (✶) :: ss := by have := left_inv ss; simp_all only @@ -346,7 +348,7 @@ def eval (gas : ℕ) (l : ∅ ⊢ a) : Steps l := match progress l with | .done v => .steps .refl <| .done v | .step r => - let ⟨rs, res⟩ := eval (gas - 1) (by trivial) + let ⟨rs, res⟩ := eval (gas - 1) _ ⟨Trans.trans r rs, res⟩ namespace Term @@ -403,17 +405,150 @@ section examples abbrev evalRes (l : ∅ ⊢ a) (gas := 100) := (eval gas l).3 -- abbrev evalResStar (l : ∅ ⊢ ✶) (gas := 100) := (eval gas l).3 - #eval evalRes (gas := 3) fourC' - #eval evalRes fourC' + /-- +info: Untyped.Result.dnf +-/ +#guard_msgs in #eval evalRes (gas := 3) fourC' + /-- +info: Untyped.Result.done + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.norm (Untyped.Neutral.var ♯0)))))))))))) +-/ +#guard_msgs in #eval evalRes fourC' - #eval evalRes oneS + /-- +info: Untyped.Result.done + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam (Untyped.Normal.lam (Untyped.Normal.norm (Untyped.Neutral.var ♯0)))))))) +-/ +#guard_msgs in #eval evalRes oneS - #eval evalRes twoS - #eval evalRes twoS'' +/-- +info: Untyped.Result.done + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam (Untyped.Normal.lam (Untyped.Normal.norm (Untyped.Neutral.var ♯0)))))))))))) +-/ +#guard_msgs in #eval evalRes twoS + /-- +info: Untyped.Result.done + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam (Untyped.Normal.lam (Untyped.Normal.norm (Untyped.Neutral.var ♯0)))))))))))) +-/ +#guard_msgs in #eval evalRes twoS'' - #eval evalRes fourS - #eval evalRes fourS' - #eval evalRes fourS'' +/-- +info: Untyped.Result.done + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam (Untyped.Normal.norm (Untyped.Neutral.var ♯0)))))))))))))))))))) +-/ +#guard_msgs in #eval evalRes fourS + /-- +info: Untyped.Result.done + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam (Untyped.Normal.norm (Untyped.Neutral.var ♯0)))))))))))))))))))) +-/ +#guard_msgs in #eval evalRes fourS' + /-- +info: Untyped.Result.done + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam + (Untyped.Normal.norm + (Untyped.Neutral.ap + (Untyped.Neutral.var ♯1) + (Untyped.Normal.lam + (Untyped.Normal.lam (Untyped.Normal.norm (Untyped.Neutral.var ♯0)))))))))))))))))))) +-/ +#guard_msgs in #eval evalRes fourS'' end examples -- https://plfa.github.io/Untyped/#multi-step-reduction-is-transitive diff --git a/Plfl/Untyped/BigStep.lean b/Plfl/Untyped/BigStep.lean index f87d4d6..a373d30 100644 --- a/Plfl/Untyped/BigStep.lean +++ b/Plfl/Untyped/BigStep.lean @@ -1,8 +1,12 @@ +module + -- https://plfa.github.io/BigStep/ -import Plfl.Init -import Plfl.Untyped -import Plfl.Untyped.Substitution +public import Plfl.Init +public import Plfl.Untyped +public import Plfl.Untyped.Substitution + +@[expose] public section namespace BigStep diff --git a/Plfl/Untyped/Confluence.lean b/Plfl/Untyped/Confluence.lean index df77304..d918805 100644 --- a/Plfl/Untyped/Confluence.lean +++ b/Plfl/Untyped/Confluence.lean @@ -1,8 +1,12 @@ +module + -- https://plfa.github.io/Confluence/ -import Plfl.Init -import Plfl.Untyped -import Plfl.Untyped.Substitution +public import Plfl.Init +public import Plfl.Untyped +public import Plfl.Untyped.Substitution + +@[expose] public section namespace Confluence @@ -55,22 +59,24 @@ namespace PReduce instance : Trans (α := Γ ⊢ a) PReduce Clos Clos where trans r c := .head r c -- https://plfa.github.io/Confluence/#equivalence-between-parallel-reduction-and-reduction - def fromReduce {Γ a} {m n : Γ ⊢ a} : m —→ n → (m ⇛ n) := by intro - | .lamβ => refine .lamβ ?rn ?rv <;> rfl - | .lamζ rn => refine .lamζ ?_; exact fromReduce rn - | .apξ₁ rl => refine .apξ ?_ (by rfl); exact fromReduce rl - | .apξ₂ rm => refine .apξ (by rfl) ?_; exact fromReduce rm - - def toReduceClos : (m ⇛ n) → (m —↠ n) := open Untyped.Reduce in by intro - | .var => rfl - | .lamβ rn rv => rename_i n n' v v'; calc (ƛ n) □ v - _ —↠ (ƛ n') □ v := by refine ap_congr₁ (toReduceClos ?_); exact .lamζ rn - _ —↠ (ƛ n') □ v' := ap_congr₂ rv.toReduceClos - _ —→ n'⟦v'⟧ := .lamβ - | .lamζ rn => apply lam_congr; exact rn.toReduceClos - | .apξ rl rm => rename_i l l' m m'; calc l □ m - _ —↠ l' □ m := ap_congr₁ rl.toReduceClos - _ —↠ l' □ m' := ap_congr₂ rm.toReduceClos + def fromReduce {Γ a} {m n : Γ ⊢ a} : m —→ n → (m ⇛ n) + | .lamβ => .lamβ (.refl _) (.refl _) + | .lamζ rn => .lamζ (fromReduce rn) + | .apξ₁ rl => .apξ (fromReduce rl) (.refl _) + | .apξ₂ rm => .apξ (.refl _) (fromReduce rm) + + def 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) + _ —→ 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) end PReduce instance instNonemptyPReduceReduceClos : (m ⇛* n) ≃ (m —↠ n) where diff --git a/Plfl/Untyped/Denotational.lean b/Plfl/Untyped/Denotational.lean index 456140c..e48bc7d 100644 --- a/Plfl/Untyped/Denotational.lean +++ b/Plfl/Untyped/Denotational.lean @@ -1,8 +1,12 @@ +module + -- https://plfa.github.io/Denotational/ -import Plfl.Init -import Plfl.Untyped -import Plfl.Untyped.Substitution +public import Plfl.Init +public import Plfl.Untyped +public import Plfl.Untyped.Substitution + +@[expose] public section namespace Denotational diff --git a/Plfl/Untyped/Denotational/Adequacy.lean b/Plfl/Untyped/Denotational/Adequacy.lean index d50d9bc..4008ca8 100644 --- a/Plfl/Untyped/Denotational/Adequacy.lean +++ b/Plfl/Untyped/Denotational/Adequacy.lean @@ -1,8 +1,12 @@ +module + -- https://plfa.github.io/Adequacy/ -import Plfl.Init -import Plfl.Untyped.BigStep -import Plfl.Untyped.Denotational.Soundness +public import Plfl.Init +public import Plfl.Untyped.BigStep +public import Plfl.Untyped.Denotational.Soundness + +@[expose] public section namespace Adequacy diff --git a/Plfl/Untyped/Denotational/Compositional.lean b/Plfl/Untyped/Denotational/Compositional.lean index 1a7420e..a04f9bd 100644 --- a/Plfl/Untyped/Denotational/Compositional.lean +++ b/Plfl/Untyped/Denotational/Compositional.lean @@ -1,7 +1,11 @@ +module + -- https://plfa.github.io/Compositional/ -import Plfl.Init -import Plfl.Untyped.Denotational +public import Plfl.Init +public import Plfl.Untyped.Denotational + +@[expose] public section namespace Compositional diff --git a/Plfl/Untyped/Denotational/ContextualEquivalence.lean b/Plfl/Untyped/Denotational/ContextualEquivalence.lean index 129e470..4f678a5 100644 --- a/Plfl/Untyped/Denotational/ContextualEquivalence.lean +++ b/Plfl/Untyped/Denotational/ContextualEquivalence.lean @@ -1,7 +1,11 @@ +module + -- https://plfa.github.io/ContextualEquivalence/ -import Plfl.Init -import Plfl.Untyped.Denotational.Adequacy +public import Plfl.Init +public import Plfl.Untyped.Denotational.Adequacy + +@[expose] public section namespace ContextualEquivalence diff --git a/Plfl/Untyped/Denotational/Soundness.lean b/Plfl/Untyped/Denotational/Soundness.lean index 4035482..cf60058 100644 --- a/Plfl/Untyped/Denotational/Soundness.lean +++ b/Plfl/Untyped/Denotational/Soundness.lean @@ -1,7 +1,11 @@ +module + -- https://plfa.github.io/Soundness/ -import Plfl.Init -import Plfl.Untyped.Denotational.Compositional +public import Plfl.Init +public import Plfl.Untyped.Denotational.Compositional + +@[expose] public section namespace Soundness diff --git a/Plfl/Untyped/Substitution.lean b/Plfl/Untyped/Substitution.lean index 2417578..3a1dc94 100644 --- a/Plfl/Untyped/Substitution.lean +++ b/Plfl/Untyped/Substitution.lean @@ -1,7 +1,11 @@ +module + -- https://plfa.github.io/Substitution/#plfa_plfa-part2-Substitution-2341 -import Plfl.Init -import Plfl.Untyped +public import Plfl.Init +public import Plfl.Untyped + +@[expose] public section namespace Substitution From a8b84a80fa1840128303a47dc11d1cbf8fcabbfd Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Sat, 23 May 2026 15:41:20 +0700 Subject: [PATCH 3/8] feat: drop last is now pop --- Plfl/Init.lean | 9 --------- Plfl/Untyped/Denotational.lean | 10 +++++----- 2 files changed, 5 insertions(+), 14 deletions(-) diff --git a/Plfl/Init.lean b/Plfl/Init.lean index d3c90fa..58f27cf 100644 --- a/Plfl/Init.lean +++ b/Plfl/Init.lean @@ -31,12 +31,3 @@ theorem congr_arg₃ (hx : x = x') (hy : y = y') (hz : z = z') : f x y z = f x' y' z' := by subst hx hy hz; rfl - -namespace Vector - def dropLast (v : Vector α n) : Vector α (n - 1) := v.pop - - theorem get_dropLast (v : Vector α (n + 1)) (i : Fin n) - -- : v.dropLast[i] = v[i.val]'(by omega) - : v.dropLast.get i = v.get ⟨i.val, by omega⟩ - := by simp [dropLast, Vector.get, Vector.pop] -end Vector diff --git a/Plfl/Untyped/Denotational.lean b/Plfl/Untyped/Denotational.lean index e48bc7d..4737d94 100644 --- a/Plfl/Untyped/Denotational.lean +++ b/Plfl/Untyped/Denotational.lean @@ -280,7 +280,7 @@ A path consists of `n` edges (`⇾`s) and `n + 1` vertices (`Value`s). -/ def Value.path : (n : ℕ) → Vector Value (n + 1) → Value | 0, _ => ⊥ -| i + 1, vs => path i vs.dropLast ⊔ vs[i] ⇾ vs[i + 1] +| i + 1, vs => path i vs.pop ⊔ vs[i] ⇾ vs[i + 1] /-- Returns the denotation of the nth Church numeral for a given path. @@ -305,12 +305,12 @@ section | succ n r => unfold church.applyN; apply ap · apply sub var; simp only [Env.snoc, Value.path]; convert Sub.refl.conjR₂ - · convert sub_env (@r vs.dropLast) ?_ using 1 - · exact (Vector.get_dropLast vs ⟨n, by omega⟩).symm + · convert sub_env (@r vs.pop) ?_ using 1 + · simp_all only [List.empty_eq, Vector.getElem_pop'] · intro x; cases x with | z => - have : vs.dropLast[0] = vs[0] := by exact Vector.get_dropLast vs ⟨0, by omega⟩ - exact this ▸ Sub.refl + simp_all only [List.empty_eq, Vector.getElem_pop'] + rfl | s i => cases i with | z => exact .conjR₁ .refl From 6a620f09db95ae5d897f669a36a27d0d5dde3b9c Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Sat, 23 May 2026 17:32:32 +0700 Subject: [PATCH 4/8] feat: uncomment BOOM lines --- Plfl/More/Inference.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Plfl/More/Inference.lean b/Plfl/More/Inference.lean index 387a2bf..b6c4dd4 100644 --- a/Plfl/More/Inference.lean +++ b/Plfl/More/Inference.lean @@ -563,7 +563,7 @@ example : fourTy.erase (Γ := ∅) = More.Term.four := by rfl -- https://plfa.github.io/Inference/#exercise-inference-multiplication-recommended example : mul.infer ∅ = .inr ⟨ℕt =⇒ ℕt =⇒ ℕt, mulTy⟩ := by rfl --- ! BOOM! The commented lines below are very CPU/RAM-intensive, and might even make LEAN4 leak memory! --- example : mulTy.erase (Γ := ∅) = More.Term.mul := by rfl --- example : four'Ty.erase (Γ := ∅) = More.Term.four' := by rfl --- example : four''Ty.erase (Γ := ∅) = More.Term.four'' := by rfl +-- ! BOOM! The commented lines below were very CPU/RAM-intensive, and might even make LEAN4 leak memory! +example : mulTy.erase (Γ := ∅) = More.Term.mul := by rfl +example : four'Ty.erase (Γ := ∅) = More.Term.four' := by rfl +example : four''Ty.erase (Γ := ∅) = More.Term.four'' := by rfl From f54e4a5d61c7005ea10f16c83d79c9275a6a6408 Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Sat, 23 May 2026 18:56:22 +0700 Subject: [PATCH 5/8] feat: uncomment another didnt-work-before lines --- Plfl/More/Inference.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Plfl/More/Inference.lean b/Plfl/More/Inference.lean index b6c4dd4..3ead3d4 100644 --- a/Plfl/More/Inference.lean +++ b/Plfl/More/Inference.lean @@ -445,20 +445,20 @@ example : four''.infer ∅ = .inr ⟨ℕt, four''Ty⟩ := by rfl -- https://plfa.github.io/Inference/#testing-the-error-cases /- -Sadly this won't work for now due to limitations with mutual recursions. +This didn't work for before due to limitations with mutual recursions. See: -/ --- example := show ((ƛ "x" : ‵"y").the (ℕt =⇒ ℕt)).infer ∅ = .inl _ by rfl +example := show ((ƛ "x" : ‵"y").the (ℕt =⇒ ℕt)).infer ∅ = .inl _ by rfl /- -This won't work either, probably due to similar reasons... +This didn't work either, probably due to similar reasons... -/ --- instance : Decidable (Nonempty (Σ a, Γ ⊢ m ⇡ a)) := (m.infer Γ).toDecidable +instance : Decidable (Nonempty (Σ a, Γ ⊢ m ⇡ a)) := (m.infer Γ).toDecidable --- example := let m := (ƛ "x" : ‵"y").the (ℕt =⇒ ℕt); show IsEmpty (Σ a, ∅ ⊢ m ⇡ a) by --- rw [←not_nonempty_iff]; decide +example := let m := (ƛ "x" : ‵"y").the (ℕt =⇒ ℕt); show IsEmpty (Σ a, ∅ ⊢ m ⇡ a) by + rw [←not_nonempty_iff]; decide -- Unbound variable: /-- From 955fd3e201d4b4f4ebe39c0937fa64d19db6af85 Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Fri, 29 May 2026 16:50:56 +0700 Subject: [PATCH 6/8] feat: update to v4.30.0 --- lake-manifest.json | 62 +++++++++++++++++++++++----------------------- lakefile.toml | 2 ++ lean-toolchain | 2 +- 3 files changed, 34 insertions(+), 32 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 2abc8b3..4276e5e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,41 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/mathlib4", + [{"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "de0f6427233fc146b04b7a5faa4f303cae41149f", + "rev": "558915ae105bfd8074e22d597613d1961822adc2", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "32dc18cde3684679f3c003de608743b57498c56f", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "293af9b2a383eed4d04d66b898d608d0a44b750f", + "rev": "a456461b368b71d2accd95234832cd9c174b5437", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef", + "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,50 +65,30 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", + "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.98", + "inputRev": "v0.0.99", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", - "inherited": true, - "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", + "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "4ee56e687ce2b9b51b097bfa65947a499da0c453", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0-rc2", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "plfl", diff --git a/lakefile.toml b/lakefile.toml index d666fd3..c542f7f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -15,11 +15,13 @@ maxSynthPendingDepth = 3 # same as mathlib, changes behaviour of typeclass in [[require]] name = "mathlib" scope = "leanprover-community" +rev = "v4.30.0" # git = "https://github.com/leanprover-community/mathlib4.git" [[require]] name = "aesop" scope = "leanprover-community" +rev = "v4.30.0" # git = "https://github.com/JLimperg/aesop" [[lean_lib]] diff --git a/lean-toolchain b/lean-toolchain index 6c7e31f..af9e5d3 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc2 +leanprover/lean4:v4.30.0 From 685d4dd50690f6c5e0df1e4cc1bc0b0086e12ade Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Fri, 29 May 2026 18:17:44 +0700 Subject: [PATCH 7/8] feat: refactor based on review --- Plfl/DeBruijn.lean | 4 +-- Plfl/Lambda.lean | 60 ++++++------------------------- Plfl/Lambda/Properties.lean | 65 ++++++++++++++++------------------ Plfl/More.lean | 29 ++------------- Plfl/More/DoubleSubst.lean | 33 +++++++++++++++-- Plfl/Untyped.lean | 4 +-- Plfl/Untyped/Denotational.lean | 47 +++++++++--------------- Plfl/Untyped/Substitution.lean | 16 +++++---- 8 files changed, 102 insertions(+), 156 deletions(-) diff --git a/Plfl/DeBruijn.lean b/Plfl/DeBruijn.lean index 309f528..a209901 100644 --- a/Plfl/DeBruijn.lean +++ b/Plfl/DeBruijn.lean @@ -360,8 +360,8 @@ def eval (gas : ℕ) (l : ∅ ⊢ a) : Steps l := else match progress l with | .done v => .steps .nil <| .done v - | .step r => - let ⟨rs, res⟩ := eval (gas - 1) _ + | .step (n := n) r => + let ⟨rs, res⟩ := eval (gas - 1) n ⟨.cons r rs, res⟩ section examples diff --git a/Plfl/Lambda.lean b/Plfl/Lambda.lean index 2f8abc8..88878a4 100644 --- a/Plfl/Lambda.lean +++ b/Plfl/Lambda.lean @@ -414,68 +414,28 @@ section examples open Term Context Lookup Context.IsTy -- https://plfa.github.io/Lambda/#non-examples - example : ∅ ⊬ 𝟘 □ 1 := by - by_contra h; unfold NoTy at h; push Not at h - let ⟨tt, ht⟩ := h - cases ht with - | intro ht => - cases ht with - | tyAp hl hr => - cases hl + example : ∅ ⊬ 𝟘 □ 1 := + ⟨fun | .tyAp hl _ => by cases hl⟩ abbrev illLam := ƛ "x" : ‵"x" □ ‵"x" - lemma nty_illLam : ∅ ⊬ illLam := by - by_contra h; unfold NoTy at h; push Not at h - let ⟨tt, ht⟩ := h - cases ht with - | intro ht => - cases ht with - | tyLam ht' => - cases ht' with - | tyAp hl hr => - cases hl with - | tyVar hx => - cases hr with - | tyVar hx' => - have heq := Lookup.functional hx hx' - exact Ty.t_to_t'_ne_t _ _ heq + 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 apply tyAp <;> trivial - example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊬ ‵"x" □ ‵"y" := by - by_contra h; unfold NoTy at h; push Not at h - let ⟨tt, ht⟩ := h - cases ht with - | intro ht => - cases ht with - | tyAp hl hr => - cases hl with - | tyVar hx => - cases hx with - | s hne _ => contradiction + 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 apply tyLam; apply tyAp <;> trivial - example : ∅‚ "x" ⦂ t ⊬ ‵"x" □ ‵"x" := by - by_contra h; unfold NoTy at h; push Not at h - let ⟨tt, ht⟩ := h - cases ht with - | intro ht => - cases ht with - | tyAp hl hr => - cases hl with - | tyVar hl' => - cases hr with - | tyVar hr' => - cases hl' with - | z => - cases hr' with - | s hne _ => contradiction - | s hne _ => contradiction + example : ∅‚ "x" ⦂ t ⊬ ‵"x" □ ‵"x" := + ⟨fun + | .tyAp (.tyVar .z) (.tyVar (.s _ _)) => by contradiction + | .tyAp (.tyVar (.s _ _)) _ => by contradiction⟩ example : ∅‚ "x" ⦂ ℕt =⇒ ℕt‚ "y" ⦂ ℕt =⇒ ℕt diff --git a/Plfl/Lambda/Properties.lean b/Plfl/Lambda/Properties.lean index 9785dda..f9255c1 100644 --- a/Plfl/Lambda/Properties.lean +++ b/Plfl/Lambda/Properties.lean @@ -66,19 +66,13 @@ namespace Canonical lemma wellTyped_right_inv (c : ∅ ⊢ v ⦂ t × Value v) : wellTyped (wellTypedInv c) = c := by - rcases c with ⟨ty, v⟩ - cases v with - | lam => - cases ty with - | tyLam ty => rfl - | zero => - cases ty with - | tyZero => rfl - | succ n => - cases ty with - | tySucc ty => - have ih := @wellTyped_right_inv _ _ ⟨ty, n⟩ - simp only [wellTypedInv, wellTyped, ih] + match c with + | ⟨tyLam ty, Value.lam⟩ => obtain ⟨fst, snd⟩ := c; rfl + | ⟨tyZero, Value.zero⟩ => obtain ⟨fst, snd⟩ := c; rfl + | ⟨tySucc ty, Value.succ n⟩ => + rename_i v'; have := @wellTyped_right_inv v' ℕt ⟨ty, n⟩; + rw [wellTypedInv, wellTyped]; + · simp_all only /-- The Canonical forms are exactly the well-typed values. @@ -210,7 +204,7 @@ namespace Renaming | tyMu j => apply tyMu; exact rename (ext ρ) j def Lookup.weaken : ∅ ∋ m ⦂ t → Γ ∋ m ⦂ t := by - intro h; cases h + nofun def weaken : ∅ ⊢ m ⦂ t → Γ ⊢ m ⦂ t := by intro j; refine rename ?_ j; exact Lookup.weaken @@ -358,37 +352,38 @@ end examples section subject_expansion open Term - abbrev illCase := 𝟘? 𝟘 [zero: 𝟘 |succ "x" : add] - -- https://plfa.github.io/Properties/#exercise-subject_expansion-practice example : IsEmpty (∀ {n t m}, ∅ ⊢ n ⦂ t → (m —→ n) → ∅ ⊢ m ⦂ t) := by - refine ⟨fun f => ?_⟩ + by_contra f + simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff] + let illCase := 𝟘? 𝟘 [zero: 𝟘 |succ "x" : add] have nty_ill : ∅ ⊬ illCase := by - intro tt + intro t refine ⟨fun j => ?_⟩ - cases j with - | tyCase _ jm jn => - cases jm with - | tyZero => - cases jn with - | tyMu jn' => - cases jn' - exact nty_ill.false (f tyZero zeroβ) - - abbrev illAp := (ƛ "x" : 𝟘) □ illLam - - example : IsEmpty (∀ {n t m}, ∅ ⊢ n ⦂ t → (m —→ n) → ∅ ⊢ m ⦂ t) := by - refine ⟨fun f => ?_⟩ + simp only [illCase] at j + cases j; rename_i jz js + cases jz + cases js; rename_i js' + cases js' + have := f 𝟘 ℕt illCase tyZero zeroβ + exact nty_ill.false this.some + +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 have nty_ill : ∅ ⊬ illAp := by intro tt refine ⟨fun j => ?_⟩ - cases j with - | tyAp _ jr => - exact nty_illLam.false jr + simp only [illAp] at j + cases j; rename_i jl jr + exact nty_illLam.false jl -- Use jl instead of jr have h_red : illAp —→ 𝟘 := by + simp only [illAp] apply lamβ exact Value.lam - exact nty_ill.false (f tyZero h_red) + have := f 𝟘 ℕt illAp tyZero h_red -- Pass arguments explicitly + exact nty_ill.false this.some end subject_expansion -- https://plfa.github.io/Properties/#well-typed-terms-dont-get-stuck diff --git a/Plfl/More.lean b/Plfl/More.lean index 8a6a169..82252cd 100644 --- a/Plfl/More.lean +++ b/Plfl/More.lean @@ -140,31 +140,6 @@ inductive Term : Context → Ty → Type where | caseList : Term Γ (.list a) → Term Γ b → Term (Γ‚ a‚ .list a) b → Term Γ b deriving DecidableEq, Repr -@[simp] -def Term.size : Term Γ a → Nat - | .var _ => 1 - | .lam t => t.size + 1 - | .ap l m => l.size + m.size + 1 - | .zero => 1 - | .succ t => t.size + 1 - | .case l m n => l.size + m.size + n.size + 1 - | .mu t => t.size + 1 - | .prim _ => 1 - | .mulP m n => m.size + n.size + 1 - | .let m n => m.size + n.size + 1 - | .prod m n => m.size + n.size + 1 - | .fst t => t.size + 1 - | .snd t => t.size + 1 - | .left t => t.size + 1 - | .right t => t.size + 1 - | .caseSum s l r => s.size + l.size + r.size + 1 - | .caseVoid v => v.size + 1 - | .unit => 1 - | .nil => 1 - | .cons m n => m.size + n.size + 1 - | .caseList l m n => l.size + m.size + n.size + 1 - - namespace Notation open Term @@ -586,8 +561,8 @@ def eval (gas : ℕ) (l : ∅ ⊢ a) : Steps l := else match progress l with | .done v => .steps .refl <| .done v - | .step r => - let ⟨rs, res⟩ := eval (gas - 1) _ + | .step (n := n) r => + let ⟨rs, res⟩ := eval (gas - 1) n ⟨Trans.trans r rs, res⟩ section examples diff --git a/Plfl/More/DoubleSubst.lean b/Plfl/More/DoubleSubst.lean index 2ca434d..db6fcad 100644 --- a/Plfl/More/DoubleSubst.lean +++ b/Plfl/More/DoubleSubst.lean @@ -149,6 +149,35 @@ lemma insert_twice_idx {Γ Δ Φ : Context} {a b c : Ty} (i : Γ‚‚ Δ‚‚ | _ :: _, .z => rfl | d :: Φ, .s i => apply congr_arg Lookup.s; exact insert_twice_idx i +/-- +Custom size function for `Term` that only counts AST nodes, ignoring the sizes of `Context` and `Ty` indices. + +Lean's default `sizeOf` includes index sizes, causing termination proofs to fail when the context grows. +-/ +@[simp] +private def More.Term.astSize : Term Γ a → Nat + | .var _ => 1 + | .lam t => t.astSize + 1 + | .ap l m => l.astSize + m.astSize + 1 + | .zero => 1 + | .succ t => t.astSize + 1 + | .case l m n => l.astSize + m.astSize + n.astSize + 1 + | .mu t => t.astSize + 1 + | .prim _ => 1 + | .mulP m n => m.astSize + n.astSize + 1 + | .let m n => m.astSize + n.astSize + 1 + | .prod m n => m.astSize + n.astSize + 1 + | .fst t => t.astSize + 1 + | .snd t => t.astSize + 1 + | .left t => t.astSize + 1 + | .right t => t.astSize + 1 + | .caseSum s l r => s.astSize + l.astSize + r.astSize + 1 + | .caseVoid v => v.astSize + 1 + | .unit => 1 + | .nil => 1 + | .cons m n => m.astSize + n.astSize + 1 + | .caseList l m n => l.astSize + m.astSize + n.astSize + 1 + -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L120 lemma insert_twice {Γ Δ Φ : Context} {a b c : Ty} (t : Γ‚‚ Δ‚‚ Φ ⊢ a) : rename @@ -187,7 +216,7 @@ lemma insert_twice {Γ Δ Φ : Context} {a b c : Ty} (t : Γ‚‚ Δ‚‚ Φ | .caseList l m n => apply congr_arg₃ caseList <;> try apply insert_twice · rename_i a'; exact insert_twice (Φ := Φ‚ a'‚ .list a') n -termination_by t.size +termination_by t.astSize -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L132 lemma insert_subst_idx @@ -242,7 +271,7 @@ lemma insert_subst | .caseList l m n => apply congr_arg₃ caseList <;> try apply insert_subst · rename_i a'; exact insert_subst (Φ := Φ‚ a'‚ .list a') n -termination_by t.size +termination_by t.astSize -- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L154 lemma shift_subst diff --git a/Plfl/Untyped.lean b/Plfl/Untyped.lean index 5d2e818..6409c47 100644 --- a/Plfl/Untyped.lean +++ b/Plfl/Untyped.lean @@ -347,8 +347,8 @@ def eval (gas : ℕ) (l : ∅ ⊢ a) : Steps l := else match progress l with | .done v => .steps .refl <| .done v - | .step r => - let ⟨rs, res⟩ := eval (gas - 1) _ + | .step (n := n) r => + let ⟨rs, res⟩ := eval (gas - 1) n ⟨Trans.trans r rs, res⟩ namespace Term diff --git a/Plfl/Untyped/Denotational.lean b/Plfl/Untyped/Denotational.lean index 4737d94..5441518 100644 --- a/Plfl/Untyped/Denotational.lean +++ b/Plfl/Untyped/Denotational.lean @@ -333,8 +333,8 @@ namespace Value instance : Trans Subset Subset Included where trans := instTrans.trans variable {u v w : Value} - def Included.fst (s : Included (u ⊔ v) w) : u ⊆ w := fun h => s (Or.inl h) - def Included.snd (s : Included (u ⊔ v) w) : v ⊆ w := fun h => s (Or.inr h) + def Included.fst (s : Included (u ⊔ v) w) : u ⊆ w := s ∘ Or.inl + def Included.snd (s : Included (u ⊔ v) w) : v ⊆ w := s ∘ Or.inr end Value theorem sub_of_elem (e : u ∈ v) : u ⊑ v := by @@ -367,8 +367,8 @@ inductive IsFn (u : Value) : Prop where | isFn (h : u = v ⇾ w) def AllFn (v : Value) : Prop := ∀ {u}, u ∈ v → IsFn u namespace AllFn - def fst (f : AllFn (u ⊔ v)) : AllFn u := fun h => f (Or.inl h) - def snd (f : AllFn (u ⊔ v)) : AllFn v := fun h => f (Or.inr h) + def fst (f : AllFn (u ⊔ v)) : AllFn u := f ∘ Or.inl + def snd (f : AllFn (u ⊔ v)) : AllFn v := f ∘ Or.inr end AllFn lemma not_isFn_bot : ¬ IsFn ⊥ := nofun @@ -402,24 +402,20 @@ theorem included_conjDom (f : AllFn u) (i : v ⇾ w ∈ u) : v ⊆ u.conjDom := rcases i with h | h · calc v _ ⊆ u.conjDom := ih f.fst h - _ ⊆ (u ⊔ u').conjDom := fun h => Or.inl h + _ ⊆ (u ⊔ u').conjDom := Or.inl · calc v _ ⊆ u'.conjDom := ih' f.snd h - _ ⊆ (u ⊔ u').conjDom := fun h => Or.inr h + _ ⊆ (u ⊔ u').conjDom := Or.inr /-- Given a set `u` of identical terms `v ⇾ w`, we know that `u.conjCodom` is included in `w`. -/ theorem conjCodom_included (s : u ⊆ v ⇾ w) : u.conjCodom ⊆ w := by induction u with | bot => - have h := s (u := ⊥) rfl - cases h + cases s (u := ⊥) rfl | fn u₁ u₂ => - have h := s (u := u₁ ⇾ u₂) rfl - cases h; intro _ hx; exact hx + cases s (u := u₁ ⇾ u₂) rfl; intro _ hx; exact hx | conj _ _ ih ih' => intro x h - rcases h with i | i - · exact ih s.fst i - · exact ih' s.snd i + exact Or.elim h (ih s.fst) (ih' s.snd) /-- We say that `v ⇾ w` factors `u` into `u`, if: @@ -438,19 +434,14 @@ def Factor (u u' v w : Value) : Prop := theorem sub_inv (lt : u ⊑ u') {v w} (i : v ⇾ w ∈ u) : ∃ u'', Factor u' u'' v w := by induction lt generalizing v w with | bot => cases i - | conjL _ _ ih ih' => - rcases i with h | h - · exact ih h - · exact ih' h - | conjR₁ _ ih => have ⟨u'', f, s, ss⟩ := ih i; exists u'', f, fun h => Or.inl (s h) - | conjR₂ _ ih => have ⟨u'', f, s, ss⟩ := ih i; exists u'', f, fun h => Or.inr (s h) - | fn lt lt' => cases i; rename_i v v' w' w _ _; exists v ⇾ w, (fun h => IsFn.isFn h), id + | conjL _ _ ih ih' => exact Or.elim i ih ih' + | conjR₁ _ ih => have ⟨u'', f, s, ss⟩ := ih i; exists u'', f, Or.inl ∘ s + | conjR₂ _ ih => have ⟨u'', f, s, ss⟩ := ih i; exists u'', f, Or.inr ∘ s + | fn lt lt' => cases i; rename_i v v' w' w _ _; exists v ⇾ w, (IsFn.isFn ·), id | dist => cases i; rename_i v w w'; exists v ⇾ w ⊔ v ⇾ w' refine ⟨?_, id, ?_, .refl⟩ - · intro _ h; rcases h with h' | h' - · exact .isFn h' - · exact .isFn h' + · exact (Or.elim · .isFn .isFn) · exact .conjL .refl .refl | trans _ _ ih ih' => rename_i u' v' w'; have ⟨u'', f, s, ss⟩ := ih i; have ⟨u'', f, s, ss'⟩ := trans f s ih' @@ -465,14 +456,8 @@ theorem sub_inv (lt : u ⊑ u') {v w} (i : v ⇾ w ∈ u) : ∃ u'', Factor u' u | conj _ _ ih ih' => have ⟨s, s'⟩ := conj_included_inv s have ⟨u₃, f₃, s, ss⟩ := ih f.fst s; have ⟨u₃', f₃', s', ss'⟩ := ih' f.snd s' - exists u₃ ⊔ u₃' - refine ⟨?_, ?_, conj_sub_conj ss.1 ss'.1, conj_sub_conj ss.2 ss'.2⟩ - · intro _ h; rcases h with h' | h' - · exact f₃ h' - · exact f₃' h' - · intro _ h; rcases h with h' | h' - · exact s h' - · exact s' h' + exists u₃ ⊔ u₃', (Or.elim · f₃ f₃'), (Or.elim · s s') + exact ⟨conj_sub_conj ss.1 ss'.1, conj_sub_conj ss.2 ss'.2⟩ lemma sub_inv_fn (lt : v ⇾ w ⊑ u) : ∃ u', diff --git a/Plfl/Untyped/Substitution.lean b/Plfl/Untyped/Substitution.lean index 3a1dc94..729f0f4 100644 --- a/Plfl/Untyped/Substitution.lean +++ b/Plfl/Untyped/Substitution.lean @@ -18,7 +18,7 @@ abbrev Subst (Γ Δ) := ∀ {a : Ty}, Γ ∋ a → Δ ⊢ a abbrev ids : Subst Γ Γ := .var abbrev shift : Subst Γ (Γ‚ a) := .var ∘ .s -@[simp] def cons (m : Δ ⊢ a) (σ : Subst Γ Δ) : Subst (Γ‚ a) Δ +abbrev cons (m : Δ ⊢ a) (σ : Subst Γ Δ) : Subst (Γ‚ a) Δ | _, .z => m | _, .s x => σ x @@ -88,10 +88,12 @@ section theorem sub_ids {Γ} {m : Γ ⊢ a} : ⟪ids (Γ := Γ)⟫ m = m := by match m with | ‵ _ => rfl - | ƛ n => apply congr_arg Term.lam; convert sub_ids; - simp_all only - ext x_1 x_2 : 2 - simp_all only [exts_ids] + | ƛ n => + apply congr_arg Term.lam + convert sub_ids + simp_all only + ext x_1 x_2 : 2 + simp_all only [exts_ids] | l □ m => simp only [sub_ap]; apply congr_arg₂ Term.ap <;> exact sub_ids theorem rename_id : rename (λ {_} x => x) m = m := by @@ -127,8 +129,8 @@ section apply congr_arg Term.lam let ρ' : ∀ {Γ}, Rename Γ (Γ‚ ✶) - | [] => λ i => by cases i - | _ :: _ => ext ρ + | [] => by intro i; apply @ρ; exact i + | ✶ :: Γ => by intro i; apply ext ρ; exact i apply comm_subst_rename (Γ := Γ‚ ✶) (Δ := Δ‚ ✶) (σ := exts σ) (ρ := ρ') (m := n); intro | .z => rfl From de2172f7ac50608575aa17b492ea3a8455bbced3 Mon Sep 17 00:00:00 2001 From: Serhii Khoma Date: Sat, 30 May 2026 18:08:33 +0700 Subject: [PATCH 8/8] feat: make compilation faster by making imports minimal --- Plfl/DeBruijn.lean | 6 +++++- Plfl/Init.lean | 5 +++-- Plfl/Lambda.lean | 3 +++ Plfl/Lambda/Properties.lean | 1 + Plfl/More.lean | 2 ++ Plfl/More/Bisimulation.lean | 1 + Plfl/Untyped.lean | 3 +++ Plfl/Untyped/BigStep.lean | 1 + Plfl/Untyped/Denotational.lean | 4 ++++ Plfl/Untyped/Denotational/Adequacy.lean | 16 +++++++++++----- Plfl/Untyped/Denotational/Compositional.lean | 1 + Plfl/Untyped/Substitution.lean | 6 ++++-- 12 files changed, 39 insertions(+), 10 deletions(-) diff --git a/Plfl/DeBruijn.lean b/Plfl/DeBruijn.lean index a209901..dfb235b 100644 --- a/Plfl/DeBruijn.lean +++ b/Plfl/DeBruijn.lean @@ -2,7 +2,11 @@ module -- https://plfa.github.io/DeBruijn/ -public import Plfl.Init +import Plfl.Init +import Batteries.Tactic.Init +import Mathlib.Data.Nat.Notation +import Mathlib.Tactic.Basic +public import Mathlib.Logic.IsEmpty.Defs @[expose] public section diff --git a/Plfl/Init.lean b/Plfl/Init.lean index 58f27cf..e35a104 100644 --- a/Plfl/Init.lean +++ b/Plfl/Init.lean @@ -1,6 +1,7 @@ module -public import Mathlib.Tactic +public import Mathlib.Logic.IsEmpty.Defs +public import Mathlib.Logic.IsEmpty.Basic @[expose] public section @@ -18,7 +19,7 @@ abbrev Decidable' α := IsEmpty α ⊕' α namespace Decidable' def toDecidable : Decidable' α → Decidable (Nonempty α) := by intro | .inr a => right; exact ⟨a⟩ - | .inl na => left; simpa + | .inl na => left; simpa only [not_nonempty_iff] end Decidable' instance [Repr α] : Repr (Decidable' α) where diff --git a/Plfl/Lambda.lean b/Plfl/Lambda.lean index 88878a4..628f79b 100644 --- a/Plfl/Lambda.lean +++ b/Plfl/Lambda.lean @@ -3,6 +3,9 @@ module -- https://plfa.github.io/Lambda/ public import Plfl.Init +import Mathlib.Data.Nat.Notation +import Mathlib.Tactic.ApplyFun +public import Mathlib.Logic.Embedding.Basic @[expose] public section diff --git a/Plfl/Lambda/Properties.lean b/Plfl/Lambda/Properties.lean index f9255c1..400a731 100644 --- a/Plfl/Lambda/Properties.lean +++ b/Plfl/Lambda/Properties.lean @@ -5,6 +5,7 @@ module public meta import Plfl.Init public meta import Plfl.Lambda import Plfl.Lambda +import Mathlib.Tactic.Basic @[expose] public section diff --git a/Plfl/More.lean b/Plfl/More.lean index 82252cd..fce7bde 100644 --- a/Plfl/More.lean +++ b/Plfl/More.lean @@ -3,6 +3,8 @@ module -- https://plfa.github.io/More/ public import Plfl.Init +import Batteries.Tactic.Init +public import Mathlib.Data.Matrix.Mul @[expose] public section diff --git a/Plfl/More/Bisimulation.lean b/Plfl/More/Bisimulation.lean index 88d3cd6..804ded3 100644 --- a/Plfl/More/Bisimulation.lean +++ b/Plfl/More/Bisimulation.lean @@ -4,6 +4,7 @@ module public import Plfl.Init public import Plfl.More +import Mathlib.Tactic.Basic @[expose] public section diff --git a/Plfl/Untyped.lean b/Plfl/Untyped.lean index 6409c47..fe10bb0 100644 --- a/Plfl/Untyped.lean +++ b/Plfl/Untyped.lean @@ -3,6 +3,9 @@ module -- https://plfa.github.io/Untyped/ public import Plfl.Init +import Mathlib.Data.Nat.Notation +public import Mathlib.Logic.Equiv.Defs +import Mathlib.Tactic.Basic @[expose] public section diff --git a/Plfl/Untyped/BigStep.lean b/Plfl/Untyped/BigStep.lean index a373d30..bc84ad8 100644 --- a/Plfl/Untyped/BigStep.lean +++ b/Plfl/Untyped/BigStep.lean @@ -5,6 +5,7 @@ module public import Plfl.Init public import Plfl.Untyped public import Plfl.Untyped.Substitution +import Mathlib.Logic.Lemmas @[expose] public section diff --git a/Plfl/Untyped/Denotational.lean b/Plfl/Untyped/Denotational.lean index 5441518..c8f0896 100644 --- a/Plfl/Untyped/Denotational.lean +++ b/Plfl/Untyped/Denotational.lean @@ -5,6 +5,10 @@ module public import Plfl.Init public import Plfl.Untyped public import Plfl.Untyped.Substitution +import Mathlib.Data.Nat.Notation +import Mathlib.Tactic.Convert +public import Mathlib.Order.Notation +import Mathlib.Tactic.Basic @[expose] public section diff --git a/Plfl/Untyped/Denotational/Adequacy.lean b/Plfl/Untyped/Denotational/Adequacy.lean index 4008ca8..f99b780 100644 --- a/Plfl/Untyped/Denotational/Adequacy.lean +++ b/Plfl/Untyped/Denotational/Adequacy.lean @@ -5,6 +5,10 @@ module public import Plfl.Init public import Plfl.Untyped.BigStep public import Plfl.Untyped.Denotational.Soundness +public import Mathlib.Tactic +import Mathlib.Algebra.Order.Monoid.Unbundled.Basic +import Mathlib.Algebra.Order.Monoid.Canonical.Defs +import Mathlib.Algebra.Order.SuccPred @[expose] public section @@ -74,10 +78,12 @@ mutual | _, .clos (_ □ _) _ => ⊥ | ⊥, .clos (ƛ _) _ => ⊤ | vw@(v ⇾ w), .clos (ƛ n) γ => - have : sizeOf w < sizeOf vw := by subst_vars; simp + have : sizeOf w < sizeOf vw := by subst_vars; simp only [Value.fn.sizeOf_spec, + lt_add_iff_pos_left, add_pos_iff, Order.lt_one_iff, true_or] ∀ {c}, 𝔼 v c → GtFn w → ∃ c', (γ‚' c ⊢ n ⇓ c') ∧ 𝕍 w c' | uv@(.conj u v), c@(.clos (ƛ _) _) => - have : sizeOf v < sizeOf uv := by subst_vars; simp + have : sizeOf v < sizeOf uv := by subst_vars; simp only [Value.conj.sizeOf_spec, + lt_add_iff_pos_left, add_pos_iff, Order.lt_one_iff, true_or] 𝕍 u c ∧ 𝕍 v c /-- @@ -103,10 +109,10 @@ def WHNF (t : Γ ⊢ a) : Prop := ∃ n : Γ‚ ✶ ⊢ ✶, t = (ƛ n) /-- A closure in a 𝕍 relation must be in WHNF. -/ lemma WHNF.of_𝕍 (vc : 𝕍 v (.clos m γ)) : WHNF m := by - cases m with (try simp [𝕍] at vc; try contradiction) | lam n => exists n + cases m with (try simp only [𝕍, «Prop».bot_eq_false] at vc; try contradiction) | lam n => exists n lemma 𝕍.conj (uc : 𝕍 u c) (vc : 𝕍 v c) : 𝕍 (u ⊔ v) c := by - let .clos m γ := c; cases m with (try simp [𝕍] at *; try contradiction) + let .clos m γ := c; cases m with (try simp only [𝕍, «Prop».bot_eq_false] at *; try contradiction) | lam => unfold 𝕍; exact ⟨uc, vc⟩ lemma 𝕍.of_not_gtFn (nf : ¬ GtFn v) : 𝕍 v (.clos (ƛ n) γ') := by induction v with unfold 𝕍 @@ -115,7 +121,7 @@ lemma 𝕍.of_not_gtFn (nf : ¬ GtFn v) : 𝕍 v (.clos (ƛ n) γ') := by induct | conj _ _ ih ih' => exact not_gtFn_conj_inv nf |>.imp ih ih' lemma 𝕍.sub {v v'} (vvc : 𝕍 v c) (lt : v' ⊑ v) : 𝕍 v' c := by - let .clos m γ := c; cases m with (try simp [𝕍] at *; try contradiction) | lam m => + let .clos m γ := c; cases m with (try simp only [𝕍, «Prop».bot_eq_false] at *; try contradiction) | lam m => rename_i Γ; induction lt generalizing Γ with | bot => unfold 𝕍; trivial | conjL _ _ ih ih' => unfold 𝕍; exact ⟨ih _ _ _ vvc, ih' _ _ _ vvc⟩ diff --git a/Plfl/Untyped/Denotational/Compositional.lean b/Plfl/Untyped/Denotational/Compositional.lean index a04f9bd..66e18f0 100644 --- a/Plfl/Untyped/Denotational/Compositional.lean +++ b/Plfl/Untyped/Denotational/Compositional.lean @@ -4,6 +4,7 @@ module public import Plfl.Init public import Plfl.Untyped.Denotational +public import Mathlib.Order.BooleanAlgebra.Defs @[expose] public section diff --git a/Plfl/Untyped/Substitution.lean b/Plfl/Untyped/Substitution.lean index 729f0f4..75b6c40 100644 --- a/Plfl/Untyped/Substitution.lean +++ b/Plfl/Untyped/Substitution.lean @@ -4,7 +4,9 @@ module public import Plfl.Init public import Plfl.Untyped - +import Batteries.Tactic.Init +import Batteries.Logic +import Mathlib.Tactic @[expose] public section namespace Substitution @@ -70,7 +72,7 @@ section simp only [rename_subst_ren]; congr theorem exts_cons_shift : exts (a := a) (b := b) σ = (‵ .z ⦂⦂ (σ ⨟ shift)) := by - funext i; cases i <;> simp [exts, seq, cons, rename_shift] + funext i; cases i <;> simp only [exts, rename_shift, cons, seq, Function.comp_apply] theorem ext_cons_z_shift : @Eq (Γ‚ b ∋ a → Δ‚ b ⊢ a) (ren (ext ρ)) (‵ .z ⦂⦂ (ren ρ ⨟ shift)) := by funext i; cases i <;> simp only [ren_ext, exts, rename_subst_ren, ren_shift]; rfl