Zulip Chat Archive

Stream: general

Topic: how does tactic.ring work?


view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:28):

I have read through programming in Lean a couple of times and now wonder if it's time I started reading something else. I decided to read the ring tactic (not least because it failed to prove something relatively simple the last time I tried to use it and I'd rather fix it myself than pester Mario, not that I have any idea about how far I need to go before I am anywhere close to being able to fix it).

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:28):

Anyway, I started to read it:

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:28):

https://github.com/kbuzzard/mathlib/blob/tactic_doc/docs/ring_tactic.rst

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:28):

There are my comments on the first 30 or so lines, plus a long intro summarising programming in lean

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:29):

There's a link to programming in lean: https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:30):

Here's Patrick's secret gem: https://hanoifabs.files.wordpress.com/2018/05/slides.pdf (thanks Johannes)

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:30):

and that is pretty much every online resource for Lean tactics. Here's the file I want to understand:

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:31):

https://github.com/leanprover/mathlib/blob/master/tactic/ring.lean

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 08:31):

if anyone wants to help me understand it, they're welcome to edit the rst file. Note: I wrote ring_ractic.rst in sphinx not markdown. It's still human-readable and pretty easy to pick up.

view this post on Zulip Johan Commelin (Jun 11 2018 at 10:42):

Typo: "especially if one does it within Lean (thus gaining the ability to hover over or click on functions and see their type, definition and so on)." <-- you mean VScode instead of Lean, right?
Another typo: "Note that evem though" <-- s/evem/even/

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 12:15):

Thanks. I had a look through all of tactic.ring and really it doesn't look too bad. I'm currently reading http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf Assia's take on the matter (which I think was Mario's source for his code)

view this post on Zulip Kevin Buzzard (Jun 11 2018 at 16:25):

in fact I know it was Mario's source for the code because I've just noticed that it says this in the comments at the top.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:41):

import tactic.ring
variables (R : Type) [comm_ring R]

example (a b : R) :
  a * (b * b) + (b * (a * a) + (b * (b * b) + (a * (2 * a * b) + b * (2 * a * b)))) =
  b * (b * b) + (3 * a * (b * b) + 3 * (a * a) * b) :=
begin
  ring,
  -- goal now (b * a + (2 * b * a + 3 * b ^ 2)) * a + b ^ 3 = (3 * b * a + 3 * b ^ 2) * a + b ^ 3
  simp,
  -- goal now (b * a + (2 * b * a + 3 * b ^ 2)) * a = (3 * b * a + 3 * b ^ 2) * a
  ring -- works
end

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:41):

elaboration: tactic execution took 2.23s
num. allocated objects:  8522
num. allocated closures: 2163
 2229ms   100.0%   scope_trace
 2229ms   100.0%   tactic.istep._lambda_1
 2229ms   100.0%   tactic.istep
 2229ms   100.0%   tactic.step
 2229ms   100.0%   _interaction._lambda_2
 1987ms    89.1%   interaction_monad_orelse
 1929ms    86.5%   tactic.ring.eval
 1156ms    51.9%   tactic.interactive.ring1
 1156ms    51.9%   tactic.interactive.ring._lambda_1
 1156ms    51.9%   tactic.interactive.ring
 1057ms    47.4%   tactic.ring.eval_mul

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:41):

etc etc

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:41):

This tactic doesn't quite work yet as far as I can see.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:42):

(noticable pause in ring whilst it's failing to prove it the first time)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:42):

But I want to fix it.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:42):

I re-read the "rings done right" paper and I understood _much_ more of it this time around.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:43):

One insight which dawned on me is that there are two completely different issues involved with writing a ring tactic. Maybe everyone else is aware of this.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:43):

Let me explain my understanding of what the ring tactic does.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:43):

Let's say d : int and we want to prove d^2 + 2*d + 1 = (d+1)^2

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:44):

If we want to prove this using ring then we are saying "this is not true because of something specific to int, this is a general fact about rings"

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:44):

So what we actually want to do is to prove that X2+2X+1=(X+1)2X^2+2X+1=(X+1)^2 in Z[X]\mathbb{Z}[X]

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:45):

and then deduce our goal by specialising to X=dX=d

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:45):

This makes it clear what we have to do here.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:46):

First we need to build a new type in Lean corresponding to polynomials in one variable

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:46):

or more generally, if we want to prove stuff like (a+b)^2=a^2+2*a*b+b^2 for ints a,b

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:46):

we will need polynomials in a finite set of variables.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:46):

Of course Lean has these.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:47):

Once we have this new type, we need to prove an "evaluation theorem", saying that if f(X)=g(X)f(X)=g(X) in our polynomial ring

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:47):

then f(d)=g(d)f(d)=g(d) in int

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:48):

Along the way it would be natural to prove things like f(d)+g(d)=(f+g)(d)f(d)+g(d)=(f+g)(d) and so on

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:49):

So we define our new polynomial type, define evaluation, prove nice properties about the evaluation map

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:49):

and now all that's left is the following problem:

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:49):

given d^2+2*d+1 with d : int

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:49):

we need to manufacture X^2+2*X+1 in our polynomial ring type.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:50):

And for this we really need to take apart d^2+2*d+1 and see how it is built from d and stuff that has analogues in the polynomial ring.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:50):

(+,^,2,1)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:51):

and I think that it's at this point that the non-tactic-user gets stuck.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:56):

@Simon Hudon Assume Lean has a working polynomial ring type ZX (there are some kicking around, but perhaps none in mathlib) representing polynomials with integer coefficients in one variable X. Am I right in thinking that it doesn't even make sense to ask for a function (in Lean's sense) which sends d^2+2*d+1 to X^2+2*X+1 where d : int is some variable? I can't even imagine what the domain of such a function would be. On the other hand, would I be able to write a tactic which took the expression d^2+2*d+1 as an input and spat out X^2+2*X+1?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 09:57):

Or is life not even that easy?

view this post on Zulip Scott Morrison (Jun 12 2018 at 10:34):

