feat: upgrade Lean version

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -1,2 +1 @@
-/build
-/lake-packages/*
+/.lake

Leansubst.lean

@@ -1,3 +1,4 @@
+-- This module serves as the root of the `Leansubst` library.
+-- Import modules here that should be built as part of the library.
 import Leansubst.Basic
-
-def hello := "world"
+import Leansubst.Examples

Leansubst/Basic.lean

@@ -1,4 +1,4 @@
-import Std.Data.Nat.Lemmas
+import Batteries.Data.Nat
 import Leansubst.Defs
 
 /-!
@@ -20,11 +20,10 @@ theorem id_applyr : applyr (.) e = e := by
       (fun e => applyr (.) e = e)
       (List.foldr (fun e etc => applyr (.) e = e ∧ etc) True)
     <;> intros <;> (try trivial)
-  case var i => rw [applyr]
   case binder e ih =>
     conv => lhs; rw [applyr]
     conv => rhs; rw [← ih]
-    congr 2; apply funext; intros k; cases k <;> rfl
+    congr 2; funext k; cases k <;> rfl
   case node x es ih =>
     induction es with
     | nil => simp only [applyr, applyr.nested]
@@ -34,7 +33,6 @@ theorem id_applyr : applyr (.) e = e := by
       congr 2
       . exact ih.left
       . specialize ih' ih.right
-        simp only [applyr, applyr.nested] at ih'
         injection ih'
 
 /-- Applying composition of renamings. -/
@@ -47,7 +45,7 @@ theorem applyr_applyr (s r) : applyr r (applyr s e) = applyr (r ∘ s) e := by
   case var i => rw [applyr, applyr, applyr]; rfl
   case binder e ih =>
     rw [applyr, applyr, applyr, ih]
-    congr 2; apply funext; intros k; cases k <;> rfl
+    congr 2; funext k; cases k <;> rfl
   case node x es ih =>
     induction es with
     | nil => simp only [applyr, applyr.nested]
@@ -57,21 +55,20 @@ theorem applyr_applyr (s r) : applyr r (applyr s e) = applyr (r ∘ s) e := by
       congr 2
       . exact ih.left _ _
       . specialize ih' ih.right
-        simp only [applyr, applyr.nested] at ih'
         injection ih'
 
 /-- `applyr` agrees with `apply` for renamings. -/
 @[simp high]
 theorem applyr_to_apply (r) : @applyr σ r = apply (.var ∘ r) := by
-  apply funext; intros e; revert r
+  funext e; revert r
   -- Induction on `e`.
   let motive := fun (e : Expr σ) => ∀ r, applyr r e = apply (.var ∘ r) e
   apply @Expr.recOn _ (fun e => motive e) (List.foldr (fun e etc => motive e ∧ etc) True)
     <;> intros <;> (try trivial) <;> intros r
   case var i => rw [applyr, apply]; rfl
   case binder e ih =>
     rw [applyr, apply, ih]
-    congr 2; apply funext; intros i
+    congr 2; funext i
     cases i with
     | zero => rfl
     | succ i => simp only [Function.comp, upr, up, cons, compr, applyr]
@@ -90,14 +87,14 @@ theorem applyr_to_apply (r) : @applyr σ r = apply (.var ∘ r) := by
 /-- `compr` agrees with `comp` for renamings. -/
 @[simp high]
 theorem compr_to_comp (s r) : @compr σ s r = comp s (.var ∘ r) := by
-  apply funext; intros i
+  funext i
   rw [compr, comp, applyr_to_apply]
 
 /-- Accessing higher entries of `upr`. -/
 theorem upr_get_high (r) : upr i r (i + j) = r j + i := by
   induction i with
   | zero => rw [Nat.zero_add]; rfl
-  | succ i ih => rw [Nat.succ_add, Nat.add_succ, ← ih]; rfl
+  | succ i ih => rw [← Nat.add_assoc, ← ih, Nat.add_assoc, Nat.add_comm 1, ← Nat.add_assoc]; rfl
 
 /-- Accessing lower entries of `upr`. -/
 theorem upr_get_low (r) (h : j < i) : (upr i r) j = j := by
@@ -119,13 +116,14 @@ theorem upr_get_low (r) (h : j < i) : (upr i r) j = j := by
         rw [ih _ (Nat.le_of_lt_succ h)]
 
 /-- Accessing higher entries of `up`. -/
-theorem up_get_high : (up i s) (i + j) = applyr (. + i) (s j) := by
+theorem up_get_high_applyr : (up i s) (i + j) = applyr (. + i) (s j) := by
   induction i with
-  | zero =>
-    rw [up, Nat.zero_add, funext Nat.add_zero, id_applyr]
-  | succ i ih =>
-    rw [up, Nat.succ_add, cons]; simp only
-    rw [compr, ih, applyr_applyr]; rfl
+  | zero => rw [up, Nat.zero_add, funext Nat.add_zero, id_applyr]
+  | succ i ih => rw [up, Nat.succ_add, cons, compr, ih, applyr_applyr]; rfl
+
+/-- Accessing higher entries of `up`. -/
+theorem up_get_high : (up i s) (i + j) = apply (shift _ i) (s j) := by
+  rw [up_get_high_applyr, applyr_to_apply]; rfl
 
 /-- Accessing lower entries of `up`. -/
 theorem up_get_low (h : j < i) : (up i s) j = .var j := by
@@ -137,26 +135,22 @@ theorem up_get_low (h : j < i) : (up i s) j = .var j := by
       subst h'; rw [up]
       cases j with
       | zero => rfl
-      | succ j =>
-        rw [cons]; simp only
-        rw [compr, ih _ (Nat.lt_succ_self _), applyr]
+      | succ j => rw [cons, compr, ih _ (Nat.lt_succ_self _), applyr]
     | inr h' =>
       rw [up]
       cases j with
       | zero => rfl
-      | succ k =>
-        rw [cons]; simp only
-        rw [compr, ih _ (Nat.le_of_lt_succ h), applyr]
+      | succ k => rw [cons, compr, ih _ (Nat.le_of_lt_succ h), applyr]
 
 /-- `upr` agrees with `up` for renamings. -/
 @[simp high]
 theorem upr_to_up (r) : .var ∘ upr i r = @up σ i (.var ∘ r) := by
-  apply funext; intros j
+  funext j
   cases Nat.lt_sum_ge j i with
   | inl h => rw [Function.comp, upr_get_low _ _ _ h, up_get_low _ _ _ h]
   | inr h =>
     have ⟨d, hd⟩ := Nat.le.dest h; subst hd; clear h
-    rw [Function.comp, upr_get_high, up_get_high, Function.comp, applyr]
+    rw [Function.comp, upr_get_high, up_get_high_applyr, Function.comp, applyr]
 
 /-- A difficult lemma for proving the `apply_apply` below... -/
 theorem gg : apply (up (i + 1) s) (applyr (upr i (. + 1)) e) = applyr (upr i (. + 1)) (apply (up i s) e) := by
@@ -171,8 +165,9 @@ theorem gg : apply (up (i + 1) s) (applyr (upr i (. + 1)) e) = applyr (upr i (.
     | inl h => rw [up_get_low _ _ _ h, applyr, upr_get_low _ _ _ h, up_get_low _ _ _ (Nat.lt_succ_of_lt h)]
     | inr h =>
       have ⟨d, hd⟩ := Nat.le.dest h; subst hd; clear h
-      rw [up_get_high, upr_get_high, Nat.add_comm (d + 1), Nat.add_comm d, ← Nat.add_assoc, up_get_high, applyr_applyr]
-      congr 1; apply funext; intros j
+      rw [up_get_high_applyr, upr_get_high, Nat.add_comm (d + 1), Nat.add_comm d, ← Nat.add_assoc]
+      rw [up_get_high_applyr, applyr_applyr]
+      congr 1; funext j
       rw [Function.comp, Nat.add_comm j i, upr_get_high, Nat.add_comm i 1, Nat.add_assoc]
   case binder e ih =>
     conv => lhs; rw [applyr, apply, up, up, ← up, upr, upr, ← upr]
@@ -189,19 +184,18 @@ theorem gg : apply (up (i + 1) s) (applyr (upr i (. + 1)) e) = applyr (upr i (.
       congr 2
       . exact ih.left _ _
       . specialize ih' ih.right
-        simp only [apply, apply.nested, applyr, applyr.nested] at ih'
         injection ih'
 
 /-!
 Instructions for the `simp` tactic.
 
-The primitive operations handled are `id`, `shift n`, `cons e s`, `up n s`, `comp s₁ s₂` `apply s e`
-and function application `s n`, where `n` are natural numbers, `s` are substitutions and `e` are
-expressions built from `var n`, `binder e` and `node _ [e]`.
+The primitive operations handled are `id`, `shift n`, `cons e s`, `up n s`, `comp s₁ s₂` and
+`apply s e`, where `n` are natural numbers, `s` are substitutions and `e` are expressions built from
+`var n`, `binder e` and `node _ [e]`.
 
-In [[1]](https://academic.oup.com/logcom/article-abstract/6/6/799/965899) it was proved that a set of
-twelve rewriting rules (so-called `σ'`-calculus in the paper) constitute a confluent and terminating rewriting
-system:
+In [[1]](https://academic.oup.com/logcom/article-abstract/6/6/799/965899) it was proved that a set
+of 12 rewriting rules (so-called `σ'`-calculus in the paper) constitute a confluent and terminating
+rewriting system:
 
 - (Id, VrId)  `apply id e`                → `e`
 - (VrCons)    `apply (cons e s) (var 0)`  → `e`
@@ -216,33 +210,31 @@ system:
 - (VrSh)      `cons (var 0) (shift 1)`    → `id`
 - (SCons)     `cons (apply s (var 0)) (comp (shift 1) s)` → `s`
 
-These rules deal with `id`, `shift 1`, `cons e s`, `comp s₁ s₂`, `apply s e` where `n`, `s` are the same,
-`e` are expressions built form `var 0`, `app e₁ e₂` and `lam e`. It was further proved in
+These rules deal with `id`, `shift 1`, `cons e s`, `comp s₁ s₂`, `apply s e` where `n`, `s` are the
+same, `e` are expressions built form `var 0`, `app e₁ e₂` and `lam e`. It was further proved in
 [[2]](https://www.ps.uni-saarland.de/Publications/documents/SchaeferEtAl_2015_Completeness.pdf)
-that these rules are also *complete* for such set of primitives (in the sense that there exists a "separating
-assignment" for two any expressions with different normal forms).
-
-> Remark: as a rewriting system, its termination is *surprisingly* difficult to establish. However this is still
-> understandable: by breaking down a simple substitution operation into many pieces, we are making the termination
-> proof strictly harder, since now we have to find some decreasing measure which orients *every* small step,
-> instead of one which just decreases from the starting position to the final position.
+that these rules are also *complete* for such set of primitives (in the sense that there exists a
+"separating assignment" for two any expressions with different normal forms).
+
+> Remark: as a rewriting system, its termination is *surprisingly* difficult to establish. However,
+> this is understandable: by breaking down a simple substitution operation into many pieces, we are
+> making the termination proof strictly harder, since now we have to find some decreasing measure
+> which orients *every* small step, instead of one which just decreases from the starting position
+> to the final position.
 > [[2]](https://www.ps.uni-saarland.de/Publications/documents/SchaeferEtAl_2015_Completeness.pdf)
 > has suggested using a proper *algorithm* instead of *rewriting* to avoid such difficulty.
 
-In this project I choose to normalise `upr`, `applyr`, `compr`, function application (*), `pointwise` and `var n`
-(to `apply (shift n) (var 0)`) first; the remaining extensions which need to be handled are
-`shift n` and `up n s`. The handling has to be more-or-less heuristic:
-
-- For `up n s`, the strategy is to merge repeated applications first, then rewrite `n` (a sum of natural numbers)
-  using `[Nat.add_succ, Nat.succ_add]` so that all `succ`s are moved to the outermost, and then I can expand
-  the definition of `up`.
-- For `shift n`, again repeated `apply (shift n)` are merged first, then `n` is rewritten so that the `succ`s
-  bubble out. Now we cannot naively expand `shift (succ n)`: sometimes we need `comp (shift 1) (shift n)`
-  (VrSh, SCons), but sometimes we need `comp (shift n) (shift 1)` (ShCons). I preferred the first expansion, and
-  used a generalised rule for ShCons.
-
-(*) Expansion of function application must be done manually for now
-    (`simp` will stack overflow, and `rw` errors with "pattern is a metavariable")...
+In this project I choose to normalise `upr`, `applyr`, `compr`, `pointwise` and `var n` (to
+`apply (shift n) (var 0)`) first; the remaining extensions which need to be handled are `shift n`
+and `up n s`. The handling has to be more-or-less heuristic:
+
+- For `up n s`, the strategy is to merge repeated applications first, then rewrite `n` (a sum of
+  natural numbers) using `[Nat.add_succ, Nat.succ_add]` so that all `succ`s are moved to the
+  outermost, and then I can expand the definition of `up`.
+- For `shift n`, again repeated `apply (shift n)` are merged first, then `n` is rewritten so that
+  the `succ`s bubble out. Now we cannot naively expand `shift (succ n)`: sometimes we need
+  `comp (shift 1) (shift n)` (VrSh, SCons), but sometimes we need `comp (shift n) (shift 1)`
+  (ShCons). I preferred the first expansion, and used a generalised rule for ShCons.
 -/
 
 -- To prevent infinite loops.
@@ -265,18 +257,18 @@ theorem var_expand : .var n = apply (shift σ n) (var0 σ) := by
 /-- Normalise `shift 0` to `id`. -/
 @[simp high]
 theorem shift_zero : shift σ 0 = id σ := by
-  apply funext; intros i
+  funext i
   rw [id, shift]; rfl
 
 /-- Merge adjacent `shift` (we can then move `succ` out). -/
 @[simp high]
 theorem shift_comp_shift : comp (shift σ n) (shift σ m) = shift σ (n + m) := by
-  apply funext; intros i; rw [shift, comp, shift, apply, shift, Nat.add_assoc]
+  funext i; rw [shift, comp, shift, apply, shift, Nat.add_assoc]
 
 /-- Expand `shift (n + 1)`. This will not cause infinite loop, but should have lower priority. -/
 @[simp low]
 theorem shift_succ : shift σ (n + 1) = comp (shift1 σ) (shift σ n) := by
-  apply funext; intros i
+  funext i
   rw [comp, shift1, shift, shift, apply, shift, Nat.add_comm n 1, Nat.add_assoc]
 
 /-- Expand `up 0` to nothing. -/
@@ -302,11 +294,10 @@ theorem id_apply : apply (id σ) e = e := by
       (fun e => apply (id σ) e = e)
       (List.foldr (fun e etc => apply (id σ) e = e ∧ etc) True)
     <;> intros <;> (try trivial)
-  case var i => rw [apply]; rfl
   case binder e ih =>
     conv => lhs; rw [apply]
     conv => rhs; rw [← ih]
-    congr 2; apply funext; intros k
+    congr 2; funext k
     cases k with
     | zero => rfl
     | succ => simp only [cons, id, compr, applyr, up]
@@ -319,7 +310,6 @@ theorem id_apply : apply (id σ) e = e := by
       congr 2
       . exact ih.left
       . specialize ih' ih.right
-        simp only [apply, apply.nested] at ih'
         injection ih'
 
 @[simp high]
@@ -345,7 +335,7 @@ theorem apply_apply : apply t (apply s e) = apply (comp s t) e := by
   case var i => rw [apply, apply]; rfl
   case binder e ih =>
     rw [apply, apply, apply, ih]
-    congr 2; apply funext; intros i
+    congr 2; funext i
     cases i with
     | zero => rfl
     | succ i => have h := gg t 0; rw [up, upr] at h; exact h (s i)
@@ -358,36 +348,35 @@ theorem apply_apply : apply t (apply s e) = apply (comp s t) e := by
       congr 2
       . exact ih.left _ _
       . specialize ih' ih.right
-        simp only [apply, apply.nested] at ih'
         injection ih'
 
 @[simp high]
 theorem id_comp : comp (id σ) s = s := by
-  apply funext; intros i; rw [comp, id, apply]
+  funext i; rw [comp, id, apply]
 
 @[simp high]
 theorem comp_id : comp s (id σ) = s := by
-  apply funext; intros i; rw [comp, id_apply]
+  funext i; rw [comp, id_apply]
 
 @[simp high]
 theorem shift_comp_cons : comp (shift1 σ) (cons e s) = s := by
-  apply funext; intros i; rw [comp, shift1, shift, apply]; rfl
+  funext i; rw [comp, shift1, shift, apply]; rfl
 
 @[simp high]
 theorem cons_comp : comp (cons e s) t = cons (apply t e) (comp s t) := by
-  apply funext; intros i; rw [comp]; cases i <;> rfl
+  funext i; rw [comp]; cases i <;> rfl
 
 @[simp high]
 theorem comp_assoc : comp (comp s t) u = comp s (comp t u) := by
-  apply funext; intros i; simp only [comp, apply_apply]
+  funext i; simp only [comp, apply_apply]
 
 @[simp high]
 theorem zero_cons_shift : cons (var0 σ) (shift1 σ) = id σ := by
-  apply funext; intros i; cases i <;> rfl
+  funext i; cases i <;> rfl
 
 @[simp high]
 theorem apply_zero_cons_shift_comp : cons (apply s (var0 σ)) (comp (shift1 σ) s) = s := by
-  apply funext; intros i; cases i <;> rfl
+  funext i; cases i <;> rfl
 
 /-- Generalises `shift_comp_cons`. -/
 @[simp]

Leansubst/Defs.lean

@@ -1,6 +1,3 @@
-import Std.Data.Nat.Basic
-import Std.Tactic.Basic
-
 /-!
 This file contains definitions of: