From 1594d3dd97b7cf3be02b43bbdb7e4e1f7c033bbd Mon Sep 17 00:00:00 2001 From: lecopivo Date: Fri, 10 Nov 2023 10:34:02 -0500 Subject: [PATCH] bump to leanprover/lean4:v4.3.0-rc1 --- .../FunctionTransformations/FwdFDeriv.lean | 20 +++++------ .../FunctionTransformations/RevCDeriv.lean | 4 ++- .../FunctionTransformations/RevFDeriv.lean | 2 +- SciLean/Core/Monads/Id.lean | 2 +- SciLean/Tactic/LSimp2/Elab.lean | 9 +++-- SciLean/Tactic/LSimp2/Main.lean | 2 +- lake-manifest.json | 36 +++++++++---------- lean-toolchain | 2 +- test/generate_ftrans.lean | 6 ++-- test/issues/17.lean | 2 +- test/issues/25.lean | 2 +- test/structural_inverse.lean | 16 ++++----- 12 files changed, 54 insertions(+), 49 deletions(-) diff --git a/SciLean/Core/FunctionTransformations/FwdFDeriv.lean b/SciLean/Core/FunctionTransformations/FwdFDeriv.lean index 36764666..e7f8c051 100644 --- a/SciLean/Core/FunctionTransformations/FwdFDeriv.lean +++ b/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 ------------------------------------------------------------------- diff --git a/SciLean/Core/FunctionTransformations/RevCDeriv.lean b/SciLean/Core/FunctionTransformations/RevCDeriv.lean index 3e344361..7bcd9db0 100644 --- a/SciLean/Core/FunctionTransformations/RevCDeriv.lean +++ b/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' diff --git a/SciLean/Core/FunctionTransformations/RevFDeriv.lean b/SciLean/Core/FunctionTransformations/RevFDeriv.lean index ffcf364a..b8fb94f9 100644 --- a/SciLean/Core/FunctionTransformations/RevFDeriv.lean +++ b/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 diff --git a/SciLean/Core/Monads/Id.lean b/SciLean/Core/Monads/Id.lean index ac00bc41..e882a8ea 100644 --- a/SciLean/Core/Monads/Id.lean +++ b/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 diff --git a/SciLean/Tactic/LSimp2/Elab.lean b/SciLean/Tactic/LSimp2/Elab.lean index b8e87f72..6291af0a 100644 --- a/SciLean/Tactic/LSimp2/Elab.lean +++ b/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 => diff --git a/SciLean/Tactic/LSimp2/Main.lean b/SciLean/Tactic/LSimp2/Main.lean index fa236880..f100eb3f 100644 --- a/SciLean/Tactic/LSimp2/Main.lean +++ b/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 } diff --git a/lake-manifest.json b/lake-manifest.json index dde340a4..5418b925 100644 --- a/lake-manifest.json +++ b/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"} diff --git a/lean-toolchain b/lean-toolchain index 400394aa..734efddd 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc1 +leanprover/lean4:v4.3.0-rc1 \ No newline at end of file diff --git a/test/generate_ftrans.lean b/test/generate_ftrans.lean index 38fd31c9..c3c3cede 100644 --- a/test/generate_ftrans.lean +++ b/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 diff --git a/test/issues/17.lean b/test/issues/17.lean index 2095a13a..e888a6e0 100644 --- a/test/issues/17.lean +++ b/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 diff --git a/test/issues/25.lean b/test/issues/25.lean index 0361dad3..fd364b0e 100644 --- a/test/issues/25.lean +++ b/test/issues/25.lean @@ -25,4 +25,4 @@ by -- failed to synthesize -- SemiInnerProductSpace K (X → X) -- ftrans - sorry + sorry_proof diff --git a/test/structural_inverse.lean b/test/structural_inverse.lean index f80ff85d..00359208 100644 --- a/test/structural_inverse.lean +++ b/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