certainly given d^2+2*d+1 as an expr (and let's say d is also given, as an expr), in meta land we can construct X^2+2*X+1.

view this post on Zulip Scott Morrison (Jun 12 2018 at 10:35):

(Mario's implementation does clever things, including a representation of sparse polynomials, but if you just want the stupid version I could probably manage that function.)

view this post on Zulip Simon Hudon (Jun 12 2018 at 12:04):

Is this simply renaming variables in the goal?

view this post on Zulip Scott Morrison (Jun 12 2018 at 12:16):

Sorry, the example wasn't very helpful: I just meant, determine if some expression is in fact a polynomial in some other expr, and if so, present it as such in some form (list of coefficients, map of coefficients, etc).

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:47):

Is this simply renaming variables in the goal?

@Simon Hudon No I think it's more. X is a genuine polynomial variable, we have a type ZX with an inclusion from int into ZX and also some element X : ZX which is not in the image of int, it's an abstract polynomial variable

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:47):

@Scott Morrison do we _have_ to do this in meta-land?

view this post on Zulip Simon Hudon (Jun 12 2018 at 12:48):

ah! i see. So a kind of parser.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:48):

I can see that Mario's implementation uses "Horner form" of a polynomial, so sparse polys are handled better.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:48):

Yes, I was interested in building the stupid version of tactic.ring

view this post on Zulip Simon Hudon (Jun 12 2018 at 12:48):

Yes, I think it has to be in meta because you need access to the expr syntax tree

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:48):

What I see in Mario's file seems to me to be a construction of an abstract polynomial ring but completely in meta-land

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:49):

Here is a concrete question.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:49):

Would it be possible to just define the polynomial ring Z[X] in "normal" Lean

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:49):

e.g. in a non-efficient way, using lists for coefficients

view this post on Zulip Simon Hudon (Jun 12 2018 at 12:49):

I believe so

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:49):

and then write a much simpler tactic than tactic/ring.lean

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:50):

which can prove statements of the form "forall d : int, (d+1)^3=d^3+3d^2+3d+1"

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:50):

by temporarily dipping into meta-land to construct the polynomials (X+1)^3 and X^3+3X^2+3X+1

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:50):

and then checking that they're equal in Z[X]

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:50):

and then evaluating at d

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:50):

and deducing the result?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:51):

Or is it an essential part of the tactic.ring tactic that one builds some version of Z[X] in meta-land?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:52):

It seems to me that Mario writes horner in normal-land and proves some lemmas about it in normal-land

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:53):

but the key facts are things like eval_add, which is meta

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:57):

eval_add seems to be some sort of theorem of the form "if this expr represents f and this expr represents g, then I will return an expr plus a proof that it is the evaluation of f plus the evaluation of g"

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:58):

I was wondering whether one could instead use a non-expr version

view this post on Zulip Simon Hudon (Jun 12 2018 at 12:58):

Because expr is in meta land, you can't do any of that stuff in non-meta land

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:58):

right

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:58):

but if I had a tactic which took d^2+2*d+1

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:59):

and returned X^2+2*X+1

view this post on Zulip Simon Hudon (Jun 12 2018 at 12:59):

I see ok yes that's possible

view this post on Zulip Simon Hudon (Jun 12 2018 at 12:59):

That's called a proof by reflection

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:59):

plus a proof that X^2+X+1 evaluated at d was d^2+2*d+1

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 12:59):

then it seems to me that there's a chance that I can prove d^2+2*d+1=(d+1)^2 using this tactic

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:00):

because I feed in both sides to the tactic

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:00):

prove they're equal in ZX

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:00):

and deduce that their valuations are equal

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:00):

I am trying to get as much of the proof out of meta-land as I can

view this post on Zulip Reid Barton (Jun 12 2018 at 13:01):

Regarding lands, have you looked at the slides on metaprogramming https://hanoifabs.files.wordpress.com/2018/05/slides.pdf?

view this post on Zulip Reid Barton (Jun 12 2018 at 13:01):

In particular page 4

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:01):

This is part of the reason I'm thinking about this now

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:02):

I have looked through all of tactic/ring.lean and all of a sudden it doesn't look as intimidating as it used ti

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:02):

to

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:04):

https://github.com/kbuzzard/mathlib/blob/ring_tactic_comments/tactic/ring.lean

view this post on Zulip Reid Barton (Jun 12 2018 at 13:04):

If you don't need access to meta-land features like general recursion or expr then you can stay in normal-land; and surely the theory of Z[X]\mathbb{Z}[X] doesn't need these things. On the other hand, you may want to avoid using noncomputable things if you want your tactic to, for example, be able to decide whether two polynomials in Z[X]\mathbb{Z}[X] are equal so that it can decide whether to succeed or fail.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:04):

I am trying to write a comment about every definition and theorem in that link

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:05):

So one can certainly make Z[X], indeed it's been done several times although I don't think it's in mathlib yet

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:05):

The problem is the function sending d^2+2d+1 to X^2+2X+1

view this post on Zulip Reid Barton (Jun 12 2018 at 13:06):

Right, so I guess the approach used here by ring is to represent a variable (which is basically something the tactic can't break down into further ring operations) by its expr

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:07):

right

view this post on Zulip Reid Barton (Jun 12 2018 at 13:07):

Here the variable is simply d, but it could have been more complicated, e.g. sin t

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:07):

right

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:07):

or there could be several variables

view this post on Zulip Reid Barton (Jun 12 2018 at 13:09):

So that must be why the destruct_ty thing is in meta, though if you wanted it to be in normal-land, you could probably just parameterize it on the expression type.

view this post on Zulip Reid Barton (Jun 12 2018 at 13:09):

BTW, _ty probably just stands for "type"

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:11):

So completely independent of the ring tactic

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:11):

there is this horner thing

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:11):

and what seems to be going on there

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:11):

is that (and this is Assia's insight, or her joint insight with her co-author)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:11):

storing polynomials as lists of coefficients might suck

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:12):

especially if you want to work out x^100 * x^100 without doing 10000 computations

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:12):

so they store e.g. x^100+3x^2+7 as (1*x^98+3)*x^2+7

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:12):

