## Stream: general

### Topic: how does tactic.ring work?

#### 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).

#### Kevin Buzzard (Jun 11 2018 at 08:28):

Anyway, I started to read it:

#### Kevin Buzzard (Jun 11 2018 at 08:28):

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

#### 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

#### 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

#### 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)

#### 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:

#### Kevin Buzzard (Jun 11 2018 at 08:31):

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

#### 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.

#### 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/

#### 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)

#### 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.

#### 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


#### 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
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


etc etc

#### Kevin Buzzard (Jun 12 2018 at 09:41):

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

#### Kevin Buzzard (Jun 12 2018 at 09:42):

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

#### Kevin Buzzard (Jun 12 2018 at 09:42):

But I want to fix it.

#### 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.

#### 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.

#### Kevin Buzzard (Jun 12 2018 at 09:43):

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

#### 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

#### 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"

#### Kevin Buzzard (Jun 12 2018 at 09:44):

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

#### Kevin Buzzard (Jun 12 2018 at 09:45):

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

#### Kevin Buzzard (Jun 12 2018 at 09:45):

This makes it clear what we have to do here.

#### Kevin Buzzard (Jun 12 2018 at 09:46):

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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 09:46):

we will need polynomials in a finite set of variables.

#### Kevin Buzzard (Jun 12 2018 at 09:46):

Of course Lean has these.

#### 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)$ in our polynomial ring

#### Kevin Buzzard (Jun 12 2018 at 09:47):

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

#### 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)$ and so on

#### Kevin Buzzard (Jun 12 2018 at 09:49):

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

#### Kevin Buzzard (Jun 12 2018 at 09:49):

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

#### Kevin Buzzard (Jun 12 2018 at 09:49):

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

#### Kevin Buzzard (Jun 12 2018 at 09:49):

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

#### 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.

(+,^,2,1)

#### Kevin Buzzard (Jun 12 2018 at 09:51):

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

#### 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?

#### Kevin Buzzard (Jun 12 2018 at 09:57):

Or is life not even that easy?

#### 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.

#### 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.)

#### Simon Hudon (Jun 12 2018 at 12:04):

Is this simply renaming variables in the goal?

#### 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).

#### 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

#### Kevin Buzzard (Jun 12 2018 at 12:47):

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

#### Simon Hudon (Jun 12 2018 at 12:48):

ah! i see. So a kind of parser.

#### 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.

#### Kevin Buzzard (Jun 12 2018 at 12:48):

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

#### 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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 12:49):

Here is a concrete question.

#### Kevin Buzzard (Jun 12 2018 at 12:49):

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

#### Kevin Buzzard (Jun 12 2018 at 12:49):

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

I believe so

#### Kevin Buzzard (Jun 12 2018 at 12:49):

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

#### 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"

#### 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

#### Kevin Buzzard (Jun 12 2018 at 12:50):

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

#### Kevin Buzzard (Jun 12 2018 at 12:50):

and then evaluating at d

#### Kevin Buzzard (Jun 12 2018 at 12:50):

and deducing the result?

#### 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?

#### 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

#### Kevin Buzzard (Jun 12 2018 at 12:53):

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

#### 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"

#### Kevin Buzzard (Jun 12 2018 at 12:58):

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

#### 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

right

#### Kevin Buzzard (Jun 12 2018 at 12:58):

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

#### Kevin Buzzard (Jun 12 2018 at 12:59):

and returned X^2+2*X+1

#### Simon Hudon (Jun 12 2018 at 12:59):

I see ok yes that's possible

#### Simon Hudon (Jun 12 2018 at 12:59):

That's called a proof by reflection

#### 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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 13:00):

because I feed in both sides to the tactic

#### Kevin Buzzard (Jun 12 2018 at 13:00):

prove they're equal in ZX

#### Kevin Buzzard (Jun 12 2018 at 13:00):

and deduce that their valuations are equal

#### 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

#### 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?

#### Reid Barton (Jun 12 2018 at 13:01):

In particular page 4

#### 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

to

#### 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 $\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 $\mathbb{Z}[X]$ are equal so that it can decide whether to succeed or fail.

#### Kevin Buzzard (Jun 12 2018 at 13:04):

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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 13:05):

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

#### 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

right

#### 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

right

#### Kevin Buzzard (Jun 12 2018 at 13:07):

or there could be several variables

#### 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.

#### Reid Barton (Jun 12 2018 at 13:09):

BTW, _ty probably just stands for "type"

#### Kevin Buzzard (Jun 12 2018 at 13:11):

So completely independent of the ring tactic

#### Kevin Buzzard (Jun 12 2018 at 13:11):

there is this horner thing

#### Kevin Buzzard (Jun 12 2018 at 13:11):

and what seems to be going on there

#### Kevin Buzzard (Jun 12 2018 at 13:11):

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

#### Kevin Buzzard (Jun 12 2018 at 13:11):

storing polynomials as lists of coefficients might suck

#### Kevin Buzzard (Jun 12 2018 at 13:12):

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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 13:12):

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

