ring tactic works at one place, fails at another

Stream: new members

[Joe]

see the following example:

[Joe]

import analysis.normed_space.basic
import data.real.basic

universes u v w

variables {α : Type u} {F : Type v} {G : Type w}

class has_inner (α : Type*) := (inner : α → α → ℝ)

export has_inner (inner)

class inner_product_space (α : Type*) [add_comm_group α] [vector_space ℝ α] extends has_inner α :=
sorry

variables [add_comm_group α] [vector_space ℝ α] [inner_product_space α]

instance inner_product_space_has_norm : has_norm α := sorry

lemma foo {x y : ℝ} :  2 * ((x + y) * (x + y) + (x + y) * (x + y)) - 4 * x * x =
             8 * x * y + 4 * y * y :=
begin ring end -- goals accomplished

instance inner_product_space_is_normed_group : normed_group α := sorry

lemma bar {x y : ℝ} :  2 * ((x + y) * (x + y) + (x + y) * (x + y)) - 4 * x * x =
             8 * x * y + 4 * y * y :=
begin ring end -- doesn't work

[Kenny Lau]

what

[Johan Commelin]

Ouch, that looks painful.

[Johan Commelin]

Does this error go away if you fill in the sorry? Does it help to put a . after the sorry? (I'm just applying cargo cult to the problem.)

[Mario Carneiro]

The thing that surprises me the most is

class inner_product_space (α : Type*) [add_comm_group α] [vector_space ℝ α] extends has_inner α :=
sorry

I didn't know that was a valid parse, and I've read the structure parser

[Johan Commelin]

Well, it's not clear that it is actually a valid parse, is it?

[Johan Commelin]

Isn't it still eating all the garbage after it?

[Johan Commelin]

/me has not read the structure parser

[Mario Carneiro]

I am assuming the above is valid lean from its presence in the example

[Mario Carneiro]

If it was garbage, then inner_product_space would not have been defined and the rest of the example would be errors everywhere

[Mario Carneiro]

I put the example in lean, and indeed that line is invalid. But apparently the parser doesn't give up completely, and treats it as

class inner_product_space (α : Type*) [add_comm_group α] [vector_space ℝ α] extends has_inner α

[Mario Carneiro]

As for the actual question, I think the problem is all the sorrys

[Johan Commelin]

sorry is an unreliable tactic :stuck_out_tongue_wink:

[Mario Carneiro]

I don't see why normed_group real is derivable here atm, but it is probably breaking the interpretation of + vs *

[Mario Carneiro]

ring infers a comm_semiring instance once and for all and gets the operations from that. So real -> comm_semiring -> has_add should infer defeq to real -> has_add

[Mario Carneiro]

In this case I think the new instance, which is defined as sorry and so has no useful defeqs, is breaking this

[Johan Commelin]

Does that mean that the example works again if you change real to rat?

[Mario Carneiro]

I don't know, my mind is working faster than lean right now

[Mario Carneiro]

My theory doesn't work. both the initial goal and the inference of comm_ring real and comm_semiring real are unchanged by the instance

[Mario Carneiro]

Aha, here's a relevant minimized version:

import tactic.ring

constant real : Type
notation `ℝ` := real
instance : comm_ring ℝ := sorry

variables {α : Type u}

class normed_group (α : Type*) extends add_comm_group α

class inner_product_space (α : Type*)

variables [add_comm_group α] [inner_product_space α]

lemma foo {x y : ℝ} :
  2 * ((x + y) * (x + y) + (x + y) * (x + y)) - 4 * x * x = 8 * x * y + 4 * y * y :=
by ring -- goals accomplished

instance inner_product_space_is_normed_group : normed_group α := sorry

lemma bar {x y : ℝ} : -- instance loop
  2 * ((x + y) * (x + y) + (x + y) * (x + y)) - 4 * x * x = 8 * x * y + 4 * y * y :=
by ring

[Mario Carneiro]

The problem is that inner_product_space_is_normed_group introduces an instance loop, because add_comm_group + inner_product_space -> normed_group -> add_comm_group

[Mario Carneiro]

The solution is to have inner_product_space A extend add_comm_group A rather than taking it as a parameter

[Joe]

Thank you. It solves the problem.

[Johan Commelin]

@Mario Carneiro Is that the correct solution, or should in fact normed_group be refactored to not exten add_comm_group? The whole point of assuming [add_comm_group A] was to allow flexibility in the scalar ring. This now seems to become harder...

[Mario Carneiro]

I don't follow. You don't get any extra flexibility either way

[Mario Carneiro]

Is a normed_group necessarily an add_comm_group or not? (in maths)

[Mario Carneiro]

I think there is some argument for noncommutative groups with an appropriate norm

[Mario Carneiro]

but regardless this changes nothing. If we want to refactor normed_group to depend on only add_group we can do that with either definition

[Mario Carneiro]

The general rule is to use a parameter if the class involves more types than the parent (e.g. a module needs two types, but it depends on structures on the individual types). In this case inner_product_space is unary and depends on add_comm_group which is also unary, so it should inherit

[Johan Commelin]

Aha, I see.

[Johan Commelin]

So this becomes an issue as soon as we want inner products over more general fields than the reals

[Mario Carneiro]

An inner product over a more general field would not have the instance inner_product_space_is_normed_group, that would be a parameter

[Johan Commelin]

Thanks for bringing me back on track