iterating the "x maps to a*x^n+b" map

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:13):

and so this is some sort of normal form for polynomials

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:13):

which we could call "horner normal form"

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:13):

and if you store polynomials in this way then it's a PITA to add or multiply them

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:13):

but this is OK because somehow this isn't the bottleneck

view this post on Zulip Reid Barton (Jun 12 2018 at 13:14):

I see, and eval_add is basically implementing addition of polynomials in this form, it looks like?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:14):

So one could envisage writing a second ring tactic which (a) was far less efficient and (b) worked in some situations where Mario's doesn't (because Mario's is currently buggy)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:14):

where you just use lists for coefficients

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:15):

and then the resulting tactic file would have this extra obfuscating layer of difficulty removed

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:15):

and this was what got me into wondering whether I could even just use one of the already-existing polynomial ring Lean implementations

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:15):

instead of making Z[X] in meta-land

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:17):

I see, and eval_add is basically implementing addition of polynomials in this form, it looks like?

Yes, it's perhaps doing something clever like not just implementing addition, it's also collecting the proofs that addition commutes with evaluation, but the five lemmas before eval_add are precisely the five lemmas you need to add polynomials in "Horner form"

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:18):

You add ax^n+b and a'x^n'+b'

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:18):

where a and a' are allowed to be polynomials in horner form

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:18):

and you have to do the three cases n<n', n=n', n>n'

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:18):

and then also you have to add ax^n+b to c where c is a constant

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:18):

both ways around

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:18):

and there's some implicit inductive type horner_form

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:19):

which is defined by: a constant is in horner_form, and if a is in horner_form then so is a*x^n+b

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:19):

and then every polynomial has a canonical horner form

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:19):

and also perhaps some non-canonical ones

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:22):

I haven't got down as far as normalize but this might be the function which puts something in horner form into its normalised state (which you need because you need an algorithm for figuring out when two polynomials are equal)

view this post on Zulip Reid Barton (Jun 12 2018 at 13:25):

and this was what got me into wondering whether I could even just use one of the already-existing polynomial ring Lean implementations

I don't see why not. Probably you can even use the one in linear_algebra.multivariate_polynomial

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:29):

You understand that I am not looking for some sort of uber-efficient ring tactic, like the one Mario wrote. I am trying to see in some sense what the minimal amount of work would be, if I wanted to write a more inefficient ring tactic of my own

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:29):

and the more I can get out of meta-land the better

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:29):

Even for just equations involving one unknown, I would be interested

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:30):

not least because example (d : ℕ) : d^2+2*d+1=(d+1)^2 := by ring currently fails and rather than pestering Mario I thought it would be an interesting exercise to try and work out why.

view this post on Zulip Reid Barton (Jun 12 2018 at 13:31):

Yes, I think a ring tactic optimized for simplicity would be valuable as a demonstration of how to write similar tactics, as well.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 13:43):

Well maybe that's where this thread is going.

view this post on Zulip Mario Carneiro (Jun 12 2018 at 13:47):

I'm not sure you can actually save that much work with a dumber ring tactic

view this post on Zulip Mario Carneiro (Jun 12 2018 at 13:48):

Probably using dense polynomial representation is a bit easier, but I don't think proof by reflection is easier (although more of it can be verified)

view this post on Zulip Mario Carneiro (Jun 12 2018 at 13:48):

but precisely because more of it is verified, there is more work to do

view this post on Zulip Mario Carneiro (Jun 12 2018 at 13:49):

If expr was not meta, almost all of the ring tactic could be non-meta

view this post on Zulip Simon Hudon (Jun 12 2018 at 13:50):

Do you know if there's any plan to make expr non-meta?

view this post on Zulip Mario Carneiro (Jun 12 2018 at 13:51):

I have not investigated the ring bug, but one way to find out what is happening is to insert type checks in eval_add and such

view this post on Zulip Reid Barton (Jun 12 2018 at 13:51):

By "simple", I really mean "easy to understand"

view this post on Zulip Reid Barton (Jun 12 2018 at 13:51):

not necessarily short

view this post on Zulip Mario Carneiro (Jun 12 2018 at 13:51):

There is no plan to make expr non-meta, and in fact I attempted such a plan and was rebuffed several months ago

view this post on Zulip Mario Carneiro (Jun 12 2018 at 13:52):

The likely alternative is to have a mirror copy of expr that is non-meta

view this post on Zulip Mario Carneiro (Jun 12 2018 at 13:52):

which would have to avoid certain meta things like macros

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:01):

I'm not sure you can actually save that much work with a dumber ring tactic

Yes, as Reid says, I'm not worried about work, I'm attempting to understand tactics in a way other than "read Programming In Lean again".

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:02):

The only other way I can think of is "read some tactic code and see if you can understand it, and see what questions arise because of it"

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:02):

and that's why I find myself in this thread

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:03):

One question: which is best? Documenting ring.lean like this https://github.com/kbuzzard/mathlib/blob/ring_tactic_comments/tactic/ring.lean

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:03):

or writing a stand-alone file with comments like this https://github.com/kbuzzard/mathlib/blob/tactic_doc/docs/ring_tactic.rst

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:03):

I currently find myself doing both

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:03):

As long as I get to the bottom using one method, I am sure I will have learnt a lot

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:04):

Currently the "adding comments to ring.lean" approach is winning

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:05):

but the waffle above about writing a simpler version -- which to be honest could I think turn into a great tutorial on how to write tactics, if we implement polynomials in one variable using some dumb list method or, even better, perhaps using some already-implemented method

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:06):

Maybe that's the goal of this thread. To write an as-stupid-as-possible ring tactic which attempts to have as little in meta-land as possible, and then stick it up on my blog as some sort of tactic tutorial as an alternative for people to read

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:07):

Next term I'll be supervising a Masters project on how to write tactics so I'd better get my act together and learn it myself

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 14:07):

The student in question is currently doing an internship at INRIA learning how to do it in Coq so I'm hoping that they will learn quickly and then teach me

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:01):

Maybe this will help: There is an implicit inductive type horner_form_expr with the following definition:

