bump to leanprover/lean4:v4.3.0-rc1

SciLean/Core/FunctionTransformations/FwdFDeriv.lean

@@ -59,7 +59,7 @@ theorem comp_rule
       let zdz := fwdFDeriv K f ydy.1 ydy.2 
       zdz :=
 by
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 theorem let_rule 
@@ -72,7 +72,7 @@ theorem let_rule
       let zdz := fwdFDeriv K (fun (xy : X×Y) => f xy.1 xy.2) (x,ydy.1) (dx,ydy.2)
       zdz :=
 by
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 theorem pi_rule
@@ -95,7 +95,7 @@ theorem comp_rule_at
       let zdz := fwdFDeriv K f ydy.1 ydy.2 
       zdz :=
 by
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 theorem let_rule_at
@@ -108,7 +108,7 @@ theorem let_rule_at
       let zdz := fwdFDeriv K (fun (xy : X×Y) => f xy.1 xy.2) (x,ydy.1) (dx,ydy.2)
       zdz :=
 by
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 theorem pi_rule_at  
@@ -408,7 +408,7 @@ theorem HMul.hMul.arg_a0a1.fwdFDeriv_rule_at
       let zdz := (fwdFDeriv K g x dx)
       (ydy.1 * zdz.1, zdz.2 * ydy.1 + ydy.2 * zdz.1) :=
 by 
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 @[ftrans]
@@ -423,7 +423,7 @@ theorem HMul.hMul.arg_a0a1.fwdFDeriv_rule
       let zdz := (fwdFDeriv K g x dx)
       (ydy.1 * zdz.1, zdz.2 * ydy.1 + ydy.2 * zdz.1) :=
 by 
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 -- HSMul.hSMul -------------------------------------------------------------------
@@ -440,7 +440,7 @@ theorem HSMul.hSMul.arg_a0a1.fwdFDeriv_rule_at
       let zdz := (fwdFDeriv K g x dx)
       (ydy.1 • zdz.1, ydy.1 • zdz.2 + ydy.2 • zdz.1) :=
 by 
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 @[ftrans]
@@ -454,7 +454,7 @@ theorem HSMul.hSMul.arg_a0a1.fwdFDeriv_rule
       let zdz := (fwdFDeriv K g x dx)
       (ydy.1 • zdz.1, ydy.1 • zdz.2 + ydy.2 • zdz.1) :=
 by 
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 -- HDiv.hDiv -------------------------------------------------------------------
@@ -472,7 +472,7 @@ theorem HDiv.hDiv.arg_a0a1.fwdFDeriv_rule_at
       let zdz := (fwdFDeriv R g x dx)
       (ydy.1 / zdz.1, (ydy.2 * zdz.1 - ydy.1 * zdz.2) / zdz.1^2) :=
 by 
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 @[ftrans]
@@ -487,7 +487,7 @@ theorem HDiv.hDiv.arg_a0a1.fwdFDeriv_rule
       let zdz := (fwdFDeriv R g x dx)
       (ydy.1 / zdz.1, (ydy.2 * zdz.1 - ydy.1 * zdz.2) / zdz.1^2) :=
 by 
-  unfold fwdFDeriv; ftrans
+  unfold fwdFDeriv; ftrans; simp
 
 
 -- HPow.hPow -------------------------------------------------------------------

SciLean/Core/FunctionTransformations/RevCDeriv.lean

@@ -150,6 +150,8 @@ by
   have ⟨_,_⟩ := hg
   unfold revCDeriv
   funext _; ftrans; ftrans
+  rfl
+
 
 theorem comp_rule'
   (f : Y → Z) (g : X → Y) 
@@ -183,7 +185,7 @@ by
   have ⟨_,_⟩ := hf
   have ⟨_,_⟩ := hg
   unfold revCDeriv
-  funext _; ftrans; ftrans
+  funext _; ftrans; ftrans; rfl
 
 
 theorem let_rule'

SciLean/Core/FunctionTransformations/RevFDeriv.lean

@@ -62,7 +62,7 @@ by
            =
            fun _ => fun dx =>L[K] dx i := sorry_proof -- by apply fderiv.proj_rule 
   rw[h]
