update to v4.33.0-rc1

Plfl/Lambda.lean

@@ -12,7 +12,7 @@ namespace Lambda
 
 open String
 
-def Sym : Type := String deriving BEq, DecidableEq, Repr
+abbrev Sym : Type := String
 
 -- https://plfa.github.io/Lambda/#syntax-of-terms
 inductive Term where
@@ -326,7 +326,7 @@ namespace Context
   : ∅‚ "x" ⦂ ℕt =⇒ ℕt‚ "y" ⦂ ℕt‚ "z" ⦂ ℕt
   ∋ "x" ⦂ ℕt =⇒ ℕt
   := open Lookup in by
-    apply s _; apply s _; apply z; repeat trivial
+    apply s (by decide); apply s (by decide); apply z
 
   -- https://plfa.github.io/Lambda/#lookup-is-functional
   theorem Lookup.functional : Γ ∋ x ⦂ t → Γ ∋ x ⦂ t' → t = t' := by intro
@@ -368,7 +368,7 @@ namespace Context
   syntax "lookup_var" : tactic
   macro_rules
   | `(tactic| lookup_var) =>
-    `(tactic| apply IsTy.tyVar; repeat (first | apply Lookup.s (by trivial) | exact Lookup.z))
+    `(tactic| apply IsTy.tyVar; repeat (first | apply Lookup.s (by decide) | exact Lookup.z))
 
   -- Inform `trivial` of our new tactic.
   macro_rules | `(tactic| trivial) => `(tactic| lookup_var)

Plfl/Lambda/Properties.lean

@@ -165,8 +165,8 @@ namespace Progress
   def equivProgress' : Progress m ≃ Progress' m where
     toFun := toProgress'
     invFun := 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']
+    left_inv := by intro | step _ => rfl | done _ => rfl
+    right_inv := by intro | inl _ => rfl | inr ⟨n, r⟩ => rfl
 end Progress
 
 -- https://plfa.github.io/Properties/#renaming
@@ -422,7 +422,7 @@ theorem preserves_unstuck : ∅ ⊢ m ⦂ t → (m —↠ n) → IsEmpty (Stuck
   intro j r; have := preserves j r; exact unstuck this
 
 -- https://plfa.github.io/Properties/#reduction-is-deterministic
-def Reduce.det : (m —→ n) → (m —→ n') → n = n' := by
+theorem Reduce.det : (m —→ n) → (m —→ n') → n = n' := by
   intro r r'; cases r
   · case lamβ =>
     cases r' <;> try trivial

Plfl/More/Bisimulation.lean

@@ -64,22 +64,22 @@ namespace Sim
       | lam => exact .lam
 
   -- https://plfa.github.io/Bisimulation/#simulation-commutes-with-renaming
-  def comm_rename (ρ : ∀ {a}, Γ ∋ a → Δ ∋ a) {m m' : Γ ⊢ a}
+  theorem comm_rename (ρ : ∀ {a}, Γ ∋ a → Δ ∋ a) {m m' : Γ ⊢ a}
   : m ~ m' → rename ρ m ~ rename ρ m'
   | .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}
+  theorem comm_exts {σ σ' : ∀ {a}, Γ ∋ a → Δ ⊢ a}
   (gs : ∀ {a}, (x : Γ ∋ a) → σ x ~ σ' x)
   : (∀ {a b}, (x : Γ‚ b ∋ a) → exts σ x ~ exts σ' x)
   := by introv; match x with
   | .z => simp only [exts]; exact .var
   | .s x => simp only [exts]; apply comm_rename Lookup.s; apply gs
 
-  def comm_subst {σ σ' : ∀ {a}, Γ ∋ a → Δ ⊢ a}
+  theorem comm_subst {σ σ' : ∀ {a}, Γ ∋ a → Δ ⊢ a}
   (gs : ∀ {a}, (x : Γ ∋ a) → @σ a x ~ @σ' a x)
   {m m' : Γ ⊢ a}
   : m ~ m' → subst σ m ~ subst σ' m'
@@ -88,7 +88,7 @@ namespace Sim
   | .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}
+  theorem comm_subst₁ {m m' : Γ ⊢ b} {n n' : Γ‚ b ⊢ a}
   (sm : m ~ m') (sn : n ~ n') : n⟦m⟧ ~ n'⟦m'⟧
   := by
     let σ {a} : Γ‚ b ∋ a → Γ ⊢ a := subst₁σ m
@@ -121,7 +121,7 @@ m' - —→ - n'
 inductive Leg (m' n : Γ ⊢ a) : Prop where
 | intro (sim : n ~ n') (red : m' —→ n')
 
-def Leg.fromLegInv {m m' n : Γ ⊢ a} : (m ~ m') → (m —→ n) → Leg m' n
+theorem 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')
@@ -145,7 +145,7 @@ m - —→ - n
 inductive LegInv (m n' : Γ ⊢ a) : Prop where
 | intro (sim : n ~ n') (red : m —→ n)
 
-def LegInv.fromLeg {m m' n' : Γ ⊢ a} : (m ~ m') → (m' —→ n') → LegInv m n'
+theorem 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')

Plfl/More/Inference.lean

@@ -14,7 +14,7 @@ namespace Inference
 -- https://plfa.github.io/Inference/#syntax
 open String
 
-def Sym : Type := String deriving BEq, DecidableEq, Repr
+abbrev Sym : Type := String
 
 inductive Ty where
 /-- Native natural type made of 𝟘 and ι. -/
@@ -184,6 +184,7 @@ namespace Notation
   scoped macro "♯ " n:term:90 : term => `(by get_elem $n)
 end Notation
 