meta inductive horner_form_expr : Type
| const : expr → horner_form_expr
| horner (a : horner_form_expr) (x : expr) (n : nat) (b : horner_form_expr) : horner_form_expr

The job of eval_add and the other definitions is to rewrite any expr into a horner_form_expr. However, since horner_form_expr can be represented as an expr, the actual inductive type is omitted to avoid the overhead of converting back and forth. Furthermore, there is a normal form requirement, that says that the x expression must be lex_lt less than any other expressions in x slots of the b subtree.

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:03):

destruct is effectively the cases_on for this inductive type

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:38):

Right -- I had basically figured this out. But you see, in some educational blog post about this stuff you could put this type in, and furthermore make it work in a more stupid way using lists of coefficients. What I am still not clear about is whethet you can get away with making it not meta (and hence get away with not actually writing it at all, because it's already written)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:39):

Because you're in meta-land you can just not even define the type, you can destruct it _assuming_ that it's in this form, and if it's not then big deal, things have gone wrong, just return none

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:40):

You can't make it non-meta and still retain the x payloads, which have to be kept as is as exprs

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:41):

My idea was to have a meta function sending d^2+2d+1 to X^2+2X+1

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:41):

unless maybe you write them down somewhere else and only keep pointers to them in your non-meta data structure (i.e. indexes into a list of exprs)

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:42):

which I guess is similar to your Z[X] suggestion

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:42):

The tactic would only work for goals with one unknown

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:42):

but you have to remember these are multivariate polynomials

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:42):

I know yours are

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:42):

but I am suggesting writing a simplified version

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:43):

I want to isolate the "now here we have to write some meta stuff" and make it as small as possible

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:43):

If you take d as an input, then there are lots of bad exprs now

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:43):

In my approach, there aren't any bad exprs because anything it doesn't understand becomes a new atom

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:44):

I know your approach is better at getting things done

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:44):

I am happy to let both d and Z be inputs

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:44):

but you want to have only one atom

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:44):

right

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:44):

and I want to store polynomials as lists

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:44):

these facts are not unrelated

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:44):

what happens if I pass d^2+x to your function?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:45):

my function will fail

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:45):

because my function is there to teach people how to write tactics

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:45):

not to actually be used in the wild

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:45):

I am writing code for a completely different reason to probably any code you ever wrote

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:45):

I am writing code to teach my students that tactics are not scary

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:46):

which is not the impression you get when reading PIL

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:46):

Okay, let me think about this

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:46):

In the mean time, the ring bug has been fixed.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:47):

:D

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:47):

OK so forget this thread, main goal achieved ;-)

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:47):

The problem was in horner_add_horner_lt (and gt). Suppose we are adding (a1 * x^n1 + b1) + (a2 * x^n2 + b2) where n1 > n2

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:47):

dammit I even looked at that function!

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:47):

It's funny, the theorem is not wrong

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:48):

but it doesn't normalize like it should

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:48):

in fact that's exactly the point I'm up to

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:48):

/-- This non-meta theorem just says a₁x^n₁+b₁+a₂x^(n₁+k)+b₂=(a₂x^k+a₁)x^n₁+(b₁+b₂) -/

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 15:49):

I think this is a great idea. It took me some time to understand reflection in Lean. Unfortunately, translating Chlipala's section on it (in CPDT) from Coq to Lean is quite difficult. So a "Lean-first" tutorial would be great.

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:49):

The current implementation normalizes b1 + b2 = b', calculates k such that n2 + k = n1, and then outputs the normal form (a1 * x^k + a2) * x^n2 + b'

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:50):

yeah (modulo the fact that the (1,2) notation is switched in this thread from the conventions used in the actual code)

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:50):

However, a1 * x^k + a2 is not necessarily in normal form

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:50):

because x might not be lt the monomials showing up in a1?

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:51):

Yes. In particular, x might appear in a2

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:51):

or a1

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:51):

;-)

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:51):

that's okay

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:52):

not when you switch it so your algebra is correct ;-)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:52):

[you only did half the editing job]

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:52):

the whole point of factorizing a1 * x^k + a2 is that a2 has no x's and a1 has all the high order terms

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:53):

a2 * x^k + a1

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:53):

I think this part of the thread is now beyond saving

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:54):

but I think we both know what the other is saying :-)

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:55):

fixed

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:55):

I actually noticed the problem in gt, but I was translating to the symmetric version and got confused

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:56):

(in this thread, that's not the bug)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:57):

[I posted my docstring for lt, but you are talking about gt, so now all is right with the world]

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:57):

Right, so let's focus on gt

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:57):

the bug is that since both a1 and a2 can contain x, we have a separate subproblem now, to normalize (a1 * x^k + 0) + a2 = a' and then output a' * x^n2+ b'

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:57):

/-- This non-meta theorem just says a₁x^(n₂+k)+b₁+a₂x^n₂+b₂=(a₁x^k+a₂)x^n₂+(b₁+b₂) -/

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:58):

so I did that and now it works

view this post on Zulip Mario Carneiro (Jun 12 2018 at 15:58):

I'm compiling now, I'll post it soon

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:58):

I would have liked to find this bug

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:59):

Because you're in meta mode you don't have to be super-anal about making sure everything is in canonical form

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 15:59):

you just write procedural code which is supposed to do it

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 16:00):

@Andrew Ashworth I did the introductory compiler exercise in CPDT, in Lean, over the weekend.

view this post on Zulip Mario Carneiro (Jun 12 2018 at 16:00):

I'll help you with a tutorial ring tactic later

view this post on Zulip Mario Carneiro (Jun 12 2018 at 16:01):

But one thing to be careful about is if you do too much non-meta, you might actually end up writing a tactic that does proof by reflection which is a completely different method

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 16:01):

reflection is _different_? I thought that it was somehow some fundamental principle which was used everywhere?

view this post on Zulip Mario Carneiro (Jun 12 2018 at 16:01):

ring is an example of how to write tactics that build proofs by induction, but it's hard to do that non-meta

view this post on Zulip Mario Carneiro (Jun 12 2018 at 16:04):

