Mathematicians learning tactics

Stream: general

[Kevin Buzzard]

instance : comm_monoid ℕ+ :=
{ mul       := λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩,
  mul_assoc := λ a b c, subtype.eq (mul_assoc _ _ _),
  one       := succ_pnat 0,
  one_mul   := λ a, subtype.eq (one_mul _),
  mul_one   := λ a, subtype.eq (mul_one _),
mul_comm := λ a b, subtype.eq (mul_comm _ _) }

[Kevin Buzzard]

https://github.com/leanprover/mathlib/blob/00a2eb4119d27761c8a6ee38eb1eae532cd3ac19/data/pnat.lean#L52

[Kevin Buzzard]

All of the proofs of the axioms are the same

[Kevin Buzzard]

"it's true for nat so done by subtype.eq"

[Kevin Buzzard]

Could I write that sentence as a tactic?

[Kevin Buzzard]

I don't even know if that's possible because I don't know what tactics know about names

[Kevin Buzzard]

I'm looking for a proof that defines mul and one and then says done by tactic

[Kevin Buzzard]

If I can do the above with a tactic then I think I can start to work on the tactic I actually want.

[Kevin Buzzard]

and maybe other mathematicians might like the same sort of tactics

[Kevin Buzzard]

Remember when we noticed that proving that if A and B were equiv and A was a ring then B was a ring, was actually quite annoying?

[Kevin Buzzard]

And Kenny would just knock off a proof and he'd just check all ten axioms

[Kevin Buzzard]