+open Notation in
 instance : Repr (Γ ∋ m ⦂ a) where reprPrec i n := "♯" ++ reprPrec n (sizeOf i)
 
 /--

Plfl/Untyped/Confluence.lean

@@ -58,13 +58,13 @@ 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)
+  theorem 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)
+  theorem toReduceClos : (m ⇛ n) → (m —↠ n)
   | .var => Untyped.Reduce.Clos.refl
   | .lamβ (n:=n) (n':=n') (v:=v) (v':=v') rn rv =>
     calc (ƛ n) □ v

Plfl/Untyped/Denotational.lean

@@ -51,34 +51,34 @@ end Notation
 instance : Trans Sub Sub Sub where trans := .trans
 
 @[refl]
-def Sub.refl : v ⊑ v := match v with
+theorem Sub.refl : v ⊑ v := match v with
 | ⊥ => .bot
 | _ ⇾ _ => .fn refl refl
 | .conj _ _ => .conjL (.conjR₁ refl) (.conjR₂ refl)
 
-def sub_of_sub_bot (d : v ⊑ ⊥) : v ⊑ u := d.trans .bot
+theorem sub_of_sub_bot (d : v ⊑ ⊥) : v ⊑ u := d.trans .bot
 
 /-- The `⊔` operation is monotonic with respect to `⊑`. -/
-def conj_sub_conj (d₁ : v ⊑ v') (d₂ : w ⊑ w') : v ⊔ w ⊑ v' ⊔ w' :=
+theorem conj_sub_conj (d₁ : v ⊑ v') (d₂ : w ⊑ w') : v ⊔ w ⊑ v' ⊔ w' :=
   .conjL (.conjR₁ d₁) (.conjR₂ d₂)
 