One way to see the difference is in the proof: A tactic that does proofs by meta-induction produces proofs that get longer as the theorem gets harder to prove, but a proof by reflection is relatively short, with the generated proof being proportional to the statement in length

view this post on Zulip Mario Carneiro (Jun 12 2018 at 16:05):

Proofs by reflection are characterized by a "heavy" rfl proof somewhere in the middle

view this post on Zulip Mario Carneiro (Jun 12 2018 at 16:05):

ring produces no heavy steps, every single theorem applied exactly matches the type it should have

view this post on Zulip Mario Carneiro (Jun 12 2018 at 16:06):

so the kernel never has to do any definitional reduction

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 16:16):

This is all very instructive and quite different from the PIL stuff which, inevitably, is skewed towards CS applications

view this post on Zulip Mario Carneiro (Jun 12 2018 at 17:33):

@Kevin Buzzard Here's a toy version of ring that works using computational reflection:

import tactic.basic data.num.lemmas

namespace ring_tac
open tactic

@[derive has_reflect]
inductive ring_expr : Type
| add : ring_expr → ring_expr → ring_expr
| mul : ring_expr → ring_expr → ring_expr
| const : znum → ring_expr
| X : ring_expr

meta def reflect_expr (X : expr) : expr → option ring_expr
| `(%%e₁ + %%e₂) := do
  p₁ ← reflect_expr e₁,
  p₂ ← reflect_expr e₂,
  return (ring_expr.add p₁ p₂)
| `(%%e₁ * %%e₂) := do
  p₁ ← reflect_expr e₁,
  p₂ ← reflect_expr e₂,
  return (ring_expr.mul p₁ p₂)
| e := if e = X then return ring_expr.X else
  do n ← expr.to_int e,
     return (ring_expr.const (znum.of_int' n))

def poly := list znum

def poly.add : poly → poly → poly := λ _ _, []
def poly.mul : poly → poly → poly := λ _ _, []
def poly.const : znum → poly := sorry
def poly.X : poly := sorry

def to_poly : ring_expr → poly
| (ring_expr.add e₁ e₂) := (to_poly e₁).add (to_poly e₂)
| (ring_expr.mul e₁ e₂) := (to_poly e₁).mul (to_poly e₂)
| (ring_expr.const z) := poly.const z
| ring_expr.X := poly.X

def poly.eval {α} [comm_ring α] (X : α) : poly → α
| [] := 0
| (n::l) := n + X * poly.eval l

@[simp] theorem poly.eval_add {α} [comm_ring α] (X : α) : ∀ p₁ p₂ : poly,
  (p₁.add p₂).eval X = p₁.eval X + p₂.eval X := sorry

@[simp] theorem poly.eval_mul {α} [comm_ring α] (X : α) : ∀ p₁ p₂ : poly,
  (p₁.mul p₂).eval X = p₁.eval X * p₂.eval X := sorry

@[simp] theorem poly.eval_const {α} [comm_ring α] (X : α) : ∀ n : znum,
  (poly.const n).eval X = n := sorry

@[simp] theorem poly.eval_X {α} [comm_ring α] (X : α) : poly.X.eval X = X := sorry

def ring_expr.eval {α} [comm_ring α] (X : α) : ring_expr → α
| (ring_expr.add e₁ e₂) := e₁.eval + e₂.eval
| (ring_expr.mul e₁ e₂) := e₁.eval * e₂.eval
| (ring_expr.const z) := z
| ring_expr.X := X

theorem to_poly_eval {α} [comm_ring α] (X : α) (e) : (to_poly e).eval X = e.eval X :=
by induction e; simp [to_poly, ring_expr.eval, *]

theorem main_thm {α} [comm_ring α] (X : α) (e₁ e₂) {x₁ x₂}
  (H : to_poly e₁ = to_poly e₂) (R1 : e₁.eval X = x₁) (R2 : e₂.eval X = x₂) : x₁ = x₂ :=
by rw [← R1, ← R2, ← to_poly_eval, H, to_poly_eval]

meta def ring_tac (X : pexpr) : tactic unit := do
  X ← to_expr X,
  `(%%x₁ = %%x₂) ← target,
  r₁ ← reflect_expr X x₁,
  r₂ ← reflect_expr X x₂,
  let e₁ : expr := reflect r₁,
  let e₂ : expr := reflect r₂,
  `[refine main_thm %%X %%e₁ %%e₂ rfl _ _],
  all_goals `[simp only [ring_expr.eval,
    znum.cast_pos, znum.cast_neg, znum.cast_zero',
    pos_num.cast_bit0, pos_num.cast_bit1,
    pos_num.cast_one']]

example (x : ℤ) : (x + 1) * (x + 1) = x*x+2*x+1 :=
by do ring_tac ```(x)

end ring_tac

view this post on Zulip Mario Carneiro (Jun 12 2018 at 17:34):

I have left the exercise of defining poly.add, poly.mul, poly.const and poly.X, and proving correctness of the functions in the eval_* theorems (all non-meta), to you.

view this post on Zulip Mario Carneiro (Jun 12 2018 at 17:35):

Here the "heavy rfl" step is the rfl proof in main_thm

view this post on Zulip Mario Carneiro (Jun 12 2018 at 17:36):

you will need the mathlib update that just appeared

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 19:47):

wooah many thanks Mario!

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 20:11):

example (a b : int) : (a+b)^11=a^11 + 11*b*a^10 + 55*b^2*a^9 + 165*b^3*a^8 + 330*b^4*a^7 + 462*b^5*a^6 + 462*b^6*a^5 + 330*b^7*a^4 + 165*b^8*a^3 + 55*b^9*a^2 + 11*b^10*a + b^11:= by ring

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 20:11):

but 12 times out :-)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 20:11):

[this is of course the official ring, not the one above]

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 20:12):

example (a b : int) : (a+b)^12=a^12 + 12*b*a^11 + 66*b^2*a^10 + 220*b^3*a^9 + 495*b^4*a^8 + 792*b^5*a^7 + 924*b^6*a^6 + 792*b^7*a^5 + 495*b^8*a^4 + 220*b^9*a^3 + 66*b^10*a^2 + 12*b^11*a + b^12:= by ring -- deterministic timeout

