tactics

Stream: new members

[Brian Jiang]

is there a factor tactic? (sort of like the reverse of mul_add)

[Kevin Buzzard]

No there is not! There is a factor-checking tactic, but not a factor-doing one.

[Kevin Buzzard]

Remember though that you can rewrite mul_add in both directions :-)

[Brian Jiang]

so if I have something like n*a +n*b = 1

[Brian Jiang]

and I do mul_add

[Brian Jiang]

I should get n*(a+b)=1?

[Kevin Buzzard]

what do you mean by "do"?

[Kevin Buzzard]

Let's get precise :-)

[Brian Jiang]

if I `rw mul_add that statement

[Kevin Buzzard]

then it will say "I can't find anything of the form x*(y+z) in your statement so I can't rewrite"

[Kevin Buzzard]

But if you rw ←mul_add then it will work fine

[Brian Jiang]

oh thanks! didn't know how to go backwards at first

[Kevin Buzzard]

if h is a proof of A = B then rw h will turn all A's in your goal to B's, and rw ←h will turn all B's into A's.

[Kevin Buzzard]

import tactic

example (x y z : ℤ) :
  x^3 + y^3 + z^3 - 3*x*y*z = (x+y+z)*(x^2+y^2+z^2-x*y-y*z-z*x) :=
  begin
    ring
  end

Lean didn't do the factoring, but it checked it once I told it.

[Brian Jiang]

Another quick tactic question

[Brian Jiang]

what tactic should I use if I want to turn a=b into b=a?

[Brian Jiang]

I tried rw eq.symm but I got some sort of "lemma lhs is a metavariable" error

[Kevin Buzzard]

The rw tactic only works with equalities or iff statements. eq.symm is an implication a = b → b = a. So you should apply it instead. This is a really important distinction and the sooner you learn it the easier your path to enlightenment will be.

[Kevin Buzzard]

Note that if you want to rewrite something, eq_comm is the proof that a = b ↔ b = a

[Kevin Buzzard]

I see undergraduate mathematicians in my department asking this question again and again. For mathematicians, equality and implication seem to basically be the same idea, or are stored in the same place or something. I guess the point is that if a mathematician knows that $P\iff Q$ is true, then obviously $P\implies Q$ is true, and the concepts can get a bit blurred, especially because in some sense the vast majority of $\implies$ statements mathematicians use in school mathematics are special cases of $\iff$ statements.

[Kevin Buzzard]

My daughter is currently learning about making new variables the subject of the equation, e.g. she is told $y=3x+5$ and has to figure out how to write $x$ as a function of $y$. The route to $x=(y-5)/3$ is expressed as a series of implications, but in practice it is a series of iff statements. I am not sure if the distinction is flagged at school.

[Scott Morrison]

You can also use symmetry, which tries to apply a relevant lemma marked with the [symm] attribute.

[Kevin Buzzard]

and #print eq.symm shows that indeed this lemma has that tag.

[Alex Zhang]

I don't quite understand the tactic obviously. I saw this tactic in

structure simple_graph (V : Type u) :=
(adj : V → V → Prop)
(sym : symmetric adj . obviously)
(loopless : irreflexive adj . obviously)

In particular, I don't understand how obviously helps here.
Could anyone please give me a #mwe illustrating the function of obviously?

[Kyle Miller]

def complete_graph (V : Type u) : simple_graph V :=
{ adj := ne }

[Kyle Miller]

What obviously does is make it equivalent to writing this:

def complete_graph (V : Type u) : simple_graph V :=
{ adj := ne, sym := by tidy, loopless := by tidy }

(At least, I think obviously does by tidy. I'm not remembering. Edit: it basically does tidy, but there's an extra thing where it checks for sorry in the type.)