fix this unfold?

Stream: new members

[Michael Beeson]

reserve infix ` ∈ ` : 49

section TEST
class  Model (M:Type) :=
(𝔽:M)
(succ:M)
(Λ:M)
(mem : M → M → Prop)
(infix  ∈ :=  mem )
(SSC: M → M)
(emptyset_axiom:   ∀ x, (¬ x ∈ Λ ))
 /- end of class definition because next line doesn't declare a member -/

variables (M:Type) [Model M] (a b x y z u v w X R W: M)

open Model
infix  ∈ :=  mem

def SSC:M→M :=  λ u, Λ

lemma ssc_members: ∀ (X u:M), ¬ (u ∈ (SSC X)) :=
  assume X u,
  begin
     unfold SSC,
  end

 end TEST

Why won't this unfold work? if you comment it out there are no errors.

[Mario Carneiro]

unfold takes a name, not an expression

[Mario Carneiro]

so just write unfold SSC

[Michael Beeson]

well, that didn't work, because SSC wasn't defined, I tried to define (SSC X) which I mis-wrote as SSC(X), but you can only define an identifier.

[Mario Carneiro]

To lean those are the same thing

[Mario Carneiro]

def SSC (X : M) : M := ... is the same as def SSC : M -> M := \lam x, ...

[Michael Beeson]

OK, but before I got a whole screenful of errors, and now I only get
unfold tactic failed, SSC does not have equational lemmas nor is a projection

[Mario Carneiro]

if you write rw SSC you get a more helpful error message:

ambiguous overload, possible interpretations
  SSC
  Model.SSC

[Mario Carneiro]

The problem is that Model has a field SSC, and you wrote open Model so you can refer to it as SSC, but then you defined another (different) definition SSC and lean doesn't know which you mean

[Michael Beeson]

I thought that after open Model, SSC would be Model.SSC.

[Mario Carneiro]

It's both

[Mario Carneiro]

because you defined another SSC and now there is a name clash

[Mario Carneiro]

The SSC in the theorem statement is Model.SSC, which lean was able to figure out because the M in _root_.SSC is explicit

[Mario Carneiro]

You should write either _root_.SSC or Model.SSC to disambiguate, or better yet remove the ambiguity

[Michael Beeson]

What is _root_?

[Mario Carneiro]

it's a fake namespace you can use to explicitly say "I want the one in the root namespace"

[Mario Carneiro]

whose name is just plain SSC

[Michael Beeson]

OK thanks, now I understand what happened here.

[Michael Beeson]

in the example, within the class I "declared" SSC:M->M. But I did not "define" it, i.e. gave no rule to determine its values.
Now, If I did that within the class all would be well. But for some irrelevant reason, I want to do it OUTSIDE the class. If I try to change
the definition outside the class (leaving the declaration inside) I get "invalid definition, a declaration named 'Model.SSC' has already been declared".
So Lean doesn't seem to distinguish between declaration and definition, and as posted, the code defines a SECOND SSC, this time in
the "root namespace". It seems like theoretically every instance M of the class Model could have its own SSC and that one could have different definitions in different M's, that should be allowed by not giving the definition inside the class but only the declaration. But that didn't work out:
instead Lean now has two functions called SSC, one declared as part of Model, but with no "body", and one only working on the instance M,
but utterly different than the SSC defined inside class Model. So I failed to tell Lean, "Now I am supplying a definition for Model.SSC that will apply
in this instance of the class." Now my question is, is there a way to do that? Or should I just get over the idea of doing that and define SSC within the class?

[Mario Carneiro]

The structure defines a single function, called Model.SSC, which has the type Model.SSC : \all (M : Type) [Model M], M -> M. It is an actual definition - it is basically a projection function, because Model M is a tuple of a bunch of things and this extracts one component

[Mario Carneiro]

Different instances of Model will tuple up different things, and so the effect of Model.SSC applied to them will give different projections. But there is nevertheless only one function Model.SSC defined once and for all

[Mario Carneiro]

I would give you more pointed advice but I'm still not exactly sure what your aim is. What is SSC supposed to mean, and what are you trying to get out of it?