#### Kevin Buzzard (Jun 12 2018 at 13:13):

and so this is some sort of normal form for polynomials

#### Kevin Buzzard (Jun 12 2018 at 13:13):

which we could call "horner normal form"

#### 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

#### Kevin Buzzard (Jun 12 2018 at 13:13):

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

#### 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?

#### 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)

#### Kevin Buzzard (Jun 12 2018 at 13:14):

where you just use lists for coefficients

#### Kevin Buzzard (Jun 12 2018 at 13:15):

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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 13:15):

instead of making Z[X] in meta-land

#### 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"

#### Kevin Buzzard (Jun 12 2018 at 13:18):

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

#### Kevin Buzzard (Jun 12 2018 at 13:18):

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

#### Kevin Buzzard (Jun 12 2018 at 13:18):

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

#### 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

both ways around

#### Kevin Buzzard (Jun 12 2018 at 13:18):

and there's some implicit inductive type horner_form

#### 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

#### Kevin Buzzard (Jun 12 2018 at 13:19):

and then every polynomial has a canonical horner form

#### Kevin Buzzard (Jun 12 2018 at 13:19):

and also perhaps some non-canonical ones

#### 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)

#### 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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 13:29):

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

#### Kevin Buzzard (Jun 12 2018 at 13:29):

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

#### 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.

#### 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.

#### Kevin Buzzard (Jun 12 2018 at 13:43):

Well maybe that's where this thread is going.

#### Mario Carneiro (Jun 12 2018 at 13:47):

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

#### 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)

#### Mario Carneiro (Jun 12 2018 at 13:48):

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

#### Mario Carneiro (Jun 12 2018 at 13:49):

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

#### Simon Hudon (Jun 12 2018 at 13:50):

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

#### 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

#### Reid Barton (Jun 12 2018 at 13:51):

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

#### Reid Barton (Jun 12 2018 at 13:51):

not necessarily short

#### 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

#### Mario Carneiro (Jun 12 2018 at 13:52):

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

#### Mario Carneiro (Jun 12 2018 at 13:52):

which would have to avoid certain meta things like macros

#### 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".

#### 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"

#### Kevin Buzzard (Jun 12 2018 at 14:02):

and that's why I find myself in this thread

#### 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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 14:03):

I currently find myself doing both

#### 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

#### 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

#### 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

#### 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

#### 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

#### 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.

#### Mario Carneiro (Jun 12 2018 at 15:03):

destruct is effectively the cases_on for this inductive type

#### 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)

#### 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

#### 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

#### 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

#### 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)

#### Mario Carneiro (Jun 12 2018 at 15:42):

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

#### Kevin Buzzard (Jun 12 2018 at 15:42):

The tactic would only work for goals with one unknown

#### Mario Carneiro (Jun 12 2018 at 15:42):

but you have to remember these are multivariate polynomials

I know yours are

#### Kevin Buzzard (Jun 12 2018 at 15:42):

but I am suggesting writing a simplified version

#### 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

#### Mario Carneiro (Jun 12 2018 at 15:43):

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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 15:44):

I know your approach is better at getting things done

#### Kevin Buzzard (Jun 12 2018 at 15:44):

I am happy to let both d and Z be inputs

#### Mario Carneiro (Jun 12 2018 at 15:44):

but you want to have only one atom

right

#### Kevin Buzzard (Jun 12 2018 at 15:44):

and I want to store polynomials as lists

#### Kevin Buzzard (Jun 12 2018 at 15:44):

these facts are not unrelated

#### Mario Carneiro (Jun 12 2018 at 15:44):

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

#### Kevin Buzzard (Jun 12 2018 at 15:45):

my function will fail

#### Kevin Buzzard (Jun 12 2018 at 15:45):

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

#### Kevin Buzzard (Jun 12 2018 at 15:45):

not to actually be used in the wild

#### Kevin Buzzard (Jun 12 2018 at 15:45):

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

#### Kevin Buzzard (Jun 12 2018 at 15:45):

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

#### Kevin Buzzard (Jun 12 2018 at 15:46):

which is not the impression you get when reading PIL

#### Mario Carneiro (Jun 12 2018 at 15:46):

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

:D

#### Kevin Buzzard (Jun 12 2018 at 15:47):

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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 15:47):

dammit I even looked at that function!

#### Mario Carneiro (Jun 12 2018 at 15:47):

It's funny, the theorem is not wrong

#### Mario Carneiro (Jun 12 2018 at 15:48):

but it doesn't normalize like it should

#### Kevin Buzzard (Jun 12 2018 at 15:48):

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

#### 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₂) -/

#### 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.

#### 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'

#### 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)

#### Mario Carneiro (Jun 12 2018 at 15:50):

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

#### Kevin Buzzard (Jun 12 2018 at 15:50):

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

#### Mario Carneiro (Jun 12 2018 at 15:51):

Yes. In particular, x might appear in a2

or a1

;-)

that's okay