view this post on Zulip Johan Commelin (Jun 12 2018 at 20:31):

@Kevin Buzzard So you need to teach ring about Chris's binomial theorem!

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 22:07):

Well, I'm not sure I would use Lean to check the binomial theorem for n=12 :-)

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 22:08):

Ironically I fired up pari-gp and computed (a+b)^12 in a gazillionth of a second and then cut and pasted the output into Lean in order to see if it could do something which I already had a much better tool for.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:06):

import tactic.basic data.num.lemmas analysis.real

namespace ring_tac
open tactic

-- why this line?
@[derive has_reflect]
inductive ring_expr : Type
| add : ring_expr  ring_expr  ring_expr
| mul : ring_expr  ring_expr  ring_expr
| const : znum  ring_expr
| X : ring_expr

meta def reflect_expr (X : expr) : expr  option ring_expr
| `(%%e₁ + %%e₂) := do
  p₁  reflect_expr e₁,
  p₂  reflect_expr e₂,
  return (ring_expr.add p₁ p₂)
| `(%%e₁ * %%e₂) := do
  p₁  reflect_expr e₁,
  p₂  reflect_expr e₂,
  return (ring_expr.mul p₁ p₂)
| e := if e = X then return ring_expr.X else
  do n  expr.to_int e,
     return (ring_expr.const (znum.of_int' n))

-- mathlib/data/num has znum and stuff like znum.of_int' (see above)
def poly := list znum
-- but why use it?

def poly.add : poly  poly  poly
| [] g := g
| f [] := f
| (a :: f') (b :: g') := (a + b) :: poly.add f' g'

@[simp] lemma poly.zero_add (p : poly) : poly.add [] p = p := by induction p;refl

def poly.smul : znum  poly  poly
| _ [] := []
| z (a :: f') := (z * a) :: poly.smul z f'

def poly.mul : poly  poly  poly
| [] _ := []
| (a :: f') g := poly.add (poly.smul a g) (0 :: (poly.mul f' g))

def poly.const : znum  poly := λ z, [z]

def poly.X : poly := [0,1]

def to_poly : ring_expr  poly
| (ring_expr.add e₁ e₂) := (to_poly e₁).add (to_poly e₂)
| (ring_expr.mul e₁ e₂) := (to_poly e₁).mul (to_poly e₂)
| (ring_expr.const z) := poly.const z
| ring_expr.X := poly.X

def poly.eval {α} [comm_ring α] (X : α) : poly  α
| [] := 0
| (n::l) := n + X * poly.eval l

@[simp] lemma poly.eval_zero {α} [comm_ring α] (X : α) : poly.eval X [] = 0 := rfl

@[simp] theorem poly.eval_add {α} [comm_ring α] (X : α) :  p₁ p₂ : poly,
  (p₁.add p₂).eval X = p₁.eval X + p₂.eval X :=
begin
  intro p₁,
  induction p₁ with h₁ t₁ H,
    -- base case
    intros,simp [poly.eval],
  -- inductive step
  intro p₂,
  cases p₂ with h₂ t₂,
    simp [poly.add],
  unfold poly.eval poly.add,
  rw (H t₂),
  simp [mul_add]
end

@[simp] lemma poly.eval_mul_zero {α} [comm_ring α] (f : poly) (X : α) :
  poly.eval X (poly.mul f []) = 0 :=
begin
  induction f with h t H,
    refl,
  unfold poly.mul poly.smul poly.add poly.mul poly.eval,
  rw H,simp
end

@[simp] lemma poly.eval_smul {α} [comm_ring α] (X : α) (z : znum) (f : poly) :
  poly.eval X (poly.smul z f) = z * poly.eval X f :=
begin
  induction f with h t H, simp [poly.smul,poly.eval,mul_zero],
  unfold poly.smul poly.eval,
  rw H,
  simp [mul_add,znum.cast_mul,mul_assoc,mul_comm]
end

@[simp] theorem poly.eval_mul {α} [comm_ring α] (X : α) :  p₁ p₂ : poly,
  (p₁.mul p₂).eval X = p₁.eval X * p₂.eval X :=
begin
  intro p₁,induction p₁ with h₁ t₁ H,
    simp [poly.mul],
  intro p₂,
  unfold poly.mul,
  rw poly.eval_add,
  unfold poly.eval,
  rw [H p₂,znum.cast_zero,zero_add,add_mul,poly.eval_smul,mul_assoc]
end


@[simp] theorem poly.eval_const {α} [comm_ring α] (X : α) :  n : znum,
  (poly.const n).eval X = n :=
begin
  intro n,
  unfold poly.const poly.eval,simp
end

@[simp] theorem poly.eval_X {α} [comm_ring α] (X : α) : poly.X.eval X = X :=
begin
  unfold poly.X poly.eval,simp
end


def ring_expr.eval {α} [comm_ring α] (X : α) : ring_expr  α
| (ring_expr.add e₁ e₂) := e₁.eval + e₂.eval
| (ring_expr.mul e₁ e₂) := e₁.eval * e₂.eval
| (ring_expr.const z) := z
| ring_expr.X := X

theorem to_poly_eval {α} [comm_ring α] (X : α) (e) : (to_poly e).eval X = e.eval X :=
by induction e; simp [to_poly, ring_expr.eval, *]

theorem main_thm {α} [comm_ring α] (X : α) (e₁ e₂) {x₁ x₂}
  (H : to_poly e₁ = to_poly e₂) (R1 : e₁.eval X = x₁) (R2 : e₂.eval X = x₂) : x₁ = x₂ :=
by rw [ R1,  R2,  to_poly_eval, H, to_poly_eval]

meta def ring_tac (X : pexpr) : tactic unit := do
  X  to_expr X,
  `(%%x₁ = %%x₂)  target,
  r₁  reflect_expr X x₁,
  r₂  reflect_expr X x₂,
  let e₁ : expr := reflect r₁,
  let e₂ : expr := reflect r₂,
  `[refine main_thm %%X %%e₁ %%e₂ rfl _ _],
  all_goals `[simp only [ring_expr.eval,
    znum.cast_pos, znum.cast_neg, znum.cast_zero',
    pos_num.cast_bit0, pos_num.cast_bit1,
    pos_num.cast_one']]

theorem X (x : ) : (x + 1) * (x + 1) = x*x+2*x+1 :=
by do ring_tac ```(x)

#print axioms X

end ring_tac

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:06):

Did my homework

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:06):