-  dsimp; ftrans only; simp
+  dsimp; ftrans only; sorry_proof -- do not understand why simp does not solve this
 variable {E}
 
 theorem comp_rule 

SciLean/Core/Monads/Id.lean

@@ -31,7 +31,7 @@ instance : RevDerivMonad K Id Id where
   revDerivM f := revCDeriv K f
   HasAdjDiffM f := HasAdjDiff K f
   revDerivM_pure f := by simp[pure]
-  revDerivM_bind := by intros; simp; ftrans
+  revDerivM_bind := by intros; simp; ftrans; rfl
   revDerivM_pair y := by intros; simp; ftrans
   HasAdjDiffM_pure := by simp[pure]
   HasAdjDiffM_bind := by simp[bind]; fprop

SciLean/Tactic/LSimp2/Elab.lean

@@ -32,9 +32,12 @@ def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
   let env ← getEnv
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
-    | .decl declName => -- global definitions in the environment
-      if env.contains declName && !simpOnlyBuiltins.contains declName then
-        args := args.push (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident))
+    | .decl declName inv => -- global definitions in the environment
+      if env.contains declName && (inv || !simpOnlyBuiltins.contains declName) then
+        args := args.push (if inv then
+          (← `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident))
+        else
+          (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident)))
     | .fvar fvarId => -- local hypotheses in the context
       if let some ldecl := lctx.find? fvarId then
         localsOrStar := localsOrStar.bind fun locals =>

SciLean/Tactic/LSimp2/Main.lean

@@ -430,7 +430,7 @@ private def mkLetCongrEq (h₁ h₂ : Expr) : MetaM Expr :=
 
 partial def simp (e : Expr) : M Result := withIncRecDepth do
   withTraceNode `lsimp (fun _ => do pure s!"lsimp") do
-  checkMaxHeartbeats "simp"
+  checkSystem "simp"
   let cfg ← Simp.getConfig
   if (← isProof e) then
     return { expr := e }

lake-manifest.json

@@ -4,49 +4,49 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "a5516f580a31bf7ec20be84cc4fe50824cd3e35a",
+    "rev": "9e03d9ced7ba4d2bf95f9ed7da0e3a3ffbc81d9e",
     "opts": {},
     "name": "mathlib",
     "inputRev?": "master",
     "inherited": false}},
   {"git":
-   {"url": "https://github.com/gebner/quote4",
+   {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "rev": "fb07d160aff0e8bdf403a78a5167fc7acf9c8227",
     "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
+    "name": "std",
+    "inputRev?": "main",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "4f8b397237411249930791f1cba0a9d2880a02dd",
+    "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
     "opts": {},
-    "name": "aesop",
+    "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
+   {"url": "https://github.com/leanprover-community/aesop",
     "subDir?": null,
-    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
     "opts": {},
-    "name": "Cli",
-    "inputRev?": "nightly",
+    "name": "aesop",
+    "inputRev?": "master",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/leanprover/std4",
+   {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
+    "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
     "opts": {},
-    "name": "std",
+    "name": "Cli",
     "inputRev?": "main",
     "inherited": true}},
   {"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
     "subDir?": null,
-    "rev": "9f68f14df384f43b74aeb2908b97ae54a0ad9d95",
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.17",
+    "inputRev?": "v0.0.21",
     "inherited": true}}],
  "name": "scilean"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc1
+leanprover/lean4:v4.3.0-rc1

test/generate_ftrans.lean

@@ -50,7 +50,7 @@ info: mymul.arg_y.revCDeriv_rule_def.{w, u} {K : Type u} [instK : IsROrC K] {W :
   (x : K) (y : W → K) (hy : HasAdjDiff K y) :
   <∂ w, mymul x (y w) = fun w =>
     let ydy' := <∂ y w;
-    mymul.arg_y.revCDeriv x ydy'.fst ydy'.snd
+    mymul.arg_y.revCDeriv x ydy'.1 ydy'.2
 -/
 #guard_msgs in
 #check mymul.arg_y.revCDeriv_rule_def
@@ -62,7 +62,7 @@ info: mymul.arg_xy.revCDeriv_rule_def.{w, u} {K : Type u} [instK : IsROrC K] {W
   <∂ w, mymul (x w) (y w) = fun w =>
     let xdx' := <∂ x w;
     let ydy' := <∂ y w;
-    mymul.arg_xy.revCDeriv xdx'.fst ydy'.fst xdx'.snd ydy'.snd
+    mymul.arg_xy.revCDeriv xdx'.1 ydy'.1 xdx'.2 ydy'.2
 -/
 #guard_msgs in
 #check mymul.arg_xy.revCDeriv_rule_def
@@ -74,7 +74,7 @@ info: mymul.arg_xy.fwdCDeriv_rule_def.{w, u} {K : Type u} [instK : IsROrC K] {W
   ∂> w, mymul (x w) (y w) = fun w dw =>
     let xdx := ∂> x w dw;
     let ydy := ∂> y w dw;
-    mymul.arg_xy.fwdCDeriv xdx.fst ydy.fst xdx.snd ydy.snd
+    mymul.arg_xy.fwdCDeriv xdx.1 ydy.1 xdx.2 ydy.2
 -/
 #guard_msgs in
 #check mymul.arg_xy.fwdCDeriv_rule_def

test/issues/17.lean

@@ -10,7 +10,7 @@ variable
 set_default_scalar K
 
 /--
-info: (∂> (x':=x;dx), f x').snd : Y
+info: (∂> (x':=x;dx), f x').2 : Y
 -/
 #guard_msgs in
 #check 

test/issues/25.lean

@@ -25,4 +25,4 @@ by
   -- failed to synthesize
   --   SemiInnerProductSpace K (X → X)
   -- ftrans 
-  sorry
+  sorry_proof

test/structural_inverse.lean

@@ -23,8 +23,8 @@ info: fun ij1 y =>
 
 /--
 info: fun ij1 y =>
-  let ij0' := fun ij2 => Function.invFun (fun ij0 => ij0 + ij2) y.fst;
-  let ij2' := fun ij1 => Function.invFun (fun ij2 => ij1 + ij0' ij2 + ij2) y.snd;
+  let ij0' := fun ij2 => Function.invFun (fun ij0 => ij0 + ij2) y.1;
+  let ij2' := fun ij1 => Function.invFun (fun ij2 => ij1 + ij0' ij2 + ij2) y.2;
   let ij2'' := ij2' ij1;
   let ij0'' := ij0' ij2'';
   (ij0'', ij1, ij2'')
@@ -35,10 +35,10 @@ info: fun ij1 y =>
   let f := q(fun ij : Int × Int × Int => (ij.1 + ij.2.2, ij.2.1 + ij.1 + ij.2.2))
   let .some (.right f', _) ← structuralInverse f
     | throwError "failed to invert"
-  IO.println (← ppExpr f'.invFun)  
+  IO.println (← ppExpr f'.invFun) 
 
 /-- 
-info: fun ij1 y => (y.snd, ij1, y.fst)
+info: fun ij1 y => (y.2, ij1, y.1)
 -/
 #guard_msgs in
 #eval show MetaM Unit from do
@@ -48,7 +48,7 @@ info: fun ij1 y => (y.snd, ij1, y.fst)
   IO.println (← ppExpr f'.invFun)  
 
 /-- 
-info: fun y => (y.snd.fst, y.snd.snd, y.fst)
+info: fun y => (y.2.1, y.2.2, y.1)
 -/
 #guard_msgs in
 #eval show MetaM Unit from do
@@ -60,8 +60,8 @@ info: fun y => (y.snd.fst, y.snd.snd, y.fst)
 
 /--
 info: fun x1 y =>
-  let x0' := fun x1 => Function.invFun (fun x0 => x0 + x1) y.snd;
-  let x2' := fun x1 => Function.invFun (fun x2 => x0' x1 + x1 + x2) y.fst;
+  let x0' := fun x1 => Function.invFun (fun x0 => x0 + x1) y.2;
+  let x2' := fun x1 => Function.invFun (fun x2 => x0' x1 + x1 + x2) y.1;
   let x2'' := x2' x1;
   let x0'' := x0' x1;
   (x0'', x1, x2'')
@@ -78,7 +78,7 @@ info: fun x1 y =>
 
 
 /--
-info: fun x1 y => (y.snd, x1, y.fst)
+info: fun x1 y => (y.2, x1, y.1)
 -/
 #guard_msgs in
 #eval show MetaM Unit from do