From 60de6c7fc6d6f65a8669dedc34be15feda51e1b8 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Sat, 13 Jan 2024 15:12:51 +1100
Subject: [PATCH] chore: adaptations for leanprover/lean4#3040 (changes to
 termination hints) (#95)

---
 AesopTest/SeqCalcProver.lean | 17 ++++++++---------
 lake-manifest.json           |  4 ++--
 lakefile.lean                |  2 +-
 lean-toolchain               |  2 +-
 4 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/AesopTest/SeqCalcProver.lean b/AesopTest/SeqCalcProver.lean
index 094b9581..b51f2d97 100644
--- a/AesopTest/SeqCalcProver.lean
+++ b/AesopTest/SeqCalcProver.lean
@@ -98,7 +98,6 @@ theorem mem (P : α → Prop) (xs : List α)
   case mpr =>
     intro ⟨a, Pa, Ea⟩
     induction Ea <;> aesop
-termination_by _ => List.length xs
 
 theorem map (P : β → Prop) (f : α → β) (xs : List α)
   : Any P (xs.map f) ↔ Any (fun x => P (f x)) xs := by
@@ -241,8 +240,8 @@ def Cal (l r : List Φ) : (Γ Δ : List (Form Φ)) → Prop
   | Γ, ♩n :: Δ => Cal l (n :: r) Γ Δ
   | φ ⇒ ψ :: Γ, [] => Cal l r Γ [φ] ∧ Cal l r (ψ :: Γ) []
   | Γ, φ ⇒ ψ :: Δ => Cal l r (φ :: Γ) (ψ :: Δ)
-termination_by _ Γ Δ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
-decreasing_by simp_wf <;> simp_arith
+termination_by Γ Δ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
+decreasing_by all_goals simp_wf <;> simp_arith
 
 instance Cal.instDecidable [DecidableEq Φ] (l r : List Φ) (Γ Δ : List (Form Φ))
   : Decidable (Cal l r Γ Δ) := by
@@ -265,8 +264,8 @@ instance Cal.instDecidable [DecidableEq Φ] (l r : List Φ) (Γ Δ : List (Form
   | Γ, φ ⇒ ψ :: Δ =>
     have ih : Decidable (Cal l r (φ :: Γ) (ψ :: Δ)) := instDecidable l r (φ :: Γ) (ψ :: Δ)
     aesop
-termination_by _ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
-decreasing_by simp_wf <;> simp_arith
+termination_by sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
+decreasing_by all_goals simp_wf <;> simp_arith
 
 abbrev Prove (φ : Form Φ) : Prop := Cal [] [] [] [φ]
 
@@ -385,8 +384,8 @@ theorem Cal_sound_complete [DecidableEq Φ]
         have AllΓ : All (Val i) (Γ ++ l.map (♩·)) := by simp_all
         have AnyφψΔ : Any (Val i) (φ ⇒ ψ :: Δ ++ r.map (♩·)) := h i dec AllΓ
         simp_all
-termination_by _ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
-decreasing_by simp_wf <;> simp_arith
+termination_by sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
+decreasing_by all_goals simp_wf <;> simp_arith
 
 theorem Prove_sound_complete [DecidableEq Φ] (φ : Form Φ)
   : Prove φ ↔ Valid φ := by
@@ -477,8 +476,8 @@ theorem Cal_Proof [DecidableEq Φ]
     simp at h
     have ih : Proof' l r (φ :: Γ) (ψ :: Δ) := Cal_Proof l r (φ :: Γ) (ψ :: Δ) h
     aesop
-termination_by _ => sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
-decreasing_by simp_wf <;> simp_arith
+termination_by sum (Γ.map sizeOf) + sum (Δ.map sizeOf)
+decreasing_by all_goals simp_wf <;> simp_arith
 
 theorem Proof_sound_complete [DecidableEq Φ] (φ : Form Φ)
   : Proof [] [φ] ↔ Valid φ := by
diff --git a/lake-manifest.json b/lake-manifest.json
index 30030b64..0622f444 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "5ce12021fcbe7d125aa0881f4e61585def9dec1a",
+   "rev": "27369b95662a33f4d89d1c70a230dd695ddc1b6a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "bump/v4.6.0",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "aesop",
diff --git a/lakefile.lean b/lakefile.lean
index c2ae1065..c2eecf11 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,4 +13,4 @@ lean_lib AesopTest {
   globs := #[.submodules "AesopTest"]
 }
 
-require std from git "https://github.com/leanprover/std4" @ "bump/v4.6.0"
+require std from git "https://github.com/leanprover/std4" @ "nightly-testing"
diff --git a/lean-toolchain b/lean-toolchain
index a1cc64c3..4db8563e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-10
+leanprover/lean4:nightly-2024-01-12