Data.Complex.Exponential !4#2785

Stream: mathlib4

[Chris Hughes]

There seems to be a Lean bug in Data.Complex.Exponential There is a red line underneath the by saying unsolved goals, with a tactic state that looks like it should have been closed by the final simp. If I write another simp and then a new line on line 1630, then the tactic state it displays is just the type of the whole theorem, but there is still a red line under the by. This whole theorem seems fairly buggy, replacing the whole proof with sorry sometimes fails as well, but not always, and I seem to have to keep restarting Lean. Maybe the file is too long or something like that. It is hard to diagnose.

[Kevin Buzzard]

I had to keep restarting lean when I was fixing up some sorrys in the file Adam was porting yesterday, because all the errors were out of sync, lean would complain that tactics weren't being used etc, just completely crazy things. Then I discovered to my delight that at least I could work around it by changing the def I was working on to deqf and then back to def again.

[Kevin Buzzard]

It triggered a "hard recompile" but just of the def I was working on

[Chris Hughes]

The new version of Lean seems to have fixed the problem

[Chris Hughes]

This PR is ready for review, and it would be great if somebody who understood the positivity tactic could finish off the extension for exp. Maybe
@David Renshaw

[Yaël Dillies]

I can do it if you're willing to wait until Wednesday morning.

[David Renshaw]

This seems to work. Want me to push it to that PR?

diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
index f24f4a1e..051397b5 100644
--- a/Mathlib/Data/Complex/Exponential.lean
+++ b/Mathlib/Data/Complex/Exponential.lean
@@ -2070,19 +2070,16 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t

 end Real

---Porting note: TODO: write this extension
--- namespace Tactic
+namespace Tactic
+open Lean.Meta Qq

--- open Positivity Real
+/-- Extension for the `positivity` tactic: `real.exp` is always positive. -/
+@[positivity Real.exp _]
+def evalExp : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ e := do
+  let (.app _ (a : Q(ℝ))) ← withReducible (whnf e) | throwError "not Real.exp"
+  pure (.positive (q(Real.exp_pos $a) : Lean.Expr))

--- /-- Extension for the `positivity` tactic: `real.exp` is always positive. -/
--- @[positivity]
--- unsafe def positivity_exp : expr → tactic strictness
---   | q(Real.exp $(a)) => positive <$> mk_app `real.exp_pos [a]
---   | e => pp e >>= fail ∘ format.bracket "The expression `" "` isn't of the form `real.exp r`"
--- #align tactic.positivity_exp tactic.positivity_exp
-
--- end Tactic
+end Tactic

 namespace Complex

[David Renshaw]

I'm a bit confused why an extension for Real.exp lives in the file Complex.Exponential.

[Chris Hughes]

Because Real.exp is defined as the real part of Complex.exp. It doesn't have to be like that, but there's no reason why not eirher.

[Chris Hughes]

Please push it. Thanks for writing the extension

[Jeremy Tan]

David Renshaw said:

This seems to work. Want me to push it to that PR?

diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
index f24f4a1e..051397b5 100644
--- a/Mathlib/Data/Complex/Exponential.lean
+++ b/Mathlib/Data/Complex/Exponential.lean
@@ -2070,19 +2070,16 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t

 end Real

---Porting note: TODO: write this extension
--- namespace Tactic
+namespace Tactic
+open Lean.Meta Qq

--- open Positivity Real
+/-- Extension for the `positivity` tactic: `real.exp` is always positive. -/
+@[positivity Real.exp _]
+def evalExp : Mathlib.Meta.Positivity.PositivityExt where eval {_ _} _ _ e := do
+  let (.app _ (a : Q(ℝ))) ← withReducible (whnf e) | throwError "not Real.exp"
+  pure (.positive (q(Real.exp_pos $a) : Lean.Expr))

--- /-- Extension for the `positivity` tactic: `real.exp` is always positive. -/
--- @[positivity]
--- unsafe def positivity_exp : expr → tactic strictness
---   | q(Real.exp $(a)) => positive <$> mk_app `real.exp_pos [a]
---   | e => pp e >>= fail ∘ format.bracket "The expression `" "` isn't of the form `real.exp r`"
--- #align tactic.positivity_exp tactic.positivity_exp
-
--- end Tactic
+end Tactic

 namespace Complex

Yes, go ahead