defining something outside a class or inside

Stream: new members

[Michael Beeson]

I have a class Model with an operation 'multiplication' that I write infix as x*y. But I would like to
define it using some stuff that has been defined after the class definition. So after open Model I have
an instance M of my class and everything takes a parameter M, e.g., the class DECIDABLE M of
decidable members of M is defined. Now I want to use some of these things that I defined "outside" the
class (so they take a parameter M) to define * (which is built into the class). Of course I could define it
outside the class but then I would have product M x y instead of x*y and I don't think I can use infix notation
then (If I could that would be fine). Of course if I "knew then what i know now" I would have done a few
more things inside the class; but now I have hundreds of uses of those things. Does anyone have a helpful
suggestion, eg. a way to use infix notation for product M x y ?

If this were C++ the answer would be, make it a virtual function.

[Mario Carneiro]

There is no relation between infix notation and being defined inside the class

[Mario Carneiro]

infix mul is provided by the has_mul M typeclass, which you can prove after the definition with an instance

[Mario Carneiro]

Now I want to use some of these things that I defined "outside" the class (so they take a parameter M) to define * (which is built into the class).

This is a contradiction: if it's built into the class, then it's not defined, it's a field of the structure

[Mario Carneiro]

I think an #mwe would help here

[Michael Beeson]

class  Model (M:Type) :=
(mul:M → M → M)
(infix * := mul)
(zero:M)
(f:M → M → M)
(f_definition:∀ (x y:M), f x y = zero)
-- (multiplication_definition:∀ (x y:M), x*y = zero)
--I do not want to define it here!
 /- end of class definition because next line doesn't declare a member -/

variables (M:Type) [Model M] (a b x y: M)
open Model
infix * := mul

def mul(a b:M) [M] := f a b
--Can I get away with defining it here and still use infix?

lemma test: ∀ (x y:M), x*y = zero:=
  assume x y,
  begin
    -- rw multiplication_definition,
    --  can I finish this proof using the def of mul?
  end

[Mario Carneiro]

class Model (M : Type) :=
(zero : M)
(f : M → M → M)
(f_definition (x y : M) : f x y = zero)

variables (M : Type) [Model M] (a b x y: M)
open Model
instance Model.has_mul : has_mul M := ⟨f⟩

lemma mul_def (x y : M) : x * y = f x y := rfl

lemma test (x y : M) : x * y = zero :=
begin
  rw mul_def,
  rw f_definition,
end

[Michael Beeson]

Thank you Mario, it's the has_mul line that I was missing. But I also do not understand 'rfl'. I previously thought 'rfl' means, reduce the two sides of an equality and if you get the same normal form that counts as a proof, if not the tactic fails. Here, however, evidently something else is happening. You call mul_def a lemma but it's really just defining what * means. So are we just telling Lean, reduce x*y to f x y?

[Mario Carneiro]

no, it does exactly as you say, it reduces both sides to a normal form. mul_def isn't the definition, Model.has_mul is

[Mario Carneiro]

Specifically, Model.has_mul says "hey lean, when you need to prove has_mul M, try Model.has_mul M", and when you write x * y it actually means @has_mul.mul M _ x y where _ is a proof of has_mul M; lean will follow the above advice, and so you end up with

@has_mul.mul M (Model.has_mul M) x y

and since Model.has_mul M is defined to be ⟨f⟩ and has_mul.mul is defined to be projection out of this single-element class, the whole thing reduces to f x y, which is why rfl proves mul_def.

[Michael Beeson]

OK, I think I've understood your example. Here's one with one more feature, the definition of multiplication can depend on M.

class Model (M : Type) :=
(zero : M)
(f : M → M → M)
(f_definition (x y : M) : f x y = zero)

variables (M : Type) [Model M] (a b x y: M)
open Model

def foo (a b:M):M := f a b

instance Model.has_mul : has_mul M := ⟨foo M⟩

lemma mul_def (x y : M) : x * y = f x y := rfl


lemma test (x y : M) : x * y = zero :=
begin
  rw mul_def,
  rw f_definition,
end

[Michael Beeson]

Wel

[Mario Carneiro]

The definition already depended on M; f is actually @Model.f M _ where _ is an instance of type Model M

[Mario Carneiro]

The difference is that M is an implicit argument in f and explicit in foo, which you can see if you print the types:

#print f
-- def Model.f : Π {M : Type} [c : Model M], M → M → M :=

#print foo
-- def foo : Π (M : Type) [_inst_1 : Model M], M → M → M :=

[Mario Carneiro]

You can (and should) make M implicit in foo by setting the binder of M in the variables line:

variables {M : Type} [Model M] (a b x y: M)
open Model

def foo (a b:M):M := f a b
#print foo
-- def foo : Π {M : Type} [_inst_1 : Model M], M → M → M :=

instance Model.has_mul : has_mul M := ⟨foo⟩

lemma mul_def (x y : M) : x * y = f x y := rfl

[Michael Beeson]

Ah, (need light-bulb-over-the-head emoji) just by changing () to {} I could have avoided typing hundreds of explicit Ms.

[Michael Beeson]

I didn't think that variables line was doing anything to speak of as I freely use variables that are not in that list and nothing goes wrong.

[Mario Carneiro]

The variables line supplies variables automatically if you use them in a statement; but you have to either have declared the variable in a variables line or in the lemma statement itself. For example, the (x y : M) in mul_def are redundant because otherwise it would pick up x y : M from the (a b x y: M) in the variables, but if you used z in mul_def it would be an error, because z was never declared, either in the variables line or in the lemma arguments