chore: move to v4.6.0-rc1, merging adaptations (#100)

Co-authored-by: Jannis Limperg <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Leonardo de Moura <[email protected]>
leanprover-community · Feb 2, 2024 · 6beed82 · 6beed82
1 parent cebd10b
commit 6beed82
Show file tree

Hide file tree

Showing 10 changed files with 41 additions and 29 deletions.
diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean
@@ -49,7 +49,6 @@ def getImmediatePremises (name : Name) (type : Expr) (md : TransparencyMode) :
       let mut unseen := immediate.sortAndDeduplicate (ord := ⟨Name.quickCmp⟩)
       let mut result := #[]
       for h : i in [:args.size] do
-        have h : i < args.size := by simp_all [Membership.mem]
         let argName := (← args[i].fvarId!.getDecl).userName
         if immediate.contains argName then
           result := result.push i

diff --git a/Aesop/Index.lean b/Aesop/Index.lean
@@ -14,8 +14,8 @@ open Lean.Meta
 namespace Aesop
 
 structure Index (α : Type) [BEq α] [Hashable α] where
-  byTarget : DiscrTree α 
-  byHyp : DiscrTree α 
+  byTarget : DiscrTree α
+  byHyp : DiscrTree α
   unindexed : PHashSet α
   deriving Inhabited
 
@@ -56,9 +56,9 @@ partial def add (r : α) (imode : IndexingMode) (ri : Index α) :
   | IndexingMode.unindexed =>
     { ri with unindexed := ri.unindexed.insert r }
   | IndexingMode.target keys =>
-    { ri with byTarget := ri.byTarget.insertCore keys r discrTreeConfig }
+    { ri with byTarget := ri.byTarget.insertCore keys r }
   | IndexingMode.hyps keys =>
-    { ri with byHyp := ri.byHyp.insertCore keys r discrTreeConfig }
+    { ri with byHyp := ri.byHyp.insertCore keys r }
   | IndexingMode.or imodes =>
     imodes.foldl (init := ri) λ ri imode =>
       ri.add r imode

diff --git a/Aesop/Search/Expansion/Simp.lean b/Aesop/Search/Expansion/Simp.lean
@@ -9,6 +9,7 @@ import Aesop.Script
 import Aesop.RuleSet
 
 open Lean Lean.Meta
+open Lean.Elab.Tactic (mkSimpOnly)
 open Simp (UsedSimps)
 
 namespace Aesop
@@ -49,13 +50,15 @@ def mkNormSimpOnlySyntax (inGoal : MVarId) (normSimpUseHyps : Bool)
   return ⟨stx⟩
 
 def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
+    (simprocs : Simp.SimprocsArray)
     (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : UsedSimps := {}) : MetaM SimpResult := do
   let mvarIdOld := mvarId
   let ctx := { ctx with config.failIfUnchanged := false }
   let (result, usedSimps) ←
-    Meta.simpGoal mvarId ctx discharge? simplifyTarget fvarIdsToSimp usedSimps
+    Meta.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
+      usedSimps
   if let some (_, mvarId) := result then
     if mvarId == mvarIdOld then
       return .unchanged mvarId
@@ -65,6 +68,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
     return .solved usedSimps
 
 def simpGoalWithAllHypotheses (mvarId : MVarId) (ctx : Simp.Context)
+    (simprocs : Simp.SimprocsArray := {})
     (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (usedSimps : UsedSimps := {}) :
     MetaM SimpResult :=
@@ -75,12 +79,14 @@ def simpGoalWithAllHypotheses (mvarId : MVarId) (ctx : Simp.Context)
       if ldecl.isImplementationDetail then
         continue
       fvarIdsToSimp := fvarIdsToSimp.push ldecl.fvarId
-    Aesop.simpGoal mvarId ctx discharge? simplifyTarget fvarIdsToSimp usedSimps
+    Aesop.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
+      usedSimps
 
 def simpAll (mvarId : MVarId) (ctx : Simp.Context)
+    (simprocs : Simp.SimprocsArray := {})
     (usedSimps : UsedSimps := {}) : MetaM SimpResult := do
   let ctx := { ctx with config.failIfUnchanged := false }
-  match ← Lean.Meta.simpAll mvarId ctx usedSimps with
+  match ← Lean.Meta.simpAll mvarId ctx simprocs usedSimps with
   | (none, usedSimps) => return .solved usedSimps
   | (some mvarIdNew, usedSimps) =>
     if mvarIdNew == mvarId then

diff --git a/Aesop/Search/SearchM.lean b/Aesop/Search/SearchM.lean
@@ -82,9 +82,10 @@ protected def run (ruleSet : RuleSet) (options : Aesop.Options')
     MetaM (α × State Q × Tree × Profile) := do
   let t ← mkInitialTree goal
   let normSimpContext := {
-    (← Simp.Context.mkDefault) with
     config := simpConfig
+    maxDischargeDepth := UInt32.ofNatTruncate simpConfig.maxDischargeDepth
     simpTheorems := ruleSet.globalNormSimpTheorems
+    congrTheorems := ← getSimpCongrTheorems
     configStx? := simpConfigStx?
     enabled := options.enableSimp
     useHyps := options.useSimpAll

diff --git a/Aesop/Util/Tactic.lean b/Aesop/Util/Tactic.lean
@@ -72,25 +72,24 @@ where
   -- is slow but correct.
   pre (e : Expr) : StateRefT (HashSet Name) SimpM Simp.Step := do
     let some decl := e.getAppFn'.constName?
-      | return .visit { expr := e }
+      | return .continue
     match unfold? decl with
     | none =>
-      return .visit { expr := e }
+      return .continue
     | some none =>
       if let some e' ← delta? e (λ n => n == decl) then
         modify (·.insert decl)
         return .done { expr := e' }
       else
-        return .visit { expr := e }
+        return .continue
     | some (some unfoldThm) =>
       let result? ← withReducible <|
         Simp.tryTheorem? e
           { origin := .decl unfoldThm
             proof := mkConst unfoldThm
             rfl := ← isRflTheorem unfoldThm }
-          (fun _ => return none)
       match result? with
-      | none   => return .visit { expr := e }
+      | none   => return .continue
       | some r =>
         modify (·.insert decl)
         match (← reduceMatcher? r.expr) with

diff --git a/AesopTest/List.lean b/AesopTest/List.lean
@@ -16,7 +16,6 @@ set_option aesop.check.script true
 -- use `sorry` because it generates lots of warnings.
 axiom ADMIT : ∀ {α : Sort _}, α
 
-@[aesop safe cases]
 class IsEmpty (α : Sort _) where
   false : α → False
 

diff --git a/AesopTest/NormSimp.lean b/AesopTest/NormSimp.lean
@@ -23,11 +23,20 @@ example (h : (α ∧ β) ∨ γ) : α ∨ γ := by
 
 -- This test checks that the norm simp config is passed around properly.
 example {α β : Prop} (ha : α) (h : α → β) : β := by
-  fail_if_success aesop (rule_sets [-builtin,-default])
-    (simp_config := { maxDischargeDepth := 0 })
-    (config := { terminal := true })
+  fail_if_success
+    aesop (rule_sets [-builtin,-default])
+      (simp_config := { maxDischargeDepth := 0 })
+      (config := { terminal := true })
   aesop (rule_sets [-builtin,-default])
 
+-- Ditto.
+example : true && false = false := by
+  fail_if_success aesop
+    (rule_sets [-default,-builtin])
+    (config := { terminal := true })
+    (simp_config := { decide := false })
+  aesop (rule_sets [-default,-builtin]) (simp_config := { decide := true })
+
 -- We can use the `useHyps` config option to switch between `simp_all` and
 -- `simp at *`.
 example {α : Prop} (ha : α) : α := by

diff --git 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
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.5.0
		leanprover/lean4:v4.6.0-rc1