tactic

Stream: new members

[Alex Zhang]

I want to prove p or q, is there any tactic that changes the stage to having not p in the context and q as the goal?

example (p q : Prop) : p ∨ q :=
begin

end

[Alex Zhang]

I can use by_cases p. Is there any one step tactic?

[Mario Carneiro]

there's always a one step tactic if the step is refine

[Mario Carneiro]

import logic.basic

example (p q : Prop) : p ∨ q :=
begin
  refine or_iff_not_imp_left.2 (λ h, _),
end

[Alex Zhang]

Suppose I have four goals in the info view, does Lean have any feature that allows me to use some tactic, say rw [h], to only certain goals, say goals 2 and 3 only.

[Alex J. Best]

One way (if the rewrite only applies to those goals) is to use tactic#any_goals as any_goals { rw h } (or do all_goals { try { rw [h] }}) otherwise there have been some discussions, and example tactics doing this https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/work_on_goals.3F/near/193204723 and https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/work_on_goals/near/220310832. I'm not sure if either of them were ever PRed @Eric Wieser ?

[Eric Rodriguez]

Something I use a lot is the or else combiner, <|>. This does left tactic unless it fails, then it does right tactic

[Eric Rodriguez]

So all_goals { rw h orelse simp} usually works well for this sort of thing (sorry for formatting, on mobile)

[Alex Zhang]

If the other goals actually don't have h, will all_goals { try { rw [h] }} fail?

[Eric Wieser]

I ended up PRing improvements to tactic#case instead of any of the tactics in that thread.

[Yakov Pechersky]

No, it will not fail. You should use any_goals instead for that purpose, without the try.

[Parivash]

import analysis.specific_limits
import data.real.basic

lemma some_name (θ : ℕ → ℝ) (a b C P q A V₀ Vads x : ℝ)
  (h1 : ∀ k, θ k = C * x ^ k * θ 0) (hA : A = ∑' k, θ k)
  (hVads : Vads = V₀ * ∑' k : ℕ, k * θ k) (hq : q = Vads / A):
  q = a * P / ((1 - b * P) * (1 - b * P + C * P)) :=
begin
  simp only [h1] at hA {single_pass := tt},
  rw hA at hq,
  simp only [h1] at hVads {single_pass := tt},
  rw hVads at hq,

end

I want to taking out $\theta_{0} \& C$ from inside the summation in hq and cancel them, which tactic works here?

[Kevin Buzzard]

That's not a tactic you're looking for, you need a lemma. You are going to come unstuck soon because you have no hypotheses about anything converging and Lean defines any divergent sum to be 0. The lemmas you'll need are tsum_mul_right and tsum_mul_left.

[Parivash]

(deleted)

[Parivash]

lemma some_name (θ : ℕ → ℝ)(a b C P q A V₀ Vads x : ℝ )
  (h1 : ∀ k, θ k = C * x ^ k * θ 0) (hA : A = ∑' k, θ k)
  (hVads : Vads = V₀ * ∑' k : ℕ, k * θ k) (hq : q = Vads / A):
  q = a * P / ((1 - b * P) * (1 - b * P + C * P)) :=
begin
  simp only [h1] at hA {single_pass := tt},
  rw hA at hq,
  simp only [h1] at hVads {single_pass := tt},
  rw hVads at hq,
  /- rw tsum_mul_left at hVads,-/
  have h4 :  V₀ *  ∑' k : ℕ, k * ( C * x ^ k * θ 0 )= (V₀ * C * θ 0  *∑' k : ℕ, k * x ^ k ) := sorry,
  rw h4 at hq,
  have h5 :  ∑' k : ℕ,( C * x ^ k * θ 0 )= (C * θ 0  *∑' k : ℕ, x ^ k ) := sorry,
  /- rw tsum_mul_left at hA,-/
  rw h5 at hq,
  /- rw int.mul_div_mul_of_pos,-/  /- to cancel θ 0 and C at hq -/
end

Why tsum_mul_left & rw int.mul_div_mul_of_ops doesn't work here!

[Eric Wieser]

What do the error messages say?

[Parivash]

@Eric Wieser
rewrite tactic failed, did not find instance of the pattern in the target expression
∑' (x : ?m_1), ?m_2 * ?m_3 x

[Eric Wieser]

What does the _full_ error message say?

[Eric Wieser]

(including the goal state)

[Parivash]

rewrite tactic failed, did not find instance of the pattern in the target expression
∑' (x : ?m_1), ?m_2 * ?m_3 x
state:
θ : ℕ → ℝ≥0,
a b C P q A V₀ Vads x : ℝ≥0,
h1 : ∀ (k : ℕ), θ k = C * x ^ k * θ 0,
hA : A = ∑' (k : ℕ), C * x ^ k * θ 0,
hVads : Vads = V₀ * ∑' (k : ℕ), ↑k * (C * x ^ k * θ 0),
hq : q = (V₀ * ∑' (k : ℕ), ↑k * (C * x ^ k * θ 0)) / ∑' (k : ℕ), C * x ^ k * θ 0
⊢ Vads = V₀ * C * θ 0 * ∑' (k : ℕ), ↑k * x ^ k

[Yaël Dillies]

I can't find the instance either. In ∑' (k : ℕ), ↑k * x ^ k, both sides of the * depend on k.

[Parivash]

Actually, I want to take out $\theta 0 and C$ which are constants from summation at hq and the cancel them. I want to change hq to this format: $\frac{C*\sum_{i=1}^{+\infty}i*x^{i}}{(1+C*\sum_{i=1}^{+\infty}x^{i})}$

[Yaël Dillies]

Click on the inside of the sum in the tactic state. You'll see that C * x ^ k * θ 0 means (C * x ^ k) * θ 0, not C * (x ^ k * θ 0). You can turn one into the other using docs#mul_assoc.

[Parivash]

@Yaël Dillies
I cannot find what you mentioned inside the sum in tactic state!