I feel like an UG again

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:08):

Notes: I had to introduce poly.smul (scalar multiplication of poly by znum) for definition of multiplication. I really tried to make simp do most of the work in general but I still had to do a lot of unfolding before I could get it going.

view this post on Zulip Kenny Lau (Jun 12 2018 at 23:08):

did you just write a tactic?

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:08):

Not really

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:08):

in the sense that no code I wrote started with meta

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:09):

but check it out

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:09):

barely any code at all has meta

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:09):

Just reflect_expr at the very top, and ring_tac at the very bottom. Mario wrote both of those

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:10):

Kenny here's the strat: to prove that for d : int we have (d+1)^2=d^2+2*d+1 we first prove that in a polynomial ring we have (X+1)^2=X^2+2X+1 and then deduce

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:10):

The problem is that if Lean just sees (d+1)^2 it can't create (X+1)^2

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:11):

so this part you have to do in meta-land

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:11):

but it's only this part

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:11):

unsurprisingly, this is what reflect_expr does

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:12):

So there's a basic one-variable ring tactic with a very small amount of meta indeed, and the meta is really not hard to comprehend. I mean, it might be hard to write, but it's not at all hard to read.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:12):

I'll write a blog post explaining it but now it's bed time. Once again many thanks Mario.

view this post on Zulip Kevin Buzzard (Jun 12 2018 at 23:14):

Just to be clear @Kenny Lau the code I posted does seem to be a fully working baby ring

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:55):

Actually it doesn't work in all cases, because there is currently no "canonical form" lemma. The polynomials [1] and [1,0] (=0*x+1) are different.

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:57):

@Mario Carneiro Here are the three questions I have about this project, which basically came up when trying to write a blog post. The first two are trivial for you: what is @[derive has_reflect] and why znum rather than int?

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:57):

The third is a bit more annoying. Because there is no algorithm to put polynomials (= lists of znums) into "canonical form", example (x : ℤ) : (x + 1) + ((-1)*x + 1) = 2 := by do ring_tac ```(x) fails

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:58):

I think this is because the polynomials [2,0] and [2] are considered distinct.

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:58):

Aah, I think I can fix this.

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:58):

I think I write some "canonical_form" function

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:58):

(not in meta land)

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:59):

and redefine add so that it puts the polynomial into canonical form afterwards.

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:59):

yeah yeah OK I think I can do this one.

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:36):

Why @[derive has_reflect]

This one is easy: otherwise you don't have a reflect instance for ring_expr. This function is used explicitly in ring_tac; the idea is that if A is a reflectable type then reflect (a : A) is an expr that denotes the same value as a

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:36):

so for example list has a reflect that just turns each cons into a expr.app ``list.cons a l

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:37):

and nat has a reflect that produces bit0 and bit1 expressions (which when printed appear as the number being denoted)

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:38):

But not all types have a reflect; in particular quotients and other things that make different expressions equal according to lean don't have a reflect, since you would have to open up the quotient to get the element to print

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:39):

In this case it is needed because reflect_expr produces a ring_expr, not an expr denoting a ring_expr

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:40):

I think in this case you could skip the extra step and just produce an expr directly, but that would be less structured and more meta

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:44):

Why znum

This one is more subtle, and actually I knew you would ask this question and I used it in part to prompt the question. You can view this as an efficiency move, but when there is an exponential performance gap I think it is close enough to essential to teach directly. Whenever you use proof by reflection, it is absolutely essential that you do everything you can to make the computation simple and direct, because you will be working with a fairly heavy handicap. A big no-no is using nat and int anywhere in your computation, because (as Seul has discovered) this works in unary and there is nothing you can do to prevent this when computing in the kernel

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:45):

This is in fact the raison d'etre for the num type - it allows for performing kernel computations on naturals and integers, with enough lemmas to relate them back to the more traditional nat type.

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:47):

It's a bit of a delicate move, since int and nat are in fact the more efficient ones in VM computations, so you want to convert from int to znum when storing the numbers inside the kernel data structure (ring_expr), but not before

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:51):

The third is a bit more annoying. Because there is no algorithm to put polynomials (= lists of znums) into "canonical form", example (x : ℤ) : (x + 1) + ((-1)*x + 1) = 2 := by do ring_tac ```(x) fails

I noticed this as well with your definition of poly.add. But there is actually another solution, which might be easier than applying a function that strips the high zeros after every operation. That is, define

def poly.is_eq : poly -> poly -> bool := sorry

so that trailing zeros are ignored in the equality test, and then replace to_poly e1 = to_poly e2 with poly.is_eq (to_poly e1) (to_poly e2) in the main_thm and prove it with this (weaker) assumption

view this post on Zulip Andrew Ashworth (Jun 13 2018 at 12:19):

So, if I defined a new poly type quotiented with this equality relation, I'd have to explicitly define my denotation function? That doesn't sound so bad, I think... or would the kernel get stuck trying to reduce it?

view this post on Zulip Andrew Ashworth (Jun 13 2018 at 12:19):

maybe I should just try it out with the helpful reflection template that's just been posted :)

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 16:03):

def poly.is_eq_aux : list znum -> list znum -> bool
| [] [] := tt
| [] (h₂ :: t₂) := if (h₂ = 0) then poly.is_eq_aux [] t₂ else ff
| (h₁ :: t₁) [] := if (h₁ = 0) then poly.is_eq_aux t₁ [] else ff
| (h₁ :: t₁) (h₂ :: t₂) := if (h₁ = h₂) then poly.is_eq_aux t₁ t₂ else ff

