Update to latest lean

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

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

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