-def fn_conj_sub_conj_fn : (v ⊔ v') ⇾ (w ⊔ w') ⊑ (v ⇾ w) ⊔ (v' ⇾ w') := calc
+theorem fn_conj_sub_conj_fn : (v ⊔ v') ⇾ (w ⊔ w') ⊑ (v ⇾ w) ⊔ (v' ⇾ w') := calc
   _ ⊑ ((v ⊔ v') ⇾ w) ⊔ ((v ⊔ v') ⇾ w') := .dist
-  _ ⊑ (v ⇾ w) ⊔ (v' ⇾ w') := open Sub in by
+  _ ⊑ (v ⇾ w) ⊔ (v' ⇾ w') := open Denotational.Sub in by
     apply conj_sub_conj <;> refine .fn ?_ .refl
     · apply conjR₁; rfl
     · apply conjR₂; rfl
 
 -- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Termination.20of.20head.20induction.20on.20.60ReflTransGen.60/near/375468050
-def conj_sub₁ (h : u ⊔ v ⊑ w) : u ⊑ w := by
+theorem conj_sub₁ (h : u ⊔ v ⊑ w) : u ⊑ w := by
   generalize hx : u ⊔ v = x at *
   induction h with (subst_vars; try cases hx)
   | conjL h _ => exact h
   | conjR₁ h ih => exact .conjR₁ (ih rfl)
   | conjR₂ h ih => exact .conjR₂ (ih rfl)
   | trans h h' ih => exact .trans (ih rfl) h'
 
-def conj_sub₂ (h : u ⊔ v ⊑ w) : v ⊑ w := by
+theorem conj_sub₂ (h : u ⊔ v ⊑ w) : v ⊑ w := by
   generalize hx : u ⊔ v = x at *
   induction h with (subst_vars; try cases hx)
   | conjL _ h => exact h
@@ -132,15 +132,15 @@ namespace Notation
 end Notation
 
 namespace Env.Sub
-  @[refl] def refl : γ `⊑ γ | _ => .refl
-  @[simp] def conjR₁ (γ δ : Env Γ) : γ `⊑ (γ ⊔ δ) | _ => .conjR₁ .refl
-  @[simp] def conjR₂ (γ δ : Env Γ) : δ `⊑ (γ ⊔ δ) | _ => .conjR₂ .refl
+  @[refl] theorem refl : γ `⊑ γ | _ => .refl
+  @[simp] theorem conjR₁ (γ δ : Env Γ) : γ `⊑ (γ ⊔ δ) | _ => .conjR₁ .refl
+  @[simp] theorem conjR₂ (γ δ : Env Γ) : δ `⊑ (γ ⊔ δ) | _ => .conjR₂ .refl
 
-  def ext_le (lt : v ⊑ v') : (γ`‚ v) `⊑ (γ`‚ v')
+  theorem ext_le (lt : v ⊑ v') : (γ`‚ v) `⊑ (γ`‚ v')
   | .z => lt
   | .s _ => .refl
 
-  def le_ext (lt : γ `⊑ γ') : (γ`‚ v) `⊑ (γ'`‚ v)
+  theorem le_ext (lt : γ `⊑ γ') : (γ`‚ v) `⊑ (γ'`‚ v)
   | .z => .refl
   | .s _ => by apply lt
 end Env.Sub
@@ -165,34 +165,34 @@ end Notation
 Relaxation of table lookup in application,
 allowing an argument to match an input entry if the latter is less than the former.
 -/