#### Kevin Buzzard (Jun 12 2018 at 15:52):

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

#### Kevin Buzzard (Jun 12 2018 at 15:52):

[you only did half the editing job]

#### 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

a2 * x^k + a1

#### Kevin Buzzard (Jun 12 2018 at 15:53):

I think this part of the thread is now beyond saving

#### Kevin Buzzard (Jun 12 2018 at 15:54):

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

fixed

#### 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

#### Mario Carneiro (Jun 12 2018 at 15:56):

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

#### 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]

#### Kevin Buzzard (Jun 12 2018 at 15:57):

Right, so let's focus on gt

#### 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'

#### 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₂) -/

#### Mario Carneiro (Jun 12 2018 at 15:58):

so I did that and now it works

#### Mario Carneiro (Jun 12 2018 at 15:58):

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

#### Kevin Buzzard (Jun 12 2018 at 15:58):

I would have liked to find this bug

#### 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

#### Kevin Buzzard (Jun 12 2018 at 15:59):

you just write procedural code which is supposed to do it

#### Kevin Buzzard (Jun 12 2018 at 16:00):

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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 16:01):

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

#### 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

#### 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

#### Mario Carneiro (Jun 12 2018 at 16:05):

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

#### Mario Carneiro (Jun 12 2018 at 16:05):

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

#### Mario Carneiro (Jun 12 2018 at 16:06):

so the kernel never has to do any definitional reduction

#### 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

#### 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₂,
| (%%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.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


#### 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.

#### Mario Carneiro (Jun 12 2018 at 17:35):

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

#### Mario Carneiro (Jun 12 2018 at 17:36):

you will need the mathlib update that just appeared

#### Kevin Buzzard (Jun 12 2018 at 19:47):

wooah many thanks Mario!

#### 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

#### Kevin Buzzard (Jun 12 2018 at 20:11):

but 12 times out :-)

#### Kevin Buzzard (Jun 12 2018 at 20:11):

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

#### 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

#### Johan Commelin (Jun 12 2018 at 20:31):

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

#### 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 :-)

#### 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.

#### 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₂,
| (%%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.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₂,
rw (H t₂),
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,
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,
unfold poly.eval,
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


Did my homework

#### Kevin Buzzard (Jun 12 2018 at 23:06):

I feel like an UG again

#### 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.

#### Kenny Lau (Jun 12 2018 at 23:08):

did you just write a tactic?

Not really

#### Kevin Buzzard (Jun 12 2018 at 23:08):

in the sense that no code I wrote started with meta

but check it out

#### Kevin Buzzard (Jun 12 2018 at 23:09):

barely any code at all has meta

#### 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

#### 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

#### 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

#### Kevin Buzzard (Jun 12 2018 at 23:11):

so this part you have to do in meta-land

#### Kevin Buzzard (Jun 12 2018 at 23:11):

but it's only this part

#### Kevin Buzzard (Jun 12 2018 at 23:11):

unsurprisingly, this is what reflect_expr does

#### 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.

#### 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.

#### 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

#### 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.

#### 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?

#### 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

#### Kevin Buzzard (Jun 13 2018 at 09:58):

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

#### Kevin Buzzard (Jun 13 2018 at 09:58):

Aah, I think I can fix this.

#### Kevin Buzzard (Jun 13 2018 at 09:58):

I think I write some "canonical_form" function

#### Kevin Buzzard (Jun 13 2018 at 09:58):

(not in meta land)

#### Kevin Buzzard (Jun 13 2018 at 09:59):

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

#### Kevin Buzzard (Jun 13 2018 at 09:59):

yeah yeah OK I think I can do this one.

#### 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

#### 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

#### 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)

#### 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

#### 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

#### 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

#### 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

#### 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.

#### 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

#### 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

#### 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?

#### 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 :)

#### 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


#### Kevin Buzzard (Jun 13 2018 at 16:04):

[recursion on poly doesn't seem to work]

#### 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]
}
}


#### Kevin Buzzard (Jun 13 2018 at 16:04):

and then all we need is

#### 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]


#### 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)


#### Kevin Buzzard (Jun 13 2018 at 16:05):

they both work :-)

#### Mario Carneiro (Jun 13 2018 at 22:56):

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

#### Mario Carneiro (Jun 13 2018 at 22:56):

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

#### 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

#### Mario Carneiro (Jun 13 2018 at 22:56):

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

#### 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)

#### Mario Carneiro (Jun 13 2018 at 23:11):

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!)

#### 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)

#### Kevin Buzzard (Jun 14 2018 at 07:07):

Why bool and not Prop?

#### Moses Schönfinkel (Jun 14 2018 at 07:11):

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

#### Kevin Buzzard (Jun 14 2018 at 08:52):

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

#### 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.

#### Kevin Buzzard (Jun 14 2018 at 08:53):

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

#### Johan Commelin (Jun 14 2018 at 09:01):

This is chapter 3 of your book?

#### 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

#### 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.

#### 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).

#### 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

#### 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