basic tests for revDeriv

lecopivo · Dec 4, 2023 · 09f2449 · 09f2449
1 parent 0318029
commit 09f2449
Show file tree

Hide file tree

Showing 2 changed files with 355 additions and 101 deletions.
diff --git a/SciLean/Core/Meta/GenerateRevDeriv.lean b/SciLean/Core/Meta/GenerateRevDeriv.lean
@@ -288,104 +288,3 @@ elab_rules : command
       | throwError "unknown function {fnStx}"
     generateRevDeriv constName mainArgs trailingArgs .withDef t (← `(conv| ($rw)))
 
-
-variable 
-  {K : Type} [RealScalar K]
-  {X : Type} [SemiInnerProductSpace K X]
-  {X₁ : Type} [SemiInnerProductSpace K X₁]
-  {X₂ : Type} [SemiInnerProductSpace K X₂]
-  {Y : Type} [SemiInnerProductSpace K Y]
-  {Z : Type} [SemiInnerProductSpace K Z]
-  {W : Type} [SemiInnerProductSpace K W]
-  {ι : Type} [EnumType ι]
-  {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)]
-
-set_default_scalar K
-
-def mul (x y : K) : K := x * y
-
-#generate_revDeriv mul x y
-  prop_by unfold mul; fprop
-  trans_by unfold mul; ftrans; ftrans
-
-#print mul.arg_xy.revDeriv
-#check mul.arg_xy.revDeriv_rule_simple
-#check mul.arg_xy.revDeriv_rule
-#check mul.arg_xy.revDerivUpdate_rule
-#check mul.arg_xy.revDeriv_rule_def_simple
-#check mul.arg_xy.HasAdjDiff_rule_simple
-#check mul.arg_xy.HasAdjDiff_rule
-
-def add (x y : X) : X := x + y
-
-#generate_revDeriv add x y
-  prop_by unfold add; fprop
-  trans_by unfold add; ftrans; ftrans
-
-#print add.arg_xy.revDeriv
-#check add.arg_xy.revDeriv_rule_simple
-#check add.arg_xy.revDeriv_rule_def_simple
-#check add.arg_xy.HasAdjDiff_rule_simple
-
-def smul {X : Type} [SemiHilbert K X]
- (x : K) (y : X) : X := x • y
-
-set_option trace.Meta.Tactic.fprop.discharge true in
-#generate_revDeriv smul x y
-  prop_by unfold smul; fprop
-  trans_by unfold smul; ftrans; ftrans
-
-
-set_option trace.Meta.Tactic.simp.discharge true in
-set_option trace.Meta.Tactic.simp.unify true in
-#check 
-  (revDeriv K fun (xy : K×K) => mul xy.1 xy.2)
-  rewrite_by
-    ftrans
-
-set_option trace.Meta.Tactic.simp.rewrite true in
-set_option trace.Meta.Tactic.simp.unify true in
-set_option trace.Meta.Tactic.simp.discharge true in
-#check 
-  (revDeriv K fun (x : K) => mul x x)
-  rewrite_by
-    ftrans
-
-#check FunLike
-
-set_option trace.Meta.Tactic.simp.rewrite true in
--- set_option trace.Meta.Tactic.simp.unify true in
-#check 
-  (revDeriv K fun (x : K) =>
-    let x1 := mul x x
-    let x2 := mul x1 (mul x x)
-    let x3 := mul x2 (mul x1 x)
-    let x4 := mul x3 (mul x2 x)
-    let x5 := mul x4 (mul x3 x)
-    x5)
-  rewrite_by
-    ftrans
-
-
-#check
-  (revDeriv K fun (x : K) =>
-    let x1 := mul x x
-    let x2 := mul x1 x1
-    let x3 := mul x2 x2
-    let x4 := mul x3 x3
-    let x5 := mul x4 x4
-    x5)
-  rewrite_by
-    ftrans
-
-
-#check 
-  (revDeriv K fun (x : K) =>
-    let x1 := mul x x
-    let x2 := mul x1 x
-    let x3 := mul x2 x
-    let x4 := mul x3 x
-    let x5 := mul x4 x
-    x5)
-  rewrite_by
-    ftrans