-def Eval.ap_sub (d : γ ⊢ l ￬ v ⇾ w) (d' : γ ⊢ m ￬ v') (lt : v ⊑ v') : γ ⊢ l □ m ￬ w
+theorem Eval.ap_sub (d : γ ⊢ l ￬ v ⇾ w) (d' : γ ⊢ m ￬ v') (lt : v ⊑ v') : γ ⊢ l □ m ￬ w
 := d.ap <| d'.sub lt
 
 namespace Example
   open Untyped.Term (id delta omega twoC addC)
   open Eval
 
   -- `id` can be seen as a mapping table for both `⊥ ⇾ ⊥` and `(⊥ ⇾ ⊥) ⇾ (⊥ ⇾ ⊥)`.
-  def denot_id₁ : γ ⊢ id ￬ ⊥ ⇾ ⊥ := .fn .var
-  def denot_id₂ : γ ⊢ id ￬ (⊥ ⇾ ⊥) ⇾ (⊥ ⇾ ⊥) := .fn .var
+  theorem denot_id₁ : γ ⊢ id ￬ ⊥ ⇾ ⊥ := .fn .var
+  theorem denot_id₂ : γ ⊢ id ￬ (⊥ ⇾ ⊥) ⇾ (⊥ ⇾ ⊥) := .fn .var
 
   -- `id` also produces a table containing both of the previous tables.
-  def denot_id₃ : γ ⊢ id ￬ (⊥ ⇾ ⊥) ⊔ ((⊥ ⇾ ⊥) ⇾ (⊥ ⇾ ⊥)) := denot_id₁.conj denot_id₂
+  theorem denot_id₃ : γ ⊢ id ￬ (⊥ ⇾ ⊥) ⊔ ((⊥ ⇾ ⊥) ⇾ (⊥ ⇾ ⊥)) := denot_id₁.conj denot_id₂
 
   -- Oops, self application!
-  def denot_id_ap_id : `∅ ⊢ id □ id ￬ v ⇾ v := .ap (.fn .var) (.fn .var)
+  theorem denot_id_ap_id : `∅ ⊢ id □ id ￬ v ⇾ v := .ap (.fn .var) (.fn .var)
 
   -- In `def twoC f u := f (f u)`,
   -- `f`'s table must include two entries, both `u ⇾ v` and `v ⇾ w`.
   -- `twoC` then merges those two entries into one: `u ⇾ w`.
-  def denot_twoC : `∅ ⊢ twoC ￬ (u ⇾ v ⊔ v ⇾ w) ⇾ u ⇾ w := by
+  theorem denot_twoC : `∅ ⊢ twoC ￬ (u ⇾ v ⊔ v ⇾ w) ⇾ u ⇾ w := by
     apply fn; apply fn; apply ap
     · apply sub .var; exact .conjR₂ .refl
     · apply ap
       · apply sub .var; exact .conjR₁ .refl
       · exact .var
 
-  def denot_delta : `∅ ⊢ delta ￬ (v ⇾ w ⊔ v) ⇾ w := by
+  theorem denot_delta : `∅ ⊢ delta ￬ (v ⇾ w ⊔ v) ⇾ w := by
     apply fn; apply ap (v := v) <;> apply sub .var
     · exact .conjR₁ .refl
     · exact .conjR₂ .refl
@@ -202,7 +202,7 @@ namespace Example
     · exact fn (v := ⊥) .bot
     · exact .bot
 
-  def denot_omega : `∅ ⊢ omega ￬ ⊥ := .bot
+  theorem denot_omega : `∅ ⊢ omega ￬ ⊥ := .bot
 
   -- https://plfa.github.io/Denotational/#exercise-denot-plus%E1%B6%9C-practice
 
@@ -211,7 +211,7 @@ namespace Example
   · n u v = w
   · m u w = x
   -/
-  def denot_addC
+  theorem denot_addC
   : let m := u ⇾ w ⇾ x
     let n := u ⇾ v ⇾ w
     `∅ ⊢ addC ￬ m ⇾ n ⇾ u ⇾ v ⇾ x
@@ -244,18 +244,18 @@ section
   -- https://plfa.github.io/Denotational/#renaming-preserves-denotations
   variable {γ : Env Γ} {δ : Env Δ}
 
-  def ext_sub (ρ : Rename Γ Δ) (lt : γ `⊑ δ ∘ ρ)
+  theorem ext_sub (ρ : Rename Γ Δ) (lt : γ `⊑ δ ∘ ρ)
   : (γ`‚ v) `⊑ (δ`‚ v) ∘ ext ρ
   | .z => .refl
   | .s i => lt i
 
-  def ext_sub' (ρ : Rename Γ Δ) (lt : δ ∘ ρ `⊑ γ)
+  theorem ext_sub' (ρ : Rename Γ Δ) (lt : δ ∘ ρ `⊑ γ)
   : (δ`‚ v) ∘ ext ρ `⊑ (γ`‚ v)
   | .z => .refl
   | .s i => lt i
 
   /-- The result of evaluation is conserved after renaming. -/
-  def rename_pres (ρ : Rename Γ Δ) (lt : γ `⊑ δ ∘ ρ) (d : γ ⊢ m ￬ v)
+  theorem rename_pres (ρ : Rename Γ Δ) (lt : γ `⊑ δ ∘ ρ) (d : γ ⊢ m ￬ v)
   : δ ⊢ rename ρ m ￬ v
   := by induction d generalizing Δ with
   | var => apply sub .var; apply lt
@@ -270,7 +270,7 @@ section
   variable {γ δ : Env Γ}
 
   /-- The result of evaluation is conserved under a superset. -/
-  def sub_env (d : γ ⊢ m ￬ v) (lt : γ `⊑ δ) : δ ⊢ m ￬ v := by
+  theorem sub_env (d : γ ⊢ m ￬ v) (lt : γ `⊑ δ) : δ ⊢ m ￬ v := by
     convert rename_pres id lt d; exact rename_id.symm
 
   lemma up_env (d : (γ`‚ u) ⊢ m ￬ v) (lt : u ⊑ u') : (γ`‚ u') ⊢ m ￬ v := by