def poly.is_eq : poly  poly  bool := poly.is_eq_aux

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 16:04):

[recursion on poly doesn't seem to work]

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 16:04):

theorem poly.eval_is_eq {α} [comm_ring α] (X : α) {p₁ p₂ : poly} :
  poly.is_eq p₁ p₂  p₁.eval X = p₂.eval X :=
begin
  revert p₂,
  induction p₁ with h₁ t₁ H₁,
  { intros p₂ H,
    induction p₂ with h₁ t₁ H₂,refl,
    unfold poly.eval,
    unfold poly.is_eq poly.is_eq_aux at H,
    split_ifs at H,swap,cases H,
    rw [h,H₂ H],
    simp,
  },
  { intros p₂ H,
    induction p₂ with h₂ t₂ H₂,
    { unfold poly.eval,
      unfold poly.is_eq poly.is_eq_aux at H,
      split_ifs at H,swap,cases H,
      rw [h,H₁ H],
      simp
    },
    { unfold poly.eval,
      unfold poly.is_eq poly.is_eq_aux at H,
      split_ifs at H,swap,cases H,
      unfold poly.is_eq at H₂,
      rw [h,H₁ H]
    }
  }

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 16:04):

and then all we need is

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 16:05):

theorem main_thm {α} [comm_ring α] (X : α) (e₁ e₂) {x₁ x₂}
  (H : poly.is_eq (to_poly e₁) (to_poly e₂)) (R1 : e₁.eval X = x₁) (R2 : e₂.eval X = x₂) : x₁ = x₂ :=
by rw [ R1,  R2,  to_poly_eval,poly.eval_is_eq X H, to_poly_eval]

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 16:05):

example (x : ) : (x + 1) * (x + 1) = x*x+2*x+1 := by do ring_tac ```(x)

example (x : ) : (x + 1) + ((-1)*x + 1) = 2 := by do ring_tac ```(x)

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 16:05):

they both work :-)

view this post on Zulip Mario Carneiro (Jun 13 2018 at 22:56):

I wouldn't recommend using a quotient, although it probably won't hurt

view this post on Zulip Mario Carneiro (Jun 13 2018 at 22:56):

The VM can erase that stuff but the kernel has to deal with it all

view this post on Zulip Mario Carneiro (Jun 13 2018 at 22:56):

if you keep all the functions simple and nondependent, the kernel doesn't have to carry around all the proof garbage

view this post on Zulip Mario Carneiro (Jun 13 2018 at 22:56):

for the reason of "working with a handicap" I mentioned

view this post on Zulip Mario Carneiro (Jun 13 2018 at 23:11):

Your definition didn't work on poly because it uses well founded recursion, which is another kernel no-no (it has to unfold the well foundedness proofs)

view this post on Zulip Mario Carneiro (Jun 13 2018 at 23:11):

Try this instead:

def poly.is_zero : poly → bool
| [] := tt
| (h :: t) := (h = 0) && poly.is_zero t

def poly.is_eq : poly → poly → bool
| l₁ [] := poly.is_zero l₁
| [] l₂ := poly.is_zero l₂
| (h₁ :: t₁) (h₂ :: t₂) := if (h₁ = h₂) then poly.is_eq t₁ t₂ else ff

(sorry for all the proof obligations!)

view this post on Zulip Mario Carneiro (Jun 13 2018 at 23:13):

(Alternatively, if you defined subtraction or an equivalent you could use only is_zero and define is_eq by (p1 - p2).is_zero)

view this post on Zulip Kevin Buzzard (Jun 14 2018 at 07:07):

Why bool and not Prop?

view this post on Zulip Moses Schönfinkel (Jun 14 2018 at 07:11):

He did it on purpose to prompt this question! ;)

view this post on Zulip Kevin Buzzard (Jun 14 2018 at 08:52):

https://xenaproject.wordpress.com/2018/06/13/ab3/

view this post on Zulip Kevin Buzzard (Jun 14 2018 at 08:53):

Comments welcome. That's how some baby version of tactic.ring works, at least. And of course many thanks to Mario, without whom that little project would have taken far longer to complete.

view this post on Zulip Kevin Buzzard (Jun 14 2018 at 08:53):

I know the post is mega-long but I am not sure I care.

view this post on Zulip Johan Commelin (Jun 14 2018 at 09:01):

This is chapter 3 of your book?

view this post on Zulip Andrew Ashworth (Jun 14 2018 at 11:23):

I read and enjoyed your blog post! My only comment is perhaps you might have a further reading section. It would be a good place to link http://adam.chlipala.net/cpdt/html/Reflection.html and https://softwarefoundations.cis.upenn.edu/vfa-current/Decide.html#lab185 for people who are trying to seriously write a reflective tactic (although, unfortunately, you have to read Coq to understand what's going on... but I think at this stage of Lean's popularity, this is somewhat necessary regardless in the tactics game). Also, minor nitpick, but znum is only uber-efficient when it is used in rfl proofs, otherwise int has special fast support

view this post on Zulip Kevin Buzzard (Jun 14 2018 at 14:31):

Many thanks Andrew. I am not a computer scientist as I'm sure you know and I don't really know about references. I have looked, briefly, at both of the things you mention, but I have never really substantially engaged with them -- I tend to stop reading when things get "too CS" because they become less relevant to what I am trying to do in Lean. Thanks for the nitpick too.

view this post on Zulip Mario Carneiro (Jun 14 2018 at 14:33):

Why bool and not Prop?

Because you can't compute with Props. You could get roughly the same behavior by using decidable p instead of bool (+ soundness proof), but since there are more dependency tricks there I suspect it's marginally slower than using bool (but not by any large margin).

view this post on Zulip Mario Carneiro (Jun 14 2018 at 14:36):

In this case, the bool definition functions both as the relation itself and its decidability proof. If you wanted to use decidable, then, it would be two definitions and a soundness proof

view this post on Zulip Kevin Buzzard (Jun 14 2018 at 17:03):

This is chapter 3 of your book?

I am not sure if this is book material.


Last updated: May 08 2021 at 09:11 UTC