Tactics

Stream: new members

[Brandon B]

I'm not fully grasping what the tactics are doing in this proof. I've written a comment that is how I'm thinking of it on paper but not sure if that's correct.

        theorem even_plus_even2 {a b : nat}
            (h1 : is_even a) (h2 : is_even b) : is_even (a + b) :=
                match h1, h2 with
                    ⟨w1, hw1⟩, ⟨w2, hw2⟩ := ⟨w1 + w2, by rw [hw1, hw2, mul_add]⟩
                end
        /-
        ∃ w1, a = 2 * w1
        w1 : ℕ
        hw1 : a = 2 * w1
        ∃ w2, b = 2 * w2
        w2 : ℕ
        hw2 : b = 2 * w2
        w1 = a/2, w2 = b/2
        w1 + w2 = a/2 + b/2
        a + b = 2 * (w1 + w2)
        -/

[Mario Carneiro]

This proof looks okay (but you didn't provide a MWE). What error do you get?

[Mario Carneiro]

Or is the proof correct and you don't understand how it works?

[Brandon B]

The proof is correct I'm just trying to understand what's going on under the hood

[Mario Carneiro]

Actually there aren't really any tactics in this proof except rw. The match is pattern matching on h1 and h2, which are existential statements once you unfold the definition of is_even, to produce w1 and hw1 : a = 2 * w1 and similarly for w2

[Brandon B]

yeah I understand match I just dont fully understand the ,by rw [hw1, hw2, mul_add]

[Mario Carneiro]

The right hand side is similarly building an existential proof saying w1 + w2 suffices, and so the by rw proof needs to prove a + b = 2 * (w1 + w2)

[Mario Carneiro]

Then the rewrites respectively change the goal to 2 * w1 + b = 2 * (w1 + w2) and 2 * w1 + 2 * w2 = 2 * (w1 + w2), and the final mul_add rewrites the right hand side to 2 * w1 + 2 * w2 = 2 * w1 + 2 * w2. Since this is true by reflexivity it closes the goal

[Mario Carneiro]

At least, that's what the lean in my head would do, since that's not an MWE I can't test it

[Brandon B]

Ohhh that makes sense, thanks!

[Brandon B]

So rewrite is a substitution rule

[Frank Dai]

you can also expand by rw [a, b, c] into begin rw a, rw b, rw c, end and step through it

theorem even_plus_even2 {a b : nat}
    (h1 : is_even a) (h2 : is_even b) : is_even (a + b) :=
        match h1, h2 with
            ⟨w1, hw1⟩, ⟨w2, hw2⟩ := ⟨w1 + w2, begin
              rw hw1,
              rw hw2,
              rw mul_add,
              end⟩
        end
 ```

[Mario Carneiro]

You should be able to step through it even if it is in rw [a,b,c] form

[Mario Carneiro]

this is one of the special privileges of the rw tactic

[Brandon B]

How does mul_add know to apply to the right hand side of the equation?

[Brandon B]

rw is rewriting terms on the LHS but mul_add works on the RHS.

[Brandon B]

⊢ 2 * w1 + 2 * w2 = 2 * (w1 + w2)

[Mario Carneiro]

rw will try to find the LHS of the input theorem anywhere in the goal, including on the RHS of the equality if the goal happens to be an equality

[Mario Carneiro]

If you used mul_add the other way around, that is rw <- mul_add, then it would try to find a * b + a * c somewhere in the goal instead. In this case it would still succeed, rewriting the LHS and resulting in 2 * (w1 + w2) = 2 * (w1 + w2) which is also reflexivity

[Brandon B]

When we use tactics, what exactly is happening? Is it replacing the tactic command with lambda expressions under-the-hood? Doesn't everything ultimately need to be reduced to lambda expressions for type checking?

[Bryan Gin-ge Chen]

Did you look at the sources we linked here when you asked this previously?

[Brandon Brown]

Yes, but I have zero background in functional programming. I know Python and R and Java and C. So a "proof state" doesn't make sense to me in the first place. I am sort of learning how to prove basic things but I'm frustrated I don't know what's going on at the computer science level.

[Mario Carneiro]

Behind the scenes Lean is building a term which has holes, metavariables, in it

[Mario Carneiro]

as you use more tactics these holes get filled with more terms with holes until eventually the holes go away

[Mario Carneiro]

each hole is marked with the type that is expected at that position, and that's the goal state that you see

[Mario Carneiro]

It's very much like writing term mode proofs using _

[Brandon Brown]

So in principle there is a way to mechanistically translate a proof written using tactics into a term mode proof?

[Brandon Brown]

And get one ugly lambda expression at the other end

[Kenny Lau]

#print

[Mario Carneiro]

See also the thread here

[Kenny Lau]

treat tactics as little C++ programs that help you write term mode proofs

[Brandon Brown]

Ohh, ok #print is exactly what I wanted to know

[Mario Carneiro]

the lean kernel only knows term proofs, so tactics have to run to produce a term proof before the theorem can be accepted

[Mario Carneiro]

these proofs are stored and #print recalls them

[Bryan Gin-ge Chen]

#print is mentioned early on in the Tactics chapter of TPiL.

[Brandon Brown]

I see - starting to make a lot more sense. I just couldnt understand why there seemed to be two completely different languages in the same language

[Mario Carneiro]

They call it metaprogramming because you are writing a program (tactic) to build a program (term)

[Brandon Brown]

Ahh, your answer there about filling holes is very lucid, thanks

[Brandon Brown]

Thanks for bearing with me - I'm actually a medical doctor just trying to learn more math so I have very little background in all of this

[Bryan Gin-ge Chen]

Feel free to keep asking questions! There aren't very many introductory sources so most of us have been learning here.

[Parivash]

lemma some_name (θ : ℕ → ℝ≥0 )(a b C P q A V₀ Vads x qq : ℝ≥0 )
  (hA : A = θ 0 + ∑' (k : ℕ), C * (θ 0 * x ^ k ))
  (hVads : Vads = 0 * θ 0 + ∑' (k : ℕ), C * ( θ 0 * (x ^ k * k)))(hq : q = Vads / A)
  (h4: qq = θ 0 * ( 1 + C * (∑' (x_1 : ℕ), x ^ x_1))) :
  q = θ 0 + C * θ 0 * (∑' (x_1 : ℕ), x ^ x_1):=
begin
  /- simp only [h1] at hA {single_pass := tt}, -/
  /- rw pow_zero at hA, -/
  /- rw one_mul at hA, -/
  rw tsum_mul_left at hA,
  rw tsum_mul_left at hA,
  rw ← mul_assoc at hA,
  rw zero_mul at hVads,
  rw zero_add at hVads,
  rw tsum_mul_left at hVads,
  rw tsum_mul_left at hVads,
  rw ← mul_assoc at hVads,
  rw left_distrib at h4,
  rw hA at hq,
  rw hVads at hq,


end

Hi, I want to cancel $\theta 0$ at hq. In other words, how can I take it out from numerator and denominator and then cancel it.

[Ruben Van de Velde]

Pasting that into an empty file yields a bunch of errors - can you create a #mwe?

[Parivash]

@Ruben Van de Velde
Not actually, let me provide the whole things that you can run it.

/- Background Copy-/
import analysis.specific_limits
import data.real.basic
import tactic
import algebra.group.defs
import logic.function.basic
import topology.algebra.infinite_sum
import topology.algebra.group_with_zero

/- left_comm has_mul.mul mul_comm mul_assoc-/

mul_eq_of_eq_div' (h : b = c / a) : a * b = c :=
begin simp [h], rw [mul_comm c, mul_inv_cancel_left] end

/-!
# Topology on `ℝ≥0`
The natural topology on `ℝ≥0` (the one induced from `ℝ`), and a basic API.
## Main definitions
Instances for the following typeclasses are defined:
* `topological_space ℝ≥0`
* `topological_semiring ℝ≥0`
* `second_countable_topology ℝ≥0`
* `order_topology ℝ≥0`
* `has_continuous_sub ℝ≥0`
* `has_continuous_inv' ℝ≥0` (continuity of `x⁻¹` away from `0`)
Everything is inherited from the corresponding structures on the reals.
## Main statements
Various mathematically trivial lemmas are proved about the compatibility
of limits and sums in `ℝ≥0` and `ℝ`. For example
* `tendsto_coe {f : filter α} {m : α → ℝ≥0} {x : ℝ≥0} :
  tendsto (λa, (m a : ℝ)) f (𝓝 (x : ℝ)) ↔ tendsto m f (𝓝 x)`
says that the limit of a filter along a map to `ℝ≥0` is the same in `ℝ` and `ℝ≥0`, and
* `coe_tsum {f : α → ℝ≥0} : ((∑'a, f a) : ℝ) = (∑'a, (f a : ℝ))`
says that says that a sum of elements in `ℝ≥0` is the same in `ℝ` and `ℝ≥0`.
Similarly, some mathematically trivial lemmas about infinite sums are proved,
a few of which rely on the fact that subtraction is continuous.
-/
noncomputable theory
open set topological_space metric filter
open_locale topological_space

namespace nnreal
open_locale nnreal big_operators

instance : topological_space ℝ≥0 := infer_instance -- short-circuit type class inference

section coe
variable {α : Type*}

variables [t2_space α]

lemma some_name (θ : ℕ → ℝ≥0 )(a b C P q A V₀ Vads x qq : ℝ≥0 )
  (hA : A = θ 0 + ∑' (k : ℕ), C * (θ 0 * x ^ k ))
  (hVads : Vads = 0 * θ 0 + ∑' (k : ℕ), C * ( θ 0 * (x ^ k * k)))(hq : q = Vads / A)
  (h4: qq = θ 0 * ( 1 + C * (∑' (x_1 : ℕ), x ^ x_1))) :
  q = θ 0 + C * θ 0 * (∑' (x_1 : ℕ), x ^ x_1):=
begin
  /- simp only [h1] at hA {single_pass := tt}, -/
  /- rw pow_zero at hA, -/
  /- rw one_mul at hA, -/
  rw tsum_mul_left at hA,
  rw tsum_mul_left at hA,
  rw ← mul_assoc at hA,
  rw zero_mul at hVads,
  rw zero_add at hVads,
  rw tsum_mul_left at hVads,
  rw tsum_mul_left at hVads,
  rw ← mul_assoc at hVads,
  rw left_distrib at h4,
  rw hA at hq,
  rw hVads at hq,
end

[Kevin Buzzard]

Your code still doesn't compile for me, but anyway even after you fix this I think the answer will be that you can't cancel θ 0 because you don't seem to have assumed anywhere that it is nonzero.

[Kevin Buzzard]

Note that Lean does not check that $b\not=0$ when you write $a/b$, it allows you to write nonsense, and just returns a junk value; you then can't use theorems about division because it is in the theorems where the hypothesis $b\not=0$ is required.