refactor: 1. split Plfl/Init to 3 files, 2. update version to v4.31.0

Plfl.lean

@@ -1,6 +1,5 @@
 module
 prelude
-public import Plfl.Init
 public import Plfl.Lambda
 public import Plfl.Lambda.Properties
 public import Plfl.DeBruijn

Plfl/DeBruijn.lean

@@ -2,7 +2,7 @@ module
 
 -- https://plfa.github.io/DeBruijn/
 
-import Plfl.Init
+import Plfl.Init.Tactics
 import Batteries.Tactic.Init
 import Mathlib.Data.Nat.Notation
 import Mathlib.Tactic.Basic

Plfl/Init.lean → Plfl/Init/Decidable'.lean

@@ -5,12 +5,6 @@ public import Mathlib.Logic.IsEmpty.Basic
 
 @[expose] public section
 
-/--
-`is_empty` converts `IsEmpty α` to `α → False`.
--/
-syntax "is_empty" : tactic
-macro_rules | `(tactic| is_empty) => `(tactic| apply Function.isEmpty (β := False))
-
 /--
 `Decidable'` is like `Decidable`, but allows arbitrary sorts.
 -/
@@ -26,9 +20,3 @@ instance [Repr α] : Repr (Decidable' α) where
   reprPrec da n := match da with
   | .inr a => ".inr " ++ reprPrec a n
   | .inl _ => ".inl _"
-
-theorem congr_arg₃
-(f : α → β → γ → δ) {x x' : α} {y y' : β} {z z' : γ}
-(hx : x = x') (hy : y = y') (hz : z = z')
-: f x y z = f x' y' z'
-:= by subst hx hy hz; rfl

Plfl/Init/Lemmas.lean

@@ -0,0 +1,9 @@
+module
+
+public section
+
+theorem congr_arg₃
+  (f : α → β → γ → δ) {x x' : α} {y y' : β} {z z' : γ}
+  (hx : x = x') (hy : y = y') (hz : z = z')
+  : f x y z = f x' y' z'
+  := by subst hx hy hz; rfl

Plfl/Init/Tactics.lean

@@ -0,0 +1,8 @@
+module
+public import Mathlib.Logic.IsEmpty.Defs
+
+/--
+`is_empty` converts `IsEmpty α` to `α → False`.
+-/
+syntax "is_empty" : tactic
+macro_rules | `(tactic| is_empty) => `(tactic| apply Function.isEmpty (β := False))

Plfl/Lambda.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Lambda/
 
-public import Plfl.Init
 import Mathlib.Data.Nat.Notation
 import Mathlib.Tactic.ApplyFun
 public import Mathlib.Logic.Embedding.Basic
@@ -214,7 +213,7 @@ namespace Term.Reduce
     apply_fun Clos'.toClos at h
     rwa [←toClos'_left_inv (x := a), ←toClos'_left_inv (x := b)]
 
-  instance Clos.embedsInClos' : (m —↠ n) ↪ (m —↠' n) where
+  def Clos.embedsInClos' : (m —↠ n) ↪ (m —↠' n) where
     toFun := toClos'
     inj' := toClos'_inj
 end Term.Reduce

Plfl/Lambda/Properties.lean

@@ -2,7 +2,7 @@ module
 
 -- https://plfa.github.io/Properties/
 
-public meta import Plfl.Init
+import Plfl.Init.Tactics
 public meta import Plfl.Lambda
 import Plfl.Lambda
 import Mathlib.Tactic.Basic
@@ -78,7 +78,7 @@ namespace Canonical
   /--
   The Canonical forms are exactly the well-typed values.
   -/
-  instance : Canonical v t ≃ (∅ ⊢ v ⦂ t) × Value v where
+  def equivWellTyped : Canonical v t ≃ (∅ ⊢ v ⦂ t) × Value v where
     toFun := wellTyped
     invFun := wellTypedInv
     left_inv := wellTyped_left_inv
@@ -162,7 +162,7 @@ namespace Progress
   @[simp] def toProgress' : Progress m → Progress' m | step r => inr ⟨_, r⟩ | done v => inl v
   @[simp] def fromProgress' : Progress' m → Progress m | inl v => done v | inr ⟨_, r⟩ => step r
 
-  instance : Progress m ≃ Progress' m where
+  def equivProgress' : Progress m ≃ Progress' m where
     toFun := toProgress'
     invFun := fromProgress'
     left_inv := by intro x; cases x <;> simp_all only [fromProgress', toProgress']

Plfl/More.lean

@@ -2,7 +2,7 @@ module
 
 -- https://plfa.github.io/More/
 
-public import Plfl.Init
+import Plfl.Init.Tactics
 import Batteries.Tactic.Init
 public import Mathlib.Data.Matrix.Mul
 

Plfl/More/Bisimulation.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Bisimulation/
 
-public import Plfl.Init
 public import Plfl.More
 import Mathlib.Tactic.Basic
 

Plfl/More/DoubleSubst.lean

@@ -4,7 +4,8 @@ module
 
 -- Adapted from <https://github.com/kaa1el/plfa_solution/blob/c5869a34bc4cac56cf970e0fe38874b62bd2dafc/src/plfa/demo/DoubleSubstitutionDeBruijn.agda>.
 
-public import Plfl.Init
+public import Plfl.Init.Tactics
+public import Plfl.Init.Lemmas
 public import Plfl.More
 
 @[expose] public section

Plfl/More/Inference.lean

@@ -2,7 +2,9 @@ module
 
 -- https://plfa.github.io/Inference/
 
-public meta import Plfl.Init
+import Plfl.Init.Tactics
+meta import Plfl.Init.Decidable'
+public import Plfl.Init.Decidable'
 public import Plfl.More
 
 @[expose] public section

Plfl/Untyped.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Untyped/
 
-public import Plfl.Init
 import Mathlib.Data.Nat.Notation
 public import Mathlib.Logic.Equiv.Defs
 import Mathlib.Tactic.Basic
@@ -23,7 +22,7 @@ end Notation
 open Notation
 
 -- https://plfa.github.io/Untyped/#exercise-type-practice
-instance : Ty ≃ Unit where
+def equivTyUnit : Ty ≃ Unit where
   toFun _ := ()
   invFun _ := ✶
   left_inv _ := by simp only
@@ -50,7 +49,7 @@ namespace Notation
 end Notation
 
 -- https://plfa.github.io/Untyped/#exercise-context%E2%84%95-practice
-instance Context.equiv_nat : Context ≃ ℕ where
+def Context.equiv_nat : Context ≃ ℕ where
   toFun := List.length
   invFun := (List.replicate · (✶))
   left_inv := left_inv

Plfl/Untyped/BigStep.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/BigStep/
 
-public import Plfl.Init
 public import Plfl.Untyped
 public import Plfl.Untyped.Substitution
 import Mathlib.Logic.Lemmas

Plfl/Untyped/Confluence.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Confluence/
 
-public import Plfl.Init
 public import Plfl.Untyped
 public import Plfl.Untyped.Substitution
 
@@ -79,7 +78,7 @@ namespace PReduce
       _ —↠ l' □ m' := Untyped.Reduce.ap_congr₂ (toReduceClos rm)
 end PReduce
 
-instance instNonemptyPReduceReduceClos : (m ⇛* n) ≃ (m —↠ n) where
+def equivPReduceClosReduceClos : (m ⇛* n) ≃ (m —↠ n) where
   toFun := toFun
   invFun := invFun
   left_inv _ := by simp only
@@ -153,14 +152,14 @@ namespace Notation
 end Notation
 
 theorem par_triangle {m n : Γ ⊢ a} : (m ⇛ n) → (n ⇛ m⁺) := open PReduce in by
-intro
-| .var => exact .var
-| .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)
-  | ƛ _  => have .lamζ pl := pl; exact lamβ (par_triangle pl) (par_triangle pm)
+  intro p; match p with
+  | .var => exact .var
+  | .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)
+    | ƛ _ => match pl with | .lamζ pl => exact lamβ (par_triangle pl) (par_triangle pm)
 
 theorem par_diamond {m n n' : Γ ⊢ a} (p : m ⇛ n) (p' : m ⇛ n')
 : ∃ (l : Γ ⊢ a), (n ⇛ l) ∧ (n' ⇛ l)
@@ -189,6 +188,6 @@ theorem par_confluence {l m m' : Γ ⊢ a} (lm : l ⇛* m) (lm' : l ⇛* m')
 theorem confluence {l m m' : Γ ⊢ a} (lm : l —↠ m) (lm' : l —↠ m')
 : ∃ (n : Γ ⊢ a), (m —↠ n) ∧ (m' —↠ n)
 := by
-  let equiv := @instNonemptyPReduceReduceClos Γ a
+  let equiv := @equivPReduceClosReduceClos Γ a
   have ⟨n, mn, m'n⟩:= par_confluence (equiv.invFun lm) (equiv.invFun lm')
   exists n; exact ⟨equiv.toFun mn, equiv.toFun m'n⟩

Plfl/Untyped/Denotational.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Denotational/
 
-public import Plfl.Init
 public import Plfl.Untyped
 public import Plfl.Untyped.Substitution
 import Mathlib.Data.Nat.Notation

Plfl/Untyped/Denotational/Adequacy.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Adequacy/
 
-public import Plfl.Init
 public import Plfl.Untyped.BigStep
 public import Plfl.Untyped.Denotational.Soundness
 public import Mathlib.Tactic

Plfl/Untyped/Denotational/Compositional.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Compositional/
 
-public import Plfl.Init
 public import Plfl.Untyped.Denotational
 public import Mathlib.Order.BooleanAlgebra.Defs
 

Plfl/Untyped/Denotational/ContextualEquivalence.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/ContextualEquivalence/
 
-public import Plfl.Init
 public import Plfl.Untyped.Denotational.Adequacy
 
 @[expose] public section

Plfl/Untyped/Denotational/Soundness.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Soundness/
 
-public import Plfl.Init
 public import Plfl.Untyped.Denotational.Compositional
 
 @[expose] public section
@@ -118,16 +117,16 @@ theorem subst_reflect {σ : Subst Γ Δ} (d : δ ⊢ l ￬ v) (h : ⟪σ⟫ m =
   induction d generalizing Γ with
   | bot => exists ⊥; exact ⟨subst_bot, .bot⟩
   | var => cases m with try contradiction
-    | var j => apply subst_reflect_var; convert Eval.var
+    | var j => apply subst_reflect_var; convert Eval.var using 1; exact h
   | ap d d' ih ih' => rename_i l' _ _ m'; cases m with try contradiction
-    | var => apply subst_reflect_var; convert d.ap d'
+    | var => apply subst_reflect_var; convert d.ap d' using 1; exact h
     | ap =>
       injection h; rename_i h h'
       let ⟨γ, dγ, dm⟩ := ih h; let ⟨γ', dγ', dm'⟩ := ih' h'; exists γ ⊔ γ'; constructor
       · exact subst_conj dγ dγ'
       · exact (sub_env dm <| Env.Sub.conjR₁ γ γ').ap (sub_env dm' <| Env.Sub.conjR₂ γ γ')
   | fn d ih => cases m with try contradiction
-    | var => apply subst_reflect_var; convert d.fn
+    | var => apply subst_reflect_var; convert d.fn using 1; exact h
     | lam =>
       injection h; rename_i h; let ⟨γ, dγ, dm⟩ := ih h; exists γ.init; constructor
       · intro i; exact rename_shift_reflect <| dγ i.s

Plfl/Untyped/Substitution.lean

@@ -2,7 +2,6 @@ module
 
 -- https://plfa.github.io/Substitution/#plfa_plfa-part2-Substitution-2341
 
-public import Plfl.Init
 public import Plfl.Untyped
 import Batteries.Tactic.Init
 import Batteries.Logic
@@ -179,7 +178,9 @@ section
     · 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
+      have : (fun {a} => subst₁σ m ∘ Lookup.s) = (fun {a} => @ids Δ a) := by
+        funext _ i; rfl
+      simp only [this, sub_ids]
 
   variable {n : Γ‚ ✶ ⊢ ✶} {m : Γ ⊢ ✶}