diff --git a/Plfl.lean b/Plfl.lean
index 657eeef..0bb1613 100644
--- a/Plfl.lean
+++ b/Plfl.lean
@@ -1,16 +1,19 @@
-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.Confluence
-import Plfl.Untyped.Substitution
-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 3efad76..dfb235b 100644
--- a/Plfl/DeBruijn.lean
+++ b/Plfl/DeBruijn.lean
@@ -1,6 +1,14 @@
+module
+
-- https://plfa.github.io/DeBruijn/
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
-- Sorry, nothing is inherited from previous chapters here. We have to start over.
namespace DeBruijn
@@ -42,12 +50,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
@@ -78,11 +86,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 +145,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 +173,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 +184,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 +205,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 +303,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 +330,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
@@ -353,8 +364,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) (by trivial)
+ | .step (n := n) r =>
+ let ⟨rs, res⟩ := eval (gas - 1) n
⟨.cons r rs, res⟩
section examples
@@ -363,7 +374,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 13989b8..e35a104 100644
--- a/Plfl/Init.lean
+++ b/Plfl/Init.lean
@@ -1,8 +1,9 @@
-import Std.Data.List.Lemmas
+module
-import Mathlib.Data.Vector
-import Mathlib.Logic.IsEmpty
-import Mathlib.Tactic
+public import Mathlib.Logic.IsEmpty.Defs
+public import Mathlib.Logic.IsEmpty.Basic
+
+@[expose] public section
/--
`is_empty` converts `IsEmpty α` to `α → False`.
@@ -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
@@ -31,17 +32,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) := by
- exists v.1.dropLast; simp only [List.length_dropLast, Vector.length_val]
-
- 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
-end Vector
diff --git a/Plfl/Lambda.lean b/Plfl/Lambda.lean
index f6e2124..628f79b 100644
--- a/Plfl/Lambda.lean
+++ b/Plfl/Lambda.lean
@@ -1,6 +1,13 @@
+module
+
-- https://plfa.github.io/Lambda/
-import Plfl.Init
+public import Plfl.Init
+import Mathlib.Data.Nat.Notation
+import Mathlib.Tactic.ApplyFun
+public import Mathlib.Logic.Embedding.Basic
+
+@[expose] public section
namespace Lambda
@@ -26,11 +33,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 +46,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 +83,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 +97,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 +131,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 +203,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 +249,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 +257,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 +342,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 +351,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 +374,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 +399,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 +408,41 @@ 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
+ example : ∅ ⊬ 𝟘 □ 1 :=
+ ⟨fun | .tyAp hl _ => by 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]
+ lemma nty_illLam : ∅ ⊬ illLam :=
+ ⟨fun | .tyLam (.tyAp (.tyVar hx) (.tyVar hx')) => Ty.t_to_t'_ne_t _ _ (Lookup.functional hx hx')⟩
-- https://plfa.github.io/Lambda/#quiz-3
- example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊢ `"y" □ `"x" ⦂ ℕt := by
+ example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊢ ‵"y" □ ‵"x" ⦂ ℕt := by
apply tyAp <;> trivial
- example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊬ `"x" □ `"y" := 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" ⦂ ℕt ⊬ ‵"x" □ ‵"y" :=
+ ⟨fun | .tyAp (.tyVar hx) _ => by cases hx with | s _ _ => contradiction⟩
- example : ∅‚ "y" ⦂ ℕt =⇒ ℕt ⊢ ƛ "x" : `"y" □ `"x" ⦂ ℕt =⇒ ℕt := by
+ example : ∅‚ "y" ⦂ ℕt =⇒ ℕt ⊢ ƛ "x" : ‵"y" □ ‵"x" ⦂ ℕt =⇒ ℕt := by
apply tyLam; apply tyAp <;> trivial
- example : ∅‚ "x" ⦂ t ⊬ `"x" □ `"x" := 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" :=
+ ⟨fun
+ | .tyAp (.tyVar .z) (.tyVar (.s _ _)) => by contradiction
+ | .tyAp (.tyVar (.s _ _)) _ => by 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..400a731 100644
--- a/Plfl/Lambda/Properties.lean
+++ b/Plfl/Lambda/Properties.lean
@@ -1,7 +1,13 @@
+module
+
-- https://plfa.github.io/Properties/
-import Plfl.Init
+public meta import Plfl.Init
+public meta import Plfl.Lambda
import Plfl.Lambda
+import Mathlib.Tactic.Basic
+
+@[expose] public section
open Lambda
@@ -11,12 +17,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 +39,41 @@ 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]
+ | ⟨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]; split
- · simp_all only [Prod.mk.injEq]
+ rw [wellTypedInv, wellTyped];
+ · simp_all only
/--
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.
+ nofun
def weaken : ∅ ⊢ m ⦂ t → Γ ⊢ m ⦂ t := by
intro j; refine rename ?_ j; exact Lookup.weaken
@@ -305,12 +318,15 @@ 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
- #eval eval 3 tySuccμ |>.3
+ /--
+ info: Properties.Result.dnf
+ -/
+ #guard_msgs in #eval eval 3 tySuccμ |>.3
abbrev add_2_2 := add □ 2 □ 2
@@ -327,7 +343,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
@@ -335,25 +355,35 @@ section subject_expansion
-- 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]
+ by_contra f
+ simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff]
let illCase := 𝟘? 𝟘 [zero: 𝟘 |succ "x" : add]
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β
+ intro t
+ refine ⟨fun j => ?_⟩
+ 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; simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff]
+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
- 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)
+ intro tt
+ refine ⟨fun j => ?_⟩
+ 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
+ have := f 𝟘 ℕt illAp tyZero h_red -- Pass arguments explicitly
exact nty_ill.false this.some
end subject_expansion
@@ -361,7 +391,7 @@ end subject_expansion
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 +400,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 +418,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..fce7bde 100644
--- a/Plfl/More.lean
+++ b/Plfl/More.lean
@@ -1,6 +1,12 @@
+module
+
-- https://plfa.github.io/More/
-import Plfl.Init
+public import Plfl.Init
+import Batteries.Tactic.Init
+public import Mathlib.Data.Matrix.Mul
+
+@[expose] public section
-- This module was extended from the original one for .
namespace More
@@ -148,13 +154,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 +221,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 +258,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 +269,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 +294,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 +309,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 +426,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 +446,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 +467,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 +479,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
@@ -554,8 +563,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) (by trivial)
+ | .step (n := n) r =>
+ let ⟨rs, res⟩ := eval (gas - 1) n
⟨Trans.trans r rs, res⟩
section examples
@@ -566,22 +575,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 2e6f63b..804ded3 100644
--- a/Plfl/More/Bisimulation.lean
+++ b/Plfl/More/Bisimulation.lean
@@ -1,14 +1,19 @@
+module
+
-- https://plfa.github.io/Bisimulation/
-import Plfl.Init
-import Plfl.More
+public import Plfl.Init
+public import Plfl.More
+import Mathlib.Tactic.Basic
+
+@[expose] public section
open More
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 +21,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 =>
@@ -62,13 +67,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 +84,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 +122,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 +146,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 76bf124..db6fcad 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
@@ -32,14 +36,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 +88,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 +133,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
@@ -145,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
@@ -153,7 +186,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 +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.astSize
-- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L132
lemma insert_subst_idx
@@ -207,7 +241,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 +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.astSize
-- https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda#L154
lemma shift_subst
@@ -262,7 +297,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 +352,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..3ead3d4 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
@@ -98,7 +102,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 +117,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 +138,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 □ 𝟘
@@ -180,14 +184,17 @@ 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
/--
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 +287,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 +316,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 +334,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 +346,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 +373,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 +385,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 +396,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 +407,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 +437,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
@@ -432,53 +445,86 @@ 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:
-#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
@@ -517,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
diff --git a/Plfl/Untyped.lean b/Plfl/Untyped.lean
index f04d855..fe10bb0 100644
--- a/Plfl/Untyped.lean
+++ b/Plfl/Untyped.lean
@@ -1,6 +1,13 @@
+module
+
-- https://plfa.github.io/Untyped/
-import Plfl.Init
+public import Plfl.Init
+import Mathlib.Data.Nat.Notation
+public import Mathlib.Logic.Equiv.Defs
+import Mathlib.Tactic.Basic
+
+@[expose] public section
namespace Untyped
@@ -45,16 +52,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
+ 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
instance : Coe ℕ Context where coe := Context.equiv_nat.invFun
@@ -89,8 +96,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 +108,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 +134,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 +161,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 +189,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 +210,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 +262,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 +302,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)
@@ -348,8 +350,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) (by trivial)
+ | .step (n := n) r =>
+ let ⟨rs, res⟩ := eval (gas - 1) n
⟨Trans.trans r rs, res⟩
namespace Term
@@ -405,18 +407,151 @@ 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
+ /--
+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 (gas := 3) fourC'
- #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 20bb1ea..bc84ad8 100644
--- a/Plfl/Untyped/BigStep.lean
+++ b/Plfl/Untyped/BigStep.lean
@@ -1,8 +1,13 @@
+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
+import Mathlib.Logic.Lemmas
+
+@[expose] public section
namespace BigStep
@@ -22,7 +27,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 +44,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 +64,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 +89,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..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
@@ -13,7 +17,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 +26,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 +44,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
@@ -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
@@ -137,7 +143,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 +158,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..c8f0896 100644
--- a/Plfl/Untyped/Denotational.lean
+++ b/Plfl/Untyped/Denotational.lean
@@ -1,8 +1,16 @@
+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
+import Mathlib.Data.Nat.Notation
+import Mathlib.Tactic.Convert
+public import Mathlib.Order.Notation
+import Mathlib.Tactic.Basic
+
+@[expose] public section
namespace Denotational
@@ -18,7 +26,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 +127,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 +151,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 +284,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.pop ⊔ 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 +305,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
+ · convert sub_env (@r vs.pop) ?_ using 1
+ · simp_all only [List.empty_eq, Vector.getElem_pop']
+ · intro x; cases x with
+ | z =>
+ simp_all only [List.empty_eq, Vector.getElem_pop']
+ rfl
+ | 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 +326,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 +337,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 := 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 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 +371,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 := f ∘ Or.inl
+ def snd (f : AllFn (u ⊔ v)) : AllFn v := f ∘ Or.inr
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 +401,25 @@ 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 := Or.inl
+ · calc v
+ _ ⊆ u'.conjDom := ih' f.snd 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 => 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 =>
+ cases s (u := ⊥) rfl
+| fn u₁ u₂ =>
+ cases s (u := u₁ ⇾ u₂) rfl; intro _ hx; exact hx
+| conj _ _ ih ih' =>
+ intro x h
+ exact Or.elim h (ih s.fst) (ih' s.snd)
/--
We say that `v ⇾ w` factors `u` into `u`, if:
@@ -420,13 +438,15 @@ 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' => 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 ⟨(Or.elim · .isFn .isFn), id, ?_, .refl⟩; exact .conjL .refl .refl
+ refine ⟨?_, id, ?_, .refl⟩
+ · 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'
exists u'', f, s; exact ⟨ss'.1.trans ss.1, ss.2.trans ss'.2⟩
@@ -435,7 +455,7 @@ 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
diff --git a/Plfl/Untyped/Denotational/Adequacy.lean b/Plfl/Untyped/Denotational/Adequacy.lean
index 3a63132..f99b780 100644
--- a/Plfl/Untyped/Denotational/Adequacy.lean
+++ b/Plfl/Untyped/Denotational/Adequacy.lean
@@ -1,8 +1,16 @@
+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
+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
namespace Adequacy
@@ -66,14 +74,16 @@ mutual
- `c`'s body evaluates according to `v`.
-/
def 𝕍 : Value → Clos → Prop
- | _, .clos (` _) _ => ⊥
+ | _, .clos (‵ _) _ => ⊥
| _, .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
/--
@@ -99,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 𝕍
@@ -111,9 +121,9 @@ 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 => 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 +160,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..66e18f0 100644
--- a/Plfl/Untyped/Denotational/Compositional.lean
+++ b/Plfl/Untyped/Denotational/Compositional.lean
@@ -1,7 +1,12 @@
+module
+
-- https://plfa.github.io/Compositional/
-import Plfl.Init
-import Plfl.Untyped.Denotational
+public import Plfl.Init
+public import Plfl.Untyped.Denotational
+public import Mathlib.Order.BooleanAlgebra.Defs
+
+@[expose] public section
namespace Compositional
@@ -77,15 +82,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 +146,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/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 461c1b7..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
@@ -47,7 +51,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 +93,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..75b6c40 100644
--- a/Plfl/Untyped/Substitution.lean
+++ b/Plfl/Untyped/Substitution.lean
@@ -1,7 +1,13 @@
+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
+import Batteries.Tactic.Init
+import Batteries.Logic
+import Mathlib.Tactic
+@[expose] public section
namespace Substitution
@@ -35,13 +41,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 +59,46 @@ 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 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
- 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 +111,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 +125,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 Γ (Γ‚ ✶)
+ | [] => by intro i; apply @ρ; exact i
+ | ✶ :: Γ => by intro i; apply ext ρ; exact i
apply comm_subst_rename (Γ := Γ‚ ✶) (Δ := Δ‚ ✶) (σ := exts σ) (ρ := ρ') (m := n); intro
| .z => rfl
@@ -137,15 +149,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 +170,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 +188,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..4276e5e 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/aesop",
"type": "git",
"subDir": null,
- "rev": "f58165d3d6e0b048d89e56944e98d9054b223d9b",
- "name": "std",
+ "scope": "leanprover-community",
+ "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+ "name": "aesop",
"manifestFile": "lake-manifest.json",
- "inputRev": "main",
- "inherited": true,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover-community/quote4",
+ "inputRev": "v4.30.0",
+ "inherited": false,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/mathlib4",
"type": "git",
"subDir": null,
- "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
- "name": "Qq",
+ "scope": "leanprover-community",
+ "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
+ "name": "mathlib",
"manifestFile": "lake-manifest.json",
- "inputRev": "master",
- "inherited": true,
+ "inputRev": "v4.30.0",
+ "inherited": false,
"configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover-community/aesop",
+ {"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
- "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
- "name": "aesop",
+ "scope": "leanprover-community",
+ "rev": "32dc18cde3684679f3c003de608743b57498c56f",
+ "name": "batteries",
"manifestFile": "lake-manifest.json",
- "inputRev": "master",
+ "inputRev": "v4.30.0",
"inherited": true,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover-community/ProofWidgets4",
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
- "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
- "name": "proofwidgets",
+ "scope": "leanprover-community",
+ "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+ "name": "plausible",
"manifestFile": "lake-manifest.json",
- "inputRev": "v0.0.30",
+ "inputRev": "main",
"inherited": true,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover/lean4-cli",
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/LeanSearchClient",
"type": "git",
"subDir": null,
- "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
- "name": "Cli",
+ "scope": "leanprover-community",
+ "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+ "name": "LeanSearchClient",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover-community/import-graph.git",
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/import-graph",
"type": "git",
"subDir": null,
- "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+ "scope": "leanprover-community",
+ "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover-community/ProofWidgets4",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover-community",
+ "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+ "name": "proofwidgets",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "v0.0.99",
+ "inherited": true,
"configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover-community/mathlib4.git",
+ {"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
- "rev": "afdc7729cafc1ca476165b2ade89d4150bcb1dd2",
- "name": "mathlib",
+ "scope": "leanprover-community",
+ "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+ "name": "Qq",
"manifestFile": "lake-manifest.json",
- "inputRev": null,
- "inherited": false,
- "configFile": "lakefile.lean"}],
+ "inputRev": "v4.30.0",
+ "inherited": true,
+ "configFile": "lakefile.toml"},
+ {"url": "https://github.com/leanprover/lean4-cli",
+ "type": "git",
+ "subDir": null,
+ "scope": "leanprover",
+ "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+ "name": "Cli",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "v4.30.0",
+ "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..c542f7f
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,33 @@
+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"
+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]]
+name = "Plfl"
+
+# [[lean_exe]]
+# name = "plfl"
+# root = "Main"
+# defaultTarget = true
diff --git a/lean-toolchain b/lean-toolchain
index 9ad3040..af9e5d3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.30.0