ring_nf changes goal twice

Stream: new members

[Bolton Bailey]

In the following snippet, applying ring_nf two times in a row changes the state twice. I would expect a tactic that puts an expression in a "normal form" to not change that expression again when it sees an expression that is putatively already in that normal form. What is going on here?

import data.real.basic

example (a b c : ℝ) : a * c + b * c = 0 :=
begin
  ring_nf, -- c * a + b * c = 0
  ring_nf, -- (a + b) * c = 0
  ring_nf, -- c * a + c * b = 0
end

[Alex J. Best]

I would guess this is the same issue as #5711, ring_nf normalizes given a fixed order on the atoms, but when it is run again it picks a different order, as the ordering is based on the order it sees the atoms.

[Will Sawin]

I wonder if this operation can be periodic with arbitrarily large period

[Bolton Bailey]

Is there any way to tell ring_nf to use a particular order?

[Yakov Pechersky]

have : a * b * d * c = a * b * c * d := by ring_nf,
rw this

[Bolton Bailey]

@Yakov Pechersky Indeed this is my current solution. But my expression takes ~15 lines to write out, so I'm looking for a way of doing this that avoids writing out the expression itself.

In fact, I don't really need to put the whole thing in normal form, I just want to factor out a few expressions from the places they occur. Ideally, I would like a tactic where I just do something like specify a list of one or two expressions [e1, e2], and then I consistently get out something of the form e1 * (...) + e_2 * (...) + <contains no e1 or e2>.

[Yakov Pechersky]

change _ = e1 * _ + e2 * _ + _?

[Bolton Bailey]

Ok, that might work, let me try it out

[Bolton Bailey]

Unfortunately, it's not telling me it knows how to do this. Let me post a schematic of what I am trying to do. Here's what I have currently:

lemma reformat (a b c d e f g : F) :
  a * c + b * c + g + d * e + d * f = c * (a + b) + d * (e + f) + g
:=
begin
  ring_nf,
end

lemma main_theorem (a b c d e f g: F) (h1: a + b = 0) (h2: e + f = 0):
  a * c + b * c + g + d * e + d * f = g
:=
begin
  rw reformat,
  simp [h1, h2],
end

Except a,b,c,d,e,f are very big expressions. I want to be able to prove the main theorem without making this reformat lemma, because writing that all out takes a long time and it's not feasible to do that every time I want to do a new theorem similar to main theorem.

[Yakov Pechersky]

import tactic.ring

variables {F : Type*} [comm_ring F]

lemma reformat (a b c d e f g : F) :
  a * c + b * c + g + d * e + d * f = c * (a + b) + d * (e + f) + g :=
begin
  convert_to _ = d * _ + c * _ + _;
  ring_nf,
  ring_nf
end

[Bolton Bailey]

This suggestion also works for the reformat lemma, but my desire is to get rid of reformat entirely.

[Bolton Bailey]

After hunting around in tactic.ring, I found docs#tactic.ring.add_atom. I think what I would effectively like to do is call this on all the expressions I want in front, then make sure that when normalize is eventually called, it is called in this preexisting monadic environment. Would this work, and are there any tips on doing this?

[Mario Carneiro]

You shouldn't be using ring_nf in proofs anyway (in most cases). It was originally intended as a debugging tool. I can't imagine that you will get a better proof using this method than just multiplying the equations together

[Mario Carneiro]

Here's a proof which only requires you to specify c, d, g:

lemma main_theorem (a b c d e f g: F) (h1: a + b = 0) (h2: e + f = 0):
  a * c + b * c + g + d * e + d * f = g :=
begin
  have := congr_arg2 (+) (congr_arg (* c) h1) (congr_arg (* d) h2),
  refine (eq.trans _ (congr_arg (+ g) this)).trans _; ring
end

Ideally it would be easier to specify these sums of products of equations; see the zulip thread on ring_rw

[Johan Commelin]

Mario Carneiro said:

You shouldn't be using ring_nf in proofs anyway (in most cases). It was originally intended as a debugging tool. I can't imagine that you will get a better proof using this method than just multiplying the equations together

But ring nowadays regularly tells you Use this: ring_nf,

[Bolton Bailey]

Unfortunately, I would really like to avoid specifying g. To give you a sense of the reality of my situation, g is actually

(∑ (i : fin n_var) in finset.fin_range n_var, polynomial.C (A_x i) * polynomial.X ^ (i : ℕ)) *
            ∑ (i : fin n_var) in finset.fin_range n_var, polynomial.C (B_x i) * polynomial.X ^ (i : ℕ)

But this is not the real problem. The problem is when I go to formalize other SNARK constructions the equations will be different, and I have no idea if all of these variables will be different, or if there will be additional terms to the sum.

Here's something that I think will solve my problem: If I rewrite h1 and h2 to b = -a and f = -e, it seems like running ring_nf on the result should do what I want.

[Alex J. Best]

Presumably just running ring also works there?
I think a variant of ring_nf that allows you to specify the term order would be a good addition to mathlib.

[Eric Wieser]

Isn't finset.fin_range k just finset.univ?

[Mario Carneiro]

Johan Commelin said:

Mario Carneiro said:

You shouldn't be using ring_nf in proofs anyway (in most cases). It was originally intended as a debugging tool. I can't imagine that you will get a better proof using this method than just multiplying the equations together

But ring nowadays regularly tells you Use this: ring_nf,

It only says that when it "fails"

[Johan Commelin]

Alex J. Best said:

I would guess this is the same issue as #5711, ring_nf normalizes given a fixed order on the atoms, but when it is run again it picks a different order, as the ordering is based on the order it sees the atoms.

Could the order instead be based on lexicographical order of the pretty-printed names, or something like that? That should give a stable ordering in 99.9% of the cases.

[Mario Carneiro]

It used to use expr.lt as the order, but that had issues with defeq

[Mario Carneiro]

If you assume there are no defeq clashes, then that would work fine, but if a and d are defeq then depending on which order you visit a + b + c + d you might end up with the list a=d, b, c or b, c, d=a

[Mario Carneiro]

adding a pass to sort the atoms after collection will probably help in most cases though