and every proof would be funext, simp [name of thing I'm proving]

[Kevin Buzzard]

I think it's about time Kenny learnt how to write this tactic too

[Mario Carneiro]

This is somewhat similar to Simon's pi instance tactic

[Kevin Buzzard]

Can you give me a link?

[Mario Carneiro]

https://github.com/leanprover/mathlib/blob/master/algebra/pi_instances.lean

[Kevin Buzzard]

It's just the same underlying question Mario. It's some concept that is natural to us -- you exchange something with something that's equiv and then an algorithm goes off in our heads which just transfers a whole bunch of structure from one thing to the other effortlessly

[Mario Carneiro]

but to be perfectly honest, the "Kenny method", which I used also in metamath days, actually gets things done

[Mario Carneiro]

It's only after you find yourself doing exactly the same thing ~20 times that you should start considering the tactic approach

[Kevin Buzzard]

That's the point. I wonder if this is what I'm staring at.

[Mario Carneiro]

with less than that, the time it takes to figure out how to write a tactic eclipses the time it would have taken to just copy paste get it over with

[Kevin Buzzard]

I'm running into it again and again, constantly proving trivial things

[Kevin Buzzard]

and the reason I'm interested

[Mario Carneiro]

That's not the same

[Kevin Buzzard]

is that the tactic formalises something which I do naturally in my brain

[Mario Carneiro]

if it's different trivial things, the tactic won't help

[Kevin Buzzard]

and I like formalizing stuff

[Mario Carneiro]

it will handle one kind of trivial and leave untouched 60 others

[Kevin Buzzard]

This is the point at which I stop understanding

[Kevin Buzzard]

and the only way I will understand

[Kevin Buzzard]

is by trying to do it and failing

[Mario Carneiro]

How many other proofs look like the proof of comm_monoid pnat?

[Kevin Buzzard]

so I want to finally understand how difficult it is to write schoolkid.

[Kevin Buzzard]

I don't know Mario. That's what I want to find out.

[Kevin Buzzard]

Instead of saying "Mario go write schoolkid like I told you, it should be there"

[Mario Carneiro]

it should already be in your file staring back at you before you want to consider writing a tactic automating it

[Kevin Buzzard]

I should just try to write it myself

[Mario Carneiro]

Another way to put it: Tactics are a refactoring technique. You should already have a repetitive proof, and now you want to get the same thing done but easier

[Reid Barton]

I also wonder whether you really need a tactic, or just a lemma/instance "a subtype of a monoid is a monoid if it's closed under multiplication and contains the identity"

[Mario Carneiro]

^ this. In this world of automation, lemmas are unsung heroes

[Andrew Ashworth]

that might be true in this case, but i think knowing how to write a tactic is a useful and core lean skill. Even if you don't write tactics, you should understand how they work so you can understand why they fail

[Andrew Ashworth]

obviously there is chapter 8 in programming in lean. now if you don't want to write anything complicated, the way forward is to browse through how the tactics are written in core lean, starting with the most basic ones like intro.

[Andrew Ashworth]

(this is all on my to-do list as well, haha)

[Andrew Ashworth]

for references there is John Harrison's "Practical Logic and Automated Reasoning", Chlipala's "Certified Programming with Dependent Types", although in Coq, is handy

[Andrew Ashworth]

for some applications I have "Term Rewriting and All That", "Decision Procedures: An Algorithmic Point of View", "Modern Computer Algebra"

[Andrew Ashworth]

All the way at the bottom of my very sad to-do list is: "learn Isabelle and study sledgehammer and nitpick" (some other popular and useful tactics...)

[Andrew Ashworth]

since i only make progress with Lean on the weekends, I'll see you guys in a few years :)

[Johan Commelin]

But the intro tactic is written in C++, right? At least I found https://github.com/leanprover/lean/tree/dac6eec55661d3a2dab56859ffc05aef1aabb185/src/library/tactic, and it contains a lot of cpp files.

[Andrew Ashworth]

try library/init/meta/interactive.lean

meta def intro : parse ident_? → tactic unit
| none     := intro1 >> skip
| (some h) := tactic.intro h >> skip

[Johan Commelin]

So what is the relation between this lean-file and the cpp-files that I found?

[Simon Hudon]

The tactics that you found are declared in Lean as constants:

meta constant intro_core    : name → tactic expr
meta constant intron        : nat → tactic unit

That is, they do not have Lean definitions and Lean simply executes the C++ implementation when they are called.

[Kevin Buzzard]

Dumb question:

[Kevin Buzzard]

what's the quickest way to generate a complete "blank" construction of a comm_ring

[Kevin Buzzard]

I want

[Kevin Buzzard]

{mul := _,

[Kevin Buzzard]

mul_assoc := _,

[Kevin Buzzard]

etc etc

[Sebastian Ullrich]

{..}

[Simon Hudon]

You should look into pexpr.mk_structure_instance

[Kevin Buzzard]

Possibly first stupid question of many

[Kevin Buzzard]

instance semigroup [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{ mul := begin intros, sorry end,
mul_assoc := sorry
}

[Kevin Buzzard]

I am just trying to play with structures to see how far I can get in tactic mode

[Kevin Buzzard]

but Lean doesn't like that instance

[Kevin Buzzard]

type mismatch at field 'mul_assoc'
  sorry
has type
  ∀ (a b c : Π (i : I), f i), ?m_1 (?m_1 a b) c = ?m_1 a (?m_1 b c)
but is expected to have type
  ∀ (a b c : Π (i : I), f i), a * b * c = a * (b * c)

[Kevin Buzzard]

@Sebastian Ullrich thanks -- that comment helped!

[Kevin Buzzard]

I'm still stuck though

[Kevin Buzzard]

fixed it

[Kevin Buzzard]

instance semigroup [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
{
mul_assoc := λ a b c,sorry,
mul := begin intros, sorry end,
}

[Kevin Buzzard]

I think Mario once explained to me what was going on there but I still find it confusing

[Kevin Buzzard]

I am experimenting with algebra.pi_instances

[Kevin Buzzard]

I kind of suspect that Kenny will know all the answers to my questions

[Kevin Buzzard]

@Kenny Lau what's your golf proof of instance comm_ring [∀ i, comm_ring $ f i] : comm_ring (Π i : I, f i)?

[Kevin Buzzard]

Product of commutative rings is a ring.

[Kevin Buzzard]

Do you have to write as many lines as there are axioms (plus a few more lines on top)?

[Kevin Buzzard]

Or can you do tricks -- but you can't use Simon's tactic, just stuff like simp

[Kevin Buzzard]

you can write tools

[Kevin Buzzard]

but in tactic mode, not new tactics

[Kenny Lau]

instance pi.comm_ring {I : Type*} {f : I → Type*} [∀ i, comm_ring $ f i] : comm_ring (Π i : I, f i) :=
by refine
{ add := λ x y i, x i + y i,
  zero := λ i, 0,
  neg := λ x i, -x i,
  mul := λ x y i, x i * y i,
  one := λ i, 1,
  .. };
{ intros, funext,
  { apply add_assoc <|> apply add_zero <|> apply zero_add
    <|> apply add_left_neg <|> apply add_comm
    <|> apply mul_assoc <|> apply mul_one <|> apply one_mul
    <|> apply left_distrib <|> apply right_distrib
    <|> apply mul_comm } }

[Kevin Buzzard]

Kenny I want to play with the add/zero/neg etc part of your code

[Kevin Buzzard]

but if I try this

[Kevin Buzzard]

instance pi.comm_ring {I : Type*} {f : I → Type*} [∀ i, comm_ring $ f i] : comm_ring (Π i : I, f i) :=
by refine
{ add := begin intros,sorry,end,-- λ x y i, x i + y i,
  zero := λ i, 0,
  neg := λ x i, -x i,
  mul := λ x y i, x i * y i,
  one := λ i, 1,
  .. };
{ intros, funext,
  { apply add_assoc <|> apply add_zero <|> apply zero_add
    <|> apply add_left_neg <|> apply add_comm
    <|> apply mul_assoc <|> apply mul_one <|> apply one_mul
    <|> apply left_distrib <|> apply right_distrib
    <|> apply mul_comm } }

[Kenny Lau]

how do you want to play with them?

[Kevin Buzzard]

then there's no definition of add so your tactic doesn't finish the job and the errors from this for some reason stop Lean from processing add

[Kenny Lau]

what do you want to change it to?

[Kevin Buzzard]

I want to change it into a begin end tactic

[Kevin Buzzard]

of the form "intros,funext,apply has_add.add end"

[Kenny Lau]

trust the force, Luke

[Kevin Buzzard]

Can you write a tactic which does add,zero,neg,mul and one?

[Kenny Lau]

not really

[Kevin Buzzard]

In every case it's "deduce it from the factors"

[Mario Carneiro]

I'm not clear on why we're rehashing this. You are rediscovering Simon's tactic

[Kevin Buzzard]

namespace pi
variable {I : Type}     -- The indexing type
variable {f : I → Type} -- The family of types already equiped with instances

class notation_crazy_structure_that_someone_else_wrote (α : Type) extends has_add α,
has_mul α, has_zero α, has_one α, has_neg α, has_le α :=
(a : α)
(H : a + a * 0 ≤ -1)

instance can_a_tactic_prove_me [∀ i, notation_crazy_structure_that_someone_else_wrote $ f i] :
notation_crazy_structure_that_someone_else_wrote (Π i : I, f i) := sorry

[Kevin Buzzard]

I'm trying to learn it

[Kevin Buzzard]

I can't prove that with pi_instance

[Kevin Buzzard]

I am hoping I can just have a proof of the form "by canonical"

[Kevin Buzzard]

I have to learn it because I can't keep pestering Simon every time I want it to do a bit more

[Kevin Buzzard]

no extra inputs or anything

[Kevin Buzzard]

because isn't it true that all that structure just transfers over completely canonically?

[Kevin Buzzard]

@Simon Hudon can pi_instance do this without being fed any extra information whatsoever?

[Kevin Buzzard]

Lean needs to get better at doing stuff which mathematicians find trivial

[Simon Hudon]

Do what specifically?

[Simon Hudon]

(deleted)

[Kevin Buzzard]

construct the instance above called can_a_tactic_prove_me

[Kevin Buzzard]

Is it possible to write a tactic which proves a goal like that without any extra prodding?

[Simon Hudon]

I think so.

[Kevin Buzzard]

By generalising your pi_instance tactic?

[Simon Hudon]

I'm working on a set of tactics to replace pi_instance. It would be the dual of cases / case which I call refine_struct/ field / apply_field. Basically, you write refine_struct { .. } ; intro ; apply_field. Maybe you'd need a bit more but you would have a generic way of referring to the field that you're looking into

[Kevin Buzzard]

oh wow!

[Simon Hudon]

I've been procrastinating with writing my dissertation and working but I should get back to it

[Kevin Buzzard]

Yes that's exactly the sort of conclusion I was coming to (that's why I was asking about ..). I wanted to do begin refine { .. },... but was having trouble with it

[Kevin Buzzard]

Well can I write these tactics somehow?

[Kevin Buzzard]

Or Kenny when he's finished doing my project?

[Simon Hudon]

It is actually some pretty tricky stuff so it would be easier for me to just do it than to explain how to do it. Although, I'd like to also write a tutorial about it

[Kevin Buzzard]

Darn it I need a route into this stuff

[Simon Hudon]

In the mean time, I have a goodie coming up: a tactic that asserts that subtractions have non-negative results (they don't hit the floor of natural numbers) and a tactic that assert that all divisors are non-null

[Kevin Buzzard]

I need to find a tactic which I can write and is somehow distantly related to what I want to be able to do with tactics

[Kevin Buzzard]

subtractions -- Patrick will be over the moon!

[Simon Hudon]

If you want, I can show you my subtraction tactic and let you figure out the version for division

[Kevin Buzzard]

I could have a look!

[Kevin Buzzard]

Somehow it's the canonical stuff that I'm interested in though

[Simon Hudon]

What do you mean by canonical?

[Simon Hudon]

Feel free to try your hand on https://gist.github.com/cipher1024/72af1694ce395d7162bab1a72c1f9c56

[Patrick Massot]

Thanks Simon! I'll have a very close look at that (but probably not today :disappointed: )