@@ -302,7 +302,7 @@ section
   open Eval
   open Env.Sub
 
-  def denot_church {vs} : `∅ ⊢ church n ￬ Value.church n vs := by
+  theorem denot_church {vs} : `∅ ⊢ church n ￬ Value.church n vs := by
     apply_rules [fn]; induction n with
     | zero => exact var
     | succ n r =>
@@ -336,8 +336,8 @@ namespace Value
   instance : Trans Subset Subset Included where trans := instTrans.trans
 
   variable {u v w : Value}
-  def Included.fst (s : Included (u ⊔ v) w) : u ⊆ w := s ∘ Or.inl
-  def Included.snd (s : Included (u ⊔ v) w) : v ⊆ w := s ∘ Or.inr
+  theorem Included.fst (s : Included (u ⊔ v) w) : u ⊆ w := s ∘ Or.inl
+  theorem Included.snd (s : Included (u ⊔ v) w) : v ⊆ w := s ∘ Or.inr
 end Value
 
 theorem sub_of_elem (e : u ∈ v) : u ⊑ v := by
@@ -370,8 +370,8 @@ inductive IsFn (u : Value) : Prop where | isFn (h : u = v ⇾ w)
 def AllFn (v : Value) : Prop := ∀ {u}, u ∈ v → IsFn u
 
 namespace AllFn
-  def fst (f : AllFn (u ⊔ v)) : AllFn u := f ∘ Or.inl
-  def snd (f : AllFn (u ⊔ v)) : AllFn v := f ∘ Or.inr
+  theorem fst (f : AllFn (u ⊔ v)) : AllFn u := f ∘ Or.inl
+  theorem snd (f : AllFn (u ⊔ v)) : AllFn v := f ∘ Or.inr
 end AllFn
 
 lemma not_isFn_bot : ¬ IsFn ⊥ := nofun

Plfl/Untyped/Denotational/Adequacy.lean

@@ -97,9 +97,9 @@ end
 /-- `𝔾` relates `γ` to `γ'` if the corresponding values and closures are related by `𝔼` -/
 def 𝔾 (γ : Env Γ) (γ' : ClosEnv Γ) : Prop := ∀ {i : Γ ∋ ✶}, 𝔼 (γ i) (γ' i)
 
-def 𝔾.empty : 𝔾 `∅ ∅ := nofun
+theorem 𝔾.empty : 𝔾 `∅ ∅ := nofun
 
-def 𝔾.ext (g : 𝔾 γ γ') (e : 𝔼 v c) : 𝔾 (γ`‚ v) (γ'‚' c) := by unfold 𝔾; intro
+theorem 𝔾.ext (g : 𝔾 γ γ') (e : 𝔼 v c) : 𝔾 (γ`‚ v) (γ'‚' c) := by unfold 𝔾; intro
 | .z => exact e
 | .s _ => exact g
 

Plfl/Untyped/Substitution.lean

@@ -92,13 +92,11 @@ section
     | ƛ n =>
       apply congr_arg Term.lam
       convert sub_ids
-      simp_all only
-      ext x_1 x_2 : 2
       simp_all only [exts_ids]
     | l □ m => simp only [sub_ap]; apply congr_arg₂ Term.ap <;> exact sub_ids
 
   theorem rename_id : rename (λ {_} x => x) m = m := by
-    convert sub_ids; ext; simp only [rename_subst_ren, ren]; congr
+    rw [rename_subst_ren]; exact sub_ids
 
   -- https://plfa.github.io/Substitution/#proof-of-sub-idr
   theorem seq_ids : @Eq (Γ ∋ a → Δ ⊢ a) (σ ⨟ ids) σ := by