Lean Prover Zulip Chat Archive

Stream: new members

Topic: ring tactic works at one place, fails at another


view this post on Zulip Joe (Jul 24 2019 at 23:18):

see the following example:

view this post on Zulip Joe (Jul 24 2019 at 23:18):

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

view this post on Zulip Kenny Lau (Jul 24 2019 at 23:21):

what

view this post on Zulip Johan Commelin (Jul 25 2019 at 01:52):

Ouch, that looks painful.

view this post on Zulip Johan Commelin (Jul 25 2019 at 01:53):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 01:54):

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

view this post on Zulip Johan Commelin (Jul 25 2019 at 01:56):

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

view this post on Zulip Johan Commelin (Jul 25 2019 at 01:56):

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

view this post on Zulip Johan Commelin (Jul 25 2019 at 01:57):

/me has not read the structure parser

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:00):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:01):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:06):

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 α

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:08):

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

view this post on Zulip Johan Commelin (Jul 25 2019 at 02:09):

sorry is an unreliable tactic :stuck_out_tongue_wink:

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:11):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:16):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:16):

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

view this post on Zulip Johan Commelin (Jul 25 2019 at 02:18):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:18):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:21):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:29):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:30):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 02:31):

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

view this post on Zulip Joe (Jul 25 2019 at 05:18):

Thank you. It solves the problem.

view this post on Zulip Johan Commelin (Jul 25 2019 at 06:42):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 06:43):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 06:43):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 06:43):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 06:44):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 06:46):

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

view this post on Zulip Johan Commelin (Jul 25 2019 at 06:47):

Aha, I see.

view this post on Zulip Johan Commelin (Jul 25 2019 at 06:48):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 06:48):

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

view this post on Zulip Johan Commelin (Jul 25 2019 at 06:49):

Thanks for bringing me back on track


Last updated: Feb 29 2020 at 02:00 UTC